Flush the journal after every write.
[pspp] / src / libpspp / model-checker.c
1 /* PSPP - a program for statistical analysis.
2    Copyright (C) 2007, 2009 Free Software Foundation, Inc.
3
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.
8
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.
13
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/>. */
16
17 #include <config.h>
18
19 #include <libpspp/model-checker.h>
20
21 #include <limits.h>
22 #include <signal.h>
23 #include <stdarg.h>
24 #include <stdio.h>
25 #include <stdlib.h>
26 #include <string.h>
27 #include <sys/time.h>
28
29 #include <libpspp/argv-parser.h>
30 #include <libpspp/bit-vector.h>
31 #include <libpspp/compiler.h>
32 #include <libpspp/deque.h>
33 #include <libpspp/misc.h>
34 #include <libpspp/str.h>
35
36 #include "error.h"
37 #include "minmax.h"
38 #include "xalloc.h"
39 \f
40 /* Initializes PATH as an empty path. */
41 void
42 mc_path_init (struct mc_path *path)
43 {
44   path->ops = NULL;
45   path->length = 0;
46   path->capacity = 0;
47 }
48
49 /* Copies the contents of OLD into NEW. */
50 void
51 mc_path_copy (struct mc_path *new, const struct mc_path *old)
52 {
53   if (old->length > new->capacity)
54     {
55       new->capacity = old->length;
56       free (new->ops);
57       new->ops = xnmalloc (new->capacity, sizeof *new->ops);
58     }
59   new->length = old->length;
60   memcpy (new->ops, old->ops, old->length * sizeof *new->ops);
61 }
62
63 /* Adds OP to the end of PATH. */
64 void
65 mc_path_push (struct mc_path *path, int op)
66 {
67   if (path->length >= path->capacity)
68     path->ops = xnrealloc (path->ops, ++path->capacity, sizeof *path->ops);
69   path->ops[path->length++] = op;
70 }
71
72 /* Removes and returns the operation at the end of PATH. */
73 int
74 mc_path_pop (struct mc_path *path)
75 {
76   int back = mc_path_back (path);
77   path->length--;
78   return back;
79 }
80
81 /* Returns the operation at the end of PATH. */
82 int
83 mc_path_back (const struct mc_path *path)
84 {
85   assert (path->length > 0);
86   return path->ops[path->length - 1];
87 }
88
89 /* Destroys PATH. */
90 void
91 mc_path_destroy (struct mc_path *path)
92 {
93   free (path->ops);
94   path->ops = NULL;
95 }
96
97 /* Returns the operation in position INDEX in PATH.
98    INDEX must be less than the length of PATH. */
99 int
100 mc_path_get_operation (const struct mc_path *path, size_t index)
101 {
102   assert (index < path->length);
103   return path->ops[index];
104 }
105
106 /* Returns the number of operations in PATH. */
107 size_t
108 mc_path_get_length (const struct mc_path *path)
109 {
110   return path->length;
111 }
112
113 /* Appends the operations in PATH to STRING, separating each one
114    with a single space. */
115 void
116 mc_path_to_string (const struct mc_path *path, struct string *string)
117 {
118   size_t i;
119
120   for (i = 0; i < mc_path_get_length (path); i++)
121     {
122       if (i > 0)
123         ds_put_char (string, ' ');
124       ds_put_format (string, "%d", mc_path_get_operation (path, i));
125     }
126 }
127 \f
128 /* Search options. */
129 struct mc_options
130   {
131     /* Search strategy. */
132     enum mc_strategy strategy;          /* Type of strategy. */
133     int max_depth;                      /* Limit on depth (or INT_MAX). */
134     int hash_bits;                      /* Number of bits to hash (or 0). */
135     unsigned int seed;                  /* Random seed for MC_RANDOM
136                                            or MC_DROP_RANDOM. */
137     struct mc_path follow_path;         /* Path for MC_PATH. */
138
139     /* Queue configuration. */
140     int queue_limit;                    /* Maximum length of queue. */
141     enum mc_queue_limit_strategy queue_limit_strategy;
142                                         /* How to choose state to drop
143                                            from queue. */
144
145     /* Stop conditions. */
146     int max_unique_states;              /* Maximum unique states to process. */
147     int max_errors;                     /* Maximum errors to detect. */
148     double time_limit;                  /* Maximum time in seconds. */
149
150     /* Output configuration. */
151     int verbosity;                      /* 0=low, 1=normal, 2+=high. */
152     int failure_verbosity;              /* If greater than verbosity,
153                                            verbosity of error replays. */
154     FILE *output_file;                  /* File to receive output. */
155
156     /* How to report intermediate progress. */
157     int progress_usec;                  /* Microseconds between reports. */
158     mc_progress_func *progress_func;    /* Function to call on each report. */
159
160     /* Client data. */
161     void *aux;
162   };
163
164 /* Default progress function. */
165 bool
166 mc_progress_dots (struct mc *mc)
167 {
168   if (mc_results_get_stop_reason (mc_get_results (mc)) == MC_CONTINUING)
169     putc ('.', stderr);
170   else
171     putc ('\n', stderr);
172   return true;
173 }
174
175 /* Progress function that prints a one-line summary of the
176    current state on stderr. */
177 bool
178 mc_progress_fancy (struct mc *mc)
179 {
180   const struct mc_results *results = mc_get_results (mc);
181   if (mc_results_get_stop_reason (results) == MC_CONTINUING)
182     fprintf (stderr, "Processed %d unique states, max depth %d, "
183              "dropped %d duplicates...\r",
184              mc_results_get_unique_state_count (results),
185              mc_results_get_max_depth_reached (results),
186              mc_results_get_duplicate_dropped_states (results));
187   else
188     putc ('\n', stderr);
189   return true;
190 }
191
192 /* Progress function that displays a detailed summary of the
193    current state on stderr. */
194 bool
195 mc_progress_verbose (struct mc *mc)
196 {
197   const struct mc_results *results = mc_get_results (mc);
198
199   /* VT100 clear screen and home cursor. */
200   fprintf (stderr, "\033[H\033[2J");
201
202   if (mc_results_get_stop_reason (results) == MC_CONTINUING)
203     mc_results_print (results, stderr);
204
205   return true;
206 }
207
208 /* Do-nothing progress function. */
209 static bool
210 null_progress (struct mc *mc UNUSED)
211 {
212   return true;
213 }
214
215 /* Creates and returns a set of options initialized to the
216    defaults. */
217 struct mc_options *
218 mc_options_create (void)
219 {
220   struct mc_options *options = xmalloc (sizeof *options);
221
222   options->strategy = MC_BROAD;
223   options->max_depth = INT_MAX;
224   options->hash_bits = 20;
225   options->seed = 0;
226   mc_path_init (&options->follow_path);
227
228   options->queue_limit = 10000;
229   options->queue_limit_strategy = MC_DROP_RANDOM;
230
231   options->max_unique_states = INT_MAX;
232   options->max_errors = 1;
233   options->time_limit = 0.0;
234
235   options->verbosity = 1;
236   options->failure_verbosity = 2;
237   options->output_file = stdout;
238   options->progress_usec = 250000;
239   options->progress_func = mc_progress_dots;
240
241   options->aux = NULL;
242
243   return options;
244 }
245
246 /* Returns a copy of the given OPTIONS. */
247 struct mc_options *
248 mc_options_clone (const struct mc_options *options)
249 {
250   return xmemdup (options, sizeof *options);
251 }
252
253 /* Destroys OPTIONS. */
254 void
255 mc_options_destroy (struct mc_options *options)
256 {
257   mc_path_destroy (&options->follow_path);
258   free (options);
259 }
260
261 /* Returns the search strategy used for OPTIONS.  The choices
262    are:
263
264    - MC_BROAD (the default): Breadth-first search.  First tries
265      all the operations with depth 1, then those with depth 2,
266      then those with depth 3, and so on.
267
268      This search algorithm finds the least number of operations
269      needed to trigger a given bug.
270
271    - MC_DEEP: Depth-first search.  Searches downward in the tree
272      of states as fast as possible.  Good for finding bugs that
273      require long sequences of operations to trigger.
274
275    - MC_RANDOM: Random-first search.  Searches through the tree
276      of states in random order.  The standard C library's rand
277      function selects the search path; you can control the seed
278      passed to srand using mc_options_set_seed.
279
280    - MC_PATH: Explicit path.  Applies an explicitly specified
281      sequence of operations. */
282 enum mc_strategy
283 mc_options_get_strategy (const struct mc_options *options)
284 {
285   return options->strategy;
286 }
287
288 /* Sets the search strategy used for OPTIONS to STRATEGY.
289
290    This function cannot be used to set MC_PATH as the search
291    strategy.  Use mc_options_set_follow_path instead. */
292 void
293 mc_options_set_strategy (struct mc_options *options, enum mc_strategy strategy)
294 {
295   assert (strategy == MC_BROAD
296           || strategy == MC_DEEP
297           || strategy == MC_RANDOM);
298   options->strategy = strategy;
299 }
300
301 /* Returns OPTION's random seed used by MC_RANDOM and
302    MC_DROP_RANDOM. */
303 unsigned int
304 mc_options_get_seed (const struct mc_options *options)
305 {
306   return options->seed;
307 }
308
309 /* Set OPTION's random seed used by MC_RANDOM and MC_DROP_RANDOM
310    to SEED. */
311 void
312 mc_options_set_seed (struct mc_options *options, unsigned int seed)
313 {
314   options->seed = seed;
315 }
316
317 /* Returns the maximum depth to which OPTIONS's search will
318    descend.  The initial states are at depth 1, states produced
319    as their mutations are at depth 2, and so on. */
320 int
321 mc_options_get_max_depth (const struct mc_options *options)
322 {
323   return options->max_depth;
324 }
325
326 /* Sets the maximum depth to which OPTIONS's search will descend
327    to MAX_DEPTH.  The initial states are at depth 1, states
328    produced as their mutations are at depth 2, and so on. */
329 void
330 mc_options_set_max_depth (struct mc_options *options, int max_depth)
331 {
332   options->max_depth = max_depth;
333 }
334
335 /* Returns the base-2 log of the number of bits in OPTIONS's hash
336    table.  The hash table is used for dropping states that are
337    probably duplicates: any state with a given hash value, as
338    will only be processed once.  A return value of 0 indicates
339    that the model checker will not discard duplicate states based
340    on their hashes.
341
342    The hash table is a power of 2 bits long, by default 2**20
343    bits (128 kB).  Depending on how many states you expect the
344    model checker to check, how much memory you're willing to let
345    the hash table take up, and how worried you are about missing
346    states due to hash collisions, you could make it larger or
347    smaller.
348
349    The "birthday paradox" points to a reasonable way to size your
350    hash table.  If you expect the model checker to check about
351    2**N states, then, assuming a perfect hash, you need a hash
352    table of 2**(N+1) bits to have a 50% chance of seeing a hash
353    collision, 2**(N+2) bits to have a 25% chance, and so on. */
354 int
355 mc_options_get_hash_bits (const struct mc_options *options)
356 {
357   return options->hash_bits;
358 }
359
360 /* Sets the base-2 log of the number of bits in OPTIONS's hash
361    table to HASH_BITS.  A HASH_BITS value of 0 requests that the
362    model checker not discard duplicate states based on their
363    hashes.  (This causes the model checker to never terminate in
364    many cases.) */
365 void
366 mc_options_set_hash_bits (struct mc_options *options, int hash_bits)
367 {
368   assert (hash_bits >= 0);
369   options->hash_bits = MIN (hash_bits, CHAR_BIT * sizeof (unsigned int) - 1);
370 }
371
372 /* Returns the path set in OPTIONS by mc_options_set_follow_path.
373    May be used only if the search strategy is MC_PATH. */
374 const struct mc_path *
375 mc_options_get_follow_path (const struct mc_options *options)
376 {
377   assert (options->strategy == MC_PATH);
378   return &options->follow_path;
379 }
380
381 /* Sets, in OPTIONS, the search algorithm to MC_PATH and the path
382    to be the explicit path specified in FOLLOW_PATH. */
383 void
384 mc_options_set_follow_path (struct mc_options *options,
385                             const struct mc_path *follow_path)
386 {
387   assert (mc_path_get_length (follow_path) > 0);
388   options->strategy = MC_PATH;
389   mc_path_copy (&options->follow_path, follow_path);
390 }
391
392 /* Returns the maximum number of queued states in OPTIONS.  The
393    default value is 10,000.  The primary reason to limit the
394    number of queued states is to conserve memory, so if you can
395    afford the memory and your model needs more room in the queue,
396    you can raise the limit.  Conversely, if your models are large
397    or memory is constrained, you can reduce the limit.
398
399    Following the execution of the model checker, you can find out
400    the maximum queue length during the run by calling
401    mc_results_get_max_queue_length. */
402 int
403 mc_options_get_queue_limit (const struct mc_options *options)
404 {
405   return options->queue_limit;
406 }
407
408 /* Sets the maximum number of queued states in OPTIONS to
409    QUEUE_LIMIT.  */
410 void
411 mc_options_set_queue_limit (struct mc_options *options, int queue_limit)
412 {
413   assert (queue_limit > 0);
414   options->queue_limit = queue_limit;
415 }
416
417 /* Returns the queue limit strategy used by OPTIONS, that is,
418    when a new state must be inserted into a full state queue is
419    full, how the state to be dropped is chosen.  The choices are:
420
421    - MC_DROP_NEWEST: Drop the newest state; that is, do not
422      insert the new state into the queue at all.
423
424    - MC_DROP_OLDEST: Drop the state that has been enqueued for
425      the longest.
426
427    - MC_DROP_RANDOM (the default): Drop a randomly selected state
428      from the queue.  The standard C library's rand function
429      selects the state to drop; you can control the seed passed
430      to srand using mc_options_set_seed. */
431 enum mc_queue_limit_strategy
432 mc_options_get_queue_limit_strategy (const struct mc_options *options)
433 {
434   return options->queue_limit_strategy;
435 }
436
437 /* Sets the queue limit strategy used by OPTIONS to STRATEGY.
438
439    This setting has no effect unless the model being checked
440    causes the state queue to overflow (see
441    mc_options_get_queue_limit). */
442 void
443 mc_options_set_queue_limit_strategy (struct mc_options *options,
444                                      enum mc_queue_limit_strategy strategy)
445 {
446   assert (strategy == MC_DROP_NEWEST
447           || strategy == MC_DROP_OLDEST
448           || strategy == MC_DROP_RANDOM);
449   options->queue_limit_strategy = strategy;
450 }
451
452 /* Returns OPTIONS's maximum number of unique states that the
453    model checker will examine before terminating.  The default is
454    INT_MAX. */
455 int
456 mc_options_get_max_unique_states (const struct mc_options *options)
457 {
458   return options->max_unique_states;
459 }
460
461 /* Sets OPTIONS's maximum number of unique states that the model
462    checker will examine before terminating to
463    MAX_UNIQUE_STATE. */
464 void
465 mc_options_set_max_unique_states (struct mc_options *options,
466                                   int max_unique_states)
467 {
468   options->max_unique_states = max_unique_states;
469 }
470
471 /* Returns the maximum number of errors that OPTIONS will allow
472    the model checker to encounter before terminating.  The
473    default is 1. */
474 int
475 mc_options_get_max_errors (const struct mc_options *options)
476 {
477   return options->max_errors;
478 }
479
480 /* Sets the maximum number of errors that OPTIONS will allow the
481    model checker to encounter before terminating to
482    MAX_ERRORS. */
483 void
484 mc_options_set_max_errors (struct mc_options *options, int max_errors)
485 {
486   options->max_errors = max_errors;
487 }
488
489 /* Returns the maximum amount of time, in seconds, that OPTIONS will allow the
490    model checker to consume before terminating.  The
491    default of 0.0 means that time consumption is unlimited. */
492 double
493 mc_options_get_time_limit (const struct mc_options *options)
494 {
495   return options->time_limit;
496 }
497
498 /* Sets the maximum amount of time, in seconds, that OPTIONS will
499    allow the model checker to consume before terminating to
500    TIME_LIMIT.  A value of 0.0 means that time consumption is
501    unlimited; otherwise, the return value will be positive. */
502 void
503 mc_options_set_time_limit (struct mc_options *options, double time_limit)
504 {
505   assert (time_limit >= 0.0);
506   options->time_limit = time_limit;
507 }
508
509 /* Returns the level of verbosity for output messages specified
510    by OPTIONS.  The default verbosity level is 1.
511
512    A verbosity level of 0 inhibits all messages except for
513    errors; a verbosity level of 1 also allows warnings; a
514    verbosity level of 2 also causes a description of each state
515    added to be output; a verbosity level of 3 also causes a
516    description of each duplicate state to be output.  Verbosity
517    levels less than 0 or greater than 3 are allowed but currently
518    have no additional effect. */
519 int
520 mc_options_get_verbosity (const struct mc_options *options)
521 {
522   return options->verbosity;
523 }
524
525 /* Sets the level of verbosity for output messages specified
526    by OPTIONS to VERBOSITY. */
527 void
528 mc_options_set_verbosity (struct mc_options *options, int verbosity)
529 {
530   options->verbosity = verbosity;
531 }
532
533 /* Returns the level of verbosity for failures specified by
534    OPTIONS.  The default failure verbosity level is 2.
535
536    The failure verbosity level has an effect only when an error
537    is reported, and only when the failure verbosity level is
538    higher than the regular verbosity level.  When this is the
539    case, the model checker replays the error path at the higher
540    verbosity level specified.  This has the effect of outputting
541    an explicit, human-readable description of the sequence of
542    operations that caused the error. */
543 int
544 mc_options_get_failure_verbosity (const struct mc_options *options)
545 {
546   return options->failure_verbosity;
547 }
548
549 /* Sets the level of verbosity for failures specified by OPTIONS
550    to FAILURE_VERBOSITY. */
551 void
552 mc_options_set_failure_verbosity (struct mc_options *options,
553                                   int failure_verbosity)
554 {
555   options->failure_verbosity = failure_verbosity;
556 }
557
558 /* Returns the output file used for messages printed by the model
559    checker specified by OPTIONS.  The default is stdout. */
560 FILE *
561 mc_options_get_output_file (const struct mc_options *options)
562 {
563   return options->output_file;
564 }
565
566 /* Sets the output file used for messages printed by the model
567    checker specified by OPTIONS to OUTPUT_FILE.
568
569    The model checker does not automatically close the specified
570    output file.  If this is desired, the model checker's client
571    must do so. */
572 void
573 mc_options_set_output_file (struct mc_options *options,
574                             FILE *output_file)
575 {
576   options->output_file = output_file;
577 }
578
579 /* Returns the number of microseconds between calls to the
580    progress function specified by OPTIONS.   The default is
581    250,000 (1/4 second).  A value of 0 disables progress
582    reporting. */
583 int
584 mc_options_get_progress_usec (const struct mc_options *options)
585 {
586   return options->progress_usec;
587 }
588
589 /* Sets the number of microseconds between calls to the progress
590    function specified by OPTIONS to PROGRESS_USEC.  A value of 0
591    disables progress reporting. */
592 void
593 mc_options_set_progress_usec (struct mc_options *options, int progress_usec)
594 {
595   assert (progress_usec >= 0);
596   options->progress_usec = progress_usec;
597 }
598
599 /* Returns the function called to report progress specified by
600    OPTIONS.  The function used by default prints '.' to
601    stderr. */
602 mc_progress_func *
603 mc_options_get_progress_func (const struct mc_options *options)
604 {
605   return options->progress_func;
606 }
607
608 /* Sets the function called to report progress specified by
609    OPTIONS to PROGRESS_FUNC.  A non-null function must be
610    specified; to disable progress reporting, set the progress
611    reporting interval to 0.
612
613    PROGRESS_FUNC will be called zero or more times while the
614    model checker's run is ongoing.  For these calls to the
615    progress function, mc_results_get_stop_reason will return
616    MC_CONTINUING.  It will also be called exactly once soon
617    before mc_run returns, in which case
618    mc_results_get_stop_reason will return a different value. */
619 void
620 mc_options_set_progress_func (struct mc_options *options,
621                               mc_progress_func *progress_func)
622 {
623   assert (options->progress_func != NULL);
624   options->progress_func = progress_func;
625 }
626
627 /* Returns the auxiliary data set in OPTIONS by the client.  The
628    default is a null pointer.
629
630    This auxiliary data value can be retrieved by the
631    client-specified functions in struct mc_class during a model
632    checking run using mc_get_aux. */
633 void *
634 mc_options_get_aux (const struct mc_options *options)
635 {
636   return options->aux;
637 }
638
639 /* Sets the auxiliary data in OPTIONS to AUX. */
640 void
641 mc_options_set_aux (struct mc_options *options, void *aux)
642 {
643   options->aux = aux;
644 }
645 \f
646 /* Options command-line parser. */
647
648 enum
649   {
650     /* Search strategies. */
651     OPT_STRATEGY,
652     OPT_PATH,
653     OPT_MAX_DEPTH,
654     OPT_HASH_BITS,
655     OPT_SEED,
656
657     /* Queuing. */
658     OPT_QUEUE_LIMIT,
659     OPT_QUEUE_DROP,
660
661     /* Stop conditions. */
662     OPT_MAX_STATES,
663     OPT_MAX_ERRORS,
664     OPT_TIME_LIMIT,
665
666     /* User interface. */
667     OPT_PROGRESS,
668     OPT_VERBOSITY,
669     OPT_FAILURE_VERBOSITY,
670   };
671
672 static const struct argv_option mc_argv_options[] =
673   {
674     {"strategy", 0, required_argument, OPT_STRATEGY},
675     {"max-depth", 0, required_argument, OPT_MAX_DEPTH},
676     {"hash-bits", 0, required_argument, OPT_HASH_BITS},
677     {"path", 0, required_argument, OPT_PATH},
678     {"queue-limit", 0, required_argument, OPT_QUEUE_LIMIT},
679     {"queue-drop", 0, required_argument, OPT_QUEUE_DROP},
680     {"seed", 0, required_argument, OPT_SEED},
681     {"max-states", 0, required_argument, OPT_MAX_STATES},
682     {"max-errors", 0, required_argument, OPT_MAX_ERRORS},
683     {"time-limit", 0, required_argument, OPT_TIME_LIMIT},
684     {"progress", 0, required_argument, OPT_PROGRESS},
685     {"verbosity", 0, required_argument, OPT_VERBOSITY},
686     {"failure-verbosity", 0, required_argument, OPT_FAILURE_VERBOSITY},
687   };
688 enum { N_MC_ARGV_OPTIONS = sizeof mc_argv_options / sizeof *mc_argv_options };
689
690 /* Called by argv_parser_run to indicate that option ID has been
691    parsed. */
692 static void
693 mc_parser_option_callback (int id, void *mc_options_)
694 {
695   struct mc_options *options = mc_options_;
696   switch (id)
697     {
698     case OPT_STRATEGY:
699       if (mc_options_get_strategy (options) == MC_PATH)
700         error (1, 0, "--strategy and --path are mutually exclusive");
701
702       if (!strcmp (optarg, "broad"))
703         mc_options_set_strategy (options, MC_BROAD);
704       else if (!strcmp (optarg, "deep"))
705         mc_options_set_strategy (options, MC_DEEP);
706       else if (!strcmp (optarg, "random"))
707         mc_options_set_strategy (options, MC_RANDOM);
708       else
709         error (1, 0,
710                "strategy must be \"broad\", \"deep\", or \"random\"");
711       break;
712
713     case OPT_MAX_DEPTH:
714       mc_options_set_max_depth (options, atoi (optarg));
715       break;
716
717     case OPT_HASH_BITS:
718       {
719         int requested_hash_bits = atoi (optarg);
720         int hash_bits;
721         mc_options_set_hash_bits (options, requested_hash_bits);
722         hash_bits = mc_options_get_hash_bits (options);
723         if (hash_bits != requested_hash_bits)
724           error (0, 0, "hash bits adjusted to %d.", hash_bits);
725       }
726       break;
727
728     case OPT_PATH:
729       {
730         struct mc_path path;
731         char *op;
732
733         if (mc_options_get_strategy (options) != MC_BROAD)
734           error (1, 0, "--strategy and --path are mutually exclusive");
735
736         mc_path_init (&path);
737         for (op = strtok (optarg, ":, \t"); op != NULL;
738              op = strtok (NULL, ":, \t"))
739           mc_path_push (&path, atoi (op));
740         if (mc_path_get_length (&path) == 0)
741           error (1, 0, "at least one value must be specified on --path");
742         mc_options_set_follow_path (options, &path);
743         mc_path_destroy (&path);
744       }
745       break;
746
747     case OPT_QUEUE_LIMIT:
748       mc_options_set_queue_limit (options, atoi (optarg));
749       break;
750
751     case OPT_QUEUE_DROP:
752       if (!strcmp (optarg, "newest"))
753         mc_options_set_queue_limit_strategy (options, MC_DROP_NEWEST);
754       else if (!strcmp (optarg, "oldest"))
755         mc_options_set_queue_limit_strategy (options, MC_DROP_OLDEST);
756       else if (!strcmp (optarg, "random"))
757         mc_options_set_queue_limit_strategy (options, MC_DROP_RANDOM);
758       else
759         error (1, 0, "--queue-drop argument must be \"newest\", "
760                "\"oldest\", or \"random\"");
761       break;
762
763     case OPT_SEED:
764       mc_options_set_seed (options, atoi (optarg));
765       break;
766
767     case OPT_MAX_STATES:
768       mc_options_set_max_unique_states (options, atoi (optarg));
769       break;
770
771     case OPT_MAX_ERRORS:
772       mc_options_set_max_errors (options, atoi (optarg));
773       break;
774
775     case OPT_TIME_LIMIT:
776       mc_options_set_time_limit (options, atof (optarg));
777       break;
778
779     case OPT_PROGRESS:
780       if (!strcmp (optarg, "none"))
781         mc_options_set_progress_usec (options, 0);
782       else if (!strcmp (optarg, "dots"))
783         mc_options_set_progress_func (options, mc_progress_dots);
784       else if (!strcmp (optarg, "fancy"))
785         mc_options_set_progress_func (options, mc_progress_fancy);
786       else if (!strcmp (optarg, "verbose"))
787         mc_options_set_progress_func (options, mc_progress_verbose);
788       break;
789
790     case OPT_VERBOSITY:
791       mc_options_set_verbosity (options, atoi (optarg));
792       break;
793
794     case OPT_FAILURE_VERBOSITY:
795       mc_options_set_failure_verbosity (options, atoi (optarg));
796       break;
797
798     default:
799       NOT_REACHED ();
800     }
801 }
802
803 /* Adds the model checker command line options to the specified
804    command line PARSER.  Model checker options parsed from the
805    command line will be applied to OPTIONS. */
806 void
807 mc_options_register_argv_parser (struct mc_options *options,
808                                  struct argv_parser *parser)
809 {
810   argv_parser_add_options (parser, mc_argv_options, N_MC_ARGV_OPTIONS,
811                            mc_parser_option_callback, options);
812 }
813
814 /* Prints a reference for the model checker command line options
815    to stdout. */
816 void
817 mc_options_usage (void)
818 {
819   fputs (
820     "\nModel checker search algorithm options:\n"
821     "  --strategy=STRATEGY  Basic search strategy.  One of:\n"
822     "                         broad: breadth-first search (default)\n"
823     "                         deep: depth-first search\n"
824     "                         random: randomly ordered search\n"
825     "  --path=#[,#]...      Fixes the exact search path to follow;\n"
826     "                       mutually exclusive with --strategy\n"
827     "  --max-depth=MAX      Limits search depth to MAX.  The initial\n"
828     "                       states are at depth 1.\n"
829     "  --hash-bits=BITS     Use 2**BITS size hash table to avoid\n"
830     "                       duplicate states (0 will disable hashing)\n"
831     "  --seed=SEED          Sets the random number seed\n"
832     "\nModel checker queuing options:\n"
833     "  --queue-limit=N      Limit queue to N states (default: 10000)\n"
834     "  --queue-drop=TYPE    How to drop states when queue overflows:\n"
835     "                         newest: drop most recently added state\n"
836     "                         oldest: drop least recently added state\n"
837     "                         random (default): drop a random state\n"
838     "\nModel checker stop condition options:\n"
839     "  --max-states=N       Stop after visiting N unique states\n"
840     "  --max-errors=N       Stop after N errors (default: 1)\n"
841     "  --time-limit=SECS    Stop after SECS seconds\n"
842     "\nModel checker user interface options:\n"
843     "  --progress=TYPE      Show progress according to TYPE.  One of:\n"
844     "                         none: Do not output progress message\n"
845     "                         dots (default): Output lines of dots\n"
846     "                         fancy: Show a few stats\n"
847     "                         verbose: Show all available stats\n"
848     "  --verbosity=LEVEL    Verbosity level before an error (default: 1)\n"
849     "  --failure-verbosity=LEVEL  Verbosity level for replaying failure\n"
850     "                       cases (default: 2)\n",
851     stdout);
852 }
853 \f
854 /* Results of a model checking run. */
855 struct mc_results
856   {
857     /* Overall results. */
858     enum mc_stop_reason stop_reason;    /* Why the run ended. */
859     int unique_state_count;             /* Number of unique states checked. */
860     int error_count;                    /* Number of errors found. */
861
862     /* Depth statistics. */
863     int max_depth_reached;              /* Max depth state examined. */
864     unsigned long int depth_sum;        /* Sum of depths. */
865     int n_depths;                       /* Number of depths in depth_sum. */
866
867     /* If error_count > 0, path to the last error reported. */
868     struct mc_path error_path;
869
870     /* States dropped... */
871     int duplicate_dropped_states;       /* ...as duplicates. */
872     int off_path_dropped_states;        /* ...as off-path (MC_PATH only). */
873     int depth_dropped_states;           /* ...due to excessive depth. */
874     int queue_dropped_states;           /* ...due to queue overflow. */
875
876     /* Queue statistics. */
877     int queued_unprocessed_states;      /* Enqueued but never dequeued. */
878     int max_queue_length;               /* Maximum queue length observed. */
879
880     /* Timing. */
881     struct timeval start;               /* Start of model checking run. */
882     struct timeval end;                 /* End of model checking run. */
883   };
884
885 /* Creates, initializes, and returns a new set of results. */
886 static struct mc_results *
887 mc_results_create (void)
888 {
889   struct mc_results *results = xcalloc (1, sizeof (struct mc_results));
890   results->stop_reason = MC_CONTINUING;
891   gettimeofday (&results->start, NULL);
892   return results;
893 }
894
895 /* Destroys RESULTS. */
896 void
897 mc_results_destroy (struct mc_results *results)
898 {
899   if (results != NULL)
900     {
901       mc_path_destroy (&results->error_path);
902       free (results);
903     }
904 }
905
906 /* Returns RESULTS's reason that the model checking run
907    terminated.  The possible reasons are:
908
909    - MC_CONTINUING: The run is not actually yet complete.  This
910      can only be returned before mc_run has returned, e.g. when
911      the progress function set by mc_options_set_progress_func
912      examines the run's results.
913
914    - MC_SUCCESS: The run completed because the queue emptied.
915      The entire state space might not have been explored due to a
916      requested limit on maximum depth, hash collisions, etc.
917
918    - MC_MAX_UNIQUE_STATES: The run completed because as many
919      unique states have been checked as were requested (using
920      mc_options_set_max_unique_states).
921
922    - MC_MAX_ERROR_COUNT: The run completed because the maximum
923      requested number of errors (by default, 1 error) was
924      reached.
925
926    - MC_END_OF_PATH: The run completed because the path specified
927      with mc_options_set_follow_path was fully traversed.
928
929    - MC_TIMEOUT: The run completed because the time limit set
930      with mc_options_set_time_limit was exceeded.
931
932    - MC_INTERRUPTED: The run completed because SIGINT was caught
933      (typically, due to the user typing Ctrl+C). */
934 enum mc_stop_reason
935 mc_results_get_stop_reason (const struct mc_results *results)
936 {
937   return results->stop_reason;
938 }
939
940 /* Returns the number of unique states checked specified by
941    RESULTS. */
942 int
943 mc_results_get_unique_state_count (const struct mc_results *results)
944 {
945   return results->unique_state_count;
946 }
947
948 /* Returns the number of errors found specified by RESULTS. */
949 int
950 mc_results_get_error_count (const struct mc_results *results)
951 {
952   return results->error_count;
953 }
954
955 /* Returns the maximum depth reached during the model checker run
956    represented by RESULTS.  The initial states are at depth 1,
957    their child states at depth 2, and so on. */
958 int
959 mc_results_get_max_depth_reached (const struct mc_results *results)
960 {
961   return results->max_depth_reached;
962 }
963
964 /* Returns the mean depth reached during the model checker run
965    represented by RESULTS. */
966 double
967 mc_results_get_mean_depth_reached (const struct mc_results *results)
968 {
969   return (results->n_depths == 0
970           ? 0
971           : (double) results->depth_sum / results->n_depths);
972 }
973
974 /* Returns the path traversed to obtain the last error
975    encountered during the model checker run represented by
976    RESULTS.  Returns a null pointer if the run did not report any
977    errors. */
978 const struct mc_path *
979 mc_results_get_error_path (const struct mc_results *results)
980 {
981   return results->error_count > 0 ? &results->error_path : NULL;
982 }
983
984 /* Returns the number of states dropped as duplicates (based on
985    hash value) during the model checker run represented by
986    RESULTS. */
987 int
988 mc_results_get_duplicate_dropped_states (const struct mc_results *results)
989 {
990   return results->duplicate_dropped_states;
991 }
992
993 /* Returns the number of states dropped because they were off the
994    path specified by mc_options_set_follow_path during the model
995    checker run represented by RESULTS.  A nonzero value here
996    indicates a missing call to mc_include_state in the
997    client-supplied mutation function. */
998 int
999 mc_results_get_off_path_dropped_states (const struct mc_results *results)
1000 {
1001   return results->off_path_dropped_states;
1002 }
1003
1004 /* Returns the number of states dropped because their depth
1005    exceeded the maximum specified with mc_options_set_max_depth
1006    during the model checker run represented by RESULTS. */
1007 int
1008 mc_results_get_depth_dropped_states (const struct mc_results *results)
1009 {
1010   return results->depth_dropped_states;
1011 }
1012
1013 /* Returns the number of states dropped from the queue due to
1014    queue overflow during the model checker run represented by
1015    RESULTS. */
1016 int
1017 mc_results_get_queue_dropped_states (const struct mc_results *results)
1018 {
1019   return results->queue_dropped_states;
1020 }
1021
1022 /* Returns the number of states that were checked and enqueued
1023    but never dequeued and processed during the model checker run
1024    represented by RESULTS.  This is zero if the stop reason is
1025    MC_CONTINUING or MC_SUCCESS; otherwise, it is the number of
1026    states in the queue at the time that the checking run
1027    stopped. */
1028 int
1029 mc_results_get_queued_unprocessed_states (const struct mc_results *results)
1030 {
1031   return results->queued_unprocessed_states;
1032 }
1033
1034 /* Returns the maximum length of the queue during the model
1035    checker run represented by RESULTS.  If this is equal to the
1036    maximum queue length, then the queue (probably) overflowed
1037    during the run; otherwise, it did not overflow. */
1038 int
1039 mc_results_get_max_queue_length (const struct mc_results *results)
1040 {
1041   return results->max_queue_length;
1042 }
1043
1044 /* Returns the time at which the model checker run represented by
1045    RESULTS started. */
1046 struct timeval
1047 mc_results_get_start (const struct mc_results *results)
1048 {
1049   return results->start;
1050 }
1051
1052 /* Returns the time at which the model checker run represented by
1053    RESULTS ended.  (This function may not be called while the run
1054    is still ongoing.) */
1055 struct timeval
1056 mc_results_get_end (const struct mc_results *results)
1057 {
1058   assert (results->stop_reason != MC_CONTINUING);
1059   return results->end;
1060 }
1061
1062 /* Returns the number of seconds obtained by subtracting time Y
1063    from time X. */
1064 static double
1065 timeval_subtract (struct timeval x, struct timeval y)
1066 {
1067   /* From libc.info. */
1068   double difference;
1069
1070   /* Perform the carry for the later subtraction by updating Y. */
1071   if (x.tv_usec < y.tv_usec) {
1072     int nsec = (y.tv_usec - x.tv_usec) / 1000000 + 1;
1073     y.tv_usec -= 1000000 * nsec;
1074     y.tv_sec += nsec;
1075   }
1076   if (x.tv_usec - y.tv_usec > 1000000) {
1077     int nsec = (x.tv_usec - y.tv_usec) / 1000000;
1078     y.tv_usec += 1000000 * nsec;
1079     y.tv_sec -= nsec;
1080   }
1081
1082   /* Compute the time remaining to wait.
1083      `tv_usec' is certainly positive. */
1084   difference = (x.tv_sec - y.tv_sec) + (x.tv_usec - y.tv_usec) / 1000000.0;
1085   if (x.tv_sec < y.tv_sec)
1086     difference = -difference;
1087   return difference;
1088 }
1089
1090
1091 /* Returns the duration, in seconds, of the model checker run
1092    represented by RESULTS.  (This function may not be called
1093    while the run is still ongoing.) */
1094 double
1095 mc_results_get_duration (const struct mc_results *results)
1096 {
1097   assert (results->stop_reason != MC_CONTINUING);
1098   return timeval_subtract (results->end, results->start);
1099 }
1100
1101 /* Prints a description of RESULTS to stream F. */
1102 void
1103 mc_results_print (const struct mc_results *results, FILE *f)
1104 {
1105   enum mc_stop_reason reason = mc_results_get_stop_reason (results);
1106
1107   if (reason != MC_CONTINUING)
1108     fprintf (f, "Stopped by: %s\n",
1109              reason == MC_SUCCESS ? "state space exhaustion"
1110              : reason == MC_MAX_UNIQUE_STATES ? "reaching max unique states"
1111              : reason == MC_MAX_ERROR_COUNT ? "reaching max error count"
1112              : reason == MC_END_OF_PATH ? "reached end of specified path"
1113              : reason == MC_TIMEOUT ? "reaching time limit"
1114              : reason == MC_INTERRUPTED ? "user interruption"
1115              : "unknown reason");
1116   fprintf (f, "Errors found: %d\n\n", mc_results_get_error_count (results));
1117
1118   fprintf (f, "Unique states checked: %d\n",
1119            mc_results_get_unique_state_count (results));
1120   fprintf (f, "Maximum depth reached: %d\n",
1121            mc_results_get_max_depth_reached (results));
1122   fprintf (f, "Mean depth reached: %.2f\n\n",
1123            mc_results_get_mean_depth_reached (results));
1124
1125   fprintf (f, "Dropped duplicate states: %d\n",
1126            mc_results_get_duplicate_dropped_states (results));
1127   fprintf (f, "Dropped off-path states: %d\n",
1128            mc_results_get_off_path_dropped_states (results));
1129   fprintf (f, "Dropped too-deep states: %d\n",
1130            mc_results_get_depth_dropped_states (results));
1131   fprintf (f, "Dropped queue-overflow states: %d\n",
1132            mc_results_get_queue_dropped_states (results));
1133   fprintf (f, "Checked states still queued when stopped: %d\n",
1134            mc_results_get_queued_unprocessed_states (results));
1135   fprintf (f, "Maximum queue length reached: %d\n",
1136            mc_results_get_max_queue_length (results));
1137
1138   if (reason != MC_CONTINUING)
1139     fprintf (f, "\nRuntime: %.2f seconds\n",
1140              mc_results_get_duration (results));
1141 }
1142 \f
1143 /* An active model checking run. */
1144 struct mc
1145   {
1146     /* Related data structures. */
1147     const struct mc_class *class;
1148     struct mc_options *options;
1149     struct mc_results *results;
1150
1151     /* Array of 2**(options->hash_bits) bits representing states
1152        already visited. */
1153     unsigned char *hash;
1154
1155     /* State queue. */
1156     struct mc_state **queue;            /* Array of pointers to states. */
1157     struct deque queue_deque;           /* Deque. */
1158
1159     /* State currently being built by "init" or "mutate". */
1160     struct mc_path path;                /* Path to current state. */
1161     struct string path_string;          /* Buffer for path_string function. */
1162     bool state_named;                   /* mc_name_operation called? */
1163     bool state_error;                   /* mc_error called? */
1164
1165     /* Statistics for calling the progress function. */
1166     unsigned int progress;              /* Current progress value. */
1167     unsigned int next_progress;         /* Next value to call progress func. */
1168     unsigned int prev_progress;         /* Last value progress func called. */
1169     struct timeval prev_progress_time;  /* Last time progress func called. */
1170
1171     /* Information for handling and restoring SIGINT. */
1172     bool interrupted;                   /* SIGINT received? */
1173     bool *saved_interrupted_ptr;        /* Saved value of interrupted_ptr. */
1174     void (*saved_sigint) (int);         /* Saved SIGINT handler. */
1175   };
1176
1177 /* A state in the queue. */
1178 struct mc_state
1179   {
1180     struct mc_path path;                /* Path to this state. */
1181     void *data;                         /* Client-supplied data. */
1182   };
1183
1184 /* Points to the current struct mc's "interrupted" member. */
1185 static bool *interrupted_ptr = NULL;
1186
1187 static const char *path_string (struct mc *);
1188 static void free_state (const struct mc *, struct mc_state *);
1189 static void stop (struct mc *, enum mc_stop_reason);
1190 static struct mc_state *make_state (const struct mc *, void *);
1191 static size_t random_queue_index (struct mc *);
1192 static void enqueue_state (struct mc *, struct mc_state *);
1193 static void do_error_state (struct mc *);
1194 static void next_operation (struct mc *);
1195 static bool is_off_path (const struct mc *);
1196 static void sigint_handler (int signum);
1197 static void init_mc (struct mc *,
1198                      const struct mc_class *, struct mc_options *);
1199 static void finish_mc (struct mc *);
1200
1201 /* Runs the model checker on the client-specified CLASS with the
1202    client-specified OPTIONS.  OPTIONS may be a null pointer if
1203    the defaults are acceptable.  Destroys OPTIONS; use
1204    mc_options_clone if a copy is needed.
1205
1206    Returns the results of the model checking run, which must be
1207    destroyed by the client with mc_results_destroy.
1208
1209    To pass auxiliary data to the functions in CLASS, use
1210    mc_options_set_aux on OPTIONS, which may be retrieved from the
1211    CLASS functions using mc_get_aux. */
1212 struct mc_results *
1213 mc_run (const struct mc_class *class, struct mc_options *options)
1214 {
1215   struct mc mc;
1216
1217   init_mc (&mc, class, options);
1218   while (!deque_is_empty (&mc.queue_deque)
1219          && mc.results->stop_reason == MC_CONTINUING)
1220     {
1221       struct mc_state *state = mc.queue[deque_pop_front (&mc.queue_deque)];
1222       mc_path_copy (&mc.path, &state->path);
1223       mc_path_push (&mc.path, 0);
1224       class->mutate (&mc, state->data);
1225       free_state (&mc, state);
1226       if (mc.interrupted)
1227         stop (&mc, MC_INTERRUPTED);
1228     }
1229   finish_mc (&mc);
1230
1231   return mc.results;
1232 }
1233
1234 /* Tests whether the current operation is one that should be
1235    performed, checked, and enqueued.  If so, returns true.
1236    Otherwise, returns false and, unless checking is stopped,
1237    advances to the next state.  The caller should then advance
1238    to the next operation.
1239
1240    This function should be called from the client-provided
1241    "mutate" function, according to the pattern explained in the
1242    big comment at the top of model-checker.h. */
1243 bool
1244 mc_include_state (struct mc *mc)
1245 {
1246   if (mc->results->stop_reason != MC_CONTINUING)
1247     return false;
1248   else if (is_off_path (mc))
1249     {
1250       next_operation (mc);
1251       return false;
1252     }
1253   else
1254     return true;
1255 }
1256
1257 /* Tests whether HASH represents a state that has (probably)
1258    already been enqueued.  If not, returns false and marks HASH
1259    so that it will be treated as a duplicate in the future.  If
1260    so, returns true and advances to the next state.  The
1261    caller should then advance to the next operation.
1262
1263    This function should be called from the client-provided
1264    "mutate" function, according to the pattern explained in the
1265    big comment at the top of model-checker.h. */
1266 bool
1267 mc_discard_dup_state (struct mc *mc, unsigned int hash)
1268 {
1269   if (!mc->state_error && mc->options->hash_bits > 0)
1270     {
1271       hash &= (1u << mc->options->hash_bits) - 1;
1272       if (TEST_BIT (mc->hash, hash))
1273         {
1274           if (mc->options->verbosity > 2)
1275             fprintf (mc->options->output_file,
1276                      "    [%s] discard duplicate state\n", path_string (mc));
1277           mc->results->duplicate_dropped_states++;
1278           next_operation (mc);
1279           return true;
1280         }
1281       SET_BIT (mc->hash, hash);
1282     }
1283   return false;
1284 }
1285
1286 /* Names the current state NAME, which may contain
1287    printf-style format specifications.  NAME should be a
1288    human-readable name for the current operation.
1289
1290    This function should be called from the client-provided
1291    "mutate" function, according to the pattern explained in the
1292    big comment at the top of model-checker.h. */
1293 void
1294 mc_name_operation (struct mc *mc, const char *name, ...)
1295 {
1296   va_list args;
1297
1298   va_start (args, name);
1299   mc_vname_operation (mc, name, args);
1300   va_end (args);
1301 }
1302
1303 /* Names the current state NAME, which may contain
1304    printf-style format specifications, for which the
1305    corresponding arguments must be given in ARGS.  NAME should be
1306    a human-readable name for the current operation.
1307
1308    This function should be called from the client-provided
1309    "mutate" function, according to the pattern explained in the
1310    big comment at the top of model-checker.h. */
1311 void
1312 mc_vname_operation (struct mc *mc, const char *name, va_list args)
1313 {
1314   if (mc->state_named && mc->options->verbosity > 0)
1315     fprintf (mc->options->output_file, "  [%s] warning: duplicate call "
1316              "to mc_name_operation (missing call to mc_add_state?)\n",
1317              path_string (mc));
1318   mc->state_named = true;
1319
1320   if (mc->options->verbosity > 1)
1321     {
1322       fprintf (mc->options->output_file, "  [%s] ", path_string (mc));
1323       vfprintf (mc->options->output_file, name, args);
1324       putc ('\n', mc->options->output_file);
1325     }
1326 }
1327
1328 /* Reports the given error MESSAGE for the current operation.
1329    The resulting state should still be passed to mc_add_state
1330    when all relevant error messages have been issued.  The state
1331    will not, however, be enqueued for later mutation of its own.
1332
1333    By default, model checking stops after the first error
1334    encountered.
1335
1336    This function should be called from the client-provided
1337    "mutate" function, according to the pattern explained in the
1338    big comment at the top of model-checker.h. */
1339 void
1340 mc_error (struct mc *mc, const char *message, ...)
1341 {
1342   va_list args;
1343
1344   if (mc->results->stop_reason != MC_CONTINUING)
1345     return;
1346
1347   if (mc->options->verbosity > 1)
1348     fputs ("    ", mc->options->output_file);
1349   fprintf (mc->options->output_file, "[%s] error: ",
1350            path_string (mc));
1351   va_start (args, message);
1352   vfprintf (mc->options->output_file, message, args);
1353   va_end (args);
1354   putc ('\n', mc->options->output_file);
1355
1356   mc->state_error = true;
1357 }
1358
1359 /* Enqueues DATA as the state corresponding to the current
1360    operation.  The operation should have been named with a call
1361    to mc_name_operation, and it should have been checked by the
1362    caller (who should have reported any errors with mc_error).
1363
1364    This function should be called from the client-provided
1365    "mutate" function, according to the pattern explained in the
1366    big comment at the top of model-checker.h. */
1367 void
1368 mc_add_state (struct mc *mc, void *data)
1369 {
1370   if (!mc->state_named && mc->options->verbosity > 0)
1371     fprintf (mc->options->output_file, "  [%s] warning: unnamed state\n",
1372              path_string (mc));
1373
1374   if (mc->results->stop_reason != MC_CONTINUING)
1375     {
1376       /* Nothing to do. */
1377     }
1378   else if (mc->state_error)
1379     do_error_state (mc);
1380   else if (is_off_path (mc))
1381     mc->results->off_path_dropped_states++;
1382   else if (mc->path.length + 1 > mc->options->max_depth)
1383     mc->results->depth_dropped_states++;
1384   else
1385     {
1386       /* This is the common case. */
1387       mc->results->unique_state_count++;
1388       if (mc->results->unique_state_count >= mc->options->max_unique_states)
1389         stop (mc, MC_MAX_UNIQUE_STATES);
1390       enqueue_state (mc, make_state (mc, data));
1391       next_operation (mc);
1392       return;
1393     }
1394
1395   mc->class->destroy (mc, data);
1396   next_operation (mc);
1397 }
1398
1399 /* Returns the options that were passed to mc_run for model
1400    checker MC. */
1401 const struct mc_options *
1402 mc_get_options (const struct mc *mc)
1403 {
1404   return mc->options;
1405 }
1406
1407 /* Returns the current state of the results for model checker
1408    MC.  This function is appropriate for use from the progress
1409    function set by mc_options_set_progress_func.
1410
1411    Not all of the results are meaningful before model checking
1412    completes. */
1413 const struct mc_results *
1414 mc_get_results (const struct mc *mc)
1415 {
1416   return mc->results;
1417 }
1418
1419 /* Returns the auxiliary data set on the options passed to mc_run
1420    with mc_options_set_aux. */
1421 void *
1422 mc_get_aux (const struct mc *mc)
1423 {
1424   return mc_options_get_aux (mc_get_options (mc));
1425 }
1426 \f
1427 /* Expresses MC->path as a string and returns the string. */
1428 static const char *
1429 path_string (struct mc *mc)
1430 {
1431   ds_clear (&mc->path_string);
1432   mc_path_to_string (&mc->path, &mc->path_string);
1433   return ds_cstr (&mc->path_string);
1434 }
1435
1436 /* Frees STATE, including client data. */
1437 static void
1438 free_state (const struct mc *mc, struct mc_state *state)
1439 {
1440   mc->class->destroy (mc, state->data);
1441   mc_path_destroy (&state->path);
1442   free (state);
1443 }
1444
1445 /* Sets STOP_REASON as the reason that MC's processing stopped,
1446    unless MC is already stopped. */
1447 static void
1448 stop (struct mc *mc, enum mc_stop_reason stop_reason)
1449 {
1450   if (mc->results->stop_reason == MC_CONTINUING)
1451     mc->results->stop_reason = stop_reason;
1452 }
1453
1454 /* Creates and returns a new state whose path is copied from
1455    MC->path and whose data is specified by DATA. */
1456 static struct mc_state *
1457 make_state (const struct mc *mc, void *data)
1458 {
1459   struct mc_state *new = xmalloc (sizeof *new);
1460   mc_path_init (&new->path);
1461   mc_path_copy (&new->path, &mc->path);
1462   new->data = data;
1463   return new;
1464 }
1465
1466 /* Returns the index in MC->queue of a random element in the
1467    queue. */
1468 static size_t
1469 random_queue_index (struct mc *mc)
1470 {
1471   assert (!deque_is_empty (&mc->queue_deque));
1472   return deque_front (&mc->queue_deque,
1473                       rand () % deque_count (&mc->queue_deque));
1474 }
1475
1476 /* Adds NEW to MC's state queue, dropping a state if necessary
1477    due to overflow. */
1478 static void
1479 enqueue_state (struct mc *mc, struct mc_state *new)
1480 {
1481   size_t idx;
1482
1483   if (new->path.length > mc->results->max_depth_reached)
1484     mc->results->max_depth_reached = new->path.length;
1485   mc->results->depth_sum += new->path.length;
1486   mc->results->n_depths++;
1487
1488   if (deque_count (&mc->queue_deque) < mc->options->queue_limit)
1489     {
1490       /* Add new state to queue. */
1491       if (deque_is_full (&mc->queue_deque))
1492         mc->queue = deque_expand (&mc->queue_deque,
1493                                    mc->queue, sizeof *mc->queue);
1494       switch (mc->options->strategy)
1495         {
1496         case MC_BROAD:
1497           idx = deque_push_back (&mc->queue_deque);
1498           break;
1499         case MC_DEEP:
1500           idx = deque_push_front (&mc->queue_deque);
1501           break;
1502         case MC_RANDOM:
1503           if (!deque_is_empty (&mc->queue_deque))
1504             {
1505               idx = random_queue_index (mc);
1506               mc->queue[deque_push_front (&mc->queue_deque)]
1507                 = mc->queue[idx];
1508             }
1509           else
1510             idx = deque_push_front (&mc->queue_deque);
1511           break;
1512         case MC_PATH:
1513           assert (deque_is_empty (&mc->queue_deque));
1514           assert (!is_off_path (mc));
1515           idx = deque_push_back (&mc->queue_deque);
1516           if (mc->path.length
1517               >= mc_path_get_length (&mc->options->follow_path))
1518             stop (mc, MC_END_OF_PATH);
1519           break;
1520         default:
1521           NOT_REACHED ();
1522         }
1523       if (deque_count (&mc->queue_deque) > mc->results->max_queue_length)
1524         mc->results->max_queue_length = deque_count (&mc->queue_deque);
1525     }
1526   else
1527     {
1528       /* Queue has reached limit, so replace an existing
1529          state. */
1530       assert (mc->options->strategy != MC_PATH);
1531       assert (!deque_is_empty (&mc->queue_deque));
1532       mc->results->queue_dropped_states++;
1533       switch (mc->options->queue_limit_strategy)
1534         {
1535         case MC_DROP_NEWEST:
1536           free_state (mc, new);
1537           return;
1538         case MC_DROP_OLDEST:
1539           switch (mc->options->strategy)
1540             {
1541             case MC_BROAD:
1542               idx = deque_front (&mc->queue_deque, 0);
1543               break;
1544             case MC_DEEP:
1545               idx = deque_back (&mc->queue_deque, 0);
1546               break;
1547             case MC_RANDOM:
1548             case MC_PATH:
1549             default:
1550               NOT_REACHED ();
1551             }
1552           break;
1553         case MC_DROP_RANDOM:
1554           idx = random_queue_index (mc);
1555           break;
1556         default:
1557           NOT_REACHED ();
1558         }
1559       free_state (mc, mc->queue[idx]);
1560     }
1561   mc->queue[idx] = new;
1562 }
1563
1564 /* Process an error state being added to MC. */
1565 static void
1566 do_error_state (struct mc *mc)
1567 {
1568   mc->results->error_count++;
1569   if (mc->results->error_count >= mc->options->max_errors)
1570     stop (mc, MC_MAX_ERROR_COUNT);
1571
1572   mc_path_copy (&mc->results->error_path, &mc->path);
1573
1574   if (mc->options->failure_verbosity > mc->options->verbosity)
1575     {
1576       struct mc_options *path_options;
1577
1578       fprintf (mc->options->output_file, "[%s] retracing error path:\n",
1579                path_string (mc));
1580       path_options = mc_options_clone (mc->options);
1581       mc_options_set_verbosity (path_options, mc->options->failure_verbosity);
1582       mc_options_set_failure_verbosity (path_options, 0);
1583       mc_options_set_follow_path (path_options, &mc->path);
1584
1585       mc_results_destroy (mc_run (mc->class, path_options));
1586
1587       putc ('\n', mc->options->output_file);
1588     }
1589 }
1590
1591 /* Advances MC to start processing the operation following the
1592    current one. */
1593 static void
1594 next_operation (struct mc *mc)
1595 {
1596   mc_path_push (&mc->path, mc_path_pop (&mc->path) + 1);
1597   mc->state_error = false;
1598   mc->state_named = false;
1599
1600   if (++mc->progress >= mc->next_progress)
1601     {
1602       struct timeval now;
1603       double elapsed, delta;
1604
1605       if (mc->results->stop_reason == MC_CONTINUING
1606           && !mc->options->progress_func (mc))
1607         stop (mc, MC_INTERRUPTED);
1608
1609       gettimeofday (&now, NULL);
1610
1611       if (mc->options->time_limit > 0.0
1612           && (timeval_subtract (now, mc->results->start)
1613               > mc->options->time_limit))
1614         stop (mc, MC_TIMEOUT);
1615
1616       elapsed = timeval_subtract (now, mc->prev_progress_time);
1617       if (elapsed > 0.0)
1618         {
1619           /* Re-estimate the amount of progress to take
1620              progress_usec microseconds. */
1621           unsigned int progress = mc->progress - mc->prev_progress;
1622           double progress_sec = mc->options->progress_usec / 1000000.0;
1623           delta = progress / elapsed * progress_sec;
1624         }
1625       else
1626         {
1627           /* No measurable time at all elapsed during that amount
1628              of progress.  Try doubling the amount of progress
1629              required. */
1630           delta = (mc->progress - mc->prev_progress) * 2;
1631         }
1632
1633       if (delta > 0.0 && delta + mc->progress + 1.0 < UINT_MAX)
1634         mc->next_progress = mc->progress + delta + 1.0;
1635       else
1636         mc->next_progress = mc->progress + (mc->progress - mc->prev_progress);
1637
1638       mc->prev_progress = mc->progress;
1639       mc->prev_progress_time = now;
1640     }
1641 }
1642
1643 /* Returns true if we're tracing an explicit path but the current
1644    operation produces a state off that path, false otherwise. */
1645 static bool
1646 is_off_path (const struct mc *mc)
1647 {
1648   return (mc->options->strategy == MC_PATH
1649           && (mc_path_back (&mc->path)
1650               != mc_path_get_operation (&mc->options->follow_path,
1651                                         mc->path.length - 1)));
1652 }
1653
1654 /* Handler for SIGINT. */
1655 static void
1656 sigint_handler (int signum UNUSED)
1657 {
1658   /* Just mark the model checker as interrupted. */
1659   *interrupted_ptr = true;
1660 }
1661
1662 /* Initializes MC as a model checker with the given CLASS and
1663    OPTIONS.  OPTIONS may be null to use the default options. */
1664 static void
1665 init_mc (struct mc *mc, const struct mc_class *class,
1666          struct mc_options *options)
1667 {
1668   /* Validate and adjust OPTIONS. */
1669   if (options == NULL)
1670     options = mc_options_create ();
1671   assert (options->queue_limit_strategy != MC_DROP_OLDEST
1672           || options->strategy != MC_RANDOM);
1673   if (options->strategy == MC_PATH)
1674     {
1675       options->max_depth = INT_MAX;
1676       options->hash_bits = 0;
1677     }
1678   if (options->progress_usec == 0)
1679     {
1680       options->progress_func = null_progress;
1681       if (options->time_limit > 0.0)
1682         options->progress_usec = 250000;
1683     }
1684
1685   /* Initialize MC. */
1686   mc->class = class;
1687   mc->options = options;
1688   mc->results = mc_results_create ();
1689
1690   mc->hash = (mc->options->hash_bits > 0
1691               ? xcalloc (1, DIV_RND_UP (1 << mc->options->hash_bits, CHAR_BIT))
1692               : NULL);
1693
1694   mc->queue = NULL;
1695   deque_init_null (&mc->queue_deque);
1696
1697   mc_path_init (&mc->path);
1698   mc_path_push (&mc->path, 0);
1699   ds_init_empty (&mc->path_string);
1700   mc->state_named = false;
1701   mc->state_error = false;
1702
1703   mc->progress = 0;
1704   mc->next_progress = mc->options->progress_usec != 0 ? 100 : UINT_MAX;
1705   mc->prev_progress = 0;
1706   mc->prev_progress_time = mc->results->start;
1707
1708   if (mc->options->strategy == MC_RANDOM
1709       || options->queue_limit_strategy == MC_DROP_RANDOM)
1710     srand (mc->options->seed);
1711
1712   mc->interrupted = false;
1713   mc->saved_interrupted_ptr = interrupted_ptr;
1714   interrupted_ptr = &mc->interrupted;
1715   mc->saved_sigint = signal (SIGINT, sigint_handler);
1716
1717   class->init (mc);
1718 }
1719
1720 /* Complete the model checker run for MC. */
1721 static void
1722 finish_mc (struct mc *mc)
1723 {
1724   /* Restore signal handlers. */
1725   signal (SIGINT, mc->saved_sigint);
1726   interrupted_ptr = mc->saved_interrupted_ptr;
1727
1728   /* Mark the run complete. */
1729   stop (mc, MC_SUCCESS);
1730   gettimeofday (&mc->results->end, NULL);
1731
1732   /* Empty the queue. */
1733   mc->results->queued_unprocessed_states = deque_count (&mc->queue_deque);
1734   while (!deque_is_empty (&mc->queue_deque))
1735     {
1736       struct mc_state *state = mc->queue[deque_pop_front (&mc->queue_deque)];
1737       free_state (mc, state);
1738     }
1739
1740   /* Notify the progress function of completion. */
1741   mc->options->progress_func (mc);
1742
1743   /* Free memory. */
1744   mc_path_destroy (&mc->path);
1745   ds_destroy (&mc->path_string);
1746   free (mc->options);
1747   free (mc->queue);
1748   free (mc->hash);
1749 }