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