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
*/
/**
@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;
/**
@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);
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
*/
/**
@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;
/**
@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);
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;
}
}
// 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;
// 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);
}
}
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();
package edu.uci.eecs.specCompiler.codeGenerator;
import java.util.ArrayList;
+import java.util.HashMap;
import java.util.HashSet;
import java.io.File;
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 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 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
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;
}
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
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
// 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 + ") {");
// 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 + ") {");