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
   7 public class CodeVariables {
   8         // C++ code or library
   9         public static final String HEADER_threads = "threads.h";
  10         public static final String ThreadIDType = "thrd_t";
  11         public static final String GET_THREAD_ID = "thrd_current";
  12         public static final String BOOLEAN = "bool";
  13         public static final String UINT64 = "uint64_t";
  14
  15         // Model checker code
  16         public static final String HEADER_CDSAnnotate = "cdsannotate.h";
  17         public static final String HEADER_SPECANNOTATION = "specannotation.h";
  18         public static final String CDSAnnotate = "cdsannotate";
  19         public static final String CDSAnnotateType = "SPEC_ANALYSIS";
  20         // It's a SPEC_TAG type, it has current() and next() function
  21         public static final String INTERFACE_CALL_SEQUENCE = "__interface_call_sequence";
  22
  23         public static final String SPEC_ANNOTATION_TYPE = "spec_anno_type";
  24         public static final String SPEC_ANNOTATION = "spec_annotation";
  25
  26         public static final String ANNO_HB_INIT = "anno_hb_init";
  27         public static final String ANNO_INTERFACE_BOUNDARY = "anno_interface_boundary";
  28         public static final String ANNO_ID = "anno_id";
  29         public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potentail_cp_define";
  30         public static final String ANNO_CP_DEFINE = "anno_cp_define";
  31         public static final String ANNO_CP_DEFINE_CHECK = "anno_cp_define_check";
  32         public static final String ANNO_HB_CONDITION = "anno_hb_condition";
  33         public static final String ANNO_POST_CHECK = "anno_post_check";
  34
  35         // Specification variables
  36         public static final String SPEC_STRUCT = "Sequential";
  37         public static final String SPEC_INSTANCE = "__sequential";
  38
  39         public static final String SPEC_CONDITION = "condition";
  40         public static final String SPEC_ID = "id";
  41         public static final String SPEC_INTERFACE = "interface";
  42         public static final String SPEC_INTERFACE_CALL_SEQUENCE = "interface_call_sequence";
  43
  44         public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_";
  45
  46         // Specification library
  47         public static final String SPEC_QUEUE = "spec_queue";
  48         public static final String SPEC_STACK = "spec_stack";
  49         public static final String SPEC_HASHTABLE = "spec_hashtable";
  50         public static final String SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable";
  51         public static final String SPEC_TAG = "spec_tag";
  52
  53         // Macro
  54         public static final String MACRO_ID = "__ID__";
  55         public static final String MACRO_COND = "__COND_SAT__";
  56         public static final String MACRO_RETURN = "__RET__";
  57
  58         public static ArrayList<String> generateHBInitAnnotation(
  59                         SemanticsChecker semantics) {
  60                 ArrayList<String> newCode = new ArrayList<String>();
  61                 int hbConditionInitIdx = 0;
  62                 for (ConditionalInterface left : semantics.getHBConditions().keySet()) {
  63                         for (ConditionalInterface right : semantics.getHBConditions().get(
  64                                         left)) {
  65                                 String structVarName = "hbConditionInit" + hbConditionInitIdx;
  66                                 hbConditionInitIdx++;
  67                                 int interfaceNumBefore = semantics.interface2Num
  68                                                 .get(left.interfaceName), hbLabelNumBefore = semantics.hbLabel2Num
  69                                                 .get(left.hbConditionLabel), interfaceNumAfter = semantics.interface2Num
  70                                                 .get(right.interfaceName), hbLabelNumAfter = semantics.hbLabel2Num
  71                                                 .get(right.hbConditionLabel);
  72                                 newCode.add(ANNO_HB_INIT + " " + structVarName + ";");
  73
  74                                 newCode.add(structVarName + "." + "interface_num_before"
  75                                                 + " = " + interfaceNumBefore + ";");
  76                                 newCode.add(structVarName + "." + "hb_condition_num_before"
  77                                                 + " = " + hbLabelNumBefore + ";");
  78                                 newCode.add(structVarName + "." + "interface_num_after" + " = "
  79                                                 + interfaceNumAfter + ";");
  80                                 newCode.add(structVarName + "." + "hb_condition_num_after"
  81                                                 + " = " + hbLabelNumAfter + ";");
  82
  83                                 newCode.add(CDSAnnotate + "(" + CDSAnnotateType + ", &" + structVarName + ");");
  84                         }
  85                 }
  86                 return newCode;
  87         }
  88 }