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

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