bug fixing
authorPeizhao Ou <peizhaoo@uci.edu>
Sat, 7 Dec 2013 05:35:12 +0000 (21:35 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Sat, 7 Dec 2013 05:35:12 +0000 (21:35 -0800)
benchmark/ms-queue/my_queue.c
benchmark/ms-queue/my_queue.h
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java

index 9db5efe..7d19e02 100644 (file)
@@ -76,29 +76,6 @@ void init_queue(queue_t *q, int num_threads)
        atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0));
 }
 
-/**
-       @Begin
-       @Global_define:
-               typedef struct tag_elem {
-                       Tag id;
-                       unsigned int data;
-                       
-                       tag_elem(Tag _id, unsigned int _data) {
-                               id = _id;
-                               data = _data;
-                       }
-               } tag_elem_t;
-
-               spec_queue<tag_elem_t> __queue;
-               Tag __tag;
-       @Happens_before:
-               # Only check the happens-before relationship according to the id of the
-               # commit_point_set. For commit_point_set that has same ID, A -> B means
-               # B happens after the previous A.
-               Enqueue -> Dequeue
-       @End
-*/
-
 /**
        @Begin
        @Interface_define: Enqueue
index 2459b9c..6f4685d 100644 (file)
@@ -52,19 +52,18 @@ void init_queue(queue_t *q, int num_threads);
                                e->data = data;
                                return e;
                        }
-
+               @DefineFunc:
                        void free_tag_elem(tag_elem_t *e) {
                                free(e);
                        }
-
+               @DefineFunc:
                        call_id_t get_id(void *wrapper) {
                                return ((tag_elem_t*) wrapper)->id;
                        }
-
+               @DefineFunc:
                        unsigned int get_data(void *wrapper) {
                                return ((tag_elem_t*) wrapper)->data;
                        }
-
        @Happens_before:
                # Only check the happens-before relationship according to the id of the
                # commit_point_set. For commit_point_set that has same ID, A -> B means
@@ -83,7 +82,7 @@ void init_queue(queue_t *q, int num_threads);
        @Action:
                # __ID__ is an internal macro that refers to the id of the current
                # interface call
-               tag_elem_t elem = new_tag_elem(__ID__, val);
+               tag_elem_t *elem = new_tag_elem(__ID__, val);
                push_back(__queue, elem);
        @End
 */
index 66bdca4..2e44f5a 100644 (file)
@@ -87,11 +87,8 @@ public class CodeGenerator {
                }
        }
 
