save
[cdsspec-compiler.git] / src / edu / uci / eecs / specCompiler / codeGenerator / SemanticsChecker.java
index 495801b97d263965c5fa5aed5828ef2dc942f63f..d09a61c8960efdf2a64eb0a0f6e0888ff474e3bb 100644 (file)
@@ -1,11 +1,14 @@
 package edu.uci.eecs.specCompiler.codeGenerator;
 
+import java.io.File;
 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.CPDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.ClassBeginConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.ClassEndConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
 import edu.uci.eecs.specCompiler.specExtraction.Construct;
 import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
@@ -13,43 +16,51 @@ 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.SourceFileInfo;
+import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
 
 public class SemanticsChecker {
+       public final HashMap<File, SourceFileInfo> srcFilesInfo;
        public final ArrayList<Construct> constructs;
        public final HashMap<String, Construct> CPLabel2Construct;
-       public final HashMap<String, Construct> potentialCPLabel2Construct;
-       public final HashMap<String, Construct> interfaceName2Construct;
+       public final HashMap<String, PotentialCPDefineConstruct> potentialCPLabel2Construct;
+       public final HashMap<String, InterfaceConstruct> interfaceName2Construct;
        public final HashMap<String, Construct> interfaceName2DefineConstruct;
        public final HashMap<String, ArrayList<InterfaceConstruct>> CPLabel2InterfaceConstruct;
-       
+
        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 Construct entryPointConstruct;
-       
+       private ArrayList<EntryPointConstruct> entryPointConstructs;
+       private ClassBeginConstruct classBeginConstruct;
+       private ClassEndConstruct classEndConstruct;
+
        private int _interfaceNum;
        private int _hbLabelNum;
-       private int _commitPointNum;    
+       private int _commitPointNum;
 
-       public SemanticsChecker(ArrayList<Construct> constructs) {
-               this.constructs = constructs;
+       public SemanticsChecker(SpecExtractor extractor) {
+               this.srcFilesInfo = extractor.srcFilesInfo;
+               this.constructs = extractor.getConstructs();
                this.CPLabel2Construct = new HashMap<String, Construct>();
-               this.potentialCPLabel2Construct = new HashMap<String, Construct>();
-               this.interfaceName2Construct = new HashMap<String, Construct>();
+               this.potentialCPLabel2Construct = new HashMap<String, PotentialCPDefineConstruct>();
+               this.interfaceName2Construct = new HashMap<String, InterfaceConstruct>();
                this.interfaceName2DefineConstruct = new HashMap<String, Construct>();
                this.CPLabel2InterfaceConstruct = new HashMap<String, ArrayList<InterfaceConstruct>>();
-               this.entryPointConstruct = null;
-               
+               this.entryPointConstructs = new ArrayList<EntryPointConstruct>();
+               this.classBeginConstruct = null;
+               this.classEndConstruct = 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;
@@ -78,16 +89,16 @@ public class SemanticsChecker {
                                                + 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)
@@ -103,17 +114,25 @@ public class SemanticsChecker {
        }
 
        private void postCheck() throws SemanticsCheckerException {
-               // This is a C program, must provide the entry point
-               if (getOption("LANG").equals("C") && entryPointConstruct == null) {
+               // C++ data structure with Class must provide the beginning and ending
+               // of its declaration
+               if (getOption("Class") != null) {
+                       if (classBeginConstruct == null || classEndConstruct == null) {
+                               throw new SemanticsCheckerException(
+                                               "Class must provide the boundary explicitly!");
+                       }
+               }
+               // It must provide the entry point
+               if (entryPointConstructs.size() == 0) {
                        throw new SemanticsCheckerException(
-                                       "C program must provide the entry point!");
+                                       "The program must have at least one 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!");
+                               throw new SemanticsCheckerException("Label \"" + name
+                                               + "\" does not have interface declaration!");
                        }
                }
        }
@@ -131,8 +150,9 @@ public class SemanticsChecker {
                                }
                                // Number the interface label
                                interface2Num.put(iConstruct.name, _interfaceNum++);
-                               
-                               interfaceName2Construct.put(iConstruct.name, constructs.get(i));
+
+                               interfaceName2Construct.put(iConstruct.name,
+                                               (InterfaceConstruct) constructs.get(i));
 
                                for (int j = 0; j < iConstruct.commitPointSet.size(); j++) {
                                        String label = iConstruct.commitPointSet.get(j);
@@ -164,7 +184,7 @@ public class SemanticsChecker {
                                for (ConditionalInterface left : hbConditions.keySet()) {
                                        HashSet<ConditionalInterface> set = hbConditions.get(left);
                                        checkHBLabelConsistency(left);
-                                       
+
                                        for (ConditionalInterface right : set) {
                                                checkHBLabelConsistency(right);
                                        }
@@ -175,15 +195,16 @@ public class SemanticsChecker {
                                checkLabelDuplication(construct, label);
                                // Number the commit_point label
                                commitPointLabel2Num.put(label, _commitPointNum++);
-                               
-                               potentialCPLabel2Construct.put(label, construct);
+
+                               potentialCPLabel2Construct.put(label,
+                                               (PotentialCPDefineConstruct) construct);
                        } 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, construct);
                        } else if (construct instanceof CPDefineConstruct) {
                                CPDefineConstruct theConstruct = (CPDefineConstruct) construct;
@@ -191,14 +212,10 @@ public class SemanticsChecker {
                                checkLabelDuplication(construct, label);
                                // Number the commit_point label
                                commitPointLabel2Num.put(label, _commitPointNum++);
-                               
+
                                CPLabel2Construct.put(label, construct);
                        } else if (construct instanceof EntryPointConstruct) {
-                               if (entryPointConstruct != null) {
-                                       throw new SemanticsCheckerException(
-                                                       "More than one entry point!");
-                               }
-                               entryPointConstruct = construct;
+                               entryPointConstructs.add((EntryPointConstruct) construct);
                        } else if (construct instanceof InterfaceDefineConstruct) {
                                InterfaceDefineConstruct theConstruct = (InterfaceDefineConstruct) construct;
                                String name = theConstruct.name;
@@ -207,24 +224,23 @@ public class SemanticsChecker {
                                                        "Interface define label duplicates!");
                                }
                                interfaceName2DefineConstruct.put(name, construct);
+                       } else if (construct instanceof ClassBeginConstruct) {
+                               classBeginConstruct = (ClassBeginConstruct) construct;
+                       } else if (construct instanceof ClassEndConstruct) {
+                               classEndConstruct = (ClassEndConstruct) construct;
                        }
                }
        }
 
        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(interfaceName + "\t"
                                        + interfaceName2Construct.get(interfaceName) + "\n");
                }
-               
+
                sb.append("Interface name 2 define construct:\n");
                for (String interfaceName : interfaceName2DefineConstruct.keySet()) {
                        sb.append(interfaceName + "\t"