From: Brian Demsky <bdemsky@uci.edu>
Date: Wed, 10 Apr 2013 18:26:19 +0000 (-0700)
Subject: add some support for traceanalysis plugins
X-Git-Tag: oopsla2013~86
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=4541dc5155c69e168beedf3bd2a8f5ece0e0e65b;hp=7921811e8bd7bba2cdd892434a58ec7254ae0f99

add some support for traceanalysis plugins
---

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