add detailed generated code examples

diff --git a/notes/generated_code_examples.txt b/notes/generated_code_examples.txt
new file mode 100644 (file)
index 0000000..5b8c279
--- /dev/null
+++ b/notes/generated_code_examples.txt
@@ -0,0 +1,213 @@
+******    Example1:    ******
+Global Variable Declaration
+
+/* Include the header files first
+** This declaration will be written into a header file
+*/
+/* @file CDSName.h */
+/* @brief automatically generated file */
+#ifndef _CDSNAME_H
+#define _CDSNAME_H
+#include <specannotation.h>
+#include <spec_private_hashtable.h>
+
+typedef struct Sequential
+{
+       spec_private_hashtabel cond;
+       spec_private_hashtabel id;
+       spec_private_hashtabel interface;
+       spec_private_hashtabel interface_call_sequence;
+
+       /* DefineVar unfolded here */
+       spec_private_hashtable Put__Old_Val;
+
+       /* Other user-defined variables */
+       bool lock_acquired;
+       int reader_lock_cnt;
+} Sequential;
+
+Sequential __sequential;
+
+/* All other user-defined functions */
+ALL_USER_DEFINED_FUNCTIONS
+
+
+#endif
+
+
+
+******    Example2:    ******
+Global Variable Initialization (Entry Point Unfolding)
+
+#include <spec_private_hashtable.h>
+#include <CDSName.h>
+
+init(&__sequential.condition);
+init(&__sequential.id);
+init(&__sequential.interface);
+init(&__sequential.interface_call_sequence);
+/* DefineVar initialized here */
+init(&Put__Old_Val);
+
+/* User-define variables */
+lock_acquired = false;
+reader_lock_cnt = 0;
+
+
+
+******    Example3:    ******
+Interface Wrapper
+
+/* Include the header files first */
+#include <threads.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+
+TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
+{
+       thrd_t tid = thrd_current();
+       uint64_t call_sequence_num = current(&__interface_call_sequence);
+       put(&__interface_call_sequence, tid, call_sequence_num);
+
+       // Interface begins
+       anno_interface_boundary interface_boundary;
+       interface_boundary.interface_num = 0; // Interface number
+       interface_boundary.call_sequence_num = call_sequence_num;
+       spec_annotation annotation_interface_begin;
+       annotation_interface_begin.type = INTERFACE_BEGIN;
+       annotation_interface_begin.annotation = &interface_boundary;
+       cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
+
+       TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
+       bool __COND__ = get(&__cond, tid);
+       uint64_t id = get(&__id, tid);
+
+       // HB conditions (if any)
+       if (HB_CONDITION1) {
+               anno_hb_condition hb_condition1;
+               hb_condition1.interface_num = 0; // Interface number
+               hb_condition1.hb_condition_num = 1; // HB condition number
+               hb_condition1.id = id;
+               hb_condition1.call_sequence_num = call_sequence_num;
+               spec_annotation annotation_hb_condition;
+               annotation_hb_condition.type = HB_CONDITION;
+               annotation_hb_condition.annotation = &hb_condition;
+               cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
+               // And more (if any)
+       }
+
+       // Post check (if any)
+       bool post_check_passed = POST_CHECK_CONDITION;
+       anno_post_check post_check;
+       post_check.check_passed = post_check_passed;
+       post_check.interface_num = interface_num;
+       post_check.call_sequence_num = call_sequence_num;
+       spec_annotation annotation_post_check;
+       annotation_post_check.type = POST_CHECK;
+       annotation_post_check.annotation = &post_check;
+       cdsannotate(SPEC_ANALYSIS, &annotation_post_check);
+
+       // Post Action (if any)
+       POST_ACTION_CODE // Unfolded in place
+
+       // Interface ends
+       spec_annotation annotation_interface_end;
+       annotation_interface_end.type = INTERFACE_END;
+       annotation_interface_end.annotation = &interface_boundary;
+       cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
+}
+
+
+******    Example4:    ******
+Potential Commit Point
+
+#include <threads.h>
+#include <cdstrace.h>
+#include <cdsannotate.h>
+#include <spec_private_hashtable.h>
+#include <CDSName.h>
+
+thrd_t __tid = thrd_current();
+uint64_t __ATOMIC_RET__ = get_prev_value(tid);
+if (POTENTIAL_CP_DEFINE_CONDITION) {
+       uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
+       int interface_num = get(&__sequential.interface, tid);
+       anno_potential_cp_define potential_cp_define;
+       potential_cp_define.interface_num = interface_num;
+       potential_cp_define.label_num = 1; // Commit point label number
+       potential_cp_define.call_sequence_num = call_sequence_num;
+       spec_annotation annotation_potential_cp_define;
+       annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
+       annotation_potential_cp_define.annotation = &potential_cp_define;
+       cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
+}
+
+******    Example5:    ******
+Commit Point Define
+
+#include <threads.h>
+#include <cdstrace.h>
+#include <cdsannotate.h>
+#include <spec_private_hashtable.h>
+#include <CDSName.h>
+
+thrd_t __tid = thrd_current();
+int interface_num = get(&__sequential.interface, tid);
+/* For all the interface check at this commit point (if there is multiple
+ * checks here) */
+/* Need to compute the relationship between labels before hand */
+switch (interface_num) {
+       case 0:
+               // Commit point 3 <=> potentialCP 4
+               if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) {
+                       if (INTERFACE0_CHECK_CONDITION) {
+                               check_passed = true;
+                       }
+                       /* For all DefineVar of INTERFACE0 (Type id = Expr) */
+                       FIXME: Type res0 = Expr;
+                       put(__sequential.put_id, tid, 
+                       #define _Old_Val __sequential.put_id
+                       INTERFACE0_ACTION; // Unfolded right in place
+
+                       anno_cp_define cp_define;
+                       uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
+                       bool check_passed = false;
+                       cp_define.check_passed = check_passed;
+                       cp_define.interface_num = interface_num;
+                       cp_define.label_num = 3;
+                       cp_define.call_sequence_num = call_sequence_num;
+                       spec_annotation annotation_cp_define;
+                       annotation_cp_define.type = CP_DEFINE;
+                       annotation_cp_define.annotation = &cp_define;
+                       cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
+               }
+               break;
+       case 1:
+               // Commit point 5 <=> potentialCP 6
+               if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) {
+                       if (INTERFACE1_CHECK_CONDITION) {
+                               check_passed = true;
+                       }
+                       INTERFACE1_ACTION; // Unfolded right in place
+
+                       anno_cp_define cp_define;
+                       uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
+                       bool check_passed = false;
+                       cp_define.check_passed = check_passed;
+                       cp_define.interface_num = interface_num;
+                       cp_define.label_num = 5;
+                       cp_define.call_sequence_num = call_sequence_num;
+                       spec_annotation annotation_cp_define;
+                       annotation_cp_define.type = CP_DEFINE;
+                       annotation_cp_define.annotation = &cp_define;
+                       cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
+               }
+               break;
+       default:
+               break;
+}
+
+
+*****    Example6:    ******
+Commit Point Define Check
+

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 05a76a79e8d113534e5f956b498ff8084bb61f37..d051906210e7b3c7c72fa25cfff85f16a3975649 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -112,7 +112,6 @@ public class CodeGenerator {
                                + ";");
                // __ID__
                newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_ID + ";");
