import java.util.HashSet;
import edu.uci.eecs.specCompiler.grammerParser.ParseException;
-import edu.uci.eecs.specCompiler.grammerParser.SpecParser;
+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.SourceFileInfo;
import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
+/**
+ * <p>
+ * A specificaiton semantics checker that checks the consistency of the
+ * specifications after they are extracted from the source code.
+ * </p>
+ *
+ * @author peizhaoo
+ *
+ */
public class SemanticsChecker {
public final HashMap<File, SourceFileInfo> srcFilesInfo;
public final ArrayList<Construct> constructs;
public final HashMap<String, PotentialCPDefineConstruct> potentialCPLabel2Construct;
public final HashMap<String, InterfaceConstruct> interfaceName2Construct;
public final HashMap<String, InterfaceDefineConstruct> interfaceName2DefineConstruct;
- public final HashMap<String, ArrayList<InterfaceConstruct>> CPLabel2InterfaceConstruct;
+ public final HashMap<String, InterfaceConstruct> CPLabel2InterfaceConstruct;
public final HashMap<String, Integer> interface2Num;
+ public final HashMap<Integer, String> num2Interface;
public final HashMap<String, Integer> hbLabel2Num;
+ public final HashMap<Integer, String> num2HBLabel;
public final HashMap<String, Integer> commitPointLabel2Num;
+ public final HashMap<Integer, String> num2CommitPointLabel;
private HashMap<String, String> options;
private HashMap<ConditionalInterface, HashSet<ConditionalInterface>> hbConditions;
private ArrayList<EntryPointConstruct> entryPointConstructs;
private ClassBeginConstruct classBeginConstruct;
private ClassEndConstruct classEndConstruct;
-
+ private GlobalConstruct globalConstruct;
+
private String templateStr;
private String templateFullStr;
private String className;
this.potentialCPLabel2Construct = new HashMap<String, PotentialCPDefineConstruct>();
this.interfaceName2Construct = new HashMap<String, InterfaceConstruct>();
this.interfaceName2DefineConstruct = new HashMap<String, InterfaceDefineConstruct>();
- this.CPLabel2InterfaceConstruct = new HashMap<String, ArrayList<InterfaceConstruct>>();
+ this.CPLabel2InterfaceConstruct = new HashMap<String, InterfaceConstruct>();
this.entryPointConstructs = new ArrayList<EntryPointConstruct>();
this.classBeginConstruct = null;
this.classEndConstruct = null;
this.interface2Num = new HashMap<String, Integer>();
+ this.num2Interface = new HashMap<Integer, String>();
this.hbLabel2Num = new HashMap<String, Integer>();
+ this.num2HBLabel = new HashMap<Integer, String>();
// Immediately init the true HB-condition to be 0
hbLabel2Num.put("", 0);
+ num2HBLabel.put(0, "");
this.commitPointLabel2Num = new HashMap<String, Integer>();
+ this.num2CommitPointLabel = new HashMap<Integer, String>();
_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<ConditionalInterface, HashSet<ConditionalInterface>> getHBConditions() {
return this.hbConditions;
}
+ /**
+ * 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);
}
+ 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++);
+ num2HBLabel.put(_hbLabelNum, label);
}
}
}
// 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<InterfaceConstruct>());
+ // }
+ // CPLabel2InterfaceConstruct.get(label).add(iConstruct);
if (!CPLabel2InterfaceConstruct.containsKey(label)) {
- CPLabel2InterfaceConstruct.put(label,
- new ArrayList<InterfaceConstruct>());
+ CPLabel2InterfaceConstruct.put(label, iConstruct);
+ } else {
+ throw new SemanticsCheckerException(
+ "Commit point has multiple interfaces!");
}
- CPLabel2InterfaceConstruct.get(label).add(iConstruct);
+
}
}
}
Construct construct = constructs.get(i);
if (construct instanceof GlobalConstruct) {
GlobalConstruct theConstruct = (GlobalConstruct) construct;
+ globalConstruct = theConstruct;
if (!hasGlobalConstruct)
hasGlobalConstruct = true;
else {
PotentialCPDefineConstruct theConstruct = (PotentialCPDefineConstruct) construct;
label = theConstruct.label;
checkLabelDuplication(construct, label);
- // Number the commit_point label
+ // Number the commit point potential commit point label
commitPointLabel2Num.put(label, _commitPointNum++);
+ num2CommitPointLabel.put(_commitPointNum, label);
potentialCPLabel2Construct.put(label,
(PotentialCPDefineConstruct) construct);
CPDefineCheckConstruct theConstruct = (CPDefineCheckConstruct) construct;
label = theConstruct.label;
checkLabelDuplication(construct, label);
- // Number the commit_point 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 label
+ // Number the commit point define label
commitPointLabel2Num.put(label, _commitPointNum++);
+ num2CommitPointLabel.put(_commitPointNum, label);
CPLabel2Construct.put(label, construct);
} else if (construct instanceof EntryPointConstruct) {
interfaceName2DefineConstruct.put(name, theConstruct);
} else if (construct instanceof ClassBeginConstruct) {
classBeginConstruct = (ClassBeginConstruct) construct;
- ArrayList<String> content = srcFilesInfo.get(classBeginConstruct.file).content;
- String firstLine = content.get(classBeginConstruct.beginLineNum), secondLine;
+ ArrayList<String> content = srcFilesInfo
+ .get(classBeginConstruct.file).content;
+ String firstLine = content
+ .get(classBeginConstruct.beginLineNum + 1), secondLine;
if (firstLine.startsWith("template")) {
- secondLine = content.get(classBeginConstruct.beginLineNum + 1);
+ 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");
}
}
}
projects / cdsspec-compiler.git / blobdiff