edits
[cdsspec-compiler.git] / grammer / spec_compiler.jj
index 150ad94f7345712b040f8c9c736c673d5dd31ef2..9195e13a6c70a479d44ade76a9d27658de8299a2 100644 (file)
                @DefineFunc:
        @Interface_cluster:
                ...
-       @Happens-before:
+       @Happens_before:
                ...
+       @Commutativity: // This is to define the admissibility condition
+               // Enq <-> Enq (_M1.q != _M2.q)
+               // Enq <-> Deq (_M1.q != _M2.q)
+               // Deq <-> Deq (_M1.q != _M2.q)
+               // Enq <-> Deq (_M1.q == _M2.q && _M2.__RET__ == NULL)
        @End
        
        b) Interface construct
        @Begin
        @Potential_commit_point_define: ...
        @Label: ...
+       @End
+
+               OR
+
+       @Begin
+       @Potential_additional_ordering_point_define: ...
+       @Label: ...
        @End
 
        d) Commit point define construct
        @Commit_point_define_check: ...
        @Label: ...
        @End
+
+               OR
        
+       # Addition ordering point is used to order operations when there are "equal"
+       # commit point operations on the same location and that we cannot decide
+       # which operation goes first, we will use additional ordering point to order
+       # them (it's just similar to commit points). In implementation, we can just
+       # treat them as commit points with a special flag.
+
+       @Begin
+       @Additional_ordering_point_define: ...
+       @Potential_additional_ordering_point_label: ...
+       @Label: ...
+       @End
+       
+               OR
+       
+       @Begin
+       @Additional_ordering_point_define: ...
+       @Label: ...
+       @End
+
                OR
 
        @Begin
-       @Commit_point_define: ...
-       @Potential_commit_point_label: ...
+       @Additional_ordering_point_define_check: ...
+       @Label: ...
+       @End
+
+       // Commit point clear (just as a normal commit point, but it is used to
+       // clear all commit points)
+       @Begin
+       @Commit_point_clear: ...
        @Label: ...
        @End
 
@@ -114,13 +153,16 @@ import java.io.File;
 import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.HashSet;
+import java.util.Arrays;
 
 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.CommutativityRule;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.CPClearConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
