add traceanalysis support

diff --git a/Makefile b/Makefile
index 26aadc9629a950fc7db6f17755a50c826810f183..acd281b3b9c2162e974c6843ba37fa455eeeb59a 100644 (file)
--- 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 scanalysis.o execution.o
+         context.o scanalysis.o execution.o plugins.o
 
 CPPFLAGS += -Iinclude -I.
 LDFLAGS = -ldl -lrt -rdynamic

diff --git a/main.cc b/main.cc
index 0ca78b97a8ced2e2cd9e9188386415f0d6192997..c8417c027666219b9fdaa6da21d256ad4ebdf42c 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -4,6 +4,7 @@
 
 #include <unistd.h>
 #include <getopt.h>
+#include <string.h>
 
 #include "common.h"
 #include "output.h"
@@ -15,6 +16,7 @@
 #include "params.h"
 #include "snapshot-interface.h"
 #include "scanalysis.h"
+#include "plugins.h"
 
 static void param_defaults(struct model_params *params)
 {
@@ -23,7 +25,6 @@ static void param_defaults(struct model_params *params)
        params->fairwindow = 0;
        params->yieldon = false;
        params->yieldblock = false;
-       params->sc_trace_analysis = false;
        params->enabledcount = 1;
        params->bound = 0;
        params->maxfuturevalues = 0;
@@ -77,7 +78,7 @@ static void print_usage(const char *program_name, struct model_params *params)
 "-u, --uninitialized=VALUE   Return VALUE any load which may read from an\n"
 "                              uninitialized atomic.\n"
 "                              Default: %u\n"
-"-c, --analysis              Use SC Trace Analysis.\n"
+"-t, --analysis=NAME         Use Trace Analysis.\n"
 " --                         Program arguments follow.\n\n",
                program_name,
                params->maxreads,
@@ -93,9 +94,24 @@ static void print_usage(const char *program_name, struct model_params *params)
        exit(EXIT_SUCCESS);
 }
 
