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.InterfaceDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct;
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, 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>();
+ this.interfaceName2DefineConstruct = new HashMap<String, SpecConstruct>();
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 {
- 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
+ "\"!");
- } else if (!label.equals("")){
+ } else if (!label.equals("")) {
InterfaceConstruct iConstruct = (InterfaceConstruct) interfaceName2Construct
.get(interfaceName).construct;
if (!iConstruct.hbConditions.containsKey(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 {
- if (potentialCPLabel2Construct.containsKey(label) ||
- CPLabel2Construct.containsKey(label))
+ 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 {
+ // 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
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);
- 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)) {
- CPLabel2InterfaceConstruct.put(label, new ArrayList<InterfaceConstruct>());
+ CPLabel2InterfaceConstruct.put(label,
+ new ArrayList<InterfaceConstruct>());
}
CPLabel2InterfaceConstruct.get(label).add(iConstruct);
}
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 right : set) {
checkHBLabelConsistency(right);
}
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);
+ // 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);
+ // Number the commit_point label
+ commitPointLabel2Num.put(label, _commitPointNum++);
+
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();
+ 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(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(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");
projects / cdsspec-compiler.git / blobdiff