fix header in the middle of code bug

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index f3d0896c817b1eefb514bd312cd27b462e240c9b..142e3766cf350e504a79079b3d80b8d14a9c8faf 100644 (file)
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -163,7 +163,7 @@ static inline int read_trylock(rwlock_t *rw)
        int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
        /**
                @Begin
        int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
        /**
                @Begin

-               @Potential_commit_point: true
+               @Potential_commit_point_define: true

                @Label: Potential_Read_Trylock_Point
                @End
        */
                @Label: Potential_Read_Trylock_Point
                @End
        */


@@ -171,8 +171,8 @@ static inline int read_trylock(rwlock_t *rw)
                /**
                        @Begin
                        @Commit_point_define: true
                /**
                        @Begin
                        @Commit_point_define: true

-                       @Label:  Read_Trylock_Succ_Point

                        @Potential_commit_point_label: Potential_Read_Trylock_Point
                        @Potential_commit_point_label: Potential_Read_Trylock_Point

+                       @Label:  Read_Trylock_Succ_Point

                        @End
                */
                return 1;
                        @End
                */
                return 1;


@@ -180,8 +180,8 @@ static inline int read_trylock(rwlock_t *rw)
        /**
                @Begin
                @Commit_point_define: true
        /**
                @Begin
                @Commit_point_define: true

-               @Label:  Read_Trylock_Fail_Point

                @Potential_commit_point_label: Potential_Read_Trylock_Point
                @Potential_commit_point_label: Potential_Read_Trylock_Point

+               @Label:  Read_Trylock_Fail_Point

                @End
        */
        atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
                @End
        */
        atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);


@@ -209,7 +209,7 @@ static inline int write_trylock(rwlock_t *rw)
        int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
        /**
                @Begin
        int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
        /**
                @Begin

-               @Potential_commit_point: true
+               @Potential_commit_point_define: true

                @Label: Potential_Write_Trylock_Point
                @End
        */
                @Label: Potential_Write_Trylock_Point
                @End
        */


@@ -217,8 +217,8 @@ static inline int write_trylock(rwlock_t *rw)
                /**
                        @Begin
                        @Commit_point_define: true
                /**
                        @Begin
                        @Commit_point_define: true

-                       @Label: Write_Trylock_Succ_Point

                        @Potential_commit_point_label: Potential_Write_Trylock_Point
                        @Potential_commit_point_label: Potential_Write_Trylock_Point

+                       @Label: Write_Trylock_Succ_Point

                        @End
                */
                return 1;
                        @End
                */
                return 1;


@@ -226,8 +226,8 @@ static inline int write_trylock(rwlock_t *rw)
        /**
                @Begin
                @Commit_point_define: true
        /**
                @Begin
                @Commit_point_define: true

-               @Label: Write_Trylock_Fail_Point

                @Potential_commit_point_label: Potential_Write_Trylock_Point
                @Potential_commit_point_label: Potential_Write_Trylock_Point

+               @Label: Write_Trylock_Fail_Point

                @End
        */
        atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
                @End
        */
        atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 11cd25845ed20574d8877274a0b9034404cd8b7a..232e5d839347794a2056a5c0de5c7e17c6d50811 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -109,7 +109,7 @@ void enqueue(queue_t *q, unsigned int val)
                                                &next, value, release, release);
                                /**
                                        @Begin
                                                &next, value, release, release);
                                /**
                                        @Begin

-                                       @Commit_point_define_check: success = true
+                                       @Commit_point_define_check: success == true

                                        @Label: Enqueue_Success_Point
                                        @End
                                */
                                        @Label: Enqueue_Success_Point
                                        @End
                                */

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index b8f163e65387843b85743e6a43d1bcd1b265cba6..4ed57ba5c20879dff5268abdb3d53ef1d56a545a 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -8,6 +8,7 @@ import java.io.IOException;
 import java.util.ArrayList;
 import java.util.Collections;
 import java.util.HashMap;
 import java.util.ArrayList;
 import java.util.Collections;
 import java.util.HashMap;

+import java.util.HashSet;

 import java.util.Iterator;
 
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
 import java.util.Iterator;
 
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;


@@ -226,8 +227,14 @@ public class CodeGenerator {
                        }
                }
                // Sort code additions
                        }
                }
                // Sort code additions

