From: Ben Pfaff Date: Fri, 24 Apr 2009 04:09:12 +0000 (-0700) Subject: model-checker: Kill dependencies and move back to libpspp. X-Git-Tag: v0.7.3~94 X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=3db80dc65b18355b719e8d56032400c753aa4eb7;p=pspp-builds.git model-checker: Kill dependencies and move back to libpspp. Commit 95b074ff3 "Moved the datasheet testing code out of src/{libspp,data}" moved the model-checker implementation from libpspp into language/tests because it depended on math/moments.h and data/val-type.h, which violates the dependency structure of the PSPP libraries. However, now I want to use the model checker in a test that should not need to use anything from language/tests, so this commit eliminates these dependencies and moves the model checker back to src/libpspp. --- diff --git a/src/language/tests/automake.mk b/src/language/tests/automake.mk index 54d95107..6268422e 100644 --- a/src/language/tests/automake.mk +++ b/src/language/tests/automake.mk @@ -11,8 +11,6 @@ language_tests_sources = \ src/language/tests/format-guesser-test.c \ src/language/tests/float-format.c \ src/language/tests/moments-test.c \ - src/language/tests/model-checker.c \ - src/language/tests/model-checker.h \ src/language/tests/paper-size.c \ src/language/tests/pool-test.c diff --git a/src/language/tests/check-model.q b/src/language/tests/check-model.q index b1f44ffa..2f7b34df 100644 --- a/src/language/tests/check-model.q +++ b/src/language/tests/check-model.q @@ -1,5 +1,5 @@ /* PSPP - a program for statistical analysis. - Copyright (C) 2007 Free Software Foundation, Inc. + Copyright (C) 2007, 2009 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 @@ -21,8 +21,8 @@ #include -#include #include +#include #include "error.h" #include "fwriteerror.h" diff --git a/src/language/tests/datasheet-check.c b/src/language/tests/datasheet-check.c index cb2732bc..53b62c31 100644 --- a/src/language/tests/datasheet-check.c +++ b/src/language/tests/datasheet-check.c @@ -18,7 +18,6 @@ #include #include "datasheet-check.h" -#include "model-checker.h" #include #include @@ -30,6 +29,7 @@ #include #include #include +#include #include #include #include diff --git a/src/language/tests/model-checker.c b/src/language/tests/model-checker.c deleted file mode 100644 index a0407500..00000000 --- a/src/language/tests/model-checker.c +++ /dev/null @@ -1,1466 +0,0 @@ -/* PSPP - a program for statistical analysis. - 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 3 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, see . */ - -#include - -#include "model-checker.h" - -#include -#include -#include -#include -#include -#include -#include - -#include -#include -#include -#include -#include -#include - -#include "error.h" -#include "minmax.h" -#include "xalloc.h" - -/* 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)); - } -} - -/* 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; -} - -/* 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); -} - -/* 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. */ - void (*saved_sigint) (int); /* 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)); -} - -/* 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); -} diff --git a/src/language/tests/model-checker.h b/src/language/tests/model-checker.h deleted file mode 100644 index 8c86fae6..00000000 --- a/src/language/tests/model-checker.h +++ /dev/null @@ -1,463 +0,0 @@ -/* PSPP - a program for statistical analysis. - 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 3 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, see . */ - -/* 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 -#include -#include -#include - -#include - -/* 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 *); - -/* 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 *); - -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); - -/* 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 */ diff --git a/src/libpspp/automake.mk b/src/libpspp/automake.mk index dc512bb2..1564569c 100644 --- a/src/libpspp/automake.mk +++ b/src/libpspp/automake.mk @@ -47,6 +47,8 @@ src_libpspp_libpspp_la_SOURCES = \ src/libpspp/message.h \ src/libpspp/misc.c \ src/libpspp/misc.h \ + src/libpspp/model-checker.c \ + src/libpspp/model-checker.h \ src/libpspp/msg-locator.c \ src/libpspp/msg-locator.h \ src/libpspp/pool.c \ diff --git a/src/libpspp/model-checker.c b/src/libpspp/model-checker.c new file mode 100644 index 00000000..1f83266a --- /dev/null +++ b/src/libpspp/model-checker.c @@ -0,0 +1,1465 @@ +/* PSPP - a program for statistical analysis. + Copyright (C) 2007, 2009 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 3 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, see . */ + +#include + +#include + +#include +#include +#include +#include +#include +#include +#include + +#include +#include +#include +#include +#include + +#include "error.h" +#include "minmax.h" +#include "xalloc.h" + +/* 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)); + } +} + +/* 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; +} + +/* 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. */ + unsigned long int depth_sum; /* Sum of depths. */ + int n_depths; /* Number of depths in depth_sum. */ + + /* 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; + gettimeofday (&results->start, NULL); + return results; +} + +/* Destroys RESULTS. */ +void +mc_results_destroy (struct mc_results *results) +{ + if (results != NULL) + { + 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) +{ + return (results->n_depths == 0 + ? 0 + : (double) results->depth_sum / results->n_depths); +} + +/* 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); +} + +/* 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. */ + void (*saved_sigint) (int); /* 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)); +} + +/* 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; + mc->results->depth_sum += new->path.length; + mc->results->n_depths++; + + 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); +} diff --git a/src/libpspp/model-checker.h b/src/libpspp/model-checker.h new file mode 100644 index 00000000..8c86fae6 --- /dev/null +++ b/src/libpspp/model-checker.h @@ -0,0 +1,463 @@ +/* PSPP - a program for statistical analysis. + 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 3 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, see . */ + +/* 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 +#include +#include +#include + +#include + +/* 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 *); + +/* 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 *); + +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); + +/* 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 */