From 554647e9313ede3b8bd2ed6c00b92bf85cfb05c7 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Sat, 19 Oct 2013 04:16:14 -0700 Subject: [PATCH] add detailed generated code examples --- notes/generated_code_examples.txt | 213 ++++++++++++++++++ .../codeGenerator/CodeGenerator.java | 27 ++- .../codeGenerator/CodeVariables.java | 19 +- test.c | 16 +- test.h | 5 + 5 files changed, 262 insertions(+), 18 deletions(-) create mode 100644 notes/generated_code_examples.txt diff --git a/notes/generated_code_examples.txt b/notes/generated_code_examples.txt new file mode 100644 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 +#include + +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 +#include + +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 +#include +#include + +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 +#include +#include +#include +#include + +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 +#include +#include +#include +#include + +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 05a76a7..d051906 100644 --- 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()); diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java index 7e424e3..e0a41fa 100644 --- 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 417f795..0333725 100644 --- a/test.c +++ b/test.c @@ -1,22 +1,32 @@ #include #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 0b752a3..e421c4c 100644 --- 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 -- 2.34.1