1 package edu.uci.eecs.specCompiler.codeGenerator;
3 import java.util.ArrayList;
5 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
7 public class CodeVariables {
9 public static final String HEADER_threads = "threads.h";
10 public static final String ThreadIDType = "thrd_t";
11 public static final String GET_THREAD_ID = "thrd_current";
12 public static final String BOOLEAN = "bool";
13 public static final String UINT64 = "uint64_t";
16 public static final String HEADER_CDSAnnotate = "cdsannotate.h";
17 public static final String HEADER_SPECANNOTATION = "specannotation.h";
18 public static final String CDSAnnotate = "cdsannotate";
19 public static final String CDSAnnotateType = "SPEC_ANALYSIS";
20 // It's a SPEC_TAG type, it has current() and next() function
21 public static final String INTERFACE_CALL_SEQUENCE = "__interface_call_sequence";
23 public static final String SPEC_ANNOTATION_TYPE = "spec_anno_type";
24 public static final String SPEC_ANNOTATION = "spec_annotation";
26 public static final String ANNO_HB_INIT = "anno_hb_init";
27 public static final String ANNO_INTERFACE_BOUNDARY = "anno_interface_boundary";
28 public static final String ANNO_ID = "anno_id";
29 public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potentail_cp_define";
30 public static final String ANNO_CP_DEFINE = "anno_cp_define";
31 public static final String ANNO_CP_DEFINE_CHECK = "anno_cp_define_check";
32 public static final String ANNO_HB_CONDITION = "anno_hb_condition";
33 public static final String ANNO_POST_CHECK = "anno_post_check";
35 // Specification variables
36 public static final String SPEC_STRUCT = "Sequential";
37 public static final String SPEC_INSTANCE = "__sequential";
39 public static final String SPEC_CONDITION = "condition";
40 public static final String SPEC_ID = "id";
41 public static final String SPEC_INTERFACE = "interface";
42 public static final String SPEC_INTERFACE_CALL_SEQUENCE = "interface_call_sequence";
44 public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_";
46 // Specification library
47 public static final String SPEC_QUEUE = "spec_queue";
48 public static final String SPEC_STACK = "spec_stack";
49 public static final String SPEC_HASHTABLE = "spec_hashtable";
50 public static final String SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable";
51 public static final String SPEC_TAG = "spec_tag";
54 public static final String MACRO_ID = "__ID__";
55 public static final String MACRO_COND = "__COND_SAT__";
56 public static final String MACRO_RETURN = "__RET__";
58 public static ArrayList<String> generateHBInitAnnotation(
59 SemanticsChecker semantics) {
60 ArrayList<String> newCode = new ArrayList<String>();
61 int hbConditionInitIdx = 0;
62 for (ConditionalInterface left : semantics.getHBConditions().keySet()) {
63 for (ConditionalInterface right : semantics.getHBConditions().get(
65 String structVarName = "hbConditionInit" + hbConditionInitIdx;
67 int interfaceNumBefore = semantics.interface2Num
68 .get(left.interfaceName), hbLabelNumBefore = semantics.hbLabel2Num
69 .get(left.hbConditionLabel), interfaceNumAfter = semantics.interface2Num
70 .get(right.interfaceName), hbLabelNumAfter = semantics.hbLabel2Num
71 .get(right.hbConditionLabel);
72 newCode.add(ANNO_HB_INIT + " " + structVarName + ";");
74 newCode.add(structVarName + "." + "interface_num_before"
75 + " = " + interfaceNumBefore + ";");
76 newCode.add(structVarName + "." + "hb_condition_num_before"
77 + " = " + hbLabelNumBefore + ";");
78 newCode.add(structVarName + "." + "interface_num_after" + " = "
79 + interfaceNumAfter + ";");
80 newCode.add(structVarName + "." + "hb_condition_num_after"
81 + " = " + hbLabelNumAfter + ";");
83 newCode.add(CDSAnnotate + "(" + CDSAnnotateType + ", &" + structVarName + ");");