1 /* PSPP - a program for statistical analysis.
2 Copyright (C) 2007, 2009 Free Software Foundation, Inc.
4 This program is free software: you can redistribute it and/or modify
5 it under the terms of the GNU General Public License as published by
6 the Free Software Foundation, either version 3 of the License, or
7 (at your option) any later version.
9 This program is distributed in the hope that it will be useful,
10 but WITHOUT ANY WARRANTY; without even the implied warranty of
11 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 GNU General Public License for more details.
14 You should have received a copy of the GNU General Public License
15 along with this program. If not, see <http://www.gnu.org/licenses/>. */
19 #include <libpspp/model-checker.h>
29 #include <libpspp/bit-vector.h>
30 #include <libpspp/compiler.h>
31 #include <libpspp/deque.h>
32 #include <libpspp/misc.h>
33 #include <libpspp/str.h>
39 /* Initializes PATH as an empty path. */
41 mc_path_init (struct mc_path *path)
48 /* Copies the contents of OLD into NEW. */
50 mc_path_copy (struct mc_path *new, const struct mc_path *old)
52 if (old->length > new->capacity)
54 new->capacity = old->length;
56 new->ops = xnmalloc (new->capacity, sizeof *new->ops);
58 new->length = old->length;
59 memcpy (new->ops, old->ops, old->length * sizeof *new->ops);
62 /* Adds OP to the end of PATH. */
64 mc_path_push (struct mc_path *path, int op)
66 if (path->length >= path->capacity)
67 path->ops = xnrealloc (path->ops, ++path->capacity, sizeof *path->ops);
68 path->ops[path->length++] = op;
71 /* Removes and returns the operation at the end of PATH. */
73 mc_path_pop (struct mc_path *path)
75 int back = mc_path_back (path);
80 /* Returns the operation at the end of PATH. */
82 mc_path_back (const struct mc_path *path)
84 assert (path->length > 0);
85 return path->ops[path->length - 1];
90 mc_path_destroy (struct mc_path *path)
96 /* Returns the operation in position INDEX in PATH.
97 INDEX must be less than the length of PATH. */
99 mc_path_get_operation (const struct mc_path *path, size_t index)
101 assert (index < path->length);
102 return path->ops[index];
105 /* Returns the number of operations in PATH. */
107 mc_path_get_length (const struct mc_path *path)
112 /* Appends the operations in PATH to STRING, separating each one
113 with a single space. */
115 mc_path_to_string (const struct mc_path *path, struct string *string)
119 for (i = 0; i < mc_path_get_length (path); i++)
122 ds_put_char (string, ' ');
123 ds_put_format (string, "%d", mc_path_get_operation (path, i));
127 /* Search options. */
130 /* Search strategy. */
131 enum mc_strategy strategy; /* Type of strategy. */
132 int max_depth; /* Limit on depth (or INT_MAX). */
133 int hash_bits; /* Number of bits to hash (or 0). */
134 unsigned int seed; /* Random seed for MC_RANDOM
135 or MC_DROP_RANDOM. */
136 struct mc_path follow_path; /* Path for MC_PATH. */
138 /* Queue configuration. */
139 int queue_limit; /* Maximum length of queue. */
140 enum mc_queue_limit_strategy queue_limit_strategy;
141 /* How to choose state to drop
144 /* Stop conditions. */
145 int max_unique_states; /* Maximum unique states to process. */
146 int max_errors; /* Maximum errors to detect. */
147 double time_limit; /* Maximum time in seconds. */
149 /* Output configuration. */
150 int verbosity; /* 0=low, 1=normal, 2+=high. */
151 int failure_verbosity; /* If greater than verbosity,
152 verbosity of error replays. */
153 FILE *output_file; /* File to receive output. */
155 /* How to report intermediate progress. */
156 int progress_usec; /* Microseconds between reports. */
157 mc_progress_func *progress_func; /* Function to call on each report. */
163 /* Default progress function. */
165 default_progress (struct mc *mc)
167 if (mc_results_get_stop_reason (mc_get_results (mc)) == MC_CONTINUING)
174 /* Do-nothing progress function. */
176 null_progress (struct mc *mc UNUSED)
181 /* Creates and returns a set of options initialized to the
184 mc_options_create (void)
186 struct mc_options *options = xmalloc (sizeof *options);
188 options->strategy = MC_BROAD;
189 options->max_depth = INT_MAX;
190 options->hash_bits = 20;
192 mc_path_init (&options->follow_path);
194 options->queue_limit = 10000;
195 options->queue_limit_strategy = MC_DROP_RANDOM;
197 options->max_unique_states = INT_MAX;
198 options->max_errors = 1;
199 options->time_limit = 0.0;
201 options->verbosity = 1;
202 options->failure_verbosity = 2;
203 options->output_file = stdout;
204 options->progress_usec = 250000;
205 options->progress_func = default_progress;
212 /* Returns a copy of the given OPTIONS. */
214 mc_options_clone (const struct mc_options *options)
216 return xmemdup (options, sizeof *options);
219 /* Destroys OPTIONS. */
221 mc_options_destroy (struct mc_options *options)
223 mc_path_destroy (&options->follow_path);
227 /* Returns the search strategy used for OPTIONS. The choices
230 - MC_BROAD (the default): Breadth-first search. First tries
231 all the operations with depth 1, then those with depth 2,
232 then those with depth 3, and so on.
234 This search algorithm finds the least number of operations
235 needed to trigger a given bug.
237 - MC_DEEP: Depth-first search. Searches downward in the tree
238 of states as fast as possible. Good for finding bugs that
239 require long sequences of operations to trigger.
241 - MC_RANDOM: Random-first search. Searches through the tree
242 of states in random order. The standard C library's rand
243 function selects the search path; you can control the seed
244 passed to srand using mc_options_set_seed.
246 - MC_PATH: Explicit path. Applies an explicitly specified
247 sequence of operations. */
249 mc_options_get_strategy (const struct mc_options *options)
251 return options->strategy;
254 /* Sets the search strategy used for OPTIONS to STRATEGY.
256 This function cannot be used to set MC_PATH as the search
257 strategy. Use mc_options_set_follow_path instead. */
259 mc_options_set_strategy (struct mc_options *options, enum mc_strategy strategy)
261 assert (strategy == MC_BROAD
262 || strategy == MC_DEEP
263 || strategy == MC_RANDOM);
264 options->strategy = strategy;
267 /* Returns OPTION's random seed used by MC_RANDOM and
270 mc_options_get_seed (const struct mc_options *options)
272 return options->seed;
275 /* Set OPTION's random seed used by MC_RANDOM and MC_DROP_RANDOM
278 mc_options_set_seed (struct mc_options *options, unsigned int seed)
280 options->seed = seed;
283 /* Returns the maximum depth to which OPTIONS's search will
284 descend. The initial states are at depth 1, states produced
285 as their mutations are at depth 2, and so on. */
287 mc_options_get_max_depth (const struct mc_options *options)
289 return options->max_depth;
292 /* Sets the maximum depth to which OPTIONS's search will descend
293 to MAX_DEPTH. The initial states are at depth 1, states
294 produced as their mutations are at depth 2, and so on. */
296 mc_options_set_max_depth (struct mc_options *options, int max_depth)
298 options->max_depth = max_depth;
301 /* Returns the base-2 log of the number of bits in OPTIONS's hash
302 table. The hash table is used for dropping states that are
303 probably duplicates: any state with a given hash value, as
304 will only be processed once. A return value of 0 indicates
305 that the model checker will not discard duplicate states based
308 The hash table is a power of 2 bits long, by default 2**20
309 bits (128 kB). Depending on how many states you expect the
310 model checker to check, how much memory you're willing to let
311 the hash table take up, and how worried you are about missing
312 states due to hash collisions, you could make it larger or
315 The "birthday paradox" points to a reasonable way to size your
316 hash table. If you expect the model checker to check about
317 2**N states, then, assuming a perfect hash, you need a hash
318 table of 2**(N+1) bits to have a 50% chance of seeing a hash
319 collision, 2**(N+2) bits to have a 25% chance, and so on. */
321 mc_options_get_hash_bits (const struct mc_options *options)
323 return options->hash_bits;
326 /* Sets the base-2 log of the number of bits in OPTIONS's hash
327 table to HASH_BITS. A HASH_BITS value of 0 requests that the
328 model checker not discard duplicate states based on their
329 hashes. (This causes the model checker to never terminate in
332 mc_options_set_hash_bits (struct mc_options *options, int hash_bits)
334 assert (hash_bits >= 0);
335 options->hash_bits = MIN (hash_bits, CHAR_BIT * sizeof (unsigned int) - 1);
338 /* Returns the path set in OPTIONS by mc_options_set_follow_path.
339 May be used only if the search strategy is MC_PATH. */
340 const struct mc_path *
341 mc_options_get_follow_path (const struct mc_options *options)
343 assert (options->strategy == MC_PATH);
344 return &options->follow_path;
347 /* Sets, in OPTIONS, the search algorithm to MC_PATH and the path
348 to be the explicit path specified in FOLLOW_PATH. */
350 mc_options_set_follow_path (struct mc_options *options,
351 const struct mc_path *follow_path)
353 assert (mc_path_get_length (follow_path) > 0);
354 options->strategy = MC_PATH;
355 mc_path_copy (&options->follow_path, follow_path);
358 /* Returns the maximum number of queued states in OPTIONS. The
359 default value is 10,000. The primary reason to limit the
360 number of queued states is to conserve memory, so if you can
361 afford the memory and your model needs more room in the queue,
362 you can raise the limit. Conversely, if your models are large
363 or memory is constrained, you can reduce the limit.
365 Following the execution of the model checker, you can find out
366 the maximum queue length during the run by calling
367 mc_results_get_max_queue_length. */
369 mc_options_get_queue_limit (const struct mc_options *options)
371 return options->queue_limit;
374 /* Sets the maximum number of queued states in OPTIONS to
377 mc_options_set_queue_limit (struct mc_options *options, int queue_limit)
379 assert (queue_limit > 0);
380 options->queue_limit = queue_limit;
383 /* Returns the queue limit strategy used by OPTIONS, that is,
384 when a new state must be inserted into a full state queue is
385 full, how the state to be dropped is chosen. The choices are:
387 - MC_DROP_NEWEST: Drop the newest state; that is, do not
388 insert the new state into the queue at all.
390 - MC_DROP_OLDEST: Drop the state that has been enqueued for
393 - MC_DROP_RANDOM (the default): Drop a randomly selected state
394 from the queue. The standard C library's rand function
395 selects the state to drop; you can control the seed passed
396 to srand using mc_options_set_seed. */
397 enum mc_queue_limit_strategy
398 mc_options_get_queue_limit_strategy (const struct mc_options *options)
400 return options->queue_limit_strategy;
403 /* Sets the queue limit strategy used by OPTIONS to STRATEGY.
405 This setting has no effect unless the model being checked
406 causes the state queue to overflow (see
407 mc_options_get_queue_limit). */
409 mc_options_set_queue_limit_strategy (struct mc_options *options,
410 enum mc_queue_limit_strategy strategy)
412 assert (strategy == MC_DROP_NEWEST
413 || strategy == MC_DROP_OLDEST
414 || strategy == MC_DROP_RANDOM);
415 options->queue_limit_strategy = strategy;
418 /* Returns OPTIONS's maximum number of unique states that the
419 model checker will examine before terminating. The default is
422 mc_options_get_max_unique_states (const struct mc_options *options)
424 return options->max_unique_states;
427 /* Sets OPTIONS's maximum number of unique states that the model
428 checker will examine before terminating to
431 mc_options_set_max_unique_states (struct mc_options *options,
432 int max_unique_states)
434 options->max_unique_states = max_unique_states;
437 /* Returns the maximum number of errors that OPTIONS will allow
438 the model checker to encounter before terminating. The
441 mc_options_get_max_errors (const struct mc_options *options)
443 return options->max_errors;
446 /* Sets the maximum number of errors that OPTIONS will allow the
447 model checker to encounter before terminating to
450 mc_options_set_max_errors (struct mc_options *options, int max_errors)
452 options->max_errors = max_errors;
455 /* Returns the maximum amount of time, in seconds, that OPTIONS will allow the
456 model checker to consume before terminating. The
457 default of 0.0 means that time consumption is unlimited. */
459 mc_options_get_time_limit (const struct mc_options *options)
461 return options->time_limit;
464 /* Sets the maximum amount of time, in seconds, that OPTIONS will
465 allow the model checker to consume before terminating to
466 TIME_LIMIT. A value of 0.0 means that time consumption is
467 unlimited; otherwise, the return value will be positive. */
469 mc_options_set_time_limit (struct mc_options *options, double time_limit)
471 assert (time_limit >= 0.0);
472 options->time_limit = time_limit;
475 /* Returns the level of verbosity for output messages specified
476 by OPTIONS. The default verbosity level is 1.
478 A verbosity level of 0 inhibits all messages except for
479 errors; a verbosity level of 1 also allows warnings; a
480 verbosity level of 2 also causes a description of each state
481 added to be output; a verbosity level of 3 also causes a
482 description of each duplicate state to be output. Verbosity
483 levels less than 0 or greater than 3 are allowed but currently
484 have no additional effect. */
486 mc_options_get_verbosity (const struct mc_options *options)
488 return options->verbosity;
491 /* Sets the level of verbosity for output messages specified
492 by OPTIONS to VERBOSITY. */
494 mc_options_set_verbosity (struct mc_options *options, int verbosity)
496 options->verbosity = verbosity;
499 /* Returns the level of verbosity for failures specified by
500 OPTIONS. The default failure verbosity level is 2.
502 The failure verbosity level has an effect only when an error
503 is reported, and only when the failure verbosity level is
504 higher than the regular verbosity level. When this is the
505 case, the model checker replays the error path at the higher
506 verbosity level specified. This has the effect of outputting
507 an explicit, human-readable description of the sequence of
508 operations that caused the error. */
510 mc_options_get_failure_verbosity (const struct mc_options *options)
512 return options->failure_verbosity;
515 /* Sets the level of verbosity for failures specified by OPTIONS
516 to FAILURE_VERBOSITY. */
518 mc_options_set_failure_verbosity (struct mc_options *options,
519 int failure_verbosity)
521 options->failure_verbosity = failure_verbosity;
524 /* Returns the output file used for messages printed by the model
525 checker specified by OPTIONS. The default is stdout. */
527 mc_options_get_output_file (const struct mc_options *options)
529 return options->output_file;
532 /* Sets the output file used for messages printed by the model
533 checker specified by OPTIONS to OUTPUT_FILE.
535 The model checker does not automatically close the specified
536 output file. If this is desired, the model checker's client
539 mc_options_set_output_file (struct mc_options *options,
542 options->output_file = output_file;
545 /* Returns the number of microseconds between calls to the
546 progress function specified by OPTIONS. The default is
547 250,000 (1/4 second). A value of 0 disables progress
550 mc_options_get_progress_usec (const struct mc_options *options)
552 return options->progress_usec;
555 /* Sets the number of microseconds between calls to the progress
556 function specified by OPTIONS to PROGRESS_USEC. A value of 0
557 disables progress reporting. */
559 mc_options_set_progress_usec (struct mc_options *options, int progress_usec)
561 assert (progress_usec >= 0);
562 options->progress_usec = progress_usec;
565 /* Returns the function called to report progress specified by
566 OPTIONS. The function used by default prints '.' to
569 mc_options_get_progress_func (const struct mc_options *options)
571 return options->progress_func;
574 /* Sets the function called to report progress specified by
575 OPTIONS to PROGRESS_FUNC. A non-null function must be
576 specified; to disable progress reporting, set the progress
577 reporting interval to 0.
579 PROGRESS_FUNC will be called zero or more times while the
580 model checker's run is ongoing. For these calls to the
581 progress function, mc_results_get_stop_reason will return
582 MC_CONTINUING. It will also be called exactly once soon
583 before mc_run returns, in which case
584 mc_results_get_stop_reason will return a different value. */
586 mc_options_set_progress_func (struct mc_options *options,
587 mc_progress_func *progress_func)
589 assert (options->progress_func != NULL);
590 options->progress_func = progress_func;
593 /* Returns the auxiliary data set in OPTIONS by the client. The
594 default is a null pointer.
596 This auxiliary data value can be retrieved by the
597 client-specified functions in struct mc_class during a model
598 checking run using mc_get_aux. */
600 mc_options_get_aux (const struct mc_options *options)
605 /* Sets the auxiliary data in OPTIONS to AUX. */
607 mc_options_set_aux (struct mc_options *options, void *aux)
612 /* Results of a model checking run. */
615 /* Overall results. */
616 enum mc_stop_reason stop_reason; /* Why the run ended. */
617 int unique_state_count; /* Number of unique states checked. */
618 int error_count; /* Number of errors found. */
620 /* Depth statistics. */
621 int max_depth_reached; /* Max depth state examined. */
622 unsigned long int depth_sum; /* Sum of depths. */
623 int n_depths; /* Number of depths in depth_sum. */
625 /* If error_count > 0, path to the last error reported. */
626 struct mc_path error_path;
628 /* States dropped... */
629 int duplicate_dropped_states; /* ...as duplicates. */
630 int off_path_dropped_states; /* ...as off-path (MC_PATH only). */
631 int depth_dropped_states; /* ...due to excessive depth. */
632 int queue_dropped_states; /* ...due to queue overflow. */
634 /* Queue statistics. */
635 int queued_unprocessed_states; /* Enqueued but never dequeued. */
636 int max_queue_length; /* Maximum queue length observed. */
639 struct timeval start; /* Start of model checking run. */
640 struct timeval end; /* End of model checking run. */
643 /* Creates, initializes, and returns a new set of results. */
644 static struct mc_results *
645 mc_results_create (void)
647 struct mc_results *results = xcalloc (1, sizeof (struct mc_results));
648 results->stop_reason = MC_CONTINUING;
649 gettimeofday (&results->start, NULL);
653 /* Destroys RESULTS. */
655 mc_results_destroy (struct mc_results *results)
659 mc_path_destroy (&results->error_path);
664 /* Returns RESULTS's reason that the model checking run
665 terminated. The possible reasons are:
667 - MC_CONTINUING: The run is not actually yet complete. This
668 can only be returned before mc_run has returned, e.g. when
669 the progress function set by mc_options_set_progress_func
670 examines the run's results.
672 - MC_SUCCESS: The run completed because the queue emptied.
673 The entire state space might not have been explored due to a
674 requested limit on maximum depth, hash collisions, etc.
676 - MC_MAX_UNIQUE_STATES: The run completed because as many
677 unique states have been checked as were requested (using
678 mc_options_set_max_unique_states).
680 - MC_MAX_ERROR_COUNT: The run completed because the maximum
681 requested number of errors (by default, 1 error) was
684 - MC_END_OF_PATH: The run completed because the path specified
685 with mc_options_set_follow_path was fully traversed.
687 - MC_TIMEOUT: The run completed because the time limit set
688 with mc_options_set_time_limit was exceeded.
690 - MC_INTERRUPTED: The run completed because SIGINT was caught
691 (typically, due to the user typing Ctrl+C). */
693 mc_results_get_stop_reason (const struct mc_results *results)
695 return results->stop_reason;
698 /* Returns the number of unique states checked specified by
701 mc_results_get_unique_state_count (const struct mc_results *results)
703 return results->unique_state_count;
706 /* Returns the number of errors found specified by RESULTS. */
708 mc_results_get_error_count (const struct mc_results *results)
710 return results->error_count;
713 /* Returns the maximum depth reached during the model checker run
714 represented by RESULTS. The initial states are at depth 1,
715 their child states at depth 2, and so on. */
717 mc_results_get_max_depth_reached (const struct mc_results *results)
719 return results->max_depth_reached;
722 /* Returns the mean depth reached during the model checker run
723 represented by RESULTS. */
725 mc_results_get_mean_depth_reached (const struct mc_results *results)
727 return (results->n_depths == 0
729 : (double) results->depth_sum / results->n_depths);
732 /* Returns the path traversed to obtain the last error
733 encountered during the model checker run represented by
734 RESULTS. Returns a null pointer if the run did not report any
736 const struct mc_path *
737 mc_results_get_error_path (const struct mc_results *results)
739 return results->error_count > 0 ? &results->error_path : NULL;
742 /* Returns the number of states dropped as duplicates (based on
743 hash value) during the model checker run represented by
746 mc_results_get_duplicate_dropped_states (const struct mc_results *results)
748 return results->duplicate_dropped_states;
751 /* Returns the number of states dropped because they were off the
752 path specified by mc_options_set_follow_path during the model
753 checker run represented by RESULTS. A nonzero value here
754 indicates a missing call to mc_include_state in the
755 client-supplied mutation function. */
757 mc_results_get_off_path_dropped_states (const struct mc_results *results)
759 return results->off_path_dropped_states;
762 /* Returns the number of states dropped because their depth
763 exceeded the maximum specified with mc_options_set_max_depth
764 during the model checker run represented by RESULTS. */
766 mc_results_get_depth_dropped_states (const struct mc_results *results)
768 return results->depth_dropped_states;
771 /* Returns the number of states dropped from the queue due to
772 queue overflow during the model checker run represented by
775 mc_results_get_queue_dropped_states (const struct mc_results *results)
777 return results->queue_dropped_states;
780 /* Returns the number of states that were checked and enqueued
781 but never dequeued and processed during the model checker run
782 represented by RESULTS. This is zero if the stop reason is
783 MC_CONTINUING or MC_SUCCESS; otherwise, it is the number of
784 states in the queue at the time that the checking run
787 mc_results_get_queued_unprocessed_states (const struct mc_results *results)
789 return results->queued_unprocessed_states;
792 /* Returns the maximum length of the queue during the model
793 checker run represented by RESULTS. If this is equal to the
794 maximum queue length, then the queue (probably) overflowed
795 during the run; otherwise, it did not overflow. */
797 mc_results_get_max_queue_length (const struct mc_results *results)
799 return results->max_queue_length;
802 /* Returns the time at which the model checker run represented by
805 mc_results_get_start (const struct mc_results *results)
807 return results->start;
810 /* Returns the time at which the model checker run represented by
811 RESULTS ended. (This function may not be called while the run
812 is still ongoing.) */
814 mc_results_get_end (const struct mc_results *results)
816 assert (results->stop_reason != MC_CONTINUING);
820 /* Returns the number of seconds obtained by subtracting time Y
823 timeval_subtract (struct timeval x, struct timeval y)
825 /* From libc.info. */
828 /* Perform the carry for the later subtraction by updating Y. */
829 if (x.tv_usec < y.tv_usec) {
830 int nsec = (y.tv_usec - x.tv_usec) / 1000000 + 1;
831 y.tv_usec -= 1000000 * nsec;
834 if (x.tv_usec - y.tv_usec > 1000000) {
835 int nsec = (x.tv_usec - y.tv_usec) / 1000000;
836 y.tv_usec += 1000000 * nsec;
840 /* Compute the time remaining to wait.
841 `tv_usec' is certainly positive. */
842 difference = (x.tv_sec - y.tv_sec) + (x.tv_usec - y.tv_usec) / 1000000.0;
843 if (x.tv_sec < y.tv_sec)
844 difference = -difference;
849 /* Returns the duration, in seconds, of the model checker run
850 represented by RESULTS. (This function may not be called
851 while the run is still ongoing.) */
853 mc_results_get_duration (const struct mc_results *results)
855 assert (results->stop_reason != MC_CONTINUING);
856 return timeval_subtract (results->end, results->start);
859 /* Prints a description of RESULTS to stream F. */
861 mc_results_print (const struct mc_results *results, FILE *f)
863 enum mc_stop_reason reason = mc_results_get_stop_reason (results);
865 if (reason != MC_CONTINUING)
866 fprintf (f, "Stopped by: %s\n",
867 reason == MC_SUCCESS ? "state space exhaustion"
868 : reason == MC_MAX_UNIQUE_STATES ? "reaching max unique states"
869 : reason == MC_MAX_ERROR_COUNT ? "reaching max error count"
870 : reason == MC_END_OF_PATH ? "reached end of specified path"
871 : reason == MC_TIMEOUT ? "reaching time limit"
872 : reason == MC_INTERRUPTED ? "user interruption"
874 fprintf (f, "Errors found: %d\n\n", mc_results_get_error_count (results));
876 fprintf (f, "Unique states checked: %d\n",
877 mc_results_get_unique_state_count (results));
878 fprintf (f, "Maximum depth reached: %d\n",
879 mc_results_get_max_depth_reached (results));
880 fprintf (f, "Mean depth reached: %.2f\n\n",
881 mc_results_get_mean_depth_reached (results));
883 fprintf (f, "Dropped duplicate states: %d\n",
884 mc_results_get_duplicate_dropped_states (results));
885 fprintf (f, "Dropped off-path states: %d\n",
886 mc_results_get_off_path_dropped_states (results));
887 fprintf (f, "Dropped too-deep states: %d\n",
888 mc_results_get_depth_dropped_states (results));
889 fprintf (f, "Dropped queue-overflow states: %d\n",
890 mc_results_get_queue_dropped_states (results));
891 fprintf (f, "Checked states still queued when stopped: %d\n",
892 mc_results_get_queued_unprocessed_states (results));
893 fprintf (f, "Maximum queue length reached: %d\n",
894 mc_results_get_max_queue_length (results));
896 if (reason != MC_CONTINUING)
897 fprintf (f, "\nRuntime: %.2f seconds\n",
898 mc_results_get_duration (results));
901 /* An active model checking run. */
904 /* Related data structures. */
905 const struct mc_class *class;
906 struct mc_options *options;
907 struct mc_results *results;
909 /* Array of 2**(options->hash_bits) bits representing states
914 struct mc_state **queue; /* Array of pointers to states. */
915 struct deque queue_deque; /* Deque. */
917 /* State currently being built by "init" or "mutate". */
918 struct mc_path path; /* Path to current state. */
919 struct string path_string; /* Buffer for path_string function. */
920 bool state_named; /* mc_name_operation called? */
921 bool state_error; /* mc_error called? */
923 /* Statistics for calling the progress function. */
924 unsigned int progress; /* Current progress value. */
925 unsigned int next_progress; /* Next value to call progress func. */
926 unsigned int prev_progress; /* Last value progress func called. */
927 struct timeval prev_progress_time; /* Last time progress func called. */
929 /* Information for handling and restoring SIGINT. */
930 bool interrupted; /* SIGINT received? */
931 bool *saved_interrupted_ptr; /* Saved value of interrupted_ptr. */
932 void (*saved_sigint) (int); /* Saved SIGINT handler. */
935 /* A state in the queue. */
938 struct mc_path path; /* Path to this state. */
939 void *data; /* Client-supplied data. */
942 /* Points to the current struct mc's "interrupted" member. */
943 static bool *interrupted_ptr = NULL;
945 static const char *path_string (struct mc *);
946 static void free_state (const struct mc *, struct mc_state *);
947 static void stop (struct mc *, enum mc_stop_reason);
948 static struct mc_state *make_state (const struct mc *, void *);
949 static size_t random_queue_index (struct mc *);
950 static void enqueue_state (struct mc *, struct mc_state *);
951 static void do_error_state (struct mc *);
952 static void next_operation (struct mc *);
953 static bool is_off_path (const struct mc *);
954 static void sigint_handler (int signum);
955 static void init_mc (struct mc *,
956 const struct mc_class *, struct mc_options *);
957 static void finish_mc (struct mc *);
959 /* Runs the model checker on the client-specified CLASS with the
960 client-specified OPTIONS. OPTIONS may be a null pointer if
961 the defaults are acceptable. Destroys OPTIONS; use
962 mc_options_clone if a copy is needed.
964 Returns the results of the model checking run, which must be
965 destroyed by the client with mc_results_destroy.
967 To pass auxiliary data to the functions in CLASS, use
968 mc_options_set_aux on OPTIONS, which may be retrieved from the
969 CLASS functions using mc_get_aux. */
971 mc_run (const struct mc_class *class, struct mc_options *options)
975 init_mc (&mc, class, options);
976 while (!deque_is_empty (&mc.queue_deque)
977 && mc.results->stop_reason == MC_CONTINUING)
979 struct mc_state *state = mc.queue[deque_pop_front (&mc.queue_deque)];
980 mc_path_copy (&mc.path, &state->path);
981 mc_path_push (&mc.path, 0);
982 class->mutate (&mc, state->data);
983 free_state (&mc, state);
985 stop (&mc, MC_INTERRUPTED);
992 /* Tests whether the current operation is one that should be
993 performed, checked, and enqueued. If so, returns true.
994 Otherwise, returns false and, unless checking is stopped,
995 advances to the next state. The caller should then advance
996 to the next operation.
998 This function should be called from the client-provided
999 "mutate" function, according to the pattern explained in the
1000 big comment at the top of model-checker.h. */
1002 mc_include_state (struct mc *mc)
1004 if (mc->results->stop_reason != MC_CONTINUING)
1006 else if (is_off_path (mc))
1008 next_operation (mc);
1015 /* Tests whether HASH represents a state that has (probably)
1016 already been enqueued. If not, returns false and marks HASH
1017 so that it will be treated as a duplicate in the future. If
1018 so, returns true and advances to the next state. The
1019 caller should then advance to the next operation.
1021 This function should be called from the client-provided
1022 "mutate" function, according to the pattern explained in the
1023 big comment at the top of model-checker.h. */
1025 mc_discard_dup_state (struct mc *mc, unsigned int hash)
1027 if (mc->options->hash_bits > 0)
1029 hash &= (1u << mc->options->hash_bits) - 1;
1030 if (TEST_BIT (mc->hash, hash))
1032 if (mc->options->verbosity > 2)
1033 fprintf (mc->options->output_file,
1034 " [%s] discard duplicate state\n", path_string (mc));
1035 mc->results->duplicate_dropped_states++;
1036 next_operation (mc);
1039 SET_BIT (mc->hash, hash);
1044 /* Names the current state NAME, which may contain
1045 printf-style format specifications. NAME should be a
1046 human-readable name for the current operation.
1048 This function should be called from the client-provided
1049 "mutate" function, according to the pattern explained in the
1050 big comment at the top of model-checker.h. */
1052 mc_name_operation (struct mc *mc, const char *name, ...)
1056 va_start (args, name);
1057 mc_vname_operation (mc, name, args);
1061 /* Names the current state NAME, which may contain
1062 printf-style format specifications, for which the
1063 corresponding arguments must be given in ARGS. NAME should be
1064 a human-readable name for the current operation.
1066 This function should be called from the client-provided
1067 "mutate" function, according to the pattern explained in the
1068 big comment at the top of model-checker.h. */
1070 mc_vname_operation (struct mc *mc, const char *name, va_list args)
1072 if (mc->state_named && mc->options->verbosity > 0)
1073 fprintf (mc->options->output_file, " [%s] warning: duplicate call "
1074 "to mc_name_operation (missing call to mc_add_state?)\n",
1076 mc->state_named = true;
1078 if (mc->options->verbosity > 1)
1080 fprintf (mc->options->output_file, " [%s] ", path_string (mc));
1081 vfprintf (mc->options->output_file, name, args);
1082 putc ('\n', mc->options->output_file);
1086 /* Reports the given error MESSAGE for the current operation.
1087 The resulting state should still be passed to mc_add_state
1088 when all relevant error messages have been issued. The state
1089 will not, however, be enqueued for later mutation of its own.
1091 By default, model checking stops after the first error
1094 This function should be called from the client-provided
1095 "mutate" function, according to the pattern explained in the
1096 big comment at the top of model-checker.h. */
1098 mc_error (struct mc *mc, const char *message, ...)
1102 if (mc->results->stop_reason != MC_CONTINUING)
1105 if (mc->options->verbosity > 1)
1106 fputs (" ", mc->options->output_file);
1107 fprintf (mc->options->output_file, "[%s] error: ",
1109 va_start (args, message);
1110 vfprintf (mc->options->output_file, message, args);
1112 putc ('\n', mc->options->output_file);
1114 mc->state_error = true;
1117 /* Enqueues DATA as the state corresponding to the current
1118 operation. The operation should have been named with a call
1119 to mc_name_operation, and it should have been checked by the
1120 caller (who should have reported any errors with mc_error).
1122 This function should be called from the client-provided
1123 "mutate" function, according to the pattern explained in the
1124 big comment at the top of model-checker.h. */
1126 mc_add_state (struct mc *mc, void *data)
1128 if (!mc->state_named && mc->options->verbosity > 0)
1129 fprintf (mc->options->output_file, " [%s] warning: unnamed state\n",
1132 if (mc->results->stop_reason != MC_CONTINUING)
1134 /* Nothing to do. */
1136 else if (mc->state_error)
1137 do_error_state (mc);
1138 else if (is_off_path (mc))
1139 mc->results->off_path_dropped_states++;
1140 else if (mc->path.length + 1 > mc->options->max_depth)
1141 mc->results->depth_dropped_states++;
1144 /* This is the common case. */
1145 mc->results->unique_state_count++;
1146 if (mc->results->unique_state_count >= mc->options->max_unique_states)
1147 stop (mc, MC_MAX_UNIQUE_STATES);
1148 enqueue_state (mc, make_state (mc, data));
1149 next_operation (mc);
1153 mc->class->destroy (mc, data);
1154 next_operation (mc);
1157 /* Returns the options that were passed to mc_run for model
1159 const struct mc_options *
1160 mc_get_options (const struct mc *mc)
1165 /* Returns the current state of the results for model checker
1166 MC. This function is appropriate for use from the progress
1167 function set by mc_options_set_progress_func.
1169 Not all of the results are meaningful before model checking
1171 const struct mc_results *
1172 mc_get_results (const struct mc *mc)
1177 /* Returns the auxiliary data set on the options passed to mc_run
1178 with mc_options_set_aux. */
1180 mc_get_aux (const struct mc *mc)
1182 return mc_options_get_aux (mc_get_options (mc));
1185 /* Expresses MC->path as a string and returns the string. */
1187 path_string (struct mc *mc)
1189 ds_clear (&mc->path_string);
1190 mc_path_to_string (&mc->path, &mc->path_string);
1191 return ds_cstr (&mc->path_string);
1194 /* Frees STATE, including client data. */
1196 free_state (const struct mc *mc, struct mc_state *state)
1198 mc->class->destroy (mc, state->data);
1199 mc_path_destroy (&state->path);
1203 /* Sets STOP_REASON as the reason that MC's processing stopped,
1204 unless MC is already stopped. */
1206 stop (struct mc *mc, enum mc_stop_reason stop_reason)
1208 if (mc->results->stop_reason == MC_CONTINUING)
1209 mc->results->stop_reason = stop_reason;
1212 /* Creates and returns a new state whose path is copied from
1213 MC->path and whose data is specified by DATA. */
1214 static struct mc_state *
1215 make_state (const struct mc *mc, void *data)
1217 struct mc_state *new = xmalloc (sizeof *new);
1218 mc_path_init (&new->path);
1219 mc_path_copy (&new->path, &mc->path);
1224 /* Returns the index in MC->queue of a random element in the
1227 random_queue_index (struct mc *mc)
1229 assert (!deque_is_empty (&mc->queue_deque));
1230 return deque_front (&mc->queue_deque,
1231 rand () % deque_count (&mc->queue_deque));
1234 /* Adds NEW to MC's state queue, dropping a state if necessary
1237 enqueue_state (struct mc *mc, struct mc_state *new)
1241 if (new->path.length > mc->results->max_depth_reached)
1242 mc->results->max_depth_reached = new->path.length;
1243 mc->results->depth_sum += new->path.length;
1244 mc->results->n_depths++;
1246 if (deque_count (&mc->queue_deque) < mc->options->queue_limit)
1248 /* Add new state to queue. */
1249 if (deque_is_full (&mc->queue_deque))
1250 mc->queue = deque_expand (&mc->queue_deque,
1251 mc->queue, sizeof *mc->queue);
1252 switch (mc->options->strategy)
1255 idx = deque_push_back (&mc->queue_deque);
1258 idx = deque_push_front (&mc->queue_deque);
1261 if (!deque_is_empty (&mc->queue_deque))
1263 idx = random_queue_index (mc);
1264 mc->queue[deque_push_front (&mc->queue_deque)]
1268 idx = deque_push_front (&mc->queue_deque);
1271 assert (deque_is_empty (&mc->queue_deque));
1272 assert (!is_off_path (mc));
1273 idx = deque_push_back (&mc->queue_deque);
1275 >= mc_path_get_length (&mc->options->follow_path))
1276 stop (mc, MC_END_OF_PATH);
1281 if (deque_count (&mc->queue_deque) > mc->results->max_queue_length)
1282 mc->results->max_queue_length = deque_count (&mc->queue_deque);
1286 /* Queue has reached limit, so replace an existing
1288 assert (mc->options->strategy != MC_PATH);
1289 assert (!deque_is_empty (&mc->queue_deque));
1290 mc->results->queue_dropped_states++;
1291 switch (mc->options->queue_limit_strategy)
1293 case MC_DROP_NEWEST:
1294 free_state (mc, new);
1296 case MC_DROP_OLDEST:
1297 switch (mc->options->strategy)
1300 idx = deque_front (&mc->queue_deque, 0);
1303 idx = deque_back (&mc->queue_deque, 0);
1311 case MC_DROP_RANDOM:
1312 idx = random_queue_index (mc);
1317 free_state (mc, mc->queue[idx]);
1319 mc->queue[idx] = new;
1322 /* Process an error state being added to MC. */
1324 do_error_state (struct mc *mc)
1326 mc->results->error_count++;
1327 if (mc->results->error_count >= mc->options->max_errors)
1328 stop (mc, MC_MAX_ERROR_COUNT);
1330 mc_path_copy (&mc->results->error_path, &mc->path);
1332 if (mc->options->failure_verbosity > mc->options->verbosity)
1334 struct mc_options *path_options;
1336 fprintf (mc->options->output_file, "[%s] retracing error path:\n",
1338 path_options = mc_options_clone (mc->options);
1339 mc_options_set_verbosity (path_options, mc->options->failure_verbosity);
1340 mc_options_set_failure_verbosity (path_options, 0);
1341 mc_options_set_follow_path (path_options, &mc->path);
1343 mc_results_destroy (mc_run (mc->class, path_options));
1345 putc ('\n', mc->options->output_file);
1349 /* Advances MC to start processing the operation following the
1352 next_operation (struct mc *mc)
1354 mc_path_push (&mc->path, mc_path_pop (&mc->path) + 1);
1355 mc->state_error = false;
1356 mc->state_named = false;
1358 if (++mc->progress >= mc->next_progress)
1361 double elapsed, delta;
1363 if (mc->results->stop_reason == MC_CONTINUING
1364 && !mc->options->progress_func (mc))
1365 stop (mc, MC_INTERRUPTED);
1367 gettimeofday (&now, NULL);
1369 if (mc->options->time_limit > 0.0
1370 && (timeval_subtract (now, mc->results->start)
1371 > mc->options->time_limit))
1372 stop (mc, MC_TIMEOUT);
1374 elapsed = timeval_subtract (now, mc->prev_progress_time);
1377 /* Re-estimate the amount of progress to take
1378 progress_usec microseconds. */
1379 unsigned int progress = mc->progress - mc->prev_progress;
1380 double progress_sec = mc->options->progress_usec / 1000000.0;
1381 delta = progress / elapsed * progress_sec;
1385 /* No measurable time at all elapsed during that amount
1386 of progress. Try doubling the amount of progress
1388 delta = (mc->progress - mc->prev_progress) * 2;
1391 if (delta > 0.0 && delta + mc->progress + 1.0 < UINT_MAX)
1392 mc->next_progress = mc->progress + delta + 1.0;
1394 mc->next_progress = mc->progress + (mc->progress - mc->prev_progress);
1396 mc->prev_progress = mc->progress;
1397 mc->prev_progress_time = now;
1401 /* Returns true if we're tracing an explicit path but the current
1402 operation produces a state off that path, false otherwise. */
1404 is_off_path (const struct mc *mc)
1406 return (mc->options->strategy == MC_PATH
1407 && (mc_path_back (&mc->path)
1408 != mc_path_get_operation (&mc->options->follow_path,
1409 mc->path.length - 1)));
1412 /* Handler for SIGINT. */
1414 sigint_handler (int signum UNUSED)
1416 /* Just mark the model checker as interrupted. */
1417 *interrupted_ptr = true;
1420 /* Initializes MC as a model checker with the given CLASS and
1421 OPTIONS. OPTIONS may be null to use the default options. */
1423 init_mc (struct mc *mc, const struct mc_class *class,
1424 struct mc_options *options)
1426 /* Validate and adjust OPTIONS. */
1427 if (options == NULL)
1428 options = mc_options_create ();
1429 assert (options->queue_limit_strategy != MC_DROP_OLDEST
1430 || options->strategy != MC_RANDOM);
1431 if (options->strategy == MC_PATH)
1433 options->max_depth = INT_MAX;
1434 options->hash_bits = 0;
1436 if (options->progress_usec == 0)
1438 options->progress_func = null_progress;
1439 if (options->time_limit > 0.0)
1440 options->progress_usec = 250000;
1443 /* Initialize MC. */
1445 mc->options = options;
1446 mc->results = mc_results_create ();
1448 mc->hash = (mc->options->hash_bits > 0
1449 ? xcalloc (1, DIV_RND_UP (1 << mc->options->hash_bits, CHAR_BIT))
1453 deque_init_null (&mc->queue_deque);
1455 mc_path_init (&mc->path);
1456 mc_path_push (&mc->path, 0);
1457 ds_init_empty (&mc->path_string);
1458 mc->state_named = false;
1459 mc->state_error = false;
1462 mc->next_progress = mc->options->progress_usec != 0 ? 100 : UINT_MAX;
1463 mc->prev_progress = 0;
1464 mc->prev_progress_time = mc->results->start;
1466 if (mc->options->strategy == MC_RANDOM
1467 || options->queue_limit_strategy == MC_DROP_RANDOM)
1468 srand (mc->options->seed);
1470 mc->interrupted = false;
1471 mc->saved_interrupted_ptr = interrupted_ptr;
1472 interrupted_ptr = &mc->interrupted;
1473 mc->saved_sigint = signal (SIGINT, sigint_handler);
1478 /* Complete the model checker run for MC. */
1480 finish_mc (struct mc *mc)
1482 /* Restore signal handlers. */
1483 signal (SIGINT, mc->saved_sigint);
1484 interrupted_ptr = mc->saved_interrupted_ptr;
1486 /* Mark the run complete. */
1487 stop (mc, MC_SUCCESS);
1488 gettimeofday (&mc->results->end, NULL);
1490 /* Empty the queue. */
1491 mc->results->queued_unprocessed_states = deque_count (&mc->queue_deque);
1492 while (!deque_is_empty (&mc->queue_deque))
1494 struct mc_state *state = mc->queue[deque_pop_front (&mc->queue_deque)];
1495 free_state (mc, state);
1498 /* Notify the progress function of completion. */
1499 mc->options->progress_func (mc);
1502 mc_path_destroy (&mc->path);
1503 ds_destroy (&mc->path_string);