projects / cdsspec-compiler.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: efe3f6d)
more changes
authorPeizhao Ou <peizhaoo@uci.edu>
Sat, 19 Oct 2013 00:39:36 +0000 (17:39 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Sat, 19 Oct 2013 00:39:36 +0000 (17:39 -0700)
grammer/spec-compiler.jj patch | blob | history
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java patch | blob | history
src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java patch | blob | history
src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java patch | blob | history
src/edu/uci/eecs/specCompiler/specExtraction/SpecConstruct.java patch | blob | history
test.c patch | blob | history
test.cc [deleted file] patch | blob | history
test.h patch | blob | history

diff --git a/grammer/spec-compiler.jj b/grammer/spec-compiler.jj
index 67769868dcf93af2a1cd16844c68a0b73a71ee31..e4f723f64f99d828bc615ef9a08e45bca4e3ce48 100644 (file)
--- a/grammer/spec-compiler.jj
+++ b/grammer/spec-compiler.jj
@@ -10,6 +10,11 @@
        
        a) Global construct
        @Begin
        
        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:
                @DeclareVar:
                @InitVar:
        @Global_define:
                @DeclareVar:
                @InitVar:
@@ -60,6 +65,16 @@
        @Potential_commit_point_label: ...
        @Label: ...
        @End
        @Potential_commit_point_label: ...
        @Label: ...
        @End
+
+       e) Entry point construct
+       @Begin
+       @Entry_point
+       @End
+
+       f) Interface define construct
+       @Begin
+       @Interface_define: <Interface_Name>
+       @End
 */
 
 
 */
 
 
@@ -90,6 +105,8 @@ import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
 import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
 
        public class SpecParser {
                public static void main(String[] argvs)
 
        public class SpecParser {
                public static void main(String[] argvs)
@@ -144,6 +161,8 @@ TOKEN :
        <BEGIN: "@Begin">
 |
        <END: "@End">
        <BEGIN: "@Begin">
 |
        <END: "@End">
+|
+       <OPTIONS: "@Options:">
 |
        <GLOBAL_DEFINE: "@Global_define:">
 |
 |
        <GLOBAL_DEFINE: "@Global_define:">
 |
@@ -160,6 +179,10 @@ TOKEN :
        <INTERFACE: "@Interface:">
 |
        <COMMIT_POINT_SET: "@Commit_point_set:">
        <INTERFACE: "@Interface:">
 |
        <COMMIT_POINT_SET: "@Commit_point_set:">
+|
+       <ENTRY_POINT: "@Entry_point">
+|
+       <INTERFACE_DEFINE: "@Interface_define:">
 |
        <CONDITION: "@Condition:">
 |
 |
        <CONDITION: "@Condition:">
 |
@@ -332,7 +355,9 @@ Construct Parse() :
        LOOKAHEAD(3) res = Interface() |
        LOOKAHEAD(3) res = Potential_commit_point_define() |
        LOOKAHEAD(3) res = Commit_point_define() |
        LOOKAHEAD(3) res = Interface() |
        LOOKAHEAD(3) res = Potential_commit_point_define() |
        LOOKAHEAD(3) res = Commit_point_define() |
-       LOOKAHEAD(3) res = Commit_point_define_check()
+       LOOKAHEAD(3) res = Commit_point_define_check() |
+       LOOKAHEAD(3) res = Entry_point() |
+       LOOKAHEAD(3) res = Interface_define()
        )
        <EOF>
        {
        )
        <EOF>
        {
@@ -345,13 +370,31 @@ GlobalConstruct Global_construct() :
 {
        GlobalConstruct res;
        SequentialDefineSubConstruct code;
 {
        GlobalConstruct res;
        SequentialDefineSubConstruct code;
+       HashMap<String, String> options;
+       String key, value;
 }
 {
 }
 {
-       { res = null; }
+       {
+               res = null;
+               options = new HashMap<String, String>();
+       }
        <HEAD>
                <BEGIN> 
        <HEAD>
                <BEGIN> 
+                       (<OPTIONS>
+                               ((key = <IDENTIFIER>.image)
+                               <EQUALS>
+                               (value = <IDENTIFIER>.image)
+                               {
+                                       if (options.containsKey(key)) {
+                                               throw new ParseException("Duplicate options!");
+                                       }
+                                       options.put(key, value);
+                               }
+                               <SEMI_COLON>
+                               )*
+                       )?
                        (code = Global_define())
                        (code = Global_define())
-                       { res = new GlobalConstruct(code); }
+                       { res = new GlobalConstruct(code, options); }
                        (Interface_clusters(res))?
                        (Happens_before(res))?
                <END>
                        (Interface_clusters(res))?
                        (Happens_before(res))?
                <END>
@@ -410,8 +453,8 @@ SequentialDefineSubConstruct Global_define() :
                initVar = "";
                defineFunc = "";
        }
                initVar = "";
                defineFunc = "";
        }
-       <GLOBAL_DEFINE> 
-       (<DECLARE_VAR> (declareVar = C_CPP_CODE()))?
+       <GLOBAL_DEFINE>
+               (<DECLARE_VAR> (declareVar = C_CPP_CODE()))?
        (<INIT_VAR> (initVar = C_CPP_CODE()))?
        (<DEFINE_FUNC> (defineFunc = C_CPP_CODE()))?
        {
        (<INIT_VAR> (initVar = C_CPP_CODE()))?
        (<DEFINE_FUNC> (defineFunc = C_CPP_CODE()))?
        {
@@ -630,3 +673,34 @@ CPDefineCheckConstruct Commit_point_define_check() :
                return res;
        }
 }
                return res;
        }
 }
