From: Peizhao Ou <peizhaoo@uci.edu>
Date: Tue, 8 Oct 2013 17:11:19 +0000 (-0700)
Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker-priv
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=2e63f889abede3b1d257e2c87f8604dd0a3613b3;hp=7f5d347eeaed25cf1cd6f5f3f440430d6900b03c

Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker-priv
---

diff --git a/annotationaction.h b/annotationaction.h
new file mode 100644
index 0000000..8fe463f
--- /dev/null
+++ b/annotationaction.h
@@ -0,0 +1,50 @@
+#ifndef _ANNOTATIONACTION_H
+#define _ANNOTATIONACTION_H
+
+// Annotation type definition
+enum anno_type {PotentialCommitPoint, CommitPointDefine, CommitPointDefineCheck,
+	HBConditionCheck, InterfaceID, InterfaceCond, InterfaceCheck,
+	InterfacePostCheck}
+
+typedef struct cond_args {
+	int arg_num;
+	void* arg_ptrs[];
+} cond_args_t;
+
+/**
+	This class abstracts the execution of the condition check for the
+	happpens-before relationship. For example, PutIfMatch(__RET__ != NULL) ->
+	Get. The "__RET__ != NULL" here is the HB condition.
+*/
+class HBConditionExecutor {
+	public:
+	HBConditionExecutor(void *_func_ptr, void **_args) :
+		func_ptr(_func_ptr),
+		args(_args)
+	{
+	}
+
+	virtual bool execute() = 0;
+
+	private:
+	void *func_ptr;
+	cond_args_t args;
+};
+
+// Function pointers that abstract ID, condition, checks and actions of the
+// interface to be done by the model checker internally
+typedef (uint64_t) (*interface_ID_t)();
+typedef (bool) (*interface_cond_t)();
+typedef (void) (*interface_action_t)();
+
+class InterfaceAction {
+	public:
+	interface_ID_t getIDAction();
+	interface_cond_t getCondAction();
+	// If the returned action is NULL, it means no need for checking!!
+	interface_action_t getCheckAction();
+	interface_action_t getPostCheckAction();
+	private:
+}
+
+#endif
diff --git a/interpreter.cc b/interpreter.cc
new file mode 100644
index 0000000..e69de29
diff --git a/interpreter.h b/interpreter.h
new file mode 100644
index 0000000..d5e5df3
--- /dev/null
+++ b/interpreter.h
@@ -0,0 +1,137 @@
+#ifndef _INTERPRETER_H
+#define _INTERPRETER_H
+
+#include <iostream>
+#include <map>
+#include <string>
+#include <vector>
+#include <utility>
+
+/**
+	SPEC constructs:
+	Each construct should be embraced by /DOUBLE_STAR ... STAR/ annotation.
+	Within there, any line beginning with a "#" is a comment of the annotation.
+	Each constrcut should begin with @Begin and end with @End. Otherwise, the
+	annotation would be considered as normal comments of the source.
+	
+	a) Global construct
+	@Begin
+	@Global_define:
+		...
+	@Interface_cluster:
+		...
+	@Happens-before:
+		...
+	@End
+	
+	b) Interface construct
+	@Begin
+	@Interface: ...
+	@Commit_point_set:
+		...
+	@Condition: ... (Optional)
+	@ID: ... (Optional, use default ID)
+	@Check: (Optional)
+		...
+	@Action: (Optional)
+		...
+	@Post_action: (Optional)
+	@Post_check: (Optional)
+	@End
+
+	c) Potential commit construct
+	@Begin
+	@Potential_commit_point_define: ...
+	@Label: ...
+	@End
+
+	d) Commit point define construct
+	@Begin
+	@Commit_point_define_check: ...
+	@Label: ...
+	@End
+	
+		OR
+
+	@Begin
+	@Commit_point_define: ...
+	@Potential_commit_point_label: ...
+	@Label: ...
+	@End
+*/
+
+/**
+	Key notes for interpreting the spec into the model checking process:
+	1. In the "include/cdsannotate.h" file, it declares a "void
+	cdsannotate(uinit64_t analysistype, void *annotation)" function to register
+	for an atomic annotation for the purpose trace analysis.
+
+	2. All the @Check, @Action, @Post_action, @Post_check can be wrapped into an
+	annotation of the model checker, and it has registered for an
+	AnnotationAction which does the internal checks and actions in the trace
+	analysis.
+*/
+
+using std::map;
+using std::string;
+using std::vector;
+
+// Forward declaration
+class FunctionDeclaration;
+class SpecInterpreter;
+
+// A function pointer that abstracts the checks and actions to be done by the
+// model checker internally
+typedef (void*) (*annotation_action_t)();
+
+class 
+
+class FunctionDeclaration {
+	/**
+		The following is an example to illustrate how to use this class.
+
+		ReturnType functionName(ArgType1 arg1, ArgType2 arg2, ... ArgTypeN argN)
+		{
+			...
+		}
+	*/
+	public:
+	FunctionDeclaration();
+	// Will get "ReturnType" exactly
+	string getReturnType();
+	// Will get "functionName(arg1, arg2, ... argN)
+	string getFunctionCallStatement();
+	// Will get N
+	int getArgumentNum();
+	// argIndex ranges from 0 -- (N - 1). if argIndex == 1, you will get
+	// "ArgType2"
+	string getNthArgType(int argIndex);
+	// argIndex ranges from 0 -- (N - 1). if argIndex == 1, you will get
+	// "arg2"
+	string getNthArg(int argIndex);
+	private:
+	// "ReturnType functionName(ArgType1 arg1, ArgType2 arg2, ... ArgTypeN
+	// argN)"
+	string originalFunctionDefinition();
+};
+
+struct 
+
+}
+
+class SpecInterpreter {
+	public:
+	SpecInterpreter();
+	SpecInterpreter(const char* dirname);
+	void scanFiles();
+	void interpretSpec();
+	
+	private:
+	// Private fields necessary to interpret the spec
+	map<string, FunctionDeclaration> _interface2Decl;
+	vector<pair<
+
+	void generateFiles();
+};
+
+#endif