tempory files
authorPeizhao Ou <peizhaoo@uci.edu>
Wed, 23 Oct 2013 05:30:33 +0000 (22:30 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Wed, 23 Oct 2013 05:30:33 +0000 (22:30 -0700)
grammer/backup-spec-compiler.jj [new file with mode: 0644]
grammer/spec-compiler.jj
grammer/spec.txt [new file with mode: 0644]

diff --git a/grammer/backup-spec-compiler.jj b/grammer/backup-spec-compiler.jj
new file mode 100644 (file)
index 0000000..e65f339
--- /dev/null
@@ -0,0 +1,800 @@
+/* spec-compiler.jj Grammer definition for the specification */
+
+
+/*
+       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
+       @Options:
+               # If LANG is not define, it's C++ by default. C does not support class
+               # and template, so if it's defined as C, we should also have a explicit
+               # entry point.
+               LANG = C;
+       @Global_define:
+               @DeclareVar:
+               @InitVar:
+               @DefineFunc:
+               ...
+       @Interface_cluster:
+               ...
+       @Happens-before:
+               ...
+       @End
+       
+       b) Interface construct
+       @Begin
+       @Interface: ...
+       @Commit_point_set:
+               IDENTIFIER | IDENTIFIER ...
+       @Condition: ... (Optional)
+       @HB_Condition:
+               IDENTIFIER :: <C_CPP_Condition>
+       @HB_Condition: ...
+       @ID: ... (Optional, use default ID)
+       @Check: (Optional)
+               ...
+       @Action: (Optional)
+               # Type here must be a pointer
+               @DefineVar: Type var1 = SomeExpression (Optional)
+               @Code (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
+
+       e) Entry point construct
+       @Begin
+       @Entry_point
+       @End
+
+       f) Interface define construct
+       @Begin
+       @Interface_define: <Interface_Name>
+       @End
+*/
+
+
+
+options {
+       STATIC = false;
+       JAVA_UNICODE_ESCAPE = true;
+}
+
+PARSER_BEGIN(SpecParser)
+package edu.uci.eecs.specCompiler.grammerParser;
+
+import java.io.FileInputStream;
+import java.io.FileNotFoundException;
+import java.io.InputStream;
+import java.io.ByteArrayInputStream;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.HashSet;
+
+import edu.uci.eecs.specCompiler.specExtraction.Construct;
+import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
+import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
+import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
+
+       public class SpecParser {
+               public static void main(String[] argvs)
+               throws ParseException, TokenMgrError {
+                       try {
+                               FileInputStream fis = new FileInputStream("./grammer/spec.txt");
+                               SpecParser parser = new SpecParser(fis);
+                               //parser.Parse();
+                               System.out.println("Parsing finished!");
+                               ArrayList<String> typeParams = parser.FormalParamList();
+                       } catch (FileNotFoundException e) {
+                               e.printStackTrace();
+                       }
+               }
+       
+               public static Construct parseSpec(String text)
+               throws ParseException, TokenMgrError {
+                       InputStream input = new ByteArrayInputStream(text.getBytes());
+                       SpecParser parser = new SpecParser(input);
+                       return parser.Parse();
+               }
+
+
+       }
+PARSER_END(SpecParser)
+
+       "/*"}
+
+< IN_COMMENT > SKIP : { <  ~[] > }
+
+< IN_COMMENT > SKIP : {
+       "*/": DEFAULT
+}
+
+<IN_COMMENT> TOKEN : {
+       <A: "@A"> |
+       <B: "@B">
+}
+
+SKIP :
+{
+       " "
+|
+       "\n"
+|
+       "\r"
+|
+       "\r\n"
+|
+       "\t"
+|
+       // "#" comment for the specification
+       <"#" (~["\n", "\r"])* (["\n", "\r"])>
+|
+       // "//" comment for the specification
+       <"//" (~["\n", "\r"])* (["\n", "\r"])>
+}
+
+<IN_COMMENT, DEFAULT> TOKEN :
+{
+/*   Above are specification-only tokens   */
+       <HEAD: "/**" : IN_COMMENT>
+|
+       <TAIL: "*/" : DEFAULT>
+|
+       <BEGIN: "@Begin">
+|
+       <END: "@End">
+|
+       <OPTIONS: "@Options:">
+|
+       <GLOBAL_DEFINE: "@Global_define:">
+|
+       <DECLARE_VAR: "@DeclareVar:">
+|
+       <INIT_VAR: "@InitVar:">
+|
+       <DEFINE_FUNC: "@DefineFunc:">
+|
+       <INTERFACE_CLUSTER: "@Interface_cluster:">
+|
+       <HAPPENS_BEFORE: "@Happens_before:">
+|
+       <INTERFACE: "@Interface:">
+|
+       <COMMIT_POINT_SET: "@Commit_point_set:">
+|
+       <ENTRY_POINT: "@Entry_point">
+|
+       <INTERFACE_DEFINE: "@Interface_define:">
+|
+       <CONDITION: "@Condition:">
+|
+       <HB_CONDITION: "@HB_condition:">
+|
+       <ID: "@ID:">
+|
+       <CHECK: "@Check:">
+|
+       <ACTION: "@Action:">
+|
+       <DEFINEVAR: "@DefineVar:">
+|
+       <CODE: "@Code:">
+|
+       <POST_ACTION: "@Post_action:">
+|
+       <POST_CHECK: "@Post_check:">
+|
+       <POTENTIAL_COMMIT_POINT_DEFINE: "@Potential_commit_point_define:">
+|
+       <LABEL: "@Label:">
+|
+       <COMMIT_POINT_DEFINE_CHECK: "@Commit_point_define_check:">
+|
+       <COMMIT_POINT_DEFINE: "@Commit_point_define:">
+|
+       <POTENTIAL_COMMIT_POINT_LABEL: "@Potential_commit_point_label:">
+
+
+/*   Specification & C/C++ shared tokens   */
+
+// Reserved keywords
+|
+       <CONST: "const">
+|
+       <STRUCT: "struct">
+|
+       <TYPENAME: "typename">
+
+
+|
+       <#DIGIT: ["0"-"9"]>
+|
+       <#LETTER: ["a"-"z", "A"-"Z"]>
+|
+       <IDENTIFIER: (<LETTER> | "_") (<LETTER> | <DIGIT> | "_")*>
+|
+       <EQUALS: "=">
+|
+       <OPEN_PAREN: "{">
+|
+       <CLOSE_PAREN: "}">
+|
+       <OPEN_BRACKET: "(">
+|
+       <CLOSE_BRACKET: ")">
+|
+       <HB_SYMBOL: "->">
+|
+       <COMMA: ",">
+
+|
+/*   C/C++ only token*/
+       <DOT: ".">
+|
+       <STAR: "*">
+|
+       <NEGATE: "~">
+|
+       <EXCLAMATION: "!">
+|
+       <AND: "&">
+|
+       <OR: "|">
+|
+       <MOD: "%">
+|
+       <PLUS: "+">
+|
+       <PLUSPLUS: "++">
+|
+       <MINUS: "-">
+|
+       <MINUSMINUS: "--">
+|
+       <DIVIDE: "/">
+|
+       <BACKSLASH: "\\">
+|
+       <LESS_THAN: "<">
+|
+       <GREATER_THAN: ">">
+|
+       <GREATER_EQUALS: ">=">
+|
+       <LESS_EQUALS: "<=">
+|
+       <LOGICAL_EQUALS: "==">
+|
+       <NOT_EQUALS: "!=">
+|
+       <LOGICAL_AND: "&&">
+|
+       <LOGICAL_OR: "||">
+|
+       <XOR: "^">
+|
+       <QUESTION_MARK: "?">
+|
+       <COLON: ":">
+|
+       <DOUBLECOLON: "::">
+|
+       <SEMI_COLON: ";">
+|
+       <STRING_LITERAL:
+       "\""
+       ((~["\"","\\","\n","\r"])
+       | ("\\"
+               ( ["n","t","b","r","f","\\","'","\""]
+               | ["0"-"7"] ( ["0"-"7"] )?
+               | ["0"-"3"] ["0"-"7"]
+                       ["0"-"7"]
+               )
+               )
+       )*
+       "\"">
+|
+       <CHARACTER_LITERAL:
+       "'"
+       ((~["'","\\","\n","\r"])
+       | ("\\"
+               (["n","t","b","r","f","\\","'","\""]
+               | ["0"-"7"] ( ["0"-"7"] )?
+               | ["0"-"3"] ["0"-"7"]
+               ["0"-"7"]
+               )
+               )
+       )
+       "'">
+|
+       < INTEGER_LITERAL:
+        <DECIMAL_LITERAL> (["l","L"])?
+      | <HEX_LITERAL> (["l","L"])?
+      | <OCTAL_LITERAL> (["l","L"])?>
+|
+       < #DECIMAL_LITERAL: ["1"-"9"] (["0"-"9"])* >
+|
+       < #HEX_LITERAL: "0" ["x","X"] (["0"-"9","a"-"f","A"-"F"])+ >
+|
+       < #OCTAL_LITERAL: "0" (["0"-"7"])* >
+|
+       < FLOATING_POINT_LITERAL:
+        <DECIMAL_FLOATING_POINT_LITERAL>
+      | <HEXADECIMAL_FLOATING_POINT_LITERAL> >
+|
+       < #DECIMAL_FLOATING_POINT_LITERAL:
+        (["0"-"9"])+ "." (["0"-"9"])* (<DECIMAL_EXPONENT>)? (["f","F","d","D"])?
+      | "." (["0"-"9"])+ (<DECIMAL_EXPONENT>)? (["f","F","d","D"])?
+      | (["0"-"9"])+ <DECIMAL_EXPONENT> (["f","F","d","D"])?
+      | (["0"-"9"])+ (<DECIMAL_EXPONENT>)? ["f","F","d","D"]>
+|
+       < #DECIMAL_EXPONENT: ["e","E"] (["+","-"])? (["0"-"9"])+ >
+|
+       < #HEXADECIMAL_FLOATING_POINT_LITERAL:
+        "0" ["x", "X"] (["0"-"9","a"-"f","A"-"F"])+ (".")? <HEXADECIMAL_EXPONENT> (["f","F","d","D"])?
+      | "0" ["x", "X"] (["0"-"9","a"-"f","A"-"F"])* "." (["0"-"9","a"-"f","A"-"F"])+ <HEXADECIMAL_EXPONENT> (["f","F","d","D"])?>
+|
+       < #HEXADECIMAL_EXPONENT: ["p","P"] (["+","-"])? (["0"-"9"])+ >
+}
+
+String Type() :
+{
+       String type;
+       String str;
+}
+{
+       { type = ""; }
+       ("const"
+       { type = "const"; }
+       )?
+       (("struct" { type = type + " struct"; })? 
+       (str = <IDENTIFIER>.image {
+               if (!type.equals(""))
+                       type = type + " " + str;
+               else
+                       type = str;
+       }))
+       ((str = "const".image {
+               if (!type.equals(""))
+                       type = type + " " + str;
+               else
+                       type = str;
+       }) |
+       (str = <STAR>.image {
+               if (!type.equals(""))
+                       type = type + " " + str;
+               else
+                       type = str;
+       }) |
+       (str = <AND>.image {
+               if (!type.equals(""))
+                       type = type + " " + str;
+               else
+                       type = str;
+       })
+       )*
+       {
+               return type;
+       }
+}
+
+ArrayList<String> FormalParamList() :
+{
+       ArrayList<String> typeParams;
+}
+{
+       {
+               typeParams = new ArrayList<String>();
+       }
+       (TypeParam(typeParams) (<COMMA> TypeParam(typeParams))*)?
+       {
+               System.out.println(typeParams);
+               return typeParams;
+       }
+}
+
+void TypeParam(ArrayList<String> typeParams) :
+{
+       String type, param;
+}
+{
+       (type = Type()) (param = <IDENTIFIER>.image)
+       {
+               typeParams.add(type);
+               typeParams.add(param);
+       }
+}
+
+Construct Parse() :
+{
+       Construct res;  
+}
+{
+       (
+       LOOKAHEAD(3) res = Global_construct() |
+       LOOKAHEAD(3) res = Interface() |
+       LOOKAHEAD(3) res = Potential_commit_point_define() |
+       LOOKAHEAD(3) res = Commit_point_define() |
+       LOOKAHEAD(3) res = Commit_point_define_check() |
+       LOOKAHEAD(3) res = Entry_point() |
+       LOOKAHEAD(3) res = Interface_define()
+       )
+       <EOF>
+       {
+               //System.out.println(res);
+               return res;
+       }
+}
+
+GlobalConstruct Global_construct() :
+{
+       GlobalConstruct res;
+       SequentialDefineSubConstruct code;
+       HashMap<String, String> options;
+       String key, value;
+}
+{
+       {
+               res = null;
+               options = new HashMap<String, String>();
+       }
+       <HEAD>
+               <BEGIN> 
+                       (<OPTIONS>
+                               ((key = <IDENTIFIER>.image)
+                               <EQUALS>
+                               (value = <IDENTIFIER>.image)
+                               {
+                                       if (options.containsKey(key)) {
+                                               throw new ParseException("Duplicate options!");
+                                       }
+                                       options.put(key, value);
+                               }
+                               <SEMI_COLON>
+                               )*
+                       )?
+                       (code = Global_define())
+                       { res = new GlobalConstruct(code, options); }
+                       (Interface_clusters(res))?
+                       (Happens_before(res))?
+               <END>
+       <TAIL>
+       {
+               res.unfoldInterfaceCluster();
+               return res;
+       }
+}
+
+String C_CPP_CODE() :
+{
+       StringBuilder text;
+       Token t;
+}
+{
+       {
+               text = new StringBuilder();
+               t = new Token();
+       }
+       (
+       //LOOKAHEAD(2)
+       (
+       t = <CONST> | t = <STRUCT> |
+       t = <IDENTIFIER> | t = <EQUALS> | t = <OPEN_PAREN> | t = <CLOSE_PAREN> |
+       t = <OPEN_BRACKET> | t = <CLOSE_BRACKET> | t = <HB_SYMBOL> | t = <COMMA> |
+       t = <DOT> | t = <STAR> | t = <NEGATE> | t = <EXCLAMATION> | t = <AND> | t = <OR> | t = <MOD> | t = <PLUS> |
+       t = <PLUSPLUS> | t = <MINUS> | t = <MINUSMINUS> | t = <DIVIDE> | t = <BACKSLASH> |
+       t = <LESS_THAN> | t = <GREATER_THAN> | t = <GREATER_EQUALS>     | t = <LESS_EQUALS> |
+       t = <LOGICAL_EQUALS> | t = <NOT_EQUALS> | t = <LOGICAL_AND> | t = <LOGICAL_OR> | t = <XOR> |
+       t = <QUESTION_MARK> | t = <COLON> | t = <DOUBLECOLON> |
+       t = <SEMI_COLON> | t = <STRING_LITERAL> | t = <CHARACTER_LITERAL> |
+       t = <INTEGER_LITERAL> | t = <FLOATING_POINT_LITERAL>
+       )
+       {
+               text.append(t.image);
+               if (t.image.equals(";") || t.image.equals("\\")
+                       || t.image.equals("{") || t.image.equals("}"))
+                       text.append("\n");
+               else
+                       text.append(" ");
+       }
+       )+
+       {
+               //System.out.println(text);
+               return text.toString();
+       }
+}
+
+SequentialDefineSubConstruct Global_define() :
+{
+       String declareVar, initVar, defineFunc;
+}
+{
+       {
+               declareVar = "";
+               initVar = "";
+               defineFunc = "";
+       }
+       <GLOBAL_DEFINE>
+               (<DECLARE_VAR> (declareVar = C_CPP_CODE()))?
+       (<INIT_VAR> (initVar = C_CPP_CODE()))?
+       (<DEFINE_FUNC> (defineFunc = C_CPP_CODE()))?
+       {
+               SequentialDefineSubConstruct res = new SequentialDefineSubConstruct(declareVar, initVar, defineFunc);
+               //System.out.println(res);
+               return res;
+       }
+}
+
+ConditionalInterface Conditional_interface() :
+{
+       String interfaceName, hbConditionLabel;
+}
+{
+       {
+               hbConditionLabel = "";
+       }
+       interfaceName = <IDENTIFIER>.image (<OPEN_BRACKET> hbConditionLabel =
+       <IDENTIFIER>.image <CLOSE_BRACKET>)?
+       {
+               return new ConditionalInterface(interfaceName, hbConditionLabel);
+       }
+}
+
+void Interface_cluster(GlobalConstruct inst) :
+{
+       String clusterName;
+       ConditionalInterface condInterface;
+}
+{
+       (clusterName= <IDENTIFIER>.image)
+       <EQUALS> <OPEN_PAREN>
+               (condInterface = Conditional_interface()
+               { inst.addInterface2Cluster(clusterName, condInterface); } 
+               )
+               (<COMMA> condInterface = Conditional_interface()
+               { inst.addInterface2Cluster(clusterName, condInterface); } 
+               )*
+       <CLOSE_PAREN>
+}
+
+void Interface_clusters(GlobalConstruct inst) :
+{}
+{
+       <INTERFACE_CLUSTER> (Interface_cluster(inst))+
+}
+
+void Happens_before(GlobalConstruct inst) :
+{
+       ConditionalInterface left, right;       
+}
+{
+       <HAPPENS_BEFORE> 
+       (
+       left = Conditional_interface() <HB_SYMBOL> right = Conditional_interface()
+       { inst.addHBCondition(left, right); }
+       )+
+}
+
+InterfaceConstruct Interface() :
+{
+       InterfaceConstruct res;
+       String interfaceName, condition, idCode, check, postAction,
+               postCheck, commitPoint, hbLabel, hbCondition;
+       ActionSubConstruct action;
+       ArrayList<String> commitPointSet;
+       HashMap<String, String> hbConditions;
+}
+{
+       {
+               res = null;
+               action = null;
+               condition = "";
+               idCode = "";
+               check = "";
+               postAction = "";
+               postCheck = "";
+               commitPointSet = new ArrayList<String>();
+               hbConditions = new HashMap<String, String>();
+       }
+       <HEAD> 
+               <BEGIN>
+                       <INTERFACE> (interfaceName = <IDENTIFIER>.image)
+                       <COMMIT_POINT_SET>
+                               (commitPoint = <IDENTIFIER>.image
+                               { commitPointSet.add(commitPoint); }
+                               )
+                               (<OR>
+                                       (commitPoint = <IDENTIFIER>.image)
+                                       {
+                                               if (commitPointSet.contains(commitPoint)) {
+                                                       throw new ParseException(interfaceName + " has" +
+                                                               "duplicate commit point labels");
+                                               }
+                                               commitPointSet.add(commitPoint);
+                                       }
+                               )*
+
+                       (<CONDITION> (condition = C_CPP_CODE()))?
+                       (
+                               <HB_CONDITION>
+                               (hbLabel = <IDENTIFIER>.image)
+                               (hbCondition = C_CPP_CODE())
+                               {
+                                       if (hbConditions.containsKey(hbLabel)) {
+                                               throw new ParseException(interfaceName + " has" +
+                                                       "duplicate happens-before condtion labels");
+                                       }
+                                       hbConditions.put(hbLabel, hbCondition);
+                               }
+                       )*
+                       (<ID> (idCode = C_CPP_CODE()))?
+                       (<CHECK> (check = C_CPP_CODE()))?
+                       (action = Action())?
+                       (<POST_ACTION> (postAction = C_CPP_CODE()))?
+                       (<POST_CHECK> (postCheck = C_CPP_CODE()))?
+               <END>
+       <TAIL>
+       {
+               res = new InterfaceConstruct(interfaceName, commitPointSet, condition,
+                       hbConditions, idCode, check, action, postAction, postCheck);
+               return res;
+       }
+}
+
+ActionSubConstruct Action() :
+{
+       String type, name, expr, defineVarStr, code;
+       ArrayList<DefineVar> defineVars;
+}
+{
+       {
+               defineVars = new ArrayList<DefineVar>();
+               code = "";
+       }
+       <ACTION>
+       (
+               (
+               (<DEFINEVAR> (defineVarStr = C_CPP_CODE()) 
+               {
+                       int eqIdx = defineVarStr.indexOf('=');
+                       int typeEnd = defineVarStr.lastIndexOf(' ', eqIdx - 2);
+                       type = defineVarStr.substring(0, typeEnd);
+                       name = defineVarStr.substring(typeEnd + 1, eqIdx - 1);
+                       expr = defineVarStr.substring(eqIdx + 2);
+                       DefineVar defineVar = new DefineVar(type, name, expr);
+                       defineVars.add(defineVar);
+               })*  (<CODE> (code = C_CPP_CODE()))? ) 
+       )
+       
+       {
+               ActionSubConstruct res = new ActionSubConstruct(defineVars, code);
+               return res;
+       }
+}
+
+PotentialCPDefineConstruct Potential_commit_point_define() :
+{
+       PotentialCPDefineConstruct res;
+       String label, condition;
+}
+{
+
+       { res = null; }
+       <HEAD> 
+               <BEGIN>
+                       <POTENTIAL_COMMIT_POINT_DEFINE> (condition = C_CPP_CODE())
+                       <LABEL> (label = <IDENTIFIER>.image)
+               <END>
+       <TAIL>
+       {
+               res = new PotentialCPDefineConstruct(label, condition); 
+               return res;
+       }
+}
+
+
+CPDefineConstruct Commit_point_define() :
+{
+       CPDefineConstruct res;
+       String label, potentialCPLabel, condition;
+}
+{
+
+       { res = null; }
+       <HEAD> 
+               <BEGIN>
+                       <COMMIT_POINT_DEFINE> (condition = C_CPP_CODE())
+                       <POTENTIAL_COMMIT_POINT_LABEL> (potentialCPLabel = <IDENTIFIER>.image)
+                       <LABEL> (label = <IDENTIFIER>.image)
+               <END>
+       <TAIL>
+       {
+               res = new CPDefineConstruct(label, potentialCPLabel, condition);
+               return res;
+       }
+}
+
+
+CPDefineCheckConstruct Commit_point_define_check() :
+{
+       CPDefineCheckConstruct res;     
+       String label, condition;
+}
+{
+
+       { res = null; }
+       <HEAD> 
+               <BEGIN> 
+                       <COMMIT_POINT_DEFINE_CHECK> (condition = C_CPP_CODE())
+                       <LABEL> (label = <IDENTIFIER>.image)
+               <END>
+       <TAIL>
+       {
+               res = new CPDefineCheckConstruct(label, condition);
+               return res;
+       }
+}
+
+EntryPointConstruct Entry_point() :
+{}
+{
+
+       <HEAD> 
+               <BEGIN> 
+                       <ENTRY_POINT>
+               <END>
+       <TAIL>
+       {
+               return new EntryPointConstruct();
+       }
+}
+
+InterfaceDefineConstruct Interface_define() :
+{
+       String name;    
+}
+{
+       <HEAD>
+               <BEGIN>
+                       <INTERFACE_DEFINE> (name = <IDENTIFIER>.image)
+               <END>
+       <TAIL>
+       {
+               return new InterfaceDefineConstruct(name);
+       }
+}
+
+
index 309fbb4..c048141 100644 (file)
@@ -115,7 +115,7 @@ import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
                        try {
                                FileInputStream fis = new FileInputStream("./grammer/spec.txt");
                                SpecParser parser = new SpecParser(fis);
-                               parser.Parse();
+                               parser.ParseSpec();
                                System.out.println("Parsing finished!");
                        } catch (FileNotFoundException e) {
                                e.printStackTrace();
@@ -133,32 +133,21 @@ import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
        }
 PARSER_END(SpecParser)
 