+
+EntryPointConstruct Entry_point() :
+{}
+{
+
+       <HEAD> 
+               <BEGIN> 
+                       <ENTRY_POINT>
+               <END>
+       <TAIL>
+       {
+               return new EntryPointConstruct();
+       }
+}
+
+InterfaceDefineConstruct Interface_define() :
+{
+       String name;    
+}
+{
+       <HEAD>
+               <BEGIN>
+                       <INTERFACE_DEFINE> (name = <IDENTIFIER>.image)
+               <END>
+       <TAIL>
+       {
+               return new InterfaceDefineConstruct(name);
+       }
+}
+
+
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 8f4537a43a6b33a39d65be969978e3a660be00c8..05a76a79e8d113534e5f956b498ff8084bb61f37 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -12,6 +12,7 @@ import java.util.Iterator;
 import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
 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.Construct;
 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
@@ -97,21 +98,20 @@ public class CodeGenerator {
                GlobalConstruct construct = (GlobalConstruct) inst.construct;
                ArrayList<String> newCode = new ArrayList<String>();
 
                GlobalConstruct construct = (GlobalConstruct) inst.construct;
                ArrayList<String> newCode = new ArrayList<String>();
 
-               // Generate the inner class definition
-               newCode.add("class " + CodeVariables.SPEC_CLASS + " {\n");
-               newCode.add("public:\n");
+               // Generate all sequential variables into a struct
+               newCode.add("struct " + CodeVariables.SPEC_STRUCT + " {\n");
 
                // Generate the code in global construct first
                SequentialDefineSubConstruct globalCode = construct.code;
                breakCodeLines(newCode, globalCode.declareVar);
 
                // Generate code from the DefineVar, __COND_SAT__ and __ID__
 
                // Generate the code in global construct first
                SequentialDefineSubConstruct globalCode = construct.code;
                breakCodeLines(newCode, globalCode.declareVar);
 
                // Generate code from the DefineVar, __COND_SAT__ and __ID__
+               // The hashtable in the contract can only contains pointers or integers
                // __COND_SAT__
                // __COND_SAT__
-               newCode.add(CodeVariables.SPEC_HASHTABLE + "<" + CodeVariables.BOOLEAN
-                               + "> " + CodeVariables.SPEC_CONDITION + ";");
+               newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_CONDITION
+                               + ";");
                // __ID__
                // __ID__
-               newCode.add(CodeVariables.SPEC_HASHTABLE + "<" + CodeVariables.SPEC_TAG
-                               + "> " + CodeVariables.SPEC_ID + ";");
+               newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_ID + ";");
 
                // DefineVars
                for (String interfaceName : _semantics.interfaceName2Construct.keySet()) {
 
                // DefineVars
                for (String interfaceName : _semantics.interfaceName2Construct.keySet()) {
@@ -120,58 +120,46 @@ public class CodeGenerator {
                        ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
                        for (int i = 0; i < defineVars.size(); i++) {
                                DefineVar var = defineVars.get(i);
                        ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
                        for (int i = 0; i < defineVars.size(); i++) {
                                DefineVar var = defineVars.get(i);
-                               newCode.add(CodeVariables.SPEC_HASHTABLE + "<" + var.varType
-                                               + "> " + var.getNewVarName() + ";");
+                               newCode.add(CodeVariables.SPEC_HASHTABLE + var.getNewVarName()
+                                               + ";");
                        }
                }
 
                        }
                }
 
-               // Enum of all interface
-               String enumDefinition = "enum " + CodeVariables.SPEC_INTERFACE_ENUM
-                               + " {";
-               Iterator<String> iter = _semantics.interfaceName2Construct.keySet()
-                               .iterator();
-               String interfaceName;
-               if (iter.hasNext()) {
-                       interfaceName = iter.next();
-                       enumDefinition = enumDefinition + "_" + interfaceName + "_";
-               }
-               while (iter.hasNext()) {
-                       interfaceName = iter.next();
-                       enumDefinition = enumDefinition + ", _" + interfaceName + "_";
-               }
-               enumDefinition = enumDefinition + "};";
-               newCode.add(enumDefinition);
-
                // __interface
                // __interface
-               newCode.add(CodeVariables.SPEC_HASHTABLE + "<enum "
-                               + CodeVariables.SPEC_INTERFACE_ENUM + "> "
-                               + CodeVariables.SPEC_INTERFACE + ";");
+               newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_INTERFACE
+                               + ";");
 
 
-               // Generate constructor (the place to initialize everything!)
-               newCode.add("\n");
-               newCode.add(CodeVariables.SPEC_CLASS + "() {");
+               // End of the struct
+               newCode.add("}");
 
 
+               // FIXME: Constructor should be modified and put in the right place
+               // Generate constructor (the place to initialize everything!)
                breakCodeLines(newCode, globalCode.initVar);
                // __COND_SAT__
                breakCodeLines(newCode, globalCode.initVar);
                // __COND_SAT__
-               newCode.add(CodeVariables.SPEC_CONDITION + " = "
-                               + CodeVariables.SPEC_HASHTABLE + "<" + CodeVariables.BOOLEAN
-                               + ">();");
+               newCode.add("init_table(&" + CodeVariables.SPEC_CONDITION + ");");
                // __ID__
                // __ID__
