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
 116                 // DefineVars
 117                 for (String interfaceName : _semantics.interfaceName2Construct.keySet()) {
 118                         InterfaceConstruct iConstruct = (InterfaceConstruct) _semantics.interfaceName2Construct
 119                                         .get(interfaceName).construct;
 120                         ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
 121                         for (int i = 0; i < defineVars.size(); i++) {
 122                                 DefineVar var = defineVars.get(i);
 123                                 newCode.add(CodeVariables.SPEC_HASHTABLE + var.getNewVarName()
 124                                                 + ";");
 125                         }
 126                 }
 127
 128                 // __interface
 129                 newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_INTERFACE
 130                                 + ";");
 131
 132                 // End of the struct
 133                 newCode.add("}");
 134
 135                 // FIXME: Constructor should be modified and put in the right place
 136                 // Generate constructor (the place to initialize everything!)
 137                 breakCodeLines(newCode, globalCode.initVar);
 138                 // __COND_SAT__
 139                 newCode.add("init_table(&" + CodeVariables.SPEC_CONDITION + ");");
 140                 // __ID__
 141                 newCode.add("init_table(&" + 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("init_table(&" + var.getNewVarName() + ");");
 150                         }
 151                 }
 152                 // __interface
 153                 newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE + ");");
 154
 155                 // Pass the happens-before relationship check here
 156                 newCode.addAll(CodeVariables.generateHBInitAnnotation(_semantics));
 157
 158                 newCode.add("\n");
 159
 160                 // Generate the sequential functions
 161                 breakCodeLines(newCode, globalCode.defineFunc);
 162
 163                 printCode(newCode);
 164
 165                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 166                 if (!codeAdditions.containsKey(inst.file)) {
 167                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 168                 }
 169                 codeAdditions.get(inst.file).add(addition);
 170         }
 171
 172         // Break the code (String) into multiple lines and add it to newCode
 173         private void breakCodeLines(ArrayList<String> newCode, String code) {
 174                 int begin = 0, end = 0;
 175                 while (end < code.length()) {
 176                         if (code.charAt(end) == '\n') {
 177                                 String line = code.substring(begin, end);
 178                                 newCode.add(line);
 179                                 begin = end + 1;
 180                         }
 181                         end++;
 182                 }
 183         }
 184
 185         private void printCode(ArrayList<String> code) {
 186                 for (int i = 0; i < code.size(); i++) {
 187                         System.out.println(code.get(i));
 188                 }
 189         }
 190
 191         // Mainly rename and wrap the interface
 192         private void interface2Code(SpecConstruct inst)
 193                         throws InterfaceWrongFormatException {
 194                 int lineNum = inst.endLineNum + 1;
 195                 InterfaceConstruct construct = (InterfaceConstruct) inst.construct;
 196                 ArrayList<String> newCode = new ArrayList<String>();
 197
 198                 // Rename the interface name
 199                 File file = inst.file;
 200                 String funcDecl = inst.interfaceDeclBody;
 201                 // Rename the function declaration
 202                 String funcName = renameInterface(inst);
 203                 // Also rename the function definition if it's separated from the
 204                 // declaration
 205                 SpecConstruct definition = _semantics.interfaceName2DefineConstruct
 206                                 .get(construct.name);
 207                 if (definition != null) {
 208                         String funcDefintionName = renameInterface(definition);
 209                         assert (funcDefintionName.equals(funcName));
 210                 }
 211
 212                 // Generate new wrapper
 213                 breakCodeLines(newCode, funcDecl);
 214
 215                 newCode.add("{");
 216
 217                 // Generate
 218
 219                 // FIXME: Add Happens-before check here
 220
 221                 newCode.add("}");
 222                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 223                 if (!codeAdditions.containsKey(inst.file)) {
 224                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 225                 }
 226                 codeAdditions.get(inst.file).add(addition);
 227         }
 228
 229         // Returns the function name that has been renamed and replace the old line
 230         private String renameInterface(SpecConstruct inst)
 231                         throws InterfaceWrongFormatException {
 232                 String funcDecl = inst.interfaceDeclBody;
 233                 ArrayList<String> content = contents.get(inst.file);
 234
 235                 // Depending on "(" to find the function name, so it doesn't matter if
 236                 // there's any template
 237                 int begin = 0, end = funcDecl.indexOf('(');
 238                 if (end == -1) {
 239                         throw new InterfaceWrongFormatException(funcDecl
 240                                         + "\n has wrong format!");
 241                 }
 242                 end--;
 243                 while (end > 0) {
 244                         char ch = funcDecl.charAt(end);
 245                         if (ch == '_' || (ch >= 'a' && ch <= 'z')
 246                                         || (ch >= 'A' && ch <= 'Z') || (ch >= '0' && ch <= '9')) {
 247                                 break;
 248                         }
 249                         end--;
 250                 }
 251                 begin = end;
 252                 while (begin > 0) {
 253                         char ch = funcDecl.charAt(begin);
 254                         if (ch == '_' || (ch >= 'a' && ch <= 'z')
 255                                         || (ch >= 'A' && ch <= 'Z') || (ch >= '0' && ch <= '9')) {
 256                                 begin--;
 257                                 continue;
 258                         }
 259                         break;
 260                 }
 261                 String funcName = funcDecl.substring(begin + 1, end + 1), newLine;
 262                 int lineBreakIdx = funcDecl.indexOf('\n');
 263                 int firstLineBreak = lineBreakIdx == -1 ? funcDecl.length()
 264                                 : lineBreakIdx;
 265                 newLine = funcDecl.substring(0, begin + 1)
 266                                 + CodeVariables.SPEC_INTERFACE_WRAPPER + funcName
 267                                 + funcDecl.substring(end + 1, firstLineBreak);
 268                 // Be careful: lineNum - 1 -> index of content array
 269                 content.set(inst.endLineNum, newLine);
 270                 return funcName;
 271         }
 272
 273         private void potentialCP2Code(SpecConstruct inst) {
 274                 int lineNum = inst.endLineNum + 1;
 275                 GlobalConstruct construct = (GlobalConstruct) inst.construct;
 276                 ArrayList<String> newCode = new ArrayList<String>();
 277
 278                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 279                 if (!codeAdditions.containsKey(inst.file)) {
 280                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 281                 }
 282                 codeAdditions.get(inst.file).add(addition);
 283         }
 284
 285         private void CPDefine2Code(SpecConstruct inst) {
 286                 int lineNum = inst.endLineNum + 1;
 287                 GlobalConstruct construct = (GlobalConstruct) inst.construct;
 288                 ArrayList<String> newCode = new ArrayList<String>();
 289
 290                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 291                 if (!codeAdditions.containsKey(inst.file)) {
 292                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 293                 }
 294                 codeAdditions.get(inst.file).add(addition);
 295         }
 296
 297         private void CPDefineCheck2Code(SpecConstruct inst) {
 298                 int lineNum = inst.endLineNum + 1;
 299                 GlobalConstruct construct = (GlobalConstruct) inst.construct;
 300                 ArrayList<String> newCode = new ArrayList<String>();
 301
 302                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 303                 if (!codeAdditions.containsKey(inst.file)) {
 304                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 305                 }
 306                 codeAdditions.get(inst.file).add(addition);
 307         }
 308
 309         public void generateCode() {
 310                 for (int i = 0; i < _semantics.constructs.size(); i++) {
 311                         SpecConstruct inst = _semantics.constructs.get(i);
 312                         Construct construct = inst.construct;
 313                         if (construct instanceof GlobalConstruct) {
 314                                 globalConstruct2Code(inst);
 315                         } else if (construct instanceof InterfaceConstruct) {
 316                                 try {
 317                                         interface2Code(inst);
 318                                 } catch (InterfaceWrongFormatException e) {
 319                                         e.printStackTrace();
 320                                 }
 321                         } else if (construct instanceof PotentialCPDefineConstruct) {
 322                                 // potentialCP2Code(inst);
 323                         } else if (construct instanceof CPDefineConstruct) {
 324                                 // CPDefine2Code(inst);
 325                         } else if (construct instanceof CPDefineCheckConstruct) {
 326                                 // CPDefineCheck2Code(inst);
 327                         }
 328                 }
 329         }
 330
 331         public static void main(String[] argvs) {
 332                 String homeDir = Environment.HOME_DIRECTORY;
 333                 File[] srcFiles = {
 334                                 // new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c"),
 335                                 // new File(homeDir
 336                                 // +
 337                                 // "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
 338                                 new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
 339                                 new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
 340                 CodeGenerator gen = new CodeGenerator(srcFiles);
 341                 gen.generateCode();
 342         }
 343 }