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.grammerParser.ParseException;
   8 import edu.uci.eecs.specCompiler.grammerParser.SpecParser;
   9 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
  10 import edu.uci.eecs.specCompiler.specExtraction.FunctionHeader;
  11 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
  12 import edu.uci.eecs.specCompiler.specExtraction.IDExtractor;
  13 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
  14 import edu.uci.eecs.specCompiler.specExtraction.ParserUtils;
  15 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
  16 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
  17 import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
  18 import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
  19
  20 public class CodeVariables {
  21         // C++ code or library
  22         public static final String HEADER_THREADS = "<threads.h>";
  23         public static final String HEADER_STDINT = "<stdint.h>";
  24         public static final String ThreadIDType = "thrd_t";
  25         public static final String GET_THREAD_ID = "thrd_current";
  26         public static final String BOOLEAN = "bool";
  27         public static final String UINT64 = "uint64_t";
  28
  29         // Model checker code
  30         public static final String HEADER_CDSANNOTATE = "<cdsannotate.h>";
  31         public static final String HEADER_SPECANNOTATION = "<specannotation.h>";
  32         public static final String HEADER_CDSTRACE = "<cdstrace.h>";
  33         public static final String CDSAnnotate = "cdsannotate";
  34         public static final String CDSAnnotateType = "SPEC_ANALYSIS";
  35         public static final String IDType = "id_t";
  36
  37         public static final String SPEC_ANNO_TYPE = "spec_anno_type";
  38         public static final String SPEC_ANNO_TYPE_HB_INIT = "HB_INIT";
  39         public static final String SPEC_ANNO_TYPE_INTERFACE_BEGIN = "INTERFACE_BEGIN";
  40         public static final String SPEC_ANNO_TYPE_HB_CONDITION = "HB_CONDITION";
  41         public static final String SPEC_ANNO_TYPE_INTERFACE_END = "INTERFACE_END";
  42         public static final String SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE = "POTENTIAL_CP_DEFINE";
  43         public static final String SPEC_ANNOTATION = "spec_annotation";
  44         public static final String SPEC_ANNOTATION_FIELD_TYPE = "type";
  45         public static final String SPEC_ANNOTATION_FIELD_ANNO = "annotation";
  46
  47         public static final String ANNO_HB_INIT = "anno_hb_init";
  48         public static final String ANNO_INTERFACE_BOUNDARY = "anno_interface_boundary";
  49         public static final String ANNO_ID = "anno_id";
  50         public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potentail_cp_define";
  51         public static final String ANNO_CP_DEFINE = "anno_cp_define";
  52         public static final String ANNO_CP_DEFINE_CHECK = "anno_cp_define_check";
  53         public static final String ANNO_HB_CONDITION = "anno_hb_condition";
  54         public static final String ANNO_POST_CHECK = "anno_post_check";
  55
  56         // Specification variables
  57         public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_";
  58         public static final String DEFAULT_ID = "0";
  59
  60         // Specification library
  61         public static final String HEADER_SPEC_LIB = "<spec_lib.h>";
  62         public static final String SPEC_QUEUE = "spec_queue";
  63         public static final String SPEC_STACK = "spec_stack";
  64         public static final String SPEC_DEQUE = "spec_deque";
  65         public static final String SPEC_HASHTABLE = "spec_hashtable";
  66         public static final String SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable";
  67         public static final String SPEC_TAG = "spec_tag";
  68         public static final String SPEC_TAG_CURRENT = "current";
  69         public static final String SPEC_TAG_NEXT = "next";
  70
  71         // Macro
  72         public static final String MACRO_ID = "__ID__";
  73         public static final String MACRO_COND = "__COND_SAT__";
  74         public static final String MACRO_RETURN = "__RET__";
  75         public static final String MACRO_ATOMIC_RETURN = "__ATOMIC_RET__";
  76
  77         public static void printCode(ArrayList<String> code) {
  78                 for (int i = 0; i < code.size(); i++) {
  79                         System.out.println(code.get(i));
  80                 }
  81         }
  82
  83         private static String COMMENT(String comment) {
  84                 return "/* " + comment + " */";
  85         }
  86
  87         private static String INCLUDE(String header) {
  88                 return "#include " + header;
  89         }
  90
  91         private static String DEFINE(String left, String right) {
  92                 return "#define " + left + " " + right;
  93         }
  94
  95         private static String UNDEFINE(String macro) {
  96                 return "#undef " + macro;
  97         }
  98
  99         private static String BRACE(String val) {
 100                 return "(" + val + ")";
 101         }
 102
 103         private static String ASSIGN(String structName, String field, String val) {
 104                 return structName + "." + field + " = " + val + ";";
 105         }
 106
 107         private static String ASSIGN_PTR(String structName, String field, String val) {
 108                 return structName + "." + field + " = &" + val + ";";
 109         }
 110
 111         private static String DECLARE(String type, String name) {
 112                 return type + " " + name + ";";
 113         }
 114
 115         private static String DECLARE(VariableDeclaration varDecl) {
 116                 String type = varDecl.type, name = varDecl.name;
 117                 return type + " " + name + ";";
 118         }
 119
 120         private static String DECLARE_DEFINE(String type, String var, String val) {
 121                 return type + " " + var + " = " + val + ";";
 122         }
 123
 124         private static String ANNOTATE(String structName) {
 125                 return CDSAnnotate + "(" + CDSAnnotateType + ", &" + structName + ");";
 126         }
 127
 128         private static ArrayList<String> DEFINE_INFO_STRUCT(String interfaceName,
 129                         FunctionHeader funcDecl) {
 130                 ArrayList<String> code = new ArrayList<String>();
 131                 code.add("typedef struct " + interfaceName + "_info {");
 132                 code.add(DECLARE(funcDecl.returnType, MACRO_RETURN));
 133                 for (int i = 0; i < funcDecl.args.size(); i++) {
 134                         code.add(DECLARE(funcDecl.args.get(i)));
 135                 }
 136                 code.add("} " + interfaceName + "_info {");
 137                 return code;
 138         }
 139
 140         private static ArrayList<String> DEFINE_ID_FUNC(String interfaceName,
 141                         String idCode) {
 142                 ArrayList<String> code = new ArrayList<String>();
 143                 code.add("static " + IDType + " " + interfaceName + "_id() {");
 144                 if (idCode != null) {
 145                         code.add(DECLARE_DEFINE(IDType, MACRO_ID, idCode));
 146                 } else {
 147                         code.add(DECLARE_DEFINE(IDType, MACRO_ID, DEFAULT_ID));
 148                 }
 149                 code.add("return " + MACRO_ID + ";");
 150                 code.add("}");
 151                 return code;
 152         }
 153
 154         private static HashSet<String> getAllHeaders(SemanticsChecker semantics) {
 155                 HashSet<String> headers = new HashSet<String>();
 156                 for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
 157                         File f = semantics.interfaceName2Construct.get(interfaceName).file;
 158                         headers.addAll(semantics.srcFilesInfo.get(f).headers);
 159                 }
 160                 return headers;
 161         }
 162
 163         private static void makeFunctionStatic(ArrayList<String> funcDefine) {
 164                 String headLine = funcDefine.get(0);
 165                 headLine = "static " + headLine;
 166                 funcDefine.set(0, headLine);
 167         }
 168
 169         private static void makeVariablesStatic(ArrayList<String> varDecls) {
 170                 for (int i = 0; i < varDecls.size(); i++) {
 171                         String varDecl = varDecls.get(i);
 172                         varDecl = "static " + varDecl;
 173                         varDecls.set(i, varDecl);
 174                 }
 175         }
 176
 177         private static FunctionHeader getFunctionHeader(SemanticsChecker semantics,
 178                         InterfaceConstruct construct) {
 179                 ArrayList<String> content = semantics.srcFilesInfo.get(construct.file).content;
 180                 String headerLine = content.get(construct.beginLineNum);
 181                 try {
 182                         return SpecParser.parseFuncHeader(headerLine);
 183                 } catch (ParseException e) {
 184                         e.printStackTrace();
 185                 }
 186                 return null;
 187         }
 188
 189         public static ArrayList<String> generateGlobalVarDeclaration(
 190                         SemanticsChecker semantics, GlobalConstruct construct) {
 191                 ArrayList<String> newCode = new ArrayList<String>();
 192                 HashSet<String> allHeaders = getAllHeaders(semantics);
 193
 194                 // All headers needed by the interface decalration
 195                 newCode.add(COMMENT("/* Include all the header files that contains the interface declaration */"));
 196                 for (String header : allHeaders) {
 197                         newCode.add(INCLUDE(header));
 198                 }
 199                 newCode.add("");
 200                 // Other necessary headers
 201                 newCode.add(INCLUDE(HEADER_STDINT));
 202                 newCode.add(INCLUDE(HEADER_CDSANNOTATE));
 203                 newCode.add(INCLUDE(HEADER_SPEC_LIB));
 204                 newCode.add("");
 205
 206                 SequentialDefineSubConstruct code = construct.code;
 207                 // User-defined functions
 208                 newCode.add(COMMENT("All other user-defined functions"));
 209                 ArrayList<ArrayList<String>> defineFuncs = code.defineFuncs;
 210                 for (int i = 0; i < defineFuncs.size(); i++) {
 211                         ArrayList<String> defineFunc = defineFuncs.get(i);
 212                         makeFunctionStatic(defineFunc);
 213                         newCode.addAll(defineFunc);
 214                         newCode.add("");
 215                 }
 216
 217                 for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
 218                         InterfaceConstruct iConstruct = semantics.interfaceName2Construct
 219                                         .get(interfaceName);
 220                         FunctionHeader funcHeader = getFunctionHeader(semantics, iConstruct);
 221                         // Define necessary info structure
 222                         newCode.add(COMMENT("Definition of interface info struct: "
 223                                         + interfaceName));
 224                         newCode.addAll(DEFINE_INFO_STRUCT(interfaceName, funcHeader));
 225                         newCode.add(COMMENT("End of info struct definition: "
 226                                         + interfaceName));
 227                         newCode.add("");
 228
 229                         // Define ID function
 230                         newCode.add(COMMENT("ID functions of interface: " + interfaceName));
 231                         newCode.addAll(DEFINE_ID_FUNC(interfaceName, iConstruct.idCode));
 232                         newCode.add("");
 233                         newCode.add(COMMENT("End of ID function: + " + interfaceName));
 234                         newCode.add("");
 235
 236                         // Define check_action function
 237
 238
 239                 }
 240
 241                 // User-defined variables
 242                 ArrayList<VariableDeclaration> varDecls = code.declareVar;
 243                 for (int i = 0; i < varDecls.size(); i++) {
 244                         VariableDeclaration varDecl = varDecls.get(i);
 245                         newCode.add(DECLARE(varDecl.type, varDecl.name));
 246                 }
 247
 248                 // printCode(newCode);
 249                 return newCode;
 250         }
 251
 252         private static ArrayList<String> generateHBInitAnnotation(
 253                         SemanticsChecker semantics) {
 254                 ArrayList<String> newCode = new ArrayList<String>();
 255                 int hbConditionInitIdx = 0;
 256                 for (ConditionalInterface left : semantics.getHBConditions().keySet()) {
 257                         for (ConditionalInterface right : semantics.getHBConditions().get(
 258                                         left)) {
 259                                 String structVarName = "hbConditionInit" + hbConditionInitIdx;
 260                                 String annotationVarName = "hb_init" + hbConditionInitIdx;
 261                                 hbConditionInitIdx++;
 262                                 String interfaceNumBefore = Integer
 263                                                 .toString(semantics.interface2Num
 264                                                                 .get(left.interfaceName)), hbLabelNumBefore = Integer
 265                                                 .toString(semantics.hbLabel2Num
 266                                                                 .get(left.hbConditionLabel)), interfaceNumAfter = Integer
 267                                                 .toString(semantics.interface2Num
 268                                                                 .get(right.interfaceName)), hbLabelNumAfter = Integer
 269                                                 .toString(semantics.hbLabel2Num
 270                                                                 .get(right.hbConditionLabel));
 271                                 newCode.add(COMMENT(left + " -> " + right));
 272
 273                                 newCode.add(ANNO_HB_INIT + " " + structVarName + ";");
 274                                 newCode.add(ASSIGN(structVarName, "interface_num_before",
 275                                                 interfaceNumBefore));
 276                                 newCode.add(ASSIGN(structVarName, "hb_condition_num_before",
 277                                                 hbLabelNumBefore));
 278                                 newCode.add(ASSIGN(structVarName, "interface_num_after",
 279                                                 interfaceNumAfter));
 280                                 newCode.add(ASSIGN(structVarName, "hb_condition_num_after",
 281                                                 hbLabelNumAfter));
 282
 283                                 newCode.add(DECLARE(SPEC_ANNOTATION, annotationVarName));
 284                                 newCode.add(ASSIGN(annotationVarName,
 285                                                 SPEC_ANNOTATION_FIELD_TYPE, SPEC_ANNO_TYPE_HB_INIT));
 286                                 newCode.add(ASSIGN_PTR(annotationVarName,
 287                                                 SPEC_ANNOTATION_FIELD_ANNO, structVarName));
 288                                 newCode.add(ANNOTATE(annotationVarName));
 289                         }
 290                 }
 291                 return newCode;
 292         }
 293
 294         public static ArrayList<String> generateInterfaceWrapper(
 295                         SemanticsChecker semantics, InterfaceConstruct construct) {
 296                 ArrayList<String> newCode = new ArrayList<String>();
 297
 298                 // Generate necessary header file (might be redundant but never mind)
 299
 300                 // Generate wrapper header
 301
 302                 // Wrapper function body
 303
 304                 // Interface begin
 305
 306                 // Call original renamed function
 307
 308                 // HB conditions
 309
 310                 // Interface end
 311
 312                 // End of the wrapper function
 313
 314                 // printCode(newCode);
 315                 return newCode;
 316         }
 317
 318         public static ArrayList<String> generatePotentialCPDefine(
 319                         SemanticsChecker semantics, PotentialCPDefineConstruct construct) {
 320                 ArrayList<String> newCode = new ArrayList<String>();
 321
 322                 // Generate redundant header files
 323                 newCode.add(COMMENT("Automatically generated code for potential commit point: "
 324                                 + construct.label));
 325                 newCode.add(COMMENT("Include redundant headers"));
 326                 newCode.add(INCLUDE(HEADER_THREADS));
 327                 newCode.add(INCLUDE(HEADER_CDSTRACE));
 328                 newCode.add("");
 329                 // Some necessary function calls
 330
 331                 return newCode;
 332         }
 333 }