-               newCode.add(CodeVariables.SPEC_ID + " = "
-                               + CodeVariables.SPEC_HASHTABLE + "<" + CodeVariables.SPEC_TAG
-                               + ">();");
+               newCode.add("init_table(&" + CodeVariables.SPEC_ID + ");");
+               // DefineVars
+               for (String interfaceName : _semantics.interfaceName2Construct.keySet()) {
+                       InterfaceConstruct iConstruct = (InterfaceConstruct) _semantics.interfaceName2Construct
+                                       .get(interfaceName).construct;
+                       ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
+                       for (int i = 0; i < defineVars.size(); i++) {
+                               DefineVar var = defineVars.get(i);
+                               newCode.add("init_table(&" + var.getNewVarName() + ");");
+                       }
+               }
                // __interface
                // __interface
-               newCode.add(CodeVariables.SPEC_INTERFACE + " = "
-                               + CodeVariables.SPEC_HASHTABLE + "<enum "
-                               + CodeVariables.SPEC_INTERFACE_ENUM + ">();");
-               // FIXME: Pass the happens-before relationship check here
-               newCode.add("}");
+               newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE + ");");
+
+               // Pass the happens-before relationship check here
+               newCode.addAll(CodeVariables.generateHBInitAnnotation(_semantics));
 
 
+               newCode.add("\n");
+               
                // Generate the sequential functions
                breakCodeLines(newCode, globalCode.defineFunc);
 
                // Generate the sequential functions
                breakCodeLines(newCode, globalCode.defineFunc);
 
-               // Generate the end of the inner class definition
-               newCode.add("};\n");
                printCode(newCode);
 
                CodeAddition addition = new CodeAddition(lineNum, newCode);
                printCode(newCode);
 
                CodeAddition addition = new CodeAddition(lineNum, newCode);
@@ -209,18 +197,27 @@ public class CodeGenerator {
 
                // Rename the interface name
                File file = inst.file;
 
                // Rename the interface name
                File file = inst.file;
-               ArrayList<String> content = contents.get(file);
                String funcDecl = inst.interfaceDeclBody;
                String funcDecl = inst.interfaceDeclBody;
-               String funcName = renameInterface(funcDecl, content, lineNum);
+               // Rename the function declaration
+               String funcName = renameInterface(inst);
+               // Also rename the function definition if it's separated from the
+               // declaration
+               SpecConstruct definition = _semantics.interfaceName2DefineConstruct
+                               .get(construct.name);
+               if (definition != null) {
+                       String funcDefintionName = renameInterface(definition);
+                       assert (funcDefintionName.equals(funcName));
+               }
 
                // Generate new wrapper
                breakCodeLines(newCode, funcDecl);
 
                // Generate new wrapper
                breakCodeLines(newCode, funcDecl);
+
                newCode.add("{");
                newCode.add("{");
-               
-               // Generate 
-               
+
+               // Generate
+
                // FIXME: Add Happens-before check here
                // FIXME: Add Happens-before check here
-               
+
                newCode.add("}");
                CodeAddition addition = new CodeAddition(lineNum, newCode);
                if (!codeAdditions.containsKey(inst.file)) {
                newCode.add("}");
                CodeAddition addition = new CodeAddition(lineNum, newCode);
                if (!codeAdditions.containsKey(inst.file)) {
@@ -230,8 +227,13 @@ public class CodeGenerator {
        }
 
        // Returns the function name that has been renamed and replace the old line
        }
 
        // Returns the function name that has been renamed and replace the old line
-       private String renameInterface(String funcDecl, ArrayList<String> content,
-                       int lineNum) throws InterfaceWrongFormatException {
+       private String renameInterface(SpecConstruct inst)
+                       throws InterfaceWrongFormatException {
+               String funcDecl = inst.interfaceDeclBody;
+               ArrayList<String> content = contents.get(inst.file);
+
+               // Depending on "(" to find the function name, so it doesn't matter if
+               // there's any template
                int begin = 0, end = funcDecl.indexOf('(');
                if (end == -1) {
                        throw new InterfaceWrongFormatException(funcDecl
                int begin = 0, end = funcDecl.indexOf('(');
                if (end == -1) {
                        throw new InterfaceWrongFormatException(funcDecl
@@ -240,24 +242,31 @@ public class CodeGenerator {
                end--;
                while (end > 0) {
                        char ch = funcDecl.charAt(end);
                end--;
                while (end > 0) {
                        char ch = funcDecl.charAt(end);
-                       if (ch == '\n' || ch == '\t' || ch == ' ')
-                               continue;
+                       if (ch == '_' || (ch >= 'a' && ch <= 'z')
+                                       || (ch >= 'A' && ch <= 'Z') || (ch >= '0' && ch <= '9')) {
+                               break;
+                       }
+                       end--;
                }
                begin = end;
                while (begin > 0) {
                        char ch = funcDecl.charAt(begin);
                        if (ch == '_' || (ch >= 'a' && ch <= 'z')
                                        || (ch >= 'A' && ch <= 'Z') || (ch >= '0' && ch <= '9')) {
                }
                begin = end;
                while (begin > 0) {
                        char ch = funcDecl.charAt(begin);
                        if (ch == '_' || (ch >= 'a' && ch <= 'z')
                                        || (ch >= 'A' && ch <= 'Z') || (ch >= '0' && ch <= '9')) {
+                               begin--;
                                continue;
                        }
                                continue;
                        }
+                       break;
                }
                String funcName = funcDecl.substring(begin + 1, end + 1), newLine;
                int lineBreakIdx = funcDecl.indexOf('\n');
                }
                String funcName = funcDecl.substring(begin + 1, end + 1), newLine;
                int lineBreakIdx = funcDecl.indexOf('\n');
-               int firstLineBreak = lineBreakIdx == -1 ? funcDecl.length() : lineBreakIdx;  
+               int firstLineBreak = lineBreakIdx == -1 ? funcDecl.length()
+                               : lineBreakIdx;
                newLine = funcDecl.substring(0, begin + 1)
                                + CodeVariables.SPEC_INTERFACE_WRAPPER + funcName
                                + funcDecl.substring(end + 1, firstLineBreak);
                newLine = funcDecl.substring(0, begin + 1)
                                + CodeVariables.SPEC_INTERFACE_WRAPPER + funcName
                                + funcDecl.substring(end + 1, firstLineBreak);
-               content.set(lineNum, newLine);
+               // Be careful: lineNum - 1 -> index of content array
+               content.set(inst.endLineNum, newLine);
                return funcName;
        }
 
                return funcName;
        }
 
@@ -310,11 +319,11 @@ public class CodeGenerator {
                                        e.printStackTrace();
                                }
                        } else if (construct instanceof PotentialCPDefineConstruct) {
                                        e.printStackTrace();
                                }
                        } else if (construct instanceof PotentialCPDefineConstruct) {
-                               potentialCP2Code(inst);
+                               // potentialCP2Code(inst);
                        } else if (construct instanceof CPDefineConstruct) {
                        } else if (construct instanceof CPDefineConstruct) {
-                               CPDefine2Code(inst);
+                               // CPDefine2Code(inst);
                        } else if (construct instanceof CPDefineCheckConstruct) {
                        } else if (construct instanceof CPDefineCheckConstruct) {
-                               CPDefineCheck2Code(inst);
+                               // CPDefineCheck2Code(inst);
                        }
                }
        }
                        }
                }
        }
