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.InterfaceConstruct;
   8 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
   9 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
  10 import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
  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         public static final String GET_PREV_ATOMIC_VAL = "get_prev_value";
  28
  29         public static final String SPEC_ANNO_TYPE = "spec_anno_type";
  30         public static final String SPEC_ANNO_TYPE_HB_INIT = "HB_INIT";
  31         public static final String SPEC_ANNO_TYPE_INTERFACE_BEGIN = "INTERFACE_BEGIN";
  32         public static final String SPEC_ANNO_TYPE_POST_CHECK = "POST_CHECK";
  33         public static final String SPEC_ANNO_TYPE_HB_CONDITION = "HB_CONDITION";
  34         public static final String SPEC_ANNO_TYPE_INTERFACE_END = "INTERFACE_END";
  35         public static final String SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE = "POTENTIAL_CP_DEFINE";
  36         public static final String SPEC_ANNOTATION = "spec_annotation";
  37         public static final String SPEC_ANNOTATION_FIELD_TYPE = "type";
  38         public static final String SPEC_ANNOTATION_FIELD_ANNO = "annotation";
  39
  40         public static final String ANNO_HB_INIT = "anno_hb_init";
  41         public static final String ANNO_INTERFACE_BOUNDARY = "anno_interface_boundary";
  42         public static final String ANNO_ID = "anno_id";
  43         public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potentail_cp_define";
  44         public static final String ANNO_CP_DEFINE = "anno_cp_define";
  45         public static final String ANNO_CP_DEFINE_CHECK = "anno_cp_define_check";
  46         public static final String ANNO_HB_CONDITION = "anno_hb_condition";
  47         public static final String ANNO_POST_CHECK = "anno_post_check";
  48
  49         // Specification variables
  50         public static final String HEADER_SPEC_SEQUENTIAL = "_spec_sequential.h";
  51         public static final String SPEC_SEQUENTIAL_HEADER_MACRO = HEADER_SPEC_SEQUENTIAL
  52                         .replace('.', '_').toUpperCase();
  53         public static final String SPEC_SEQUENTIAL_STRUCT = "Sequential";
  54         public static final String SPEC_SEQUENTIAL_INSTANCE = "__sequential";
  55
  56         public static final String SPEC_CONDITION = "condition";
  57         public static final String SPEC_ID = "id";
  58         public static final String SPEC_INTERFACE = "interface";
  59         public static final String SPEC_INTERFACE_CALL_SEQUENCE = "interface_call_sequence";
  60         public static final String SPEC_GLOBAL_CALL_SEQUENCE = "global_call_sequence";
  61
  62         public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_";
  63
  64         public static final String VAR_ThreadID = "tid";
  65         public static final String VAR_CALL_SEQUENCE_NUM = "call_sequence_num";
  66
  67         // Specification library
  68         public static final String SPEC_QUEUE = "spec_queue";
  69         public static final String SPEC_STACK = "spec_stack";
  70         public static final String SPEC_DEQUE = "spec_deque";
  71         public static final String SPEC_HASHTABLE = "spec_hashtable";
  72         public static final String HEADER_SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable.h";
  73         public static final String SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable";
  74         public static final String HEADER_SPEC_TAG = "spec_tag.h";
  75         public static final String SPEC_TAG = "spec_tag";
  76         public static final String SPEC_TAG_CURRENT = "current";
  77         public static final String SPEC_TAG_NEXT = "next";
  78
  79         // Macro
  80         public static final String MACRO_ID = "__ID__";
  81         public static final String MACRO_COND = "__COND_SAT__";
  82         public static final String MACRO_RETURN = "__RET__";
  83         public static final String MACRO_ATOMIC_RETURN = "__ATOMIC_RET__";
  84
  85         // Break the code (String) into multiple lines and add it to newCode
  86         private static void breakCodeLines(ArrayList<String> newCode, String code) {
  87                 int begin = 0, end = 0;
  88                 while (end < code.length()) {
  89                         if (code.charAt(end) == '\n') {
  90                                 String line = code.substring(begin, end);
  91                                 newCode.add(line);
  92                                 begin = end + 1;
  93                         }
  94                         end++;
  95                 }
  96         }
  97
  98         public static void printCode(ArrayList<String> code) {
  99                 for (int i = 0; i < code.size(); i++) {
 100                         System.out.println(code.get(i));
 101                 }
 102         }
 103
 104         public static String getFuncName(String funcDecl) {
 105                 int beginIdx = funcDecl.indexOf('(');
 106                 IDExtractor idExtractor = new IDExtractor(funcDecl, beginIdx);
 107                 return idExtractor.getPrevID();
 108         }
 109
 110         public static String getFuncReturnType(String funcDecl) {
 111                 int beginIdx = funcDecl.indexOf('(');
 112                 IDExtractor idExtractor = new IDExtractor(funcDecl, beginIdx);
 113                 idExtractor.getPrevID();
 114                 int idLineBegin = idExtractor.lineBeginIdxOfID(), idBegin = idExtractor
 115                                 .getIDBeginIdx();
 116                 String type = funcDecl.substring(idLineBegin, idBegin);
 117                 return SpecExtractor.trimSpace(type);
 118         }
 119
 120         public static ArrayList<String> getFuncArgs(String funcDecl) {
 121                 ArrayList<String> args = new ArrayList<String>();
 122                 int beginIdx = funcDecl.indexOf('('), endIdx = funcDecl.indexOf(')');
 123                 IDExtractor idExtractor = new IDExtractor(funcDecl, endIdx);
 124                 String arg = idExtractor.getPrevID();
 125                 // Void argument
 126                 if (arg == null || idExtractor.getIDBeginIdx() < beginIdx) {
 127                         return args;
 128                 } else {
 129                         args.add(arg);
 130                 }
 131
 132                 do {
 133                         endIdx = funcDecl.lastIndexOf(',', endIdx);
 134                         if (endIdx == -1) {
 135                                 return args;
 136                         }
 137                         idExtractor.reset(endIdx);
 138                         args.add(idExtractor.getPrevID());
 139                 } while (true);
 140         }
 141
 142         private static String COMMENT(String comment) {
 143                 return "/* " + comment + " */";
 144         }
 145
 146         private static String GET(String var) {
 147                 return "get(&" + VAR(var) + ", " + VAR_ThreadID + ")";
 148         }
 149
 150         private static String PUT(String var, String tid, String val) {
 151                 return "put(&" + VAR(var) + ", " + tid + ", " + val + ");";
 152         }
 153
 154         private static String INIT(String var) {
 155                 return "init(&" + VAR(var) + ");";
 156         }
 157
 158         private static String INCLUDE(String header) {
 159                 return "#include <" + header + ">";
 160         }
 161
 162         private static String DEFINE(String left, String right) {
 163                 return "#define " + left + " " + right;
 164         }
 165
 166         private static String UNDEFINE(String macro) {
 167                 return "#undef " + macro;
 168         }
 169
 170         private static String VAR(String var) {
 171                 return SPEC_SEQUENTIAL_INSTANCE + "." + var;
 172         }
 173
 174         private static String BRACE(String val) {
 175                 return "(" + val + ")";
 176         }
 177
 178         private static String VAR_PTR(String var) {
 179                 return "&" + SPEC_SEQUENTIAL_INSTANCE + "." + var;
 180         }
 181
 182         private static String ASSIGN(String structName, String field, String val) {
 183                 return structName + "." + field + " = " + val + ";";
 184         }
 185
 186         private static String ASSIGN_PTR(String structName, String field, String val) {
 187                 return structName + "." + field + " = &" + val + ";";
 188         }
 189
 190         private static String DECLARE(String structType, String structName) {
 191                 return structType + " " + structName + ";";
 192         }
 193
 194         private static String DECLARE_DEFINE(String type, String var, String val) {
 195                 return type + " " + var + " = " + val + ";";
 196         }
 197
 198         private static String ANNOTATE(String structName) {
 199                 return CDSAnnotate + "(" + CDSAnnotateType + ", &" + structName + ");";
 200         }
 201
 202         public static ArrayList<String> generateGlobalVarDeclaration(
 203                         SemanticsChecker semantics, GlobalConstruct construct) {
 204                 ArrayList<String> newCode = new ArrayList<String>();
 205
 206                 // Header conflicting avoidance macro & headers
 207                 newCode.add("/** @file " + HEADER_SPEC_SEQUENTIAL);
 208                 newCode.add(" *  @brief Automatically generated header file for sequential variables");
 209                 newCode.add(" */");
 210                 newCode.add("#ifndef " + SPEC_SEQUENTIAL_HEADER_MACRO);
 211                 newCode.add("#define " + SPEC_SEQUENTIAL_HEADER_MACRO);
 212                 newCode.add("");
 213                 newCode.add(INCLUDE(HEADER_SPEC_PRIVATE_HASHTABLE));
 214                 newCode.add(INCLUDE(HEADER_SPECANNOTATION));
 215                 newCode.add(INCLUDE(HEADER_SPEC_TAG));
 216                 newCode.add("");
 217
 218                 // Generate all sequential variables into a struct
 219                 newCode.add(COMMENT("Beginning of struct " + SPEC_SEQUENTIAL_STRUCT));
 220                 newCode.add("typedef struct " + SPEC_SEQUENTIAL_STRUCT + " {");
 221                 newCode.add(COMMENT("Condition"));
 222                 newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE, SPEC_CONDITION));
 223                 newCode.add(COMMENT("ID"));
 224                 newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE, SPEC_ID));
 225                 newCode.add(COMMENT("Current interface call"));
 226                 newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE, SPEC_INTERFACE));
 227                 newCode.add(COMMENT("Current interface call sequence"));
 228                 newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE,
 229                                 SPEC_INTERFACE_CALL_SEQUENCE));
 230                 newCode.add(COMMENT("Global interface call sequence number"));
 231                 newCode.add(DECLARE(SPEC_TAG, SPEC_GLOBAL_CALL_SEQUENCE));
 232                 newCode.add("");
 233                 // DefineVar declaration
 234                 for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
 235                         InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct
 236                                         .get(interfaceName);
 237                         ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
 238                         if (defineVars.size() > 0) {
 239                                 newCode.add(COMMENT("DefineVar in " + interfaceName));
 240                                 for (int i = 0; i < defineVars.size(); i++) {
 241                                         DefineVar var = defineVars.get(i);
 242                                         newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE,
 243                                                         var.getNewVarName()));
 244                                 }
 245                         }
 246                         newCode.add("");
 247                 }
 248                 // Generate user-defined variable declaration
 249                 newCode.add(COMMENT("Beginnint of other user-defined variables"));
 250                 SequentialDefineSubConstruct globalCode = construct.code;
 251                 breakCodeLines(newCode, globalCode.declareVar);
 252                 newCode.add(COMMENT("End of other user-defined variables"));
 253                 // End of struct Sequential
 254                 newCode.add("} " + SPEC_SEQUENTIAL_STRUCT + "; "
 255                                 + COMMENT("End of struct " + SPEC_SEQUENTIAL_STRUCT));
 256
 257                 // Generate definition of the sequential struct
 258                 newCode.add("");
 259                 newCode.add(COMMENT("Instance of the struct"));
 260                 newCode.add(DECLARE(SPEC_SEQUENTIAL_STRUCT, SPEC_SEQUENTIAL_INSTANCE));
 261
 262                 newCode.add("");
 263                 newCode.add(COMMENT("Define function for sequential code initialization"));
 264                 newCode.add("void " + SPEC_SEQUENTIAL_INSTANCE + "_init() {");
 265                 // Internal variables
 266                 newCode.add(COMMENT("Init internal variables"));
 267                 newCode.add(INIT(SPEC_CONDITION));
 268                 newCode.add(INIT(SPEC_ID));
 269                 newCode.add(INIT(SPEC_INTERFACE));
 270                 newCode.add(INIT(SPEC_INTERFACE_CALL_SEQUENCE));
 271                 newCode.add(INIT(SPEC_GLOBAL_CALL_SEQUENCE));
 272                 // Init DefineVars
 273                 newCode.add(COMMENT("Init DefineVars"));
 274                 for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
 275                         InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct
 276                                         .get(interfaceName);
 277                         ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
 278                         if (defineVars.size() > 0) {
 279                                 newCode.add(COMMENT("DefineVar in " + interfaceName));
 280                                 for (int i = 0; i < defineVars.size(); i++) {
 281                                         DefineVar var = defineVars.get(i);
 282                                         newCode.add(INIT(var.getNewVarName()));
 283                                 }
 284                         }
 285                 }
 286                 // Init user-defined variables
 287                 newCode.add(COMMENT("Init user-defined variables"));
 288                 breakCodeLines(newCode, globalCode.initVar);
 289                 // Pass the HB initialization
 290                 newCode.add(COMMENT("Pass the happens-before initialization here"));
 291                 newCode.addAll(CodeVariables.generateHBInitAnnotation(semantics));
 292                 // End of init the function
 293                 newCode.add("} " + COMMENT("End of init function"));
 294
 295                 // Generate the user-defined sequential functions
 296                 newCode.add("");
 297                 newCode.add(COMMENT("All other user-defined functions"));
 298                 breakCodeLines(newCode, globalCode.defineFunc);
 299
 300                 // The end
 301                 newCode.add("");
 302                 newCode.add("#endif " + SPEC_SEQUENTIAL_HEADER_MACRO + "\t"
 303                                 + COMMENT("End of " + HEADER_SPEC_SEQUENTIAL));
 304
 305                 // printCode(newCode);
 306                 return newCode;
 307         }
 308
 309         private static ArrayList<String> generateHBInitAnnotation(
 310                         SemanticsChecker semantics) {
 311                 ArrayList<String> newCode = new ArrayList<String>();
 312                 int hbConditionInitIdx = 0;
 313                 for (ConditionalInterface left : semantics.getHBConditions().keySet()) {
 314                         for (ConditionalInterface right : semantics.getHBConditions().get(
 315                                         left)) {
 316                                 String structVarName = "hbConditionInit" + hbConditionInitIdx;
 317                                 String annotationVarName = "hb_init" + hbConditionInitIdx;
 318                                 hbConditionInitIdx++;
 319                                 String interfaceNumBefore = Integer
 320                                                 .toString(semantics.interface2Num
 321                                                                 .get(left.interfaceName)), hbLabelNumBefore = Integer
 322                                                 .toString(semantics.hbLabel2Num
 323                                                                 .get(left.hbConditionLabel)), interfaceNumAfter = Integer
 324                                                 .toString(semantics.interface2Num
 325                                                                 .get(right.interfaceName)), hbLabelNumAfter = Integer
 326                                                 .toString(semantics.hbLabel2Num
 327                                                                 .get(right.hbConditionLabel));
 328                                 newCode.add(COMMENT(left + " -> " + right));
 329
 330                                 newCode.add(ANNO_HB_INIT + " " + structVarName + ";");
 331                                 newCode.add(ASSIGN(structVarName, "interface_num_before",
 332                                                 interfaceNumBefore));
 333                                 newCode.add(ASSIGN(structVarName, "hb_condition_num_before",
 334                                                 hbLabelNumBefore));
 335                                 newCode.add(ASSIGN(structVarName, "interface_num_after",
 336                                                 interfaceNumAfter));
 337                                 newCode.add(ASSIGN(structVarName, "hb_condition_num_after",
 338                                                 hbLabelNumAfter));
 339
 340                                 newCode.add(DECLARE(SPEC_ANNOTATION, annotationVarName));
 341                                 newCode.add(ASSIGN(annotationVarName,
 342                                                 SPEC_ANNOTATION_FIELD_TYPE, SPEC_ANNO_TYPE_HB_INIT));
 343                                 newCode.add(ASSIGN_PTR(annotationVarName,
 344                                                 SPEC_ANNOTATION_FIELD_ANNO, structVarName));
 345                                 newCode.add(ANNOTATE(annotationVarName));
 346                         }
 347                 }
 348                 return newCode;
 349         }
 350
 351         public static ArrayList<String> generateInterfaceWrapper(
 352                         SemanticsChecker semantics, InterfaceConstruct construct) {
 353                 ArrayList<String> newCode = new ArrayList<String>();
 354                 String funcDecl = construct.interfaceDeclBody.substring(0,
 355                                 construct.interfaceDeclBody.indexOf(')') + 1);
 356                 String returnType = getFuncReturnType(funcDecl), funcName = getFuncName(funcDecl), renamedFuncName = SPEC_INTERFACE_WRAPPER
 357                                 + funcName;
 358                 ArrayList<String> args = getFuncArgs(funcDecl);
 359
 360                 // Generate necessary header file (might be redundant but never mind)
 361                 newCode.add(COMMENT("Automatically generated code for interface: "
 362                                 + construct.name));
 363                 newCode.add(COMMENT("Include redundant headers"));
 364                 newCode.add(INCLUDE(HEADER_THREADS));
 365                 newCode.add(INCLUDE(HEADER_CDSANNOTATE));
 366                 newCode.add(INCLUDE(HEADER_SPECANNOTATION));
 367                 newCode.add(INCLUDE(HEADER_SPEC_TAG));
 368                 newCode.add(INCLUDE(HEADER_SPEC_PRIVATE_HASHTABLE));
 369                 newCode.add("");
 370
 371                 // Generate wrapper header
 372                 newCode.add(COMMENT("Wrapper for " + SPEC_INTERFACE_WRAPPER + funcName));
 373                 breakCodeLines(newCode, funcDecl);
 374                 newCode.add("{");
 375
 376                 // Wrapper function body
 377                 newCode.add(DECLARE_DEFINE(ThreadIDType, VAR_ThreadID, GET_THREAD_ID
 378                                 + BRACE("")));
 379                 newCode.add(DECLARE_DEFINE(UINT64, VAR_CALL_SEQUENCE_NUM,
 380                                 SPEC_TAG_CURRENT + BRACE(VAR_PTR(SPEC_GLOBAL_CALL_SEQUENCE))));
 381                 newCode.add(SPEC_TAG_NEXT + BRACE(VAR_PTR(SPEC_GLOBAL_CALL_SEQUENCE)));
 382                 newCode.add(PUT(SPEC_INTERFACE_CALL_SEQUENCE, VAR_ThreadID,
 383                                 VAR_CALL_SEQUENCE_NUM));
 384                 // Interface begin
 385                 newCode.add("");
 386                 newCode.add(COMMENT("Interface begin"));
 387                 String interfaceName = construct.name;
 388                 String annoStruct = "interface_boundary", interfaceNum = Integer
 389                                 .toString(semantics.interface2Num.get(interfaceName));
 390                 newCode.add(DECLARE(ANNO_INTERFACE_BOUNDARY, annoStruct));
 391                 newCode.add(ASSIGN(annoStruct, "interface_num", interfaceNum));
 392                 newCode.add(ASSIGN(annoStruct, "call_sequence_num",
 393                                 VAR_CALL_SEQUENCE_NUM));
 394                 String anno = "annotation_interface_begin";
 395                 newCode.add(DECLARE(SPEC_ANNOTATION, anno));
 396                 newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
 397                                 SPEC_ANNO_TYPE_INTERFACE_BEGIN));
 398                 newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
 399                 newCode.add(ANNOTATE(anno));
 400                 // Call original renamed function
 401                 String funcCall = renamedFuncName + "(";
 402                 if (args.size() == 0) {
 403                         funcCall = funcCall + ")";
 404                 } else {
 405                         funcCall = funcCall + args.get(0);
 406                         for (int i = 1; i < args.size(); i++) {
 407                                 funcCall = funcCall + ", " + args.get(i);
 408                         }
 409                         funcCall = funcCall + ")";
 410                 }
 411                 newCode.add(DECLARE_DEFINE(returnType, MACRO_RETURN, funcCall));
 412                 newCode.add(DECLARE_DEFINE("int", MACRO_COND, GET(SPEC_CONDITION)));
 413                 newCode.add(DECLARE_DEFINE(UINT64, MACRO_ID, GET(SPEC_ID)));
 414                 // Post check & action
 415                 newCode.add("");
 416                 newCode.add(COMMENT("Post_check action, define macros for all DefineVars"));
 417                 // Define all DefineVar macro
 418                 ArrayList<DefineVar> defineVars = construct.action.defineVars;
 419                 for (int i = 0; i < defineVars.size(); i++) {
 420                         DefineVar var = defineVars.get(i);
 421                         newCode.add(DEFINE(var.varName, BRACE(GET(interfaceName + "_"
 422                                         + var.varName))));
 423                 }
 424                 // Post check
 425                 newCode.add(DECLARE_DEFINE("bool", "post_check_passed",
 426                                 construct.postCheck));
 427                 annoStruct = "post_check";
 428                 newCode.add(DECLARE(ANNO_POST_CHECK, annoStruct));
 429                 newCode.add(ASSIGN(annoStruct, "check_passed", "post_check_passed"));
 430                 newCode.add(ASSIGN(annoStruct, "interface_num", interfaceNum));
 431                 newCode.add(ASSIGN(annoStruct, "call_sequence_num",
 432                                 VAR_CALL_SEQUENCE_NUM));
 433                 anno = "annotation_post_check";
 434                 newCode.add(DECLARE(SPEC_ANNOTATION, anno));
 435                 newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
 436                                 SPEC_ANNO_TYPE_POST_CHECK));
 437                 newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
 438                 newCode.add(ANNOTATE(anno));
 439                 // Post action if any
 440                 breakCodeLines(newCode, construct.postAction);
 441                 // Undefine all DefineVar macro
 442                 for (int i = 0; i < defineVars.size(); i++) {
 443                         DefineVar var = defineVars.get(i);
 444                         newCode.add(UNDEFINE(var.varName));
 445                 }
 446                 // HB conditions
 447                 newCode.add("");
 448                 for (String label : construct.hbConditions.keySet()) {
 449                         String hbCondition = construct.hbConditions.get(label);
 450                         newCode.add(COMMENT("Happens-before condition for " + label
 451                                         + " ::= " + hbCondition));
 452                         newCode.add("if " + BRACE(hbCondition) + " {");
 453                         String hbNum = Integer.toString(semantics.hbLabel2Num.get(label));
 454                         annoStruct = "hb_condition" + hbNum;
 455                         newCode.add(DECLARE(ANNO_HB_CONDITION, annoStruct));
 456                         newCode.add(ASSIGN(annoStruct, "interface_num", interfaceNum));
 457                         newCode.add(ASSIGN(annoStruct, "hb_condition_num", hbNum));
 458                         newCode.add(ASSIGN(annoStruct, "id", MACRO_ID));
 459                         newCode.add(ASSIGN(annoStruct, "call_sequence_num",
 460                                         VAR_CALL_SEQUENCE_NUM));
 461                         anno = "annotation_hb_condition";
 462                         newCode.add(DECLARE(SPEC_ANNOTATION, anno));
 463                         newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
 464                                         SPEC_ANNO_TYPE_HB_CONDITION));
 465                         newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
 466                         ANNOTATE(anno);
 467                         newCode.add("} " + COMMENT("End of HB condition " + label));
 468                         newCode.add("");
 469                 }
 470                 // Interface end
 471                 annoStruct = "interface_boundary";
 472                 anno = "annotation_interface_end";
 473                 newCode.add(DECLARE(SPEC_ANNOTATION, anno));
 474                 newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
 475                                 SPEC_ANNO_TYPE_INTERFACE_END));
 476                 newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
 477                 newCode.add(ANNOTATE(anno));
 478
 479                 // End of the wrapper function
 480                 newCode.add("} "
 481                                 + COMMENT("End of automatically generated code for interface wrapper"));
 482
 483                 printCode(newCode);
 484                 return newCode;
 485         }
 486
 487         public static ArrayList<String> generatePotentialCPDefine(
 488                         SemanticsChecker semantics, PotentialCPDefineConstruct construct) {
 489                 ArrayList<String> newCode = new ArrayList<String>();
 490
 491                 // Generate redundant header files
 492                 newCode.add(COMMENT("Automatically generated code for potential commit point: "
 493                                 + construct.label));
 494                 newCode.add(COMMENT("Include redundant headers"));
 495                 newCode.add(INCLUDE(HEADER_THREADS));
 496                 newCode.add(INCLUDE(HEADER_CDSTRACE));
 497                 newCode.add(INCLUDE(HEADER_SPEC_PRIVATE_HASHTABLE));
 498                 newCode.add(INCLUDE(HEADER_SPEC_SEQUENTIAL));
 499                 newCode.add("");
 500                 // Some necessary function calls
 501                 newCode.add(DECLARE_DEFINE(ThreadIDType, VAR_ThreadID, GET_THREAD_ID
 502                                 + BRACE("")));
 503                 newCode.add(DECLARE_DEFINE(UINT64, MACRO_ATOMIC_RETURN,
 504                                 GET_PREV_ATOMIC_VAL + BRACE(VAR_ThreadID)));
 505                 newCode.add("if " + BRACE(construct.condition) + " {");
 506                 newCode.add(DECLARE_DEFINE(UINT64, VAR_CALL_SEQUENCE_NUM,
 507                                 GET(SPEC_INTERFACE_CALL_SEQUENCE)));
 508                 String annoStruct = "potential_cp_define";
 509                 newCode.add(DECLARE(ANNO_POTENTIAL_CP_DEFINE, annoStruct));
 510                 newCode.add(ASSIGN(annoStruct, "interface_num", GET(SPEC_INTERFACE)));
 511                 String labelNum = Integer.toString(semantics.commitPointLabel2Num
 512                                 .get(construct.label));
 513                 newCode.add(ASSIGN(annoStruct, "label_num", labelNum));
 514                 newCode.add(ASSIGN(annoStruct, "call_sequence_num",
 515                                 VAR_CALL_SEQUENCE_NUM));
 516                 String anno = "annotation_potential_cp_define";
 517                 newCode.add(DECLARE(SPEC_ANNOTATION, anno));
 518                 newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
 519                                 SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE));
 520                 newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
 521                 ANNOTATE(anno);
 522
 523                 newCode.add("} "
 524                                 + COMMENT("End of automatically generated code for potential commit point"));
 525
 526                 return newCode;
 527         }
 528 }