+
+ public static ArrayList<String> generateInterfaceWrapper(
+ SemanticsChecker semantics, SpecConstruct inst) {
+ InterfaceConstruct construct = (InterfaceConstruct) inst.construct;
+ ArrayList<String> newCode = new ArrayList<String>();
+ String funcDecl = inst.interfaceDeclBody.substring(0,
+ inst.interfaceDeclBody.indexOf(')') + 1);
+ String returnType = getFuncReturnType(funcDecl), funcName = getFuncName(funcDecl), renamedFuncName = SPEC_INTERFACE_WRAPPER
+ + funcName;
+ ArrayList<String> args = getFuncArgs(funcDecl);
+
+ // Generate necessary header file (might be redundant but never mind)
+ newCode.add(COMMENT("Automatically generated code for interface: "
+ + construct.name));
+ newCode.add(COMMENT("Include redundant headers"));
+ newCode.add(INCLUDE(HEADER_THREADS));
+ newCode.add(INCLUDE(HEADER_CDSANNOTATE));
+ newCode.add(INCLUDE(HEADER_SPECANNOTATION));
+ newCode.add(INCLUDE(HEADER_SPEC_TAG));
+ newCode.add(INCLUDE(HEADER_SPEC_PRIVATE_HASHTABLE));
+ newCode.add("");
+
+ // Generate wrapper header
+ newCode.add(COMMENT("Wrapper for " + SPEC_INTERFACE_WRAPPER + funcName));
+ breakCodeLines(newCode, funcDecl);
+ newCode.add("{");
+
+ // Wrapper function body
+ newCode.add(DECLARE_DEFINE(ThreadIDType, VAR_ThreadID, GET_THREAD_ID
+ + BRACE("")));
+ newCode.add(DECLARE_DEFINE(UINT64, VAR_CALL_SEQUENCE_NUM,
+ SPEC_TAG_CURRENT + BRACE(VAR_PTR(SPEC_GLOBAL_CALL_SEQUENCE))));
+ newCode.add(SPEC_TAG_NEXT + BRACE(VAR_PTR(SPEC_GLOBAL_CALL_SEQUENCE)));
+ newCode.add(PUT(SPEC_INTERFACE_CALL_SEQUENCE, VAR_ThreadID,
+ VAR_CALL_SEQUENCE_NUM));
+ // Interface begin
+ newCode.add("");
+ newCode.add(COMMENT("Interface begin"));
+ String interfaceName = construct.name;
+ String annoStruct = "interface_boundary", interfaceNum = Integer
+ .toString(semantics.interface2Num.get(interfaceName));
+ newCode.add(DECLARE(ANNO_INTERFACE_BOUNDARY, annoStruct));
+ newCode.add(ASSIGN(annoStruct, "interface_num", interfaceNum));
+ newCode.add(ASSIGN(annoStruct, "call_sequence_num",
+ VAR_CALL_SEQUENCE_NUM));
+ String anno = "annotation_interface_begin";
+ newCode.add(DECLARE(SPEC_ANNOTATION, anno));
+ newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
+ SPEC_ANNO_TYPE_INTERFACE_BEGIN));
+ newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
+ newCode.add(ANNOTATE(anno));
+ // Call original renamed function
+ String funcCall = renamedFuncName + "(";
+ if (args.size() == 0) {
+ funcCall = funcCall + ")";
+ } else {
+ funcCall = funcCall + args.get(0);
+ for (int i = 1; i < args.size(); i++) {
+ funcCall = funcCall + ", " + args.get(i);
+ }
+ funcCall = funcCall + ")";
+ }
+ newCode.add(DECLARE_DEFINE(returnType, MACRO_RETURN, funcCall));
+ newCode.add(DECLARE_DEFINE("int", MACRO_COND, GET(SPEC_CONDITION)));
+ newCode.add(DECLARE_DEFINE(UINT64, MACRO_ID, GET(SPEC_ID)));
+ // Post check & action
+ newCode.add("");
+ newCode.add(COMMENT("Post_check action, define macros for all DefineVars"));
+ // Define all DefineVar macro
+ ArrayList<DefineVar> defineVars = construct.action.defineVars;
+ for (int i = 0; i < defineVars.size(); i++) {
+ DefineVar var = defineVars.get(i);
+ newCode.add(DEFINE(var.varName, BRACE(GET(interfaceName + "_"
+ + var.varName))));
+ }
+ // Post check
+ newCode.add(DECLARE_DEFINE("bool", "post_check_passed",
+ construct.postCheck));
+ annoStruct = "post_check";
+ newCode.add(DECLARE(ANNO_POST_CHECK, annoStruct));
+ newCode.add(ASSIGN(annoStruct, "check_passed", "post_check_passed"));
+ newCode.add(ASSIGN(annoStruct, "interface_num", interfaceNum));
+ newCode.add(ASSIGN(annoStruct, "call_sequence_num",
+ VAR_CALL_SEQUENCE_NUM));
+ anno = "annotation_post_check";
+ newCode.add(DECLARE(SPEC_ANNOTATION, anno));
+ newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
+ SPEC_ANNO_TYPE_POST_CHECK));
+ newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
+ newCode.add(ANNOTATE(anno));
+ // Post action if any
+ breakCodeLines(newCode, construct.postAction);
+ // Undefine all DefineVar macro
+ for (int i = 0; i < defineVars.size(); i++) {
+ DefineVar var = defineVars.get(i);
+ newCode.add(UNDEFINE(var.varName));
+ }
+ // HB conditions
+ newCode.add("");
+ for (String label : construct.hbConditions.keySet()) {
+ String hbCondition = construct.hbConditions.get(label);
+ newCode.add(COMMENT("Happens-before condition for " + label
+ + " ::= " + hbCondition));
+ newCode.add("if " + BRACE(hbCondition) + " {");
+ String hbNum = Integer.toString(semantics.hbLabel2Num.get(label));
+ annoStruct = "hb_condition" + hbNum;
+ newCode.add(DECLARE(ANNO_HB_CONDITION, annoStruct));
+ newCode.add(ASSIGN(annoStruct, "interface_num", interfaceNum));
+ newCode.add(ASSIGN(annoStruct, "hb_condition_num", hbNum));
+ newCode.add(ASSIGN(annoStruct, "id", MACRO_ID));
+ newCode.add(ASSIGN(annoStruct, "call_sequence_num",
+ VAR_CALL_SEQUENCE_NUM));
+ anno = "annotation_hb_condition";
+ newCode.add(DECLARE(SPEC_ANNOTATION, anno));
+ newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
+ SPEC_ANNO_TYPE_HB_CONDITION));
+ newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
+ ANNOTATE(anno);
+ newCode.add("} " + COMMENT("End of HB condition " + label));
+ newCode.add("");
+ }
+ // Interface end
+ annoStruct = "interface_boundary";
+ anno = "annotation_interface_end";
+ newCode.add(DECLARE(SPEC_ANNOTATION, anno));
+ newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
+ SPEC_ANNO_TYPE_INTERFACE_END));
+ newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
+ newCode.add(ANNOTATE(anno));
+
+ // End of the wrapper function
+ newCode.add("} "
+ + COMMENT("End of automatically generated code for interface wrapper"));
+
+ printCode(newCode);
+ return newCode;
+ }
+
+ public static ArrayList<String> generatePotentialCPDefine(
+ SemanticsChecker semantics, SpecConstruct inst) {
+ PotentialCPDefineConstruct construct = (PotentialCPDefineConstruct) inst.construct;
+ ArrayList<String> newCode = new ArrayList<String>();
+
+ // Generate redundant header files
+ newCode.add(COMMENT("Automatically generated code for potential commit point: "
+ + construct.label));
+ newCode.add(COMMENT("Include redundant headers"));
+ newCode.add(INCLUDE(HEADER_THREADS));
+ newCode.add(INCLUDE(HEADER_CDSTRACE));
+ newCode.add(INCLUDE(HEADER_SPEC_PRIVATE_HASHTABLE));
+ newCode.add(INCLUDE(HEADER_SPEC_SEQUENTIAL));
+ newCode.add("");
+ // Some necessary function calls
+ newCode.add(DECLARE_DEFINE(ThreadIDType, VAR_ThreadID, GET_THREAD_ID
+ + BRACE("")));
+ newCode.add(DECLARE_DEFINE(UINT64, MACRO_ATOMIC_RETURN,
+ GET_PREV_ATOMIC_VAL + BRACE(VAR_ThreadID)));
+ newCode.add("if " + BRACE(construct.condition) + " {");
+ newCode.add(DECLARE_DEFINE(UINT64, VAR_CALL_SEQUENCE_NUM,
+ GET(SPEC_INTERFACE_CALL_SEQUENCE)));
+ String annoStruct = "potential_cp_define";
+ newCode.add(DECLARE(ANNO_POTENTIAL_CP_DEFINE, annoStruct));
+ newCode.add(ASSIGN(annoStruct, "interface_num", GET(SPEC_INTERFACE)));
+ String labelNum = Integer.toString(semantics.commitPointLabel2Num
+ .get(construct.label));
+ newCode.add(ASSIGN(annoStruct, "label_num", labelNum));
+ newCode.add(ASSIGN(annoStruct, "call_sequence_num",
+ VAR_CALL_SEQUENCE_NUM));
+ String anno = "annotation_potential_cp_define";
+ newCode.add(DECLARE(SPEC_ANNOTATION, anno));
+ newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
+ SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE));
+ newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
+ ANNOTATE(anno);
+
+ newCode.add("} "
+ + COMMENT("End of automatically generated code for potential commit point"));
+
+ return newCode;
+ }