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.SequentialDefineSubConstruct;
   9 import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
  10
  11 public class CodeVariables {
  12         // C++ code or library
  13         public static final String HEADER_threads = "threads.h";
  14         public static final String ThreadIDType = "thrd_t";
  15         public static final String GET_THREAD_ID = "thrd_current";
  16         public static final String BOOLEAN = "bool";
  17         public static final String UINT64 = "uint64_t";
  18
  19         // Model checker code
  20         public static final String HEADER_CDSAnnotate = "cdsannotate.h";
  21         public static final String HEADER_SPECANNOTATION = "specannotation.h";
  22         public static final String CDSAnnotate = "cdsannotate";
  23         public static final String CDSAnnotateType = "SPEC_ANALYSIS";
  24         // It's a SPEC_TAG type, it has current() and next() function
  25         public static final String INTERFACE_CALL_SEQUENCE = "__interface_call_sequence";
  26
  27         public static final String SPEC_ANNOTATION_TYPE = "spec_anno_type";
  28         public static final String SPEC_ANNOTATION = "spec_annotation";
  29
  30         public static final String ANNO_HB_INIT = "anno_hb_init";
  31         public static final String ANNO_INTERFACE_BOUNDARY = "anno_interface_boundary";
  32         public static final String ANNO_ID = "anno_id";
  33         public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potentail_cp_define";
  34         public static final String ANNO_CP_DEFINE = "anno_cp_define";
  35         public static final String ANNO_CP_DEFINE_CHECK = "anno_cp_define_check";
  36         public static final String ANNO_HB_CONDITION = "anno_hb_condition";
  37         public static final String ANNO_POST_CHECK = "anno_post_check";
  38
  39         // Specification variables
  40         public static final String SPEC_SEQUENTIAL_HEADER = "_spec_sequential.h";
  41         public static final String SPEC_SEQUENTIAL_HEADER_MACRO = SPEC_SEQUENTIAL_HEADER
  42                         .replace('.', '_').toUpperCase();
  43         public static final String SPEC_SEQUENTIAL_STRUCT = "Sequential";
  44         public static final String SPEC_SEQUENTIAL_INSTANCE = "__sequential";
  45
  46         public static final String SPEC_CONDITION = "condition";
  47         public static final String SPEC_ID = "id";
  48         public static final String SPEC_INTERFACE = "interface";
  49         public static final String SPEC_INTERFACE_CALL_SEQUENCE = "interface_call_sequence";
  50
  51         public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_";
  52
  53         // Specification library
  54         public static final String SPEC_QUEUE = "spec_queue";
  55         public static final String SPEC_STACK = "spec_stack";
  56         public static final String SPEC_HASHTABLE = "spec_hashtable";
  57         public static final String SPEC_PRIVATE_HASHTABLE_HEADER = "spec_private_hashtable.h";
  58         public static final String SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable";
  59         public static final String SPEC_TAG = "spec_tag";
  60
  61         // Macro
  62         public static final String MACRO_ID = "__ID__";
  63         public static final String MACRO_COND = "__COND_SAT__";
  64         public static final String MACRO_RETURN = "__RET__";
  65
  66         // Break the code (String) into multiple lines and add it to newCode
  67         private static void breakCodeLines(ArrayList<String> newCode, String code) {
  68                 int begin = 0, end = 0;
  69                 while (end < code.length()) {
  70                         if (code.charAt(end) == '\n') {
  71                                 String line = code.substring(begin, end);
  72                                 newCode.add(line);
  73                                 begin = end + 1;
  74                         }
  75                         end++;
  76                 }
  77         }
  78
  79         private static void printCode(ArrayList<String> code) {
  80                 for (int i = 0; i < code.size(); i++) {
  81                         System.out.println(code.get(i));
  82                 }
  83         }
  84
  85         public static ArrayList<String> generateGlobalVarDeclaration(
  86                         SemanticsChecker semantics, GlobalConstruct construct) {
  87                 ArrayList<String> newCode = new ArrayList<String>();
  88
  89                 // Header conflicting avoidance macro & headers
  90                 newCode.add("/** @file " + SPEC_SEQUENTIAL_HEADER);
  91                 newCode.add(" *  @brief Automatically generated header file for sequential variables");
  92                 newCode.add(" */");
  93                 newCode.add("#ifndef " + SPEC_SEQUENTIAL_HEADER_MACRO);
  94                 newCode.add("#define " + SPEC_SEQUENTIAL_HEADER_MACRO);
  95                 newCode.add("#include " + "<" + SPEC_PRIVATE_HASHTABLE_HEADER + ">");
  96                 newCode.add("#include " + "<" + HEADER_SPECANNOTATION + ">");
  97
  98                 // Generate all sequential variables into a struct
  99                 newCode.add("/* Beginning of struct " + SPEC_SEQUENTIAL_STRUCT + " */");
 100                 newCode.add("typedef struct " + SPEC_SEQUENTIAL_STRUCT + " {");
 101                 newCode.add("/* Condition of interface */");
 102                 newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_CONDITION + ";");
 103                 newCode.add("/* ID of interface */");
 104                 newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_ID + ";");
 105                 newCode.add("/* Current interface call */");
 106                 newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_INTERFACE + ";");
 107                 newCode.add("/* Current interface call sequence */");
 108                 newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_INTERFACE_CALL_SEQUENCE
 109                                 + ";");
 110                 newCode.add("");
 111                 // DefineVar declaration
 112                 for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
 113                         InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct
 114                                         .get(interfaceName).construct;
 115                         ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
 116                         newCode.add("/* DefineVar in " + interfaceName + " */");
 117                         for (int i = 0; i < defineVars.size(); i++) {
 118                                 DefineVar var = defineVars.get(i);
 119                                 newCode.add(SPEC_PRIVATE_HASHTABLE + " " + var.getNewVarName()
 120                                                 + ";");
 121                         }
 122                         newCode.add("");
 123                 }
 124                 // Generate user-defined variable declaration
 125                 newCode.add("/* Beginnint of other user-defined variables */");
 126                 SequentialDefineSubConstruct globalCode = construct.code;
 127                 breakCodeLines(newCode, globalCode.declareVar);
 128                 newCode.add("/* End of other user-defined variables */");
 129                 // End of struct Sequential
 130                 newCode.add("} " + SPEC_SEQUENTIAL_STRUCT + "; /* End of struct "
 131                                 + SPEC_SEQUENTIAL_STRUCT + " */");
 132
 133                 // Generate
 134
 135                 // Generate code from the DefineVar, __COND_SAT__ and __ID__
 136                 // The hashtable in the contract can only contains pointers or integers
 137                 // __COND_SAT__
 138                 newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_CONDITION
 139                                 + ";");
 140                 // __ID__
 141                 newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_ID + ";");
 142                 // DefineVars
 143                 for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
 144                         InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct
 145                                         .get(interfaceName).construct;
 146                         ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
 147                         for (int i = 0; i < defineVars.size(); i++) {
 148                                 DefineVar var = defineVars.get(i);
 149                                 newCode.add(CodeVariables.SPEC_HASHTABLE + var.getNewVarName()
 150                                                 + ";");
 151                         }
 152                 }
 153                 // __interface
 154                 newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_INTERFACE
 155                                 + ";");
 156                 // __interface_call_sequence
 157                 newCode.add(CodeVariables.SPEC_HASHTABLE
 158                                 + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ";");
 159                 // Interface call sequence varaiable
 160                 newCode.add(CodeVariables.SPEC_TAG + " "
 161                                 + CodeVariables.INTERFACE_CALL_SEQUENCE + ";");
 162                 // End of the struct
 163                 newCode.add("}");
 164
 165                 // FIXME: Constructor should be modified and put in the right place
 166                 // Generate constructor (the place to initialize everything!)
 167                 breakCodeLines(newCode, globalCode.initVar);
 168                 // __COND_SAT__
 169                 newCode.add("init_table(&" + CodeVariables.SPEC_CONDITION + ");");
 170                 // __ID__
 171                 newCode.add("init_table(&" + CodeVariables.SPEC_ID + ");");
 172                 // DefineVars
 173                 for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
 174                         InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct
 175                                         .get(interfaceName).construct;
 176                         ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
 177                         for (int i = 0; i < defineVars.size(); i++) {
 178                                 DefineVar var = defineVars.get(i);
 179                                 newCode.add("init_table(&" + var.getNewVarName() + ");");
 180                         }
 181                 }
 182                 // __interface
 183                 newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE + ");");
 184                 // __interface_call_sequence
 185                 newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE
 186                                 + ");");
 187
 188                 // Pass the happens-before relationship check here
 189                 newCode.addAll(CodeVariables.generateHBInitAnnotation(semantics));
 190
 191                 newCode.add("\n");
 192
 193                 // Generate the sequential functions
 194                 breakCodeLines(newCode, globalCode.defineFunc);
 195
 196                 // The end
 197                 newCode.add("#endif " + SPEC_SEQUENTIAL_HEADER_MACRO + "\t/* End of "
 198                                 + SPEC_SEQUENTIAL_HEADER + " */");
 199
 200                 printCode(newCode);
 201                 return newCode;
 202         }
 203
 204         public static ArrayList<String> generateHBInitAnnotation(
 205                         SemanticsChecker semantics) {
 206                 ArrayList<String> newCode = new ArrayList<String>();
 207                 int hbConditionInitIdx = 0;
 208                 for (ConditionalInterface left : semantics.getHBConditions().keySet()) {
 209                         for (ConditionalInterface right : semantics.getHBConditions().get(
 210                                         left)) {
 211                                 String structVarName = "hbConditionInit" + hbConditionInitIdx;
 212                                 hbConditionInitIdx++;
 213                                 int interfaceNumBefore = semantics.interface2Num
 214                                                 .get(left.interfaceName), hbLabelNumBefore = semantics.hbLabel2Num
 215                                                 .get(left.hbConditionLabel), interfaceNumAfter = semantics.interface2Num
 216                                                 .get(right.interfaceName), hbLabelNumAfter = semantics.hbLabel2Num
 217                                                 .get(right.hbConditionLabel);
 218                                 newCode.add(ANNO_HB_INIT + " " + structVarName + ";");
 219
 220                                 newCode.add(structVarName + "." + "interface_num_before"
 221                                                 + " = " + interfaceNumBefore + ";");
 222                                 newCode.add(structVarName + "." + "hb_condition_num_before"
 223                                                 + " = " + hbLabelNumBefore + ";");
 224                                 newCode.add(structVarName + "." + "interface_num_after" + " = "
 225                                                 + interfaceNumAfter + ";");
 226                                 newCode.add(structVarName + "." + "hb_condition_num_after"
 227                                                 + " = " + hbLabelNumAfter + ";");
 228
 229                                 newCode.add(CDSAnnotate + "(" + CDSAnnotateType + ", &"
 230                                                 + structVarName + ");");
 231                         }
 232                 }
 233                 return newCode;
 234         }
 235 }