From 4f1008a7b5b186a9d40254698b98bd4628c3a8db Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Fri, 18 Oct 2013 17:39:36 -0700 Subject: [PATCH] more changes --- grammer/spec-compiler.jj | 84 +++++++++- .../codeGenerator/CodeGenerator.java | 140 +++++++++-------- .../codeGenerator/CodeVariables.java | 66 +++++++- .../codeGenerator/SemanticsChecker.java | 143 ++++++++++++++++-- .../specExtraction/SpecConstruct.java | 4 +- test.c | 9 ++ test.cc | 81 ---------- test.h | 3 +- 8 files changed, 355 insertions(+), 175 deletions(-) delete mode 100644 test.cc diff --git a/grammer/spec-compiler.jj b/grammer/spec-compiler.jj index 6776986..e4f723f 100644 --- a/grammer/spec-compiler.jj +++ b/grammer/spec-compiler.jj @@ -10,6 +10,11 @@ a) Global construct @Begin + @Options: + # If LANG is not define, it's C++ by default. C does not support class + # and template, so if it's defined as C, we should also have a explicit + # entry point. + LANG = C; @Global_define: @DeclareVar: @InitVar: @@ -60,6 +65,16 @@ @Potential_commit_point_label: ... @Label: ... @End + + e) Entry point construct + @Begin + @Entry_point + @End + + f) Interface define construct + @Begin + @Interface_define: + @End */ @@ -90,6 +105,8 @@ import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface; import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct; import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar; import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct; +import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct; +import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct; public class SpecParser { public static void main(String[] argvs) @@ -144,6 +161,8 @@ TOKEN : | +| + | | @@ -160,6 +179,10 @@ TOKEN : | +| + +| + | | @@ -332,7 +355,9 @@ Construct Parse() : LOOKAHEAD(3) res = Interface() | LOOKAHEAD(3) res = Potential_commit_point_define() | LOOKAHEAD(3) res = Commit_point_define() | - LOOKAHEAD(3) res = Commit_point_define_check() + LOOKAHEAD(3) res = Commit_point_define_check() | + LOOKAHEAD(3) res = Entry_point() | + LOOKAHEAD(3) res = Interface_define() ) { @@ -345,13 +370,31 @@ GlobalConstruct Global_construct() : { GlobalConstruct res; SequentialDefineSubConstruct code; + HashMap options; + String key, value; } { - { res = null; } + { + res = null; + options = new HashMap(); + } + ( + ((key = .image) + + (value = .image) + { + if (options.containsKey(key)) { + throw new ParseException("Duplicate options!"); + } + options.put(key, value); + } + + )* + )? (code = Global_define()) - { res = new GlobalConstruct(code); } + { res = new GlobalConstruct(code, options); } (Interface_clusters(res))? (Happens_before(res))? @@ -410,8 +453,8 @@ SequentialDefineSubConstruct Global_define() : initVar = ""; defineFunc = ""; } - - ( (declareVar = C_CPP_CODE()))? + + ( (declareVar = C_CPP_CODE()))? ( (initVar = C_CPP_CODE()))? ( (defineFunc = C_CPP_CODE()))? { @@ -630,3 +673,34 @@ CPDefineCheckConstruct Commit_point_define_check() : return res; } } + +EntryPointConstruct Entry_point() : +{} +{ + + + + + + + { + return new EntryPointConstruct(); + } +} + +InterfaceDefineConstruct Interface_define() : +{ + String name; +} +{ + + + (name = .image) + + + { + return new InterfaceDefineConstruct(name); + } +} + + diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index 8f4537a..05a76a7 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -12,6 +12,7 @@ import java.util.Iterator; import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar; import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct; 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.GlobalConstruct; import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct; @@ -97,21 +98,20 @@ public class CodeGenerator { GlobalConstruct construct = (GlobalConstruct) inst.construct; ArrayList newCode = new ArrayList(); - // Generate the inner class definition - newCode.add("class " + CodeVariables.SPEC_CLASS + " {\n"); - newCode.add("public:\n"); + // Generate all sequential variables into a struct + newCode.add("struct " + CodeVariables.SPEC_STRUCT + " {\n"); // Generate the code in global construct first SequentialDefineSubConstruct globalCode = construct.code; breakCodeLines(newCode, globalCode.declareVar); // Generate code from the DefineVar, __COND_SAT__ and __ID__ + // The hashtable in the contract can only contains pointers or integers // __COND_SAT__ - newCode.add(CodeVariables.SPEC_HASHTABLE + "<" + CodeVariables.BOOLEAN - + "> " + CodeVariables.SPEC_CONDITION + ";"); + newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_CONDITION + + ";"); // __ID__ - newCode.add(CodeVariables.SPEC_HASHTABLE + "<" + CodeVariables.SPEC_TAG - + "> " + CodeVariables.SPEC_ID + ";"); + newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_ID + ";"); // DefineVars for (String interfaceName : _semantics.interfaceName2Construct.keySet()) { @@ -120,58 +120,46 @@ public class CodeGenerator { ArrayList defineVars = iConstruct.action.defineVars; for (int i = 0; i < defineVars.size(); i++) { DefineVar var = defineVars.get(i); - newCode.add(CodeVariables.SPEC_HASHTABLE + "<" + var.varType - + "> " + var.getNewVarName() + ";"); + newCode.add(CodeVariables.SPEC_HASHTABLE + var.getNewVarName() + + ";"); } } - // Enum of all interface - String enumDefinition = "enum " + CodeVariables.SPEC_INTERFACE_ENUM - + " {"; - Iterator iter = _semantics.interfaceName2Construct.keySet() - .iterator(); - String interfaceName; - if (iter.hasNext()) { - interfaceName = iter.next(); - enumDefinition = enumDefinition + "_" + interfaceName + "_"; - } - while (iter.hasNext()) { - interfaceName = iter.next(); - enumDefinition = enumDefinition + ", _" + interfaceName + "_"; - } - enumDefinition = enumDefinition + "};"; - newCode.add(enumDefinition); - // __interface - newCode.add(CodeVariables.SPEC_HASHTABLE + " " - + CodeVariables.SPEC_INTERFACE + ";"); + newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_INTERFACE + + ";"); - // Generate constructor (the place to initialize everything!) - newCode.add("\n"); - newCode.add(CodeVariables.SPEC_CLASS + "() {"); + // End of the struct + newCode.add("}"); + // FIXME: Constructor should be modified and put in the right place + // Generate constructor (the place to initialize everything!) breakCodeLines(newCode, globalCode.initVar); // __COND_SAT__ - newCode.add(CodeVariables.SPEC_CONDITION + " = " - + CodeVariables.SPEC_HASHTABLE + "<" + CodeVariables.BOOLEAN - + ">();"); + newCode.add("init_table(&" + CodeVariables.SPEC_CONDITION + ");"); // __ID__ - newCode.add(CodeVariables.SPEC_ID + " = " - + CodeVariables.SPEC_HASHTABLE + "<" + CodeVariables.SPEC_TAG - + ">();"); + newCode.add("init_table(&" + CodeVariables.SPEC_ID + ");"); + // DefineVars + for (String interfaceName : _semantics.interfaceName2Construct.keySet()) { + InterfaceConstruct iConstruct = (InterfaceConstruct) _semantics.interfaceName2Construct + .get(interfaceName).construct; + ArrayList defineVars = iConstruct.action.defineVars; + for (int i = 0; i < defineVars.size(); i++) { + DefineVar var = defineVars.get(i); + newCode.add("init_table(&" + var.getNewVarName() + ");"); + } + } // __interface - newCode.add(CodeVariables.SPEC_INTERFACE + " = " - + CodeVariables.SPEC_HASHTABLE + "();"); - // FIXME: Pass the happens-before relationship check here - newCode.add("}"); + newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE + ");"); + + // Pass the happens-before relationship check here + newCode.addAll(CodeVariables.generateHBInitAnnotation(_semantics)); + newCode.add("\n"); + // Generate the sequential functions breakCodeLines(newCode, globalCode.defineFunc); - // Generate the end of the inner class definition - newCode.add("};\n"); printCode(newCode); CodeAddition addition = new CodeAddition(lineNum, newCode); @@ -209,18 +197,27 @@ public class CodeGenerator { // Rename the interface name File file = inst.file; - ArrayList content = contents.get(file); String funcDecl = inst.interfaceDeclBody; - String funcName = renameInterface(funcDecl, content, lineNum); + // Rename the function declaration + String funcName = renameInterface(inst); + // Also rename the function definition if it's separated from the + // declaration + SpecConstruct definition = _semantics.interfaceName2DefineConstruct + .get(construct.name); + if (definition != null) { + String funcDefintionName = renameInterface(definition); + assert (funcDefintionName.equals(funcName)); + } // Generate new wrapper breakCodeLines(newCode, funcDecl); + newCode.add("{"); - - // Generate - + + // Generate + // FIXME: Add Happens-before check here - + newCode.add("}"); CodeAddition addition = new CodeAddition(lineNum, newCode); if (!codeAdditions.containsKey(inst.file)) { @@ -230,8 +227,13 @@ public class CodeGenerator { } // Returns the function name that has been renamed and replace the old line - private String renameInterface(String funcDecl, ArrayList content, - int lineNum) throws InterfaceWrongFormatException { + private String renameInterface(SpecConstruct inst) + throws InterfaceWrongFormatException { + String funcDecl = inst.interfaceDeclBody; + ArrayList content = contents.get(inst.file); + + // Depending on "(" to find the function name, so it doesn't matter if + // there's any template int begin = 0, end = funcDecl.indexOf('('); if (end == -1) { throw new InterfaceWrongFormatException(funcDecl @@ -240,24 +242,31 @@ public class CodeGenerator { end--; while (end > 0) { char ch = funcDecl.charAt(end); - if (ch == '\n' || ch == '\t' || ch == ' ') - continue; + if (ch == '_' || (ch >= 'a' && ch <= 'z') + || (ch >= 'A' && ch <= 'Z') || (ch >= '0' && ch <= '9')) { + break; + } + end--; } begin = end; while (begin > 0) { char ch = funcDecl.charAt(begin); if (ch == '_' || (ch >= 'a' && ch <= 'z') || (ch >= 'A' && ch <= 'Z') || (ch >= '0' && ch <= '9')) { + begin--; continue; } + break; } String funcName = funcDecl.substring(begin + 1, end + 1), newLine; int lineBreakIdx = funcDecl.indexOf('\n'); - int firstLineBreak = lineBreakIdx == -1 ? funcDecl.length() : lineBreakIdx; + int firstLineBreak = lineBreakIdx == -1 ? funcDecl.length() + : lineBreakIdx; newLine = funcDecl.substring(0, begin + 1) + CodeVariables.SPEC_INTERFACE_WRAPPER + funcName + funcDecl.substring(end + 1, firstLineBreak); - content.set(lineNum, newLine); + // Be careful: lineNum - 1 -> index of content array + content.set(inst.endLineNum, newLine); return funcName; } @@ -310,11 +319,11 @@ public class CodeGenerator { e.printStackTrace(); } } else if (construct instanceof PotentialCPDefineConstruct) { - potentialCP2Code(inst); + // potentialCP2Code(inst); } else if (construct instanceof CPDefineConstruct) { - CPDefine2Code(inst); + // CPDefine2Code(inst); } else if (construct instanceof CPDefineCheckConstruct) { - CPDefineCheck2Code(inst); + // CPDefineCheck2Code(inst); } } } @@ -322,11 +331,12 @@ public class CodeGenerator { public static void main(String[] argvs) { String homeDir = Environment.HOME_DIRECTORY; File[] srcFiles = { - // new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c"), - new File(homeDir - + "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"), - // new File(homeDir + "/benchmark/ms-queue/my_queue.c") - }; + // new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c"), + // new File(homeDir + // + + // "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"), + new File(homeDir + "/benchmark/ms-queue/my_queue.c"), + new File(homeDir + "/benchmark/ms-queue/my_queue.h") }; CodeGenerator gen = new CodeGenerator(srcFiles); gen.generateCode(); } diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java index 301cd12..7e424e3 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java @@ -1,29 +1,81 @@ package edu.uci.eecs.specCompiler.codeGenerator; +import java.util.ArrayList; + +import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface; + public class CodeVariables { // C++ code or library public static final String ThreadIDType = "thread_id_t"; public static final String BOOLEAN = "bool"; - + + // Model checker code + public static final String HEADER_CDSAnnotate = "cdsannotate.h"; + public static final String CDSAnnotate = "cdsannotate"; + public static final String CDSAnnotateType = "SPEC_ANALYSIS"; + + public static final String SPEC_ANNOTATION_TYPE = "spec_anno_type"; + public static final String SPEC_ANNOTATION = "spec_annotation"; + + public static final String ANNO_HB_INIT = "anno_hb_init"; + public static final String ANNO_INTERFACE_BEGIN = "anno_interface_begin"; + public static final String ANNO_INTERFACE_END = "anno_interface_end"; + public static final String ANNO_ID = "anno_id"; + public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potentail_cp_define"; + public static final String ANNO_CP_DEFINE = "anno_cp_define"; + public static final String ANNO_CP_DEFINE_CHECK = "anno_cp_define_check"; + public static final String ANNO_HB_CONDITION = "anno_hb_condition"; + public static final String ANNO_POST_CHECK = "anno_post_check"; + // Specification variables - public static final String SPEC_CLASS = "Sequential"; + public static final String SPEC_STRUCT = "Sequential"; public static final String SPEC_INSTANCE = "__sequential"; + public static final String SPEC_CONDITION = "__cond"; public static final String SPEC_ID = "__id"; - public static final String SPEC_INTERFACE_ENUM = "_interface_t"; public static final String SPEC_INTERFACE = "__interface"; - + public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_"; - + // Specification library public static final String SPEC_QUEUE = "spec_queue"; public static final String SPEC_STACK = "spec_stack"; public static final String SPEC_HASHTABLE = "spec_hashtable"; public static final String SPEC_TAG = "spec_tag"; - + // Macro public static final String MACRO_ID = "__ID__"; public static final String MACRO_COND = "__COND_SAT__"; public static final String MACRO_RETURN = "__RET__"; - + + public static ArrayList generateHBInitAnnotation( + SemanticsChecker semantics) { + ArrayList newCode = new ArrayList(); + int hbConditionInitIdx = 0; + for (ConditionalInterface left : semantics.getHBConditions().keySet()) { + for (ConditionalInterface right : semantics.getHBConditions().get( + left)) { + String structVarName = "hbConditionInit" + hbConditionInitIdx; + hbConditionInitIdx++; + int interfaceNumBefore = semantics.interface2Num + .get(left.interfaceName), hbLabelNumBefore = semantics.hbLabel2Num + .get(left.hbConditionLabel), interfaceNumAfter = semantics.interface2Num + .get(right.interfaceName), hbLabelNumAfter = semantics.hbLabel2Num + .get(right.hbConditionLabel); + newCode.add(ANNO_HB_INIT + " " + structVarName + ";"); + + newCode.add(structVarName + "." + "interface_num_before" + + " = " + interfaceNumBefore + ";"); + newCode.add(structVarName + "." + "hb_condition_num_before" + + " = " + hbLabelNumBefore + ";"); + newCode.add(structVarName + "." + "interface_num_after" + " = " + + interfaceNumAfter + ";"); + newCode.add(structVarName + "." + "hb_condition_num_after" + + " = " + hbLabelNumAfter + ";"); + + newCode.add(CDSAnnotate + "(" + CDSAnnotateType + ", &" + structVarName + ");"); + } + } + return newCode; + } } diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java index 3bd801c..9eca53b 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java @@ -9,8 +9,10 @@ import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct; 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; @@ -19,27 +21,60 @@ public class SemanticsChecker { public final HashMap CPLabel2Construct; public final HashMap potentialCPLabel2Construct; public final HashMap interfaceName2Construct; + public final HashMap interfaceName2DefineConstruct; public final HashMap> CPLabel2InterfaceConstruct; public final HashSet defineVars; + + public final HashMap interface2Num; + public final HashMap hbLabel2Num; + public final HashMap commitPointLabel2Num; + + private HashMap options; + private HashMap> hbConditions; + private SpecConstruct entryPointConstruct; + + private int _interfaceNum; + private int _hbLabelNum; + private int _commitPointNum; public SemanticsChecker(ArrayList constructs) { this.constructs = constructs; this.CPLabel2Construct = new HashMap(); this.potentialCPLabel2Construct = new HashMap(); this.interfaceName2Construct = new HashMap(); + this.interfaceName2DefineConstruct = new HashMap(); this.CPLabel2InterfaceConstruct = new HashMap>(); this.defineVars = new HashSet(); + this.entryPointConstruct = null; + + this.interface2Num = new HashMap(); + this.hbLabel2Num = new HashMap(); + // Immediately init the true HB-condition to be 0 + hbLabel2Num.put("", 0); + + this.commitPointLabel2Num = new HashMap(); + + _interfaceNum = 0; + _hbLabelNum = 0; + _commitPointNum = 0; + } + + public HashMap> 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)) { @@ -47,17 +82,46 @@ 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) 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 @@ -65,16 +129,25 @@ public class SemanticsChecker { 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()); + CPLabel2InterfaceConstruct.put(label, + new ArrayList()); } CPLabel2InterfaceConstruct.get(label).add(iConstruct); } @@ -93,10 +166,15 @@ public class SemanticsChecker { 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 +183,70 @@ public class SemanticsChecker { 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"); diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/SpecConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/SpecConstruct.java index 95650cc..e80cbd7 100644 --- a/src/edu/uci/eecs/specCompiler/specExtraction/SpecConstruct.java +++ b/src/edu/uci/eecs/specCompiler/specExtraction/SpecConstruct.java @@ -46,10 +46,10 @@ public class SpecConstruct { sb.append("Begin: " + beginLineNum + " End: " + endLineNum + "\n"); sb.append(construct); - if (construct instanceof InterfaceConstruct) { + if (construct instanceof InterfaceConstruct + || construct instanceof InterfaceDefineConstruct) { sb.append("Function declaration: " + interfaceDeclBody); } - boolean a = !false, b = 3 > 0 ? a : !a; return sb.toString(); } diff --git a/test.c b/test.c index 2dec27e..417f795 100644 --- a/test.c +++ b/test.c @@ -1,6 +1,14 @@ #include #include "test.h" +struct XX { + +}; + +enum E { + a, b, c +}; + void _foo(struct Test t) { printf("%d\n", t.x); } @@ -10,5 +18,6 @@ void foo(struct Test t) { } int main() { + printf("%d\n", b); return 0; } diff --git a/test.cc b/test.cc deleted file mode 100644 index c7cb0db..0000000 --- a/test.cc +++ /dev/null @@ -1,81 +0,0 @@ -#include -#include -#include - -using namespace std; - - -template -class A { - private: - int outer; - class B { - private: - vector v; - T str; - public: - typedef struct C { - T x; - } C_t; - - enum interface_t {put, get}; - B() { - v = vector(); - str = "abc"; - - } - - void _pushBack(int a) { - cout << str << endl; - v.push_back(a); - } - - int _size() { - return v.size(); - } - - C_t func() { - char *cStr = "struct_ab"; - C_t c; - c.x = cStr; - return c; - } - } b; - - public: - A() { - } - - void pushBack(int a) { - //printf("Size: %d\n", b.size()); - b._pushBack(a); - //printf("Size: %d\n", b.size()); - } - - int size() { - //B::interface_t inter; - struct B::C_t c = b.func(); - enum B::interface_t a = B::put; - vector ve(3); - ve.push_back(B::put); - cout << "Size: " << ve.size() << endl; - cout << b.func().x << endl; - return b._size(); - } -}; - -int main() { - #define __COND_SAT__ a.size() - A a; - a.pushBack(1); - if (__COND_SAT__ != 0) { - cout << "Size greater than 0" << endl; - } - #undef __COND_SAT__ - - bool __COND_SAT__ = false; - if (!__COND_SAT__) { - cout << "False!" << endl; - } - return 0; -} diff --git a/test.h b/test.h index fb016e4..0b752a3 100644 --- a/test.h +++ b/test.h @@ -1,7 +1,8 @@ struct Test { int x; - +/* Test() { x = 2; } + */ }; -- 2.34.1