src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java

   1 package edu.uci.eecs.specCompiler.codeGenerator;
   2
   3 import java.util.ArrayList;
   4
   5 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
   6 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
   7 import edu.uci.eecs.specCompiler.specExtraction.IDExtractor;
   8 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
   9 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
  10 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
  11 import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
  12
  13 public class CodeVariables {
  14         // C++ code or library
  15         public static final String HEADER_THREADS = "threads.h";
  16         public static final String ThreadIDType = "thrd_t";
  17         public static final String GET_THREAD_ID = "thrd_current";
  18         public static final String BOOLEAN = "bool";
  19         public static final String UINT64 = "uint64_t";
  20
  21         // Model checker code
  22         public static final String HEADER_CDSANNOTATE = "cdsannotate.h";
  23         public static final String HEADER_SPECANNOTATION = "specannotation.h";
  24         public static final String HEADER_CDSTRACE = "cdstrace.h";
  25         public static final String CDSAnnotate = "cdsannotate";
  26         public static final String CDSAnnotateType = "SPEC_ANALYSIS";
  27
  28         public static final String SPEC_ANNO_TYPE = "spec_anno_type";
  29         public static final String SPEC_ANNO_TYPE_HB_INIT = "HB_INIT";
  30         public static final String SPEC_ANNO_TYPE_INTERFACE_BEGIN = "INTERFACE_BEGIN";
  31         public static final String SPEC_ANNO_TYPE_HB_CONDITION = "HB_CONDITION";
  32         public static final String SPEC_ANNO_TYPE_INTERFACE_END = "INTERFACE_END";
  33         public static final String SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE = "POTENTIAL_CP_DEFINE";
  34         public static final String SPEC_ANNOTATION = "spec_annotation";
  35         public static final String SPEC_ANNOTATION_FIELD_TYPE = "type";
  36         public static final String SPEC_ANNOTATION_FIELD_ANNO = "annotation";
  37
  38         public static final String ANNO_HB_INIT = "anno_hb_init";
  39         public static final String ANNO_INTERFACE_BOUNDARY = "anno_interface_boundary";
  40         public static final String ANNO_ID = "anno_id";
  41         public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potentail_cp_define";
  42         public static final String ANNO_CP_DEFINE = "anno_cp_define";
  43         public static final String ANNO_CP_DEFINE_CHECK = "anno_cp_define_check";
  44         public static final String ANNO_HB_CONDITION = "anno_hb_condition";
  45         public static final String ANNO_POST_CHECK = "anno_post_check";
  46
  47         // Specification variables
  48         public static final String HEADER_SPEC_SEQUENTIAL = "_spec_sequential.h";
  49         public static final String SPEC_SEQUENTIAL_HEADER_MACRO = HEADER_SPEC_SEQUENTIAL
  50                         .replace('.', '_').toUpperCase();
  51
  52         public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_";
  53         public static final String VAR_CALL_SEQUENCE_NUM = "call_sequence_num";
  54
  55         // Specification library
  56         public static final String SPEC_QUEUE = "spec_queue";
  57         public static final String SPEC_STACK = "spec_stack";
  58         public static final String SPEC_DEQUE = "spec_deque";
  59         public static final String SPEC_HASHTABLE = "spec_hashtable";
  60         public static final String HEADER_SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable.h";
  61         public static final String SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable";
  62         public static final String HEADER_SPEC_TAG = "spec_tag.h";
  63         public static final String SPEC_TAG = "spec_tag";
  64         public static final String SPEC_TAG_CURRENT = "current";
  65         public static final String SPEC_TAG_NEXT = "next";
  66
  67         // Macro
  68         public static final String MACRO_ID = "__ID__";
  69         public static final String MACRO_COND = "__COND_SAT__";
  70         public static final String MACRO_RETURN = "__RET__";
  71         public static final String MACRO_ATOMIC_RETURN = "__ATOMIC_RET__";
  72
  73         public static void printCode(ArrayList<String> code) {
  74                 for (int i = 0; i < code.size(); i++) {
  75                         System.out.println(code.get(i));
  76                 }
  77         }
  78
  79         private static String COMMENT(String comment) {
  80                 return "/* " + comment + " */";
  81         }
  82
  83         private static String INCLUDE(String header) {
  84                 return "#include <" + header + ">";
  85         }
  86
  87         private static String DEFINE(String left, String right) {
  88                 return "#define " + left + " " + right;
  89         }
  90
  91         private static String UNDEFINE(String macro) {
  92                 return "#undef " + macro;
  93         }
  94
  95         private static String BRACE(String val) {
  96                 return "(" + val + ")";
  97         }
  98
  99         private static String ASSIGN(String structName, String field, String val) {
 100                 return structName + "." + field + " = " + val + ";";
 101         }
 102
 103         private static String ASSIGN_PTR(String structName, String field, String val) {
 104                 return structName + "." + field + " = &" + val + ";";
 105         }
 106
 107         private static String DECLARE(String structType, String structName) {
 108                 return structType + " " + structName + ";";
 109         }
 110
 111         private static String DECLARE_DEFINE(String type, String var, String val) {
 112                 return type + " " + var + " = " + val + ";";
 113         }
 114
 115         private static String ANNOTATE(String structName) {
 116                 return CDSAnnotate + "(" + CDSAnnotateType + ", &" + structName + ");";
 117         }
 118
 119         public static ArrayList<String> generateGlobalVarDeclaration(
 120                         SemanticsChecker semantics, GlobalConstruct construct) {
 121                 ArrayList<String> newCode = new ArrayList<String>();
 122
 123                 // Header conflicting avoidance macro & headers
 124                 newCode.add("/** @file " + HEADER_SPEC_SEQUENTIAL);
 125                 newCode.add(" *  @brief Automatically generated header file for sequential variables");
 126                 newCode.add(" */");
 127                 newCode.add("#ifndef " + SPEC_SEQUENTIAL_HEADER_MACRO);
 128                 newCode.add("#define " + SPEC_SEQUENTIAL_HEADER_MACRO);
 129                 newCode.add("");
 130                 newCode.add(INCLUDE(HEADER_SPEC_PRIVATE_HASHTABLE));
 131                 newCode.add(INCLUDE(HEADER_SPECANNOTATION));
 132                 newCode.add(INCLUDE(HEADER_SPEC_TAG));
 133                 newCode.add("");
 134
 135
 136
 137                 // printCode(newCode);
 138                 return newCode;
 139         }
 140
 141         private static ArrayList<String> generateHBInitAnnotation(
 142                         SemanticsChecker semantics) {
 143                 ArrayList<String> newCode = new ArrayList<String>();
 144                 int hbConditionInitIdx = 0;
 145                 for (ConditionalInterface left : semantics.getHBConditions().keySet()) {
 146                         for (ConditionalInterface right : semantics.getHBConditions().get(
 147                                         left)) {
 148                                 String structVarName = "hbConditionInit" + hbConditionInitIdx;
 149                                 String annotationVarName = "hb_init" + hbConditionInitIdx;
 150                                 hbConditionInitIdx++;
 151                                 String interfaceNumBefore = Integer
 152                                                 .toString(semantics.interface2Num
 153                                                                 .get(left.interfaceName)), hbLabelNumBefore = Integer
 154                                                 .toString(semantics.hbLabel2Num
 155                                                                 .get(left.hbConditionLabel)), interfaceNumAfter = Integer
 156                                                 .toString(semantics.interface2Num
 157                                                                 .get(right.interfaceName)), hbLabelNumAfter = Integer
 158                                                 .toString(semantics.hbLabel2Num
 159                                                                 .get(right.hbConditionLabel));
 160                                 newCode.add(COMMENT(left + " -> " + right));
 161
 162                                 newCode.add(ANNO_HB_INIT + " " + structVarName + ";");
 163                                 newCode.add(ASSIGN(structVarName, "interface_num_before",
 164                                                 interfaceNumBefore));
 165                                 newCode.add(ASSIGN(structVarName, "hb_condition_num_before",
 166                                                 hbLabelNumBefore));
 167                                 newCode.add(ASSIGN(structVarName, "interface_num_after",
 168                                                 interfaceNumAfter));
 169                                 newCode.add(ASSIGN(structVarName, "hb_condition_num_after",
 170                                                 hbLabelNumAfter));
 171
 172                                 newCode.add(DECLARE(SPEC_ANNOTATION, annotationVarName));
 173                                 newCode.add(ASSIGN(annotationVarName,
 174                                                 SPEC_ANNOTATION_FIELD_TYPE, SPEC_ANNO_TYPE_HB_INIT));
 175                                 newCode.add(ASSIGN_PTR(annotationVarName,
 176                                                 SPEC_ANNOTATION_FIELD_ANNO, structVarName));
 177                                 newCode.add(ANNOTATE(annotationVarName));
 178                         }
 179                 }
 180                 return newCode;
 181         }
 182
 183         public static ArrayList<String> generateInterfaceWrapper(
 184                         SemanticsChecker semantics, InterfaceConstruct construct) {
 185                 ArrayList<String> newCode = new ArrayList<String>();
 186
 187                 // Generate necessary header file (might be redundant but never mind)
 188
 189
 190                 // Generate wrapper header
 191
 192
 193                 // Wrapper function body
 194
 195                 // Interface begin
 196
 197                 // Call original renamed function
 198
 199                 // HB conditions
 200
 201
 202                 // Interface end
 203
 204
 205                 // End of the wrapper function
 206
 207
 208 //              printCode(newCode);
 209                 return newCode;
 210         }
 211
 212         public static ArrayList<String> generatePotentialCPDefine(
 213                         SemanticsChecker semantics, PotentialCPDefineConstruct construct) {
 214                 ArrayList<String> newCode = new ArrayList<String>();
 215
 216                 // Generate redundant header files
 217                 newCode.add(COMMENT("Automatically generated code for potential commit point: "
 218                                 + construct.label));
 219                 newCode.add(COMMENT("Include redundant headers"));
 220                 newCode.add(INCLUDE(HEADER_THREADS));
 221                 newCode.add(INCLUDE(HEADER_CDSTRACE));
 222                 newCode.add(INCLUDE(HEADER_SPEC_PRIVATE_HASHTABLE));
 223                 newCode.add(INCLUDE(HEADER_SPEC_SEQUENTIAL));
 224                 newCode.add("");
 225                 // Some necessary function calls
 226
 227
 228                 return newCode;
 229         }
 230 }