src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java

   1 package edu.uci.eecs.specCompiler.codeGenerator;
   2
   3 import java.io.BufferedReader;
   4 import java.io.File;
   5 import java.io.FileNotFoundException;
   6 import java.io.FileReader;
   7 import java.io.IOException;
   8 import java.util.ArrayList;
   9 import java.util.HashMap;
  10 import java.util.Iterator;
  11
  12 import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
  13 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
  14 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
  15 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
  16 import edu.uci.eecs.specCompiler.specExtraction.Construct;
  17 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
  18 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
  19 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
  20 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
  21 import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct;
  22 import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
  23 import edu.uci.eecs.specCompiler.specExtraction.SpecNotMatchException;
  24
  25 /**
  26  * <p>
  27  * This class will generate the annotated C code that can run on the current
  28  * model checker.
  29  * </p>
  30  *
  31  * @author peizhaoo
  32  *
  33  */
  34 public class CodeGenerator {
  35         private SemanticsChecker _semantics;
  36         private SpecExtractor _extractor;
  37
  38         private File[] srcFiles;
  39
  40         private HashMap<File, ArrayList<String>> contents;
  41
  42         private HashMap<File, ArrayList<CodeAddition>> codeAdditions;
  43
  44         public CodeGenerator(File[] srcFiles) {
  45                 this.srcFiles = srcFiles;
  46                 this.contents = new HashMap<File, ArrayList<String>>();
  47                 readSrcFiles();
  48                 this.codeAdditions = new HashMap<File, ArrayList<CodeAddition>>();
  49
  50                 _extractor = new SpecExtractor();
  51
  52                 try {
  53                         _extractor.extract(srcFiles);
  54                 } catch (SpecNotMatchException e1) {
  55                         e1.printStackTrace();
  56                 }
  57
  58                 _semantics = new SemanticsChecker(_extractor.getConstructs());
  59                 try {
  60                         _semantics.check();
  61                         System.out.println(_semantics);
  62                 } catch (SemanticsCheckerException e) {
  63                         e.printStackTrace();
  64                 }
  65         }
  66
  67         private ArrayList<String> readSrcFile(File f) throws IOException {
  68                 BufferedReader bf = new BufferedReader(new FileReader(f));
  69                 ArrayList<String> content = new ArrayList<String>();
  70                 String curLine;
  71                 while ((curLine = bf.readLine()) != null) {
  72                         content.add(curLine);
  73                 }
  74                 return content;
  75         }
  76
  77         private void readSrcFiles() {
  78                 for (int i = 0; i < srcFiles.length; i++) {
  79                         File f = srcFiles[i];
  80                         if (!contents.containsKey(f)) {
  81                                 try {
  82                                         contents.put(f, readSrcFile(f));
  83                                 } catch (IOException e) {
  84                                         e.printStackTrace();
  85                                 }
  86                         }
  87                 }
  88         }
  89
  90         /**
  91          * <p>
  92          * Generate all the global code, including the "@DefineVar" in each
  93          * "@Interface" define
  94          * </p>
  95          */
  96         private void globalConstruct2Code(SpecConstruct inst) {
  97                 int lineNum = inst.endLineNum + 1;
  98                 GlobalConstruct construct = (GlobalConstruct) inst.construct;
  99                 ArrayList<String> newCode = new ArrayList<String>();
 100
 101                 // Generate all sequential variables into a struct
 102                 newCode.add("struct " + CodeVariables.SPEC_STRUCT + " {\n");
 103
 104                 // Generate the code in global construct first
 105                 SequentialDefineSubConstruct globalCode = construct.code;
 106                 breakCodeLines(newCode, globalCode.declareVar);
 107
 108                 // Generate code from the DefineVar, __COND_SAT__ and __ID__
 109                 // The hashtable in the contract can only contains pointers or integers
 110                 // __COND_SAT__
 111                 newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_CONDITION
 112                                 + ";");
 113                 // __ID__
 114                 newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_ID + ";");
 115                 // DefineVars
 116                 for (String interfaceName : _semantics.interfaceName2Construct.keySet()) {
 117                         InterfaceConstruct iConstruct = (InterfaceConstruct) _semantics.interfaceName2Construct
 118                                         .get(interfaceName).construct;
 119                         ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
 120                         for (int i = 0; i < defineVars.size(); i++) {
 121                                 DefineVar var = defineVars.get(i);
 122                                 newCode.add(CodeVariables.SPEC_HASHTABLE + var.getNewVarName()
 123                                                 + ";");
 124                         }
 125                 }
 126                 // __interface
 127                 newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_INTERFACE
 128                                 + ";");
 129                 // __interface_call_sequence
 130                 newCode.add(CodeVariables.SPEC_HASHTABLE
 131                                 + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ";");
 132                 // Interface call sequence varaiable
 133                 newCode.add(CodeVariables.SPEC_TAG + " "
 134                                 + CodeVariables.INTERFACE_CALL_SEQUENCE + ";");
 135                 // End of the struct
 136                 newCode.add("}");
 137
 138                 // FIXME: Constructor should be modified and put in the right place
 139                 // Generate constructor (the place to initialize everything!)
 140                 breakCodeLines(newCode, globalCode.initVar);
 141                 // __COND_SAT__
 142                 newCode.add("init_table(&" + CodeVariables.SPEC_CONDITION + ");");
 143                 // __ID__
 144                 newCode.add("init_table(&" + CodeVariables.SPEC_ID + ");");
 145                 // DefineVars
 146                 for (String interfaceName : _semantics.interfaceName2Construct.keySet()) {
 147                         InterfaceConstruct iConstruct = (InterfaceConstruct) _semantics.interfaceName2Construct
 148                                         .get(interfaceName).construct;
 149                         ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
 150                         for (int i = 0; i < defineVars.size(); i++) {
 151                                 DefineVar var = defineVars.get(i);
 152                                 newCode.add("init_table(&" + var.getNewVarName() + ");");
 153                         }
 154                 }
 155                 // __interface
 156                 newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE + ");");
 157                 // __interface_call_sequence
 158                 newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ");");
 159
 160                 // Pass the happens-before relationship check here
 161                 newCode.addAll(CodeVariables.generateHBInitAnnotation(_semantics));
 162
 163                 newCode.add("\n");
 164
 165                 // Generate the sequential functions
 166                 breakCodeLines(newCode, globalCode.defineFunc);
 167
 168                 printCode(newCode);
 169
 170                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 171                 if (!codeAdditions.containsKey(inst.file)) {
 172                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 173                 }
 174                 codeAdditions.get(inst.file).add(addition);
 175         }
 176
 177         // Break the code (String) into multiple lines and add it to newCode
 178         private void breakCodeLines(ArrayList<String> newCode, String code) {
 179                 int begin = 0, end = 0;
 180                 while (end < code.length()) {
 181                         if (code.charAt(end) == '\n') {
 182                                 String line = code.substring(begin, end);
 183                                 newCode.add(line);
 184                                 begin = end + 1;
 185                         }
 186                         end++;
 187                 }
 188         }
 189
 190         private void printCode(ArrayList<String> code) {
 191                 for (int i = 0; i < code.size(); i++) {
 192                         System.out.println(code.get(i));
 193                 }
 194         }
 195
 196         // Mainly rename and wrap the interface
 197         private void interface2Code(SpecConstruct inst)
 198                         throws InterfaceWrongFormatException {
 199                 int lineNum = inst.endLineNum + 1;
 200                 InterfaceConstruct construct = (InterfaceConstruct) inst.construct;
 201                 ArrayList<String> newCode = new ArrayList<String>();
 202
 203                 // Rename the interface name
 204                 File file = inst.file;
 205                 String funcDecl = inst.interfaceDeclBody;
 206                 // Rename the function declaration
 207                 String funcName = renameInterface(inst);
 208                 // Also rename the function definition if it's separated from the
 209                 // declaration
 210                 SpecConstruct definition = _semantics.interfaceName2DefineConstruct
 211                                 .get(construct.name);
 212                 if (definition != null) {
 213                         String funcDefintionName = renameInterface(definition);
 214                         assert (funcDefintionName.equals(funcName));
 215                 }
 216
 217                 // Generate new wrapper
 218                 /**
 219                  *
 220                  *
 221                  */
 222
 223                 breakCodeLines(newCode, funcDecl);
 224                 newCode.add("{");
 225                 // Generate interface sequence call
 226                 newCode.add(CodeVariables.UINT64 + " call_sequence_num = current(&"
 227                                 + CodeVariables.INTERFACE_CALL_SEQUENCE + ");");
 228                 // FIXME: Add Happens-before check here
 229                 newCode.add("}");
 230
 231                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 232                 if (!codeAdditions.containsKey(inst.file)) {
 233                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 234                 }
 235                 codeAdditions.get(inst.file).add(addition);
 236         }
 237
 238         // Returns the function name that has been renamed and replace the old line
 239         private String renameInterface(SpecConstruct inst)
 240                         throws InterfaceWrongFormatException {
 241                 String funcDecl = inst.interfaceDeclBody;
 242                 ArrayList<String> content = contents.get(inst.file);
 243
 244                 // Depending on "(" to find the function name, so it doesn't matter if
 245                 // there's any template
 246                 int begin = 0, end = funcDecl.indexOf('(');
 247                 if (end == -1) {
 248                         throw new InterfaceWrongFormatException(funcDecl
 249                                         + "\n has wrong format!");
 250                 }
 251                 end--;
 252                 while (end > 0) {
 253                         char ch = funcDecl.charAt(end);
 254                         if (ch == '_' || (ch >= 'a' && ch <= 'z')
 255                                         || (ch >= 'A' && ch <= 'Z') || (ch >= '0' && ch <= '9')) {
 256                                 break;
 257                         }
 258                         end--;
 259                 }
 260                 begin = end;
 261                 while (begin > 0) {
 262                         char ch = funcDecl.charAt(begin);
 263                         if (ch == '_' || (ch >= 'a' && ch <= 'z')
 264                                         || (ch >= 'A' && ch <= 'Z') || (ch >= '0' && ch <= '9')) {
 265                                 begin--;
 266                                 continue;
 267                         }
 268                         break;
 269                 }
 270                 String funcName = funcDecl.substring(begin + 1, end + 1), newLine;
 271                 int lineBreakIdx = funcDecl.indexOf('\n');
 272                 int firstLineBreak = lineBreakIdx == -1 ? funcDecl.length()
 273                                 : lineBreakIdx;
 274                 newLine = funcDecl.substring(0, begin + 1)
 275                                 + CodeVariables.SPEC_INTERFACE_WRAPPER + funcName
 276                                 + funcDecl.substring(end + 1, firstLineBreak);
 277                 // Be careful: lineNum - 1 -> index of content array
 278                 content.set(inst.endLineNum, newLine);
 279                 return funcName;
 280         }
 281
 282         private void potentialCP2Code(SpecConstruct inst) {
 283                 int lineNum = inst.endLineNum + 1;
 284                 GlobalConstruct construct = (GlobalConstruct) inst.construct;
 285                 ArrayList<String> newCode = new ArrayList<String>();
 286
 287                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 288                 if (!codeAdditions.containsKey(inst.file)) {
 289                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 290                 }
 291                 codeAdditions.get(inst.file).add(addition);
 292         }
 293
 294         private void CPDefine2Code(SpecConstruct inst) {
 295                 int lineNum = inst.endLineNum + 1;
 296                 GlobalConstruct construct = (GlobalConstruct) inst.construct;
 297                 ArrayList<String> newCode = new ArrayList<String>();
 298
 299                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 300                 if (!codeAdditions.containsKey(inst.file)) {
 301                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 302                 }
 303                 codeAdditions.get(inst.file).add(addition);
 304         }
 305
 306         private void CPDefineCheck2Code(SpecConstruct inst) {
 307                 int lineNum = inst.endLineNum + 1;
 308                 GlobalConstruct construct = (GlobalConstruct) inst.construct;
 309                 ArrayList<String> newCode = new ArrayList<String>();
 310
 311                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 312                 if (!codeAdditions.containsKey(inst.file)) {
 313                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 314                 }
 315                 codeAdditions.get(inst.file).add(addition);
 316         }
 317
 318         public void generateCode() {
 319                 for (int i = 0; i < _semantics.constructs.size(); i++) {
 320                         SpecConstruct inst = _semantics.constructs.get(i);
 321                         Construct construct = inst.construct;
 322                         if (construct instanceof GlobalConstruct) {
 323                                 globalConstruct2Code(inst);
 324                         } else if (construct instanceof InterfaceConstruct) {
 325                                 try {
 326                                         interface2Code(inst);
 327                                 } catch (InterfaceWrongFormatException e) {
 328                                         e.printStackTrace();
 329                                 }
 330                         } else if (construct instanceof PotentialCPDefineConstruct) {
 331                                 // potentialCP2Code(inst);
 332                         } else if (construct instanceof CPDefineConstruct) {
 333                                 // CPDefine2Code(inst);
 334                         } else if (construct instanceof CPDefineCheckConstruct) {
 335                                 // CPDefineCheck2Code(inst);
 336                         }
 337                 }
 338         }
 339
 340         public static void main(String[] argvs) {
 341                 String homeDir = Environment.HOME_DIRECTORY;
 342                 File[] srcFiles = {
 343                                 // new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c"),
 344                                 // new File(homeDir
 345                                 // +
 346                                 // "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
 347                                 new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
 348                                 new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
 349                 CodeGenerator gen = new CodeGenerator(srcFiles);
 350                 gen.generateCode();
 351         }
 352 }