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 java.util.Iterator;
import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
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.SequentialDefineSubConstruct;
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 all sequential variables into a struct
newCode.add("struct " + CodeVariables.SPEC_SEQUENTIAL_STRUCT + " {\n");
// Generate the code in global construct first
SequentialDefineSubConstruct globalCode = construct.code;
breakCodeLines(newCode, globalCode.declareVar);
// Generate code from the DefineVar, __COND_SAT__ and __ID__
// The hashtable in the contract can only contains pointers or integers
// __COND_SAT__
newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_CONDITION
+ ";");
// __ID__
newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_ID + ";");
// DefineVars
for (String interfaceName : _semantics.interfaceName2Construct.keySet()) {
InterfaceConstruct iConstruct = (InterfaceConstruct) _semantics.interfaceName2Construct
.get(interfaceName).construct;
ArrayList defineVars = iConstruct.action.defineVars;
for (int i = 0; i < defineVars.size(); i++) {
DefineVar var = defineVars.get(i);
newCode.add(CodeVariables.SPEC_HASHTABLE + var.getNewVarName()
+ ";");
}
}
// __interface
newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_INTERFACE
+ ";");
// __interface_call_sequence
newCode.add(CodeVariables.SPEC_HASHTABLE
+ CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ";");
// Interface call sequence varaiable
newCode.add(CodeVariables.SPEC_TAG + " "
+ CodeVariables.INTERFACE_CALL_SEQUENCE + ";");
// End of the struct
newCode.add("}");
// FIXME: Constructor should be modified and put in the right place
// Generate constructor (the place to initialize everything!)
breakCodeLines(newCode, globalCode.initVar);
// __COND_SAT__
newCode.add("init_table(&" + CodeVariables.SPEC_CONDITION + ");");
// __ID__
newCode.add("init_table(&" + CodeVariables.SPEC_ID + ");");
// DefineVars
for (String interfaceName : _semantics.interfaceName2Construct.keySet()) {
InterfaceConstruct iConstruct = (InterfaceConstruct) _semantics.interfaceName2Construct
.get(interfaceName).construct;
ArrayList defineVars = iConstruct.action.defineVars;
for (int i = 0; i < defineVars.size(); i++) {
DefineVar var = defineVars.get(i);
newCode.add("init_table(&" + var.getNewVarName() + ");");
}
}
// __interface
newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE + ");");
// __interface_call_sequence
newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ");");
// Pass the happens-before relationship check here
newCode.addAll(CodeVariables.generateHBInitAnnotation(_semantics));
newCode.add("\n");
// Generate the sequential functions
breakCodeLines(newCode, globalCode.defineFunc);
printCode(newCode);
CodeAddition addition = new CodeAddition(lineNum, newCode);
if (!codeAdditions.containsKey(inst.file)) {
codeAdditions.put(inst.file, new ArrayList());
}
codeAdditions.get(inst.file).add(addition);
}
// Break the code (String) into multiple lines and add it to newCode
private void breakCodeLines(ArrayList newCode, String code) {
int begin = 0, end = 0;
while (end < code.length()) {
if (code.charAt(end) == '\n') {
String line = code.substring(begin, end);
newCode.add(line);
begin = end + 1;
}
end++;
}
}
private void printCode(ArrayList code) {
for (int i = 0; i < code.size(); i++) {
System.out.println(code.get(i));
}
}
// Mainly rename and wrap the interface
private void interface2Code(SpecConstruct inst)
throws InterfaceWrongFormatException {
int lineNum = inst.endLineNum + 1;
InterfaceConstruct construct = (InterfaceConstruct) inst.construct;
ArrayList newCode = new ArrayList();
// Rename the interface name
File file = inst.file;
String funcDecl = inst.interfaceDeclBody;
// Rename the function declaration
String funcName = renameInterface(inst);
// Also rename the function definition if it's separated from the
// declaration
SpecConstruct definition = _semantics.interfaceName2DefineConstruct
.get(construct.name);
if (definition != null) {
String funcDefintionName = renameInterface(definition);
assert (funcDefintionName.equals(funcName));
}
// Generate new wrapper
/**
*
*
*/
breakCodeLines(newCode, funcDecl);
newCode.add("{");
// Generate interface sequence call
newCode.add(CodeVariables.UINT64 + " call_sequence_num = current(&"
+ CodeVariables.INTERFACE_CALL_SEQUENCE + ");");
// FIXME: Add Happens-before check here
newCode.add("}");
CodeAddition addition = new CodeAddition(lineNum, newCode);
if (!codeAdditions.containsKey(inst.file)) {
codeAdditions.put(inst.file, new ArrayList());
}
codeAdditions.get(inst.file).add(addition);
}
// Returns the function name that has been renamed and replace the old line
private String renameInterface(SpecConstruct inst)
throws InterfaceWrongFormatException {
String funcDecl = inst.interfaceDeclBody;
ArrayList content = contents.get(inst.file);
// Depending on "(" to find the function name, so it doesn't matter if
// there's any template
int begin = 0, end = funcDecl.indexOf('(');
if (end == -1) {
throw new InterfaceWrongFormatException(funcDecl
+ "\n has wrong format!");
}
end--;
while (end > 0) {
char ch = funcDecl.charAt(end);
if (ch == '_' || (ch >= 'a' && ch <= 'z')
|| (ch >= 'A' && ch <= 'Z') || (ch >= '0' && ch <= '9')) {
break;
}
end--;
}
begin = end;
while (begin > 0) {
char ch = funcDecl.charAt(begin);
if (ch == '_' || (ch >= 'a' && ch <= 'z')
|| (ch >= 'A' && ch <= 'Z') || (ch >= '0' && ch <= '9')) {
begin--;
continue;
}
break;
}
String funcName = funcDecl.substring(begin + 1, end + 1), newLine;
int lineBreakIdx = funcDecl.indexOf('\n');
int firstLineBreak = lineBreakIdx == -1 ? funcDecl.length()
: lineBreakIdx;
newLine = funcDecl.substring(0, begin + 1)
+ CodeVariables.SPEC_INTERFACE_WRAPPER + funcName
+ funcDecl.substring(end + 1, firstLineBreak);
// Be careful: lineNum - 1 -> index of content array
content.set(inst.endLineNum, newLine);
return funcName;
}
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) {
try {
interface2Code(inst);
} catch (InterfaceWrongFormatException e) {
e.printStackTrace();
}
} 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"),
new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
CodeGenerator gen = new CodeGenerator(srcFiles);
gen.generateCode();
}
}