From: Peizhao Ou Date: Wed, 9 Oct 2013 07:20:38 +0000 (-0700) Subject: add more more spec-compiler.jj X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=8d199aee8315cdc8d9649b0707579b6afd082da8 add more more spec-compiler.jj --- diff --git a/grammer/spec-compiler.jj b/grammer/spec-compiler.jj index 9627a89..965e4f5 100644 --- a/grammer/spec-compiler.jj +++ b/grammer/spec-compiler.jj @@ -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" | } - -TOKEN : +SKIP : { - + " " +| + "\n" +| + "\r" | - "#" (~["\n", "\r"])* ["\n", "\r"]> + "\t" | + // Comment for the specification + <"#" (~["\n", "\r"])* (["\n", "\r"])> +} + +TOKEN : +{ | @@ -34,11 +98,26 @@ TOKEN : | | - + +| + +| + +| + +| + | | - + +| + (~["@", "#", "$"])+> +| + )*> +| + +| | | @@ -46,18 +125,114 @@ TOKEN : | | - + | - + | - + + | - - + +| + +| + } void Start() : {} { - + +} + +void Global_construct() : +{} +{ + + + "(" ")" "->" + + +} + +void C_CPP_CODE() : +{} +{ + <(~["@", "#", "$"])+> +} + +void Global_define() : +{} +{ + C_CPP_CODE() +} + +void Conditional_interface() : +{} +{ + (<"(" ")"> | "") +} + +void Interface_cluster() : +{} +{ + "=" "{" Conditional_interface() (",," Conditional_interface())* "}" +} + +void Interface_clusters() : +{} +{ + (Interface_cluster())+ +} + +void Happens_before() : +{} +{ + + + "(" ")" "->" + + +} + +void Interface() : +{} +{ + + + "(" ")" "->" + + +} + +void Potential_commit_point_define() : +{} +{ + + + "(" ")" "->" + + +} + + +void Commit_point_define() : +{} +{ + + + "(" ")" "->" + + +} + + +void Commit_point_define_check() : +{} +{ + + + "(" ")" "->" + + } diff --git a/setup-env.sh b/setup-env.sh index 4946f85..1738ee4 100644 --- a/setup-env.sh +++ b/setup-env.sh @@ -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