+               HashSet<String> headers = CodeVariables.getAllHeaders(_semantics);
+               ArrayList<String> headerCode = new ArrayList<String>(headers.size());
+               for (String header : headers) {
+                       headerCode.add("#include " + header + ";");
+               }

                for (File file : codeAdditions.keySet()) {
                        ArrayList<CodeAddition> additions = codeAdditions.get(file);
                for (File file : codeAdditions.keySet()) {
                        ArrayList<CodeAddition> additions = codeAdditions.get(file);

+                       

                        if (additions.size() == 0) // Simply do nothing
                                continue;
                        ArrayList<String> content = _semantics.srcFilesInfo.get(file).content;
                        if (additions.size() == 0) // Simply do nothing
                                continue;
                        ArrayList<String> content = _semantics.srcFilesInfo.get(file).content;


@@ -235,8 +242,11 @@ public class CodeGenerator {
                        // Insert generated annotation to the source files
                        ArrayList<String> newContent = insertAnnotation2Src(additions,
                                        content);
                        // Insert generated annotation to the source files
                        ArrayList<String> newContent = insertAnnotation2Src(additions,
                                        content);

+                       ArrayList<String> finalContent = new ArrayList<String>(headerCode.size() + newContent.size());
+                       finalContent.addAll(headerCode);
+                       finalContent.addAll(newContent);

                        // Write it back to file
                        // Write it back to file

-                       ParserUtils.write2File(file, newContent);
+                       ParserUtils.write2File(file, finalContent);

                }
 
        }
                }
 
        }


