From 38c72a8748ae74a5bb8b75e713f363a49b48e7af Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
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 <stdint.h>
#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 <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 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<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;
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 *> 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