ready to generate code

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
new file mode 100644 (file)
index 0000000..faac44c
--- /dev/null
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -0,0 +1,19 @@
+package edu.uci.eecs.specCompiler.codeGenerator;
+
+import java.util.ArrayList;
+
+import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct;
+
+/**
+ * <p>
+ * This class will generate the annotated C code that can run on the current
+ * model checker.
+ * </p>
+ * 
+ * @author peizhaoo
+ * 
+ */
+public class CodeGenerator {
+       ArrayList<SpecConstruct> _constructs;
+       
+}

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
new file mode 100644 (file)
index 0000000..f053ba4
--- /dev/null
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
@@ -0,0 +1,84 @@
+package edu.uci.eecs.specCompiler.codeGenerator;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.HashSet;
+
+import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
+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.PotentialCPDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct;
+
+public class SemanticsChecker {
+       public final ArrayList<SpecConstruct> constructs;
+       public final HashMap<String, SpecConstruct> label2Construct;
+       public final HashMap<String, SpecConstruct> interfaceName2Construct;
+
+       public SemanticsChecker(ArrayList<SpecConstruct> constructs) {
+               this.constructs = constructs;
+               this.label2Construct = new HashMap<String, SpecConstruct>();
+               this.interfaceName2Construct = new HashMap<String, SpecConstruct>();
+       }
+
+       private void checkHBLabelConsistency(String interfaceName, String label)
+                       throws SemanticsCheckerException {
+               if (!interfaceName2Construct.containsKey(interfaceName)) {
+                       throw new SemanticsCheckerException(
+                                       "In global construct, no interface \""
+                                                       + interfaceName + "\"!");
+               } else {
+                       InterfaceConstruct iConstruct = (InterfaceConstruct) interfaceName2Construct
+                                       .get(interfaceName).construct;
+                       if (!iConstruct.hbConditions.containsKey(label)) {
+                               throw new SemanticsCheckerException("Interface "
+                                               + interfaceName
+                                               + " doesn't contain HB_codition: " + label
+                                               + "!");
+                       }
+               }
+       }
+
+       public void check() throws SemanticsCheckerException {
+               boolean hasGlobalConstruct = false;
+               // First grab the information from the interface
+               for (int i = 0; i < constructs.size(); i++) {
+                       Construct inst = constructs.get(i).construct;
+                       if (inst instanceof InterfaceConstruct) {
+                               InterfaceConstruct iConstruct = (InterfaceConstruct) inst;
+                               interfaceName2Construct.put(iConstruct.name, constructs.get(i));
+                       }
+               }
+
+               for (int i = 0; i < constructs.size(); i++) {
+                       SpecConstruct inst = constructs.get(i);
+                       Construct construct = inst.construct;
+                       if (construct instanceof GlobalConstruct) {
+                               GlobalConstruct theConstruct = (GlobalConstruct) construct;
+                               if (!hasGlobalConstruct)
+                                       hasGlobalConstruct = true;
+                               else {
+                                       throw new SemanticsCheckerException(
+                                                       "More than one global construct!");
+                               }
+
+                               HashMap<ConditionalInterface, HashSet<ConditionalInterface>> hbConditions = theConstruct.hbRelations;
+                               for (ConditionalInterface left : hbConditions.keySet()) {
+                                       HashSet<ConditionalInterface> set = hbConditions.get(left);
+                                       checkHBLabelConsistency(left.interfaceName, left.hbConditionLabel);
+                                       for (ConditionalInterface right : set) {
+                                               checkHBLabelConsistency(right.interfaceName, right.hbConditionLabel);
+                                       }
+                               }
+                       } else if (construct instanceof PotentialCPDefineConstruct) {
+                               PotentialCPDefineConstruct theConstruct = (PotentialCPDefineConstruct) construct;
+                               label2Construct.put(theConstruct.label, inst);
+                       } else if (construct instanceof CPDefineCheckConstruct) {
+                               CPDefineCheckConstruct theConstruct = (CPDefineCheckConstruct) construct;
+                               label2Construct.put(theConstruct.label, inst);
+                       }
+               }
+       }
+}

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsCheckerException.java b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsCheckerException.java
new file mode 100644 (file)
index 0000000..c44da96
--- /dev/null
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsCheckerException.java
@@ -0,0 +1,7 @@
+package edu.uci.eecs.specCompiler.codeGenerator;
+
+public class SemanticsCheckerException extends Exception {
+       public SemanticsCheckerException(String msg) {
+               super(msg);
+       }
+}
\ No newline at end of file

diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java
index ac6de02b405f06a4db25b1a184009eb6d150c0a9..eb4bdb2d5d6ea704da9c7b1c5f858906b7613152 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java
@@ -179,6 +179,10 @@ public class SpecExtractor {
                else
                        return line.substring(i, j + 1);
        }
+       
+       public ArrayList<SpecConstruct> getConstructs() {
+               return this._constructs;
+       }
 
        public static void main(String[] argvs) {
                SpecExtractor extractor = new SpecExtractor();