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=3bd801ce1a323f2b526ce102aecb07df4e80b505;hpb=275b0c45df6810492526210aff9c914848fbdf3b;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 3bd801c..ed20aa8 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java @@ -1,102 +1,263 @@ 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.ActionSubConstruct.DefineVar; +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 CPLabel2Construct; - public final HashMap potentialCPLabel2Construct; - public final HashMap interfaceName2Construct; - public final HashMap> CPLabel2InterfaceConstruct; - public final HashSet defineVars; - - public SemanticsChecker(ArrayList constructs) { - this.constructs = constructs; - this.CPLabel2Construct = new HashMap(); - this.potentialCPLabel2Construct = new HashMap(); - this.interfaceName2Construct = new HashMap(); - this.CPLabel2InterfaceConstruct = new HashMap>(); - this.defineVars = new HashSet(); + 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 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; + } + + /** + * 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; + 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; + .get(interfaceName); if (!iConstruct.hbConditions.containsKey(label)) { throw new SemanticsCheckerException("Interface " + 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)) + 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!"); + } + } + } + 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; + Construct inst = constructs.get(i); if (inst instanceof InterfaceConstruct) { InterfaceConstruct iConstruct = (InterfaceConstruct) inst; - 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 + "__"); + 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, new ArrayList()); + CPLabel2InterfaceConstruct.put(label, iConstruct); + } else { + throw new SemanticsCheckerException( + "Commit point has multiple interfaces!"); } - CPLabel2InterfaceConstruct.get(label).add(iConstruct); + } } } 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!"); } - HashMap> 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 set = hbConditions.get(left); checkHBLabelConsistency(left); + for (ConditionalInterface right : set) { checkHBLabelConsistency(right); } @@ -105,33 +266,93 @@ public class SemanticsChecker { PotentialCPDefineConstruct theConstruct = (PotentialCPDefineConstruct) construct; label = theConstruct.label; checkLabelDuplication(construct, label); - potentialCPLabel2Construct.put(label, inst); + // 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; label = theConstruct.label; checkLabelDuplication(construct, label); - CPLabel2Construct.put(label, inst); + // 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); - CPLabel2Construct.put(label, inst); + // 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(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");