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
  11 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
  12 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
  13 import edu.uci.eecs.specCompiler.specExtraction.Construct;
  14 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
  15 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
  16 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
  17 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
  18 import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct;
  19 import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
  20 import edu.uci.eecs.specCompiler.specExtraction.SpecNotMatchException;
  21
  22 /**
  23  * <p>
  24  * This class will generate the annotated C code that can run on the current
  25  * model checker.
  26  * </p>
  27  *
  28  * @author peizhaoo
  29  *
  30  */
  31 public class CodeGenerator {
  32         private SemanticsChecker _semantics;
  33         private SpecExtractor _extractor;
  34
  35         private File[] srcFiles;
  36
  37         private HashMap<File, ArrayList<String>> contents;
  38
  39         private HashMap<File, ArrayList<CodeAddition>> codeAdditions;
  40
  41         public CodeGenerator(File[] srcFiles) {
  42                 this.srcFiles = srcFiles;
  43                 this.contents = new HashMap<File, ArrayList<String>>();
  44                 readSrcFiles();
  45                 this.codeAdditions = new HashMap<File, ArrayList<CodeAddition>>();
  46
  47                 _extractor = new SpecExtractor();
  48
  49                 try {
  50                         _extractor.extract(srcFiles);
  51                 } catch (SpecNotMatchException e1) {
  52                         e1.printStackTrace();
  53                 }
  54
  55                 _semantics = new SemanticsChecker(_extractor.getConstructs());
  56                 try {
  57                         _semantics.check();
  58                         System.out.println(_semantics);
  59                 } catch (SemanticsCheckerException e) {
  60                         e.printStackTrace();
  61                 }
  62         }
  63
  64         private ArrayList<String> readSrcFile(File f) throws IOException {
  65                 BufferedReader bf = new BufferedReader(new FileReader(f));
  66                 ArrayList<String> content = new ArrayList<String>();
  67                 String curLine;
  68                 while ((curLine = bf.readLine()) != null) {
  69                         content.add(curLine);
  70                 }
  71                 return content;
  72         }
  73
  74         private void readSrcFiles() {
  75                 for (int i = 0; i < srcFiles.length; i++) {
  76                         File f = srcFiles[i];
  77                         if (!contents.containsKey(f)) {
  78                                 try {
  79                                         contents.put(f, readSrcFile(f));
  80                                 } catch (IOException e) {
  81                                         e.printStackTrace();
  82                                 }
  83                         }
  84                 }
  85         }
  86
  87         /**
  88          * <p>
  89          * Generate all the global code, including the "@DefineVar" in each
  90          * "@Interface" define
  91          * </p>
  92          */
  93         private void globalConstruct2Code(SpecConstruct inst) {
  94                 int lineNum = inst.endLineNum + 1;
  95                 GlobalConstruct construct = (GlobalConstruct) inst.construct;
  96                 ArrayList<String> newCode = new ArrayList<String>();
  97
  98                 // Generate the inner class definition
  99                 newCode.add("class Sequential {\n");
 100                 newCode.add("public:\n");
 101
 102                 // Generate the code in global construct first
 103                 SequentialDefineSubConstruct globalCode = construct.code;
 104                 breakCodeLines(newCode, globalCode.declareVar);
 105                 breakCodeLines(newCode, globalCode.defineFunc);
 106
 107                 // Generate code from the DefineVar, __COND_SAT__ and __ID__
 108
 109
 110                 // Generate the end of the inner class definition
 111                 newCode.add("};\n");
 112 //              printCode(newCode);
 113
 114                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 115                 if (!codeAdditions.containsKey(inst.file)) {
 116                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 117                 }
 118                 codeAdditions.get(inst.file).add(addition);
 119         }
 120
 121         private void breakCodeLines(ArrayList<String> newCode, String code) {
 122                 int begin = 0, end = 0;
 123                 while (end < code.length()) {
 124                         if (code.charAt(end) == '\n') {
 125                                 String line = code.substring(begin, end);
 126                                 newCode.add(line);
 127                                 begin = end + 1;
 128                         }
 129                         end++;
 130                 }
 131         }
 132
 133         private void printCode(ArrayList<String> code) {
 134                 for (int i = 0; i < code.size(); i++) {
 135                         System.out.println(code.get(i));
 136                 }
 137         }
 138
 139         private void interface2Code(SpecConstruct inst) {
 140                 int lineNum = inst.endLineNum + 1;
 141                 GlobalConstruct construct = (GlobalConstruct) inst.construct;
 142                 ArrayList<String> newCode = new ArrayList<String>();
 143
 144
 145                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 146                 if (!codeAdditions.containsKey(inst.file)) {
 147                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 148                 }
 149                 codeAdditions.get(inst.file).add(addition);
 150         }
 151
 152         private void potentialCP2Code(SpecConstruct inst) {
 153                 int lineNum = inst.endLineNum + 1;
 154                 GlobalConstruct construct = (GlobalConstruct) inst.construct;
 155                 ArrayList<String> newCode = new ArrayList<String>();
 156
 157
 158                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 159                 if (!codeAdditions.containsKey(inst.file)) {
 160                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 161                 }
 162                 codeAdditions.get(inst.file).add(addition);
 163         }
 164
 165         private void CPDefine2Code(SpecConstruct inst) {
 166                 int lineNum = inst.endLineNum + 1;
 167                 GlobalConstruct construct = (GlobalConstruct) inst.construct;
 168                 ArrayList<String> newCode = new ArrayList<String>();
 169
 170
 171                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 172                 if (!codeAdditions.containsKey(inst.file)) {
 173                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 174                 }
 175                 codeAdditions.get(inst.file).add(addition);
 176         }
 177
 178         private void CPDefineCheck2Code(SpecConstruct inst) {
 179                 int lineNum = inst.endLineNum + 1;
 180                 GlobalConstruct construct = (GlobalConstruct) inst.construct;
 181                 ArrayList<String> newCode = new ArrayList<String>();
 182
 183
 184                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 185                 if (!codeAdditions.containsKey(inst.file)) {
 186                         codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
 187                 }
 188                 codeAdditions.get(inst.file).add(addition);
 189         }
 190
 191         public void generateCode() {
 192                 for (int i = 0; i < _semantics.constructs.size(); i++) {
 193                         SpecConstruct inst = _semantics.constructs.get(i);
 194                         Construct construct = inst.construct;
 195                         if (construct instanceof GlobalConstruct) {
 196                                 globalConstruct2Code(inst);
 197                         } else if (construct instanceof InterfaceConstruct) {
 198                                 interface2Code(inst);
 199                         } else if (construct instanceof PotentialCPDefineConstruct) {
 200                                 potentialCP2Code(inst);
 201                         } else if (construct instanceof CPDefineConstruct) {
 202                                 CPDefine2Code(inst);
 203                         } else if (construct instanceof CPDefineCheckConstruct) {
 204                                 CPDefineCheck2Code(inst);
 205                         }
 206                 }
 207         }
 208
 209         public static void main(String[] argvs) {
 210                 String homeDir = Environment.HOME_DIRECTORY;
 211                 File[] srcFiles = {
 212                 // new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c"),
 213                 new File(homeDir
 214                                 + "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
 215                 // new File(homeDir + "/benchmark/ms-queue/my_queue.c")
 216                 };
 217                 CodeGenerator gen = new CodeGenerator(srcFiles);
 218                 gen.generateCode();
 219         }
 220 }