-SKIP :
-{
-       " "
-|
-       "\n"
-|
-       "\r"
-|
-       "\r\n"
-|
-       "\t"
-|
-       // "#" comment for the specification
-       <"#" (~["\n", "\r"])* (["\n", "\r"])>
-|
-       // "//" comment for the specification
-       <"//" (~["\n", "\r"])* (["\n", "\r"])>
+< IN_COMMENT > SKIP : { <  ~[] > }
+
+< IN_COMMENT, IN_SPEC > SKIP : {
+       "*/": DEFAULT
 }
 
-TOKEN :
-{
-/*   Above are specification-only tokens   */
-       <HEAD: "/**">
-|
-       <TAIL: "*/">
-|
+SKIP : {
+       "/*": IN_COMMENT
+}
+
+SKIP : {
+       "/**": IN_SPEC
+}
+
+<IN_SPEC> TOKEN : {
        <BEGIN: "@Begin">
 |
        <END: "@End">
@@ -212,9 +201,36 @@ TOKEN :
        <COMMIT_POINT_DEFINE: "@Commit_point_define:">
 |
        <POTENTIAL_COMMIT_POINT_LABEL: "@Potential_commit_point_label:">
+}
 
+SKIP :
+{
+       " "
+|
+       "\n"
+|
+       "\r"
+|
+       "\r\n"
+|
+       "\t"
+|
+       // "#" comment for the specification
+       <"#" (~["\n", "\r"])* (["\n", "\r"])>
+|
+       // "//" comment for the specification
+       <"//" (~["\n", "\r"])* (["\n", "\r"])>
+}
 
+<IN_SPEC, DEFAULT> TOKEN :
+{
 /*   Specification & C/C++ shared tokens   */
+// Reserved keywords
+       <CONST: "const">
+|
+       <STRUCT: "struct">
+|
+       <TYPENAME: "typename">
 |
        <#DIGIT: ["0"-"9"]>
 |
@@ -346,66 +362,80 @@ TOKEN :
        < #HEXADECIMAL_EXPONENT: ["p","P"] (["+","-"])? (["0"-"9"])+ >
 }
 
-Construct Parse() :
+String Type() :
 {
-       Construct res;  
+       String type;
+       String str;
 }
 {
-       (
-       LOOKAHEAD(3) res = Global_construct() |
-       LOOKAHEAD(3) res = Interface() |
-       LOOKAHEAD(3) res = Potential_commit_point_define() |
-       LOOKAHEAD(3) res = Commit_point_define() |
-       LOOKAHEAD(3) res = Commit_point_define_check() |
-       LOOKAHEAD(3) res = Entry_point() |
-       LOOKAHEAD(3) res = Interface_define()
-       )
-       <EOF>
+       { type = ""; }
+       ("const"
+       { type = "const"; }
+       )?
+       (("struct" { type = type + " struct"; })? 
+       (str = <IDENTIFIER>.image {
+               if (!type.equals(""))
+                       type = type + " " + str;
+               else
+                       type = str;
+       }))
+       ((str = "const".image {
+               if (!type.equals(""))
+                       type = type + " " + str;
+               else
+                       type = str;
+       }) |
+       (str = <STAR>.image {
+               if (!type.equals(""))
+                       type = type + " " + str;
+               else
+                       type = str;
+       }) |
+       (str = <AND>.image {
+               if (!type.equals(""))
+                       type = type + " " + str;
+               else
+                       type = str;
+       })
+       )*
        {
-               //System.out.println(res);
-               return res;
+               return type;
        }
 }
 
-GlobalConstruct Global_construct() :
+ArrayList<String> FormalParamList() :
 {
-       GlobalConstruct res;
-       SequentialDefineSubConstruct code;
-       HashMap<String, String> options;
-       String key, value;
+       ArrayList<String> typeParams;
 }
 {
        {
-               res = null;
-               options = new HashMap<String, String>();
+               typeParams = new ArrayList<String>();
        }
-       <HEAD>
-               <BEGIN> 
-                       (<OPTIONS>
-                               ((key = <IDENTIFIER>.image)
-                               <EQUALS>
-                               (value = <IDENTIFIER>.image)
-                               {
-                                       if (options.containsKey(key)) {
-                                               throw new ParseException("Duplicate options!");
-                                       }
-                                       options.put(key, value);
-                               }
-                               <SEMI_COLON>
-                               )*
-                       )?
-                       (code = Global_define())
-                       { res = new GlobalConstruct(code, options); }
-                       (Interface_clusters(res))?
-                       (Happens_before(res))?
-               <END>
-       <TAIL>
+       (TypeParam(typeParams) (<COMMA> TypeParam(typeParams))*)?
        {
-               res.unfoldInterfaceCluster();
-               return res;
+               System.out.println(typeParams);
+               return typeParams;
        }
 }
 
+void TypeParam(ArrayList<String> typeParams) :
+{
+       String type, param;
+}
+{
+       (type = Type()) (param = <IDENTIFIER>.image)
+       {
+               typeParams.add(type);
+               typeParams.add(param);
+       }
+}
+
+void ParseSpec() :
+{}
+{
+       <BEGIN> <POTENTIAL_COMMIT_POINT_DEFINE> C_CPP_CODE() <LABEL> <END>
+}
+
 String C_CPP_CODE() :
 {
        StringBuilder text;
@@ -419,6 +449,7 @@ String C_CPP_CODE() :
        (
        //LOOKAHEAD(2)
        (
+       t = <CONST> | t = <STRUCT> |
        t = <IDENTIFIER> | t = <EQUALS> | t = <OPEN_PAREN> | t = <CLOSE_PAREN> |
        t = <OPEN_BRACKET> | t = <CLOSE_BRACKET> | t = <HB_SYMBOL> | t = <COMMA> |
        t = <DOT> | t = <STAR> | t = <NEGATE> | t = <EXCLAMATION> | t = <AND> | t = <OR> | t = <MOD> | t = <PLUS> |
@@ -444,264 +475,16 @@ String C_CPP_CODE() :
        }
 }
 
-SequentialDefineSubConstruct Global_define() :
-{
-       String declareVar, initVar, defineFunc;
-}
-{
-       {
-               declareVar = "";
-               initVar = "";
-               defineFunc = "";
-       }
-       <GLOBAL_DEFINE>
-               (<DECLARE_VAR> (declareVar = C_CPP_CODE()))?
-       (<INIT_VAR> (initVar = C_CPP_CODE()))?
-       (<DEFINE_FUNC> (defineFunc = C_CPP_CODE()))?
-       {
-               SequentialDefineSubConstruct res = new SequentialDefineSubConstruct(declareVar, initVar, defineFunc);
-               //System.out.println(res);
-               return res;
-       }
-}
-
-ConditionalInterface Conditional_interface() :
-{
-       String interfaceName, hbConditionLabel;
-}
-{
-       {
-               hbConditionLabel = "";
-       }
-       interfaceName = <IDENTIFIER>.image (<OPEN_BRACKET> hbConditionLabel =
-       <IDENTIFIER>.image <CLOSE_BRACKET>)?
-       {
-               return new ConditionalInterface(interfaceName, hbConditionLabel);
-       }
-}
-
-void Interface_cluster(GlobalConstruct inst) :
-{
-       String clusterName;
-       ConditionalInterface condInterface;
-}
-{
-       (clusterName= <IDENTIFIER>.image)
-       <EQUALS> <OPEN_PAREN>
-               (condInterface = Conditional_interface()
-               { inst.addInterface2Cluster(clusterName, condInterface); } 
-               )
-               (<COMMA> condInterface = Conditional_interface()
-               { inst.addInterface2Cluster(clusterName, condInterface); } 
-               )*
-       <CLOSE_PAREN>
-}
 
-void Interface_clusters(GlobalConstruct inst) :
+void Comment() :
 {}
 {
-       <INTERFACE_CLUSTER> (Interface_cluster(inst))+
-}
-
-void Happens_before(GlobalConstruct inst) :
-{
-       ConditionalInterface left, right;       
-}
-{
-       <HAPPENS_BEFORE> 
-       (
-       left = Conditional_interface() <HB_SYMBOL> right = Conditional_interface()
-       { inst.addHBCondition(left, right); }
-       )+
-}
-
-InterfaceConstruct Interface() :
-{
-       InterfaceConstruct res;
-       String interfaceName, condition, idCode, check, postAction,
-               postCheck, commitPoint, hbLabel, hbCondition;
-       ActionSubConstruct action;
-       ArrayList<String> commitPointSet;
-       HashMap<String, String> hbConditions;
-}
-{
-       {
-               res = null;
-               action = null;
-               condition = "";
-               idCode = "";
-               check = "";
-               postAction = "";
-               postCheck = "";
-               commitPointSet = new ArrayList<String>();
-               hbConditions = new HashMap<String, String>();
-       }
-       <HEAD> 
-               <BEGIN>
-                       <INTERFACE> (interfaceName = <IDENTIFIER>.image)
-                       <COMMIT_POINT_SET>
-                               (commitPoint = <IDENTIFIER>.image
-                               { commitPointSet.add(commitPoint); }
-                               )
-                               (<OR>
-                                       (commitPoint = <IDENTIFIER>.image)
-                                       {
-                                               if (commitPointSet.contains(commitPoint)) {
-                                                       throw new ParseException(interfaceName + " has" +
-                                                               "duplicate commit point labels");
-                                               }
-                                               commitPointSet.add(commitPoint);
-                                       }
-                               )*
-
-                       (<CONDITION> (condition = C_CPP_CODE()))?
-                       (
-                               <HB_CONDITION>
-                               (hbLabel = <IDENTIFIER>.image)
-                               (hbCondition = C_CPP_CODE())
-                               {
-                                       if (hbConditions.containsKey(hbLabel)) {
-                                               throw new ParseException(interfaceName + " has" +
-                                                       "duplicate happens-before condtion labels");
-                                       }
-                                       hbConditions.put(hbLabel, hbCondition);
-                               }
-                       )*
-                       (<ID> (idCode = C_CPP_CODE()))?
-                       (<CHECK> (check = C_CPP_CODE()))?
-                       (action = Action())?
-                       (<POST_ACTION> (postAction = C_CPP_CODE()))?
-                       (<POST_CHECK> (postCheck = C_CPP_CODE()))?
-               <END>
-       <TAIL>
-       {
-               res = new InterfaceConstruct(interfaceName, commitPointSet, condition,
-                       hbConditions, idCode, check, action, postAction, postCheck);
-               return res;
-       }
-}
-
-ActionSubConstruct Action() :
-{
-       String type, name, expr, defineVarStr, code;
-       ArrayList<DefineVar> defineVars;
-}
-{
-       {
-               defineVars = new ArrayList<DefineVar>();
-               code = "";
-       }
-       <ACTION>
-       (
-               (
-               (<DEFINEVAR> (defineVarStr = C_CPP_CODE()) 
-               {
-                       int eqIdx = defineVarStr.indexOf('=');
-                       int typeEnd = defineVarStr.lastIndexOf(' ', eqIdx - 2);
-                       type = defineVarStr.substring(0, typeEnd);
-                       name = defineVarStr.substring(typeEnd + 1, eqIdx - 1);
-                       expr = defineVarStr.substring(eqIdx + 2);
-                       DefineVar defineVar = new DefineVar(type, name, expr);
-                       defineVars.add(defineVar);
-               })*  (<CODE> (code = C_CPP_CODE()))? ) 
-       )
-       
-       {
-               ActionSubConstruct res = new ActionSubConstruct(defineVars, code);
-               return res;
-       }
-}
-
-PotentialCPDefineConstruct Potential_commit_point_define() :
-{
-       PotentialCPDefineConstruct res;
-       String label, condition;
-}
-{
-
-       { res = null; }
-       <HEAD> 
-               <BEGIN>
-                       <POTENTIAL_COMMIT_POINT_DEFINE> (condition = C_CPP_CODE())
-                       <LABEL> (label = <IDENTIFIER>.image)
-               <END>
-       <TAIL>
-       {
-               res = new PotentialCPDefineConstruct(label, condition); 
-               return res;
-       }
-}
-
-
-CPDefineConstruct Commit_point_define() :
-{
-       CPDefineConstruct res;
-       String label, potentialCPLabel, condition;
-}
-{
-
-       { res = null; }
-       <HEAD> 
-               <BEGIN>
-                       <COMMIT_POINT_DEFINE> (condition = C_CPP_CODE())
-                       <POTENTIAL_COMMIT_POINT_LABEL> (potentialCPLabel = <IDENTIFIER>.image)
-                       <LABEL> (label = <IDENTIFIER>.image)
-               <END>
-       <TAIL>
-       {
-               res = new CPDefineConstruct(label, potentialCPLabel, condition);
-               return res;
-       }
+       C_CPP_CODE() 
 }
 
-
-CPDefineCheckConstruct Commit_point_define_check() :
-{
-       CPDefineCheckConstruct res;     
-       String label, condition;
-}
-{
-
-       { res = null; }
-       <HEAD> 
-               <BEGIN> 
-                       <COMMIT_POINT_DEFINE_CHECK> (condition = C_CPP_CODE())
-                       <LABEL> (label = <IDENTIFIER>.image)
-               <END>
-       <TAIL>
-       {
-               res = new CPDefineCheckConstruct(label, condition);
-               return res;
-       }
-}
-
-EntryPointConstruct Entry_point() :
+void Parse() :
 {}
 {
-
-       <HEAD> 
-               <BEGIN> 
-                       <ENTRY_POINT>
-               <END>
-       <TAIL>
-       {
-               return new EntryPointConstruct();
-       }
-}
-
-InterfaceDefineConstruct Interface_define() :
-{
-       String name;    
-}
-{
-       <HEAD>
-               <BEGIN>
-                       <INTERFACE_DEFINE> (name = <IDENTIFIER>.image)
-               <END>
-       <TAIL>
-       {
-               return new InterfaceDefineConstruct(name);
-       }
+       C_CPP_CODE() | 
+       <EOF>
 }
-
-
diff --git a/grammer/spec.txt b/grammer/spec.txt
new file mode 100644 (file)
index 0000000..ec46024
--- /dev/null
@@ -0,0 +1,191 @@
+#include <threads.h>
+#include <stdlib.h>
+#include "librace.h"
+#include "model-assert.h"
+
+#include "my_queue.h"
+
+#define relaxed memory_order_relaxed
+#define release memory_order_release
+#define acquire memory_order_acquire
+
+#define MAX_FREELIST 4 /* Each thread can own up to MAX_FREELIST free nodes */
+#define INITIAL_FREE 2 /* Each thread starts with INITIAL_FREE free nodes */
+
+#define POISON_IDX 0x666
+
+static unsigned int (*free_lists)[MAX_FREELIST];
+
+/* Search this thread's free list for a "new" node */
+static unsigned int new_node()
+{
+       int i;
+       int t = get_thread_num();
+       for (i = 0; i < MAX_FREELIST; i++) {
+               unsigned int node = load_32(&free_lists[t][i]);
+               if (node) {
+                       store_32(&free_lists[t][i], 0);
+                       return node;
+               }
+       }
+       /* free_list is empty? */
+       MODEL_ASSERT(0);
+       return 0;
+}
+
+/* Place this node index back on this thread's free list */
+static void reclaim(unsigned int node)
+{
+       int i;
+       int t = get_thread_num();
+
+       /* Don't reclaim NULL node */
+       MODEL_ASSERT(node);
+
+       for (i = 0; i < MAX_FREELIST; i++) {
+               /* Should never race with our own thread here */
+               unsigned int idx = load_32(&free_lists[t][i]);
+
+               /* Found empty spot in free list */
+               if (idx == 0) {
+                       store_32(&free_lists[t][i], node);
+                       return;
+               }
+       }
+       /* free list is full? */
+       MODEL_ASSERT(0);
+}
+
+void init_queue(queue_t *q, int num_threads)
+{
+       /*
+               @Begin
+               @Entry_point
+               @End
+       */
+
+       int i, j;
+
+       /* Initialize each thread's free list with INITIAL_FREE pointers */
+       /* The actual nodes are initialized with poison indexes */
+       free_lists = malloc(num_threads * sizeof(*free_lists));
+       for (i = 0; i < num_threads; i++) {
+               for (j = 0; j < INITIAL_FREE; j++) {
+                       free_lists[i][j] = 2 + i * MAX_FREELIST + j;
+                       atomic_init(&q->nodes[free_lists[i][j]].next, MAKE_POINTER(POISON_IDX, 0));
+               }
+       }
+
+       /* initialize queue */
+       atomic_init(&q->head, MAKE_POINTER(1, 0));
+       atomic_init(&q->tail, MAKE_POINTER(1, 0));
+       atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0));
+}
+
+/*
+       @Begin
+       @Interface_define: Enqueue
+       @End
+*/
+void enqueue(queue_t *q, unsigned int val)
+{
+       int success = 0;
+       unsigned int node;
+       pointer tail;
+       pointer next;
+       pointer tmp;
+
+       node = new_node();
+       store_32(&q->nodes[node].value, val);
+       tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
+       set_ptr(&tmp, 0); // NULL
+       atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
+
+       while (!success) {
+               tail = atomic_load_explicit(&q->tail, acquire);
+               next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
+               if (tail == atomic_load_explicit(&q->tail, relaxed)) {
+
+                       /* Check for uninitialized 'next' */
+                       MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+
+                       if (get_ptr(next) == 0) { // == NULL
+                               pointer value = MAKE_POINTER(node, get_count(next) + 1);
+                               success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
+                                               &next, value, release, release);
+                       }
+                       if (!success) {
+                               unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
+                               pointer value = MAKE_POINTER(ptr,
+                                               get_count(tail) + 1);
+                               int commit_success = 0;
+                               commit_success = atomic_compare_exchange_strong_explicit(&q->tail,
+                                               &tail, value, release, release);
+                               /**
+                                       @Begin
+                                       @Potential_commit_point_check: __ATOMIC_RET__ == true
+                                       @Label: Enqueue_Success_Point
+                                       @End
+                               */
+                               thrd_yield();
+                       }
+               }
+       }
+       atomic_compare_exchange_strong_explicit(&q->tail,
+                       &tail,
+                       MAKE_POINTER(node, get_count(tail) + 1),
+                       release, release);
+}
+
+
+/*
+       @Begin
+       @Interface_define: Dequeue
+       @End
+*/
+unsigned int dequeue(queue_t *q)
+{
+       unsigned int value;
+       int success = 0;
+       pointer head;
+       pointer tail;
+       pointer next;
+
+       while (!success) {
+               head = atomic_load_explicit(&q->head, acquire);
+               tail = atomic_load_explicit(&q->tail, relaxed);
+               next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
+               if (atomic_load_explicit(&q->head, relaxed) == head) {
+                       if (get_ptr(head) == get_ptr(tail)) {
+
+                               /* Check for uninitialized 'next' */
+                               MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+
+                               if (get_ptr(next) == 0) { // NULL
+                                       return 0; // NULL
+                               }
+                               atomic_compare_exchange_strong_explicit(&q->tail,
+                                               &tail,
+                                               MAKE_POINTER(get_ptr(next), get_count(tail) + 1),
+                                               release, release);
+                               thrd_yield();
+                       } else {
+                               value = load_32(&q->nodes[get_ptr(next)].value);
+                               success = atomic_compare_exchange_strong_explicit(&q->head,
+                                               &head,
+                                               MAKE_POINTER(get_ptr(next), get_count(head) + 1),
+                                               release, release);
+                               /*
+                                       @Begin
+                                       @Commit_point_define_check: __ATOMIC_RET__ == true
+                                       @Label: Dequeue_Success_Point
+                                       @End
+                               */
+                               if (!success)
+                                       thrd_yield();
+                       }
+               }
+       }
+       reclaim(get_ptr(head));
+       return value;
+}