X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=grammer%2Fspec_compiler.jj;h=2a8c779d07e5e34e34f05c2e6eadefa763b5e097;hp=cbe2e28d6240ab8a6853df36d0c68c7d647ce15a;hb=37a6bc832e220afbfb100848da62fb1b2123af63;hpb=541ee814ad10bc181abd4d8825397249c6f86ad7 diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj index cbe2e28..2a8c779 100644 --- a/grammer/spec_compiler.jj +++ b/grammer/spec_compiler.jj @@ -9,90 +9,52 @@ 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: - @DeclareStruct: - @DeclareVar: - @InitVar: - @DefineFunc: - ... - @DefineFunc: - @Interface_cluster: - ... - @Happens-before: - ... - @End + @DeclareState: C/C++ variable declaration; // Declare the state structure + @InitState: C/C++ statements; // Specify how to initialize the state + @CopyState: // A function on how to copy an existing state (Not sure if we + // need this because we might be able to auto this + @Commutativity: Method1 <-> Method2 (Guard) // Admissibility condition. + // Allow specify 0-many rules b) Interface construct - @Begin - @Interface_decl: ... - @Commit_point_set: - IDENTIFIER | IDENTIFIER ... - @Condition: ... (Optional) - @HB_Condition: - IDENTIFIER :: - @HB_Condition: ... - @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 - - e) Entry point construct - @Begin - @Entry_point - @End - - f) Interface define construct - @Begin - @Interface_define: - @End - - g) Interface declare & define construct - @Begin - @Interface_decl_define: - @Commit_point_set: - IDENTIFIER | IDENTIFIER ... - @Condition: ... (Optional) - @HB_Condition: - IDENTIFIER :: - @HB_Condition: ... - @ID: ... (Optional, use default ID) - @Check: (Optional) - ... - @Action: (Optional) - ... - @Post_action: (Optional) - @Post_check: (Optional) - @End + @Interface: InterfaceName // Required; a label to represent the interface + @LocalState: // Optional; to calculate the accumulative local state before this + // method call in a customized fashion. If not specified here, the + // local state would be default, which is the result of the + // execution on the subset of method calls in the sequential order + @PreCondition: // Optional; checking code + @LocalSideEffect: // Optional; to calculate the side effect this method call + // have on the local state in a customized fashion. If this + // field is not stated, it means we don't care about it. + @SideEffect: // Optional; to calculate the side effect on the global state. When + // the "@LocalSideEffect" specification is ommitted, we also impose the + // same side effect on the set of method calls that happen before this + // method call in the sequential order. + @PostCondition: // Optional; checking code + + + c) Ordering point construct + @OPDefine: condition // If the specified condition satisfied, the atomic + // operation right before is an ordering point + + @PotentialOP(Label): condition // If the specified condition satisfied, the + // atomic operation right before is a potential + // ordering point, and we label it with a tag + + @OPCheck(Label): condition // If the specified condition satisfied, the + // potential ordering point defined earlier with the + // same tag becomes an ordering point + + @OPClear: condition // If the specified condition satisfied, all the + // ordering points and potential ordering points will be + // cleared + + @OPClearDefine: condition // If the specified condition satisfied, all the + // ordering points and potential ordering points will + // be cleared, and the atomic operation right before + // becomes an ordering point. This is a syntax sugar + // as the combination of an "OPClear" and "OPDefine" + // statement */ @@ -114,13 +76,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 +106,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 content = new ArrayList(); ArrayList constructs = new ArrayList(); ArrayList headers = new ArrayList(); @@ -156,9 +121,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,7 +146,14 @@ import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration; return null; } - public static ArrayList getTemplateArg(String line) + + private static ArrayList breakLines(String all) { + String lines[] = all.split("[\\r\\n]+"); + return new ArrayList(Arrays.asList(lines)); + } + + + public static ArrayList getTemplateArg(String line) throws ParseException { InputStream input = new ByteArrayInputStream(line.getBytes()); SpecParser parser = new SpecParser(input); @@ -206,12 +178,61 @@ import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration; return sb.toString(); } + /** + boolean spaceSeparator(Token t) { + switch (t.image) { + case "[": + case "]": + case "=": + case "(": + case ")": + case ",": + case ".": + case "*": + case "~": + case "!": + case "&": + case "|": + case "%": + case "+": + case "-": + case "/": + case "<": + case ">": + case "<=": + case ">=": + case "==": + case "!=": + case "&&": + case "||": + case "^": + case "?": + case ":": + case "::": + case "<<": + case ">>": + case ">>>": + case "+=": + case "-=": + case "*=": + case "/=": + case "%=": + case "^=": + case "&=": + case ";": + return false; + default: + return true; + } + } + */ + } PARSER_END(SpecParser) -<*> SKIP : + SKIP : { " " | @@ -240,6 +261,10 @@ SKIP : { "/*": IN_COMMENT } + TOKEN: { + +} + <*> SKIP : { // "//" comment for the specification <"//" (~["\n", "\r"])* (["\n", "\r"])> @@ -270,12 +295,16 @@ SKIP : { | +| + | | | +| + | | @@ -306,18 +335,28 @@ SKIP : { | +| + | | +| + | +| + +| + | +| + } - TOKEN : + TOKEN : { /* Specification & C/C++ shared tokens */ // Reserved keywords @@ -334,6 +373,8 @@ SKIP : { | +| + | <#DIGIT: ["0"-"9"]> | @@ -358,11 +399,15 @@ SKIP : { | "> +| + "> | | /* C/C++ only token*/ +| + | | @@ -433,7 +478,6 @@ SKIP : { | @@ -510,7 +554,7 @@ String Type() : } { { type = ""; } - ("const" + ( { type = "const"; } )? (((str = .image | str = .image | str = .image) { type = type + " " + str; })? @@ -522,7 +566,7 @@ String Type() : type = name.fullName; }) ) - ((str = "const".image { + ((str = .image { if (!type.equals("")) type = type + " " + str; else @@ -546,24 +590,6 @@ String Type() : } } -void Test() : -{ - String str; - FunctionHeader func; -} -{ - /* - str = Type() - { - System.out.println(str); - } - */ - func = FuncDecl() - { - System.out.println(func); - } - -} String ParameterizedName() : { @@ -572,8 +598,8 @@ String ParameterizedName() : } { (str = .image {res = str;}) - ("<" str = Type() { res = res + "<" + str; } - ("," str = Type() { res = res + ", " + str; })* ">" + ( str = Type() { res = res + "<" + str; } + ( str = Type() { res = res + ", " + str; })* { res = res + ">"; } )? { @@ -583,13 +609,11 @@ String ParameterizedName() : FunctionHeader FuncDecl() : { - ArrayList templateList; String ret; QualifiedName funcName; ArrayList args; } { -aa ( | )* ret = Type() funcName = ParseQualifiedName() @@ -628,7 +652,7 @@ ArrayList TemplateParamList() : params = new ArrayList(); }