@@ -246,15 +256,15 @@ public class CodeGenerator {
                File[] srcFiles = {
                                // new File(Environment.MODEL_CHECKER_TEST_DIR +
                                // "/backup_linuxrwlocks.c") };
                File[] srcFiles = {
                                // new File(Environment.MODEL_CHECKER_TEST_DIR +
                                // "/backup_linuxrwlocks.c") };

-                                new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c")
-                                };
+//                              new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c")
+//                              };

                                // new File(homeDir
                                // +
                                // "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
                                // };
                                // 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/main.c"),
-//                             new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
+                               new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
+                               new File(homeDir + "/benchmark/ms-queue/main.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 c64517ae4b046a3e6f216e24031f31502854c369..a97edc34e2aa968452e886ed83a0411b924721dd 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -1,6 +1,7 @@
 package edu.uci.eecs.specCompiler.codeGenerator;
 
 import java.util.ArrayList;
 package edu.uci.eecs.specCompiler.codeGenerator;
 
 import java.util.ArrayList;

+import java.util.HashMap;

 import java.util.HashSet;
 import java.io.File;
 
 import java.util.HashSet;
 import java.io.File;
 


@@ -38,8 +39,8 @@ public class CodeVariables {
        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 HEADER_SPECANNOTATION = "<specannotation.h>";
        public static final String HEADER_CDSTRACE = "<cdstrace.h>";
        // public static final String CDSAnnotate = "cdsannotate";

-//     public static final String CDSAnnotate = "_Z11cdsannotatemPv";
-       public static final String CDSAnnotate = "cdsannotate";
+       public static final String CDSAnnotate = "_Z11cdsannotatemPv";
+       // public static final String CDSAnnotate = "cdsannotate";

        public static final String CDSAnnotateType = "SPEC_ANALYSIS";
        public static final String IDType = "call_id_t";
 
        public static final String CDSAnnotateType = "SPEC_ANALYSIS";
        public static final String IDType = "call_id_t";
 


@@ -60,7 +61,7 @@ public class CodeVariables {
        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";
        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";

-       public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potentail_cp_define";
+       public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potential_cp_define";

        public static final String ANNO_CP_DEFINE = "anno_cp_define";
        public static final String ANNO_CP_DEFINE_CHECK = "anno_cp_define_check";
        public static final String ANNO_HB_CONDITION = "anno_hb_condition";
        public static final String ANNO_CP_DEFINE = "anno_cp_define";
        public static final String ANNO_CP_DEFINE_CHECK = "anno_cp_define_check";
        public static final String ANNO_HB_CONDITION = "anno_hb_condition";


@@ -79,7 +80,7 @@ public class CodeVariables {
        public static final String SPEC_TAG = "spec_tag";
        public static final String SPEC_TAG_CURRENT = "current";
        public static final String SPEC_TAG_NEXT = "next";
        public static final String SPEC_TAG = "spec_tag";
        public static final String SPEC_TAG_CURRENT = "current";
        public static final String SPEC_TAG_NEXT = "next";

-       
+

        public static final String MODEL_MALLOC = "model_malloc";
 
        // Macro
        public static final String MODEL_MALLOC = "model_malloc";
 
        // Macro


@@ -248,12 +249,20 @@ public class CodeVariables {
                return code;
        }
 
                return code;
        }
 

-       private static HashSet<String> getAllHeaders(SemanticsChecker semantics) {
+       public static HashSet<String> getAllHeaders(SemanticsChecker semantics) {

                HashSet<String> headers = new HashSet<String>();
                for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
                        File f = semantics.interfaceName2Construct.get(interfaceName).file;
                        headers.addAll(semantics.srcFilesInfo.get(f).headers);
                }
                HashSet<String> headers = new HashSet<String>();
                for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
                        File f = semantics.interfaceName2Construct.get(interfaceName).file;
                        headers.addAll(semantics.srcFilesInfo.get(f).headers);
                }

+               headers.add(HEADER_STDLIB);
+               headers.add(HEADER_STDINT);
+               headers.add(HEADER_MODELMEMORY);
+               headers.add(HEADER_STDINT);
+               headers.add(HEADER_CDSANNOTATE);
+               headers.add(HEADER_COMMON);
+               headers.add(HEADER_SPEC_LIB);
+               headers.add(HEADER_SPECANNOTATION);

                return headers;
        }
 
                return headers;
        }
 


@@ -296,21 +305,6 @@ public class CodeVariables {
                ArrayList<String> newCode = new ArrayList<String>();
                HashSet<String> allHeaders = getAllHeaders(semantics);
 
                ArrayList<String> newCode = new ArrayList<String>();
                HashSet<String> allHeaders = getAllHeaders(semantics);
 

-               // All headers needed by the interface decalration
-               newCode.add(COMMENT("Include all the header files that contains the interface declaration"));
-               for (String header : allHeaders) {
-                       newCode.add(INCLUDE(header));
-               }
-               newCode.add("");
-               // Other necessary headers
-               newCode.add(INCLUDE(HEADER_STDLIB));
-               newCode.add(INCLUDE(HEADER_MODELMEMORY));
-               newCode.add(INCLUDE(HEADER_STDINT));
-               newCode.add(INCLUDE(HEADER_CDSANNOTATE));
-               newCode.add(INCLUDE(HEADER_COMMON));
-               newCode.add(INCLUDE(HEADER_SPEC_LIB));
-               newCode.add(INCLUDE(HEADER_SPECANNOTATION));
-               newCode.add("");

 
                SequentialDefineSubConstruct code = construct.code;
                // User-defined structs first
 
                SequentialDefineSubConstruct code = construct.code;
                // User-defined structs first


@@ -536,12 +530,6 @@ public class CodeVariables {
                        SemanticsChecker semantics, InterfaceConstruct construct) {
                ArrayList<String> newCode = new ArrayList<String>();
                String interfaceName = construct.name;
                        SemanticsChecker semantics, InterfaceConstruct construct) {
                ArrayList<String> newCode = new ArrayList<String>();
                String interfaceName = construct.name;

-               // Generate necessary header file (might be redundant but never mind)
-               newCode.add(INCLUDE(HEADER_STDLIB));
-               newCode.add(INCLUDE(HEADER_MODELMEMORY));
-               newCode.add(INCLUDE(HEADER_CDSANNOTATE));
-               newCode.add(INCLUDE(HEADER_SPECANNOTATION));
-               newCode.add(INCLUDE(HEADER_SPEC_LIB));

 
                FunctionHeader header = getFunctionHeader(semantics, construct);
                String interfaceNum = Integer.toString(semantics.interface2Num
 
                FunctionHeader header = getFunctionHeader(semantics, construct);
                String interfaceNum = Integer.toString(semantics.interface2Num


@@ -688,10 +676,6 @@ public class CodeVariables {
                // Generate redundant header files
                newCode.add(COMMENT("Automatically generated code for potential commit point: "
                                + construct.label));
                // 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_STDINT));
-               newCode.add(INCLUDE(HEADER_CDSANNOTATE));
-               newCode.add(INCLUDE(HEADER_SPECANNOTATION));

                newCode.add("");
                // Add annotation
                newCode.add("if (" + construct.condition + ") {");
                newCode.add("");
                // Add annotation
                newCode.add("if (" + construct.condition + ") {");


@@ -720,9 +704,6 @@ public class CodeVariables {
                // Generate redundant header files
                newCode.add(COMMENT("Automatically generated code for commit point define check: "
                                + construct.label));
                // Generate redundant header files
                newCode.add(COMMENT("Automatically generated code for commit point define check: "
                                + construct.label));

-               newCode.add(COMMENT("Include redundant headers"));
-               newCode.add(INCLUDE(HEADER_STDINT));
-               newCode.add(INCLUDE(HEADER_CDSANNOTATE));

                newCode.add("");
                // Add annotation
                newCode.add("if (" + construct.condition + ") {");
                newCode.add("");
                // Add annotation
                newCode.add("if (" + construct.condition + ") {");