more
authorPeizhao Ou <peizhaoo@uci.edu>
Thu, 5 Dec 2013 05:53:03 +0000 (21:53 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Thu, 5 Dec 2013 05:53:03 +0000 (21:53 -0800)
grammer/spec_compiler.jj
src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java
src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java
src/edu/uci/eecs/specCompiler/specExtraction/InterfaceDefineConstruct.java

index 24accc9..cbe2e28 100644 (file)
@@ -30,7 +30,7 @@
        
        b) Interface construct
        @Begin
-       @Interface: ...
+       @Interface_decl: ...
        @Commit_point_set:
                IDENTIFIER | IDENTIFIER ...
        @Condition: ... (Optional)
        @Begin
        @Interface_define: <Interface_Name>
        @End
+
+       g) Interface declare & define construct
+       @Begin
+       @Interface_decl_define: <Interface_Name>
+       @Commit_point_set:
+               IDENTIFIER | IDENTIFIER ...
+       @Condition: ... (Optional)
+       @HB_Condition:
+               IDENTIFIER :: <C_CPP_Condition>
+       @HB_Condition: ...
+       @ID: ... (Optional, use default ID)
+       @Check: (Optional)
+               ...
+       @Action: (Optional)
+               ...
+       @Post_action: (Optional)
+       @Post_check: (Optional)
+       @End
+
 */
 
 
@@ -564,11 +583,13 @@ String ParameterizedName() :
 
 FunctionHeader FuncDecl() :
 {
+       ArrayList<VariableDeclaration> templateList;
        String ret;
        QualifiedName funcName;
        ArrayList<VariableDeclaration> args;
 }
 {
+aa
        (<STATIC> | <INLINE>)*
        ret = Type() 
        funcName = ParseQualifiedName() 
@@ -596,22 +617,31 @@ QualifiedName ParseQualifiedName() :
        }
 }
 
-ArrayList<String> TemplateParamList() :
+ArrayList<VariableDeclaration> TemplateParamList() :
 {
-       ArrayList<String> params;
-       String str;
+       ArrayList<VariableDeclaration> params;
+       String type;
+       String name;
 }
 {
        {
-               params = new ArrayList<String>();
+               params = new ArrayList<VariableDeclaration>();
        }
        <TEMPLATE>
        "<"
-       (str = <IDENTIFIER>.image 
-       str = <IDENTIFIER>.image {params.add(str);})
+       (type = <IDENTIFIER>.image 
+       name = <IDENTIFIER>.image
+       {
+               params.add(new VariableDeclaration(type, name));
+       }
+       )
 
-       ("," str = <IDENTIFIER>.image 
-       str = <IDENTIFIER>.image {params.add(str);})*
+       ("," type = <IDENTIFIER>.image 
+       name = <IDENTIFIER>.image
+       {
+               params.add(new VariableDeclaration(type, name));
+       }
+       )*
        ">"
        {
                //System.out.println(params);
index f98250d..e6dfc1d 100644 (file)
@@ -482,7 +482,6 @@ public class CodeVariables {
                String interfaceName = construct.name;
                // Generate necessary header file (might be redundant but never mind)
                newCode.add(INCLUDE(HEADER_STDLIB));
-               newCode.add(INCLUDE(HEADER_THREADS));
                newCode.add(INCLUDE(HEADER_CDSANNOTATE));
                newCode.add(INCLUDE(HEADER_SPECANNOTATION));
                newCode.add(INCLUDE(HEADER_SPEC_LIB));
@@ -596,6 +595,7 @@ public class CodeVariables {
                return newCode;
        }
 
+       // Rename the interface depending on if it's declaration or definition
        public static void renameInterface(SemanticsChecker semantics,
                        Construct construct) {
                FunctionHeader header = getFunctionHeader(semantics, construct);
index 654e579..d48462a 100644 (file)
@@ -4,6 +4,11 @@ public class Environment {
        public static String HOME_DIRECTORY = System.getProperty("user.dir");
        public static String GENERATED_FILE_DIR = HOME_DIRECTORY + "/" + "output";
        public static String MODEL_CHECKER_HOME_DIR = System
-                       .getProperty("user.home") + "/model-checker-priv";
+                       .getProperty("user.home") + "/test/model-checker-priv";
        public static String MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_HOME_DIR + "/test";
+       
+       public static String MS_QUEUE = MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_TEST_DIR + "/ms-queue";
+       public static String LINUXRWLOCKS = MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_TEST_DIR + "/linuxrwlocks";
+       public static String CLIFFC_HASHTABLE = MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_TEST_DIR + "/cliffc-hashtable";
+                       
 }
index f8e84bc..60f7700 100644 (file)
@@ -3,12 +3,15 @@ package edu.uci.eecs.specCompiler.specExtraction;
 import java.util.ArrayList;
 
 public class FunctionHeader {
+       public final ArrayList<VariableDeclaration> templateList;
+       
        public final String returnType;
        public final QualifiedName qualifiedName;
        public final ArrayList<VariableDeclaration> args;
 
-       public FunctionHeader(String returnType, QualifiedName qualifiedName,
+       public FunctionHeader(ArrayList<VariableDeclaration> templateList, String returnType, QualifiedName qualifiedName,
                        ArrayList<VariableDeclaration> args) {
+               this.templateList = templateList;
                this.returnType = returnType;
                this.qualifiedName = qualifiedName;
                this.args = args;
@@ -29,7 +32,7 @@ public class FunctionHeader {
        public FunctionHeader getRenamedHeader(String prefix) {
                String newFullName = qualifiedName.qualifiedName + prefix + "_"
                                + qualifiedName.bareName;
-               FunctionHeader newHeader = new FunctionHeader(returnType,
+               FunctionHeader newHeader = new FunctionHeader(templateList, returnType,
                                new QualifiedName(newFullName), args);
                return newHeader;
        }
index 8231c18..657b270 100644 (file)
@@ -4,7 +4,6 @@ import java.io.File;
 
 public class InterfaceDefineConstruct extends Construct {
        public final String name;
-       private String funcDecl;
 
        public InterfaceDefineConstruct(File file, int beginLineNum, String name) {
                super(file, beginLineNum);