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.Collections;
  10 import java.util.HashMap;
  11 import java.util.Iterator;
  12
  13 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
  14 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
  15 import edu.uci.eecs.specCompiler.specExtraction.ClassEndConstruct;
  16 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
  17 import edu.uci.eecs.specCompiler.specExtraction.Construct;
  18 import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
  19 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
  20 import edu.uci.eecs.specCompiler.specExtraction.IDExtractor;
  21 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
  22 import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
  23 import edu.uci.eecs.specCompiler.specExtraction.ParserUtils;
  24 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
  25 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
  26 import edu.uci.eecs.specCompiler.specExtraction.SourceFileInfo;
  27 import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
  28
  29 /**
  30  * <p>
  31  * This class will generate the annotated C code that can run on the current
  32  * model checker.
  33  * </p>
  34  *
  35  * @author peizhaoo
  36  *
  37  */
  38 public class CodeGenerator {
  39         private SemanticsChecker _semantics;
  40         private SpecExtractor _extractor;
  41
  42         private File[] srcFiles;
  43
  44         private HashMap<File, SourceFileInfo> srcFilesInfo;
  45
  46         private HashMap<File, ArrayList<CodeAddition>> codeAdditions;
  47
  48         public CodeGenerator(File[] srcFiles) {
  49                 this.srcFiles = srcFiles;
  50                 _extractor = new SpecExtractor();
  51                 _extractor.extract(srcFiles);
  52
  53                 this.srcFilesInfo = _extractor.srcFilesInfo;
  54
  55                 this.codeAdditions = new HashMap<File, ArrayList<CodeAddition>>();
  56
  57                 _semantics = new SemanticsChecker(_extractor);
  58                 try {
  59                         _semantics.check();
  60                         System.out.println(_semantics);
  61                 } catch (SemanticsCheckerException e) {
  62                         e.printStackTrace();
  63                 }
  64         }
  65
  66         /**
  67          * <p>
  68          * Generate all the global code, including the "@DefineVar" in each
  69          * "@Interface" define
  70          * </p>
  71          */
  72         private void globalConstruct2Code(GlobalConstruct construct) {
  73                 ArrayList<String> newCode = CodeVariables.generateGlobalVarDeclaration(
  74                                 _semantics, construct);
  75                 // Add it to the codeAdditions
  76                 if (!codeAdditions.containsKey(construct.file)) {
  77                         codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
  78                 }
  79                 CodeAddition addition = new CodeAddition(construct.beginLineNum,
  80                                 newCode);
  81                 codeAdditions.get(construct.file).add(addition);
  82                 newCode = CodeVariables.generateStaticVarDefine(_semantics, construct);
  83                 if (newCode.size() > 0) {
  84                         addition = new CodeAddition(
  85                                         _semantics.getClassEndConstruct().beginLineNum, newCode);
  86                         codeAdditions.get(construct.file).add(addition);
  87                 }
  88         }
  89
  90         // Wrap the interface and then renaem it
  91         private void interface2Code(InterfaceConstruct construct) {
  92                 // If there's no define construct for it, we generate the wrapper just
  93                 // in place without declaration
  94                 InterfaceDefineConstruct defineConstruct = _semantics.interfaceName2DefineConstruct
  95                                 .get(construct.name);
  96                 ArrayList<String> newCode;
  97                 int lineNum;
  98                 CodeAddition addition;
  99                 // Then generate the wrapper if necessary
 100                 if (defineConstruct != null) { // Need to have a wrapper declaration
 101                         newCode = CodeVariables.generateInterfaceWrapperDeclaration(
 102                                         _semantics, construct);
 103                         lineNum = construct.beginLineNum;
 104                         // Add the wrapper declaration
 105                         addition = new CodeAddition(lineNum, newCode);
 106                         if (!codeAdditions.containsKey(construct.file)) {
 107                                 codeAdditions
 108                                                 .put(construct.file, new ArrayList<CodeAddition>());
 109                         }
 110                         codeAdditions.get(construct.file).add(addition);
 111
 112                         // Add the wrapper definition
 113                         newCode = CodeVariables.generateInterfaceWrapperDefinition(
 114                                         _semantics, construct);
 115                         lineNum = defineConstruct.beginLineNum;
 116                         // Add the wrapper declaration
 117                         addition = new CodeAddition(lineNum, newCode);
 118                         if (!codeAdditions.containsKey(defineConstruct.file)) {
 119                                 codeAdditions.put(defineConstruct.file,
 120                                                 new ArrayList<CodeAddition>());
 121                         }
 122                         codeAdditions.get(defineConstruct.file).add(addition);
 123                 } else { // No declaration needed
 124                         // Last generate the definition
 125                         newCode = CodeVariables.generateInterfaceWrapperDefinition(
 126                                         _semantics, construct);
 127                         lineNum = construct.beginLineNum;
 128                         // Add the wrapper declaration
 129                         addition = new CodeAddition(lineNum, newCode);
 130                         if (!codeAdditions.containsKey(construct.file)) {
 131                                 codeAdditions
 132                                                 .put(construct.file, new ArrayList<CodeAddition>());
 133                         }
 134                         codeAdditions.get(construct.file).add(addition);
 135                 }
 136
 137                 // Don't forget to rename the interface
 138                 CodeVariables.renameInterface(_semantics, construct);
 139         }
 140
 141         private void potentialCPDefine2Code(PotentialCPDefineConstruct construct) {
 142                 int lineNum = construct.beginLineNum;
 143                 ArrayList<String> newCode = CodeVariables.generatePotentialCPDefine(
 144                                 _semantics, construct);
 145
 146                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 147                 if (!codeAdditions.containsKey(construct.file)) {
 148                         codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
 149                 }
 150                 codeAdditions.get(construct.file).add(addition);
 151         }
 152
 153         private void CPDefine2Code(CPDefineConstruct construct) {
 154                 int lineNum = construct.beginLineNum;
 155                 ArrayList<String> newCode = CodeVariables.generateCPDefine(_semantics,
 156                                 construct);
 157
 158                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 159                 if (!codeAdditions.containsKey(construct.file)) {
 160                         codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
 161                 }
 162                 codeAdditions.get(construct.file).add(addition);
 163         }
 164
 165         private void CPDefineCheck2Code(CPDefineCheckConstruct construct) {
 166                 int lineNum = construct.beginLineNum;
 167                 ArrayList<String> newCode = CodeVariables.generateCPDefineCheck(
 168                                 _semantics, construct);
 169
 170                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 171                 if (!codeAdditions.containsKey(construct.file)) {
 172                         codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
 173                 }
 174                 codeAdditions.get(construct.file).add(addition);
 175         }
 176
 177         private void EntryPoint2Code(EntryPointConstruct construct) {
 178                 int lineNum = construct.beginLineNum;
 179                 ArrayList<String> newCode = new ArrayList<String>();
 180                 newCode.addAll(CodeVariables.generateEntryPointInitCall());
 181
 182                 CodeAddition addition = new CodeAddition(lineNum, newCode);
 183                 if (!codeAdditions.containsKey(construct.file)) {
 184                         codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
 185                 }
 186                 codeAdditions.get(construct.file).add(addition);
 187         }
 188
 189         private ArrayList<String> insertAnnotation2Src(
 190                         ArrayList<CodeAddition> additions, ArrayList<String> content) {
 191                 int totalSize = content.size();
 192                 for (int i = 0; i < additions.size(); i++) {
 193                         totalSize += additions.size();
 194                 }
 195                 ArrayList<String> newContent = new ArrayList<String>(totalSize);
 196                 int curSrcLine = 0;
 197                 for (int i = 0; i < additions.size(); i++) {
 198                         CodeAddition addition = additions.get(i);
 199                         if (curSrcLine < addition.lineNum) {
 200                                 // Be careful, subList is the interval [begin, end)
 201                                 newContent
 202                                                 .addAll(content.subList(curSrcLine, addition.lineNum));
 203                                 curSrcLine = addition.lineNum;
 204                         }
 205                         newContent.addAll(addition.newCode);
 206                 }
 207                 newContent.addAll(content.subList(curSrcLine, content.size()));
 208                 return newContent;
 209         }
 210
 211         public void generateCode() {
 212                 for (int i = 0; i < _semantics.constructs.size(); i++) {
 213                         Construct construct = _semantics.constructs.get(i);
 214                         if (construct instanceof GlobalConstruct) {
 215                                 globalConstruct2Code((GlobalConstruct) construct);
 216                         } else if (construct instanceof InterfaceConstruct) {
 217                                 interface2Code((InterfaceConstruct) construct);
 218                         } else if (construct instanceof PotentialCPDefineConstruct) {
 219                                 potentialCPDefine2Code((PotentialCPDefineConstruct) construct);
 220                         } else if (construct instanceof CPDefineConstruct) {
 221                                 CPDefine2Code((CPDefineConstruct) construct);
 222                         } else if (construct instanceof CPDefineCheckConstruct) {
 223                                 CPDefineCheck2Code((CPDefineCheckConstruct) construct);
 224                         } else if (construct instanceof EntryPointConstruct) {
 225                                 EntryPoint2Code((EntryPointConstruct) construct);
 226                         }
 227                 }
 228                 // Sort code additions
 229                 for (File file : codeAdditions.keySet()) {
 230                         ArrayList<CodeAddition> additions = codeAdditions.get(file);
 231                         if (additions.size() == 0) // Simply do nothing
 232                                 continue;
 233                         ArrayList<String> content = _semantics.srcFilesInfo.get(file).content;
 234                         Collections.sort(additions, CodeAddition.lineNumComparator);
 235                         // Insert generated annotation to the source files
 236                         ArrayList<String> newContent = insertAnnotation2Src(additions,
 237                                         content);
 238                         // Write it back to file
 239                         ParserUtils.write2File(file, newContent);
 240                 }
 241
 242         }
 243
 244         public static void main(String[] argvs) {
 245                 String homeDir = Environment.HOME_DIRECTORY;
 246                 File[] srcFiles = {
 247                                 // new File(Environment.MODEL_CHECKER_TEST_DIR +
 248                                 // "/backup_linuxrwlocks.c") };
 249                                  new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c")
 250                                  };
 251                                 // new File(homeDir
 252                                 // +
 253                                 // "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
 254                                 // };
 255 //                              new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
 256 //                              new File(homeDir + "/benchmark/ms-queue/main.c"),
 257 //                              new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
 258                 // new File(homeDir + "/benchmark/test/test.c") };
 259                 CodeGenerator gen = new CodeGenerator(srcFiles);
 260                 gen.generateCode();
 261         }
 262 }