add some support for traceanalysis plugins

diff --git a/Makefile b/Makefile
index 5120cce8845ce1e4858b4bd5e7cd9d2618e59203..7539aca6acb25facc760924f90a45949b364be0e 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
+         context.o scanalysis.o
 
 CPPFLAGS += -Iinclude -I.
 LDFLAGS = -ldl -lrt -rdynamic

diff --git a/main.cc b/main.cc
index 6459f139d7b01e78ad8b7c3fcfb4ca6cfd26a451..fa7075408f7d16c8bf92a00abfb13b0e0c878d5d 100644 (file)
--- 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 90c8a55e5f96f7ca93a6adcd6c6f28fdac96fa4a..864f6aeedcc8072c96d19b6071f95169f02be134 100644 (file)
--- 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 (file)
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 (file)
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 5c63cfd80de2c706969f9c1a9d372c7937542d6a..46856d2fca44761cbffc05b2a7eec2ed85dd2951 100644 (file)
--- 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