-
                // DefineVars
                for (String interfaceName : _semantics.interfaceName2Construct.keySet()) {
                        InterfaceConstruct iConstruct = (InterfaceConstruct) _semantics.interfaceName2Construct
@@ -124,11 +123,15 @@ public class CodeGenerator {
                                                + ";");
                        }
                }
-
                // __interface
                newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_INTERFACE
                                + ";");
-
+               // __interface_call_sequence
+               newCode.add(CodeVariables.SPEC_HASHTABLE
+                               + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ";");
+               // Interface call sequence varaiable
+               newCode.add(CodeVariables.SPEC_TAG + " "
+                               + CodeVariables.INTERFACE_CALL_SEQUENCE + ";");
                // End of the struct
                newCode.add("}");
 
@@ -151,12 +154,14 @@ public class CodeGenerator {
                }
                // __interface
                newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE + ");");
+               // __interface_call_sequence
+               newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ");");
 
                // Pass the happens-before relationship check here
                newCode.addAll(CodeVariables.generateHBInitAnnotation(_semantics));
 
                newCode.add("\n");
-               
+
                // Generate the sequential functions
                breakCodeLines(newCode, globalCode.defineFunc);
 
@@ -210,15 +215,19 @@ public class CodeGenerator {
                }
 
                // Generate new wrapper
-               breakCodeLines(newCode, funcDecl);
+               /**
+                * 
+                * 
+                */
 
