interpreter.h

   1 #ifndef _INTERPRETER_H
   2 #define _INTERPRETER_H
   3
   4 #include <iostream>
   5 #include <map>
   6 #include <string>
   7 #include <vector>
   8 #include <utility>
   9
  10 /**
  11         SPEC constructs:
  12         Each construct should be embraced by /DOUBLE_STAR ... STAR/ annotation.
  13         Within there, any line beginning with a "#" is a comment of the annotation.
  14         Each constrcut should begin with @Begin and end with @End. Otherwise, the
  15         annotation would be considered as normal comments of the source.
  16
  17         a) Global construct
  18         @Begin
  19         @Global_define:
  20                 ...
  21         @Interface_cluster:
  22                 ...
  23         @Happens-before:
  24                 ...
  25         @End
  26
  27         b) Interface construct
  28         @Begin
  29         @Interface: ...
  30         @Commit_point_set:
  31                 ...
  32         @Condition: ... (Optional)
  33         @ID: ... (Optional, use default ID)
  34         @Check: (Optional)
  35                 ...
  36         @Action: (Optional)
  37                 ...
  38         @Post_action: (Optional)
  39         @Post_check: (Optional)
  40         @End
  41
  42         c) Potential commit construct
  43         @Begin
  44         @Potential_commit_point_define: ...
  45         @Label: ...
  46         @End
  47
  48         d) Commit point define construct
  49         @Begin
  50         @Commit_point_define_check: ...
  51         @Label: ...
  52         @End
  53
  54                 OR
  55
  56         @Begin
  57         @Commit_point_define: ...
  58         @Potential_commit_point_label: ...
  59         @Label: ...
  60         @End
  61 */
  62
  63 /**
  64         Key notes for interpreting the spec into the model checking process:
  65         1. In the "include/cdsannotate.h" file, it declares a "void
  66         cdsannotate(uinit64_t analysistype, void *annotation)" function to register
  67         for an atomic annotation for the purpose trace analysis.
  68
  69         2. All the @Check, @Action, @Post_action, @Post_check can be wrapped into an
  70         annotation of the model checker, and it has registered for an
  71         AnnotationAction which does the internal checks and actions in the trace
  72         analysis.
  73 */
  74
  75 using std::map;
  76 using std::string;
  77 using std::vector;
  78
  79 // Forward declaration
  80 class FunctionDeclaration;
  81 class SpecInterpreter;
  82
  83 // A function pointer that abstracts the checks and actions to be done by the
  84 // model checker internally
  85 typedef (void*) (*annotation_action_t)();
  86
  87 class
  88
  89 class FunctionDeclaration {
  90         /**
  91                 The following is an example to illustrate how to use this class.
  92
  93                 ReturnType functionName(ArgType1 arg1, ArgType2 arg2, ... ArgTypeN argN)
  94                 {
  95                         ...
  96                 }
  97         */
  98         public:
  99         FunctionDeclaration();
 100         // Will get "ReturnType" exactly
 101         string getReturnType();
 102         // Will get "functionName(arg1, arg2, ... argN)
 103         string getFunctionCallStatement();
 104         // Will get N
 105         int getArgumentNum();
 106         // argIndex ranges from 0 -- (N - 1). if argIndex == 1, you will get
 107         // "ArgType2"
 108         string getNthArgType(int argIndex);
 109         // argIndex ranges from 0 -- (N - 1). if argIndex == 1, you will get
 110         // "arg2"
 111         string getNthArg(int argIndex);
 112         private:
 113         // "ReturnType functionName(ArgType1 arg1, ArgType2 arg2, ... ArgTypeN
 114         // argN)"
 115         string originalFunctionDefinition();
 116 };
 117
 118 struct
 119
 120 }
 121
 122 class SpecInterpreter {
 123         public:
 124         SpecInterpreter();
 125         SpecInterpreter(const char* dirname);
 126         void scanFiles();
 127         void interpretSpec();
 128
 129         private:
 130         // Private fields necessary to interpret the spec
 131         map<string, FunctionDeclaration> _interface2Decl;
 132         vector<pair<
 133
 134         void generateFiles();
 135 };
 136
 137 #endif