save it

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 1cbe52545b26af849c1a2bfdfad2c0cf76d1093d..0f52b66b65f5887ed5e0ee6955d079eb3ac97b51 100644 (file)
--- 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 0993e2f349fccff1518a2b522909cf1ffb3e2318..2a7241c6156c00721d753f8592f1ab9938a779ec 100644 (file)
--- 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 a0bc9571a2e970be44eab36e22f93844b376c0b0..f18be8b3eae4b6c5fc2713b206aa088c35db2d65 100644 (file)
--- 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 20f6e53f9ecd90d45c0624d34b2ead19e4646db3..008ef66366277be3fb019e69e13f476815c86f6d 100644 (file)
--- 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 980e42064d74cb09dd1533fbeff413e5ab5591d1..af2ebcaf218008363756bfda7412ea2e78b81b4f 100644 (file)
--- 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 6d1c41e8d17558e932c57a057fb1557c43695c0f..654e57974b45cb5388ba54695fea3fede47c95de 100644 (file)
--- 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 b279809005cdebfc77f40ef6a8ecad4548f73c36..d771ce4368c0d8e0334826134f17bd4292323b0d 100644 (file)
--- 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 64a4e3b63c7a1034ac4c1140d8fd229fe4f26a44..56bc5546c28d0754ecd48157094eca5ce6b92b00 100644 (file)
--- 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;
 }