+               breakCodeLines(newCode, funcDecl);
                newCode.add("{");
-
-               // Generate
-
+               // Generate interface sequence call
+               newCode.add(CodeVariables.UINT64 + " call_sequence_num = current(&"
+                               + CodeVariables.INTERFACE_CALL_SEQUENCE + ");");
                // FIXME: Add Happens-before check here
-
                newCode.add("}");
+
                CodeAddition addition = new CodeAddition(lineNum, newCode);
                if (!codeAdditions.containsKey(inst.file)) {
                        codeAdditions.put(inst.file, new ArrayList<CodeAddition>());

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index 7e424e34bd0d5ccc9fa5d986d7a344fd6de2f954..e0a41fa2593bc692b15689fb34f5964a16808e7a 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -6,20 +6,25 @@ import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
 
 public class CodeVariables {
        // C++ code or library
-       public static final String ThreadIDType = "thread_id_t";
+       public static final String HEADER_threads = "threads.h";
+       public static final String ThreadIDType = "thrd_t";
+       public static final String GET_THREAD_ID = "thrd_current";
        public static final String BOOLEAN = "bool";
+       public static final String UINT64 = "uint64_t";
 
        // Model checker code
        public static final String HEADER_CDSAnnotate = "cdsannotate.h";
+       public static final String HEADER_SPECANNOTATION = "specannotation.h";
        public static final String CDSAnnotate = "cdsannotate";
        public static final String CDSAnnotateType = "SPEC_ANALYSIS";
+       // It's a SPEC_TAG type, it has current() and next() function
+       public static final String INTERFACE_CALL_SEQUENCE = "__interface_call_sequence";
 
        public static final String SPEC_ANNOTATION_TYPE = "spec_anno_type";
        public static final String SPEC_ANNOTATION = "spec_annotation";
 
        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_INTERFACE_BOUNDARY = "anno_interface_boundary";
        public static final String ANNO_ID = "anno_id";
        public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potentail_cp_define";
        public static final String ANNO_CP_DEFINE = "anno_cp_define";
@@ -31,9 +36,10 @@ public class CodeVariables {
        public static final String SPEC_STRUCT = "Sequential";
        public static final String SPEC_INSTANCE = "__sequential";
 
-       public static final String SPEC_CONDITION = "__cond";
-       public static final String SPEC_ID = "__id";
-       public static final String SPEC_INTERFACE = "__interface";
+       public static final String SPEC_CONDITION = "condition";
+       public static final String SPEC_ID = "id";
+       public static final String SPEC_INTERFACE = "interface";
+       public static final String SPEC_INTERFACE_CALL_SEQUENCE = "interface_call_sequence";
 
        public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_";
 
@@ -41,6 +47,7 @@ public class CodeVariables {
        public static final String SPEC_QUEUE = "spec_queue";
        public static final String SPEC_STACK = "spec_stack";
        public static final String SPEC_HASHTABLE = "spec_hashtable";
+       public static final String SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable";
        public static final String SPEC_TAG = "spec_tag";
 
        // Macro

diff --git a/test.c b/test.c
index 417f795ccef101c0e1cf47e4bf56429a894ab27c..0333725e45bc790405032234454bc3311ef54a08 100644 (file)
--- a/test.c
+++ b/test.c
@@ -1,22 +1,32 @@
 #include <stdio.h>
 #include "test.h"
+#include "test.h"
 
-struct XX {
-       
+struct pair {
+       int x, y;
 };
 
+struct pair p[] = {{1,2}, {2,3}};
+
 enum E {
        a, b, c
 };
-
+const int inte = 3;
 void _foo(struct Test t) {
+       for (int i = 0; i < 10; i++) {
+               int j;
+       }
        printf("%d\n", t.x);
 }
 
 void foo(struct Test t) {
+       int num[] = {5, 3};
        _foo(t);
 }
 
+void func() {
+}
+
 int main() {
        printf("%d\n", b);
        return 0;

diff --git a/test.h b/test.h
index 0b752a38c2bd7715931e679c8568d44465d60435..e421c4c01f7fee28585d685af177496ea88f830f 100644 (file)
--- a/test.h
+++ b/test.h
@@ -1,3 +1,6 @@
+#ifndef _TEST_H
+#define _TEST_H
+
 struct Test {
        int x;
 /*
@@ -6,3 +9,5 @@ struct Test {
        }
        */
 };
+
+#endif