cleanup plugin interface a little more.

add support for options for SCAnalysis

diff --git a/main.cc b/main.cc
index d2d8d4ab835a5d44d35789f1075f8f7d55a09063..5a33baf996bc3d0f85f11108797b8907c89b6507 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -35,6 +35,7 @@ static void param_defaults(struct model_params *params)
 
 static void print_usage(const char *program_name, struct model_params *params)
 {
+       ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
        /* Reset defaults before printing */
        param_defaults(params);
 
@@ -78,8 +79,9 @@ 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"
-"-t, --analysis=NAME         Use Trace Analysis.\n"
-"-o, --options=NAME          Options.\n"
+"-t, --analysis=NAME         Use Analysis Plugin.\n"
+"-o, --options=NAME          Option for previous analysis plugin.  \n"
+"                            -o help for a list of options\n"
 " --                         Program arguments follow.\n\n",
                program_name,
                params->maxreads,
@@ -92,6 +94,11 @@ static void print_usage(const char *program_name, struct model_params *params)
                params->enabledcount,
                params->bound,
                params->uninitvalue);
+       model_print("Analysis plug ins:\n");
+       for(unsigned int i=0;i<registeredanalysis->size();i++) {
+               TraceAnalysis * analysis=(*registeredanalysis)[i];
+               model_print("%s\n", analysis->name());
+       }
        exit(EXIT_SUCCESS);
 }
 

diff --git a/model.cc b/model.cc
index e0c3089e4ec1558e072cd3577b22caa3d3a546e1..d9caf9a91e72ef727835a24433ba3496c74f7cd6 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -36,8 +36,6 @@ ModelChecker::ModelChecker(struct model_params params) :
 ModelChecker::~ModelChecker()
 {
        delete node_stack;
-       for (unsigned int i = 0; i < trace_analyses.size(); i++)
-               delete trace_analyses[i];
        delete scheduler;
 }
 

diff --git a/scanalysis.cc b/scanalysis.cc
index 2738bb50a907a76f6ee6a60fb38d0f68406de7cc..13aada1a8fee202149f11b94b8ab3a9078971d39 100644 (file)
--- a/scanalysis.cc
+++ b/scanalysis.cc
@@ -10,7 +10,9 @@ SCAnalysis::SCAnalysis() :
        badrfset(),
        lastwrmap(),
        threadlists(1),
-       execution(NULL)
+       execution(NULL),
+       print_always(false),
+       print_buggy(true)
 {
 }
 
@@ -21,13 +23,31 @@ void SCAnalysis::setExecution(ModelExecution * execution) {
        this->execution=execution;
 }
 
-char * SCAnalysis::name() {
-       char * name = "SC";
+const char * SCAnalysis::name() {
+       const char * name = "SC";
        return name;
 }
 
-bool SCAnalysis::option(char *) {
-       return false;
+bool SCAnalysis::option(char * opt) {
+       if (strcmp(opt, "verbose")==0) {
+               print_always=true;
+               return false;
+       } else if (strcmp(opt, "buggy")==0) {
+               return false;
+       } else if (strcmp(opt, "quiet")==0) {
+               print_buggy=false;
+               return false;
+       } if (strcmp(opt, "help") != 0) {
+               model_print("Unrecognized option: %s\n", opt);
+       }
+
+       model_print("SC Analysis options\n");
+       model_print("verbose -- print all feasible executions\n");
+       model_print("buggy -- print only buggy executions (default)\n");
+       model_print("quiet -- print nothing\n");
+       model_print("\n");
+       
+       return true;
 }
 
 void SCAnalysis::print_list(action_list_t *list) {
@@ -55,7 +75,8 @@ void SCAnalysis::print_list(action_list_t *list) {
 void SCAnalysis::analyze(action_list_t *actions) {
        action_list_t *list = generateSC(actions);
        check_rf(list);
-       print_list(list);
+       if (print_always || (print_buggy && execution->have_bug_reports()))
+               print_list(list);
 }
 
 void SCAnalysis::check_rf(action_list_t *list) {

diff --git a/scanalysis.h b/scanalysis.h
index 286f73dea6ec00f065af822f66ae4c3baee1f59c..3ad69e57023b074993083c4268c74aac0ec341c9 100644 (file)
--- a/scanalysis.h
+++ b/scanalysis.h
@@ -9,7 +9,7 @@ class SCAnalysis : public TraceAnalysis {
        ~SCAnalysis();
        virtual void setExecution(ModelExecution * execution);
        virtual void analyze(action_list_t *);
-       virtual char * name();
+       virtual const char * name();
        virtual bool option(char *);
 
        SNAPSHOTALLOC
@@ -33,5 +33,7 @@ class SCAnalysis : public TraceAnalysis {
        HashTable<void *, const ModelAction *, uintptr_t, 4 > lastwrmap;
        SnapVector<action_list_t> threadlists;
        ModelExecution *execution;
+       bool print_always;
+       bool print_buggy;
 };
 #endif

diff --git a/traceanalysis.h b/traceanalysis.h
index a71e8c9df9b08123ca371f5bd48b8c193f75fb4d..fe60591f68603d55dcc2a5c546c11099c2866050 100644 (file)
--- a/traceanalysis.h
+++ b/traceanalysis.h
@@ -6,7 +6,7 @@ class TraceAnalysis {
  public:
        virtual void setExecution(ModelExecution * execution) = 0;
        virtual void analyze(action_list_t *) = 0;
-       virtual char * name() = 0;
+       virtual const char * name() = 0;
        virtual bool option(char *) = 0;
 
        SNAPSHOTALLOC