package edu.uci.eecs.specCompiler.codeGenerator;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.IOException;
import java.util.ArrayList;
import java.util.HashMap;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.Construct;
import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct;
import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
import edu.uci.eecs.specCompiler.specExtraction.SpecNotMatchException;
/**
*
* This class will generate the annotated C code that can run on the current
* model checker.
*
*
* @author peizhaoo
*
*/
public class CodeGenerator {
private SemanticsChecker _semantics;
private SpecExtractor _extractor;
private File[] srcFiles;
private HashMap> contents;
private HashMap> codeAdditions;
public CodeGenerator(File[] srcFiles) {
this.srcFiles = srcFiles;
this.contents = new HashMap>();
readSrcFiles();
this.codeAdditions = new HashMap>();
_extractor = new SpecExtractor();
try {
_extractor.extract(srcFiles);
} catch (SpecNotMatchException e1) {
e1.printStackTrace();
}
_semantics = new SemanticsChecker(_extractor.getConstructs());
try {
_semantics.check();
System.out.println(_semantics);
} catch (SemanticsCheckerException e) {
e.printStackTrace();
}
}
private ArrayList readSrcFile(File f) throws IOException {
BufferedReader bf = new BufferedReader(new FileReader(f));
ArrayList content = new ArrayList();
String curLine;
while ((curLine = bf.readLine()) != null) {
content.add(curLine);
}
return content;
}
private void readSrcFiles() {
for (int i = 0; i < srcFiles.length; i++) {
File f = srcFiles[i];
if (!contents.containsKey(f)) {
try {
contents.put(f, readSrcFile(f));
} catch (IOException e) {
e.printStackTrace();
}
}
}
}
/**
*
* Generate all the global code, including the "@DefineVar" in each
* "@Interface" define
*
*/
private void globalConstruct2Code(SpecConstruct inst) {
int lineNum = inst.endLineNum + 1;
GlobalConstruct construct = (GlobalConstruct) inst.construct;
ArrayList newCode = new ArrayList();
// Generate the code in global construct first
String globalCode = construct.code;
int begin = 0, end = 0;
while (end < globalCode.length()) {
if (globalCode.charAt(end) == '\n') {
String line = globalCode.substring(begin, end);
newCode.add(line);
begin = end + 1;
}
end++;
}
// Generate code from the DefineVar and __COND_SAT__
CodeAddition addition = new CodeAddition(lineNum, newCode);
if (!codeAdditions.containsKey(inst.file)) {
codeAdditions.put(inst.file, new ArrayList());
}
codeAdditions.get(inst.file).add(addition);
}
private void interface2Code(SpecConstruct inst) {
int lineNum = inst.endLineNum + 1;
GlobalConstruct construct = (GlobalConstruct) inst.construct;
ArrayList newCode = new ArrayList();
CodeAddition addition = new CodeAddition(lineNum, newCode);
if (!codeAdditions.containsKey(inst.file)) {
codeAdditions.put(inst.file, new ArrayList());
}
codeAdditions.get(inst.file).add(addition);
}
private void potentialCP2Code(SpecConstruct inst) {
int lineNum = inst.endLineNum + 1;
GlobalConstruct construct = (GlobalConstruct) inst.construct;
ArrayList newCode = new ArrayList();
CodeAddition addition = new CodeAddition(lineNum, newCode);
if (!codeAdditions.containsKey(inst.file)) {
codeAdditions.put(inst.file, new ArrayList());
}
codeAdditions.get(inst.file).add(addition);
}
private void CPDefine2Code(SpecConstruct inst) {
int lineNum = inst.endLineNum + 1;
GlobalConstruct construct = (GlobalConstruct) inst.construct;
ArrayList newCode = new ArrayList();
CodeAddition addition = new CodeAddition(lineNum, newCode);
if (!codeAdditions.containsKey(inst.file)) {
codeAdditions.put(inst.file, new ArrayList());
}
codeAdditions.get(inst.file).add(addition);
}
private void CPDefineCheck2Code(SpecConstruct inst) {
int lineNum = inst.endLineNum + 1;
GlobalConstruct construct = (GlobalConstruct) inst.construct;
ArrayList newCode = new ArrayList();
CodeAddition addition = new CodeAddition(lineNum, newCode);
if (!codeAdditions.containsKey(inst.file)) {
codeAdditions.put(inst.file, new ArrayList());
}
codeAdditions.get(inst.file).add(addition);
}
public void generateCode() {
for (int i = 0; i < _semantics.constructs.size(); i++) {
SpecConstruct inst = _semantics.constructs.get(i);
Construct construct = inst.construct;
if (construct instanceof GlobalConstruct) {
globalConstruct2Code(inst);
} else if (construct instanceof InterfaceConstruct) {
interface2Code(inst);
} else if (construct instanceof PotentialCPDefineConstruct) {
potentialCP2Code(inst);
} else if (construct instanceof CPDefineConstruct) {
CPDefine2Code(inst);
} else if (construct instanceof CPDefineCheckConstruct) {
CPDefineCheck2Code(inst);
}
}
}
public static void main(String[] argvs) {
String homeDir = Environment.HOME_DIRECTORY;
File[] srcFiles = {
// new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c"),
new File(homeDir
+ "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
// new File(homeDir + "/benchmark/ms-queue/my_queue.c")
};
CodeGenerator gen = new CodeGenerator(srcFiles);
gen.generateCode();
}
}