fix header in the middle of code bug
authorPeizhao Ou <peizhaoo@uci.edu>
Wed, 15 Jan 2014 01:19:14 +0000 (17:19 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Wed, 15 Jan 2014 01:19:14 +0000 (17:19 -0800)
benchmark/linuxrwlocks/linuxrwlocks.c
benchmark/ms-queue/my_queue.c
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java

index f3d0896..142e376 100644 (file)
@@ -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
-               @Potential_commit_point: true
+               @Potential_commit_point_define: true
                @Label: Potential_Read_Trylock_Point
                @End
        */
@@ -171,8 +171,8 @@ static inline int read_trylock(rwlock_t *rw)
                /**
                        @Begin
                        @Commit_point_define: true
-                       @Label:  Read_Trylock_Succ_Point
                        @Potential_commit_point_label: Potential_Read_Trylock_Point
+                       @Label:  Read_Trylock_Succ_Point
                        @End
                */
                return 1;
@@ -180,8 +180,8 @@ static inline int read_trylock(rwlock_t *rw)
        /**
                @Begin
                @Commit_point_define: true
-               @Label:  Read_Trylock_Fail_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);
@@ -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
-               @Potential_commit_point: true
+               @Potential_commit_point_define: true
                @Label: Potential_Write_Trylock_Point
                @End
        */
@@ -217,8 +217,8 @@ static inline int write_trylock(rwlock_t *rw)
                /**
                        @Begin
                        @Commit_point_define: true
-                       @Label: Write_Trylock_Succ_Point
                        @Potential_commit_point_label: Potential_Write_Trylock_Point
+                       @Label: Write_Trylock_Succ_Point
                        @End
                */
                return 1;
@@ -226,8 +226,8 @@ static inline int write_trylock(rwlock_t *rw)
        /**
                @Begin
                @Commit_point_define: true
-               @Label: Write_Trylock_Fail_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);
index 11cd258..232e5d8 100644 (file)
@@ -109,7 +109,7 @@ void enqueue(queue_t *q, unsigned int val)
                                                &next, value, release, release);
                                /**
                                        @Begin
-                                       @Commit_point_define_check: success = true
+                                       @Commit_point_define_check: success == true
                                        @Label: Enqueue_Success_Point
                                        @End
                                */
index b8f163e..4ed57ba 100644 (file)
@@ -8,6 +8,7 @@ import java.io.IOException;
 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;
@@ -226,8 +227,14 @@ public class CodeGenerator {
                        }
                }
                // 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);
+                       
                        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);
+                       ArrayList<String> finalContent = new ArrayList<String>(headerCode.size() + newContent.size());
+                       finalContent.addAll(headerCode);
+                       finalContent.addAll(newContent);
                        // 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") };
-                                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/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();
index c64517a..a97edc3 100644 (file)
@@ -1,6 +1,7 @@
 package edu.uci.eecs.specCompiler.codeGenerator;
 
 import java.util.ArrayList;
+import java.util.HashMap;
 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 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";
 
@@ -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_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";
@@ -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 MODEL_MALLOC = "model_malloc";
 
        // Macro
@@ -248,12 +249,20 @@ public class CodeVariables {
                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);
                }
+               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;
        }
 
@@ -296,21 +305,6 @@ public class CodeVariables {
                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
@@ -536,12 +530,6 @@ public class CodeVariables {
                        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
@@ -688,10 +676,6 @@ public class CodeVariables {
                // 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 + ") {");
@@ -720,9 +704,6 @@ public class CodeVariables {
                // 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 + ") {");