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:
@Potential_commit_point_label: ...
@Label: ...
@End
+
+ e) Entry point construct
+ @Begin
+ @Entry_point
+ @End
+
+ f) Interface define construct
+ @Begin
+ @Interface_define: <Interface_Name>
+ @End
*/
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)
<BEGIN: "@Begin">
|
<END: "@End">
+|
+ <OPTIONS: "@Options:">
|
<GLOBAL_DEFINE: "@Global_define:">
|
<INTERFACE: "@Interface:">
|
<COMMIT_POINT_SET: "@Commit_point_set:">
+|
+ <ENTRY_POINT: "@Entry_point">
+|
+ <INTERFACE_DEFINE: "@Interface_define:">
|
<CONDITION: "@Condition:">
|
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()
)
<EOF>
{
{
GlobalConstruct res;
SequentialDefineSubConstruct code;
+ HashMap<String, String> options;
+ String key, value;
}
{
- { res = null; }
+ {
+ res = null;
+ options = new HashMap<String, String>();
+ }
<HEAD>
<BEGIN>
+ (<OPTIONS>
+ ((key = <IDENTIFIER>.image)
+ <EQUALS>
+ (value = <IDENTIFIER>.image)
+ {
+ if (options.containsKey(key)) {
+ throw new ParseException("Duplicate options!");
+ }
+ options.put(key, value);
+ }
+ <SEMI_COLON>
+ )*
+ )?
(code = Global_define())
- { res = new GlobalConstruct(code); }
+ { res = new GlobalConstruct(code, options); }
(Interface_clusters(res))?
(Happens_before(res))?
<END>
initVar = "";
defineFunc = "";
}
- <GLOBAL_DEFINE>
- (<DECLARE_VAR> (declareVar = C_CPP_CODE()))?
+ <GLOBAL_DEFINE>
+ (<DECLARE_VAR> (declareVar = C_CPP_CODE()))?
(<INIT_VAR> (initVar = C_CPP_CODE()))?
(<DEFINE_FUNC> (defineFunc = C_CPP_CODE()))?
{
return res;
}
}
+
+EntryPointConstruct Entry_point() :
+{}
+{
+
+ <HEAD>
+ <BEGIN>
+ <ENTRY_POINT>
+ <END>
+ <TAIL>
+ {
+ return new EntryPointConstruct();
+ }
+}
+
+InterfaceDefineConstruct Interface_define() :
+{
+ String name;
+}
+{
+ <HEAD>
+ <BEGIN>
+ <INTERFACE_DEFINE> (name = <IDENTIFIER>.image)
+ <END>
+ <TAIL>
+ {
+ return new InterfaceDefineConstruct(name);
+ }
+}
+
+
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;
GlobalConstruct construct = (GlobalConstruct) inst.construct;
ArrayList<String> newCode = new ArrayList<String>();
- // 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()) {
ArrayList<DefineVar> 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<String> 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 + "<enum "
- + CodeVariables.SPEC_INTERFACE_ENUM + "> "
- + 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<DefineVar> 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 + "<enum "
- + CodeVariables.SPEC_INTERFACE_ENUM + ">();");
- // 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);
// Rename the interface name
File file = inst.file;
- ArrayList<String> 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)) {
}
// Returns the function name that has been renamed and replace the old line
- private String renameInterface(String funcDecl, ArrayList<String> content,
- int lineNum) throws InterfaceWrongFormatException {
+ private String renameInterface(SpecConstruct inst)
+ throws InterfaceWrongFormatException {
+ String funcDecl = inst.interfaceDeclBody;
+ ArrayList<String> 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
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;
}
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);
}
}
}
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();
}
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<String> generateHBInitAnnotation(
+ SemanticsChecker semantics) {
+ ArrayList<String> newCode = new ArrayList<String>();
+ 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;
+ }
}
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");
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();
}
#include <stdio.h>
#include "test.h"
+struct XX {
+
+};
+
+enum E {
+ a, b, c
+};
+
void _foo(struct Test t) {
printf("%d\n", t.x);
}
}
int main() {
+ printf("%d\n", b);
return 0;
}
+++ /dev/null
-#include <stdio.h>
-#include <iostream>
-#include <vector>
-
-using namespace std;
-
-
-template<typename T>
-class A {
- private:
- int outer;
- class B {
- private:
- vector<int> v;
- T str;
- public:
- typedef struct C {
- T x;
- } C_t;
-
- enum interface_t {put, get};
- B() {
- v = vector<int>();
- 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<T>::interface_t inter;
- struct B::C_t c = b.func();
- enum B::interface_t a = B::put;
- vector<enum B::interface_t> 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<string> 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;
-}
struct Test {
int x;
-
+/*
Test() {
x = 2;
}
+ */
};