From 3e65b0d466278eaf5cbd93ff01404e1cd1a8404d Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Mon, 21 Oct 2013 18:33:01 -0700 Subject: [PATCH] generate more structured code --- notes/generated_code_examples.txt | 41 +- .../codeGenerator/CodeGenerator.java | 173 +----- .../codeGenerator/CodeVariables.java | 506 ++++++++++++++---- .../codeGenerator/IDExtractor.java | 120 +++++ .../specExtraction/SpecExtractor.java | 5 +- test.c | 26 +- test.h | 2 + 7 files changed, 585 insertions(+), 288 deletions(-) create mode 100644 src/edu/uci/eecs/specCompiler/codeGenerator/IDExtractor.java diff --git a/notes/generated_code_examples.txt b/notes/generated_code_examples.txt index 5dc22b7..b8d9707 100644 --- a/notes/generated_code_examples.txt +++ b/notes/generated_code_examples.txt @@ -10,13 +10,15 @@ Global Variable Declaration #define __SPEC_SEQUENTIAL_GENERATED_H #include #include +#include /* Beginning of struct Sequential */ typedef struct Sequential { - spec_private_hashtable cond; + spec_private_hashtable condition; spec_private_hashtable id; spec_private_hashtable interface; spec_private_hashtable interface_call_sequence; + Tag global_call_sequence; /* DefineVar unfolded here */ spec_private_hashtable Put__Old_Val; @@ -34,15 +36,29 @@ Sequential __sequential; /* Define function for sequential code initialization */ void __sequential_init() { /* Init internal variables */ - init(&__sequential.cond); + init(&__sequential.condition); init(&__sequential.id); init(&__sequential.interface); init(&__sequential.interface_call_sequence); + init(&global_call_sequence); /* Init DefineVars */ init(&__sequential.Put__Old_Val); /* Init user-defined variables */ lock_acquired = false; reader_lock_cnt = 0; + + /* Pass the happens-before initialization here */ + /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */ + anno_hb_init hbConditionInit0; + hbConditionInit0.interface_num_before = 1; + hbConditionInit0.hb_condition_num_before = 1; + hbConditionInit0.interface_num_after = 2; + hbConditionInit0.hb_condition_num_after = 0; + spec_annotation hb_init0; + hb_init0.type = HB_INIT; + hb_init0.annotation = &hbConditionInit0; + cdsannotate(SPEC_ANALYSIS, &hb_init0); + } /* All other user-defined functions */ @@ -59,12 +75,15 @@ Interface Wrapper #include #include #include +#include +#include TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2) { thrd_t tid = thrd_current(); - uint64_t call_sequence_num = current(&__interface_call_sequence); - put(&__interface_call_sequence, tid, call_sequence_num); + uint64_t call_sequence_num = current(&__sequential.global_call_sequence); + next(&__sequential.global_call_sequence); + put(&__sequential.interface_call_sequence, tid, call_sequence_num); // Interface begins anno_interface_boundary interface_boundary; @@ -76,15 +95,13 @@ TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2) cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin); TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2); - int __COND__ = get(&__sequential.cond, tid); + int __COND__ = get(&__sequential.condition, tid); uint64_t __ID__ = get(&__sequential.id, tid); /* Post_check action, define macros for all DefineVars */ #define _Old_Val (get(&__sequential.put__Old_Val, tid)) // And more... bool post_check_passed = INTERFACE_POST_CHECK_CONDITION; - #undef _Old_Val - // And more... anno_post_check post_check; post_check.check_passed = post_check_passed; @@ -97,13 +114,15 @@ TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2) // Post Action (if any) POST_ACTION_CODE // Unfolded in place + #undef _Old_Val + // And more... // HB conditions (if any) if (HB_CONDITION1) { anno_hb_condition hb_condition1; hb_condition1.interface_num = 0; // Interface number hb_condition1.hb_condition_num = 1; // HB condition number - hb_condition1.id = id; + hb_condition1.id = __ID__; hb_condition1.call_sequence_num = call_sequence_num; spec_annotation annotation_hb_condition; annotation_hb_condition.type = HB_CONDITION; @@ -129,13 +148,13 @@ Potential Commit Point #include #include <_sepc_sequential_genenrated.h> -thrd_t __tid = thrd_current(); +thrd_t tid = thrd_current(); uint64_t __ATOMIC_RET__ = get_prev_value(tid); if (POTENTIAL_CP_DEFINE_CONDITION) { uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid); - int interface_num = get(&__sequential.interface, tid); + anno_potential_cp_define potential_cp_define; - potential_cp_define.interface_num = interface_num; + potential_cp_define.interface_num = get(&__sequential.interface, tid); potential_cp_define.label_num = 1; // Commit point label number potential_cp_define.call_sequence_num = call_sequence_num; spec_annotation annotation_potential_cp_define; diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index c69473a..3569e20 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -41,9 +41,12 @@ public class CodeGenerator { private HashMap> codeAdditions; + private ArrayList globalContent; + public CodeGenerator(File[] srcFiles) { this.srcFiles = srcFiles; this.contents = new HashMap>(); + this.globalContent = null; readSrcFiles(); this.codeAdditions = new HashMap>(); @@ -94,103 +97,11 @@ public class CodeGenerator { *

