Revert "remove plugins"

This reverts commit e92e6791f399195438d687925a7e6020047b4c60.

diff --git a/Makefile b/Makefile
index 313445da9da5c411ed23635a586d36aebb937d10..e47c4ada3dbf21daacbd398784a3337dce9ba5e0 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 conditionvariable.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 conditionvariable.o \

-          context.o execution.o libannotate.o pthread.o futex.o
+          context.o execution.o libannotate.o plugins.o pthread.o futex.o

 
 CPPFLAGS += -Iinclude -I.
 LDFLAGS := -ldl -lrt -rdynamic
 
 CPPFLAGS += -Iinclude -I.
 LDFLAGS := -ldl -lrt -rdynamic

diff --git a/execution.cc b/execution.cc
index 8fba766ba2e518d0d2fa7ad996c5f7ee5f25b1c1..62a7346b56ee22055952bbf7f45bb367df3f117d 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -77,8 +77,8 @@ ModelExecution::ModelExecution(ModelChecker *m,
        mo_graph(new CycleGraph())
 {
        /* Initialize a model-checker thread, for special ModelActions */
        mo_graph(new CycleGraph())
 {
        /* Initialize a model-checker thread, for special ModelActions */

-       model_thread = new Thread(get_next_id());       // L: Create model thread
-       add_thread(model_thread);                       // L: Add model thread to scheduler
+       model_thread = new Thread(get_next_id());
+       add_thread(model_thread);

        scheduler->register_engine(this);
        node_stack->register_engine(this);
 }
        scheduler->register_engine(this);
        node_stack->register_engine(this);
 }

diff --git a/main.cc b/main.cc
index 0f1fbf2bc75c4c30c7110d3b00c2fc279b9516b4..199e23bf13d018e98ef4f8786a241ce22e46a2d5 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -15,6 +15,7 @@
 #include "model.h"
 #include "params.h"
 #include "snapshot-interface.h"
 #include "model.h"
 #include "params.h"
 #include "snapshot-interface.h"

+#include "plugins.h"

 
 static void param_defaults(struct model_params *params)
 {
 
 static void param_defaults(struct model_params *params)
 {


@@ -27,6 +28,7 @@ static void param_defaults(struct model_params *params)
 
 static void print_usage(const char *program_name, 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);
 
        /* Reset defaults before printing */
        param_defaults(params);
 


@@ -65,10 +67,29 @@ static void print_usage(const char *program_name, struct model_params *params)
                params->verbose,
                params->uninitvalue,
                params->maxexecutions);
                params->verbose,
                params->uninitvalue,
                params->maxexecutions);

-
+       model_print("Analysis plugins:\n");
+       for(unsigned int i=0;i<registeredanalysis->size();i++) {
+               TraceAnalysis * analysis=(*registeredanalysis)[i];
+               model_print("%s\n", analysis->name());
+       }

        exit(EXIT_SUCCESS);
 }
 
        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 = "ht:o:e:b:u:x:v::";
 static void parse_options(struct model_params *params, int argc, char **argv)
 {
        const char *shortopts = "ht:o:e:b:u:x:v::";


@@ -105,7 +126,7 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                case 'u':
                        params->uninitvalue = atoi(optarg);
                        break;
                case 'u':
                        params->uninitvalue = atoi(optarg);
                        break;

-/**            case 't':
+               case 't':

                        if (install_plugin(optarg))
                                error = true;
                        break;
                        if (install_plugin(optarg))
                                error = true;
                        break;


@@ -116,7 +137,6 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                                        error = true;
                        }
                        break;
                                        error = true;
                        }
                        break;

-*/

                default: /* '?' */
                        error = true;
                        break;
                default: /* '?' */
                        error = true;
                        break;


@@ -140,12 +160,25 @@ static void parse_options(struct model_params *params, int argc, char **argv)
 int main_argc;
 char **main_argv;
 
 int main_argc;
 char **main_argv;
 

+static void install_trace_analyses(ModelExecution *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);
+               /** Call the installation event for each installed plugin */
+               ta->actionAtInstallation();
+       }
+}
+

 /** The model_main function contains the main model checking loop. */
 static void model_main()
 {
        struct model_params params;
 
        param_defaults(&params);
 /** The model_main function contains the main model checking loop. */
 static void model_main()
 {
        struct model_params params;
 
        param_defaults(&params);

+       register_plugins();

 
        parse_options(&params, main_argc, main_argv);
 
 
        parse_options(&params, main_argc, main_argv);
 


@@ -154,8 +187,8 @@ static void model_main()
 
        snapshot_stack_init();
 
 
        snapshot_stack_init();
 

-       model = new ModelChecker(params);       // L: Model thread is created
-//     install_trace_analyses(model->get_execution());         L: disable plugin
+       model = new ModelChecker(params);
+       install_trace_analyses(model->get_execution());

 
        snapshot_record(0);
        model->run();
 
        snapshot_record(0);
        model->run();

diff --git a/model.cc b/model.cc
index f277970a6166e33205a871edcc59ab7bc501daae..e9f34da5afb6efee11813ace8ba17d099e8d1c58 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -28,7 +28,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        exit_flag(false),
        scheduler(new Scheduler()),
        node_stack(new NodeStack()),
        exit_flag(false),
        scheduler(new Scheduler()),
        node_stack(new NodeStack()),

-       execution(new ModelExecution(this, &this->params, scheduler, node_stack)),      // L: Model thread is created inside
+       execution(new ModelExecution(this, &this->params, scheduler, node_stack)),

        execution_number(1),
        diverge(NULL),
        earliest_diverge(NULL),
        execution_number(1),
        diverge(NULL),
        earliest_diverge(NULL),