@@ -322,11 +331,12 @@ public class CodeGenerator {
        public static void main(String[] argvs) {
                String homeDir = Environment.HOME_DIRECTORY;
                File[] srcFiles = {
        public static void main(String[] argvs) {
                String homeDir = Environment.HOME_DIRECTORY;
                File[] srcFiles = {
-               // new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c"),
-               new File(homeDir
-                               + "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
-               // new File(homeDir + "/benchmark/ms-queue/my_queue.c")
-               };
+                               // new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c"),
+                               // new File(homeDir
+                               // +
+                               // "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
+                               new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
+                               new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
                CodeGenerator gen = new CodeGenerator(srcFiles);
                gen.generateCode();
        }
                CodeGenerator gen = new CodeGenerator(srcFiles);
                gen.generateCode();
        }
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index 301cd1239d3232aabbcf8f65250c6d692d8c4de9..7e424e34bd0d5ccc9fa5d986d7a344fd6de2f954 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -1,29 +1,81 @@
 package edu.uci.eecs.specCompiler.codeGenerator;
 
 package edu.uci.eecs.specCompiler.codeGenerator;
 
+import java.util.ArrayList;
+
+import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
+
 public class CodeVariables {
        // C++ code or library
        public static final String ThreadIDType = "thread_id_t";
        public static final String BOOLEAN = "bool";
 public class CodeVariables {
        // C++ code or library
        public static final String ThreadIDType = "thread_id_t";
        public static final String BOOLEAN = "bool";
-       
+
+       // Model checker code
+       public static final String HEADER_CDSAnnotate = "cdsannotate.h";
+       public static final String CDSAnnotate = "cdsannotate";
+       public static final String CDSAnnotateType = "SPEC_ANALYSIS";
+
+       public static final String SPEC_ANNOTATION_TYPE = "spec_anno_type";
+       public static final String SPEC_ANNOTATION = "spec_annotation";
+
+       public static final String ANNO_HB_INIT = "anno_hb_init";
+       public static final String ANNO_INTERFACE_BEGIN = "anno_interface_begin";
+       public static final String ANNO_INTERFACE_END = "anno_interface_end";
+       public static final String ANNO_ID = "anno_id";
+       public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potentail_cp_define";
+       public static final String ANNO_CP_DEFINE = "anno_cp_define";
+       public static final String ANNO_CP_DEFINE_CHECK = "anno_cp_define_check";
+       public static final String ANNO_HB_CONDITION = "anno_hb_condition";
+       public static final String ANNO_POST_CHECK = "anno_post_check";
+
        // Specification variables
        // Specification variables
-       public static final String SPEC_CLASS = "Sequential";
+       public static final String SPEC_STRUCT = "Sequential";
        public static final String SPEC_INSTANCE = "__sequential";
        public static final String SPEC_INSTANCE = "__sequential";
+
        public static final String SPEC_CONDITION = "__cond";
        public static final String SPEC_ID = "__id";
        public static final String SPEC_CONDITION = "__cond";
        public static final String SPEC_ID = "__id";
-       public static final String SPEC_INTERFACE_ENUM = "_interface_t";
        public static final String SPEC_INTERFACE = "__interface";
        public static final String SPEC_INTERFACE = "__interface";
-       
+
        public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_";
        public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_";
-       
+
        // Specification library
        public static final String SPEC_QUEUE = "spec_queue";
        public static final String SPEC_STACK = "spec_stack";
        public static final String SPEC_HASHTABLE = "spec_hashtable";
        public static final String SPEC_TAG = "spec_tag";
        // Specification library
        public static final String SPEC_QUEUE = "spec_queue";
        public static final String SPEC_STACK = "spec_stack";
        public static final String SPEC_HASHTABLE = "spec_hashtable";
        public static final String SPEC_TAG = "spec_tag";
-       
+
        // Macro
        public static final String MACRO_ID = "__ID__";
        public static final String MACRO_COND = "__COND_SAT__";
        public static final String MACRO_RETURN = "__RET__";
        // Macro
        public static final String MACRO_ID = "__ID__";
        public static final String MACRO_COND = "__COND_SAT__";
        public static final String MACRO_RETURN = "__RET__";
-       
+
+       public static ArrayList<String> generateHBInitAnnotation(
+                       SemanticsChecker semantics) {
+               ArrayList<String> newCode = new ArrayList<String>();
+               int hbConditionInitIdx = 0;
+               for (ConditionalInterface left : semantics.getHBConditions().keySet()) {
+                       for (ConditionalInterface right : semantics.getHBConditions().get(
+                                       left)) {
+                               String structVarName = "hbConditionInit" + hbConditionInitIdx;
+                               hbConditionInitIdx++;
+                               int interfaceNumBefore = semantics.interface2Num
+                                               .get(left.interfaceName), hbLabelNumBefore = semantics.hbLabel2Num
+                                               .get(left.hbConditionLabel), interfaceNumAfter = semantics.interface2Num
+                                               .get(right.interfaceName), hbLabelNumAfter = semantics.hbLabel2Num
+                                               .get(right.hbConditionLabel);
+                               newCode.add(ANNO_HB_INIT + " " + structVarName + ";");
+
+                               newCode.add(structVarName + "." + "interface_num_before"
+                                               + " = " + interfaceNumBefore + ";");
+                               newCode.add(structVarName + "." + "hb_condition_num_before"
+                                               + " = " + hbLabelNumBefore + ";");
+                               newCode.add(structVarName + "." + "interface_num_after" + " = "
+                                               + interfaceNumAfter + ";");
+                               newCode.add(structVarName + "." + "hb_condition_num_after"
+                                               + " = " + hbLabelNumAfter + ";");
+                               
+                               newCode.add(CDSAnnotate + "(" + CDSAnnotateType + ", &" + structVarName + ");");
+                       }
+               }
+               return newCode;
+       }
 }
 }
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
index 3bd801ce1a323f2b526ce102aecb07df4e80b505..9eca53be2923dd8b70c284c3f03128aab4b00cd4 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
@@ -9,8 +9,10 @@ import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
 import edu.uci.eecs.specCompiler.specExtraction.Construct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
 import edu.uci.eecs.specCompiler.specExtraction.Construct;
+import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct;
 
 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct;
 
@@ -19,27 +21,60 @@ public class SemanticsChecker {
        public final HashMap<String, SpecConstruct> CPLabel2Construct;
        public final HashMap<String, SpecConstruct> potentialCPLabel2Construct;
        public final HashMap<String, SpecConstruct> interfaceName2Construct;
        public final HashMap<String, SpecConstruct> CPLabel2Construct;
        public final HashMap<String, SpecConstruct> potentialCPLabel2Construct;
        public final HashMap<String, SpecConstruct> interfaceName2Construct;
+       public final HashMap<String, SpecConstruct> interfaceName2DefineConstruct;
        public final HashMap<String, ArrayList<InterfaceConstruct>> CPLabel2InterfaceConstruct;
        public final HashSet<DefineVar> defineVars;
        public final HashMap<String, ArrayList<InterfaceConstruct>> CPLabel2InterfaceConstruct;
        public final HashSet<DefineVar> defineVars;
+       
+       public final HashMap<String, Integer> interface2Num;
+       public final HashMap<String, Integer> hbLabel2Num;
+       public final HashMap<String, Integer> commitPointLabel2Num;
+
+       private HashMap<String, String> options;
+       private HashMap<ConditionalInterface, HashSet<ConditionalInterface>> hbConditions;
+       private SpecConstruct entryPointConstruct;
+       
+       private int _interfaceNum;
+       private int _hbLabelNum;
+       private int _commitPointNum;    
 
        public SemanticsChecker(ArrayList<SpecConstruct> constructs) {
                this.constructs = constructs;
                this.CPLabel2Construct = new HashMap<String, SpecConstruct>();
                this.potentialCPLabel2Construct = new HashMap<String, SpecConstruct>();
                this.interfaceName2Construct = new HashMap<String, SpecConstruct>();
 
        public SemanticsChecker(ArrayList<SpecConstruct> constructs) {
                this.constructs = constructs;
                this.CPLabel2Construct = new HashMap<String, SpecConstruct>();
                this.potentialCPLabel2Construct = new HashMap<String, SpecConstruct>();
                this.interfaceName2Construct = new HashMap<String, SpecConstruct>();
+               this.interfaceName2DefineConstruct = new HashMap<String, SpecConstruct>();
                this.CPLabel2InterfaceConstruct = new HashMap<String, ArrayList<InterfaceConstruct>>();
                this.defineVars = new HashSet<DefineVar>();
                this.CPLabel2InterfaceConstruct = new HashMap<String, ArrayList<InterfaceConstruct>>();
                this.defineVars = new HashSet<DefineVar>();
+               this.entryPointConstruct = null;
+               
+               this.interface2Num = new HashMap<String, Integer>();
+               this.hbLabel2Num = new HashMap<String, Integer>();
+               // Immediately init the true HB-condition to be 0
+               hbLabel2Num.put("", 0);
+               
+               this.commitPointLabel2Num = new HashMap<String, Integer>();
+               
+               _interfaceNum = 0;
+               _hbLabelNum = 0;
+               _commitPointNum = 0;
+       }
+
+       public HashMap<ConditionalInterface, HashSet<ConditionalInterface>> getHBConditions() {
+               return this.hbConditions;
+       }
+
+       public String getOption(String key) {
+               return options.get(key);
        }
 
        private void checkHBLabelConsistency(ConditionalInterface inst)
                        throws SemanticsCheckerException {
        }
 
        private void checkHBLabelConsistency(ConditionalInterface inst)
                        throws SemanticsCheckerException {
-               String interfaceName = inst.interfaceName,
-                               label = inst.hbConditionLabel;
+               String interfaceName = inst.interfaceName, label = inst.hbConditionLabel;
                if (!interfaceName2Construct.containsKey(interfaceName)) {
                        throw new SemanticsCheckerException(
                                        "In global construct, no interface \"" + interfaceName
                                                        + "\"!");
                if (!interfaceName2Construct.containsKey(interfaceName)) {
                        throw new SemanticsCheckerException(
                                        "In global construct, no interface \"" + interfaceName
                                                        + "\"!");
-               } else if (!label.equals("")){
+               } else if (!label.equals("")) {
                        InterfaceConstruct iConstruct = (InterfaceConstruct) interfaceName2Construct
                                        .get(interfaceName).construct;
                        if (!iConstruct.hbConditions.containsKey(label)) {
                        InterfaceConstruct iConstruct = (InterfaceConstruct) interfaceName2Construct
                                        .get(interfaceName).construct;
                        if (!iConstruct.hbConditions.containsKey(label)) {
@@ -47,17 +82,46 @@ public class SemanticsChecker {
                                                + interfaceName + " doesn't contain HB_codition: "
                                                + label + "!");
                        }
                                                + interfaceName + " doesn't contain HB_codition: "
                                                + label + "!");
                        }
-               }
+                       
+                       // No HB condition label can duplicate!
+                       if (hbLabel2Num.containsKey(label)) {
+                               throw new SemanticsCheckerException("Happens-before label: "
+                                               + label + " duplicates!");
+                       }
+                       
+                       // Number the HB-condition label
+                       hbLabel2Num.put(label, _hbLabelNum++);
+               }       
        }
 
        private void checkLabelDuplication(Construct construct, String label)
                        throws SemanticsCheckerException {
        }
 
        private void checkLabelDuplication(Construct construct, String label)
                        throws SemanticsCheckerException {
-               if (potentialCPLabel2Construct.containsKey(label) ||
-                               CPLabel2Construct.containsKey(label))
+               if (potentialCPLabel2Construct.containsKey(label)
+                               || CPLabel2Construct.containsKey(label))
                        throw new SemanticsCheckerException("In construct: " + construct
                                        + "\"" + label + "\" has duplication.");
        }
 
                        throw new SemanticsCheckerException("In construct: " + construct
                                        + "\"" + label + "\" has duplication.");
        }
 
+       private void checkOptions() throws SemanticsCheckerException {
+               // FIXME: We don't have any check here
+       }
+
+       private void postCheck() throws SemanticsCheckerException {
+               // This is a C program, must provide the entry point
+               if (getOption("LANG").equals("C") && entryPointConstruct == null) {
+                       throw new SemanticsCheckerException(
+                                       "C program must provide the entry point!");
+               }
+
+               // Check if interface define construct labels are correct
+               for (String name : interfaceName2DefineConstruct.keySet()) {
+                       if (!interfaceName2Construct.containsKey(name)) {
+                               throw new SemanticsCheckerException(
+                                               "Label \"" + name + "\" does not have interface declaration!");
+                       }
+               }
+       }
+
        public void check() throws SemanticsCheckerException {
                boolean hasGlobalConstruct = false;
                // First grab the information from the interface
        public void check() throws SemanticsCheckerException {
                boolean hasGlobalConstruct = false;
                // First grab the information from the interface
@@ -65,16 +129,25 @@ public class SemanticsChecker {
                        Construct inst = constructs.get(i).construct;
                        if (inst instanceof InterfaceConstruct) {
                                InterfaceConstruct iConstruct = (InterfaceConstruct) inst;
                        Construct inst = constructs.get(i).construct;
                        if (inst instanceof InterfaceConstruct) {
                                InterfaceConstruct iConstruct = (InterfaceConstruct) inst;
+                               if (interfaceName2Construct.containsKey(iConstruct.name)) {
+                                       throw new SemanticsCheckerException("Interface name: "
+                                                       + iConstruct.name + " duplicates!");
+                               }
+                               // Number the interface label
+                               interface2Num.put(iConstruct.name, _interfaceNum++);
+                               
                                interfaceName2Construct.put(iConstruct.name, constructs.get(i));
                                for (int j = 0; j < iConstruct.action.defineVars.size(); j++) {
                                        DefineVar var = iConstruct.action.defineVars.get(j);
                                interfaceName2Construct.put(iConstruct.name, constructs.get(i));
                                for (int j = 0; j < iConstruct.action.defineVars.size(); j++) {
                                        DefineVar var = iConstruct.action.defineVars.get(j);
-                                       var.renameVarName("__" + iConstruct.name + "_" + var.varName + "__");
+                                       var.renameVarName("__" + iConstruct.name + "_"
+                                                       + var.varName + "__");
                                }
                                }
-                               
+
                                for (int j = 0; j < iConstruct.commitPointSet.size(); j++) {
                                        String label = iConstruct.commitPointSet.get(j);
                                        if (!CPLabel2InterfaceConstruct.containsKey(label)) {
                                for (int j = 0; j < iConstruct.commitPointSet.size(); j++) {
                                        String label = iConstruct.commitPointSet.get(j);
                                        if (!CPLabel2InterfaceConstruct.containsKey(label)) {
-                                               CPLabel2InterfaceConstruct.put(label, new ArrayList<InterfaceConstruct>());
+                                               CPLabel2InterfaceConstruct.put(label,
+                                                               new ArrayList<InterfaceConstruct>());
                                        }
                                        CPLabel2InterfaceConstruct.get(label).add(iConstruct);
                                }
                                        }
                                        CPLabel2InterfaceConstruct.get(label).add(iConstruct);
                                }
@@ -93,10 +166,15 @@ public class SemanticsChecker {
                                        throw new SemanticsCheckerException(
                                                        "More than one global construct!");
                                }
                                        throw new SemanticsCheckerException(
                                                        "More than one global construct!");
                                }
-                               HashMap<ConditionalInterface, HashSet<ConditionalInterface>> hbConditions = theConstruct.hbRelations;
+                               // Record the options and check them
+                               options = theConstruct.options;
+
+                               // Record the HB conditions and check it
+                               hbConditions = theConstruct.hbRelations;
                                for (ConditionalInterface left : hbConditions.keySet()) {
                                        HashSet<ConditionalInterface> set = hbConditions.get(left);
                                        checkHBLabelConsistency(left);
                                for (ConditionalInterface left : hbConditions.keySet()) {
                                        HashSet<ConditionalInterface> set = hbConditions.get(left);
                                        checkHBLabelConsistency(left);
+                                       
                                        for (ConditionalInterface right : set) {
                                                checkHBLabelConsistency(right);
                                        }
                                        for (ConditionalInterface right : set) {
                                                checkHBLabelConsistency(right);
                                        }
@@ -105,33 +183,70 @@ public class SemanticsChecker {
                                PotentialCPDefineConstruct theConstruct = (PotentialCPDefineConstruct) construct;
                                label = theConstruct.label;
                                checkLabelDuplication(construct, label);
                                PotentialCPDefineConstruct theConstruct = (PotentialCPDefineConstruct) construct;
                                label = theConstruct.label;
                                checkLabelDuplication(construct, label);
+                               // Number the commit_point label
+                               commitPointLabel2Num.put(label, _commitPointNum++);
+                               
                                potentialCPLabel2Construct.put(label, inst);
                        } else if (construct instanceof CPDefineCheckConstruct) {
                                CPDefineCheckConstruct theConstruct = (CPDefineCheckConstruct) construct;
                                label = theConstruct.label;
                                checkLabelDuplication(construct, label);
                                potentialCPLabel2Construct.put(label, inst);
                        } else if (construct instanceof CPDefineCheckConstruct) {
                                CPDefineCheckConstruct theConstruct = (CPDefineCheckConstruct) construct;
                                label = theConstruct.label;
                                checkLabelDuplication(construct, label);
+                               // Number the commit_point label
+                               commitPointLabel2Num.put(label, _commitPointNum++);
+                               
                                CPLabel2Construct.put(label, inst);
                        } else if (construct instanceof CPDefineConstruct) {
                                CPDefineConstruct theConstruct = (CPDefineConstruct) construct;
                                label = theConstruct.label;
                                checkLabelDuplication(construct, label);
                                CPLabel2Construct.put(label, inst);
                        } else if (construct instanceof CPDefineConstruct) {
                                CPDefineConstruct theConstruct = (CPDefineConstruct) construct;
                                label = theConstruct.label;
                                checkLabelDuplication(construct, label);
+                               // Number the commit_point label
+                               commitPointLabel2Num.put(label, _commitPointNum++);
+                               
                                CPLabel2Construct.put(label, inst);
                                CPLabel2Construct.put(label, inst);
+                       } else if (construct instanceof EntryPointConstruct) {
+                               if (entryPointConstruct != null) {
+                                       throw new SemanticsCheckerException(
+                                                       "More than one entry point!");
+                               }
+                               entryPointConstruct = inst;
+                       } else if (construct instanceof InterfaceDefineConstruct) {
+                               InterfaceDefineConstruct theConstruct = (InterfaceDefineConstruct) construct;
+                               String name = theConstruct.name;
+                               if (interfaceName2DefineConstruct.containsKey(name)) {
+                                       throw new SemanticsCheckerException(
+                                                       "Interface define label duplicates!");
+                               }
+                               interfaceName2DefineConstruct.put(name, inst);
                        }
                }
        }
                        }
                }
        }
-       
+
        public String toString() {
                StringBuilder sb = new StringBuilder();
        public String toString() {
                StringBuilder sb = new StringBuilder();
+               if (entryPointConstruct == null) {
+                       sb.append("Entry point is not specified!");
+               } else {
+                       sb.append("@Entry_point:\n" + entryPointConstruct);
+               }
+               
                sb.append("Interface name 2 Construct:\n");
                for (String interfaceName : interfaceName2Construct.keySet()) {
                sb.append("Interface name 2 Construct:\n");
                for (String interfaceName : interfaceName2Construct.keySet()) {
-                       sb.append(interfaceName + "\t" + interfaceName2Construct.get(interfaceName) + "\n");
+                       sb.append(interfaceName + "\t"
+                                       + interfaceName2Construct.get(interfaceName) + "\n");
                }
                
                }
                
+               sb.append("Interface name 2 define construct:\n");
+               for (String interfaceName : interfaceName2DefineConstruct.keySet()) {
+                       sb.append(interfaceName + "\t"
+                                       + interfaceName2DefineConstruct.get(interfaceName) + "\n");
+               }
+
                sb.append("Potential commit point label 2 Construct:\n");
                for (String label : potentialCPLabel2Construct.keySet()) {
                sb.append("Potential commit point label 2 Construct:\n");
                for (String label : potentialCPLabel2Construct.keySet()) {
-                       sb.append(label + "\t" + potentialCPLabel2Construct.get(label) + "\n");
+                       sb.append(label + "\t" + potentialCPLabel2Construct.get(label)
+                                       + "\n");
                }
                }
-               
+
                sb.append("Commit point label 2 Construct:\n");
                for (String label : CPLabel2Construct.keySet()) {
                        sb.append(label + "\t" + CPLabel2Construct.get(label) + "\n");
                sb.append("Commit point label 2 Construct:\n");
                for (String label : CPLabel2Construct.keySet()) {
                        sb.append(label + "\t" + CPLabel2Construct.get(label) + "\n");
diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/SpecConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/SpecConstruct.java
index 95650ccdf0a9420f2cea428831683f638e96d043..e80cbd73fdf205860d56f24687eacda0926d073f 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/specExtraction/SpecConstruct.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/SpecConstruct.java
@@ -46,10 +46,10 @@ public class SpecConstruct {
                sb.append("Begin: "
                                + beginLineNum + "  End: " + endLineNum + "\n");
                sb.append(construct);
                sb.append("Begin: "
                                + beginLineNum + "  End: " + endLineNum + "\n");
                sb.append(construct);
-               if (construct instanceof InterfaceConstruct) {
+               if (construct instanceof InterfaceConstruct
+                               || construct instanceof InterfaceDefineConstruct) {
                        sb.append("Function declaration: " + interfaceDeclBody);
                }
                        sb.append("Function declaration: " + interfaceDeclBody);
                }
-               boolean a = !false, b = 3 > 0 ? a : !a;
                return sb.toString();
                
        }
                return sb.toString();
                
        }
diff --git a/test.c b/test.c
index 2dec27eceb3b6ac000f73b34cd581585e452b24f..417f795ccef101c0e1cf47e4bf56429a894ab27c 100644 (file)
--- a/test.c
+++ b/test.c
@@ -1,6 +1,14 @@
 #include <stdio.h>
 #include "test.h"
 
 #include <stdio.h>
 #include "test.h"
 
+struct XX {
+       
+};
+
+enum E {
+       a, b, c
+};
+
 void _foo(struct Test t) {
        printf("%d\n", t.x);
 }
 void _foo(struct Test t) {
        printf("%d\n", t.x);
 }
@@ -10,5 +18,6 @@ void foo(struct Test t) {
 }
 
 int main() {
 }
 
 int main() {
+       printf("%d\n", b);
        return 0;
 }
        return 0;
 }
diff --git a/test.cc b/test.cc
deleted file mode 100644 (file)
index c7cb0db..0000000
--- a/test.cc
+++ /dev/null
@@ -1,81 +0,0 @@
-#include <stdio.h>
-#include <iostream>
-#include <vector>
-
-using namespace std;
-
-
-template<typename T>
-class A {
-       private:
-       int outer;
-       class B {
-               private:
-                       vector<int> v;
-                       T str;
-               public:
-                       typedef struct C {
-                               T x;
-                       } C_t;
-
-                       enum interface_t {put, get};
-                       B() {
-                               v = vector<int>();
-                               str = "abc";
-
-                       }
-
-                       void _pushBack(int a) {
-                               cout << str << endl;
-                               v.push_back(a);
-                       }
-
-                       int _size() {
-                               return v.size();
-                       }
-
-                       C_t func() {
-                               char *cStr = "struct_ab";
-                               C_t c;
-                               c.x = cStr;
-                               return c;
-                       }
-       } b;
-
-       public:
-       A() {
-       }
-       
-       void pushBack(int a) {
-               //printf("Size: %d\n", b.size());
-               b._pushBack(a);
-               //printf("Size: %d\n", b.size());
-       }
-
-       int size() {
-               //B<T>::interface_t inter;
-               struct B::C_t c = b.func();
-               enum B::interface_t a = B::put;
-               vector<enum B::interface_t> ve(3);
-               ve.push_back(B::put);
-               cout << "Size: " << ve.size() << endl;
-               cout << b.func().x << endl;
-               return b._size();
-       }
-};
-
-int main() {
-       #define __COND_SAT__ a.size()
-       A<string> a;
-       a.pushBack(1);
-       if (__COND_SAT__ != 0) {
-               cout << "Size greater than 0" << endl;
-       }
-       #undef __COND_SAT__
-
-       bool __COND_SAT__ = false;
-       if (!__COND_SAT__) {
-               cout << "False!" << endl;
-       }
-       return 0;
-}
diff --git a/test.h b/test.h
index fb016e432718b2ef1c672b8c749a72f0c85b2397..0b752a38c2bd7715931e679c8568d44465d60435 100644 (file)
--- a/test.h
+++ b/test.h
@@ -1,7 +1,8 @@
 struct Test {
        int x;
 struct Test {
        int x;
-
+/*
        Test() {
                x = 2;
        }
        Test() {
                x = 2;
        }
+       */
 };
 };
This is the public repository for the CDSSpec specification compiler.