--- /dev/null
+/* PSPP - computes sample statistics.
+ Copyright (C) 2007 Free Software Foundation, Inc.
+
+ This program is free software; you can redistribute it and/or
+ modify it under the terms of the GNU General Public License as
+ published by the Free Software Foundation; either version 2 of the
+ License, or (at your option) any later version.
+
+ This program is distributed in the hope that it will be useful, but
+ WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with this program; if not, write to the Free Software
+ Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
+ 02110-1301, USA. */
+
+#include <config.h>
+
+#include <language/tests/check-model.h>
+
+#include <errno.h>
+
+#include <libpspp/model-checker.h>
+#include <language/lexer/lexer.h>
+
+#include "error.h"
+#include "fwriteerror.h"
+
+#include "gettext.h"
+#define _(msgid) gettext (msgid)
+#define N_(msgid) msgid
+
+/* (headers) */
+
+/* (specification)
+ "CHECK MODEL" (chm_):
+ search=strategy:broad/deep/random,
+ :mxd(n:max_depth),
+ :hash(n:hash_bits);
+ path=integer list;
+ queue=:limit(n:queue_limit,"%s>0"),
+ drop:newest/oldest/random;
+ seed=integer;
+ stop=:states(n:max_unique_states,"%s>0"),
+ :errors(n:max_errors),
+ :timeout(d:time_limit,"%s>0");
+ progress=progress:none/dots/fancy;
+ output=:verbosity(n:verbosity),
+ :errverbosity(n:err_verbosity),
+ :file(s:output_file).
+*/
+/* (declarations) */
+/* (functions) */
+
+static struct mc_options *parse_options (struct lexer *);
+static void print_results (const struct mc_results *, FILE *);
+
+/* Parses a syntax description of model checker options from
+ LEXER and passes them, along with AUX, to the CHECKER
+ function, which must wrap a call to mc_run and return the
+ mc_results that it returned. This function then prints a
+ description of the mc_results to the output file. Returns
+ true if the model checker run found no errors, false
+ otherwise. */
+bool
+check_model (struct lexer *lexer,
+ struct mc_results *(*checker) (struct mc_options *, void *aux),
+ void *aux)
+{
+ struct mc_options *options;
+ struct mc_results *results;
+ FILE *output_file;
+ bool ok;
+
+ options = parse_options (lexer);
+ if (options == NULL)
+ return false;
+ output_file = mc_options_get_output_file (options);
+
+ results = checker (options, aux);
+
+ print_results (results, output_file);
+
+ if (output_file != stdout && output_file != stderr)
+ {
+ if (fwriteerror (output_file) < 0)
+ {
+ /* We've already discarded the name of the output file.
+ Oh well. */
+ error (0, errno, "error closing output file");
+ }
+ }
+
+ ok = mc_results_get_error_count (results) == 0;
+ mc_results_destroy (results);
+
+ return ok;
+}
+
+/* Fancy progress function for mc_options_set_progress_func. */
+static bool
+fancy_progress (struct mc *mc)
+{
+ const struct mc_results *results = mc_get_results (mc);
+ if (mc_results_get_stop_reason (results) == MC_CONTINUING)
+ fprintf (stderr, "Processed %d unique states, max depth %d, "
+ "dropped %d duplicates...\r",
+ mc_results_get_unique_state_count (results),
+ mc_results_get_max_depth_reached (results),
+ mc_results_get_duplicate_dropped_states (results));
+ else
+ putc ('\n', stderr);
+ return true;
+}
+
+/* Parses options from LEXER and returns a corresponding
+ mc_options, or a null pointer if parsing fails. */
+static struct mc_options *
+parse_options (struct lexer *lexer)
+{
+ struct cmd_check_model cmd;
+ struct mc_options *options;
+
+ if (!parse_check_model (lexer, NULL, &cmd, NULL))
+ return NULL;
+
+ options = mc_options_create ();
+ if (cmd.strategy != -1)
+ mc_options_set_strategy (options,
+ cmd.strategy == CHM_BROAD ? MC_BROAD
+ : cmd.strategy == CHM_DEEP ? MC_DEEP
+ : cmd.strategy == CHM_RANDOM ? MC_RANDOM
+ : -1);
+ if (cmd.sbc_path > 0)
+ {
+ if (cmd.sbc_search > 0)
+ msg (SW, _("PATH and SEARCH subcommands are mutually exclusive. "
+ "Ignoring PATH."));
+ else
+ {
+ struct subc_list_int *list = &cmd.il_path[0];
+ int count = subc_list_int_count (list);
+ if (count > 0)
+ {
+ struct mc_path path;
+ int i;
+
+ mc_path_init (&path);
+ for (i = 0; i < count; i++)
+ mc_path_push (&path, subc_list_int_at (list, i));
+ mc_options_set_follow_path (options, &path);
+ mc_path_destroy (&path);
+ }
+ else
+ msg (SW, _("At least one value must be specified on PATH."));
+ }
+ }
+ if (cmd.max_depth != NOT_LONG)
+ mc_options_set_max_depth (options, cmd.max_depth);
+ if (cmd.hash_bits != NOT_LONG)
+ {
+ int hash_bits;
+ mc_options_set_hash_bits (options, cmd.hash_bits);
+ hash_bits = mc_options_get_hash_bits (options);
+ if (hash_bits != cmd.hash_bits)
+ msg (SW, _("Hash bits adjusted to %d."), hash_bits);
+ }
+ if (cmd.queue_limit != NOT_LONG)
+ mc_options_set_queue_limit (options, cmd.queue_limit);
+ if (cmd.drop != -1)
+ {
+ enum mc_queue_limit_strategy drop
+ = (cmd.drop == CHM_NEWEST ? MC_DROP_NEWEST
+ : cmd.drop == CHM_OLDEST ? MC_DROP_OLDEST
+ : cmd.drop == CHM_RANDOM ? MC_DROP_RANDOM
+ : -1);
+ mc_options_set_queue_limit_strategy (options, drop);
+ }
+ if (cmd.sbc_search > 0)
+ mc_options_set_seed (options, cmd.n_seed[0]);
+ if (cmd.max_unique_states != NOT_LONG)
+ mc_options_set_max_unique_states (options, cmd.max_unique_states);
+ if (cmd.max_errors != NOT_LONG)
+ mc_options_set_max_errors (options, cmd.max_errors);
+ if (cmd.time_limit != SYSMIS)
+ mc_options_set_time_limit (options, cmd.time_limit);
+ if (cmd.verbosity != NOT_LONG)
+ mc_options_set_verbosity (options, cmd.verbosity);
+ if (cmd.err_verbosity != NOT_LONG)
+ mc_options_set_failure_verbosity (options, cmd.err_verbosity);
+ if (cmd.progress != -1)
+ {
+ if (cmd.progress == CHM_NONE)
+ mc_options_set_progress_usec (options, 0);
+ else if (cmd.progress == CHM_DOTS)
+ {
+ /* Nothing to do: that's the default anyway. */
+ }
+ else if (cmd.progress == CHM_FANCY)
+ mc_options_set_progress_func (options, fancy_progress);
+ }
+ if (cmd.output_file != NULL)
+ {
+ FILE *output_file = fopen (cmd.output_file, "w");
+ if (output_file == NULL)
+ {
+ error (0, errno, _("error opening \"%s\" for writing"),
+ cmd.output_file);
+ free_check_model (&cmd);
+ mc_options_destroy (options);
+ return NULL;
+ }
+ mc_options_set_output_file (options, output_file);
+ }
+
+ return options;
+}
+
+/* Prints a description of RESULTS to stream F. */
+static void
+print_results (const struct mc_results *results, FILE *f)
+{
+ enum mc_stop_reason reason = mc_results_get_stop_reason (results);
+
+ fputs ("\n"
+ "MODEL CHECKING SUMMARY\n"
+ "----------------------\n\n", f);
+
+ fprintf (f, "Stopped by: %s\n",
+ reason == MC_SUCCESS ? "state space exhaustion"
+ : reason == MC_MAX_UNIQUE_STATES ? "reaching max unique states"
+ : reason == MC_MAX_ERROR_COUNT ? "reaching max error count"
+ : reason == MC_END_OF_PATH ? "reached end of specified path"
+ : reason == MC_TIMEOUT ? "reaching time limit"
+ : reason == MC_INTERRUPTED ? "user interruption"
+ : "unknown reason");
+ fprintf (f, "Errors found: %d\n\n", mc_results_get_error_count (results));
+
+ fprintf (f, "Unique states checked: %d\n",
+ mc_results_get_unique_state_count (results));
+ fprintf (f, "Maximum depth reached: %d\n",
+ mc_results_get_max_depth_reached (results));
+ fprintf (f, "Mean depth reached: %.2f\n\n",
+ mc_results_get_mean_depth_reached (results));
+
+ fprintf (f, "Dropped duplicate states: %d\n",
+ mc_results_get_duplicate_dropped_states (results));
+ fprintf (f, "Dropped off-path states: %d\n",
+ mc_results_get_off_path_dropped_states (results));
+ fprintf (f, "Dropped too-deep states: %d\n",
+ mc_results_get_depth_dropped_states (results));
+ fprintf (f, "Dropped queue-overflow states: %d\n",
+ mc_results_get_queue_dropped_states (results));
+ fprintf (f, "Checked states still queued when stopped: %d\n",
+ mc_results_get_queued_unprocessed_states (results));
+ fprintf (f, "Maximum queue length reached: %d\n\n",
+ mc_results_get_max_queue_length (results));
+
+ fprintf (f, "Runtime: %.2f seconds\n",
+ mc_results_get_duration (results));
+
+ putc ('\n', f);
+}
+
+/*
+ Local Variables:
+ mode: c
+ End:
+*/
--- /dev/null
+/* PSPP - computes sample statistics.
+ Copyright (C) 2007 Free Software Foundation, Inc.
+
+ This program is free software; you can redistribute it and/or
+ modify it under the terms of the GNU General Public License as
+ published by the Free Software Foundation; either version 2 of the
+ License, or (at your option) any later version.
+
+ This program is distributed in the hope that it will be useful, but
+ WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with this program; if not, write to the Free Software
+ Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
+ 02110-1301, USA. */
+
+#include <config.h>
+
+#include <libpspp/model-checker.h>
+
+#include <limits.h>
+#include <signal.h>
+#include <stdarg.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <sys/time.h>
+
+#include <libpspp/bit-vector.h>
+#include <libpspp/compiler.h>
+#include <libpspp/deque.h>
+#include <libpspp/str.h>
+#include <math/moments.h>
+
+#include "error.h"
+#include "minmax.h"
+#include "xalloc.h"
+\f
+/* Initializes PATH as an empty path. */
+void
+mc_path_init (struct mc_path *path)
+{
+ path->ops = NULL;
+ path->length = 0;
+ path->capacity = 0;
+}
+
+/* Copies the contents of OLD into NEW. */
+void
+mc_path_copy (struct mc_path *new, const struct mc_path *old)
+{
+ if (old->length > new->capacity)
+ {
+ new->capacity = old->length;
+ free (new->ops);
+ new->ops = xnmalloc (new->capacity, sizeof *new->ops);
+ }
+ new->length = old->length;
+ memcpy (new->ops, old->ops, old->length * sizeof *new->ops);
+}
+
+/* Adds OP to the end of PATH. */
+void
+mc_path_push (struct mc_path *path, int op)
+{
+ if (path->length >= path->capacity)
+ path->ops = xnrealloc (path->ops, ++path->capacity, sizeof *path->ops);
+ path->ops[path->length++] = op;
+}
+
+/* Removes and returns the operation at the end of PATH. */
+int
+mc_path_pop (struct mc_path *path)
+{
+ int back = mc_path_back (path);
+ path->length--;
+ return back;
+}
+
+/* Returns the operation at the end of PATH. */
+int
+mc_path_back (const struct mc_path *path)
+{
+ assert (path->length > 0);
+ return path->ops[path->length - 1];
+}
+
+/* Destroys PATH. */
+void
+mc_path_destroy (struct mc_path *path)
+{
+ free (path->ops);
+ path->ops = NULL;
+}
+
+/* Returns the operation in position INDEX in PATH.
+ INDEX must be less than the length of PATH. */
+int
+mc_path_get_operation (const struct mc_path *path, size_t index)
+{
+ assert (index < path->length);
+ return path->ops[index];
+}
+
+/* Returns the number of operations in PATH. */
+size_t
+mc_path_get_length (const struct mc_path *path)
+{
+ return path->length;
+}
+
+/* Appends the operations in PATH to STRING, separating each one
+ with a single space. */
+void
+mc_path_to_string (const struct mc_path *path, struct string *string)
+{
+ size_t i;
+
+ for (i = 0; i < mc_path_get_length (path); i++)
+ {
+ if (i > 0)
+ ds_put_char (string, ' ');
+ ds_put_format (string, "%d", mc_path_get_operation (path, i));
+ }
+}
+\f
+/* Search options. */
+struct mc_options
+ {
+ /* Search strategy. */
+ enum mc_strategy strategy; /* Type of strategy. */
+ int max_depth; /* Limit on depth (or INT_MAX). */
+ int hash_bits; /* Number of bits to hash (or 0). */
+ unsigned int seed; /* Random seed for MC_RANDOM
+ or MC_DROP_RANDOM. */
+ struct mc_path follow_path; /* Path for MC_PATH. */
+
+ /* Queue configuration. */
+ int queue_limit; /* Maximum length of queue. */
+ enum mc_queue_limit_strategy queue_limit_strategy;
+ /* How to choose state to drop
+ from queue. */
+
+ /* Stop conditions. */
+ int max_unique_states; /* Maximum unique states to process. */
+ int max_errors; /* Maximum errors to detect. */
+ double time_limit; /* Maximum time in seconds. */
+
+ /* Output configuration. */
+ int verbosity; /* 0=low, 1=normal, 2+=high. */
+ int failure_verbosity; /* If greater than verbosity,
+ verbosity of error replays. */
+ FILE *output_file; /* File to receive output. */
+
+ /* How to report intermediate progress. */
+ int progress_usec; /* Microseconds between reports. */
+ mc_progress_func *progress_func; /* Function to call on each report. */
+
+ /* Client data. */
+ void *aux;
+ };
+
+/* Default progress function. */
+static bool
+default_progress (struct mc *mc)
+{
+ if (mc_results_get_stop_reason (mc_get_results (mc)) == MC_CONTINUING)
+ putc ('.', stderr);
+ else
+ putc ('\n', stderr);
+ return true;
+}
+
+/* Do-nothing progress function. */
+static bool
+null_progress (struct mc *mc UNUSED)
+{
+ return true;
+}
+
+/* Creates and returns a set of options initialized to the
+ defaults. */
+struct mc_options *
+mc_options_create (void)
+{
+ struct mc_options *options = xmalloc (sizeof *options);
+
+ options->strategy = MC_BROAD;
+ options->max_depth = INT_MAX;
+ options->hash_bits = 20;
+ options->seed = 0;
+ mc_path_init (&options->follow_path);
+
+ options->queue_limit = 10000;
+ options->queue_limit_strategy = MC_DROP_RANDOM;
+
+ options->max_unique_states = INT_MAX;
+ options->max_errors = 1;
+ options->time_limit = 0.0;
+
+ options->verbosity = 1;
+ options->failure_verbosity = 2;
+ options->output_file = stdout;
+ options->progress_usec = 250000;
+ options->progress_func = default_progress;
+
+ options->aux = NULL;
+
+ return options;
+}
+
+/* Returns a copy of the given OPTIONS. */
+struct mc_options *
+mc_options_clone (const struct mc_options *options)
+{
+ return xmemdup (options, sizeof *options);
+}
+
+/* Destroys OPTIONS. */
+void
+mc_options_destroy (struct mc_options *options)
+{
+ mc_path_destroy (&options->follow_path);
+ free (options);
+}
+
+/* Returns the search strategy used for OPTIONS. The choices
+ are:
+
+ - MC_BROAD (the default): Breadth-first search. First tries
+ all the operations with depth 1, then those with depth 2,
+ then those with depth 3, and so on.
+
+ This search algorithm finds the least number of operations
+ needed to trigger a given bug.
+
+ - MC_DEEP: Depth-first search. Searches downward in the tree
+ of states as fast as possible. Good for finding bugs that
+ require long sequences of operations to trigger.
+
+ - MC_RANDOM: Random-first search. Searches through the tree
+ of states in random order. The standard C library's rand
+ function selects the search path; you can control the seed
+ passed to srand using mc_options_set_seed.
+
+ - MC_PATH: Explicit path. Applies an explicitly specified
+ sequence of operations. */
+enum mc_strategy
+mc_options_get_strategy (const struct mc_options *options)
+{
+ return options->strategy;
+}
+
+/* Sets the search strategy used for OPTIONS to STRATEGY.
+
+ This function cannot be used to set MC_PATH as the search
+ strategy. Use mc_options_set_follow_path instead. */
+void
+mc_options_set_strategy (struct mc_options *options, enum mc_strategy strategy)
+{
+ assert (strategy == MC_BROAD
+ || strategy == MC_DEEP
+ || strategy == MC_RANDOM);
+ options->strategy = strategy;
+}
+
+/* Returns OPTION's random seed used by MC_RANDOM and
+ MC_DROP_RANDOM. */
+unsigned int
+mc_options_get_seed (const struct mc_options *options)
+{
+ return options->seed;
+}
+
+/* Set OPTION's random seed used by MC_RANDOM and MC_DROP_RANDOM
+ to SEED. */
+void
+mc_options_set_seed (struct mc_options *options, unsigned int seed)
+{
+ options->seed = seed;
+}
+
+/* Returns the maximum depth to which OPTIONS's search will
+ descend. The initial states are at depth 1, states produced
+ as their mutations are at depth 2, and so on. */
+int
+mc_options_get_max_depth (const struct mc_options *options)
+{
+ return options->max_depth;
+}
+
+/* Sets the maximum depth to which OPTIONS's search will descend
+ to MAX_DEPTH. The initial states are at depth 1, states
+ produced as their mutations are at depth 2, and so on. */
+void
+mc_options_set_max_depth (struct mc_options *options, int max_depth)
+{
+ options->max_depth = max_depth;
+}
+
+/* Returns the base-2 log of the number of bits in OPTIONS's hash
+ table. The hash table is used for dropping states that are
+ probably duplicates: any state with a given hash value, as
+ will only be processed once. A return value of 0 indicates
+ that the model checker will not discard duplicate states based
+ on their hashes.
+
+ The hash table is a power of 2 bits long, by default 2**20
+ bits (128 kB). Depending on how many states you expect the
+ model checker to check, how much memory you're willing to let
+ the hash table take up, and how worried you are about missing
+ states due to hash collisions, you could make it larger or
+ smaller.
+
+ The "birthday paradox" points to a reasonable way to size your
+ hash table. If you expect the model checker to check about
+ 2**N states, then, assuming a perfect hash, you need a hash
+ table of 2**(N+1) bits to have a 50% chance of seeing a hash
+ collision, 2**(N+2) bits to have a 25% chance, and so on. */
+int
+mc_options_get_hash_bits (const struct mc_options *options)
+{
+ return options->hash_bits;
+}
+
+/* Sets the base-2 log of the number of bits in OPTIONS's hash
+ table to HASH_BITS. A HASH_BITS value of 0 requests that the
+ model checker not discard duplicate states based on their
+ hashes. (This causes the model checker to never terminate in
+ many cases.) */
+void
+mc_options_set_hash_bits (struct mc_options *options, int hash_bits)
+{
+ assert (hash_bits >= 0);
+ options->hash_bits = MIN (hash_bits, CHAR_BIT * sizeof (unsigned int) - 1);
+}
+
+/* Returns the path set in OPTIONS by mc_options_set_follow_path.
+ May be used only if the search strategy is MC_PATH. */
+const struct mc_path *
+mc_options_get_follow_path (const struct mc_options *options)
+{
+ assert (options->strategy == MC_PATH);
+ return &options->follow_path;
+}
+
+/* Sets, in OPTIONS, the search algorithm to MC_PATH and the path
+ to be the explicit path specified in FOLLOW_PATH. */
+void
+mc_options_set_follow_path (struct mc_options *options,
+ const struct mc_path *follow_path)
+{
+ assert (mc_path_get_length (follow_path) > 0);
+ options->strategy = MC_PATH;
+ mc_path_copy (&options->follow_path, follow_path);
+}
+
+/* Returns the maximum number of queued states in OPTIONS. The
+ default value is 10,000. The primary reason to limit the
+ number of queued states is to conserve memory, so if you can
+ afford the memory and your model needs more room in the queue,
+ you can raise the limit. Conversely, if your models are large
+ or memory is constrained, you can reduce the limit.
+
+ Following the execution of the model checker, you can find out
+ the maximum queue length during the run by calling
+ mc_results_get_max_queue_length. */
+int
+mc_options_get_queue_limit (const struct mc_options *options)
+{
+ return options->queue_limit;
+}
+
+/* Sets the maximum number of queued states in OPTIONS to
+ QUEUE_LIMIT. */
+void
+mc_options_set_queue_limit (struct mc_options *options, int queue_limit)
+{
+ assert (queue_limit > 0);
+ options->queue_limit = queue_limit;
+}
+
+/* Returns the queue limit strategy used by OPTIONS, that is,
+ when a new state must be inserted into a full state queue is
+ full, how the state to be dropped is chosen. The choices are:
+
+ - MC_DROP_NEWEST: Drop the newest state; that is, do not
+ insert the new state into the queue at all.
+
+ - MC_DROP_OLDEST: Drop the state that has been enqueued for
+ the longest.
+
+ - MC_DROP_RANDOM (the default): Drop a randomly selected state
+ from the queue. The standard C library's rand function
+ selects the state to drop; you can control the seed passed
+ to srand using mc_options_set_seed. */
+enum mc_queue_limit_strategy
+mc_options_get_queue_limit_strategy (const struct mc_options *options)
+{
+ return options->queue_limit_strategy;
+}
+
+/* Sets the queue limit strategy used by OPTIONS to STRATEGY.
+
+ This setting has no effect unless the model being checked
+ causes the state queue to overflow (see
+ mc_options_get_queue_limit). */
+void
+mc_options_set_queue_limit_strategy (struct mc_options *options,
+ enum mc_queue_limit_strategy strategy)
+{
+ assert (strategy == MC_DROP_NEWEST
+ || strategy == MC_DROP_OLDEST
+ || strategy == MC_DROP_RANDOM);
+ options->queue_limit_strategy = strategy;
+}
+
+/* Returns OPTIONS's maximum number of unique states that the
+ model checker will examine before terminating. The default is
+ INT_MAX. */
+int
+mc_options_get_max_unique_states (const struct mc_options *options)
+{
+ return options->max_unique_states;
+}
+
+/* Sets OPTIONS's maximum number of unique states that the model
+ checker will examine before terminating to
+ MAX_UNIQUE_STATE. */
+void
+mc_options_set_max_unique_states (struct mc_options *options,
+ int max_unique_states)
+{
+ options->max_unique_states = max_unique_states;
+}
+
+/* Returns the maximum number of errors that OPTIONS will allow
+ the model checker to encounter before terminating. The
+ default is 1. */
+int
+mc_options_get_max_errors (const struct mc_options *options)
+{
+ return options->max_errors;
+}
+
+/* Sets the maximum number of errors that OPTIONS will allow the
+ model checker to encounter before terminating to
+ MAX_ERRORS. */
+void
+mc_options_set_max_errors (struct mc_options *options, int max_errors)
+{
+ options->max_errors = max_errors;
+}
+
+/* Returns the maximum amount of time, in seconds, that OPTIONS will allow the
+ model checker to consume before terminating. The
+ default of 0.0 means that time consumption is unlimited. */
+double
+mc_options_get_time_limit (const struct mc_options *options)
+{
+ return options->time_limit;
+}
+
+/* Sets the maximum amount of time, in seconds, that OPTIONS will
+ allow the model checker to consume before terminating to
+ TIME_LIMIT. A value of 0.0 means that time consumption is
+ unlimited; otherwise, the return value will be positive. */
+void
+mc_options_set_time_limit (struct mc_options *options, double time_limit)
+{
+ assert (time_limit >= 0.0);
+ options->time_limit = time_limit;
+}
+
+/* Returns the level of verbosity for output messages specified
+ by OPTIONS. The default verbosity level is 1.
+
+ A verbosity level of 0 inhibits all messages except for
+ errors; a verbosity level of 1 also allows warnings; a
+ verbosity level of 2 also causes a description of each state
+ added to be output; a verbosity level of 3 also causes a
+ description of each duplicate state to be output. Verbosity
+ levels less than 0 or greater than 3 are allowed but currently
+ have no additional effect. */
+int
+mc_options_get_verbosity (const struct mc_options *options)
+{
+ return options->verbosity;
+}
+
+/* Sets the level of verbosity for output messages specified
+ by OPTIONS to VERBOSITY. */
+void
+mc_options_set_verbosity (struct mc_options *options, int verbosity)
+{
+ options->verbosity = verbosity;
+}
+
+/* Returns the level of verbosity for failures specified by
+ OPTIONS. The default failure verbosity level is 2.
+
+ The failure verbosity level has an effect only when an error
+ is reported, and only when the failure verbosity level is
+ higher than the regular verbosity level. When this is the
+ case, the model checker replays the error path at the higher
+ verbosity level specified. This has the effect of outputting
+ an explicit, human-readable description of the sequence of
+ operations that caused the error. */
+int
+mc_options_get_failure_verbosity (const struct mc_options *options)
+{
+ return options->failure_verbosity;
+}
+
+/* Sets the level of verbosity for failures specified by OPTIONS
+ to FAILURE_VERBOSITY. */
+void
+mc_options_set_failure_verbosity (struct mc_options *options,
+ int failure_verbosity)
+{
+ options->failure_verbosity = failure_verbosity;
+}
+
+/* Returns the output file used for messages printed by the model
+ checker specified by OPTIONS. The default is stdout. */
+FILE *
+mc_options_get_output_file (const struct mc_options *options)
+{
+ return options->output_file;
+}
+
+/* Sets the output file used for messages printed by the model
+ checker specified by OPTIONS to OUTPUT_FILE.
+
+ The model checker does not automatically close the specified
+ output file. If this is desired, the model checker's client
+ must do so. */
+void
+mc_options_set_output_file (struct mc_options *options,
+ FILE *output_file)
+{
+ options->output_file = output_file;
+}
+
+/* Returns the number of microseconds between calls to the
+ progress function specified by OPTIONS. The default is
+ 250,000 (1/4 second). A value of 0 disables progress
+ reporting. */
+int
+mc_options_get_progress_usec (const struct mc_options *options)
+{
+ return options->progress_usec;
+}
+
+/* Sets the number of microseconds between calls to the progress
+ function specified by OPTIONS to PROGRESS_USEC. A value of 0
+ disables progress reporting. */
+void
+mc_options_set_progress_usec (struct mc_options *options, int progress_usec)
+{
+ assert (progress_usec >= 0);
+ options->progress_usec = progress_usec;
+}
+
+/* Returns the function called to report progress specified by
+ OPTIONS. The function used by default prints '.' to
+ stderr. */
+mc_progress_func *
+mc_options_get_progress_func (const struct mc_options *options)
+{
+ return options->progress_func;
+}
+
+/* Sets the function called to report progress specified by
+ OPTIONS to PROGRESS_FUNC. A non-null function must be
+ specified; to disable progress reporting, set the progress
+ reporting interval to 0.
+
+ PROGRESS_FUNC will be called zero or more times while the
+ model checker's run is ongoing. For these calls to the
+ progress function, mc_results_get_stop_reason will return
+ MC_CONTINUING. It will also be called exactly once soon
+ before mc_run returns, in which case
+ mc_results_get_stop_reason will return a different value. */
+void
+mc_options_set_progress_func (struct mc_options *options,
+ mc_progress_func *progress_func)
+{
+ assert (options->progress_func != NULL);
+ options->progress_func = progress_func;
+}
+
+/* Returns the auxiliary data set in OPTIONS by the client. The
+ default is a null pointer.
+
+ This auxiliary data value can be retrieved by the
+ client-specified functions in struct mc_class during a model
+ checking run using mc_get_aux. */
+void *
+mc_options_get_aux (const struct mc_options *options)
+{
+ return options->aux;
+}
+
+/* Sets the auxiliary data in OPTIONS to AUX. */
+void
+mc_options_set_aux (struct mc_options *options, void *aux)
+{
+ options->aux = aux;
+}
+\f
+/* Results of a model checking run. */
+struct mc_results
+ {
+ /* Overall results. */
+ enum mc_stop_reason stop_reason; /* Why the run ended. */
+ int unique_state_count; /* Number of unique states checked. */
+ int error_count; /* Number of errors found. */
+
+ /* Depth statistics. */
+ int max_depth_reached; /* Max depth state examined. */
+ struct moments1 *depth_moments; /* Enables reporting mean depth. */
+
+ /* If error_count > 0, path to the last error reported. */
+ struct mc_path error_path;
+
+ /* States dropped... */
+ int duplicate_dropped_states; /* ...as duplicates. */
+ int off_path_dropped_states; /* ...as off-path (MC_PATH only). */
+ int depth_dropped_states; /* ...due to excessive depth. */
+ int queue_dropped_states; /* ...due to queue overflow. */
+
+ /* Queue statistics. */
+ int queued_unprocessed_states; /* Enqueued but never dequeued. */
+ int max_queue_length; /* Maximum queue length observed. */
+
+ /* Timing. */
+ struct timeval start; /* Start of model checking run. */
+ struct timeval end; /* End of model checking run. */
+ };
+
+/* Creates, initializes, and returns a new set of results. */
+static struct mc_results *
+mc_results_create (void)
+{
+ struct mc_results *results = xcalloc (1, sizeof (struct mc_results));
+ results->stop_reason = MC_CONTINUING;
+ results->depth_moments = moments1_create (MOMENT_MEAN);
+ gettimeofday (&results->start, NULL);
+ return results;
+}
+
+/* Destroys RESULTS. */
+void
+mc_results_destroy (struct mc_results *results)
+{
+ if (results != NULL)
+ {
+ moments1_destroy (results->depth_moments);
+ mc_path_destroy (&results->error_path);
+ free (results);
+ }
+}
+
+/* Returns RESULTS's reason that the model checking run
+ terminated. The possible reasons are:
+
+ - MC_CONTINUING: The run is not actually yet complete. This
+ can only be returned before mc_run has returned, e.g. when
+ the progress function set by mc_options_set_progress_func
+ examines the run's results.
+
+ - MC_SUCCESS: The run completed because the queue emptied.
+ The entire state space might not have been explored due to a
+ requested limit on maximum depth, hash collisions, etc.
+
+ - MC_MAX_UNIQUE_STATES: The run completed because as many
+ unique states have been checked as were requested (using
+ mc_options_set_max_unique_states).
+
+ - MC_MAX_ERROR_COUNT: The run completed because the maximum
+ requested number of errors (by default, 1 error) was
+ reached.
+
+ - MC_END_OF_PATH: The run completed because the path specified
+ with mc_options_set_follow_path was fully traversed.
+
+ - MC_TIMEOUT: The run completed because the time limit set
+ with mc_options_set_time_limit was exceeded.
+
+ - MC_INTERRUPTED: The run completed because SIGINT was caught
+ (typically, due to the user typing Ctrl+C). */
+enum mc_stop_reason
+mc_results_get_stop_reason (const struct mc_results *results)
+{
+ return results->stop_reason;
+}
+
+/* Returns the number of unique states checked specified by
+ RESULTS. */
+int
+mc_results_get_unique_state_count (const struct mc_results *results)
+{
+ return results->unique_state_count;
+}
+
+/* Returns the number of errors found specified by RESULTS. */
+int
+mc_results_get_error_count (const struct mc_results *results)
+{
+ return results->error_count;
+}
+
+/* Returns the maximum depth reached during the model checker run
+ represented by RESULTS. The initial states are at depth 1,
+ their child states at depth 2, and so on. */
+int
+mc_results_get_max_depth_reached (const struct mc_results *results)
+{
+ return results->max_depth_reached;
+}
+
+/* Returns the mean depth reached during the model checker run
+ represented by RESULTS. */
+double
+mc_results_get_mean_depth_reached (const struct mc_results *results)
+{
+ double mean;
+ moments1_calculate (results->depth_moments, NULL, &mean, NULL, NULL, NULL);
+ return mean != SYSMIS ? mean : 0.0;
+}
+
+/* Returns the path traversed to obtain the last error
+ encountered during the model checker run represented by
+ RESULTS. Returns a null pointer if the run did not report any
+ errors. */
+const struct mc_path *
+mc_results_get_error_path (const struct mc_results *results)
+{
+ return results->error_count > 0 ? &results->error_path : NULL;
+}
+
+/* Returns the number of states dropped as duplicates (based on
+ hash value) during the model checker run represented by
+ RESULTS. */
+int
+mc_results_get_duplicate_dropped_states (const struct mc_results *results)
+{
+ return results->duplicate_dropped_states;
+}
+
+/* Returns the number of states dropped because they were off the
+ path specified by mc_options_set_follow_path during the model
+ checker run represented by RESULTS. A nonzero value here
+ indicates a missing call to mc_include_state in the
+ client-supplied mutation function. */
+int
+mc_results_get_off_path_dropped_states (const struct mc_results *results)
+{
+ return results->off_path_dropped_states;
+}
+
+/* Returns the number of states dropped because their depth
+ exceeded the maximum specified with mc_options_set_max_depth
+ during the model checker run represented by RESULTS. */
+int
+mc_results_get_depth_dropped_states (const struct mc_results *results)
+{
+ return results->depth_dropped_states;
+}
+
+/* Returns the number of states dropped from the queue due to
+ queue overflow during the model checker run represented by
+ RESULTS. */
+int
+mc_results_get_queue_dropped_states (const struct mc_results *results)
+{
+ return results->queue_dropped_states;
+}
+
+/* Returns the number of states that were checked and enqueued
+ but never dequeued and processed during the model checker run
+ represented by RESULTS. This is zero if the stop reason is
+ MC_CONTINUING or MC_SUCCESS; otherwise, it is the number of
+ states in the queue at the time that the checking run
+ stopped. */
+int
+mc_results_get_queued_unprocessed_states (const struct mc_results *results)
+{
+ return results->queued_unprocessed_states;
+}
+
+/* Returns the maximum length of the queue during the model
+ checker run represented by RESULTS. If this is equal to the
+ maximum queue length, then the queue (probably) overflowed
+ during the run; otherwise, it did not overflow. */
+int
+mc_results_get_max_queue_length (const struct mc_results *results)
+{
+ return results->max_queue_length;
+}
+
+/* Returns the time at which the model checker run represented by
+ RESULTS started. */
+struct timeval
+mc_results_get_start (const struct mc_results *results)
+{
+ return results->start;
+}
+
+/* Returns the time at which the model checker run represented by
+ RESULTS ended. (This function may not be called while the run
+ is still ongoing.) */
+struct timeval
+mc_results_get_end (const struct mc_results *results)
+{
+ assert (results->stop_reason != MC_CONTINUING);
+ return results->end;
+}
+
+/* Returns the number of seconds obtained by subtracting time Y
+ from time X. */
+static double
+timeval_subtract (struct timeval x, struct timeval y)
+{
+ /* From libc.info. */
+ double difference;
+
+ /* Perform the carry for the later subtraction by updating Y. */
+ if (x.tv_usec < y.tv_usec) {
+ int nsec = (y.tv_usec - x.tv_usec) / 1000000 + 1;
+ y.tv_usec -= 1000000 * nsec;
+ y.tv_sec += nsec;
+ }
+ if (x.tv_usec - y.tv_usec > 1000000) {
+ int nsec = (x.tv_usec - y.tv_usec) / 1000000;
+ y.tv_usec += 1000000 * nsec;
+ y.tv_sec -= nsec;
+ }
+
+ /* Compute the time remaining to wait.
+ `tv_usec' is certainly positive. */
+ difference = (x.tv_sec - y.tv_sec) + (x.tv_usec - y.tv_usec) / 1000000.0;
+ if (x.tv_sec < y.tv_sec)
+ difference = -difference;
+ return difference;
+}
+
+
+/* Returns the duration, in seconds, of the model checker run
+ represented by RESULTS. (This function may not be called
+ while the run is still ongoing.) */
+double
+mc_results_get_duration (const struct mc_results *results)
+{
+ assert (results->stop_reason != MC_CONTINUING);
+ return timeval_subtract (results->end, results->start);
+}
+\f
+/* An active model checking run. */
+struct mc
+ {
+ /* Related data structures. */
+ const struct mc_class *class;
+ struct mc_options *options;
+ struct mc_results *results;
+
+ /* Array of 2**(options->hash_bits) bits representing states
+ already visited. */
+ unsigned char *hash;
+
+ /* State queue. */
+ struct mc_state **queue; /* Array of pointers to states. */
+ struct deque queue_deque; /* Deque. */
+
+ /* State currently being built by "init" or "mutate". */
+ struct mc_path path; /* Path to current state. */
+ struct string path_string; /* Buffer for path_string function. */
+ bool state_named; /* mc_name_operation called? */
+ bool state_error; /* mc_error called? */
+
+ /* Statistics for calling the progress function. */
+ unsigned int progress; /* Current progress value. */
+ unsigned int next_progress; /* Next value to call progress func. */
+ unsigned int prev_progress; /* Last value progress func called. */
+ struct timeval prev_progress_time; /* Last time progress func called. */
+
+ /* Information for handling and restoring SIGINT. */
+ bool interrupted; /* SIGINT received? */
+ bool *saved_interrupted_ptr; /* Saved value of interrupted_ptr. */
+ sighandler_t saved_sigint; /* Saved SIGINT handler. */
+ };
+
+/* A state in the queue. */
+struct mc_state
+ {
+ struct mc_path path; /* Path to this state. */
+ void *data; /* Client-supplied data. */
+ };
+
+/* Points to the current struct mc's "interrupted" member. */
+static bool *interrupted_ptr = NULL;
+
+static const char *path_string (struct mc *);
+static void free_state (const struct mc *, struct mc_state *);
+static void stop (struct mc *, enum mc_stop_reason);
+static struct mc_state *make_state (const struct mc *, void *);
+static size_t random_queue_index (struct mc *);
+static void enqueue_state (struct mc *, struct mc_state *);
+static void do_error_state (struct mc *);
+static void next_operation (struct mc *);
+static bool is_off_path (const struct mc *);
+static void sigint_handler (int signum);
+static void init_mc (struct mc *,
+ const struct mc_class *, struct mc_options *);
+static void finish_mc (struct mc *);
+
+/* Runs the model checker on the client-specified CLASS with the
+ client-specified OPTIONS. OPTIONS may be a null pointer if
+ the defaults are acceptable. Destroys OPTIONS; use
+ mc_options_clone if a copy is needed.
+
+ Returns the results of the model checking run, which must be
+ destroyed by the client with mc_results_destroy.
+
+ To pass auxiliary data to the functions in CLASS, use
+ mc_options_set_aux on OPTIONS, which may be retrieved from the
+ CLASS functions using mc_get_aux. */
+struct mc_results *
+mc_run (const struct mc_class *class, struct mc_options *options)
+{
+ struct mc mc;
+
+ init_mc (&mc, class, options);
+ while (!deque_is_empty (&mc.queue_deque)
+ && mc.results->stop_reason == MC_CONTINUING)
+ {
+ struct mc_state *state = mc.queue[deque_pop_front (&mc.queue_deque)];
+ mc_path_copy (&mc.path, &state->path);
+ mc_path_push (&mc.path, 0);
+ class->mutate (&mc, state->data);
+ free_state (&mc, state);
+ if (mc.interrupted)
+ stop (&mc, MC_INTERRUPTED);
+ }
+ finish_mc (&mc);
+
+ return mc.results;
+}
+
+/* Tests whether the current operation is one that should be
+ performed, checked, and enqueued. If so, returns true.
+ Otherwise, returns false and, unless checking is stopped,
+ advances to the next state. The caller should then advance
+ to the next operation.
+
+ This function should be called from the client-provided
+ "mutate" function, according to the pattern explained in the
+ big comment at the top of model-checker.h. */
+bool
+mc_include_state (struct mc *mc)
+{
+ if (mc->results->stop_reason != MC_CONTINUING)
+ return false;
+ else if (is_off_path (mc))
+ {
+ next_operation (mc);
+ return false;
+ }
+ else
+ return true;
+}
+
+/* Tests whether HASH represents a state that has (probably)
+ already been enqueued. If not, returns false and marks HASH
+ so that it will be treated as a duplicate in the future. If
+ so, returns true and advances to the next state. The
+ caller should then advance to the next operation.
+
+ This function should be called from the client-provided
+ "mutate" function, according to the pattern explained in the
+ big comment at the top of model-checker.h. */
+bool
+mc_discard_dup_state (struct mc *mc, unsigned int hash)
+{
+ if (mc->options->hash_bits > 0)
+ {
+ hash &= (1u << mc->options->hash_bits) - 1;
+ if (TEST_BIT (mc->hash, hash))
+ {
+ if (mc->options->verbosity > 2)
+ fprintf (mc->options->output_file,
+ " [%s] discard duplicate state\n", path_string (mc));
+ mc->results->duplicate_dropped_states++;
+ next_operation (mc);
+ return true;
+ }
+ SET_BIT (mc->hash, hash);
+ }
+ return false;
+}
+
+/* Names the current state NAME, which may contain
+ printf-style format specifications. NAME should be a
+ human-readable name for the current operation.
+
+ This function should be called from the client-provided
+ "mutate" function, according to the pattern explained in the
+ big comment at the top of model-checker.h. */
+void
+mc_name_operation (struct mc *mc, const char *name, ...)
+{
+ va_list args;
+
+ va_start (args, name);
+ mc_vname_operation (mc, name, args);
+ va_end (args);
+}
+
+/* Names the current state NAME, which may contain
+ printf-style format specifications, for which the
+ corresponding arguments must be given in ARGS. NAME should be
+ a human-readable name for the current operation.
+
+ This function should be called from the client-provided
+ "mutate" function, according to the pattern explained in the
+ big comment at the top of model-checker.h. */
+void
+mc_vname_operation (struct mc *mc, const char *name, va_list args)
+{
+ if (mc->state_named && mc->options->verbosity > 0)
+ fprintf (mc->options->output_file, " [%s] warning: duplicate call "
+ "to mc_name_operation (missing call to mc_add_state?)\n",
+ path_string (mc));
+ mc->state_named = true;
+
+ if (mc->options->verbosity > 1)
+ {
+ fprintf (mc->options->output_file, " [%s] ", path_string (mc));
+ vfprintf (mc->options->output_file, name, args);
+ putc ('\n', mc->options->output_file);
+ }
+}
+
+/* Reports the given error MESSAGE for the current operation.
+ The resulting state should still be passed to mc_add_state
+ when all relevant error messages have been issued. The state
+ will not, however, be enqueued for later mutation of its own.
+
+ By default, model checking stops after the first error
+ encountered.
+
+ This function should be called from the client-provided
+ "mutate" function, according to the pattern explained in the
+ big comment at the top of model-checker.h. */
+void
+mc_error (struct mc *mc, const char *message, ...)
+{
+ va_list args;
+
+ if (mc->results->stop_reason != MC_CONTINUING)
+ return;
+
+ if (mc->options->verbosity > 1)
+ fputs (" ", mc->options->output_file);
+ fprintf (mc->options->output_file, "[%s] error: ",
+ path_string (mc));
+ va_start (args, message);
+ vfprintf (mc->options->output_file, message, args);
+ va_end (args);
+ putc ('\n', mc->options->output_file);
+
+ mc->state_error = true;
+}
+
+/* Enqueues DATA as the state corresponding to the current
+ operation. The operation should have been named with a call
+ to mc_name_operation, and it should have been checked by the
+ caller (who should have reported any errors with mc_error).
+
+ This function should be called from the client-provided
+ "mutate" function, according to the pattern explained in the
+ big comment at the top of model-checker.h. */
+void
+mc_add_state (struct mc *mc, void *data)
+{
+ if (!mc->state_named && mc->options->verbosity > 0)
+ fprintf (mc->options->output_file, " [%s] warning: unnamed state\n",
+ path_string (mc));
+
+ if (mc->results->stop_reason != MC_CONTINUING)
+ {
+ /* Nothing to do. */
+ }
+ else if (mc->state_error)
+ do_error_state (mc);
+ else if (is_off_path (mc))
+ mc->results->off_path_dropped_states++;
+ else if (mc->path.length + 1 > mc->options->max_depth)
+ mc->results->depth_dropped_states++;
+ else
+ {
+ /* This is the common case. */
+ mc->results->unique_state_count++;
+ if (mc->results->unique_state_count >= mc->options->max_unique_states)
+ stop (mc, MC_MAX_UNIQUE_STATES);
+ enqueue_state (mc, make_state (mc, data));
+ next_operation (mc);
+ return;
+ }
+
+ mc->class->destroy (mc, data);
+ next_operation (mc);
+}
+
+/* Returns the options that were passed to mc_run for model
+ checker MC. */
+const struct mc_options *
+mc_get_options (const struct mc *mc)
+{
+ return mc->options;
+}
+
+/* Returns the current state of the results for model checker
+ MC. This function is appropriate for use from the progress
+ function set by mc_options_set_progress_func.
+
+ Not all of the results are meaningful before model checking
+ completes. */
+const struct mc_results *
+mc_get_results (const struct mc *mc)
+{
+ return mc->results;
+}
+
+/* Returns the auxiliary data set on the options passed to mc_run
+ with mc_options_set_aux. */
+void *
+mc_get_aux (const struct mc *mc)
+{
+ return mc_options_get_aux (mc_get_options (mc));
+}
+\f
+/* Expresses MC->path as a string and returns the string. */
+static const char *
+path_string (struct mc *mc)
+{
+ ds_clear (&mc->path_string);
+ mc_path_to_string (&mc->path, &mc->path_string);
+ return ds_cstr (&mc->path_string);
+}
+
+/* Frees STATE, including client data. */
+static void
+free_state (const struct mc *mc, struct mc_state *state)
+{
+ mc->class->destroy (mc, state->data);
+ mc_path_destroy (&state->path);
+ free (state);
+}
+
+/* Sets STOP_REASON as the reason that MC's processing stopped,
+ unless MC is already stopped. */
+static void
+stop (struct mc *mc, enum mc_stop_reason stop_reason)
+{
+ if (mc->results->stop_reason == MC_CONTINUING)
+ mc->results->stop_reason = stop_reason;
+}
+
+/* Creates and returns a new state whose path is copied from
+ MC->path and whose data is specified by DATA. */
+static struct mc_state *
+make_state (const struct mc *mc, void *data)
+{
+ struct mc_state *new = xmalloc (sizeof *new);
+ mc_path_init (&new->path);
+ mc_path_copy (&new->path, &mc->path);
+ new->data = data;
+ return new;
+}
+
+/* Returns the index in MC->queue of a random element in the
+ queue. */
+static size_t
+random_queue_index (struct mc *mc)
+{
+ assert (!deque_is_empty (&mc->queue_deque));
+ return deque_front (&mc->queue_deque,
+ rand () % deque_count (&mc->queue_deque));
+}
+
+/* Adds NEW to MC's state queue, dropping a state if necessary
+ due to overflow. */
+static void
+enqueue_state (struct mc *mc, struct mc_state *new)
+{
+ size_t idx;
+
+ if (new->path.length > mc->results->max_depth_reached)
+ mc->results->max_depth_reached = new->path.length;
+ moments1_add (mc->results->depth_moments, new->path.length, 1.0);
+
+ if (deque_count (&mc->queue_deque) < mc->options->queue_limit)
+ {
+ /* Add new state to queue. */
+ if (deque_is_full (&mc->queue_deque))
+ mc->queue = deque_expand (&mc->queue_deque,
+ mc->queue, sizeof *mc->queue);
+ switch (mc->options->strategy)
+ {
+ case MC_BROAD:
+ idx = deque_push_back (&mc->queue_deque);
+ break;
+ case MC_DEEP:
+ idx = deque_push_front (&mc->queue_deque);
+ break;
+ case MC_RANDOM:
+ if (!deque_is_empty (&mc->queue_deque))
+ {
+ idx = random_queue_index (mc);
+ mc->queue[deque_push_front (&mc->queue_deque)]
+ = mc->queue[idx];
+ }
+ else
+ idx = deque_push_front (&mc->queue_deque);
+ break;
+ case MC_PATH:
+ assert (deque_is_empty (&mc->queue_deque));
+ assert (!is_off_path (mc));
+ idx = deque_push_back (&mc->queue_deque);
+ if (mc->path.length
+ >= mc_path_get_length (&mc->options->follow_path))
+ stop (mc, MC_END_OF_PATH);
+ break;
+ default:
+ NOT_REACHED ();
+ }
+ if (deque_count (&mc->queue_deque) > mc->results->max_queue_length)
+ mc->results->max_queue_length = deque_count (&mc->queue_deque);
+ }
+ else
+ {
+ /* Queue has reached limit, so replace an existing
+ state. */
+ assert (mc->options->strategy != MC_PATH);
+ assert (!deque_is_empty (&mc->queue_deque));
+ mc->results->queue_dropped_states++;
+ switch (mc->options->queue_limit_strategy)
+ {
+ case MC_DROP_NEWEST:
+ free_state (mc, new);
+ return;
+ case MC_DROP_OLDEST:
+ switch (mc->options->strategy)
+ {
+ case MC_BROAD:
+ idx = deque_front (&mc->queue_deque, 0);
+ break;
+ case MC_DEEP:
+ idx = deque_back (&mc->queue_deque, 0);
+ break;
+ case MC_RANDOM:
+ case MC_PATH:
+ default:
+ NOT_REACHED ();
+ }
+ break;
+ case MC_DROP_RANDOM:
+ idx = random_queue_index (mc);
+ break;
+ default:
+ NOT_REACHED ();
+ }
+ free_state (mc, mc->queue[idx]);
+ }
+ mc->queue[idx] = new;
+}
+
+/* Process an error state being added to MC. */
+static void
+do_error_state (struct mc *mc)
+{
+ mc->results->error_count++;
+ if (mc->results->error_count >= mc->options->max_errors)
+ stop (mc, MC_MAX_ERROR_COUNT);
+
+ mc_path_copy (&mc->results->error_path, &mc->path);
+
+ if (mc->options->failure_verbosity > mc->options->verbosity)
+ {
+ struct mc_options *path_options;
+
+ fprintf (mc->options->output_file, "[%s] retracing error path:\n",
+ path_string (mc));
+ path_options = mc_options_clone (mc->options);
+ mc_options_set_verbosity (path_options, mc->options->failure_verbosity);
+ mc_options_set_failure_verbosity (path_options, 0);
+ mc_options_set_follow_path (path_options, &mc->path);
+
+ mc_results_destroy (mc_run (mc->class, path_options));
+
+ putc ('\n', mc->options->output_file);
+ }
+}
+
+/* Advances MC to start processing the operation following the
+ current one. */
+static void
+next_operation (struct mc *mc)
+{
+ mc_path_push (&mc->path, mc_path_pop (&mc->path) + 1);
+ mc->state_error = false;
+ mc->state_named = false;
+
+ if (++mc->progress >= mc->next_progress)
+ {
+ struct timeval now;
+ double elapsed, delta;
+
+ if (mc->results->stop_reason == MC_CONTINUING
+ && !mc->options->progress_func (mc))
+ stop (mc, MC_INTERRUPTED);
+
+ gettimeofday (&now, NULL);
+
+ if (mc->options->time_limit > 0.0
+ && (timeval_subtract (now, mc->results->start)
+ > mc->options->time_limit))
+ stop (mc, MC_TIMEOUT);
+
+ elapsed = timeval_subtract (now, mc->prev_progress_time);
+ if (elapsed > 0.0)
+ {
+ /* Re-estimate the amount of progress to take
+ progress_usec microseconds. */
+ unsigned int progress = mc->progress - mc->prev_progress;
+ double progress_sec = mc->options->progress_usec / 1000000.0;
+ delta = progress / elapsed * progress_sec;
+ }
+ else
+ {
+ /* No measurable time at all elapsed during that amount
+ of progress. Try doubling the amount of progress
+ required. */
+ delta = (mc->progress - mc->prev_progress) * 2;
+ }
+
+ if (delta > 0.0 && delta + mc->progress + 1.0 < UINT_MAX)
+ mc->next_progress = mc->progress + delta + 1.0;
+ else
+ mc->next_progress = mc->progress + (mc->progress - mc->prev_progress);
+
+ mc->prev_progress = mc->progress;
+ mc->prev_progress_time = now;
+ }
+}
+
+/* Returns true if we're tracing an explicit path but the current
+ operation produces a state off that path, false otherwise. */
+static bool
+is_off_path (const struct mc *mc)
+{
+ return (mc->options->strategy == MC_PATH
+ && (mc_path_back (&mc->path)
+ != mc_path_get_operation (&mc->options->follow_path,
+ mc->path.length - 1)));
+}
+
+/* Handler for SIGINT. */
+static void
+sigint_handler (int signum UNUSED)
+{
+ /* Just mark the model checker as interrupted. */
+ *interrupted_ptr = true;
+}
+
+/* Initializes MC as a model checker with the given CLASS and
+ OPTIONS. OPTIONS may be null to use the default options. */
+static void
+init_mc (struct mc *mc, const struct mc_class *class,
+ struct mc_options *options)
+{
+ /* Validate and adjust OPTIONS. */
+ if (options == NULL)
+ options = mc_options_create ();
+ assert (options->queue_limit_strategy != MC_DROP_OLDEST
+ || options->strategy != MC_RANDOM);
+ if (options->strategy == MC_PATH)
+ {
+ options->max_depth = INT_MAX;
+ options->hash_bits = 0;
+ }
+ if (options->progress_usec == 0)
+ {
+ options->progress_func = null_progress;
+ if (options->time_limit > 0.0)
+ options->progress_usec = 250000;
+ }
+
+ /* Initialize MC. */
+ mc->class = class;
+ mc->options = options;
+ mc->results = mc_results_create ();
+
+ mc->hash = (mc->options->hash_bits > 0
+ ? xcalloc (1, DIV_RND_UP (1 << mc->options->hash_bits, CHAR_BIT))
+ : NULL);
+
+ mc->queue = NULL;
+ deque_init_null (&mc->queue_deque);
+
+ mc_path_init (&mc->path);
+ mc_path_push (&mc->path, 0);
+ ds_init_empty (&mc->path_string);
+ mc->state_named = false;
+ mc->state_error = false;
+
+ mc->progress = 0;
+ mc->next_progress = mc->options->progress_usec != 0 ? 100 : UINT_MAX;
+ mc->prev_progress = 0;
+ mc->prev_progress_time = mc->results->start;
+
+ if (mc->options->strategy == MC_RANDOM
+ || options->queue_limit_strategy == MC_DROP_RANDOM)
+ srand (mc->options->seed);
+
+ mc->interrupted = false;
+ mc->saved_interrupted_ptr = interrupted_ptr;
+ interrupted_ptr = &mc->interrupted;
+ mc->saved_sigint = signal (SIGINT, sigint_handler);
+
+ class->init (mc);
+}
+
+/* Complete the model checker run for MC. */
+static void
+finish_mc (struct mc *mc)
+{
+ /* Restore signal handlers. */
+ signal (SIGINT, mc->saved_sigint);
+ interrupted_ptr = mc->saved_interrupted_ptr;
+
+ /* Mark the run complete. */
+ stop (mc, MC_SUCCESS);
+ gettimeofday (&mc->results->end, NULL);
+
+ /* Empty the queue. */
+ mc->results->queued_unprocessed_states = deque_count (&mc->queue_deque);
+ while (!deque_is_empty (&mc->queue_deque))
+ {
+ struct mc_state *state = mc->queue[deque_pop_front (&mc->queue_deque)];
+ free_state (mc, state);
+ }
+
+ /* Notify the progress function of completion. */
+ mc->options->progress_func (mc);
+
+ /* Free memory. */
+ mc_path_destroy (&mc->path);
+ ds_destroy (&mc->path_string);
+ free (mc->options);
+ free (mc->queue);
+ free (mc->hash);
+}
--- /dev/null
+/* PSPP - computes sample statistics.
+ Copyright (C) 2007 Free Software Foundation, Inc.
+
+ This program is free software; you can redistribute it and/or
+ modify it under the terms of the GNU General Public License as
+ published by the Free Software Foundation; either version 2 of the
+ License, or (at your option) any later version.
+
+ This program is distributed in the hope that it will be useful, but
+ WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with this program; if not, write to the Free Software
+ Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
+ 02110-1301, USA. */
+
+/* Implementation-level model checker.
+
+ A model checker is a tool for software testing and
+ verification that works by exploring all the possible states
+ in a system and verifying their internal consistency. A
+ conventional model checker requires that the code in a system
+ be translated into a specification language. The model
+ checker then verifies the specification, rather than the code.
+
+ This is instead an implementation-level model checker, which
+ does not require a separate specification. Instead, the model
+ checker requires writing a second implementation of the system
+ being checked. The second implementation can usually be made
+ almost trivial in comparison to the one being checked, because
+ it's usually acceptable for its performance to be
+ comparatively poor, e.g. O(N^2) instead of O(lg N), and thus
+ to use much simpler algorithms.
+
+ For introduction to the implementation-level model checking
+ approach used here, please refer to the following papers:
+
+ Musuvathi, Park, Chou, Engler, Dill, "CMC: A Pragmatic
+ Approach to Model Checking Real Code", Proceedings of the
+ Fifth Symposium on Operating Systems Design and
+ Implementation (OSDI), Dec 2002.
+ http://sprout.stanford.edu/PAPERS/CMC-OSDI-2002/CMC-OSDI-2002.pdf
+
+ Yang, Twohey, Engler, Musuvathi, "Using Model Checking to
+ Find Serious File System Errors", Proceedings of the Sixth
+ Symposium on Operating System Design and Implementation
+ (OSDI), Dec 2004.
+ http://www.stanford.edu/~engler/osdi04-fisc.pdf
+
+ Yang, Twohey, Pfaff, Sar, Engler, "EXPLODE: A Lightweight,
+ General Approach to Finding Serious Errors in Storage
+ Systems", First Workshop on the Evaluation of Software
+ Defect Detection Tools (BUGS), June 2005.
+ http://benpfaff.org/papers/explode.pdf
+
+ Use of a model checker is appropriate when the system being
+ checked is difficult to test using handwritten tests. This
+ can be the case, for example, when the system has a
+ complicated internal state that is difficult to reason about
+ over a long series of operations.
+
+ The implementation model checker works by putting a set of one
+ of more initial states in a queue (and checking them for
+ consistency). Then the model checker removes a state from the
+ queue and applies all possible operations of interest to it
+ ("mutates" it), obtaining a set of zero or more child states
+ (and checking each of them for consistency). Each of these
+ states is itself added to the queue. The model checker
+ continues dequeuing states and mutating and checking them
+ until the queue is empty.
+
+ In pseudo-code, the process looks like this:
+
+ Q = { initial states }
+ while Q is not empty:
+ S = dequeue(Q)
+ for each operation applicable to S do:
+ T = operation(S)
+ check(T)
+ enqueue(Q, T)
+
+ In many cases this process will never terminate, because every
+ state has one or more child states. For some systems this is
+ unavoidable, but in others we can make the process finite by
+ pursuing a few stratagems:
+
+ 1. Limit the maximum size of the system; for example, limit
+ the number of rows and columns in the implementation of a
+ table being checked. The client of the model checker is
+ responsible for implementing such limits.
+
+ 2. Avoid checking a single state more than one time. This
+ model checker provides assistance for this function by
+ allowing the client to provide a hash of the system state.
+ States with identical hashes will only be checked once
+ during a single run.
+
+ When a system cannot be made finite, or when a finite system
+ is too large to check in a practical amount of time, the model
+ checker provides multiple ways to limit the checking run:
+ based on maximum depth, maximum unique states checked, maximum
+ errors found (by default, 1), or maximum time used for
+ checking.
+
+ The client of the model checker must provide three functions
+ via function pointers embedded into a "struct mc_class":
+
+ 1. void init (struct mc *mc);
+
+ This function is called once at the beginning of a
+ checking run. It checks one or more initial states and
+ adds them to the model checker's queue. (If it does not
+ add any states to the queue, then there is nothing to
+ check.)
+
+ Here's an outline for writing the init function:
+
+ void
+ init_foo (struct mc *mc)
+ {
+ struct foo *foo;
+
+ mc_name_operation (mc, "initial state");
+ foo = generate_initial_foo ();
+ if (!state_is_consistent (foo))
+ mc_error (mc, "inconsistent state");
+ mc_add_state (mc, foo);
+ }
+
+ 2. void mutate (struct mc *mc, const void *data);
+
+ This function is called when a dequeued state is ready to
+ be mutated. For each operation that can be applied to
+ the client-specified DATA, it applies that operation to a
+ clone of the DATA, checks that the clone is consistent,
+ and adds the clone to the model checker's queue.
+
+ Here's an outline for writing the mutate function:
+
+ void
+ mutate_foo (struct mc *mc, void *state_)
+ {
+ struct foo *state = state_;
+
+ for (...each operation...)
+ if (mc_include_state (mc))
+ {
+ struct foo *clone;
+
+ mc_name_operation (mc, "do operation %s", ...);
+ clone = clone_foo (state);
+ do_operation (clone);
+ if (!mc_discard_dup_state (mc, hash_foo (clone)))
+ {
+ if (!state_is_consistent (clone))
+ mc_error (mc, "inconsistent state");
+ mc_add_state (mc, clone);
+ }
+ else
+ destroy_foo (clone);
+ }
+ }
+
+ Notes on the above outline:
+
+ - The call to mc_include_state allows currently
+ uninteresting operations to be skipped. It is not
+ essential.
+
+ - The call to mc_name_operation should give the current
+ operation a human-readable name. The name may
+ include printf-style format specifications.
+
+ When an error occurs, the model checker (by default)
+ replays the sequence of operations performed to reach
+ the error, printing the name of the operation at each
+ step, which is often sufficient information in itself
+ to debug the error.
+
+ At higher levels of verbosity, the name is printed
+ for each operation.
+
+ - Operations should be performed on a copy of the data
+ provided. The data provided should not be destroyed
+ or modified.
+
+ - The call to mc_discard_dup_state is needed to discard
+ (probably) duplicate states. It is otherwise
+ optional.
+
+ To reduce the probability of collisions, use a
+ high-quality hash function. MD4 is a reasonable
+ choice: it is fast but high-quality. In one test,
+ switching to MD4 from MD5 increased overall speed of
+ model checking by 8% and actually reduced (!) the
+ number of collisions.
+
+ The hash value needs to include enough of the state
+ to ensure that interesting states are not excluded,
+ but it need not include the entire state. For
+ example, in many cases, the structure of complex data
+ (metadata) is often much more important than the
+ contents (data), so it may be reasonable to hash only
+ the metadata.
+
+ mc_discard_dup_state may be called before or after
+ checking for consistency, but calling it first avoids
+ wasting time checking duplicate states for
+ consistency, which again can be a significant
+ performance boost.
+
+ - The mc_error function reports errors. It may be
+ called as many times as desired to report each kind
+ of inconsistency in a state.
+
+ - The mc_add_state function adds the new state to the
+ queue. It should be called regardless of whether an
+ error was reported, to indicate to the model checker
+ that state processing has finished.
+
+ - The mutation function should be deterministic, to
+ make it possible to reliably reproduce errors.
+
+ 3. void destroy (struct mc *mc, void *data);
+
+ This function is called to discard the client-specified
+ DATA associated with a state.
+
+ Numerous options are available for configuring the model
+ checker. The most important of these are:
+
+ - Search algorithm:
+
+ * Breadth-first search (the default): First try all the
+ operations with depth 1, then those with depth 2, then
+ those with depth 3, and so on.
+
+ This search algorithm finds the least number of
+ operations needed to trigger a given bug.
+
+ * Depth-first search: Searches downward in the tree of
+ states as fast as possible. Good for finding bugs that
+ require long sequences of operations to trigger.
+
+ * Random-first search: Searches through the tree of
+ states in random order.
+
+ * Explicit path: Applies an explicitly specified sequence
+ of operations.
+
+ - Verbosity: By default, messages are printed only when an
+ error is encountered, but you can cause the checker to
+ print a message on every state transition. This is most
+ useful when the errors in your code cause segfaults or
+ some other kind of sudden termination.
+
+ - Treatment of errors: By default, when an error is
+ encountered, the model checker recursively invokes itself
+ with an increased verbosity level and configured to follow
+ only the error path. As long as the mutation function is
+ deterministic, this quickly and concisely replays the
+ error and describes the path followed to reach it in an
+ easily human-readable manner.
+
+ - Limits:
+
+ * Maximum depth: You can limit the depth of the operations
+ performed. Most often useful with depth-first search.
+ By default, depth is unlimited.
+
+ * Maximum queue length: You can limit the number of states
+ kept in the queue at any given time. The main reason to
+ do so is to limit memory consumption. The default
+ limit is 10,000 states. Several strategies are
+ available for choosing which state to drop when the
+ queue overflows.
+
+ - Stop conditions: based on maximum unique states checked,
+ maximum errors found (by default, 1), or maximum time used
+ for checking.
+
+ - Progress: by default, the checker prints a '.' on stderr
+ every .25 seconds, but you can substitute another progress
+ function or disable progress printing.
+
+ This model checker does not (yet) include two features
+ described in the papers cited above: utility scoring
+ heuristics to guide the search strategy and "choice points" to
+ explore alternative cases. The former feature is less
+ interesting for this model checker, because the data
+ structures we are thus far using it to model are much smaller
+ than those discussed in the paper. The latter feature we
+ should implement at some point. */
+
+#ifndef LIBPSPP_MODEL_CHECKER_H
+#define LIBPSPP_MODEL_CHECKER_H 1
+
+#include <stdarg.h>
+#include <stdbool.h>
+#include <stdio.h>
+#include <sys/time.h>
+
+#include <libpspp/compiler.h>
+
+/* An active model checking run. */
+struct mc;
+
+/* Provided by each client of the model checker. */
+struct mc_class
+ {
+ void (*init) (struct mc *);
+ void (*mutate) (struct mc *, const void *);
+ void (*destroy) (const struct mc *, void *);
+ };
+
+/* Results of a model checking run. */
+struct mc_results;
+
+/* Configuration for running the model checker. */
+struct mc_options;
+
+/* Primary external interface to model checker. */
+struct mc_results *mc_run (const struct mc_class *, struct mc_options *);
+
+/* Functions for use from client-supplied "init" and "mutate"
+ functions. */
+bool mc_include_state (struct mc *);
+bool mc_discard_dup_state (struct mc *, unsigned int hash);
+void mc_name_operation (struct mc *, const char *, ...) PRINTF_FORMAT (2, 3);
+void mc_vname_operation (struct mc *, const char *, va_list)
+ PRINTF_FORMAT (2, 0);
+void mc_error (struct mc *, const char *, ...) PRINTF_FORMAT (2, 3);
+void mc_add_state (struct mc *, void *data);
+
+/* Functions for use from client-supplied "init", "mutate", and
+ "destroy" functions. */
+const struct mc_options *mc_get_options (const struct mc *);
+const struct mc_results *mc_get_results (const struct mc *);
+void *mc_get_aux (const struct mc *);
+\f
+/* A path of operations through a model to arrive at some
+ particular state. */
+struct mc_path
+ {
+ int *ops; /* Sequence of operations. */
+ size_t length; /* Number of operations. */
+ size_t capacity; /* Number of operations for which room is allocated. */
+ };
+
+void mc_path_init (struct mc_path *);
+void mc_path_copy (struct mc_path *, const struct mc_path *);
+void mc_path_push (struct mc_path *, int new_state);
+int mc_path_pop (struct mc_path *);
+int mc_path_back (const struct mc_path *);
+void mc_path_destroy (struct mc_path *);
+
+int mc_path_get_operation (const struct mc_path *, size_t index);
+size_t mc_path_get_length (const struct mc_path *);
+
+struct string;
+void mc_path_to_string (const struct mc_path *, struct string *);
+\f
+struct mc_options *mc_options_create (void);
+struct mc_options *mc_options_clone (const struct mc_options *);
+void mc_options_destroy (struct mc_options *);
+
+/* Search strategy. */
+enum mc_strategy
+ {
+ MC_BROAD, /* Breadth-first search. */
+ MC_DEEP, /* Depth-first search. */
+ MC_RANDOM, /* Randomly ordered search. */
+ MC_PATH /* Follow one explicit path. */
+ };
+
+enum mc_strategy mc_options_get_strategy (const struct mc_options *);
+void mc_options_set_strategy (struct mc_options *, enum mc_strategy);
+unsigned int mc_options_get_seed (const struct mc_options *);
+void mc_options_set_seed (struct mc_options *, unsigned int seed);
+int mc_options_get_max_depth (const struct mc_options *);
+void mc_options_set_max_depth (struct mc_options *, int max_depth);
+int mc_options_get_hash_bits (const struct mc_options *);
+void mc_options_set_hash_bits (struct mc_options *, int hash_bits);
+
+const struct mc_path *mc_options_get_follow_path (const struct mc_options *);
+void mc_options_set_follow_path (struct mc_options *, const struct mc_path *);
+
+/* Strategy for dropped states from the queue when it
+ overflows. */
+enum mc_queue_limit_strategy
+ {
+ MC_DROP_NEWEST, /* Don't enqueue the new state at all. */
+ MC_DROP_OLDEST, /* Drop the oldest state in the queue. */
+ MC_DROP_RANDOM /* Drop a random state from the queue. */
+ };
+
+int mc_options_get_queue_limit (const struct mc_options *);
+void mc_options_set_queue_limit (struct mc_options *, int queue_limit);
+enum mc_queue_limit_strategy mc_options_get_queue_limit_strategy (
+ const struct mc_options *);
+void mc_options_set_queue_limit_strategy (struct mc_options *,
+ enum mc_queue_limit_strategy);
+
+int mc_options_get_max_unique_states (const struct mc_options *);
+void mc_options_set_max_unique_states (struct mc_options *,
+ int max_unique_states);
+int mc_options_get_max_errors (const struct mc_options *);
+void mc_options_set_max_errors (struct mc_options *, int max_errors);
+double mc_options_get_time_limit (const struct mc_options *);
+void mc_options_set_time_limit (struct mc_options *, double time_limit);
+
+int mc_options_get_verbosity (const struct mc_options *);
+void mc_options_set_verbosity (struct mc_options *, int verbosity);
+int mc_options_get_failure_verbosity (const struct mc_options *);
+void mc_options_set_failure_verbosity (struct mc_options *,
+ int failure_verbosity);
+FILE *mc_options_get_output_file (const struct mc_options *);
+void mc_options_set_output_file (struct mc_options *, FILE *);
+
+typedef bool mc_progress_func (struct mc *);
+int mc_options_get_progress_usec (const struct mc_options *);
+void mc_options_set_progress_usec (struct mc_options *, int progress_usec);
+mc_progress_func *mc_options_get_progress_func (const struct mc_options *);
+void mc_options_set_progress_func (struct mc_options *, mc_progress_func *);
+
+void *mc_options_get_aux (const struct mc_options *);
+void mc_options_set_aux (struct mc_options *, void *aux);
+\f
+/* Reason that a model checking run terminated. */
+enum mc_stop_reason
+ {
+ MC_CONTINUING, /* Run has not yet terminated. */
+ MC_SUCCESS, /* Queue emptied (ran out of states). */
+ MC_MAX_UNIQUE_STATES, /* Did requested number of unique states. */
+ MC_MAX_ERROR_COUNT, /* Too many errors. */
+ MC_END_OF_PATH, /* Processed requested path (MC_PATH only). */
+ MC_TIMEOUT, /* Timeout. */
+ MC_INTERRUPTED /* Received SIGINT (Ctrl+C). */
+ };
+
+void mc_results_destroy (struct mc_results *);
+
+enum mc_stop_reason mc_results_get_stop_reason (const struct mc_results *);
+int mc_results_get_unique_state_count (const struct mc_results *);
+int mc_results_get_error_count (const struct mc_results *);
+
+int mc_results_get_max_depth_reached (const struct mc_results *);
+double mc_results_get_mean_depth_reached (const struct mc_results *);
+
+const struct mc_path *mc_results_get_error_path (const struct mc_results *);
+
+int mc_results_get_duplicate_dropped_states (const struct mc_results *);
+int mc_results_get_off_path_dropped_states (const struct mc_results *);
+int mc_results_get_depth_dropped_states (const struct mc_results *);
+int mc_results_get_queue_dropped_states (const struct mc_results *);
+int mc_results_get_queued_unprocessed_states (const struct mc_results *);
+int mc_results_get_max_queue_length (const struct mc_results *);
+
+struct timeval mc_results_get_start (const struct mc_results *);
+struct timeval mc_results_get_end (const struct mc_results *);
+double mc_results_get_duration (const struct mc_results *);
+
+#endif /* libpspp/model-checker.h */
projects / pspp-builds.git / commitdiff