add more more spec-compiler.jj
authorPeizhao Ou <peizhaoo@uci.edu>
Wed, 9 Oct 2013 07:20:38 +0000 (00:20 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Wed, 9 Oct 2013 07:20:38 +0000 (00:20 -0700)
grammer/spec-compiler.jj
setup-env.sh

index 9627a89eb92534aebd95313c4cc4adaf977a8ed6..965e4f5fabc1951becf1361d8b500824f715fb24 100644 (file)
@@ -1,5 +1,61 @@
 /* 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
+       @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
+*/
+
+
+
 options {
        STATIC = false;
        JAVA_UNICODE_ESCAPE = true;
@@ -18,14 +74,22 @@ package edu.uci.eecs.specCompiler.grammerParser;
        }
 PARSER_END(SpecParser)
 
-SKIP : {" " | "\n" | "\r" | "\r\n" | <COMMENT>}
-
-TOKEN :
+SKIP :
 {
-       <SPACE: (" " | "\t")+>
+       " "
+|
+       "\n"
+|
+       "\r"
 |
-       <COMMENT: <SPACE> "#" (~["\n", "\r"])* ["\n", "\r"]>
+       "\t"
 |
+       // Comment for the specification
+       <"#" (~["\n", "\r"])* (["\n", "\r"])>
+}
+
+TOKEN :
+{
        <HEAD: "/**">
 |
        <TAIL: "*/">
@@ -34,11 +98,26 @@ TOKEN :
 |
        <END: "@End">
 |
-       <ID: "@ID:">
+       <GLOBAL_DEFINE: "@Global_define:">
+|
+       <INTERFACE_CLUSTER: "@Interface_cluster:">
+|
+       <HAPPENS_BEFORE: "@Happens_before:">
+|
+       <INTERFACE: "@Interface:">
+|
+       <COMMIT_POINT_SET: "@Commit_point_set:">
 |
        <CONDITION: "@Condition:">
 |
-       <CHECK: "@Check:">
+       <NUM_OR_EMPTY: ["1"-"9"](["0"-"9"])+ | "">
+|
+       <ONE_HB_CONDITION: "@HB_condition:" <NUM_OR_EMPTY> (~["@", "#", "$"])+> 
+|
+       <ALL_HB_CONDITIONS: (<ONE_HB_CONDITION>)*>
+|
+       <ID: "@ID:">
+| <CHECK: "@Check:">
 |
        <ACTION: "@Action:">
 |
@@ -46,18 +125,114 @@ TOKEN :
 |
        <POST_CHECK: "@Post_check:">
 |
-       <GLOBAL_DEFINE: "@Global_define:">
+       <POTENTIAL_COMMIT_POINT_DEFINE: "@Potential_commit_point_define:">
 |
-       <HAPPENS_BEFORE: "@Happens_before:">
+       <LABEL: "@Label:">
 |
-       <INTERFACE_CLUSTER: "@Interface_cluster:">
+       <COMMIT_POINT_DEFINE_CHECK: "@Commit_point_define_check:">
+
 |
-       <POTENTIAL_COMMIT_POINT: "@Potential_commit_point:">
-       
+       <COMMIT_POINT_DEFINE: "@Commit_point_define:">
+|
+       <POTENTIAL_COMMIT_POINT_LABEL: "@Potential_commit_point_label:">
+|
+       <IDENTIFIER: (["a"-"z", "A"-"Z", "_"]) (["0"-"9", "a"-"z", "A"-"Z", "_"])*>
 }
 
 void Start() :
 {}
 {
-       <HEAD> <BEGIN> <END> <TAIL> <EOF>
+       <EOF>
+}
+
+void Global_construct() :
+{}
+{
+       <HEAD> 
+               <BEGIN> 
+                       <HAPPENS_BEFORE> <IDENTIFIER> "(" <IDENTIFIER> ")"  "->" <IDENTIFIER>
+               <END>
+       <TAIL>
+}
+
+void C_CPP_CODE() :
+{}
+{
+       <(~["@", "#", "$"])+>
+}
+
+void Global_define() :
+{}
+{
+       <GLOBAL_DEFINE> C_CPP_CODE()
+}
+
+void Conditional_interface() :
+{}
+{
+       <IDENTIFIER> (<"(" <IDENTIFIER> ")"> | "")
+}
+
+void Interface_cluster() :
+{}
+{
+       <IDENTIFIER> "=" "{" Conditional_interface() (",," Conditional_interface())* "}"
+}
+
+void Interface_clusters() :
+{}
+{
+       <INTERFACE_CLUSTER> (Interface_cluster())+
+}
+
+void Happens_before() :
+{}
+{
+       <HEAD> 
+               <BEGIN> 
+                       <HAPPENS_BEFORE> <IDENTIFIER> "(" <IDENTIFIER> ")"  "->" <IDENTIFIER>
+               <END>
+       <TAIL>
+}
+
+void Interface() :
+{}
+{
+       <HEAD> 
+               <BEGIN> 
+                       <HAPPENS_BEFORE> <IDENTIFIER> "(" <IDENTIFIER> ")"  "->" <IDENTIFIER>
+               <END>
+       <TAIL>
+}
+
+void Potential_commit_point_define() :
+{}
+{
+       <HEAD> 
+               <BEGIN> 
+                       <HAPPENS_BEFORE> <IDENTIFIER> "(" <IDENTIFIER> ")"  "->" <IDENTIFIER>
+               <END>
+       <TAIL>
+}
+
+
+void Commit_point_define() :
+{}
+{
+       <HEAD> 
+               <BEGIN> 
+                       <HAPPENS_BEFORE> <IDENTIFIER> "(" <IDENTIFIER> ")"  "->" <IDENTIFIER>
+               <END>
+       <TAIL>
+}
+
+
+void Commit_point_define_check() :
+{}
+{
+       <HEAD> 
+               <BEGIN> 
+                       <HAPPENS_BEFORE> <IDENTIFIER> "(" <IDENTIFIER> ")"  "->" <IDENTIFIER>
+               <END>
+       <TAIL>
 }
index 4946f85788b44343768f740a739b31bc626919d8..1738ee414a73c50e35f262f7cd01a3437ff0be59 100644 (file)
@@ -1,7 +1,7 @@
 #!/bin/bash
 
 if [ -z $1 ]; then
-       export SPEC_COMPILER_HOME=~/spec-compiler-home
+       export SPEC_COMPILER_HOME=~/spec-checker-compiler
 else
        export SPEC_COMPILER_HOME=$1
 fi