More fuzzing changes
authorbdemsky <bdemsky@uci.edu>
Tue, 4 Jun 2019 22:35:47 +0000 (15:35 -0700)
committerbdemsky <bdemsky@uci.edu>
Wed, 5 Jun 2019 00:59:04 +0000 (17:59 -0700)
17 files changed:
action.h
classlist.h [new file with mode: 0644]
clockvector.h
cyclegraph.h
datarace.h
execution.cc
execution.h
main.cc
model.cc
model.h
nodestack.cc
nodestack.h
params.h
pthread.cc
schedule.h
test/userprog.c
threads-model.h

index fead25e..de5bca9 100644 (file)
--- a/action.h
+++ b/action.h
 #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 (file)
index 0000000..6d9106f
--- /dev/null
@@ -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
index e19a211..0e5ba86 100644 (file)
@@ -7,9 +7,7 @@
 
 #include "mymemory.h"
 #include "modeltypes.h"
-
-/* Forward declaration */
-class ModelAction;
+#include "classlist.h"
 
 class ClockVector {
 public:
index 4f23e32..b9807fc 100644 (file)
@@ -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 {
index 737a6d6..a8f0ba3 100644 (file)
@@ -8,9 +8,7 @@
 #include "config.h"
 #include <stdint.h>
 #include "modeltypes.h"
-
-/* Forward declaration */
-class ModelAction;
+#include "classlist.h"
 
 struct ShadowTable {
        void * array[65536];
index 62a7346..7d38eb4 100644 (file)
@@ -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
index 65c250a..e15270f 100644 (file)
 
 #include "mutex.h"
 #include <condition_variable>
-
-/* 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<const ModelAction *> 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 199e23b..1e5ad16 100644 (file)
--- a/main.cc
+++ b/main.cc
 
 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);
index 9bf9764..f5f20dd 100644 (file)
--- a/model.cc
+++ b/model.cc
 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(&params);
+}
+
 /**
  * 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 9f7804d..166eb12 100644 (file)
--- a/model.h
+++ b/model.h
 #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<ModelAction *> 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<TraceAnalysis *> trace_analyses;
index fdabf28..b9aaf6f 100644 (file)
  * 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
index 06d9866..edaf397 100644 (file)
 #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 *> 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__ */
index a4a1a8c..4f49d81 100644 (file)
--- 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;
 
index 9ab2f28..3f0a1e4 100644 (file)
 #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(&params);
-
-        //parse_options(&params, 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();
index 4269c4d..6498789 100644 (file)
@@ -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,
index 0ff8f12..415eb24 100644 (file)
@@ -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;
 
index 752731e..8ba9d9b 100644 (file)
@@ -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 {