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