-       // Mainly rename and wrap the interface
+       // Wrap the interface and then renaem it
        private void interface2Code(InterfaceConstruct construct) {
-               // First rename the interface
-               CodeVariables.renameInterface(_semantics, construct);
-
                // If there's no define construct for it, we generate the wrapper just
                // in place without declaration
                InterfaceDefineConstruct defineConstruct = _semantics.interfaceName2DefineConstruct
@@ -101,36 +98,44 @@ public class CodeGenerator {
                CodeAddition addition;
                // Then generate the wrapper if necessary
                if (defineConstruct != null) { // Need to have a wrapper declaration
-                       newCode = CodeVariables.generateInterfaceWrapperDeclaration(_semantics, construct);
+                       newCode = CodeVariables.generateInterfaceWrapperDeclaration(
+                                       _semantics, construct);
                        lineNum = construct.beginLineNum;
                        // Add the wrapper declaration
                        addition = new CodeAddition(lineNum, newCode);
                        if (!codeAdditions.containsKey(construct.file)) {
-                               codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
+                               codeAdditions
+                                               .put(construct.file, new ArrayList<CodeAddition>());
                        }
                        codeAdditions.get(construct.file).add(addition);
-                       
+
                        // Add the wrapper definition
-                       newCode = CodeVariables.generateInterfaceWrapperDefinition(_semantics, construct);
+                       newCode = CodeVariables.generateInterfaceWrapperDefinition(
+                                       _semantics, construct);
                        lineNum = defineConstruct.beginLineNum;
                        // Add the wrapper declaration
                        addition = new CodeAddition(lineNum, newCode);
                        if (!codeAdditions.containsKey(defineConstruct.file)) {
-                               codeAdditions.put(defineConstruct.file, new ArrayList<CodeAddition>());
+                               codeAdditions.put(defineConstruct.file,
+                                               new ArrayList<CodeAddition>());
                        }
                        codeAdditions.get(defineConstruct.file).add(addition);
                } else { // No declaration needed
                        // Last generate the definition
-                       newCode = CodeVariables.generateInterfaceWrapperDefinition(_semantics, construct);
+                       newCode = CodeVariables.generateInterfaceWrapperDefinition(
+                                       _semantics, construct);
                        lineNum = construct.beginLineNum;
                        // Add the wrapper declaration
                        addition = new CodeAddition(lineNum, newCode);
                        if (!codeAdditions.containsKey(construct.file)) {
-                               codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
+                               codeAdditions
+                                               .put(construct.file, new ArrayList<CodeAddition>());
                        }
                        codeAdditions.get(construct.file).add(addition);
                }
-               
+
+               // Don't forget to rename the interface
+               CodeVariables.renameInterface(_semantics, construct);
        }
 
        private void potentialCPDefine2Code(PotentialCPDefineConstruct construct) {
@@ -223,8 +228,7 @@ public class CodeGenerator {
                // Sort code additions
                for (File file : codeAdditions.keySet()) {
                        ArrayList<CodeAddition> additions = codeAdditions.get(file);
-                       if (additions.size() == 0) // Simply do nothing, already written
-                                                                               // once
+                       if (additions.size() == 0) // Simply do nothing
                                continue;
                        ArrayList<String> content = _semantics.srcFilesInfo.get(file).content;
                        Collections.sort(additions, CodeAddition.lineNumComparator);
@@ -240,13 +244,16 @@ public class CodeGenerator {
        public static void main(String[] argvs) {
                String homeDir = Environment.HOME_DIRECTORY;
                File[] srcFiles = {
-               // 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.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();
index 0e4a712..c87e688 100644 (file)
@@ -179,7 +179,7 @@ public class CodeVariables {
        private static ArrayList<String> DEFINE_ID_FUNC(String interfaceName,
                        String idCode) {
                ArrayList<String> code = new ArrayList<String>();
-               code.add("static " + IDType + " " + interfaceName + "_id() {");
+               code.add("inline static " + IDType + " " + interfaceName + "_id() {");
                if (!idCode.equals("")) {
                        code.add(DECLARE_DEFINE(IDType, MACRO_ID, idCode));
                } else {
@@ -194,7 +194,7 @@ public class CodeVariables {
                        InterfaceConstruct construct, FunctionHeader header) {
                String interfaceName = construct.name;
                ArrayList<String> code = new ArrayList<String>();
-               code.add("static bool " + interfaceName + "_check_action(void *info, "
+               code.add("inline static bool " + interfaceName + "_check_action(void *info, "
                                + IDType + " " + MACRO_ID + ") {");
                code.add(DECLARE("bool", "check_passed"));
                // Read info struct
@@ -254,7 +254,7 @@ public class CodeVariables {
 
        private static void makeFunctionStatic(ArrayList<String> funcDefine) {
                String headLine = funcDefine.get(0);
-               headLine = "static " + headLine;
+               headLine = "inline static " + headLine;
                funcDefine.set(0, headLine);
        }
 
@@ -369,7 +369,7 @@ public class CodeVariables {
 
                newCode.add("");
                newCode.add(COMMENT("Define function for sequential code initialization"));
-               newCode.add("static void __sequential_init() {");
+               newCode.add("inline static void __sequential_init() {");
                // Init func_ptr_table
                newCode.add(COMMENT("Init func_ptr_table"));
                newCode.add(ASSIGN("func_ptr_table", "(void**) malloc(sizeof(void*) * "
index 769087d..cb6da9d 100644 (file)
@@ -29,7 +29,7 @@ public class FunctionHeader {
        
        public String getTemplateFullStr() {
                String templateStr = "";
-               if (templateList.size() == 0)
+               if (templateList == null)
                        return templateStr;
                VariableDeclaration decl;
                decl = templateList.get(0);