bug fixing

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 9db5efe731793ae335b20852ca9758e98a75348d..7d19e02f678ec2c53e828a606f26b0d954630037 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -76,29 +76,6 @@ void init_queue(queue_t *q, int num_threads)
        atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0));
 }
 
        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
 /**
        @Begin
        @Interface_define: Enqueue

diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index 2459b9cbba070f663cb4b5880087b219d3f812cb..6f4685de6295b3deb90690f9714f755b3e2e2f30 100644 (file)
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -52,19 +52,18 @@ void init_queue(queue_t *q, int num_threads);
                                e->data = data;
                                return e;
                        }
                                e->data = data;
                                return e;
                        }

-
+               @DefineFunc:

                        void free_tag_elem(tag_elem_t *e) {
                                free(e);
                        }
                        void free_tag_elem(tag_elem_t *e) {
                                free(e);
                        }

-
+               @DefineFunc:

                        call_id_t get_id(void *wrapper) {
                                return ((tag_elem_t*) wrapper)->id;
                        }
                        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;
                        }
                        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
        @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
        @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
 */
                push_back(__queue, elem);
        @End
 */

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 66bdca4ab408d740edb6a444ad684fc9fc48ee02..2e44f5ad9b7e0d63d56cf9f502d8f6b52c5bea8f 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -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) {
        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
                // 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
                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)) {
                        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);
                        }
                        codeAdditions.get(construct.file).add(addition);

-                       
+

                        // Add the wrapper definition
                        // 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)) {
                        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
                        }
                        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)) {
                        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);
                }
                        }
                        codeAdditions.get(construct.file).add(addition);
                }

-               
+
+               // Don't forget to rename the interface
+               CodeVariables.renameInterface(_semantics, construct);

        }
 
        private void potentialCPDefine2Code(PotentialCPDefineConstruct 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);
                // 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);
                                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 = {
        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();
                // 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 0e4a712e4c75e23c9794f11baa5a9b5057d44c02..c87e6883681c5196185fc1962a006bdc555cb514 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -179,7 +179,7 @@ public class CodeVariables {
        private static ArrayList<String> DEFINE_ID_FUNC(String interfaceName,
                        String idCode) {
                ArrayList<String> code = new ArrayList<String>();
        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 {
                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>();
                        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
                                + 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);
 
        private static void makeFunctionStatic(ArrayList<String> funcDefine) {
                String headLine = funcDefine.get(0);

-               headLine = "static " + headLine;
+               headLine = "inline static " + headLine;

                funcDefine.set(0, 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("");
                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*) * "
                // Init func_ptr_table
                newCode.add(COMMENT("Init func_ptr_table"));
                newCode.add(ASSIGN("func_ptr_table", "(void**) malloc(sizeof(void*) * "

diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java b/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java
index 769087dcd7a6298f172b6e1e5006251cd6c7547c..cb6da9dbae743a229bbebc8fe2ffc0dd34be5be6 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java
@@ -29,7 +29,7 @@ public class FunctionHeader {
        
        public String getTemplateFullStr() {
                String templateStr = "";
        
        public String getTemplateFullStr() {
                String templateStr = "";

-               if (templateList.size() == 0)
+               if (templateList == null)

                        return templateStr;
                VariableDeclaration decl;
                decl = templateList.get(0);
                        return templateStr;
                VariableDeclaration decl;
                decl = templateList.get(0);