From 99de26ee130b9bbf2dd336c02ac63da7914296f3 Mon Sep 17 00:00:00 2001
From: Peizhao Ou <peizhaoo@uci.edu>
Date: Tue, 5 Nov 2013 19:12:28 -0800
Subject: [PATCH] save it
---
benchmark/linuxrwlocks/linuxrwlocks.c | 25 +++----
notes/generated_code_examples.txt | 9 +++
.../codeGenerator/CodeAddition.java | 8 +++
.../codeGenerator/CodeGenerator.java | 8 ++-
.../codeGenerator/CodeVariables.java | 71 +++++++++++++------
.../codeGenerator/Environment.java | 3 +
test.c | 12 +---
test.cc | 19 +----
8 files changed, 95 insertions(+), 60 deletions(-)
diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 1cbe525..0f52b66 100644
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -7,6 +7,10 @@
#define RW_LOCK_BIAS 0x00100000
#define WRITE_LOCK_CMP RW_LOCK_BIAS
+typedef union {
+ atomic_int lock;
+} rwlock_t;
+
/** Example implementation of linux rw lock along with 2 thread test
* driver... */
@@ -59,13 +63,6 @@
@End
*/
-/**
- */
-
-typedef union {
- atomic_int lock;
-} rwlock_t;
-
static inline int read_can_lock(rwlock_t *lock)
{
return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
@@ -93,7 +90,7 @@ static inline void read_lock(rwlock_t *rw)
int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
/**
@Begin
- @Commit_point_define_check: __ATOMIC_RET__ > 0
+ @Commit_point_define_check: priorvalue > 0
@Label:Read_Lock_Success_1
@End
*/
@@ -105,7 +102,7 @@ static inline void read_lock(rwlock_t *rw)
priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
/**
@Begin
- @Commit_point_define_check: __ATOMIC_RET__ > 0
+ @Commit_point_define_check: priorvalue > 0
@Label:Read_Lock_Success_2
@End
*/
@@ -129,7 +126,7 @@ static inline void write_lock(rwlock_t *rw)
int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
/**
@Begin
- @Commit_point_define_check: __ATOMIC_RET__ == RW_LOCK_BIAS
+ @Commit_point_define_check: priorvalue == RW_LOCK_BIAS
@Label: Write_Lock_Success_1
@End
*/
@@ -141,7 +138,7 @@ static inline void write_lock(rwlock_t *rw)
priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
/**
@Begin
- @Commit_point_define_check: __ATOMIC_RET__ == RW_LOCK_BIAS
+ @Commit_point_define_check: priorvalue == RW_LOCK_BIAS
@Label: Write_Lock_Success_2
@End
*/
@@ -243,7 +240,6 @@ static inline void read_unlock(rwlock_t *rw)
writer_lock_acquired = false;
@End
*/
-
static inline void write_unlock(rwlock_t *rw)
{
atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
@@ -276,6 +272,11 @@ static void a(void *obj)
int user_main(int argc, char **argv)
{
+ /**
+ @Begin
+ @Entry_point
+ @End
+ */
thrd_t t1, t2;
atomic_init(&mylock.lock, RW_LOCK_BIAS);
diff --git a/notes/generated_code_examples.txt b/notes/generated_code_examples.txt
index 0993e2f..2a7241c 100644
--- a/notes/generated_code_examples.txt
+++ b/notes/generated_code_examples.txt
@@ -98,6 +98,15 @@ void __sequential_init() {
lock_acquired = false;
reader_lock_cnt = 0;
+ /* Pass function table info */
+ anno_func_table_init func_table;
+ func_table.size = INTERFACE_SIZE;
+ func_table.table = func_ptr_table;
+ spec_annotation func_init;
+ func_init.type = FUNC_TABLE_INIT;
+ func_init.annotation = &anno_func_table_init;
+ cdsannotate(SPEC_ANALYSIS, &func_init);
+
/* Pass the happens-before initialization here */
/* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
anno_hb_init hbConditionInit0;
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java
index a0bc957..f18be8b 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java
@@ -3,6 +3,10 @@ package edu.uci.eecs.specCompiler.codeGenerator;
import java.util.ArrayList;
import java.util.Comparator;
+import com.sun.xml.internal.ws.wsdl.parser.ParserUtil;
+
+import edu.uci.eecs.specCompiler.specExtraction.ParserUtils;
+
public class CodeAddition {
public static Comparator<CodeAddition> lineNumComparator = new Comparator<CodeAddition>() {
public int compare(CodeAddition addition1, CodeAddition addition2) {
@@ -17,4 +21,8 @@ public class CodeAddition {
this.lineNum = lineNum;
this.newCode = newCode;
}
+
+ public String toString() {
+ return "Line: " + lineNum + "\n" + ParserUtils.array2Str(newCode);
+ }
}
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 20f6e53..008ef66 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -159,11 +159,13 @@ public class CodeGenerator {
for (int i = 0; i < additions.size(); i++) {
CodeAddition addition = additions.get(i);
if (curSrcLine < addition.lineNum) {
- newContent.addAll(content.subList(curSrcLine, addition.lineNum - 1));
+ // Be careful, subList is the interval [begin, end)
+ newContent.addAll(content.subList(curSrcLine, addition.lineNum));
curSrcLine = addition.lineNum;
}
newContent.addAll(addition.newCode);
}
+ newContent.addAll(content.subList(curSrcLine, content.size()));
return newContent;
}
@@ -204,11 +206,13 @@ public class CodeGenerator {
public static void main(String[] argvs) {
String homeDir = Environment.HOME_DIRECTORY;
File[] srcFiles = {
- new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.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();
}
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index 980e420..af2ebca 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -35,11 +35,13 @@ public class CodeVariables {
public static final String HEADER_CDSANNOTATE = "<cdsannotate.h>";
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 = "cdsannotate";
+ public static final String CDSAnnotate = "_Z11cdsannotatemPv";
public static final String CDSAnnotateType = "SPEC_ANALYSIS";
- public static final String IDType = "id_t";
+ public static final String IDType = "call_id_t";
public static final String SPEC_ANNO_TYPE = "spec_anno_type";
+ public static final String SPEC_ANNO_TYPE_FUNC_TABLE_INIT = "FUNC_TABLE_INIT";
public static final String SPEC_ANNO_TYPE_HB_INIT = "HB_INIT";
public static final String SPEC_ANNO_TYPE_INTERFACE_BEGIN = "INTERFACE_BEGIN";
public static final String SPEC_ANNO_TYPE_HB_CONDITION = "HB_CONDITION";
@@ -51,6 +53,7 @@ public class CodeVariables {
public static final String SPEC_ANNOTATION_FIELD_TYPE = "type";
public static final String SPEC_ANNOTATION_FIELD_ANNO = "annotation";
+ public static final String ANNO_FUNC_TABLE_INIT = "anno_func_table_init";
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";
@@ -158,7 +161,7 @@ public class CodeVariables {
for (int i = 0; i < header.args.size(); i++) {
code.add(DECLARE(header.args.get(i)));
}
- code.add("} " + interfaceName + "_info {");
+ code.add("} " + interfaceName + "_info;");
return code;
}
@@ -187,7 +190,7 @@ public class CodeVariables {
if (!header.returnType.equals("void") || header.args.size() != 0) {
String infoStructType = interfaceName + "_info", infoStructName = "theInfo";
code.add(DECLARE_DEFINE(infoStructType + "*", infoStructName,
- BRACE(infoStructType) + "info"));
+ BRACE(infoStructType + "*") + "info"));
if (!header.returnType.equals("void")) {
code.add((DECLARE_DEFINE(header.returnType, MACRO_RETURN,
GET_FIELD_BY_PTR(infoStructName, MACRO_RETURN))));
@@ -221,6 +224,8 @@ public class CodeVariables {
if (construct.postAction.size() > 0) {
code.addAll(construct.postAction);
}
+ // Return true finally
+ code.add("return true;");
code.add("}");
@@ -275,9 +280,11 @@ public class CodeVariables {
}
newCode.add("");
// Other necessary headers
+ newCode.add(INCLUDE(HEADER_STDLIB));
newCode.add(INCLUDE(HEADER_STDINT));
newCode.add(INCLUDE(HEADER_CDSANNOTATE));
newCode.add(INCLUDE(HEADER_SPEC_LIB));
+ newCode.add(INCLUDE(HEADER_SPECANNOTATION));
newCode.add("");
SequentialDefineSubConstruct code = construct.code;
@@ -289,6 +296,13 @@ public class CodeVariables {
newCode.addAll(declareStruct);
newCode.add("");
}
+ // User-defined variables
+ ArrayList<VariableDeclaration> varDecls = code.declareVar;
+ for (int i = 0; i < varDecls.size(); i++) {
+ VariableDeclaration varDecl = varDecls.get(i);
+ // Don't forget to make them static
+ newCode.add(makeVariablesStatic(varDecl));
+ }
// User-defined functions
newCode.add(COMMENT("All other user-defined functions"));
ArrayList<ArrayList<String>> defineFuncs = code.defineFuncs;
@@ -304,7 +318,8 @@ public class CodeVariables {
.get(interfaceName);
FunctionHeader funcHeader = getFunctionHeader(semantics, iConstruct);
// Define necessary info structure
- if (!funcHeader.returnType.equals("void") || funcHeader.args.size() > 0) {
+ if (!funcHeader.returnType.equals("void")
+ || funcHeader.args.size() > 0) {
newCode.add(COMMENT("Definition of interface info struct: "
+ interfaceName));
newCode.addAll(DEFINE_INFO_STRUCT(interfaceName, funcHeader));
@@ -316,14 +331,14 @@ public class CodeVariables {
// Define ID function
newCode.add(COMMENT("ID function of interface: " + interfaceName));
newCode.addAll(DEFINE_ID_FUNC(interfaceName, iConstruct.idCode));
- newCode.add(COMMENT("End of ID function: + " + interfaceName));
+ newCode.add(COMMENT("End of ID function: " + interfaceName));
newCode.add("");
// Define check_action function
newCode.add(COMMENT("Check action function of interface: "
+ interfaceName));
newCode.addAll(DEFINE_CHECK_ACTION_FUNC(iConstruct, funcHeader));
- newCode.add(COMMENT("End of check action function: + "
+ newCode.add(COMMENT("End of check action function: "
+ interfaceName));
newCode.add("");
}
@@ -332,13 +347,6 @@ public class CodeVariables {
.toString(semantics.interfaceName2Construct.size());
newCode.add(DEFINE("INTERFACE_SIZE", interfaceSize));
newCode.add(DECLARE("void**", "func_ptr_table"));
- // User-defined variables
- ArrayList<VariableDeclaration> varDecls = code.declareVar;
- for (int i = 0; i < varDecls.size(); i++) {
- VariableDeclaration varDecl = varDecls.get(i);
- // Don't forget to make them static
- newCode.add(makeVariablesStatic(varDecl));
- }
newCode.add("");
newCode.add(COMMENT("Define function for sequential code initialization"));
@@ -358,8 +366,19 @@ public class CodeVariables {
newCode.add("");
// Init user-defined variables
newCode.addAll(construct.code.initVar);
+ // Pass function table info
+ newCode.add(COMMENT("Pass function table info"));
+ String structName = "anno_func_table_init", anno = "func_init";
+ newCode.add(DECLARE(ANNO_FUNC_TABLE_INIT, structName));
+ newCode.add(ASSIGN(structName, "size", "INTERFACE_SIZE"));
+ newCode.add(ASSIGN(structName, "table", "func_ptr_table"));
+ newCode.add(DECLARE(SPEC_ANNOTATION, anno));
+ newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_FUNC_TABLE_INIT));
+ newCode.add(ASSIGN_PTR(anno, "annotation", structName));
+ newCode.add(ANNOTATE(anno));
+
// Pass Happens-before relationship
- generateHBInitAnnotation(semantics);
+ newCode.addAll(generateHBInitAnnotation(semantics));
newCode.add("}");
newCode.add(COMMENT("End of Global construct generation in class"));
@@ -470,6 +489,14 @@ public class CodeVariables {
}
// Generate wrapper header
+ // If it's not in a class, we should declare the wrapper function
+ if (semantics.getClassName() == null) {
+ FunctionHeader renamedHeader = header
+ .getRenamedHeader(SPEC_INTERFACE_WRAPPER);
+ newCode.add(COMMENT("Declaration of the wrapper"));
+ newCode.add(renamedHeader + ";");
+ newCode.add("");
+ }
newCode.add(header.toString() + " {");
// Wrapper function body
newCode.add(COMMENT("Interface begins"));
@@ -479,12 +506,12 @@ public class CodeVariables {
newCode.add(ASSIGN(structName, "interface_num", interfaceNum));
String anno = "annotation_interface_begin";
newCode.add(DECLARE(SPEC_ANNOTATION, anno));
- newCode.add(ASSIGN(structName, "type", SPEC_ANNO_TYPE_INTERFACE_BEGIN));
- newCode.add(ASSIGN_PTR(structName, "annotation", structName));
+ newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_INTERFACE_BEGIN));
+ newCode.add(ASSIGN_PTR(anno, "annotation", structName));
newCode.add(ANNOTATE(anno));
// Call original renamed function
if (header.returnType.equals("void")) {
- newCode.add(header.getRenamedCall(SPEC_INTERFACE_WRAPPER));
+ newCode.add(header.getRenamedCall(SPEC_INTERFACE_WRAPPER) + ";");
} else {
newCode.add(DECLARE_DEFINE(header.returnType, MACRO_RETURN,
header.getRenamedCall(SPEC_INTERFACE_WRAPPER)));
@@ -513,7 +540,7 @@ public class CodeVariables {
if (!header.returnType.equals("void") || header.args.size() > 0) {
infoStructType = interfaceName + "_info";
infoName = "info";
- newCode.add(DECLARE_DEFINE(infoStructType, infoName,
+ newCode.add(DECLARE_DEFINE(infoStructType + "*", infoName,
BRACE(infoStructType + "*") + " malloc(sizeof("
+ infoStructType + "))"));
if (!header.returnType.equals("void")) {
@@ -534,7 +561,11 @@ public class CodeVariables {
newCode.add(DECLARE(SPEC_ANNOTATION, anno));
newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_INTERFACE_END));
newCode.add(ASSIGN_PTR(anno, "annotation", structName));
- ANNOTATE(anno);
+ newCode.add(ANNOTATE(anno));
+ // Return __RET__ if it's not void
+ if (!header.returnType.equals("void")) {
+ newCode.add("return " + MACRO_RETURN + ";");
+ }
// End of the wrapper function
newCode.add("}");
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java b/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java
index 6d1c41e..654e579 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java
@@ -3,4 +3,7 @@ package edu.uci.eecs.specCompiler.codeGenerator;
public class Environment {
public static String HOME_DIRECTORY = System.getProperty("user.dir");
public static String GENERATED_FILE_DIR = HOME_DIRECTORY + "/" + "output";
+ public static String MODEL_CHECKER_HOME_DIR = System
+ .getProperty("user.home") + "/model-checker-priv";
+ public static String MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_HOME_DIR + "/test";
}
diff --git a/test.c b/test.c
index b279809..d771ce4 100644
--- a/test.c
+++ b/test.c
@@ -1,15 +1,9 @@
-# include <stdio.h>
-#include <stdlib.h>
-#include <stdint.h>
+#include <stdio.h>
-typedef struct A {
-
-} A;
+int test();
int main() {
- uint64_t i64 = (uint64_t) NULL;
- A *a = (A*) malloc (sizeof(A));
- printf("%d\n", sizeof(A));
+ int a = test();
printf("%d\n", a);
return 1;
}
diff --git a/test.cc b/test.cc
index 64a4e3b..56bc554 100644
--- a/test.cc
+++ b/test.cc
@@ -1,18 +1,3 @@
-class A {
- public:
- A() {
- }
-
-};
-
-
-int main() {
- A a;
- if (true) {
- int i = 5;
- }
- if (true) {
- int i = 1;
- }
- return 1;
+extern int test() {
+ return 10;
}
--
2.34.1