From 4541dc5155c69e168beedf3bd2a8f5ece0e0e65b Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Wed, 10 Apr 2013 11:26:19 -0700 Subject: [PATCH] add some support for traceanalysis plugins --- Makefile | 2 +- main.cc | 15 ++++++++++++++- model.h | 4 ++++ scanalysis.cc | 10 ++++++++++ scanalysis.h | 11 +++++++++++ traceanalysis.h | 2 +- 6 files changed, 41 insertions(+), 3 deletions(-) create mode 100644 scanalysis.cc create mode 100644 scanalysis.h diff --git a/Makefile b/Makefile index 5120cce..7539aca 100644 --- a/Makefile +++ b/Makefile @@ -4,7 +4,7 @@ OBJECTS = libthreads.o schedule.o model.o threads.o librace.o action.o \ nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \ datarace.o impatomic.o cmodelint.o \ snapshot.o malloc.o mymemory.o common.o mutex.o promise.o conditionvariable.o \ - context.o + context.o scanalysis.o CPPFLAGS += -Iinclude -I. LDFLAGS = -ldl -lrt -rdynamic diff --git a/main.cc b/main.cc index 6459f13..fa70754 100644 --- a/main.cc +++ b/main.cc @@ -12,6 +12,7 @@ /* global "model" object */ #include "model.h" #include "snapshot-interface.h" +#include "scanalysis.h" static void param_defaults(struct model_params *params) { @@ -19,6 +20,7 @@ static void param_defaults(struct model_params *params) params->maxfuturedelay = 6; params->fairwindow = 0; params->yieldon = false; + params->sc_trace_analysis = false; params->enabledcount = 1; params->bound = 0; params->maxfuturevalues = 0; @@ -58,6 +60,7 @@ static void print_usage(struct model_params *params) "-b Upper length bound. Default: %d\n" "-v Print verbose execution information.\n" "-u Value for uninitialized reads. Default: %u\n" +"-c Use SC Trace Analysis.\n" "-- Program arguments follow.\n\n", params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->yieldon, params->enabledcount, params->bound, params->uninitvalue); exit(EXIT_SUCCESS); @@ -65,7 +68,7 @@ params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expir static void parse_options(struct model_params *params, int argc, char **argv) { - const char *shortopts = "hym:M:s:S:f:e:b:u:v"; + const char *shortopts = "hymc:M:s:S:f:e:b:u:v"; int opt; bool error = false; while (!error && (opt = getopt(argc, argv, shortopts)) != -1) { @@ -100,6 +103,9 @@ static void parse_options(struct model_params *params, int argc, char **argv) case 'u': params->uninitvalue = atoi(optarg); break; + case 'c': + params->sc_trace_analysis = true; + break; case 'y': params->yieldon = true; break; @@ -126,6 +132,11 @@ static void parse_options(struct model_params *params, int argc, char **argv) int main_argc; char **main_argv; +void install_trace_analyses() { + if (model->params.sc_trace_analysis) + model->add_trace_analysis(new SCAnalysis()); +} + /** The model_main function contains the main model checking loop. */ static void model_main() { @@ -141,6 +152,8 @@ static void model_main() snapshot_stack_init(); model = new ModelChecker(params); + install_trace_analyses(); + snapshot_record(0); model->run(); delete model; diff --git a/model.h b/model.h index 90c8a55..864f6ae 100644 --- a/model.h +++ b/model.h @@ -40,6 +40,7 @@ struct model_params { int maxreads; int maxfuturedelay; bool yieldon; + bool sc_trace_analysis; unsigned int fairwindow; unsigned int enabledcount; unsigned int bound; @@ -138,6 +139,9 @@ public: const model_params params; Node * get_curr_node() const; + void add_trace_analysis(Trace_Analysis * a) { + trace_analyses->push_back(a); + } MEMALLOC private: diff --git a/scanalysis.cc b/scanalysis.cc new file mode 100644 index 0000000..701c50b --- /dev/null +++ b/scanalysis.cc @@ -0,0 +1,10 @@ +#include "scanalysis.h" +#include "model.h" + +SCAnalysis::SCAnalysis() { +} + +void SCAnalysis::analyze(action_list_t * actions) { + + +} diff --git a/scanalysis.h b/scanalysis.h new file mode 100644 index 0000000..0ef12ba --- /dev/null +++ b/scanalysis.h @@ -0,0 +1,11 @@ +#ifndef SCANALYSIS_H +#define SCANALYSIS_H +#include "traceanalysis.h" + +class SCAnalysis : public Trace_Analysis { + public: + SCAnalysis(); + virtual void analyze(action_list_t *); + +}; +#endif diff --git a/traceanalysis.h b/traceanalysis.h index 5c63cfd..46856d2 100644 --- a/traceanalysis.h +++ b/traceanalysis.h @@ -4,6 +4,6 @@ class Trace_Analysis { public: - virtual void analyze(action_list_t *); + virtual void analyze(action_list_t *) = 0; }; #endif -- 2.34.1