From: Peizhao Ou Date: Wed, 6 Nov 2013 03:12:28 +0000 (-0800) Subject: save it X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=99de26ee130b9bbf2dd336c02ac63da7914296f3;p=cdsspec-compiler.git save it --- diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c index 1cbe525..0f52b66 100644 --- a/benchmark/linuxrwlocks/linuxrwlocks.c +++ b/benchmark/linuxrwlocks/linuxrwlocks.c @@ -7,6 +7,10 @@ #define RW_LOCK_BIAS 0x00100000 #define WRITE_LOCK_CMP RW_LOCK_BIAS +typedef union { + atomic_int lock; +} rwlock_t; + /** Example implementation of linux rw lock along with 2 thread test * driver... */ @@ -59,13 +63,6 @@ @End */ -/** - */ - -typedef union { - atomic_int lock; -} rwlock_t; - static inline int read_can_lock(rwlock_t *lock) { return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0; @@ -93,7 +90,7 @@ static inline void read_lock(rwlock_t *rw) int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); /** @Begin - @Commit_point_define_check: __ATOMIC_RET__ > 0 + @Commit_point_define_check: priorvalue > 0 @Label:Read_Lock_Success_1 @End */ @@ -105,7 +102,7 @@ static inline void read_lock(rwlock_t *rw) priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); /** @Begin - @Commit_point_define_check: __ATOMIC_RET__ > 0 + @Commit_point_define_check: priorvalue > 0 @Label:Read_Lock_Success_2 @End */ @@ -129,7 +126,7 @@ static inline void write_lock(rwlock_t *rw) int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); /** @Begin - @Commit_point_define_check: __ATOMIC_RET__ == RW_LOCK_BIAS + @Commit_point_define_check: priorvalue == RW_LOCK_BIAS @Label: Write_Lock_Success_1 @End */ @@ -141,7 +138,7 @@ static inline void write_lock(rwlock_t *rw) priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); /** @Begin - @Commit_point_define_check: __ATOMIC_RET__ == RW_LOCK_BIAS + @Commit_point_define_check: priorvalue == RW_LOCK_BIAS @Label: Write_Lock_Success_2 @End */ @@ -243,7 +240,6 @@ static inline void read_unlock(rwlock_t *rw) writer_lock_acquired = false; @End */ - static inline void write_unlock(rwlock_t *rw) { atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release); @@ -276,6 +272,11 @@ static void a(void *obj) int user_main(int argc, char **argv) { + /** + @Begin + @Entry_point + @End + */ thrd_t t1, t2; atomic_init(&mylock.lock, RW_LOCK_BIAS); diff --git a/notes/generated_code_examples.txt b/notes/generated_code_examples.txt index 0993e2f..2a7241c 100644 --- a/notes/generated_code_examples.txt +++ b/notes/generated_code_examples.txt @@ -98,6 +98,15 @@ void __sequential_init() { lock_acquired = false; reader_lock_cnt = 0; + /* Pass function table info */ + anno_func_table_init func_table; + func_table.size = INTERFACE_SIZE; + func_table.table = func_ptr_table; + spec_annotation func_init; + func_init.type = FUNC_TABLE_INIT; + func_init.annotation = &anno_func_table_init; + cdsannotate(SPEC_ANALYSIS, &func_init); + /* Pass the happens-before initialization here */ /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */ anno_hb_init hbConditionInit0; diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java index a0bc957..f18be8b 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java @@ -3,6 +3,10 @@ package edu.uci.eecs.specCompiler.codeGenerator; import java.util.ArrayList; import java.util.Comparator; +import com.sun.xml.internal.ws.wsdl.parser.ParserUtil; + +import edu.uci.eecs.specCompiler.specExtraction.ParserUtils; + public class CodeAddition { public static Comparator lineNumComparator = new Comparator() { public int compare(CodeAddition addition1, CodeAddition addition2) { @@ -17,4 +21,8 @@ public class CodeAddition { this.lineNum = lineNum; this.newCode = newCode; } + + public String toString() { + return "Line: " + lineNum + "\n" + ParserUtils.array2Str(newCode); + } } diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index 20f6e53..008ef66 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -159,11 +159,13 @@ public class CodeGenerator { for (int i = 0; i < additions.size(); i++) { CodeAddition addition = additions.get(i); if (curSrcLine < addition.lineNum) { - newContent.addAll(content.subList(curSrcLine, addition.lineNum - 1)); + // Be careful, subList is the interval [begin, end) + newContent.addAll(content.subList(curSrcLine, addition.lineNum)); curSrcLine = addition.lineNum; } newContent.addAll(addition.newCode); } + newContent.addAll(content.subList(curSrcLine, content.size())); return newContent; } @@ -204,11 +206,13 @@ 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(Environment.MODEL_CHECKER_TEST_DIR + "/backup_linuxrwlocks.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") }; +// new File(homeDir + "/benchmark/test/test.c") }; 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 980e420..af2ebca 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java @@ -35,11 +35,13 @@ public class CodeVariables { public static final String HEADER_CDSANNOTATE = ""; public static final String HEADER_SPECANNOTATION = ""; public static final String HEADER_CDSTRACE = ""; - public static final String CDSAnnotate = "cdsannotate"; +// public static final String CDSAnnotate = "cdsannotate"; + public static final String CDSAnnotate = "_Z11cdsannotatemPv"; public static final String CDSAnnotateType = "SPEC_ANALYSIS"; - public static final String IDType = "id_t"; + public static final String IDType = "call_id_t"; public static final String SPEC_ANNO_TYPE = "spec_anno_type"; + public static final String SPEC_ANNO_TYPE_FUNC_TABLE_INIT = "FUNC_TABLE_INIT"; 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_HB_CONDITION = "HB_CONDITION"; @@ -51,6 +53,7 @@ public class CodeVariables { public static final String SPEC_ANNOTATION_FIELD_TYPE = "type"; public static final String SPEC_ANNOTATION_FIELD_ANNO = "annotation"; + public static final String ANNO_FUNC_TABLE_INIT = "anno_func_table_init"; 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"; @@ -158,7 +161,7 @@ public class CodeVariables { for (int i = 0; i < header.args.size(); i++) { code.add(DECLARE(header.args.get(i))); } - code.add("} " + interfaceName + "_info {"); + code.add("} " + interfaceName + "_info;"); return code; } @@ -187,7 +190,7 @@ public class CodeVariables { if (!header.returnType.equals("void") || header.args.size() != 0) { String infoStructType = interfaceName + "_info", infoStructName = "theInfo"; code.add(DECLARE_DEFINE(infoStructType + "*", infoStructName, - BRACE(infoStructType) + "info")); + BRACE(infoStructType + "*") + "info")); if (!header.returnType.equals("void")) { code.add((DECLARE_DEFINE(header.returnType, MACRO_RETURN, GET_FIELD_BY_PTR(infoStructName, MACRO_RETURN)))); @@ -221,6 +224,8 @@ public class CodeVariables { if (construct.postAction.size() > 0) { code.addAll(construct.postAction); } + // Return true finally + code.add("return true;"); code.add("}"); @@ -275,9 +280,11 @@ public class CodeVariables { } newCode.add(""); // Other necessary headers + newCode.add(INCLUDE(HEADER_STDLIB)); newCode.add(INCLUDE(HEADER_STDINT)); newCode.add(INCLUDE(HEADER_CDSANNOTATE)); newCode.add(INCLUDE(HEADER_SPEC_LIB)); + newCode.add(INCLUDE(HEADER_SPECANNOTATION)); newCode.add(""); SequentialDefineSubConstruct code = construct.code; @@ -289,6 +296,13 @@ public class CodeVariables { newCode.addAll(declareStruct); newCode.add(""); } + // User-defined variables + ArrayList varDecls = code.declareVar; + for (int i = 0; i < varDecls.size(); i++) { + VariableDeclaration varDecl = varDecls.get(i); + // Don't forget to make them static + newCode.add(makeVariablesStatic(varDecl)); + } // User-defined functions newCode.add(COMMENT("All other user-defined functions")); ArrayList> defineFuncs = code.defineFuncs; @@ -304,7 +318,8 @@ public class CodeVariables { .get(interfaceName); FunctionHeader funcHeader = getFunctionHeader(semantics, iConstruct); // Define necessary info structure - if (!funcHeader.returnType.equals("void") || funcHeader.args.size() > 0) { + if (!funcHeader.returnType.equals("void") + || funcHeader.args.size() > 0) { newCode.add(COMMENT("Definition of interface info struct: " + interfaceName)); newCode.addAll(DEFINE_INFO_STRUCT(interfaceName, funcHeader)); @@ -316,14 +331,14 @@ public class CodeVariables { // Define ID function newCode.add(COMMENT("ID function of interface: " + interfaceName)); newCode.addAll(DEFINE_ID_FUNC(interfaceName, iConstruct.idCode)); - newCode.add(COMMENT("End of ID function: + " + interfaceName)); + newCode.add(COMMENT("End of ID function: " + interfaceName)); newCode.add(""); // Define check_action function newCode.add(COMMENT("Check action function of interface: " + interfaceName)); newCode.addAll(DEFINE_CHECK_ACTION_FUNC(iConstruct, funcHeader)); - newCode.add(COMMENT("End of check action function: + " + newCode.add(COMMENT("End of check action function: " + interfaceName)); newCode.add(""); } @@ -332,13 +347,6 @@ public class CodeVariables { .toString(semantics.interfaceName2Construct.size()); newCode.add(DEFINE("INTERFACE_SIZE", interfaceSize)); newCode.add(DECLARE("void**", "func_ptr_table")); - // User-defined variables - ArrayList varDecls = code.declareVar; - for (int i = 0; i < varDecls.size(); i++) { - VariableDeclaration varDecl = varDecls.get(i); - // Don't forget to make them static - newCode.add(makeVariablesStatic(varDecl)); - } newCode.add(""); newCode.add(COMMENT("Define function for sequential code initialization")); @@ -358,8 +366,19 @@ public class CodeVariables { newCode.add(""); // Init user-defined variables newCode.addAll(construct.code.initVar); + // Pass function table info + newCode.add(COMMENT("Pass function table info")); + String structName = "anno_func_table_init", anno = "func_init"; + newCode.add(DECLARE(ANNO_FUNC_TABLE_INIT, structName)); + newCode.add(ASSIGN(structName, "size", "INTERFACE_SIZE")); + newCode.add(ASSIGN(structName, "table", "func_ptr_table")); + newCode.add(DECLARE(SPEC_ANNOTATION, anno)); + newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_FUNC_TABLE_INIT)); + newCode.add(ASSIGN_PTR(anno, "annotation", structName)); + newCode.add(ANNOTATE(anno)); + // Pass Happens-before relationship - generateHBInitAnnotation(semantics); + newCode.addAll(generateHBInitAnnotation(semantics)); newCode.add("}"); newCode.add(COMMENT("End of Global construct generation in class")); @@ -470,6 +489,14 @@ public class CodeVariables { } // Generate wrapper header + // If it's not in a class, we should declare the wrapper function + if (semantics.getClassName() == null) { + FunctionHeader renamedHeader = header + .getRenamedHeader(SPEC_INTERFACE_WRAPPER); + newCode.add(COMMENT("Declaration of the wrapper")); + newCode.add(renamedHeader + ";"); + newCode.add(""); + } newCode.add(header.toString() + " {"); // Wrapper function body newCode.add(COMMENT("Interface begins")); @@ -479,12 +506,12 @@ public class CodeVariables { newCode.add(ASSIGN(structName, "interface_num", interfaceNum)); String anno = "annotation_interface_begin"; newCode.add(DECLARE(SPEC_ANNOTATION, anno)); - newCode.add(ASSIGN(structName, "type", SPEC_ANNO_TYPE_INTERFACE_BEGIN)); - newCode.add(ASSIGN_PTR(structName, "annotation", structName)); + newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_INTERFACE_BEGIN)); + newCode.add(ASSIGN_PTR(anno, "annotation", structName)); newCode.add(ANNOTATE(anno)); // Call original renamed function if (header.returnType.equals("void")) { - newCode.add(header.getRenamedCall(SPEC_INTERFACE_WRAPPER)); + newCode.add(header.getRenamedCall(SPEC_INTERFACE_WRAPPER) + ";"); } else { newCode.add(DECLARE_DEFINE(header.returnType, MACRO_RETURN, header.getRenamedCall(SPEC_INTERFACE_WRAPPER))); @@ -513,7 +540,7 @@ public class CodeVariables { if (!header.returnType.equals("void") || header.args.size() > 0) { infoStructType = interfaceName + "_info"; infoName = "info"; - newCode.add(DECLARE_DEFINE(infoStructType, infoName, + newCode.add(DECLARE_DEFINE(infoStructType + "*", infoName, BRACE(infoStructType + "*") + " malloc(sizeof(" + infoStructType + "))")); if (!header.returnType.equals("void")) { @@ -534,7 +561,11 @@ public class CodeVariables { newCode.add(DECLARE(SPEC_ANNOTATION, anno)); newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_INTERFACE_END)); newCode.add(ASSIGN_PTR(anno, "annotation", structName)); - ANNOTATE(anno); + newCode.add(ANNOTATE(anno)); + // Return __RET__ if it's not void + if (!header.returnType.equals("void")) { + newCode.add("return " + MACRO_RETURN + ";"); + } // End of the wrapper function newCode.add("}"); diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java b/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java index 6d1c41e..654e579 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java @@ -3,4 +3,7 @@ package edu.uci.eecs.specCompiler.codeGenerator; public class Environment { public static String HOME_DIRECTORY = System.getProperty("user.dir"); public static String GENERATED_FILE_DIR = HOME_DIRECTORY + "/" + "output"; + public static String MODEL_CHECKER_HOME_DIR = System + .getProperty("user.home") + "/model-checker-priv"; + public static String MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_HOME_DIR + "/test"; } diff --git a/test.c b/test.c index b279809..d771ce4 100644 --- a/test.c +++ b/test.c @@ -1,15 +1,9 @@ -# include -#include -#include +#include -typedef struct A { - -} A; +int test(); int main() { - uint64_t i64 = (uint64_t) NULL; - A *a = (A*) malloc (sizeof(A)); - printf("%d\n", sizeof(A)); + int a = test(); printf("%d\n", a); return 1; } diff --git a/test.cc b/test.cc index 64a4e3b..56bc554 100644 --- a/test.cc +++ b/test.cc @@ -1,18 +1,3 @@ -class A { - public: - A() { - } - -}; - - -int main() { - A a; - if (true) { - int i = 5; - } - if (true) { - int i = 1; - } - return 1; +extern int test() { + return 10; }