+bool install_plugin(char * name) {
+       ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
+       ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
+
+       for(unsigned int i=0;i<registeredanalysis->size();i++) {
+               TraceAnalysis * analysis=(*registeredanalysis)[i];
+               if (strcmp(name, analysis->name())==0) {
+                       installedanalysis->push_back(analysis);
+                       return false;
+               }
+       }
+       model_print("Analysis %s Not Found\n", name);
+       return true;
+}
+
 static void parse_options(struct model_params *params, int argc, char **argv)
 {
-       const char *shortopts = "hyYcm:M:s:S:f:e:b:u:v::";
+       const char *shortopts = "hyYt:m:M:s:S:f:e:b:u:v::";
        const struct option longopts[] = {
                {"help", no_argument, NULL, 'h'},
                {"liveness", required_argument, NULL, 'm'},
@@ -109,7 +125,7 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                {"bound", required_argument, NULL, 'b'},
                {"verbose", optional_argument, NULL, 'v'},
                {"uninitialized", optional_argument, NULL, 'u'},
-               {"analysis", optional_argument, NULL, 'c'},
+               {"analysis", optional_argument, NULL, 't'},
                {0, 0, 0, 0} /* Terminator */
        };
        int opt, longindex;
@@ -146,12 +162,13 @@ 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;
+               case 't':
+                       if (install_plugin(optarg))
+                               error = true;
+                       break;
                case 'Y':
                        params->yieldblock = true;
                        break;
@@ -178,10 +195,14 @@ static void parse_options(struct model_params *params, int argc, char **argv)
 int main_argc;
 char **main_argv;
 
-static void install_trace_analyses(const ModelExecution *execution)
+static void install_trace_analyses(ModelExecution *execution)
 {
-       if (model->params.sc_trace_analysis)
-               model->add_trace_analysis(new SCAnalysis(execution));
+       ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
+       for(unsigned int i=0;i<installedanalysis->size();i++) {
+               TraceAnalysis * ta=(*installedanalysis)[i];
+               ta->setExecution(execution);
+               model->add_trace_analysis(ta);
+       }
 }
 
 /** The model_main function contains the main model checking loop. */
@@ -190,6 +211,7 @@ static void model_main()
        struct model_params params;
 
        param_defaults(&params);
+       register_plugins();
 
        parse_options(&params, main_argc, main_argv);
 

diff --git a/model.h b/model.h
index 77db6aa79569c9611d1e296fa5fa2b4134f6e584..25e20b129dc6b5280fc28af939495b713c7b1971 100644 (file)
--- a/model.h
+++ b/model.h
@@ -50,7 +50,7 @@ public:
        /** @returns the context for the main model-checking system thread */
        ucontext_t * get_system_context() { return &system_context; }
 
-       const ModelExecution * get_execution() const { return execution; }
+       ModelExecution * get_execution() const { return execution; }
 
        int get_execution_number() const { return execution_number; }
 

diff --git a/params.h b/params.h
index 043b2a5c530bd8a4ed1d78b7f1f81007757c1cb2..0eda8bfa562e281a7bf1e93ae4f565c0449da455 100644 (file)
--- a/params.h
+++ b/params.h
@@ -10,7 +10,6 @@ struct model_params {
        int maxfuturedelay;
        bool yieldon;
        bool yieldblock;
-       bool sc_trace_analysis;
        unsigned int fairwindow;
        unsigned int enabledcount;
        unsigned int bound;

diff --git a/plugins.cc b/plugins.cc
new file mode 100644 (file)
index 0000000..b1d3cfb
--- /dev/null
+++ b/plugins.cc
@@ -0,0 +1,19 @@
+#include "plugins.h"
+#include "scanalysis.h"
+
+ModelVector<TraceAnalysis *> * registered_analysis;
+ModelVector<TraceAnalysis *> * installed_analysis;
+
+void register_plugins() {
+       registered_analysis=new ModelVector<TraceAnalysis *>();
+       installed_analysis=new ModelVector<TraceAnalysis *>();
+       registered_analysis->push_back(new SCAnalysis());
+}
+
+ModelVector<TraceAnalysis *> * getRegisteredTraceAnalysis() {
+       return registered_analysis;
+}
+
+ModelVector<TraceAnalysis *> * getInstalledTraceAnalysis() {
+       return installed_analysis;
+}

diff --git a/plugins.h b/plugins.h
new file mode 100644 (file)
index 0000000..ce0f529
--- /dev/null
+++ b/plugins.h
@@ -0,0 +1,10 @@
+#ifndef PLUGINS_H
+#define PLUGINS_H
+#include "traceanalysis.h"
+#include "stl-model.h"
+
+void register_plugins();
+ModelVector<TraceAnalysis *> * getRegisteredTraceAnalysis();
+ModelVector<TraceAnalysis *> * getInstalledTraceAnalysis();
+
+#endif

diff --git a/scanalysis.cc b/scanalysis.cc
index 98dd8eb43d43bd729a59139dff778a93ceb9fd48..265c84cd4fdf3e937ea48adfbc7e145b14efcb15 100644 (file)
--- a/scanalysis.cc
+++ b/scanalysis.cc
@@ -4,19 +4,28 @@
 #include "clockvector.h"
 #include "execution.h"
 
-SCAnalysis::SCAnalysis(const ModelExecution *execution) :
+SCAnalysis::SCAnalysis() :
        cvmap(),
        cyclic(false),
        badrfset(),
        lastwrmap(),
        threadlists(1),
-       execution(execution)
+       execution(NULL)
 {
 }
 
 SCAnalysis::~SCAnalysis() {
 }
 
+void SCAnalysis::setExecution(ModelExecution * execution) {
+       this->execution=execution;
+}
+
+char * SCAnalysis::name() {
+       char * name = "SC";
+       return name;
+}
+
 void SCAnalysis::print_list(action_list_t *list) {
        model_print("---------------------------------------------------------------------\n");
        if (cyclic)

diff --git a/scanalysis.h b/scanalysis.h
index 3b9fed3547dc74b8cf7d27c80eb25fbc423c87c3..ffa933ad5e2b872769199ca81fbcec9d7afd8333 100644 (file)
--- a/scanalysis.h
+++ b/scanalysis.h
@@ -5,9 +5,12 @@
 
 class SCAnalysis : public TraceAnalysis {
  public:
-       SCAnalysis(const ModelExecution *execution);
+       SCAnalysis();
        ~SCAnalysis();
+       virtual void setExecution(ModelExecution * execution);
        virtual void analyze(action_list_t *);
+       virtual char * name();
+
 
        SNAPSHOTALLOC
  private:
@@ -29,6 +32,6 @@ class SCAnalysis : public TraceAnalysis {
        HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > badrfset;
        HashTable<void *, const ModelAction *, uintptr_t, 4 > lastwrmap;
        SnapVector<action_list_t> threadlists;
-       const ModelExecution *execution;
+       ModelExecution *execution;
 };
 #endif

diff --git a/traceanalysis.h b/traceanalysis.h
index 8376bbcf10c1fa433f18ff8bb8501727e649a15f..43c6ebacfac7d9d2a94b0bbd27335e5b8c975396 100644 (file)
--- a/traceanalysis.h
+++ b/traceanalysis.h
@@ -4,7 +4,9 @@
 
 class TraceAnalysis {
  public:
+       virtual void setExecution(ModelExecution * execution) = 0;
        virtual void analyze(action_list_t *) = 0;
+       virtual char * name() = 0;
        SNAPSHOTALLOC
 };
 #endif