*/ private void globalConstruct2Code(SpecConstruct inst) { - int lineNum = inst.endLineNum + 1; GlobalConstruct construct = (GlobalConstruct) inst.construct; - ArrayList newCode = new ArrayList(); - - // Generate all sequential variables into a struct - newCode.add("struct " + CodeVariables.SPEC_SEQUENTIAL_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.SPEC_CONDITION - + ";"); - // __ID__ - newCode.add(CodeVariables.SPEC_HASHTABLE + 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(CodeVariables.SPEC_HASHTABLE + var.getNewVarName() - + ";"); - } - } - // __interface - newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_INTERFACE - + ";"); - // __interface_call_sequence - newCode.add(CodeVariables.SPEC_HASHTABLE - + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ";"); - // Interface call sequence varaiable - newCode.add(CodeVariables.SPEC_TAG + " " - + CodeVariables.INTERFACE_CALL_SEQUENCE + ";"); - // 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("init_table(&" + CodeVariables.SPEC_CONDITION + ");"); - // __ID__ - 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("init_table(&" + CodeVariables.SPEC_INTERFACE + ");"); - // __interface_call_sequence - newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ");"); - - // Pass the happens-before relationship check here - newCode.addAll(CodeVariables.generateHBInitAnnotation(_semantics)); - - newCode.add("\n"); - - // Generate the sequential functions - breakCodeLines(newCode, globalCode.defineFunc); - - printCode(newCode); - - CodeAddition addition = new CodeAddition(lineNum, newCode); - if (!codeAdditions.containsKey(inst.file)) { - codeAdditions.put(inst.file, new ArrayList()); - } - codeAdditions.get(inst.file).add(addition); - } - - // Break the code (String) into multiple lines and add it to newCode - private void breakCodeLines(ArrayList newCode, String code) { - int begin = 0, end = 0; - while (end < code.length()) { - if (code.charAt(end) == '\n') { - String line = code.substring(begin, end); - newCode.add(line); - begin = end + 1; - } - end++; - } - } - - private void printCode(ArrayList code) { - for (int i = 0; i < code.size(); i++) { - System.out.println(code.get(i)); - } + ArrayList newCode = CodeVariables.generateGlobalVarDeclaration( + _semantics, construct); + // Record the global content array to generate the new file + globalContent = newCode; } // Mainly rename and wrap the interface @@ -198,8 +109,7 @@ public class CodeGenerator { throws InterfaceWrongFormatException { int lineNum = inst.endLineNum + 1; InterfaceConstruct construct = (InterfaceConstruct) inst.construct; - ArrayList newCode = new ArrayList(); - + // Rename the interface name File file = inst.file; String funcDecl = inst.interfaceDeclBody; @@ -215,19 +125,8 @@ public class CodeGenerator { } // Generate new wrapper - /** - * - * - */ - - breakCodeLines(newCode, funcDecl); - newCode.add("{"); - // Generate interface sequence call - newCode.add(CodeVariables.UINT64 + " call_sequence_num = current(&" - + CodeVariables.INTERFACE_CALL_SEQUENCE + ");"); - // FIXME: Add Happens-before check here - newCode.add("}"); - + ArrayList newCode = CodeVariables.generateInterfaceWrapper(_semantics, inst); + // Add it to the codeAdditions CodeAddition addition = new CodeAddition(lineNum, newCode); if (!codeAdditions.containsKey(inst.file)) { codeAdditions.put(inst.file, new ArrayList()); @@ -243,39 +142,24 @@ public class CodeGenerator { // 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) { + int beginIdx = funcDecl.indexOf('('); + if (beginIdx == -1) { throw new InterfaceWrongFormatException(funcDecl + "\n has wrong format!"); } - end--; - while (end > 0) { - char ch = funcDecl.charAt(end); - 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; - newLine = funcDecl.substring(0, begin + 1) + IDExtractor idExtractor = new IDExtractor(funcDecl, beginIdx); + String funcName = idExtractor.getPrevID(); + int idBeginIdx = idExtractor.getIDBeginIdx(), + idEndIdx = idExtractor.getIDEndIdx(), + idLineBeginIdx = idExtractor.lineBeginIdxOfID(), + idLineEndIdx = idExtractor.lineEndIdxOfID(); + String newLine = funcDecl.substring(idLineBeginIdx, idBeginIdx) + CodeVariables.SPEC_INTERFACE_WRAPPER + funcName - + funcDecl.substring(end + 1, firstLineBreak); + + funcDecl.substring(idEndIdx + 1, idLineEndIdx + 1); + + int lineNumOfID = idExtractor.lineNumOfID(); // Be careful: lineNum - 1 -> index of content array - content.set(inst.endLineNum, newLine); + content.set(inst.endLineNum + lineNumOfID, newLine); return funcName; } @@ -340,12 +224,11 @@ 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/ms-queue/my_queue.h") }; + // 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 4ee3e3d..d2fe6b8 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java @@ -5,27 +5,38 @@ import java.util.ArrayList; import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface; import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct; import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct; +import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct; import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct; +import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor; import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar; +import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct; public class CodeVariables { // C++ code or library - public static final String HEADER_threads = "threads.h"; + public static final String HEADER_THREADS = "threads.h"; public static final String ThreadIDType = "thrd_t"; public static final String GET_THREAD_ID = "thrd_current"; public static final String BOOLEAN = "bool"; public static final String UINT64 = "uint64_t"; // Model checker code - public static final String HEADER_CDSAnnotate = "cdsannotate.h"; + public static final String HEADER_CDSANNOTATE = "cdsannotate.h"; public static final String HEADER_SPECANNOTATION = "specannotation.h"; + public static final String HEADER_CDSTRACE = "cdstrace.h"; public static final String CDSAnnotate = "cdsannotate"; public static final String CDSAnnotateType = "SPEC_ANALYSIS"; - // It's a SPEC_TAG type, it has current() and next() function - public static final String INTERFACE_CALL_SEQUENCE = "__interface_call_sequence"; + public static final String GET_PREV_ATOMIC_VAL = "get_prev_value"; - public static final String SPEC_ANNOTATION_TYPE = "spec_anno_type"; + public static final String SPEC_ANNO_TYPE = "spec_anno_type"; + public static final String SPEC_ANNO_TYPE_HB_INIT = "HB_INIT"; + public static final String SPEC_ANNO_TYPE_INTERFACE_BEGIN = "INTERFACE_BEGIN"; + public static final String SPEC_ANNO_TYPE_POST_CHECK = "POST_CHECK"; + public static final String SPEC_ANNO_TYPE_HB_CONDITION = "HB_CONDITION"; + public static final String SPEC_ANNO_TYPE_INTERFACE_END = "INTERFACE_END"; + public static final String SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE = "POTENTIAL_CP_DEFINE"; public static final String SPEC_ANNOTATION = "spec_annotation"; + public static final String SPEC_ANNOTATION_FIELD_TYPE = "type"; + public static final String SPEC_ANNOTATION_FIELD_ANNO = "annotation"; public static final String ANNO_HB_INIT = "anno_hb_init"; public static final String ANNO_INTERFACE_BOUNDARY = "anno_interface_boundary"; @@ -37,8 +48,8 @@ public class CodeVariables { public static final String ANNO_POST_CHECK = "anno_post_check"; // Specification variables - public static final String SPEC_SEQUENTIAL_HEADER = "_spec_sequential.h"; - public static final String SPEC_SEQUENTIAL_HEADER_MACRO = SPEC_SEQUENTIAL_HEADER + public static final String HEADER_SPEC_SEQUENTIAL = "_spec_sequential.h"; + public static final String SPEC_SEQUENTIAL_HEADER_MACRO = HEADER_SPEC_SEQUENTIAL .replace('.', '_').toUpperCase(); public static final String SPEC_SEQUENTIAL_STRUCT = "Sequential"; public static final String SPEC_SEQUENTIAL_INSTANCE = "__sequential"; @@ -47,21 +58,30 @@ public class CodeVariables { public static final String SPEC_ID = "id"; public static final String SPEC_INTERFACE = "interface"; public static final String SPEC_INTERFACE_CALL_SEQUENCE = "interface_call_sequence"; + public static final String SPEC_GLOBAL_CALL_SEQUENCE = "global_call_sequence"; public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_"; + public static final String VAR_ThreadID = "tid"; + public static final String VAR_CALL_SEQUENCE_NUM = "call_sequence_num"; + // Specification library public static final String SPEC_QUEUE = "spec_queue"; public static final String SPEC_STACK = "spec_stack"; + public static final String SPEC_DEQUE = "spec_deque"; public static final String SPEC_HASHTABLE = "spec_hashtable"; - public static final String SPEC_PRIVATE_HASHTABLE_HEADER = "spec_private_hashtable.h"; + public static final String HEADER_SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable.h"; public static final String SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable"; + public static final String HEADER_SPEC_TAG = "spec_tag.h"; public static final String SPEC_TAG = "spec_tag"; + public static final String SPEC_TAG_CURRENT = "current"; + public static final String SPEC_TAG_NEXT = "next"; // 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 final String MACRO_ATOMIC_RETURN = "__ATOMIC_RET__"; // Break the code (String) into multiple lines and add it to newCode private static void breakCodeLines(ArrayList newCode, String code) { @@ -76,132 +96,218 @@ public class CodeVariables { } } - private static void printCode(ArrayList code) { + public static void printCode(ArrayList code) { for (int i = 0; i < code.size(); i++) { System.out.println(code.get(i)); } } - + + public static String getFuncName(String funcDecl) { + int beginIdx = funcDecl.indexOf('('); + IDExtractor idExtractor = new IDExtractor(funcDecl, beginIdx); + return idExtractor.getPrevID(); + } + + public static String getFuncReturnType(String funcDecl) { + int beginIdx = funcDecl.indexOf('('); + IDExtractor idExtractor = new IDExtractor(funcDecl, beginIdx); + idExtractor.getPrevID(); + int idLineBegin = idExtractor.lineBeginIdxOfID(), idBegin = idExtractor + .getIDBeginIdx(); + String type = funcDecl.substring(idLineBegin, idBegin); + return SpecExtractor.trimSpace(type); + } + + public static ArrayList getFuncArgs(String funcDecl) { + ArrayList args = new ArrayList(); + int beginIdx = funcDecl.indexOf('('), endIdx = funcDecl.indexOf(')'); + IDExtractor idExtractor = new IDExtractor(funcDecl, endIdx); + String arg = idExtractor.getPrevID(); + // Void argument + if (arg == null || idExtractor.getIDBeginIdx() < beginIdx) { + return args; + } else { + args.add(arg); + } + + do { + endIdx = funcDecl.lastIndexOf(',', endIdx); + if (endIdx == -1) { + return args; + } + idExtractor.reset(endIdx); + args.add(idExtractor.getPrevID()); + } while (true); + } + + private static String COMMENT(String comment) { + return "/* " + comment + " */"; + } + + private static String GET(String var) { + return "get(&" + VAR(var) + ", " + VAR_ThreadID + ")"; + } + + private static String PUT(String var, String tid, String val) { + return "put(&" + VAR(var) + ", " + tid + ", " + val + ");"; + } + + private static String INIT(String var) { + return "init(&" + VAR(var) + ");"; + } + + private static String INCLUDE(String header) { + return "#include <" + header + ">"; + } + + private static String DEFINE(String left, String right) { + return "#define " + left + " " + right; + } + + private static String UNDEFINE(String macro) { + return "#undef " + macro; + } + + private static String VAR(String var) { + return SPEC_SEQUENTIAL_INSTANCE + "." + var; + } + + private static String BRACE(String val) { + return "(" + val + ")"; + } + + private static String VAR_PTR(String var) { + return "&" + SPEC_SEQUENTIAL_INSTANCE + "." + var; + } + + private static String ASSIGN(String structName, String field, String val) { + return structName + "." + field + " = " + val + ";"; + } + + private static String ASSIGN_PTR(String structName, String field, String val) { + return structName + "." + field + " = &" + val + ";"; + } + + private static String DECLARE(String structType, String structName) { + return structType + " " + structName + ";"; + } + + private static String DECLARE_DEFINE(String type, String var, String val) { + return type + " " + var + " = " + val + ";"; + } + + private static String ANNOTATE(String structName) { + return CDSAnnotate + "(" + CDSAnnotateType + ", &" + structName + ");"; + } + public static ArrayList generateGlobalVarDeclaration( SemanticsChecker semantics, GlobalConstruct construct) { ArrayList newCode = new ArrayList(); // Header conflicting avoidance macro & headers - newCode.add("/** @file " + SPEC_SEQUENTIAL_HEADER); + newCode.add("/** @file " + HEADER_SPEC_SEQUENTIAL); newCode.add(" * @brief Automatically generated header file for sequential variables"); newCode.add(" */"); newCode.add("#ifndef " + SPEC_SEQUENTIAL_HEADER_MACRO); newCode.add("#define " + SPEC_SEQUENTIAL_HEADER_MACRO); - newCode.add("#include " + "<" + SPEC_PRIVATE_HASHTABLE_HEADER + ">"); - newCode.add("#include " + "<" + HEADER_SPECANNOTATION + ">"); + newCode.add(""); + newCode.add(INCLUDE(HEADER_SPEC_PRIVATE_HASHTABLE)); + newCode.add(INCLUDE(HEADER_SPECANNOTATION)); + newCode.add(INCLUDE(HEADER_SPEC_TAG)); + newCode.add(""); // Generate all sequential variables into a struct - newCode.add("/* Beginning of struct " + SPEC_SEQUENTIAL_STRUCT + " */"); + newCode.add(COMMENT("Beginning of struct " + SPEC_SEQUENTIAL_STRUCT)); newCode.add("typedef struct " + SPEC_SEQUENTIAL_STRUCT + " {"); - newCode.add("/* Condition of interface */"); - newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_CONDITION + ";"); - newCode.add("/* ID of interface */"); - newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_ID + ";"); - newCode.add("/* Current interface call */"); - newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_INTERFACE + ";"); - newCode.add("/* Current interface call sequence */"); - newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_INTERFACE_CALL_SEQUENCE - + ";"); + newCode.add(COMMENT("Condition")); + newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE, SPEC_CONDITION)); + newCode.add(COMMENT("ID")); + newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE, SPEC_ID)); + newCode.add(COMMENT("Current interface call")); + newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE, SPEC_INTERFACE)); + newCode.add(COMMENT("Current interface call sequence")); + newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE, + SPEC_INTERFACE_CALL_SEQUENCE)); + newCode.add(COMMENT("Global interface call sequence number")); + newCode.add(DECLARE(SPEC_TAG, SPEC_GLOBAL_CALL_SEQUENCE)); newCode.add(""); // DefineVar declaration for (String interfaceName : semantics.interfaceName2Construct.keySet()) { InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct .get(interfaceName).construct; ArrayList defineVars = iConstruct.action.defineVars; - newCode.add("/* DefineVar in " + interfaceName + " */"); - for (int i = 0; i < defineVars.size(); i++) { - DefineVar var = defineVars.get(i); - newCode.add(SPEC_PRIVATE_HASHTABLE + " " + var.getNewVarName() - + ";"); + if (defineVars.size() > 0) { + newCode.add(COMMENT("DefineVar in " + interfaceName)); + for (int i = 0; i < defineVars.size(); i++) { + DefineVar var = defineVars.get(i); + newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE, + var.getNewVarName())); + } } newCode.add(""); } // Generate user-defined variable declaration - newCode.add("/* Beginnint of other user-defined variables */"); + newCode.add(COMMENT("Beginnint of other user-defined variables")); SequentialDefineSubConstruct globalCode = construct.code; breakCodeLines(newCode, globalCode.declareVar); - newCode.add("/* End of other user-defined variables */"); + newCode.add(COMMENT("End of other user-defined variables")); // End of struct Sequential - newCode.add("} " + SPEC_SEQUENTIAL_STRUCT + "; /* End of struct " - + SPEC_SEQUENTIAL_STRUCT + " */"); - - // Generate - - // 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.SPEC_CONDITION - + ";"); - // __ID__ - newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_ID + ";"); - // DefineVars + newCode.add("} " + SPEC_SEQUENTIAL_STRUCT + "; " + + COMMENT("End of struct " + SPEC_SEQUENTIAL_STRUCT)); + + // Generate definition of the sequential struct + newCode.add(""); + newCode.add(COMMENT("Instance of the struct")); + newCode.add(DECLARE(SPEC_SEQUENTIAL_STRUCT, SPEC_SEQUENTIAL_INSTANCE)); + + newCode.add(""); + newCode.add(COMMENT("Define function for sequential code initialization")); + newCode.add("void " + SPEC_SEQUENTIAL_INSTANCE + "_init() {"); + // Internal variables + newCode.add(COMMENT("Init internal variables")); + newCode.add(INIT(SPEC_CONDITION)); + newCode.add(INIT(SPEC_ID)); + newCode.add(INIT(SPEC_INTERFACE)); + newCode.add(INIT(SPEC_INTERFACE_CALL_SEQUENCE)); + newCode.add(INIT(SPEC_GLOBAL_CALL_SEQUENCE)); + // Init DefineVars + newCode.add(COMMENT("Init 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(CodeVariables.SPEC_HASHTABLE + var.getNewVarName() - + ";"); + if (defineVars.size() > 0) { + newCode.add(COMMENT("DefineVar in " + interfaceName)); + for (int i = 0; i < defineVars.size(); i++) { + DefineVar var = defineVars.get(i); + newCode.add(INIT(var.getNewVarName())); + } } } - // __interface - newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_INTERFACE - + ";"); - // __interface_call_sequence - newCode.add(CodeVariables.SPEC_HASHTABLE - + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ";"); - // Interface call sequence varaiable - newCode.add(CodeVariables.SPEC_TAG + " " - + CodeVariables.INTERFACE_CALL_SEQUENCE + ";"); - // End of the struct - newCode.add("}"); - - // FIXME: Constructor should be modified and put in the right place - // Generate constructor (the place to initialize everything!) + // Init user-defined variables + newCode.add(COMMENT("Init user-defined variables")); breakCodeLines(newCode, globalCode.initVar); - // __COND_SAT__ - newCode.add("init_table(&" + CodeVariables.SPEC_CONDITION + ");"); - // __ID__ - 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("init_table(&" + CodeVariables.SPEC_INTERFACE + ");"); - // __interface_call_sequence - newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE - + ");"); - - // Pass the happens-before relationship check here + // Pass the HB initialization + newCode.add(COMMENT("Pass the happens-before initialization here")); newCode.addAll(CodeVariables.generateHBInitAnnotation(semantics)); + // End of init the function + newCode.add("} " + COMMENT("End of init function")); - newCode.add("\n"); - - // Generate the sequential functions + // Generate the user-defined sequential functions + newCode.add(""); + newCode.add(COMMENT("All other user-defined functions")); breakCodeLines(newCode, globalCode.defineFunc); // The end - newCode.add("#endif " + SPEC_SEQUENTIAL_HEADER_MACRO + "\t/* End of " - + SPEC_SEQUENTIAL_HEADER + " */"); + newCode.add(""); + newCode.add("#endif " + SPEC_SEQUENTIAL_HEADER_MACRO + "\t" + + COMMENT("End of " + HEADER_SPEC_SEQUENTIAL)); - printCode(newCode); + // printCode(newCode); return newCode; } - public static ArrayList generateHBInitAnnotation( + private static ArrayList generateHBInitAnnotation( SemanticsChecker semantics) { ArrayList newCode = new ArrayList(); int hbConditionInitIdx = 0; @@ -209,27 +315,217 @@ public class CodeVariables { for (ConditionalInterface right : semantics.getHBConditions().get( left)) { String structVarName = "hbConditionInit" + hbConditionInitIdx; + String annotationVarName = "hb_init" + 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); + String interfaceNumBefore = Integer + .toString(semantics.interface2Num + .get(left.interfaceName)), hbLabelNumBefore = Integer + .toString(semantics.hbLabel2Num + .get(left.hbConditionLabel)), interfaceNumAfter = Integer + .toString(semantics.interface2Num + .get(right.interfaceName)), hbLabelNumAfter = Integer + .toString(semantics.hbLabel2Num + .get(right.hbConditionLabel)); + newCode.add(COMMENT(left + " -> " + right)); + newCode.add(ANNO_HB_INIT + " " + structVarName + ";"); + newCode.add(ASSIGN(structVarName, "interface_num_before", + interfaceNumBefore)); + newCode.add(ASSIGN(structVarName, "hb_condition_num_before", + hbLabelNumBefore)); + newCode.add(ASSIGN(structVarName, "interface_num_after", + interfaceNumAfter)); + newCode.add(ASSIGN(structVarName, "hb_condition_num_after", + hbLabelNumAfter)); - 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 + ");"); + newCode.add(DECLARE(SPEC_ANNOTATION, annotationVarName)); + newCode.add(ASSIGN(annotationVarName, + SPEC_ANNOTATION_FIELD_TYPE, SPEC_ANNO_TYPE_HB_INIT)); + newCode.add(ASSIGN_PTR(annotationVarName, + SPEC_ANNOTATION_FIELD_ANNO, structVarName)); + newCode.add(ANNOTATE(annotationVarName)); } } return newCode; } + + public static ArrayList generateInterfaceWrapper( + SemanticsChecker semantics, SpecConstruct inst) { + InterfaceConstruct construct = (InterfaceConstruct) inst.construct; + ArrayList newCode = new ArrayList(); + String funcDecl = inst.interfaceDeclBody.substring(0, + inst.interfaceDeclBody.indexOf(')') + 1); + String returnType = getFuncReturnType(funcDecl), funcName = getFuncName(funcDecl), renamedFuncName = SPEC_INTERFACE_WRAPPER + + funcName; + ArrayList 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 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 generatePotentialCPDefine( + SemanticsChecker semantics, SpecConstruct inst) { + PotentialCPDefineConstruct construct = (PotentialCPDefineConstruct) inst.construct; + ArrayList newCode = new ArrayList(); + + // 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; + } } diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/IDExtractor.java b/src/edu/uci/eecs/specCompiler/codeGenerator/IDExtractor.java new file mode 100644 index 0000000..d2326ce --- /dev/null +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/IDExtractor.java @@ -0,0 +1,120 @@ +package edu.uci.eecs.specCompiler.codeGenerator; + +public class IDExtractor { + private String code; + private int index = 0; + + private int idBeginIdx, idEndIdx; + + public IDExtractor(String code) { + this.code = code; + this.index = 0; + } + + public IDExtractor(String code, int beginIdx) { + this.code = code; + this.index = beginIdx; + } + + public void reset(int beginIdx) { + this.index = beginIdx; + } + + public void reset() { + this.index = 0; + } + + public int getIDBeginIdx() { + return this.idBeginIdx; + } + + public int getIDEndIdx() { + return this.idEndIdx; + } + + public int lineNumOfID() { + int cnt = 0; + for (int i = 0; i < idBeginIdx; i++) { + if (code.charAt(i) == '\n') + cnt++; + } + return cnt; + } + + public int lineBeginIdxOfID() { + int i; + for (i = idBeginIdx - 1; i >= 0; i--) { + if (code.charAt(i) == '\n') + break; + } + return i + 1; + } + + public int lineEndIdxOfID() { + int i = 0; + for (i = idEndIdx + 1; i < code.length(); i++) { + if (code.charAt(i) == '\n') { + break; + } + } + return i - 1; + } + + public String getPrevID() { + int beginIdx = index; + int endIdx = index; + char ch; + while (true) { + ch = code.charAt(endIdx); + if ((ch == '_' || (ch >= 'a' && ch <= 'z') || ch >= 'A' + && ch <= 'Z')) { + break; + } + endIdx--; + } + beginIdx = endIdx; + while (true) { + ch = code.charAt(beginIdx); + if (!((ch == '_' || (ch >= 'a' && ch <= 'z') || ch >= 'A' + && ch <= 'Z'))) { + break; + } + beginIdx--; + } + index = beginIdx; + if (beginIdx > endIdx) + return null; + idBeginIdx = beginIdx + 1; + idEndIdx = endIdx; + return code.substring(beginIdx + 1, endIdx + 1); + } + + public String getNextID() { + int beginIdx = index; + int endIdx = index; + char ch; + while (true) { + ch = code.charAt(beginIdx); + if ((ch == '_' || (ch >= 'a' && ch <= 'z') || ch >= 'A' + && ch <= 'Z')) { + break; + } + beginIdx++; + } + endIdx = beginIdx; + while (true) { + ch = code.charAt(endIdx); + if (!((ch == '_' || (ch >= 'a' && ch <= 'z') || ch >= 'A' + && ch <= 'Z'))) { + break; + } + endIdx++; + } + index = endIdx; + if (beginIdx > endIdx) + return null; + idBeginIdx = beginIdx; + idEndIdx = endIdx - 1; + return code.substring(beginIdx, endIdx); + } +} diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java index 1d34199..58b463f 100644 --- a/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java +++ b/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java @@ -157,15 +157,14 @@ public class SpecExtractor { if (braceIdx == -1) { res = res + " " + curLine; } else { - res = res + curLine.substring(0, braceIdx + 1); - res = trimSpace(res); + res = res + curLine; break; } } return res; } - private String trimSpace(String line) { + public static String trimSpace(String line) { int i, j; char ch; for (i = 0; i < line.length(); i++) { diff --git a/test.c b/test.c index 0333725..5a4776c 100644 --- a/test.c +++ b/test.c @@ -1,33 +1,11 @@ #include -#include "test.h" -#include "test.h" struct pair { int x, y; }; -struct pair p[] = {{1,2}, {2,3}}; - -enum E { - a, b, c -}; -const int inte = 3; -void _foo(struct Test t) { - for (int i = 0; i < 10; i++) { - int j; - } - printf("%d\n", t.x); -} - -void foo(struct Test t) { - int num[] = {5, 3}; - _foo(t); -} - -void func() { -} - int main() { - printf("%d\n", b); +#include "test.h" + printf("%d\n", globalVar); return 0; } diff --git a/test.h b/test.h index e421c4c..4517194 100644 --- a/test.h +++ b/test.h @@ -10,4 +10,6 @@ struct Test { */ }; +int globalVar = 0; + #endif -- 2.34.1