From 38c72a8748ae74a5bb8b75e713f363a49b48e7af Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 4 Jun 2019 15:35:47 -0700 Subject: [PATCH] More fuzzing changes --- action.h | 8 +----- classlist.h | 18 ++++++++++++ clockvector.h | 4 +-- cyclegraph.h | 4 +-- datarace.h | 4 +-- execution.cc | 9 +----- execution.h | 23 ++++------------ main.cc | 24 ++++------------ model.cc | 73 ++++++++----------------------------------------- model.h | 26 +++--------------- nodestack.cc | 22 +++------------ nodestack.h | 33 ++-------------------- params.h | 2 -- pthread.cc | 34 +---------------------- schedule.h | 6 +--- test/userprog.c | 2 +- threads-model.h | 2 +- 17 files changed, 60 insertions(+), 234 deletions(-) create mode 100644 classlist.h diff --git a/action.h b/action.h index fead25e6..de5bca90 100644 --- a/action.h +++ b/action.h @@ -12,10 +12,7 @@ #include "memoryorder.h" #include "modeltypes.h" #include "pthread.h" - -/* Forward declarations */ -class ClockVector; -class Thread; +#include "classlist.h" namespace cdsc { class mutex; @@ -78,9 +75,6 @@ typedef enum action_type { NOOP } action_type_t; -/* Forward declaration */ -class Node; -class ClockVector; /** * @brief Represents a single atomic action diff --git a/classlist.h b/classlist.h new file mode 100644 index 00000000..6d9106fc --- /dev/null +++ b/classlist.h @@ -0,0 +1,18 @@ +#ifndef CLASSLIST_H +#define CLASSLIST_H +class ClockVector; +class CycleGraph; +class CycleNode; +class ModelAction; +class ModelChecker; +class ModelExecution; +class Node; +class NodeStack; +class Scheduler; +class Thread; +class TraceAnalysis; + +struct model_snapshot_members; +struct bug_message; + +#endif diff --git a/clockvector.h b/clockvector.h index e19a2113..0e5ba865 100644 --- a/clockvector.h +++ b/clockvector.h @@ -7,9 +7,7 @@ #include "mymemory.h" #include "modeltypes.h" - -/* Forward declaration */ -class ModelAction; +#include "classlist.h" class ClockVector { public: diff --git a/cyclegraph.h b/cyclegraph.h index 4f23e322..b9807fca 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -16,9 +16,7 @@ #include "config.h" #include "mymemory.h" #include "stl-model.h" - -class CycleNode; -class ModelAction; +#include "classlist.h" /** @brief A graph of Model Actions for tracking cycles. */ class CycleGraph { diff --git a/datarace.h b/datarace.h index 737a6d6e..a8f0ba32 100644 --- a/datarace.h +++ b/datarace.h @@ -8,9 +8,7 @@ #include "config.h" #include #include "modeltypes.h" - -/* Forward declaration */ -class ModelAction; +#include "classlist.h" struct ShadowTable { void * array[65536]; diff --git a/execution.cc b/execution.cc index 62a7346b..7d38eb43 100644 --- a/execution.cc +++ b/execution.cc @@ -56,11 +56,10 @@ struct model_snapshot_members { /** @brief Constructor */ ModelExecution::ModelExecution(ModelChecker *m, - const struct model_params *params, Scheduler *scheduler, NodeStack *node_stack) : model(m), - params(params), + params(NULL), scheduler(scheduler), action_trace(), thread_map(2), /* We'll always need at least 2 threads */ @@ -1585,12 +1584,6 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons return NULL; } -/** @return True if the execution has taken too many steps */ -bool ModelExecution::too_many_steps() const -{ - return params->bound != 0 && priv->used_sequence_numbers > params->bound; -} - /** * Takes the next step in the execution, if possible. * @param curr The current step to take diff --git a/execution.h b/execution.h index 65c250a6..e15270f4 100644 --- a/execution.h +++ b/execution.h @@ -17,17 +17,7 @@ #include "mutex.h" #include - -/* Forward declaration */ -class Node; -class NodeStack; -class CycleGraph; -class Scheduler; -class Thread; -class ClockVector; -struct model_snapshot_members; -class ModelChecker; -struct bug_message; +#include "classlist.h" /** @brief Shorthand for a list of release sequence heads */ typedef ModelVector rel_heads_list_t; @@ -62,13 +52,13 @@ struct release_seq { class ModelExecution { public: ModelExecution(ModelChecker *m, - const struct model_params *params, - Scheduler *scheduler, + Scheduler *scheduler, NodeStack *node_stack); ~ModelExecution(); - const struct model_params * get_params() const { return params; } - + struct model_params * get_params() const { return params; } + void setParams(struct model_params * _params) {params = _params;} + Thread * take_step(ModelAction *curr); void print_summary() const; @@ -110,7 +100,6 @@ public: void print_infeasibility(const char *prefix) const; bool is_infeasible() const; bool is_deadlocked() const; - bool too_many_steps() const; action_list_t * get_action_trace() { return &action_trace; } @@ -124,7 +113,7 @@ private: ModelChecker *model; - const model_params * const params; + struct model_params * params; /** The scheduler to use: tracks the running/ready Threads */ Scheduler * const scheduler; diff --git a/main.cc b/main.cc index 199e23bf..1e5ad166 100644 --- a/main.cc +++ b/main.cc @@ -19,11 +19,9 @@ static void param_defaults(struct model_params *params) { - params->enabledcount = 1; - params->bound = 0; params->verbose = !!DBG_ENABLED(); params->uninitvalue = 0; - params->maxexecutions = 0; + params->maxexecutions = 10; } static void print_usage(const char *program_name, struct model_params *params) @@ -44,10 +42,6 @@ static void print_usage(const char *program_name, struct model_params *params) "\n" "Model-checker options:\n" "-h, --help Display this help message and exit\n" -"-e, --enabled=COUNT Enabled count.\n" -" Default: %d\n" -"-b, --bound=MAX Upper length bound.\n" -" Default: %d\n" "-v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:\n" " 0 is quiet; 1 shows valid executions; 2 is noisy;\n" " 3 is noisier.\n" @@ -62,8 +56,6 @@ static void print_usage(const char *program_name, struct model_params *params) " -o help for a list of options\n" " -- Program arguments follow.\n\n", program_name, - params->enabledcount, - params->bound, params->verbose, params->uninitvalue, params->maxexecutions); @@ -92,11 +84,9 @@ bool install_plugin(char * name) { static void parse_options(struct model_params *params, int argc, char **argv) { - const char *shortopts = "ht:o:e:b:u:x:v::"; + const char *shortopts = "ht:o:u:x:v::"; const struct option longopts[] = { {"help", no_argument, NULL, 'h'}, - {"enabled", required_argument, NULL, 'e'}, - {"bound", required_argument, NULL, 'b'}, {"verbose", optional_argument, NULL, 'v'}, {"uninitialized", required_argument, NULL, 'u'}, {"analysis", required_argument, NULL, 't'}, @@ -114,12 +104,6 @@ static void parse_options(struct model_params *params, int argc, char **argv) case 'x': params->maxexecutions = atoi(optarg); break; - case 'e': - params->enabledcount = atoi(optarg); - break; - case 'b': - params->bound = atoi(optarg); - break; case 'v': params->verbose = optarg ? atoi(optarg) : 1; break; @@ -187,7 +171,9 @@ static void model_main() snapshot_stack_init(); - model = new ModelChecker(params); + if (!model) + model = new ModelChecker(); + model->setParams(params); install_trace_analyses(model->get_execution()); snapshot_record(0); diff --git a/model.cc b/model.cc index 9bf97641..f5f20dd7 100644 --- a/model.cc +++ b/model.cc @@ -21,17 +21,14 @@ ModelChecker *model; /** @brief Constructor */ -ModelChecker::ModelChecker(struct model_params params) : +ModelChecker::ModelChecker() : /* Initialize default scheduler */ - params(params), + params(), restart_flag(false), - exit_flag(false), scheduler(new Scheduler()), node_stack(new NodeStack()), - execution(new ModelExecution(this, &this->params, scheduler, node_stack)), + execution(new ModelExecution(this, scheduler, node_stack)), execution_number(1), - diverge(NULL), - earliest_diverge(NULL), trace_analyses(), inspect_plugin(NULL) { @@ -45,6 +42,12 @@ ModelChecker::~ModelChecker() delete scheduler; } +/** Method to set parameters */ +void ModelChecker::setParams(struct model_params params) { + this->params = params; + execution->setParams(¶ms); +} + /** * Restores user program to initial state and resets all model-checker data * structures. @@ -186,8 +189,6 @@ void ModelChecker::print_stats() const model_print("Number of buggy executions: %d\n", stats.num_buggy_executions); model_print("Number of infeasible executions: %d\n", stats.num_infeasible); model_print("Total executions: %d\n", stats.num_total); - if (params.verbose) - model_print("Total nodes created: %d\n", node_stack->get_total_nodes()); } /** @@ -201,13 +202,6 @@ void ModelChecker::print_execution(bool printbugs) const print_program_output(); if (params.verbose >= 3) { - model_print("\nEarliest divergence point since last feasible execution:\n"); - if (earliest_diverge) - earliest_diverge->print(); - else - model_print("(Not set)\n"); - - model_print("\n"); print_stats(); } @@ -260,37 +254,7 @@ bool ModelChecker::next_execution() execution_number++; reset_to_initial_state(); node_stack->full_reset(); - diverge = NULL; return false; -/* test - if (complete) - earliest_diverge = NULL; - - if (exit_flag) - return false; - -// diverge = execution->get_next_backtrack(); - if (diverge == NULL) { - execution_number++; - reset_to_initial_state(); - model_print("Does not diverge\n"); - return false; - } - - if (DBG_ENABLED()) { - model_print("Next execution will diverge at:\n"); - diverge->print(); - } - - execution_number++; - - if (params.maxexecutions != 0 && stats.num_complete >= params.maxexecutions) - return false; - - reset_to_initial_state(); - return true; -*/ - } /** @brief Run trace analyses on complete trace */ @@ -376,19 +340,9 @@ bool ModelChecker::should_terminate_execution() execution->set_assert(); return true; } - - if (execution->too_many_steps()) - return true; return false; } -/** @brief Exit ModelChecker upon returning to the run loop of the - * model checker. */ -void ModelChecker::exit_model_checker() -{ - exit_flag = true; -} - /** @brief Restart ModelChecker upon returning to the run loop of the * model checker. */ void ModelChecker::restart() @@ -399,8 +353,6 @@ void ModelChecker::restart() void ModelChecker::do_restart() { restart_flag = false; - diverge = NULL; - earliest_diverge = NULL; reset_to_initial_state(); node_stack->full_reset(); memset(&stats,0,sizeof(struct execution_stats)); @@ -410,11 +362,11 @@ void ModelChecker::do_restart() /** @brief Run ModelChecker for the user program */ void ModelChecker::run() { - int i = 0; //Need to initial random number generator state to avoid resets on rollback char random_state[256]; initstate(423121, random_state, sizeof(random_state)); - do { + + for(int exec = 0; exec < params.maxexecutions; exec++) { thrd_t user_thread; Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program execution->add_thread(t); @@ -483,10 +435,9 @@ void ModelChecker::run() t = execution->take_step(curr); } while (!should_terminate_execution()); next_execution(); - i++; //restore random number generator state after rollback setstate(random_state); - } while (i<5); // while (has_next); + } model_print("******* Model-checking complete: *******\n"); print_stats(); diff --git a/model.h b/model.h index 9f7804d8..166eb12d 100644 --- a/model.h +++ b/model.h @@ -15,17 +15,7 @@ #include "stl-model.h" #include "context.h" #include "params.h" - -/* Forward declaration */ -class Node; -class NodeStack; -class CycleGraph; -class Scheduler; -class Thread; -class ClockVector; -class TraceAnalysis; -class ModelExecution; -class ModelAction; +#include "classlist.h" typedef SnapList action_list_t; @@ -41,9 +31,9 @@ struct execution_stats { /** @brief The central structure for model-checking */ class ModelChecker { public: - ModelChecker(struct model_params params); + ModelChecker(); ~ModelChecker(); - + void setParams(struct model_params params); void run(); /** Restart the model checker, intended for pluggins. */ @@ -52,9 +42,6 @@ public: /** Exit the model checker, intended for pluggins. */ void exit_model_checker(); - /** Check the exit_flag. */ - bool get_exit_flag() const { return exit_flag; } - /** @returns the context for the main model-checking system thread */ ucontext_t * get_system_context() { return &system_context; } @@ -73,15 +60,13 @@ public: bool assert_bug(const char *msg, ...); void assert_user_bug(const char *msg); - const model_params params; + model_params params; void add_trace_analysis(TraceAnalysis *a) { trace_analyses.push_back(a); } void set_inspect_plugin(TraceAnalysis *a) { inspect_plugin=a; } MEMALLOC private: /** Flag indicates whether to restart the model checker. */ bool restart_flag; - /** Flag indicates whether to exit the model checker. */ - bool exit_flag; /** The scheduler to use: tracks the running/ready Threads */ Scheduler * const scheduler; @@ -98,9 +83,6 @@ private: Thread * get_next_thread(); void reset_to_initial_state(); - ModelAction *diverge; - ModelAction *earliest_diverge; - ucontext_t system_context; ModelVector trace_analyses; diff --git a/nodestack.cc b/nodestack.cc index fdabf288..b9aaf6fd 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -21,16 +21,12 @@ * parent. * * @param act The ModelAction to associate with this Node. May be NULL. - * @param par The parent Node in the NodeStack. May be NULL if there is no - * parent. * @param nthreads The number of threads which exist at this point in the * execution trace. */ -Node::Node(ModelAction *act, Node *par, int nthreads) : +Node::Node(ModelAction *act) : action(act), - uninit_action(NULL), - parent(par), - num_threads(nthreads) + uninit_action(NULL) { ASSERT(act); act->set_node(this); @@ -52,10 +48,8 @@ void Node::print() const NodeStack::NodeStack() : node_list(), - head_idx(-1), - total_nodes(0) + head_idx(-1) { - total_nodes++; } NodeStack::~NodeStack() @@ -96,14 +90,7 @@ ModelAction * NodeStack::explore_action(ModelAction *act) { DBG(); - /* Record action */ - Node *head = get_head(); - - int next_threads = execution->get_num_threads(); - if (act->get_type() == THREAD_CREATE || act->get_type() == PTHREAD_CREATE ) // may need to be changed - next_threads++; - node_list.push_back(new Node(act, head, next_threads)); - total_nodes++; + node_list.push_back(new Node(act)); head_idx++; return NULL; } @@ -116,7 +103,6 @@ void NodeStack::full_reset() delete node_list[i]; node_list.clear(); reset_execution(); - total_nodes = 1; } Node * NodeStack::get_head() const diff --git a/nodestack.h b/nodestack.h index 06d98663..edaf397e 100644 --- a/nodestack.h +++ b/nodestack.h @@ -11,16 +11,7 @@ #include "mymemory.h" #include "schedule.h" #include "stl-model.h" - -class ModelAction; -class Thread; - -struct fairness_info { - unsigned int enabled_count; - unsigned int turns; - bool priority; -}; - +#include "classlist.h" /** * @brief A single node in a NodeStack @@ -33,24 +24,12 @@ struct fairness_info { */ class Node { public: - Node(ModelAction *act, Node *par, - int nthreads); + Node(ModelAction *act); ~Node(); - bool is_enabled(Thread *t) const; - bool is_enabled(thread_id_t tid) const; - ModelAction * get_action() const { return action; } void set_uninit_action(ModelAction *act) { uninit_action = act; } ModelAction * get_uninit_action() const { return uninit_action; } - - int get_num_threads() const { return num_threads; } - /** @return the parent Node to this Node; that is, the action that - * occurred previously in the stack. */ - Node * get_parent() const { return parent; } - - - void print() const; MEMALLOC @@ -59,8 +38,6 @@ private: /** @brief ATOMIC_UNINIT action which was created at this Node */ ModelAction *uninit_action; - Node * const parent; - const int num_threads; }; typedef ModelVector node_list_t; @@ -79,20 +56,16 @@ public: ~NodeStack(); void register_engine(const ModelExecution *exec); - ModelAction * explore_action(ModelAction *act); Node * get_head() const; Node * get_next() const; void reset_execution(); void full_reset(); - int get_total_nodes() { return total_nodes; } - void print() const; MEMALLOC private: node_list_t node_list; - const struct model_params * get_params() const; /** @brief The model-checker execution object */ @@ -105,8 +78,6 @@ private: * current head Node. It is negative when the list is empty. */ int head_idx; - - int total_nodes; }; #endif /* __NODESTACK_H__ */ diff --git a/params.h b/params.h index a4a1a8c2..4f49d81f 100644 --- a/params.h +++ b/params.h @@ -6,8 +6,6 @@ * the model checker. */ struct model_params { - unsigned int enabledcount; - unsigned int bound; unsigned int uninitvalue; int maxexecutions; diff --git a/pthread.cc b/pthread.cc index 9ab2f285..3f0a1e4f 100644 --- a/pthread.cc +++ b/pthread.cc @@ -14,38 +14,6 @@ #include "model.h" #include "execution.h" -static void param_defaults(struct model_params *params) -{ - params->enabledcount = 1; - params->bound = 0; - params->verbose = !!DBG_ENABLED(); - params->uninitvalue = 0; - params->maxexecutions = 0; -} - -static void model_main() -{ - struct model_params params; - - param_defaults(¶ms); - - //parse_options(¶ms, main_argc, main_argv); - - //Initialize race detector - initRaceDetector(); - - snapshot_stack_init(); - - model = new ModelChecker(params); // L: Model thread is created -// install_trace_analyses(model->get_execution()); L: disable plugin - - snapshot_record(0); - model->run(); - delete model; - - DEBUG("Exiting\n"); -} - int pthread_create(pthread_t *t, const pthread_attr_t * attr, pthread_start_t start_routine, void * arg) { struct pthread_params params = { start_routine, arg }; @@ -80,7 +48,7 @@ void pthread_exit(void *value_ptr) { int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) { if (!model) { - snapshot_system_init(10000, 1024, 1024, 40000, &model_main); + model = new ModelChecker(); } cdsc::mutex *m = new cdsc::mutex(); diff --git a/schedule.h b/schedule.h index 4269c4de..6498789a 100644 --- a/schedule.h +++ b/schedule.h @@ -7,11 +7,7 @@ #include "mymemory.h" #include "modeltypes.h" - -/* Forward declaration */ -class Thread; -class Node; -class ModelExecution; +#include "classlist.h" typedef enum enabled_type { THREAD_DISABLED, diff --git a/test/userprog.c b/test/userprog.c index 0ff8f125..415eb248 100644 --- a/test/userprog.c +++ b/test/userprog.c @@ -24,7 +24,7 @@ static void b(void *obj) printf("r2=%d\n",r2); } -int main(int argc, char **argv) +int user_main(int argc, char **argv) { thrd_t t1, t2; diff --git a/threads-model.h b/threads-model.h index 752731e2..8ba9d9b6 100644 --- a/threads-model.h +++ b/threads-model.h @@ -12,6 +12,7 @@ #include "modeltypes.h" #include "stl-model.h" #include "context.h" +#include "classlist.h" struct thread_params { thrd_start_t func; @@ -35,7 +36,6 @@ typedef enum thread_state { THREAD_COMPLETED } thread_state; -class ModelAction; /** @brief A Thread is created for each user-space thread */ class Thread { -- 2.34.1