X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fedu%2Fuci%2Feecs%2FspecCompiler%2FcodeGenerator%2FSemanticsChecker.java;h=ed20aa86ef6ed9a7765572315669e5283fcda979;hb=375b8b02ae398aceddb920e0e7e94287e33f231e;hp=f053ba4186f2424373b4646875e420a59a20eaf9;hpb=70fd401b67750e8efbd73540e1affa7f65c61c1c;p=cdsspec-compiler.git
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
index f053ba4..ed20aa8 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
@@ -1,42 +1,202 @@
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.grammerParser.ParseException;
+import edu.uci.eecs.specCompiler.specExtraction.CPClearConstruct;
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;
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.ParserUtils;
import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.SourceFileInfo;
+import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
+/**
+ *
+ * A specificaiton semantics checker that checks the consistency of the
+ * specifications after they are extracted from the source code.
+ *
+ *
+ * @author peizhaoo
+ *
+ */
public class SemanticsChecker {
- public final ArrayList constructs;
- public final HashMap label2Construct;
- public final HashMap interfaceName2Construct;
+ public final HashMap srcFilesInfo;
+ public final ArrayList constructs;
+ public final HashMap CPLabel2Construct;
+ public final HashMap potentialCPLabel2Construct;
+ public final HashMap interfaceName2Construct;
+ public final HashMap interfaceName2DefineConstruct;
+ public final HashMap CPLabel2InterfaceConstruct;
- public SemanticsChecker(ArrayList constructs) {
- this.constructs = constructs;
- this.label2Construct = new HashMap();
- this.interfaceName2Construct = new HashMap();
+ public final HashMap interface2Num;
+ public final HashMap num2Interface;
+ public final HashMap hbLabel2Num;
+ public final HashMap num2HBLabel;
+ public final HashMap commitPointLabel2Num;
+ public final HashMap num2CommitPointLabel;
+
+ private HashMap options;
+ private HashMap> hbConditions;
+ private ArrayList entryPointConstructs;
+ private ClassBeginConstruct classBeginConstruct;
+ private ClassEndConstruct classEndConstruct;
+ private GlobalConstruct globalConstruct;
+
+ private String templateStr;
+ private String templateFullStr;
+ private String className;
+
+ private int _interfaceNum;
+ private int _hbLabelNum;
+ private int _commitPointNum;
+
+ public SemanticsChecker(SpecExtractor extractor) {
+ this.srcFilesInfo = extractor.srcFilesInfo;
+ this.constructs = extractor.getConstructs();
+ this.CPLabel2Construct = new HashMap();
+ this.potentialCPLabel2Construct = new HashMap();
+ this.interfaceName2Construct = new HashMap();
+ this.interfaceName2DefineConstruct = new HashMap();
+ this.CPLabel2InterfaceConstruct = new HashMap();
+ this.entryPointConstructs = new ArrayList();
+ this.classBeginConstruct = null;
+ this.classEndConstruct = null;
+
+ this.interface2Num = new HashMap();
+ this.num2Interface = new HashMap();
+ this.hbLabel2Num = new HashMap();
+ this.num2HBLabel = new HashMap();
+ // Immediately init the true HB-condition to be 0
+ hbLabel2Num.put("", 0);
+ num2HBLabel.put(0, "");
+
+ this.commitPointLabel2Num = new HashMap();
+ this.num2CommitPointLabel = new HashMap();
+
+ _interfaceNum = 0;
+ _hbLabelNum = 0;
+ _commitPointNum = 0;
+
+ templateStr = null;
+ templateFullStr = null;
+ className = null;
+ }
+
+ public ClassBeginConstruct getClassBeginConstruct() {
+ return this.classBeginConstruct;
+ }
+
+ public ClassEndConstruct getClassEndConstruct() {
+ return this.classEndConstruct;
+ }
+
+ public String getTemplateFullStr() {
+ return this.templateFullStr;
+ }
+
+ public String getTemplateStr() {
+ return this.templateStr;
+ }
+
+ public String getClassName() {
+ return this.className;
+ }
+
+ public GlobalConstruct getGlobalConstruct() {
+ return this.globalConstruct;
+ }
+
+ public HashMap> getHBConditions() {
+ return this.hbConditions;
}
- private void checkHBLabelConsistency(String interfaceName, String label)
+ /**
+ * Check if the conditional interface is in the HB checking list
+ *
+ * @param condInterface
+ * @return
+ */
+ public boolean containsConditionalInterface(
+ ConditionalInterface condInterface) {
+ if (hbConditions.containsKey(condInterface))
+ return true;
+ for (ConditionalInterface key : hbConditions.keySet()) {
+ if (hbConditions.get(key).contains(condInterface))
+ return true;
+ }
+ return false;
+ }
+
+ public String getOption(String key) {
+ return options.get(key);
+ }
+
+ private void checkHBLabelConsistency(ConditionalInterface inst)
throws SemanticsCheckerException {
+ String interfaceName = inst.interfaceName, label = inst.hbConditionLabel;
if (!interfaceName2Construct.containsKey(interfaceName)) {
throw new SemanticsCheckerException(
- "In global construct, no interface \""
- + interfaceName + "\"!");
- } else {
+ "In global construct, no interface \"" + interfaceName
+ + "\"!");
+ } else if (!label.equals("")) {
InterfaceConstruct iConstruct = (InterfaceConstruct) interfaceName2Construct
- .get(interfaceName).construct;
+ .get(interfaceName);
if (!iConstruct.hbConditions.containsKey(label)) {
throw new SemanticsCheckerException("Interface "
- + interfaceName
- + " doesn't contain HB_codition: " + label
- + "!");
+ + interfaceName + " doesn't contain HB_codition: "
+ + label + "!");
+ }
+
+ // Number the HB-condition label
+ hbLabel2Num.put(label, _hbLabelNum++);
+ num2HBLabel.put(_hbLabelNum, label);
+ }
+ }
+
+ private void checkLabelDuplication(Construct construct, String label)
+ throws SemanticsCheckerException {
+ if (potentialCPLabel2Construct.containsKey(label)
+ || CPLabel2Construct.containsKey(label))
+ 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 {
+ // 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(
+ "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!");
}
}
}
@@ -45,40 +205,158 @@ public class SemanticsChecker {
boolean hasGlobalConstruct = false;
// First grab the information from the interface
for (int i = 0; i < constructs.size(); i++) {
- Construct inst = constructs.get(i).construct;
+ Construct inst = constructs.get(i);
if (inst instanceof InterfaceConstruct) {
InterfaceConstruct iConstruct = (InterfaceConstruct) inst;
- interfaceName2Construct.put(iConstruct.name, constructs.get(i));
+ if (interfaceName2Construct.containsKey(iConstruct.name)) {
+ throw new SemanticsCheckerException("Interface name: "
+ + iConstruct.name + " duplicates!");
+ }
+ // Number the interface label
+ interface2Num.put(iConstruct.name, _interfaceNum++);
+ num2Interface.put(_interfaceNum, iConstruct.name);
+
+ interfaceName2Construct.put(iConstruct.name,
+ (InterfaceConstruct) constructs.get(i));
+
+ for (int j = 0; j < iConstruct.commitPointSet.size(); j++) {
+ String label = iConstruct.commitPointSet.get(j);
+ // if (!CPLabel2InterfaceConstruct.containsKey(label)) {
+ // CPLabel2InterfaceConstruct.put(label,
+ // new ArrayList());
+ // }
+ // CPLabel2InterfaceConstruct.get(label).add(iConstruct);
+ if (!CPLabel2InterfaceConstruct.containsKey(label)) {
+ CPLabel2InterfaceConstruct.put(label, iConstruct);
+ } else {
+ throw new SemanticsCheckerException(
+ "Commit point has multiple interfaces!");
+ }
+
+ }
}
}
+ String label;
for (int i = 0; i < constructs.size(); i++) {
- SpecConstruct inst = constructs.get(i);
- Construct construct = inst.construct;
+ Construct construct = constructs.get(i);
if (construct instanceof GlobalConstruct) {
GlobalConstruct theConstruct = (GlobalConstruct) construct;
+ globalConstruct = theConstruct;
if (!hasGlobalConstruct)
hasGlobalConstruct = true;
else {
throw new SemanticsCheckerException(
"More than one global construct!");
}
+ // Record the options and check them
+ options = theConstruct.options;
- HashMap> hbConditions = theConstruct.hbRelations;
+ // Record the HB conditions and check it
+ hbConditions = theConstruct.hbRelations;
for (ConditionalInterface left : hbConditions.keySet()) {
HashSet set = hbConditions.get(left);
- checkHBLabelConsistency(left.interfaceName, left.hbConditionLabel);
+ checkHBLabelConsistency(left);
+
for (ConditionalInterface right : set) {
- checkHBLabelConsistency(right.interfaceName, right.hbConditionLabel);
+ checkHBLabelConsistency(right);
}
}
} else if (construct instanceof PotentialCPDefineConstruct) {
PotentialCPDefineConstruct theConstruct = (PotentialCPDefineConstruct) construct;
- label2Construct.put(theConstruct.label, inst);
+ label = theConstruct.label;
+ checkLabelDuplication(construct, label);
+ // Number the commit point potential commit point label
+ commitPointLabel2Num.put(label, _commitPointNum++);
+ num2CommitPointLabel.put(_commitPointNum, label);
+
+ potentialCPLabel2Construct.put(label,
+ (PotentialCPDefineConstruct) construct);
} else if (construct instanceof CPDefineCheckConstruct) {
CPDefineCheckConstruct theConstruct = (CPDefineCheckConstruct) construct;
- label2Construct.put(theConstruct.label, inst);
+ label = theConstruct.label;
+ checkLabelDuplication(construct, label);
+ // Number the commit point define check label
+ commitPointLabel2Num.put(label, _commitPointNum++);
+ num2CommitPointLabel.put(_commitPointNum, label);
+
+ CPLabel2Construct.put(label, construct);
+ } else if (construct instanceof CPClearConstruct) {
+ CPClearConstruct theConstruct = (CPClearConstruct) construct;
+ label = theConstruct.label;
+ checkLabelDuplication(construct, label);
+ // Number the commit point define check label
+ commitPointLabel2Num.put(label, _commitPointNum++);
+ num2CommitPointLabel.put(_commitPointNum, label);
+
+ CPLabel2Construct.put(label, construct);
+ } else if (construct instanceof CPDefineConstruct) {
+ CPDefineConstruct theConstruct = (CPDefineConstruct) construct;
+ label = theConstruct.label;
+ checkLabelDuplication(construct, label);
+ // Number the commit point define label
+ commitPointLabel2Num.put(label, _commitPointNum++);
+ num2CommitPointLabel.put(_commitPointNum, label);
+
+ CPLabel2Construct.put(label, construct);
+ } else if (construct instanceof EntryPointConstruct) {
+ entryPointConstructs.add((EntryPointConstruct) construct);
+ } 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, theConstruct);
+ } else if (construct instanceof ClassBeginConstruct) {
+ classBeginConstruct = (ClassBeginConstruct) construct;
+ ArrayList content = srcFilesInfo
+ .get(classBeginConstruct.file).content;
+ String firstLine = content
+ .get(classBeginConstruct.beginLineNum + 1), secondLine;
+ if (firstLine.startsWith("template")) {
+ secondLine = content
+ .get(classBeginConstruct.beginLineNum + 1);
+ templateFullStr = firstLine;
+ templateStr = ParserUtils.getTemplateStr(firstLine);
+ className = ParserUtils.getClassName(secondLine);
+ } else {
+ className = ParserUtils.getClassName(firstLine);
+ }
+
+ } else if (construct instanceof ClassEndConstruct) {
+ classEndConstruct = (ClassEndConstruct) construct;
+ className = getOption("CLASS");
}
}
}
+
+ public String toString() {
+ StringBuilder sb = new StringBuilder();
+
+ 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"
+ + interfaceName2DefineConstruct.get(interfaceName) + "\n");
+ }
+
+ sb.append("Potential commit point label 2 Construct:\n");
+ for (String label : potentialCPLabel2Construct.keySet()) {
+ 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");
+ }
+ return sb.toString();
+ }
}