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 ThreadIDType = "thread_id_t";
  10         public static final String BOOLEAN = "bool";
  11
  12         // Model checker code
  13         public static final String HEADER_CDSAnnotate = "cdsannotate.h";
  14         public static final String CDSAnnotate = "cdsannotate";
  15         public static final String CDSAnnotateType = "SPEC_ANALYSIS";
  16
  17         public static final String SPEC_ANNOTATION_TYPE = "spec_anno_type";
  18         public static final String SPEC_ANNOTATION = "spec_annotation";
  19
  20         public static final String ANNO_HB_INIT = "anno_hb_init";
  21         public static final String ANNO_INTERFACE_BEGIN = "anno_interface_begin";
  22         public static final String ANNO_INTERFACE_END = "anno_interface_end";
  23         public static final String ANNO_ID = "anno_id";
  24         public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potentail_cp_define";
  25         public static final String ANNO_CP_DEFINE = "anno_cp_define";
  26         public static final String ANNO_CP_DEFINE_CHECK = "anno_cp_define_check";
  27         public static final String ANNO_HB_CONDITION = "anno_hb_condition";
  28         public static final String ANNO_POST_CHECK = "anno_post_check";
  29
  30         // Specification variables
  31         public static final String SPEC_STRUCT = "Sequential";
  32         public static final String SPEC_INSTANCE = "__sequential";
  33
  34         public static final String SPEC_CONDITION = "__cond";
  35         public static final String SPEC_ID = "__id";
  36         public static final String SPEC_INTERFACE = "__interface";
  37
  38         public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_";
  39
  40         // Specification library
  41         public static final String SPEC_QUEUE = "spec_queue";
  42         public static final String SPEC_STACK = "spec_stack";
  43         public static final String SPEC_HASHTABLE = "spec_hashtable";
  44         public static final String SPEC_TAG = "spec_tag";
  45
  46         // Macro
  47         public static final String MACRO_ID = "__ID__";
  48         public static final String MACRO_COND = "__COND_SAT__";
  49         public static final String MACRO_RETURN = "__RET__";
  50
  51         public static ArrayList<String> generateHBInitAnnotation(
  52                         SemanticsChecker semantics) {
  53                 ArrayList<String> newCode = new ArrayList<String>();
  54                 int hbConditionInitIdx = 0;
  55                 for (ConditionalInterface left : semantics.getHBConditions().keySet()) {
  56                         for (ConditionalInterface right : semantics.getHBConditions().get(
  57                                         left)) {
  58                                 String structVarName = "hbConditionInit" + hbConditionInitIdx;
  59                                 hbConditionInitIdx++;
  60                                 int interfaceNumBefore = semantics.interface2Num
  61                                                 .get(left.interfaceName), hbLabelNumBefore = semantics.hbLabel2Num
  62                                                 .get(left.hbConditionLabel), interfaceNumAfter = semantics.interface2Num
  63                                                 .get(right.interfaceName), hbLabelNumAfter = semantics.hbLabel2Num
  64                                                 .get(right.hbConditionLabel);
  65                                 newCode.add(ANNO_HB_INIT + " " + structVarName + ";");
  66
  67                                 newCode.add(structVarName + "." + "interface_num_before"
  68                                                 + " = " + interfaceNumBefore + ";");
  69                                 newCode.add(structVarName + "." + "hb_condition_num_before"
  70                                                 + " = " + hbLabelNumBefore + ";");
  71                                 newCode.add(structVarName + "." + "interface_num_after" + " = "
  72                                                 + interfaceNumAfter + ";");
  73                                 newCode.add(structVarName + "." + "hb_condition_num_after"
  74                                                 + " = " + hbLabelNumAfter + ";");
  75
  76                                 newCode.add(CDSAnnotate + "(" + CDSAnnotateType + ", &" + structVarName + ");");
  77                         }
  78                 }
  79                 return newCode;
  80         }
  81 }