From e551d9733ed4e29fe2928713c34ad3e58e424e95 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Tue, 14 Jan 2014 17:19:14 -0800 Subject: [PATCH] fix header in the middle of code bug --- benchmark/linuxrwlocks/linuxrwlocks.c | 12 ++--- benchmark/ms-queue/my_queue.c | 2 +- .../codeGenerator/CodeGenerator.java | 22 ++++++--- .../codeGenerator/CodeVariables.java | 47 ++++++------------- 4 files changed, 37 insertions(+), 46 deletions(-) diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c index f3d0896..142e376 100644 --- 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 - @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); diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c index 11cd258..232e5d8 100644 --- 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 - @Commit_point_define_check: success = true + @Commit_point_define_check: success == true @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 b8f163e..4ed57ba 100644 --- 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.HashSet; import java.util.Iterator; import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct; @@ -226,8 +227,14 @@ public class CodeGenerator { } } // Sort code additions + HashSet headers = CodeVariables.getAllHeaders(_semantics); + ArrayList headerCode = new ArrayList(headers.size()); + for (String header : headers) { + headerCode.add("#include " + header + ";"); + } for (File file : codeAdditions.keySet()) { ArrayList additions = codeAdditions.get(file); + if (additions.size() == 0) // Simply do nothing continue; ArrayList content = _semantics.srcFilesInfo.get(file).content; @@ -235,8 +242,11 @@ public class CodeGenerator { // Insert generated annotation to the source files ArrayList newContent = insertAnnotation2Src(additions, content); + ArrayList finalContent = new ArrayList(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(); diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java index c64517a..a97edc3 100644 --- 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; +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 = ""; public static final String HEADER_CDSTRACE = ""; // 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 getAllHeaders(SemanticsChecker semantics) { + public static HashSet getAllHeaders(SemanticsChecker semantics) { HashSet headers = new HashSet(); 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 newCode = new ArrayList(); HashSet 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 newCode = new ArrayList(); 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 + ") {"); -- 2.34.1