@@ -141,10 +183,10 @@ import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
                public static void main(String[] argvs)
                throws ParseException, TokenMgrError {
                        try {
-                               File f = new File("./grammer/spec.txt");
+                               File f = new File("./grammer/spec1.txt");
                                FileInputStream fis = new FileInputStream(f);
                                SpecParser parser = new SpecParser(fis);
-                               /*
+                               
                                ArrayList<String> content = new ArrayList<String>();
                                ArrayList<Construct> constructs = new ArrayList<Construct>();
                                ArrayList<String> headers = new ArrayList<String>();
@@ -156,9 +198,9 @@ import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
                                for (int i = 0; i < constructs.size(); i++) {
                                        System.out.println(constructs.get(i));
                                }
-                               */
                                
-                               parser.Test();
+                               
+                               //parser.Test();
                                System.out.println("Parsing finished!");
                        } catch (FileNotFoundException e) {
                                e.printStackTrace();
@@ -181,6 +223,13 @@ import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
                        return null;
                }
 
+
+               private static ArrayList<String> breakLines(String all) {
+                       String lines[] = all.split("[\\r\\n]+");
+                       return new ArrayList<String>(Arrays.asList(lines));
+               }
+
+
                public static ArrayList<VariableDeclaration> getTemplateArg(String line)
                throws ParseException {
                        InputStream input = new ByteArrayInputStream(line.getBytes());
@@ -260,7 +309,7 @@ PARSER_END(SpecParser)
 
 
 
-<*> SKIP :
+<IN_POTENTIAL_SPEC, IN_SPEC> SKIP :
 {
        " "
 |
@@ -289,6 +338,10 @@ SKIP : {
        "/*": IN_COMMENT
 }
 
+<DEFAULT> TOKEN: {
+       <ANY: ~[]>
+}
+
 <*> SKIP : {
        // "//" comment for the specification
        <"//" (~["\n", "\r"])* (["\n", "\r"])>
@@ -319,12 +372,16 @@ SKIP : {
        <DECLARE_VAR: "@DeclareVar:">
 |
        <INIT_VAR: "@InitVar:">
+|
+       <CLEANUP: "@Finalize:">
 |
        <DEFINE_FUNC: "@DefineFunc:">
 |
        <INTERFACE_CLUSTER: "@Interface_cluster:">
 |
        <HAPPENS_BEFORE: "@Happens_before:">
+|
+       <COMMUTATIVITY: "@Commutativity:">
 |
        <INTERFACE: "@Interface:">
 |
@@ -355,18 +412,28 @@ SKIP : {
        <POST_CHECK: "@Post_check:">
 |
        <POTENTIAL_COMMIT_POINT_DEFINE: "@Potential_commit_point_define:">
+|
+       <POTENTIAL_ADDITIONAL_ORDERING_POINT_DEFINE: "@Potential_additional_ordering_point_define:">
 |
        <LABEL: "@Label:">
 |
        <COMMIT_POINT_DEFINE_CHECK: "@Commit_point_define_check:">
+|
+       <ADDITIONAL_ORDERING_POINT_DEFINE_CHECK: "@Additional_ordering_point_define_check:">
 |
        <COMMIT_POINT_DEFINE: "@Commit_point_define:">
+|
+       <ADDITIONAL_ORDERING_POINT_DEFINE: "@Additional_ordering_point_define:">
+|
+       <COMMIT_POINT_CLEAR: "@Commit_point_clear:">
 |
        <POTENTIAL_COMMIT_POINT_LABEL: "@Potential_commit_point_label:">
+|
+       <POTENTIAL_ADDITIONAL_ORDERING_POINT_LABEL: "@Potential_additional_ordering_point_label:">
 }
 
 
-<IN_SPEC, DEFAULT> TOKEN :
+<IN_SPEC> TOKEN :
 {
 /*   Specification & C/C++ shared tokens   */
 // Reserved keywords
@@ -409,11 +476,15 @@ SKIP : {
        <CLOSE_BRACE: "}">
 |
        <HB_SYMBOL: "->">
+|
+       <COMMUTATIVITY_SYMBOL: "<->">
 |
        <COMMA: ",">
 |
 /*   C/C++ only token*/
        <DOT: ".">
+|
+       <DOLLAR: "$">
 |
        <STAR: "*">
 |
@@ -560,7 +631,7 @@ String Type() :
 }
 {
        { type = ""; }
-       ("const"
+       (<CONST>
        { type = "const"; }
        )?
        (((str = <STRUCT>.image | str = <CLASS>.image | str = <UNSIGNED>.image) { type = type + " " + str; })? 
@@ -572,7 +643,7 @@ String Type() :
                        type = name.fullName;
        })
        )
-       ((str = "const".image {
+       ((str = <CONST>.image {
                if (!type.equals(""))
                        type = type + " " + str;
                else
@@ -596,24 +667,6 @@ String Type() :
        }
 }
 
-void Test() :
-{
-       String str;     
-       FunctionHeader func;
-}
-{
-       /*
-       str = Type()
-       {
-               System.out.println(str);
-       }
-       */
-       func = FuncDecl() 
-       {
-               System.out.println(func);
-       }
-       
-}
 
 String ParameterizedName() :
 {
@@ -622,8 +675,8 @@ String ParameterizedName() :
 }
 {
        (str = <IDENTIFIER>.image {res = str;})
-       ("<" str = Type() { res = res + "<" + str; }
-       ("," str = Type() { res = res + ", " + str; })* ">"
+       (<OPEN_BRACKET> str = Type() { res = res + "<" + str; }
+       (<COMMA> str = Type() { res = res + ", " + str; })* <CLOSE_BRACKET>
        { res = res + ">"; }
        )?
        {
@@ -676,7 +729,7 @@ ArrayList<VariableDeclaration> TemplateParamList() :
                params = new ArrayList<VariableDeclaration>();
        }
        <TEMPLATE>
-       "<"
+       <OPEN_BRACKET>
        (type = <IDENTIFIER>.image 
        name = <IDENTIFIER>.image
        {
@@ -684,13 +737,13 @@ ArrayList<VariableDeclaration> TemplateParamList() :
        }
        )
 
-       ("," type = <IDENTIFIER>.image 
+       (<COMMA> type = <IDENTIFIER>.image 
        name = <IDENTIFIER>.image
        {
                params.add(new VariableDeclaration(type, name));
        }
        )*
-       ">"
+       <CLOSE_BRACKET>
        {
                //System.out.println(params);
                return params;
@@ -706,10 +759,10 @@ ArrayList<VariableDeclaration > FormalParamList() :
        {
                typeParams = new ArrayList<VariableDeclaration >();
        }
-       "("
+       <OPEN_PAREN>
        ((varDecl = TypeParam() {typeParams.add(varDecl);})
        ((<COMMA> varDecl = TypeParam() {typeParams.add(varDecl);}))*)?
-       ")"
+       <CLOSE_PAREN>
        {
                return typeParams;
        }
@@ -766,7 +819,7 @@ ArrayList<String> C_CPP_CODE(ArrayList<String> headers) :
        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 = <DOT> | t = <STAR> | t = <DOLLAR> | 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> { if (inTemplate) newLine = true; }) |
@@ -827,17 +880,55 @@ ArrayList<String> C_CPP_CODE(ArrayList<String> headers) :
 void Parse(File f, ArrayList<String> content, ArrayList<Construct> constructs, ArrayList<String> headers) :
 {
        Construct inst;
-       ArrayList<String> code;
+       StringBuilder sb;
+       boolean flushSB;
 }
 {
        {
                _file = f;
                _content = content;
                _constructs = constructs;
+               sb = new StringBuilder();
+       }
+       (
+       (inst = ParseSpec()
+       {
+               _constructs.add(inst);
+       }
+       ) |
+       //((code = C_CPP_CODE(headers)) { _content.addAll(code); })
+       (
+       flushSB = OriginalCode(sb)
+       {
+               if (flushSB) {
+                       sb = new StringBuilder();
+               }
+       }
+       )
+       )* 
+       // For the last piece of code
+       {
+               _content.add(sb.toString());
+       }
+       <EOF>
+}
+
+// If true, there's a new line and sb should be flushed
+boolean OriginalCode(StringBuilder sb) :
+{
+       String str;
+}
+{
+       str = <ANY>.image
+       {
+               if (!str.equals("\n")) {
+                       sb.append(str);
+                       return false;
+               } else {
+                       _content.add(sb.toString());
+                       return true;
+               }
        }
-       ((inst = ParseSpec() { _constructs.add(inst); }) |
-       ((code = C_CPP_CODE(headers)) { _content.addAll(code); })
-       )* <EOF>
 }
 
 Construct ParseSpec() :
@@ -851,6 +942,10 @@ Construct ParseSpec() :
        LOOKAHEAD(2) res = Potential_commit_point_define() |
        LOOKAHEAD(2) res = Commit_point_define() |
        LOOKAHEAD(2) res = Commit_point_define_check() |
+       LOOKAHEAD(2) res = Potential_additional_ordering_point_define() |
+       LOOKAHEAD(2) res = Additional_ordering_point_define() |
+       LOOKAHEAD(2) res = Additional_ordering_point_define_check() |
+       LOOKAHEAD(2) res = Commit_point_clear() |
        LOOKAHEAD(2) res = Entry_point() |
        LOOKAHEAD(2) res = Class_begin() |
        LOOKAHEAD(2) res = Class_end() |
@@ -892,6 +987,7 @@ GlobalConstruct Global_construct() :
                        { res = new GlobalConstruct(_file, _content.size(), code, options); }
                        (Interface_clusters(res))?
                        (Happens_before(res))?
+                       (Commutativity(res))?
                <END>
        {
                res.unfoldInterfaceCluster();
@@ -901,7 +997,7 @@ GlobalConstruct Global_construct() :
 
 SequentialDefineSubConstruct Global_define() :
 {
-       ArrayList<String> initVar, defineFunc, code, declareStruct;
+       ArrayList<String> initVar, cleanup, defineFunc, code, declareStruct;
        ArrayList<ArrayList<String>> defineFuncs;
        ArrayList<VariableDeclaration> declareVars;
        ArrayList<ArrayList<String>> declareStructs;
@@ -911,20 +1007,22 @@ SequentialDefineSubConstruct Global_define() :
 {
        {
                declareVars = new ArrayList<VariableDeclaration>();
-               initVar = null;
+               initVar = new ArrayList<String>();
+               cleanup = new ArrayList<String>();
                defineFuncs = new ArrayList<ArrayList<String>>();
                declareStructs = new ArrayList<ArrayList<String>>();
        }
        <GLOBAL_DEFINE>
        (<DECLARE_STRUCT> (declareStruct = C_CPP_CODE(null) {
                declareStructs.add(declareStruct); }))*
-               (<DECLARE_VAR> ((declareVar = TypeParam() ";" {
+               (<DECLARE_VAR> ((declareVar = TypeParam() <SEMI_COLON> {
                        declareVars.add(declareVar); } )*))?
        (<INIT_VAR> (code = C_CPP_CODE(null) { initVar = code; } ))?
+       (<CLEANUP> (code = C_CPP_CODE(null) { cleanup = code; } ))?
        (<DEFINE_FUNC> (defineFunc = C_CPP_CODE(null) { defineFuncs.add(defineFunc); }))*
        {
                SequentialDefineSubConstruct res = new
-                       SequentialDefineSubConstruct(declareStructs, declareVars, initVar, defineFuncs);
+                       SequentialDefineSubConstruct(declareStructs, declareVars, initVar, cleanup, defineFuncs);
                //System.out.println(res);
                return res;
        }
@@ -980,6 +1078,29 @@ void Happens_before(GlobalConstruct inst) :
        )+
 }
 
+void Commutativity(GlobalConstruct inst) :
+{
+       String method1, method2, condition;
+       ArrayList<String> content;
+}
+{
+       {
+               content = new ArrayList<String>();
+       }
+
+       (
+       <COMMUTATIVITY>
+       method1 = <IDENTIFIER>.image  <COMMUTATIVITY_SYMBOL>
+       method2 = <IDENTIFIER>.image
+       <COLON>
+       content = C_CPP_CODE(null)
+       { condition = stringArray2String(content); }
+       {
+               inst.addCommutativityRule(method1, method2, condition);
+       }
+       )+
+}
+
 InterfaceConstruct Interface() :
 {
        InterfaceConstruct res;
@@ -1065,6 +1186,26 @@ PotentialCPDefineConstruct Potential_commit_point_define() :
        }
 }
 
+PotentialCPDefineConstruct Potential_additional_ordering_point_define() :
+{
+       PotentialCPDefineConstruct res;
+       String label, condition;
+       ArrayList<String> content;
+}
+{
+
+       { res = null; }
+               <BEGIN>
+                       <POTENTIAL_ADDITIONAL_ORDERING_POINT_DEFINE> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
+                       <LABEL> (label = <IDENTIFIER>.image)
+               <END>
+       {
+               // Set the boolean flag isAdditionalOrderingPoint to be true
+               res = new PotentialCPDefineConstruct(_file, _content.size(), true, label, condition); 
+               return res;
+       }
+}
+
 
 CPDefineConstruct Commit_point_define() :
 {
@@ -1081,7 +1222,47 @@ CPDefineConstruct Commit_point_define() :
                        <LABEL> (label = <IDENTIFIER>.image)
                <END>
        {
-               res = new CPDefineConstruct(_file, _content.size(), label, potentialCPLabel, condition);
+               res = new CPDefineConstruct(_file, _content.size(), false, label, potentialCPLabel, condition);
+               return res;
+       }
+}
+
+CPDefineConstruct Additional_ordering_point_define() :
+{
+       CPDefineConstruct res;
+       String label, potentialCPLabel, condition;
+       ArrayList<String> content;
+}
+{
+
+       { res = null; }
+               <BEGIN>
+                       <ADDITIONAL_ORDERING_POINT_DEFINE> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
+                       <POTENTIAL_ADDITIONAL_ORDERING_POINT_LABEL> (potentialCPLabel = <IDENTIFIER>.image)
+                       <LABEL> (label = <IDENTIFIER>.image)
+               <END>
+       {
+               // Set the boolean flag isAdditionalOrderingPoint to be true
+               res = new CPDefineConstruct(_file, _content.size(), true, label, potentialCPLabel, condition);
+               return res;
+       }
+}
+
+CPClearConstruct Commit_point_clear() :
+{
+       CPClearConstruct res;   
+       String label, condition;
+       ArrayList<String> content;
+}
+{
+
+       { res = null; }
+               <BEGIN> 
+                       <COMMIT_POINT_CLEAR> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
+                       <LABEL> (label = <IDENTIFIER>.image)
+               <END>
+       {
+               res = new CPClearConstruct(_file, _content.size(), label, condition);
                return res;
        }
 }
@@ -1101,7 +1282,27 @@ CPDefineCheckConstruct Commit_point_define_check() :
                        <LABEL> (label = <IDENTIFIER>.image)
                <END>
        {
-               res = new CPDefineCheckConstruct(_file, _content.size(), label, condition);
+               res = new CPDefineCheckConstruct(_file, _content.size(), false, label, condition);
+               return res;
+       }
+}
+
+CPDefineCheckConstruct Additional_ordering_point_define_check() :
+{
+       CPDefineCheckConstruct res;     
+       String label, condition;
+       ArrayList<String> content;
+}
+{
+
+       { res = null; }
+               <BEGIN> 
+                       <ADDITIONAL_ORDERING_POINT_DEFINE_CHECK> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
+                       <LABEL> (label = <IDENTIFIER>.image)
+               <END>
+       {
+               // Set the boolean flag isAdditionalOrderingPoint to be true
+               res = new CPDefineCheckConstruct(_file, _content.size(), true, label, condition);
                return res;
        }
 }