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.CPDefineCheckConstruct;
  13 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
  14 import edu.uci.eecs.specCompiler.specExtraction.ClassEndConstruct;
  15 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
  16 import edu.uci.eecs.specCompiler.specExtraction.Construct;
  17 import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
  18 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
  19 import edu.uci.eecs.specCompiler.specExtraction.IDExtractor;
  20 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
  21 import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
  22 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
  23 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
  24 import edu.uci.eecs.specCompiler.specExtraction.SourceFileInfo;
  25 import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
  26
  27 /**
  28  * <p>
  29  * This class will generate the annotated C code that can run on the current
  30  * model checker.
  31  * </p>
  32  *
  33  * @author peizhaoo
  34  *
  35  */
  36 public class CodeGenerator {
  37         private SemanticsChecker _semantics;
  38         private SpecExtractor _extractor;
  39
  40         private File[] srcFiles;
  41
  42         private HashMap<File, SourceFileInfo> srcFilesInfo;
  43
  44         private HashMap<File, ArrayList<CodeAddition>> codeAdditions;
  45
  46         public CodeGenerator(File[] srcFiles) {
  47                 this.srcFiles = srcFiles;
  48                 _extractor = new SpecExtractor();
  49                 _extractor.extract(srcFiles);
  50
  51                 this.srcFilesInfo = _extractor.srcFilesInfo;
  52
  53                 this.codeAdditions = new HashMap<File, ArrayList<CodeAddition>>();
  54
  55                 _semantics = new SemanticsChecker(_extractor);
  56                 try {
  57                         _semantics.check();
  58                         System.out.println(_semantics);
  59                 } catch (SemanticsCheckerException e) {
  60                         e.printStackTrace();
  61                 }
  62         }
  63
  64         /**
  65          * <p>
  66          * Generate all the global code, including the "@DefineVar" in each
  67          * "@Interface" define
  68          * </p>
  69          */
  70         private void globalConstruct2Code(GlobalConstruct construct) {
  71                 ArrayList<String> newCode = CodeVariables.generateGlobalVarDeclaration(
  72                                 _semantics, construct);
  73                 // Add it to the codeAdditions
  74                 if (!codeAdditions.containsKey(construct.file)) {
  75                         codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
  76                 }
  77                 CodeAddition addition = new CodeAddition(construct.beginLineNum,
  78                                 newCode);
  79                 codeAdditions.get(construct.file).add(addition);
  80                 newCode = CodeVariables.generateStaticVarDefine(_semantics, construct);
  81                 if (newCode.size() > 0) {
  82                         addition = new CodeAddition(_semantics.getClassEndConstruct().beginLineNum, newCode);
  83                         codeAdditions.get(construct.file).add(addition);
  84                 }
  85         }
  86
  87         // Mainly rename and wrap the interface
  88         private void interface2Code(InterfaceConstruct construct)
  89                         throws InterfaceWrongFormatException {
  90                 ArrayList<String> newCode = CodeVariables.generateInterfaceWrapper(
  91                                 _semantics, construct);
  92                 int lineNum = construct.beginLineNum;
  93                 // Add it to the codeAdditions
  94                 CodeAddition addition = new CodeAddition(lineNum, newCode);
  95                 if (!codeAdditions.containsKey(construct.file)) {
  96                         codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
  97                 }
  98                 codeAdditions.get(construct.file).add(addition);
  99         }
 100
 101         private void potentialCPDefine2Code(PotentialCPDefineConstruct construct) {
 102                 int lineNum = construct.beginLineNum;
 103                 ArrayList<String> newCode = CodeVariables.generatePotentialCPDefine(
 104                                 _semantics, construct);
 105
 106                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 107                 if (!codeAdditions.containsKey(construct.file)) {
 108                         codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
 109                 }
 110                 codeAdditions.get(construct.file).add(addition);
 111         }
 112
 113         private void CPDefine2Code(CPDefineConstruct construct) {
 114                 int lineNum = construct.beginLineNum;
 115                 ArrayList<String> newCode = CodeVariables.generateCPDefine(_semantics, construct);
 116
 117                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 118                 if (!codeAdditions.containsKey(construct.file)) {
 119                         codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
 120                 }
 121                 codeAdditions.get(construct.file).add(addition);
 122         }
 123
 124         private void CPDefineCheck2Code(CPDefineCheckConstruct construct) {
 125                 int lineNum = construct.beginLineNum;
 126                 ArrayList<String> newCode = CodeVariables.generateCPDefineCheck(_semantics, construct);
 127
 128                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 129                 if (!codeAdditions.containsKey(construct.file)) {
 130                         codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
 131                 }
 132                 codeAdditions.get(construct.file).add(addition);
 133         }
 134
 135         private void EntryPoint2Code(EntryPointConstruct construct) {
 136                 int lineNum = construct.beginLineNum;
 137                 ArrayList<String> newCode = new ArrayList<String>();
 138                 newCode.add(")
 139
 140                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 141                 if (!codeAdditions.containsKey(construct.file)) {
 142                         codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
 143                 }
 144                 codeAdditions.get(construct.file).add(addition);
 145         }
 146
 147
 148         public void generateCode() {
 149                 for (int i = 0; i < _semantics.constructs.size(); i++) {
 150                         Construct construct = _semantics.constructs.get(i);
 151                         if (construct instanceof GlobalConstruct) {
 152                                 globalConstruct2Code((GlobalConstruct) construct);
 153                         } else if (construct instanceof InterfaceConstruct) {
 154                                 try {
 155                                         interface2Code((InterfaceConstruct) construct);
 156                                 } catch (InterfaceWrongFormatException e) {
 157                                         e.printStackTrace();
 158                                 }
 159                         } else if (construct instanceof PotentialCPDefineConstruct) {
 160                                 // potentialCP2Code(inst);
 161                         } else if (construct instanceof CPDefineConstruct) {
 162                                 // CPDefine2Code(inst);
 163                         } else if (construct instanceof CPDefineCheckConstruct) {
 164                                 // CPDefineCheck2Code(inst);
 165                         }
 166                 }
 167         }
 168
 169         public static void main(String[] argvs) {
 170                 String homeDir = Environment.HOME_DIRECTORY;
 171                 File[] srcFiles = {
 172                 // new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c"),
 173                 new File(homeDir
 174                                 + "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"), };
 175                 // new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
 176                 // new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
 177                 CodeGenerator gen = new CodeGenerator(srcFiles);
 178                 gen.generateCode();
 179         }
 180 }