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 (file)
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 (file)
index 0000000..e69de29

diff --git a/interpreter.h b/interpreter.h
new file mode 100644 (file)
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