ModelBuilder.java
/**
* This class process a front-end AST and builds
* the IR model.
*
* author: Yi Wei
*/
package edu.udel.cis.vsl.tass.front.minimp;
import java.util.Collection;
import java.util.HashMap;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Scanner;
import java.util.Stack;
import java.util.Vector;
import edu.udel.cis.vsl.tass.config.CompareConfiguration;
import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.config.VerifyConfiguration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTAbstractFunctionDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTArrayVariableDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTDeclarationIF;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTFormalParameterDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTFunctionDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTSimpleVariableDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTSystemFunctionDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTVariableDeclaration;
import edu.udel.cis.vsl.tass.front.minimp.ast.declaration.ASTVariableDeclaration.VariableCategory;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTArrayLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTArraySubscriptExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTAssignExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTBinaryExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTBoolLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTCharLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTConstantExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTEvaluatedFunction;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTExpressionIF;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTIfThenElseExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTIntegerLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTLhsExpressionIF;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTLiteralExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTNullLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTQuantifierExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTRealLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTSelfChangeExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTSizeofExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTSpecExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTStructLiteral;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTStructMemberRefExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTSystemVariable;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTTypeCast;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTUnaryExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTVariableExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTWildcardExpression;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTBinaryExpression.BinaryOperator;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTQuantifierExpression.QuantifierKind;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTSelfChangeExpression.SelfChangeOperator;
import edu.udel.cis.vsl.tass.front.minimp.ast.expression.ASTSystemVariable.SYS_VAR;
import edu.udel.cis.vsl.tass.front.minimp.ast.misc.AST;
import edu.udel.cis.vsl.tass.front.minimp.ast.misc.ASTFunction;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTAllocateStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTAssertStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTAssignmentStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTAssumeStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTCompoundStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTConditionStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTEmptyStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTExpressionStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTForStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTInvocationStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTReceiveStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTReturnStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTSelectStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTSelection;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTSendStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTStatementIF;
import edu.udel.cis.vsl.tass.front.minimp.ast.statement.ASTWhileStatement;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTArrayType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTBoolType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTCharType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTIntegerType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTPointerType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTRealType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTStructType;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTTypeIF;
import edu.udel.cis.vsl.tass.front.minimp.ast.type.ASTVoidType;
import edu.udel.cis.vsl.tass.front.minimp.lib.LibraryIF;
import edu.udel.cis.vsl.tass.front.minimp.lib.LibraryLoader;
import edu.udel.cis.vsl.tass.model.Models;
import edu.udel.cis.vsl.tass.model.IF.AbstractFunctionIF;
import edu.udel.cis.vsl.tass.model.IF.CollectiveAssertionIF;
import edu.udel.cis.vsl.tass.model.IF.FunctionIF;
import edu.udel.cis.vsl.tass.model.IF.ModelFactoryIF;
import edu.udel.cis.vsl.tass.model.IF.ModelIF;
import edu.udel.cis.vsl.tass.model.IF.ProcessIF;
import edu.udel.cis.vsl.tass.model.IF.SyntaxException;
import edu.udel.cis.vsl.tass.model.IF.SystemFunctionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.BoundExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.EvaluatedFunctionExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.LHSExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.LiteralExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ProcessReferenceExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.location.AllocateLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.AssertionLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.AssignmentLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.AssumeLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.BranchLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.ChoiceLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.ForLoopLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.InvocationLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.LoopLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.ReceiveLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.ReturnLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.SendLocationIF;
import edu.udel.cis.vsl.tass.model.IF.scope.BoundScopeIF;
import edu.udel.cis.vsl.tass.model.IF.scope.LocalScopeIF;
import edu.udel.cis.vsl.tass.model.IF.scope.ModelScopeIF;
import edu.udel.cis.vsl.tass.model.IF.scope.ProcessScopeIF;
import edu.udel.cis.vsl.tass.model.IF.scope.ScopeIF;
import edu.udel.cis.vsl.tass.model.IF.statement.AllocateStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.AssertionStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.AssignmentStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.AssumeStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.InvocationStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.NoopStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.ReceiveStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.ReturnStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.SendStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.StatementIF;
import edu.udel.cis.vsl.tass.model.IF.type.ArrayTypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.PointerTypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.RecordTypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.TypeIF;
import edu.udel.cis.vsl.tass.model.IF.variable.BoundVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.FormalVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.SharedVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.VariableIF;
import edu.udel.cis.vsl.tass.model.impl.CollectiveAssertion;
import edu.udel.cis.vsl.tass.util.Pair;
import edu.udel.cis.vsl.tass.util.Strings;
/*All front end classes will be imported, and other classes that have the same name with front end classes
* will be referred using full package name.*/
public class ModelBuilder {
/* Model factory */
private ModelFactoryIF factory = null;
private LibraryLoader libraryLoader = new LibraryLoader();
private Map<String, LibraryIF> functionLibraryMap = new HashMap<String, LibraryIF>();
/**
* List of function-decl pairs for which the function header has been added
* to the model, but the function body still needs to be added.
* */
private LinkedList<Pair<FunctionIF, ASTFunctionDeclaration>> functionWorkList = new LinkedList<Pair<FunctionIF, ASTFunctionDeclaration>>();
/* Stack to store the statement which do not have target location set */
private Stack<List<StatementIF>> lastStmt;
private Stack<LocationIF> unsetLoc;
// private boolean hasWildcardExpr = false;
private BranchLocationIF unsetBranchLoc = null;
private Stack<BranchLocationIF> unsetBranchLocStack = new Stack<BranchLocationIF>();
private ModelIF specModel;
private ModelIF implModel;
private Map<String, String> correspondingMap;
private Map<String, ASTExpressionIF> constantMap = new LinkedHashMap<String, ASTExpressionIF>();
private AST spec;
private AST impl;
private Map<ASTStatementIF, Integer> specSkewMap;
private Map<ASTStatementIF, Integer> implSkewMap;
private Stack<Integer> factorCount;
// private boolean loopLocSet = true;
private RunConfiguration configuration = null;
/** This maps the names of record types to the type in the model package */
private Map<String, TypeIF> typeTable;
/** Maps front end types to model types */
private Map<ASTTypeIF, TypeIF> typeMap;
private Map<String, CollectiveAssertionIF> collectiveAssertionMap;
private CollectiveAssertionIF lastCollectiveAssertion = null;
private ExpressionIF lastCollectiveAssertionExpression = null;
private ScopeIF systemScope;
public ModelBuilder(RunConfiguration configuration) {
assert configuration != null;
this.configuration = configuration;
this.factory = Models.newModelFactory(configuration);
this.correspondingMap = new LinkedHashMap<String, String>();
this.specSkewMap = new LinkedHashMap<ASTStatementIF, Integer>();
this.implSkewMap = new LinkedHashMap<ASTStatementIF, Integer>();
this.factorCount = new Stack<Integer>();
this.systemScope = factory.systemScope();
}
/* Build Model */
public ModelIF[] buildModel(AST[] ast) throws SyntaxException {
ModelScopeIF specScope, implScope;
CompareConfiguration configuration = (CompareConfiguration) this.configuration;
if (ast.length != 2) {
throw new SyntaxException("There must be exactly two programs.");
}
this.spec = ast[0];
this.impl = ast[1];
// Find the skew factors
if (configuration.useLoopTechnique()) {
findSkewFactors();
}
// Create two empty model with specific number of processes.
specModel = factory.newModel(configuration.specModelName(),
configuration.specNumProcs());
specScope = specModel.scope();
implModel = factory.newModel(configuration.implModelName(),
configuration.implNumProcs());
implScope = implModel.scope();
// Convert the ast into a model for each process
this.lastStmt = new Stack<List<StatementIF>>();
this.unsetLoc = new Stack<LocationIF>();
this.typeTable = new LinkedHashMap<String, TypeIF>();
this.typeMap = new LinkedHashMap<ASTTypeIF, TypeIF>();
this.collectiveAssertionMap = new LinkedHashMap<String, CollectiveAssertionIF>();
processAST(specModel, ast[0]);
this.lastStmt = new Stack<List<StatementIF>>();
this.unsetLoc = new Stack<LocationIF>();
this.typeTable = new LinkedHashMap<String, TypeIF>();
this.collectiveAssertionMap = new LinkedHashMap<String, CollectiveAssertionIF>();
for (CollectiveAssertionIF collectiveAssertion : specModel
.collectiveAssertions()) {
// Add joint assertions to the collective assertion map.
if (collectiveAssertion.isJointAssertion()) {
this.collectiveAssertionMap.put(collectiveAssertion
.identifier(), collectiveAssertion);
Collection<ProcessIF> processes = new Vector<ProcessIF>();
for (int i = 0; i < implModel.numProcs(); i++) {
processes.add(implModel.process(i));
}
((CollectiveAssertion) collectiveAssertion)
.addProcesses(processes);
}
}
processAST(implModel, ast[1]);
// Set the corresponding variables
if (this.correspondingMap.size() != 0) {
for (String specVar : this.correspondingMap.keySet()) {
if (specScope.variableWithName(specVar) != null) {
if (implScope.variableWithName(this.correspondingMap
.get(specVar)) == null) {
throw new SyntaxException("There is no variable named "
+ this.correspondingMap.get(specVar)
+ " in model " + implModel.name());
}
specModel.setCorrespondingVariable(specScope
.variableWithName(specVar), implScope
.variableWithName(this.correspondingMap
.get(specVar)));
implModel.setCorrespondingVariable(implScope
.variableWithName(this.correspondingMap
.get(specVar)), specScope
.variableWithName(specVar));
} else {
if (specScope.variableWithName(this.correspondingMap
.get(specVar)) == null) {
throw new SyntaxException("There is no variable named "
+ this.correspondingMap.get(specVar)
+ " in model " + specModel.name());
}
implModel.setCorrespondingVariable(implScope
.variableWithName(specVar), specScope
.variableWithName(this.correspondingMap
.get(specVar)));
specModel.setCorrespondingVariable(specScope
.variableWithName(this.correspondingMap
.get(specVar)), implScope
.variableWithName(specVar));
}
}
}
// Check any input/output variables that have no corresponding variables
for (VariableIF variable : specScope.variables()) {
SharedVariableIF var = (SharedVariableIF) variable;
String name = var.name();
if (var.isInput() || var.isOutput()) {
if (var.correspondingVariable() == null) {
if (implScope.variableWithName(name) != null) {
SharedVariableIF temp = implScope
.variableWithName(name);
if (var.isInput()) {
if (temp.isInput()) {
if (temp.correspondingVariable() == null) {
specModel.setCorrespondingVariable(var,
temp);
implModel.setCorrespondingVariable(temp,
var);
} else {
throw new SyntaxException(var,
"No corresponding variable in model "
+ implModel.name()
+ " with variable "
+ var.name() + " in model "
+ specModel.name());
}
} else {
throw new SyntaxException(var,
"The variable with name " + var.name()
+ " in model "
+ implModel.name()
+ " is not an input variable.");
}
} else if (var.isOutput()) {
if (temp.isOutput()) {
if (temp.correspondingVariable() == null) {
specModel.setCorrespondingVariable(var,
temp);
implModel.setCorrespondingVariable(temp,
var);
} else {
throw new SyntaxException(var,
"No corresponding variable in model "
+ implModel.name()
+ " with variable "
+ var.name() + " in model "
+ specModel.name());
}
} else {
throw new SyntaxException(var,
"The variable with name " + var.name()
+ " in model "
+ implModel.name()
+ " is not an output variable.");
}
}
} else {
throw new SyntaxException(var,
"No possible corresponding variables in model "
+ implModel.name() + " with variable "
+ var.name() + " exist.");
}
}
}
}
ModelIF[] result = new ModelIF[] { specModel, implModel };
return result;
}
public ModelIF buildModel(AST ast) throws SyntaxException {
ModelIF targetModel;
VerifyConfiguration configuration = (VerifyConfiguration) this.configuration;
assert configuration != null;
assert factory != null;
targetModel = factory.newModel(configuration.modelName(), configuration
.numProcs());
this.lastStmt = new Stack<List<StatementIF>>();
this.unsetLoc = new Stack<LocationIF>();
this.typeTable = new LinkedHashMap<String, TypeIF>();
this.typeMap = new LinkedHashMap<ASTTypeIF, TypeIF>();
this.collectiveAssertionMap = new LinkedHashMap<String, CollectiveAssertionIF>();
processAST(targetModel, ast);
return targetModel;
}
private void processAST(ModelIF model, AST ast) throws SyntaxException {
constantMap = ast.getConstantMap();
processLibraries(model, ast.getLibraryNames());
processGlobalVariables(model, ast.getGlobalVariableList());
processAbstractFunctions(ast.getAbstractFunctionList());
processFunctionHeaders(model, ast.getFunctionList());
processFunctionBodies();
setMainFunction(model);
model.complete();
}
private void processLibraries(ModelIF model, Collection<String> libraryNames)
throws SyntaxException {
for (String libraryName : libraryNames) {
LibraryIF library = libraryLoader.loadLibrary(null, libraryName);
for (String functionName : library.getFunctionNames()) {
functionLibraryMap.put(functionName, library);
}
}
}
/**
* Creates all abstract functions specified in the given list, defining them
* in the system-level scope.
*/
private void processAbstractFunctions(
List<ASTAbstractFunctionDeclaration> abstractFunctionList)
throws SyntaxException {
for (ASTAbstractFunctionDeclaration decl : abstractFunctionList) {
addAbstractFunction(decl);
}
}
private AbstractFunctionIF addAbstractFunction(
ASTAbstractFunctionDeclaration decl) throws SyntaxException {
String name = decl.getName().toString();
TypeIF returnType = processType(systemScope, decl.getType());
int numFormals = decl.numFormalParameter();
int continuity = decl.continuity();
FunctionIF oldFunction = systemScope.functionWithName(name);
if (oldFunction != null) {
if (!(oldFunction instanceof AbstractFunctionIF))
throw new SyntaxException("Redefinition of function " + name
+ ": original definition was concrete:\n"
+ oldFunction.getSource() + "\n" + decl.source());
// here should do more to check old is compatible with new,
// for now, just ignore
return (AbstractFunctionIF) oldFunction;
} else {
AbstractFunctionIF result = factory.newAbstractFunction(name,
returnType, numFormals);
result.setContinuity(continuity);
return result;
}
}
/* Process Variables */
/* Process global variables */
private void processGlobalVariables(ModelIF model,
List<ASTDeclarationIF> varList) throws SyntaxException {
TypeIF type = null;
String name = null;
VariableIF variable = null;
/* Shared variables belong to the model */
for (ASTDeclarationIF decl : varList) {
ScopeIF scope; // the scope of this decl
name = decl.getName().toString();
if (name.equals("PROC")) {
continue;
}
type = processType(model.scope(), decl.getType());
switch (((ASTVariableDeclaration) decl).getVariableCategory()) {
case INPUT:
scope = model.scope();
variable = model.newInputVariable(type, name);
if (((ASTVariableDeclaration) decl).getAssumption() != null) {
ExpressionIF assumption = processExpression(scope,
((ASTVariableDeclaration) decl).getAssumption());
model
.setAssumption((SharedVariableIF) variable,
assumption);
}
if (((ASTVariableDeclaration) decl).getCorrespondence() != null) {
this.correspondingMap.put(name,
((ASTVariableDeclaration) decl).getCorrespondence()
.toString());
}
break;
case OUTPUT:
variable = model.newOutputVariable(type, name);
if (((ASTVariableDeclaration) decl).getCorrespondence() != null) {
this.correspondingMap.put(name,
((ASTVariableDeclaration) decl).getCorrespondence()
.toString());
}
scope = model.scope();
break;
case SHARED:
scope = model.scope();
variable = model.newVariable(model.scope(), type, name);
if (((ASTVariableDeclaration) decl).hasInit()) {
ExpressionIF init = processExpression(scope,
((ASTSimpleVariableDeclaration) decl).getInit());
model.setInitializationExpression(variable, init);
}
break;
/* Process scope variable */
default:
for (int i = 0; i < model.numProcs(); i++) {
scope = model.process(i).scope();
variable = model.newVariable(scope, type, name);
/*
* If it is an array variable, we need to process the
* dimension informations.
*/
if (decl.getType() instanceof ASTArrayType) {
model.setArrayDimensions(variable, processDimensions(
scope, ((ASTArrayVariableDeclaration) decl)
.getDimensions()));
}
if (((ASTVariableDeclaration) decl).hasInit()) {
ExpressionIF init = processExpression(scope,
((ASTVariableDeclaration) decl).getInit());
model.setInitializationExpression(variable, init);
}
/* Set the source to store more information */
variable.setSource(decl.source());
}
continue;
}
/*
* If it is an array variable, we need to process the dimension
* informations.
*/
if (decl.getType() instanceof ASTArrayType)
model.setArrayDimensions(variable, processDimensions(scope,
((ASTArrayVariableDeclaration) decl).getDimensions()));
/* Set the source to store more information */
variable.setSource(decl.source());
}
}
/* Process Types */
private TypeIF processType(ScopeIF scope, ASTTypeIF type)
throws SyntaxException {
TypeIF result = typeMap.get(type);
if (result != null)
return result;
if (type instanceof ASTBoolType) {
result = this.factory.booleanType();
} else if (type instanceof ASTCharType) {
result = this.factory.characterType();
} else if (type instanceof ASTIntegerType) {
result = this.factory.integerType();
} else if (type instanceof ASTRealType) {
result = this.factory.rationalType();
} else if (type instanceof ASTVoidType) {
result = this.factory.voidType();
} else if (type instanceof ASTArrayType) {
result = processArrayType(scope, (ASTArrayType) type);
} else if (type instanceof ASTPointerType) {
ASTTypeIF astBaseType = ((ASTPointerType) type).getBaseType();
TypeIF modelBaseType = typeMap.get(astBaseType);
if (modelBaseType != null) {
result = this.factory.pointerType(modelBaseType);
} else {
// cyclic resolution...
result = this.factory.newPointerType();
typeMap.put(type, result);
modelBaseType = processType(scope, astBaseType);
result = this.factory.setBaseType((PointerTypeIF) result,
modelBaseType);
}
} else if (type instanceof ASTStructType) {
result = this.processStructType(scope, (ASTStructType) type);
} else {
throw new SyntaxException(type, "Unknown type: " + type);
}
typeMap.put(type, result);
return result;
}
/* Process array types */
private ArrayTypeIF processArrayType(ScopeIF scope, ASTArrayType type)
throws SyntaxException {
/* Recursive calls */
return this.factory.arrayType(processType(scope, type.getBaseType()));
}
/* Process dimensions */
private ExpressionIF[] processDimensions(ScopeIF scope,
ASTExpressionIF[] dimensions) throws SyntaxException {
List<ExpressionIF> result = new Vector<ExpressionIF>();
for (ASTExpressionIF dimension : dimensions) {
result.add(processExpression(scope, dimension));
}
/* Convert the list of expressions to an array of expressions */
ExpressionIF[] res = new ExpressionIF[result.size()];
for (int i = 0; i < result.size(); i++) {
res[i] = result.get(i);
}
return res;
}
/* Process struct type */
private RecordTypeIF processStructType(ScopeIF scope, ASTStructType type)
throws SyntaxException {
String structName = type.getName();
if (this.typeTable.containsKey(structName)) {
return (RecordTypeIF) (this.typeTable.get(structName));
} else {
int numFields = type.numFieldTypes();
// dimension information array
ExpressionIF[][] dimensionExpressions = new ExpressionIF[numFields][];
String[] fieldNames = new String[numFields];
TypeIF[] fieldTypes = new TypeIF[numFields];
int i = 0;
for (int j = 0; j < type.numFieldTypes(); j++) {
fieldNames[i] = type.getFieldName(j);
fieldTypes[i] = this.processType(scope, type.getFieldType(j));
dimensionExpressions[i] = this.findDimensionInfo(scope, type
.getFieldType(j));
i++;
}
RecordTypeIF result = (RecordTypeIF) typeMap.get(type);
if (result != null)
return result;
result = this.factory.recordType(structName, fieldNames,
fieldTypes, dimensionExpressions);
this.typeTable.put(structName, result);
// this.setPointerBase(model, pid, function, boundVariable, result);
return result;
}
}
/* Get the dimension information from a type */
// This method returns null when the type argument is not an array type. It
// should only be used in processing the field types of a struct type.
private ExpressionIF[] findDimensionInfo(ScopeIF scope, ASTTypeIF type)
throws SyntaxException {
ExpressionIF[] result = null;
if (type instanceof ASTArrayType) {
Vector<ExpressionIF> dimensions = new Vector<ExpressionIF>();
while (type instanceof ASTArrayType) {
dimensions.add(this.processExpression(scope,
((ASTArrayType) type).getLength()));
type = ((ASTArrayType) type).getBaseType();
}
result = new ExpressionIF[dimensions.size()];
dimensions.toArray(result);
}
return result;
}
/** Process Functions */
private void processFunctionHeaders(ModelIF model,
List<ASTFunctionDeclaration> functionList) throws SyntaxException {
for (int i = 0; i < model.numProcs(); i++) {
ProcessIF process = model.process(i);
ProcessScopeIF processScope = process.scope();
for (ASTFunctionDeclaration decl : functionList) {
FunctionIF function = addFunctionHeader(processScope, decl);
Pair<FunctionIF, ASTFunctionDeclaration> pair = new Pair<FunctionIF, ASTFunctionDeclaration>(
function, decl);
functionWorkList.add(pair);
}
}
}
/**
* Goes through functionWorkList and processes function bodies found there.
* Dynamic procedure: entries may be added to the list as they are being
* processes, because in processing a function body you may discover that a
* library function is called.
*/
private void processFunctionBodies() throws SyntaxException {
while (!functionWorkList.isEmpty()) {
Pair<FunctionIF, ASTFunctionDeclaration> pair = functionWorkList
.removeFirst();
FunctionIF function = pair.left;
ASTFunctionDeclaration decl = pair.right;
addFunctionBody(function, decl);
}
}
private FunctionIF addFunctionHeader(ProcessScopeIF scope,
ASTFunctionDeclaration decl) throws SyntaxException {
ModelIF model = scope.model();
/* Return type */
TypeIF type = processType(scope, decl.getType());
/* Function name */
String name = decl.getName().toString();
/* Number of formal parameters */
int numFormals = decl.numFormalParameter();
/* New empty function */
FunctionIF head = model.newFunction(scope.process(), name, type,
numFormals);
for (int m = 0; m < decl.numFormalParameter(); m++) {
processFormalParameter(head, decl.getFormalParameter(m));
}
return head;
}
private void addFunctionBody(FunctionIF function,
ASTFunctionDeclaration decl) throws SyntaxException {
ModelIF model = function.model();
LocationIF loc;
this.unsetLoc = new Stack<LocationIF>();
this.lastStmt = new Stack<List<StatementIF>>();
function.setSource(decl.source());
processFunctionBody(function, decl.getBody());
loc = model.newTerminalLocation(function.outermostScope());
this.unsetLoc.push(loc);
setTargetLocation(model);
}
/* Process formal parameter */
private void processFormalParameter(FunctionIF function,
ASTDeclarationIF decl) throws SyntaxException {
// Process parameter type
TypeIF type = processType(function.outermostScope(), decl.getType());
// parameter name
String name = decl.getName().toString();
// parameter index
int index = ((ASTFormalParameterDeclaration) decl).getIndex();
FormalVariableIF result = function.model().newFormalVariable(function,
type, name, index);
result.setSource(decl.source());
}
/* Process function body */
private void processFunctionBody(FunctionIF function, ASTFunction body)
throws SyntaxException {
processLocalVariables(function.outermostScope(), body
.getLocalVariableMap());
processStatementList(function, body.getStatementList());
}
/* Process local variables */
private void processLocalVariables(LocalScopeIF scope,
Map<String, ASTDeclarationIF> varMap) throws SyntaxException {
for (ASTDeclarationIF temp : varMap.values()) {
FunctionIF function = scope.function();
ModelIF model = function.model();
ASTVariableDeclaration decl = (ASTVariableDeclaration) temp;
VariableIF var = null;
TypeIF type = processType(scope, decl.getType()); /* variable type */
String name = decl.getName().toString(); /* variable name */
if (decl.getVariableCategory() == VariableCategory.FORMAL) {
// var = model.newFormalVariable(function, type, name,
// ((FormalParamDeclaration)decl).getIndex());
} else {
var = model.newVariable(function.outermostScope(), type, name);
if (((ASTVariableDeclaration) decl).hasInit()) {
ExpressionIF init = processExpression(scope,
((ASTVariableDeclaration) decl).getInit());
model.setInitializationExpression(var, init);
}
/* Set the dimensions */
if (decl.getType() instanceof ASTArrayType) {
model.setArrayDimensions(var, processDimensions(scope,
((ASTArrayVariableDeclaration) decl)
.getDimensions()));
}
// Set source
var.setSource(decl.source());
}
}
}
/* Process statement */
private void processStatementList(FunctionIF function,
List<ASTStatementIF> stmtList) throws SyntaxException {
ModelIF model = function.model();
LocalScopeIF scope = function.outermostScope();
for (int i = 0; i < stmtList.size(); i++) {
ASTStatementIF stmt = stmtList.get(i);
LocationIF loc = processStatement(scope, stmt);
if (i == 0) {
while (loc == null) {
// Allow a collective assertion at the beginning of the
// statement list
i++;
stmt = stmtList.get(i);
loc = processStatement(scope, stmt);
}
model.setStartLocation(function, loc);
}
// If the last statement in the list is a collective assertion
// throw a syntax exception
if (loc == null && i == stmtList.size() - 1) {
throw new SyntaxException(
lastCollectiveAssertion,
"A collective assertion cannot "
+ "be the last statement in the list. A possible fix is to add an empty statement (i.e. ;).");
}
/*
* // If the last statement in the list is a collective assertion //
* add a Noop so that there is a location for this collective //
* assertion to be associated to if (loc == null && i ==
* stmtList.size() - 1) { loc = processNoopStatement(model, pid,
* function, boundVariables, stmt); }
*/
if (lastCollectiveAssertion != null && loc != null) {
lastCollectiveAssertion.locations().add(loc);
model.addToLocation(loc, lastCollectiveAssertion,
lastCollectiveAssertionExpression);
lastCollectiveAssertion = null;
lastCollectiveAssertionExpression = null;
}
}
}
private LocationIF processStatement(LocalScopeIF scope,
ASTStatementIF statement) throws SyntaxException {
FunctionIF function = scope.function();
ProcessIF process = function.process();
if (statement instanceof ASTAssertStatement) {
if (((ASTAssertStatement) statement).isCollective()
|| ((ASTAssertStatement) statement).isInvariant()) {
// Ignore joint assertions during verification
if (((ASTAssertStatement) statement).isJoint()
&& configuration instanceof VerifyConfiguration) {
return null;
}
// TODO: We eventually want to remove this check. It's a way
// around some problems
// Ignore collective assertions during comparison
if (!((ASTAssertStatement) statement).isJoint()
&& configuration instanceof CompareConfiguration) {
return null;
}
// Process the assertion expression
ExpressionIF assertion = processExpression(scope,
((ASTAssertStatement) statement).getAssertion());
lastCollectiveAssertionExpression = assertion;
String identifier = ((ASTAssertStatement) statement).id()
.toString();
/*
* If this collective assertion is stored in the
* collectiveAssertionMap, use it unless it only involves one
* process
*/
if (collectiveAssertionMap.containsKey(identifier)
&& ((ASTAssertStatement) statement).isCollective()) {
lastCollectiveAssertion = collectiveAssertionMap
.get(identifier);
if (lastCollectiveAssertion.isJointAssertion()
^ ((ASTAssertStatement) statement).isJoint()) {
throw new SyntaxException(statement,
"Cannot have both joint and collective assertions with the same identifier");
}
} else {
ProcessIF[] processes;
ModelIF model = scope.model();
assert model != null;
if (((ASTAssertStatement) statement).isCollective()) {
// All processes are involved in a collective assertion
processes = new ProcessIF[model.numProcs()];
for (int i = 0; i < model.numProcs(); i++) {
processes[i] = model.process(i);
}
} else {
processes = new ProcessIF[1];
processes[0] = process;
}
CollectiveAssertionIF collectiveAssertion = model
.newCollectiveAssertion(statement,
processes,
// assertion,
identifier,
((ASTAssertStatement) statement)
.isInvariant(),
((ASTAssertStatement) statement).isJoint());
lastCollectiveAssertion = collectiveAssertion;
collectiveAssertionMap.put(identifier, collectiveAssertion);
}
// Collective assertions are associated with the next location
// so don't return a location
return null;
}
return processAssertStmt(scope, (ASTAssertStatement) statement);
} else if (statement instanceof ASTAssignmentStatement) {
return processAssignStmt(scope, (ASTAssignmentStatement) statement);
} else if (statement instanceof ASTAssumeStatement) {
return processAssumeStmt(scope, (ASTAssumeStatement) statement);
} else if (statement instanceof ASTCompoundStatement) {
return processCompoundStmt(scope, (ASTCompoundStatement) statement);
} else if (statement instanceof ASTConditionStatement) {
return processConditionStmt(scope,
(ASTConditionStatement) statement);
} else if (statement instanceof ASTSelectStatement) {
return processSelectStmt(scope, (ASTSelectStatement) statement);
} else if (statement instanceof ASTEmptyStatement) {
return processNoopStatement(scope, statement);
} else if (statement instanceof ASTInvocationStatement) {
return processInvocationStmt(scope,
(ASTInvocationStatement) statement);
} else if (statement instanceof ASTReceiveStatement) {
return processReceiveStmt(scope, (ASTReceiveStatement) statement);
} else if (statement instanceof ASTReturnStatement) {
return processReturnStmt(scope, (ASTReturnStatement) statement);
} else if (statement instanceof ASTSendStatement) {
return processSendStmt(scope, (ASTSendStatement) statement);
} else if (statement instanceof ASTForStatement) {
return processForStmt(scope, (ASTForStatement) statement);
} else if (statement instanceof ASTWhileStatement) {
return processWhileStmt(scope, (ASTWhileStatement) statement);
} else if (statement instanceof ASTExpressionStatement) {
return processExprStmt(scope, (ASTExpressionStatement) statement);
} else if (statement instanceof ASTAllocateStatement) {
return processAllocateStmt(scope, (ASTAllocateStatement) statement);
} else {
throw new SyntaxException(statement, "Unknown statement type: "
+ statement);
}
}
private LocationIF processNoopStatement(LocalScopeIF scope,
ASTStatementIF statement) throws SyntaxException {
ModelIF model = scope.model();
// Create a new location
LocationIF loc = model.newChoiceLocation(scope);
this.unsetLoc.push(loc);
// Set target location
setTargetLocation(model);
List<StatementIF> stmtList = new Vector<StatementIF>();
// Set source
loc.setSource(statement.getSource());
NoopStatementIF stmt = model.newChoiceStatement((ChoiceLocationIF) loc,
factory.booleanLiteralExpression(true));
// Set source
stmt.setSource(statement.getSource());
// push the unset statement to the stack
stmtList.add(stmt);
this.lastStmt.push(stmtList);
return loc;
}
// Allocate statement
private LocationIF processAllocateStmt(LocalScopeIF scope,
ASTAllocateStatement statement) throws SyntaxException {
ModelIF model = scope.model();
AllocateLocationIF loc = model.newAllocateLocation(scope);
List<StatementIF> stmtList = new Vector<StatementIF>();
this.unsetLoc.push(loc);
this.setTargetLocation(model);
// Process the buffer
ExpressionIF buffer = this.processExpression(scope, statement
.getBuffer());
if (!(buffer instanceof LHSExpressionIF)) {
throw new SyntaxException(buffer,
"The buffer of an allocate statement must be a left-value.");
}
// Process element type
TypeIF elementType = this
.processType(scope, statement.getElementType());
// Process element count
ExpressionIF elementCount = this.processExpression(scope, statement
.getElementCount());
// Create the statement
AllocateStatementIF stmt = model.newAllocateStatement(loc,
(LHSExpressionIF) buffer, elementType, elementCount);
stmt.setSource(statement.getSource());
stmtList.add(stmt);
this.lastStmt.push(stmtList);
return loc;
}
private LocationIF processAssertStmt(LocalScopeIF scope,
ASTAssertStatement statement) throws SyntaxException {
ModelIF model = scope.model();
// Create a new location
AssertionLocationIF loc = model.newAssertionLocation(scope);
this.unsetLoc.push(loc);
// Set target location
setTargetLocation(model);
List<StatementIF> stmtList = new Vector<StatementIF>();
// Set source
loc.setSource(statement.getSource());
// Process the assertion expression
ExpressionIF assertion = processExpression(scope, statement
.getAssertion());
String message = statement.getMessage();
AssertionStatementIF stmt = null;
if (!message.equals("")) {
stmt = model.newAssertionStatement(loc, assertion, message);
} else {
stmt = model.newAssertionStatement(loc, assertion);
}
// Set source
stmt.setSource(statement.getSource());
// push the unset statement to the stack
stmtList.add(stmt);
this.lastStmt.push(stmtList);
return loc;
}
private LocationIF processAssignStmt(LocalScopeIF scope,
ASTAssignmentStatement statement) throws SyntaxException {
ModelIF model = scope.model();
/* Create a new location */
AssignmentLocationIF loc = model.newAssignmentLocation(scope);
List<StatementIF> stmtList = new Vector<StatementIF>();
this.unsetLoc.push(loc);
// Set target location
setTargetLocation(model);
// Set source
loc.setSource(statement.getSource());
/* Process the left hand side expression */
ExpressionIF temp = processExpression(scope, statement.getLeft());
if (!(temp instanceof LHSExpressionIF)) {
throw new SyntaxException(
temp,
"Type error: the left hand side of an invocation statement must be a LHSExpressionIF.");
}
LHSExpressionIF lhs = (LHSExpressionIF) temp;
ExpressionIF rhs = processExpression(scope, statement.getRight());
AssignmentStatementIF stmt = model
.newAssignmentStatement(loc, lhs, rhs);
stmt.setSource(statement.getSource());
stmtList.add(stmt);
this.lastStmt.push(stmtList);
return loc;
}
private LocationIF processAssumeStmt(LocalScopeIF scope,
ASTAssumeStatement statement) throws SyntaxException {
ModelIF model = scope.model();
ExpressionIF assumption = processExpression(scope, statement
.getAssumption());
AssumeLocationIF loc = model.newAssumeLocation(scope);
List<StatementIF> stmtList = new Vector<StatementIF>();
this.unsetLoc.push(loc);
// Set target location
setTargetLocation(model);
// Set source
loc.setSource(statement.getSource());
AssumeStatementIF stmt = model.newAssumeStatement(loc, assumption);
stmt.setSource(statement.getSource());
stmtList.add(stmt);
this.lastStmt.push(stmtList);
return loc;
}
/* Process compound statement */
// TODO: start new scope?
private LocationIF processCompoundStmt(LocalScopeIF scope,
ASTCompoundStatement statement) throws SyntaxException {
ModelIF model = scope.model();
LocationIF loc = null, loc0 = null;
for (int i = 0; i < statement.getBody().size(); i++) {
if (i == 0) {
loc0 = loc = processStatement(scope, statement.getStatement(i));
} else {
loc = processStatement(scope, statement.getStatement(i));
}
/*
* If the last statement in the body is a collective assertion,
* throw an exception
*/
/*
* if (loc == null && i == statement.getBody().size() - 1) { throw
* new SyntaxException(lastCollectiveAssertion,
* "A collective assertion cannot " +
* "be the last statement in the list. A possible fix is to add an empty statement (i.e. ;)."
* ); }
*/
if (lastCollectiveAssertion != null && loc != null) {
lastCollectiveAssertion.locations().add(loc);
model.addToLocation(loc, lastCollectiveAssertion,
lastCollectiveAssertionExpression);
lastCollectiveAssertion = null;
lastCollectiveAssertionExpression = null;
}
}
return loc0;
}
/* If..then..else statement */
private LocationIF processConditionStmt(LocalScopeIF scope,
ASTConditionStatement statement) throws SyntaxException {
ModelIF model = scope.model();
int before = 0;
int after = 0;
ExpressionIF condition = processExpression(scope, statement
.getPredicate());
/* Create a new branch location. It has two statements outgoing it. */
BranchLocationIF loc = model.newBranchLocation(scope, condition);
LocationIF tempLoc = null;
this.unsetLoc.push(loc);
setTargetLocation(model);
// Set source
loc.setSource(statement.getSource());
/* Create Noop statements for the true branch and the false branch */
NoopStatementIF trueBranch = model.newTrueBranchStatement(loc);
NoopStatementIF falseBranch = model.newFalseBranchStatement(loc);
// Set source
trueBranch.setSource(statement.getSource());
falseBranch.setSource(statement.getSource());
/* Process true branch */
List<StatementIF> trueBranchList = new Vector<StatementIF>();
trueBranchList.add(trueBranch);
this.lastStmt.push(trueBranchList);
before = this.lastStmt.size();
tempLoc = processStatement(scope, statement.getTrueBranch());
if (lastCollectiveAssertion != null) {
throw new SyntaxException(
lastCollectiveAssertion,
"A collective assertion cannot "
+ "be the last statement in the list. A possible fix is to add an empty statement (i.e. ;).");
/*
* lastCollectiveAssertion.locations().add(tempLoc);
* model.addToLocation(tempLoc, lastCollectiveAssertion,
* lastCollectiveAssertionExpression); lastCollectiveAssertion =
* null; lastCollectiveAssertionExpression = null;
*/
}
after = this.lastStmt.size();
List<StatementIF> branchExitList = new Vector<StatementIF>();
for (int i = 0; i < after - before + 1; i++) {
for (StatementIF stmt : this.lastStmt.pop()) {
branchExitList.add(stmt);
}
}
List<StatementIF> falseBranchList = new Vector<StatementIF>();
falseBranchList.add(falseBranch);
before = this.lastStmt.size();
this.lastStmt.push(falseBranchList);
if (statement.getFalseBranch() != null) {
/* Process false branch */
tempLoc = processStatement(scope, statement.getFalseBranch());
if (lastCollectiveAssertion != null && tempLoc != null) {
lastCollectiveAssertion.locations().add(tempLoc);
model.addToLocation(tempLoc, lastCollectiveAssertion,
lastCollectiveAssertionExpression);
lastCollectiveAssertion = null;
lastCollectiveAssertionExpression = null;
}
}
after = this.lastStmt.size();
if (after != before) {
for (int i = 0; i < after - before; i++) {
for (StatementIF stmt : this.lastStmt.pop()) {
branchExitList.add(stmt);
}
}
}
this.lastStmt.push(branchExitList);
if (this.unsetBranchLoc == null) {
this.unsetBranchLoc = loc;
} else {
this.unsetBranchLocStack.push(loc);
}
return loc;
}
private LocationIF processSelectStmt(LocalScopeIF scope,
ASTSelectStatement statement) throws SyntaxException {
ModelIF model = scope.model();
ChoiceLocationIF loc = model.newChoiceLocation(scope);
LocationIF tempLoc = null;
this.unsetLoc.push(loc);
setTargetLocation(model);
// Set source
loc.setSource(statement.getSource());
// Set target location
this.unsetLoc.push(loc);
this.setTargetLocation(model);
List<StatementIF> lastStmtList = new Vector<StatementIF>();
/* Process the guards */
for (int i = 0; i < statement.getSelectionCount(); i++) {
ASTSelection sel = statement.getSelection(i);
ExpressionIF guard = processExpression(scope, sel.getPredicate());
NoopStatementIF stmt = model.newChoiceStatement(loc, guard);
// Set source
stmt.setSource(sel.source());
List<StatementIF> stmtList = new Vector<StatementIF>();
stmtList.add(stmt);
this.lastStmt.push(stmtList);
tempLoc = processStatement(scope, sel.getStatement());
if (lastCollectiveAssertion != null && tempLoc != null) {
lastCollectiveAssertion.locations().add(tempLoc);
model.addToLocation(tempLoc, lastCollectiveAssertion,
lastCollectiveAssertionExpression);
lastCollectiveAssertion = null;
lastCollectiveAssertionExpression = null;
} else if (lastCollectiveAssertion != null) {
// collective assertion with no subsequent location, so throw
// exception
throw new SyntaxException(
lastCollectiveAssertion,
"A collective assertion cannot "
+ "be the last statement in the list. A possible fix is to add an empty statement (i.e. ;).");
}
// Exit location.
List<StatementIF> temp = this.lastStmt.pop();
for (int j = 0; j < temp.size(); j++) {
lastStmtList.add(temp.get(j));
}
}
this.lastStmt.push(lastStmtList);
return loc;
}
/**
* Adds system function to model. A system function has no body. It may have
* an optional guard expression. It is defined in a library. There should be
* a class which defines its semantics by defining the state change
* resulting from executing the function.
*/
private SystemFunctionIF addSystemFunction(ProcessScopeIF scope,
LibraryIF library, ASTSystemFunctionDeclaration decl)
throws SyntaxException {
int numFormals = decl.numFormalParameter();
TypeIF type = processType(scope, decl.getType());
ModelIF model = scope.model();
String shortLibraryName = Strings.rootName(library.name());
SystemFunctionIF function = model.newSystemFunction(shortLibraryName,
scope.process(), decl.getName().toString(), type, numFormals);
LocalScopeIF localScope = function.outermostScope();
ASTExpressionIF astGuard = decl.getGuard();
for (int i = 0; i < numFormals; i++) {
ASTDeclarationIF formalDecl = decl.getFormalParameter(i);
TypeIF formalType = processType(localScope, formalDecl.getType());
model.newFormalVariable(function, formalType, formalDecl.getName()
.toString(), i);
}
if (astGuard != null) {
ExpressionIF guard = processExpression(localScope, astGuard);
model.setGuard(function, guard);
}
return function;
}
private LocationIF processInvocationStmt(LocalScopeIF localScope,
ASTInvocationStatement statement) throws SyntaxException {
ASTLhsExpressionIF astLhs = statement.getLeft();
LHSExpressionIF lhs = null;
String name = statement.getFunctionName();
FunctionIF callee = localScope.getLexicalFunction(name);
List<ASTExpressionIF> actualList = statement.getActualParameterList();
ModelIF model = localScope.model();
FunctionIF function = localScope.function();
ProcessIF process = function.process();
ProcessScopeIF processScope = process.scope();
List<StatementIF> stmtList = new Vector<StatementIF>();
/* Figure out left-hand side, if non-null */
if (astLhs != null) {
ExpressionIF temp = processExpression(localScope, astLhs);
if (!(temp instanceof LHSExpressionIF))
throw new SyntaxException(
temp,
"The left hand side of an invocation statement must be a left-hand side expression");
lhs = (LHSExpressionIF) temp;
}
/* If the callee not found, the function had better be from a library */
if (callee == null) {
ASTFunctionDeclaration decl;
LibraryIF library = functionLibraryMap.get(name);
if (library == null)
throw new SyntaxException(statement, "Unknown function: "
+ name);
decl = library.getFunction(name);
if (decl instanceof ASTAbstractFunctionDeclaration) {
callee = addAbstractFunction((ASTAbstractFunctionDeclaration) decl);
} else if (decl instanceof ASTSystemFunctionDeclaration) {
callee = addSystemFunction(processScope, library,
(ASTSystemFunctionDeclaration) decl);
} else {
// a concrete library function (i.e., with body)
callee = addFunctionHeader(processScope, decl);
functionWorkList
.add(new Pair<FunctionIF, ASTFunctionDeclaration>(
callee, decl));
}
}
assert callee != null;
if (callee instanceof AbstractFunctionIF) {
// should have form lhs=f(x): this is actually an assignment
// statement
EvaluatedFunctionExpressionIF rhs = evaluatedFunction(localScope,
(AbstractFunctionIF) callee, actualList);
AssignmentLocationIF loc = model.newAssignmentLocation(localScope);
AssignmentStatementIF stmt;
if (lhs == null)
throw new SyntaxException(lhs,
"Illegal use of abstract function");
this.unsetLoc.push(loc);
setTargetLocation(model);
loc.setSource(statement.getSource());
stmt = model.newAssignmentStatement(loc, lhs, rhs);
stmt.setSource(statement.getSource());
stmtList.add(stmt);
this.lastStmt.push(stmtList);
return loc;
} else { // system function or concrete function
List<ExpressionIF> paramList = new Vector<ExpressionIF>();
InvocationLocationIF loc = model.newInvocationLocation(localScope);
InvocationStatementIF stmt;
/* convert actual parameters */
for (int i = 0; i < actualList.size(); i++)
paramList.add(processExpression(localScope, actualList.get(i)));
this.unsetLoc.push(loc);
setTargetLocation(model);
loc.setSource(statement.getSource());
stmt = model.newInvocationStatement(loc, lhs, callee, paramList);
stmt.setSource(statement.getSource());
stmtList.add(stmt);
this.lastStmt.push(stmtList);
return loc;
}
}
private LocationIF processReceiveStmt(LocalScopeIF scope,
ASTReceiveStatement statement) throws SyntaxException {
ModelIF model = scope.model();
ReceiveLocationIF loc = null;
ExpressionIF source = null;
ExpressionIF tag = null;
LHSExpressionIF sizeExpression = null;
List<StatementIF> stmtList = new Vector<StatementIF>();
LHSExpressionIF buffer = (LHSExpressionIF) processExpression(scope,
statement.getRecvBody());
// Process tag expression
if (statement.getTag() instanceof ASTWildcardExpression) {
// any tag
ExpressionIF temp = processExpression(scope,
((ASTWildcardExpression) (statement.getTag())).getBody());
if (!(temp instanceof LHSExpressionIF)) {
throw new SyntaxException(temp,
"The expression in any tag must be a left-hand side expression.");
}
tag = factory.anyExpression((LHSExpressionIF) temp);
} else {
tag = processExpression(scope, statement.getTag());
}
// Process size
if (statement.getSize() != null) {
sizeExpression = (LHSExpressionIF) processExpression(scope,
statement.getSize());
}
// Process source expression
if (statement.getRecvSource() instanceof ASTWildcardExpression) {
// Any source
loc = model.newAnySourceReceiveLocation(scope);
this.unsetLoc.push(loc);
setTargetLocation(model);
// Process the argument in any() expression
ASTExpressionIF temp = ((ASTWildcardExpression) (statement
.getRecvSource())).getBody();
ExpressionIF anySourceArgument = null;
if (temp != null) {
anySourceArgument = processExpression(scope, temp);
}
if (!(anySourceArgument instanceof LHSExpressionIF)) {
throw new SyntaxException(anySourceArgument,
"The argument of an any expression must be a left-hand side expression.");
}
for (int i = 0; i < model.numProcs(); i++) {
ExpressionIF srcArg = this.factory.literalExpression(String
.valueOf(i));
StatementIF recvStmt = null;
if (sizeExpression == null) {
recvStmt = model.newReceiveStatement(loc, buffer, srcArg,
tag);
} else {
recvStmt = model.newReceiveStatement(loc, buffer, srcArg,
tag, sizeExpression);
}
AssignmentLocationIF assignLoc = model
.newAssignmentLocation(scope);
model.setTargetLocation(recvStmt, assignLoc);
StatementIF assignStmt = model.newAssignmentStatement(
assignLoc, (LHSExpressionIF) anySourceArgument, srcArg);
assignLoc.setSource(statement.getSource());
assignStmt.setSource(statement.getSource());
recvStmt.setSource(statement.getSource());
stmtList.add(assignStmt);
}
} else {
// Single source
loc = model.newStandardReceiveLocation(scope);
this.unsetLoc.push(loc);
setTargetLocation(model);
source = processExpression(scope, statement.getRecvSource());
ReceiveStatementIF stmt = null;
if (sizeExpression == null) {
stmt = model.newReceiveStatement(loc, buffer, source, tag);
} else {
stmt = model.newReceiveStatement(loc, buffer, source, tag,
sizeExpression);
}
// Set source
stmt.setSource(statement.getSource());
stmtList.add(stmt);
}
this.lastStmt.push(stmtList);
// Set source
loc.setSource(statement.getSource());
return loc;
}
private LocationIF processReturnStmt(LocalScopeIF scope,
ASTReturnStatement statement) throws SyntaxException {
ModelIF model = scope.model();
ExpressionIF result = null;
List<StatementIF> stmtList = new Vector<StatementIF>();
ReturnLocationIF loc = model.newReturnLocation(scope);
this.unsetLoc.push(loc);
// Set target location
setTargetLocation(model);
if (statement.getReturnBody() != null) {
result = processExpression(scope, statement.getReturnBody());
}
ReturnStatementIF stmt = model.newReturnStatement(loc, result);
// Set source
stmt.setSource(statement.getSource());
stmtList.add(stmt);
this.lastStmt.push(stmtList);
return loc;
}
private LocationIF processSendStmt(LocalScopeIF scope,
ASTSendStatement statement) throws SyntaxException {
ModelIF model = scope.model();
SendLocationIF loc = model.newSendLocation(scope);
List<StatementIF> stmtList = new Vector<StatementIF>();
this.unsetLoc.push(loc);
setTargetLocation(model);
// Set source
loc.setSource(statement.getSource());
LHSExpressionIF buffer = (LHSExpressionIF) processExpression(scope,
statement.getSendBody());
ExpressionIF dest = processExpression(scope, statement.getDestination());
ExpressionIF tag = processExpression(scope, statement.getTag());
SendStatementIF stmt = model.newSendStatement(loc, buffer, dest, tag);
// Set source
stmt.setSource(statement.getSource());
stmtList.add(stmt);
this.lastStmt.push(stmtList);
return loc;
}
private LocationIF processWhileStmt(LocalScopeIF scope,
ASTWhileStatement statement) throws SyntaxException {
ModelIF model = scope.model();
/* Process predicate */
int loopCount = 1;
CollectiveAssertionIF ca = null;
ExpressionIF caExpression = null;
if (lastCollectiveAssertion != null) {
ca = lastCollectiveAssertion;
caExpression = lastCollectiveAssertionExpression;
lastCollectiveAssertion = null;
lastCollectiveAssertionExpression = null;
}
List<StatementIF> falseBranchList = new Vector<StatementIF>();
if (configuration.useLoopTechnique()) {
if (this.specSkewMap.containsKey(statement)) {
loopCount = this.specSkewMap.get(statement).intValue();
} else if (this.implSkewMap.containsKey(statement)) {
loopCount = this.implSkewMap.get(statement).intValue();
}
}
LocationIF firstLoc = null;
ExpressionIF condition = processExpression(scope, statement
.getPredicate());
for (int i = 0; i < loopCount; i++) {
List<StatementIF> trueBranchList = new Vector<StatementIF>();
LocationIF loc = null, tempLoc = null;
NoopStatementIF trueBranch = null;
NoopStatementIF falseBranch = null;
if (i == 0) {
loc = model.newLoopLocation(scope, condition);
firstLoc = loc;
if (ca != null) {
model.addToLocation(firstLoc, ca, caExpression);
}
// Create two statements to represent the true and the false
// branch
trueBranch = model
.newLoopTrueBranchStatement((LoopLocationIF) loc);
falseBranch = model
.newLoopFalseBranchStatement((LoopLocationIF) loc);
} else {
loc = model.newBranchLocation(scope, condition);
trueBranch = model
.newTrueBranchStatement((BranchLocationIF) loc);
falseBranch = model
.newFalseBranchStatement((BranchLocationIF) loc);
}
trueBranch.setSource(statement.getSource());
falseBranch.setSource(statement.getSource());
this.unsetLoc.push(loc);
setTargetLocation(model);
// Set source
loc.setSource(statement.getSource());
if (i == 0) {
/* Set the label of the invariant */
if (statement.getInvariant() != null) {
model.setLabel(loc, statement.getInvariant().getLabel());
/* Process loop invariants */
if (statement.getInvariant().getInvariant() != null) {
ExpressionIF expr = processExpression(scope, statement
.getInvariant().getInvariant());
loc.putAnnotation(expr.toString(), expr);
}
}
trueBranchList.add(trueBranch);
falseBranchList.add(falseBranch);
this.lastStmt.push(falseBranchList);
this.lastStmt.push(trueBranchList);
/* Process Loop body */
tempLoc = processStatement(scope, statement.getLoopBody());
// If the loop has an empty body except for a collective
// assertion, throw an exception
if (tempLoc == null && lastCollectiveAssertion != null) {
/*
* tempLoc = processNoopStatement(model, pid, function,
* boundVariables, statement.getLoopBody());
* lastCollectiveAssertion.locations().add(loc);
* model.addToLocation(loc, lastCollectiveAssertion,
* lastCollectiveAssertionExpression);
* lastCollectiveAssertion = null;
* lastCollectiveAssertionExpression = null;
*/
throw new SyntaxException(
lastCollectiveAssertion,
"A collective assertion cannot "
+ "be the last statement in the list. A possible fix is to add an empty statement (i.e. ;).");
}
// Set the target location of the last statement in the loop
// body to
// the loop location
this.unsetLoc.push(loc);
}
// Basically we are processing an if-then statement.
else {
int before = 0;
int after = 0;
trueBranchList.add(trueBranch);
this.lastStmt.push(trueBranchList);
before = this.lastStmt.size();
tempLoc = processStatement(scope, statement.getLoopBody());
after = this.lastStmt.size();
List<StatementIF> branchExitList = new Vector<StatementIF>();
for (int j = 0; j < after - before + 1; j++) {
for (StatementIF stmt : this.lastStmt.pop()) {
branchExitList.add(stmt);
}
}
falseBranchList.add(falseBranch);
this.lastStmt.push(falseBranchList);
this.lastStmt.push(branchExitList);
if (this.unsetBranchLoc == null) {
this.unsetBranchLoc = (BranchLocationIF) loc;
} else {
this.unsetBranchLocStack.push((BranchLocationIF) loc);
}
if (lastCollectiveAssertion != null && tempLoc != null) {
lastCollectiveAssertion.locations().add(tempLoc);
model.addToLocation(tempLoc, lastCollectiveAssertion,
lastCollectiveAssertionExpression);
lastCollectiveAssertion = null;
lastCollectiveAssertionExpression = null;
}
}
if (i == loopCount - 1) {
this.unsetLoc.push(firstLoc);
this.setTargetLocation(model);
}
}
if (loopCount > 1) {
this.factorCount.push(new Integer(loopCount));
// this.loopLocSet = false;
}
return firstLoc;
}
private LocationIF processForStmt(LocalScopeIF scope,
ASTForStatement statement) throws SyntaxException {
ModelIF model = scope.model();
LocationIF result = null; // unused: loc = null;
if (statement.getInitializer() != null) {
List<StatementIF> initStmtList = new Vector<StatementIF>();
if (statement.getInitializer() instanceof ASTAssignExpression) {
AssignmentLocationIF initLoc = model
.newAssignmentLocation(scope);
// if (lastCollectiveAssertion != null && initLoc != null) {
// lastCollectiveAssertion.locations().add(initLoc);
// model.addToLocation(initLoc, lastCollectiveAssertion,
// lastCollectiveAssertionExpression);
// lastCollectiveAssertion = null;
// lastCollectiveAssertionExpression = null;
// }
this.unsetLoc.push(initLoc);
this.setTargetLocation(model);
LHSExpressionIF lhs = (LHSExpressionIF) processExpression(
scope, ((ASTAssignExpression) (statement
.getInitializer())).getLeft());
ExpressionIF rhs = processExpression(scope,
((ASTAssignExpression) (statement.getInitializer()))
.getRight());
StatementIF initStmt = model.newAssignmentStatement(initLoc,
lhs, rhs);
initStmt.setSource(statement.getInitializer().getSource());
initStmtList.add(initStmt);
this.lastStmt.push(initStmtList);
result = initLoc;
}
}
ExpressionIF predicate = null;
if (statement.getPredicate() != null) {
if (!(statement.getPredicate().getType() instanceof ASTBoolType)) {
throw new SyntaxException(statement,
"The predicate of the for statement must have boolean type instead of "
+ statement.getPredicate().getType());
}
predicate = processExpression(scope, statement.getPredicate());
} else {
predicate = this.factory.literalExpression(String.valueOf(true));
}
ForLoopLocationIF loopLoc = model.newForLoopLocation(scope, predicate);
// Note: We originally associated collective assertions at for loops
// with the init
// and later changed it to be associated with the loop location
if (lastCollectiveAssertion != null && loopLoc != null) {
lastCollectiveAssertion.locations().add(loopLoc);
model.addToLocation(loopLoc, lastCollectiveAssertion,
lastCollectiveAssertionExpression);
lastCollectiveAssertion = null;
lastCollectiveAssertionExpression = null;
}
if (result == null) {
result = loopLoc;
} else {
loopLoc.setInit(result);
}
List<StatementIF> trueBranchList = new Vector<StatementIF>();
List<StatementIF> falseBranchList = new Vector<StatementIF>();
NoopStatementIF trueBranch = model.newLoopTrueBranchStatement(loopLoc);
NoopStatementIF falseBranch = model
.newLoopFalseBranchStatement(loopLoc);
trueBranch.setSource(statement.getSource());
falseBranch.setSource(statement.getSource());
this.unsetLoc.push(loopLoc);
this.setTargetLocation(model);
trueBranchList.add(trueBranch);
falseBranchList.add(falseBranch);
this.lastStmt.push(falseBranchList);
this.lastStmt.push(trueBranchList);
// unused: loc =
processStatement(scope, statement.getBody());
if (statement.getUpdate() != null) {
LocationIF update = processStatement(scope,
new ASTExpressionStatement(statement.getUpdate()));
loopLoc.setUpdate(update);
if (lastCollectiveAssertion != null && update != null) {
lastCollectiveAssertion.locations().add(update);
model.addToLocation(update, lastCollectiveAssertion,
lastCollectiveAssertionExpression);
lastCollectiveAssertion = null;
lastCollectiveAssertionExpression = null;
}
} else if (lastCollectiveAssertion != null) {
// no update, so throw exception
throw new SyntaxException(
lastCollectiveAssertion,
"A collective assertion cannot "
+ "be the last statement in the list. A possible fix is to add an empty statement (i.e. ;).");
/*
* loc = processNoopStatement(scope, new ASTEmptyStatement());
* lastCollectiveAssertion.locations().add(loc);
* model.addToLocation(loc, lastCollectiveAssertion,
* lastCollectiveAssertionExpression); lastCollectiveAssertion =
* null; lastCollectiveAssertionExpression = null;
*/
}
this.unsetLoc.push(loopLoc);
this.setTargetLocation(model);
return result;
}
private LocationIF processExprStmt(LocalScopeIF scope,
ASTExpressionStatement statement) throws SyntaxException {
ASTExpressionIF body = statement.getBody();
ASTAssignmentStatement stmt = null;
LocationIF loc = null;
if (body instanceof ASTAssignExpression) {
stmt = new ASTAssignmentStatement((ASTAssignExpression) body);
stmt.setSource(body.getSource());
loc = this.processAssignStmt(scope, stmt);
} else if (body instanceof ASTSelfChangeExpression) {
ASTExpressionIF temp = ((ASTSelfChangeExpression) body).getBody();
ASTAssignExpression newBody = null;
if (((ASTSelfChangeExpression) body).getOperator() == SelfChangeOperator.INCREMENT) {
newBody = new ASTAssignExpression(
(ASTLhsExpressionIF) temp,
new ASTBinaryExpression(
BinaryOperator.PLUS,
temp,
new ASTIntegerLiteral(new ASTIntegerType(), "1")));
} else {
newBody = new ASTAssignExpression(
(ASTLhsExpressionIF) temp,
new ASTBinaryExpression(
BinaryOperator.SUB,
temp,
new ASTIntegerLiteral(new ASTIntegerType(), "1")));
}
newBody.setSource(body.getSource());
stmt = new ASTAssignmentStatement((ASTAssignExpression) newBody);
stmt.setSource(newBody.getSource());
loc = this.processAssignStmt(scope, stmt);
}
return loc;
}
/* Process expressions */
private ExpressionIF processExpression(ScopeIF scope, ASTExpressionIF expr)
throws SyntaxException {
if (expr instanceof ASTArraySubscriptExpression) {
return processArraySubExpr(scope,
(ASTArraySubscriptExpression) expr);
} else if (expr instanceof ASTBinaryExpression) {
return processBinaryExpr(scope, (ASTBinaryExpression) expr);
} else if (expr instanceof ASTIfThenElseExpression) {
return processIfThenElseExpr(scope, (ASTIfThenElseExpression) expr);
} else if (expr instanceof ASTConstantExpression) {
return processConstantExpression(scope,
(ASTConstantExpression) expr);
} else if (expr instanceof ASTLiteralExpression) {
return processLiteralExpr(scope, (ASTLiteralExpression) expr);
} else if (expr instanceof ASTUnaryExpression) {
return processUnaryExpr(scope, (ASTUnaryExpression) expr);
} else if (expr instanceof ASTVariableExpression) {
return processVariableExpr(scope, (ASTVariableExpression) expr);
} else if (expr instanceof ASTSpecExpression) {
return processSpecExpr(scope, (ASTSpecExpression) expr);
} else if (expr instanceof ASTStructMemberRefExpression) {
return processStructMemberRefExpr(scope,
(ASTStructMemberRefExpression) expr);
} else if (expr instanceof ASTSizeofExpression) {
return processSizeofExpr(scope, (ASTSizeofExpression) expr);
} else if (expr instanceof ASTEvaluatedFunction) {
return processEvaluatedFunction(scope, (ASTEvaluatedFunction) expr);
} else if (expr instanceof ASTTypeCast) {
return processTypeCast(scope, (ASTTypeCast) expr);
} else if (expr instanceof ASTQuantifierExpression) {
return processQuantifier(scope, (ASTQuantifierExpression) expr);
}
/*
* else if(expr instanceof SelfChangeExpression) { return
* processSelfchangeExpr(scope, (SelfChangeExpression)expr); }
*/
else {
throw new SyntaxException(expr, "Unknown expression type: "
+ expr.getClass().getSimpleName());
}
}
private ExpressionIF processConstantExpression(ScopeIF scope,
ASTConstantExpression constant) throws SyntaxException {
String name = constant.name();
ExpressionIF result = null;
ASTExpressionIF literal = constant.literal();
/* boolean constant */
if (literal instanceof ASTBoolLiteral) {
result = this.factory.namedLiteralExpression(
((ASTBoolLiteral) literal).toString(), name);
} else if (literal instanceof ASTUnaryExpression) {
ASTUnaryExpression unary = (ASTUnaryExpression) literal;
if (unary.getOperator() != ASTUnaryExpression.UnaryOperator.MINUS)
throw new SyntaxException(
unary,
"Only negative numbers are allowed as unary expressions when dealing with constants.");
if (unary.getOperand() instanceof ASTIntegerLiteral) {
result = this.factory.namedIntegerLiteralExpression("-"
+ ((ASTIntegerLiteral) unary.getOperand()).getValue(),
name);
} else if (unary.getOperand() instanceof ASTRealLiteral) {
result = this.factory.namedRealLiteralExpression("-"
+ ((ASTRealLiteral) unary.getOperand()).getValue(),
name);
} else
throw new SyntaxException(unary,
"Only integers or reals can be used as a negative constant.");
}
/* integer constant */
else if (literal instanceof ASTIntegerLiteral) {
result = this.factory.namedIntegerLiteralExpression(
((ASTIntegerLiteral) literal).getValue(), name);
}
/* rational constant */
else if (literal instanceof ASTRealLiteral) {
result = this.factory.namedRealLiteralExpression(
((ASTRealLiteral) literal).getValue(), name);
} else if (literal instanceof ASTNullLiteral) {
result = this.factory.namedNullExpression(name);
}
/* char constant */
else if (literal instanceof ASTCharLiteral) {
result = this.factory.namedCharacterLiteralExpression(
((ASTCharLiteral) literal).getValue(), name);
} else if (literal instanceof ASTArrayLiteral) {
LiteralExpressionIF[] literalArray = new LiteralExpressionIF[((ASTArrayLiteral) literal)
.numLiteral()];
for (int i = 0; i < literalArray.length; i++) {
ASTExpressionIF temp = ((ASTArrayLiteral) constant.literal())
.getLiteral(i);
if (temp != null) {
literalArray[i] = (LiteralExpressionIF) (this
.processLiteralExpr(scope,
(ASTLiteralExpression) temp));
} else {
literalArray[i] = null;
}
}
result = this.factory.namedArrayLiteralExpression(
(ArrayTypeIF) literal, literalArray, name);
} else if (literal instanceof ASTStructLiteral) {
LiteralExpressionIF[] literalArray = new LiteralExpressionIF[((ASTStructLiteral) literal)
.numValues()];
for (int i = 0; i < literalArray.length; i++) {
ASTExpressionIF temp = ((ASTStructLiteral) constant.literal())
.getFieldValue(i);
if (temp != null) {
literalArray[i] = (LiteralExpressionIF) (this
.processLiteralExpr(scope,
(ASTLiteralExpression) temp));
} else {
literalArray[i] = null;
}
}
result = this.factory.namedRecordLiteralExpression(
(RecordTypeIF) literal, literalArray, name);
} else if (constantMap.containsKey(name)) {
result = processExpression(scope,
((ASTConstantExpression) constantMap.get(name)).literal());
} else {
throw new SyntaxException(literal, "Unknown constant: " + name);
}
// Set source
result.setSource(constant.getSource());
return result;
}
private BoundExpressionIF processQuantifier(ScopeIF parentScope,
ASTQuantifierExpression expr) throws SyntaxException {
QuantifierKind kind;
BoundVariableIF variable;
ExpressionIF restriction, expression;
BoundExpressionIF result;
BoundScopeIF boundScope;
TypeIF type;
boundScope = factory.newBoundScope(parentScope);
type = processType(parentScope, expr.getVariable().getType());
variable = factory.newBoundVariable(expr.getVariable().toString(),
type, boundScope);
variable.setSource(expr.getVariable().getSource());
if (expr.getBoundExpression() != null) {
restriction = processExpression(boundScope, expr
.getBoundExpression());
restriction.setSource(expr.getBoundExpression().getSource());
} else {
restriction = this.factory.booleanLiteralExpression(true);
}
expression = processExpression(boundScope, expr.getExpr());
expression.setSource(expr.getExpr().getSource());
kind = expr.getQuantifierKind();
if (kind == QuantifierKind.EXISTS)
result = this.factory.existsExpression(variable, restriction,
expression);
else if (kind == QuantifierKind.FORALL)
result = this.factory.forallExpression(variable, restriction,
expression);
else
throw new SyntaxException(expr, "Unknown quantifier kind");
assert result != null;
result.setSource(expr.getSource());
return result;
}
private ExpressionIF processTypeCast(ScopeIF scope, ASTTypeCast expr)
throws SyntaxException {
TypeIF type = processType(scope, expr.getType());
ExpressionIF baseExpression = processExpression(scope, expr
.getExpression());
return this.factory.castExpression(type, baseExpression);
}
private ExpressionIF processEvaluatedFunction(ScopeIF scope,
ASTEvaluatedFunction expr) throws SyntaxException {
String functionName = expr.getName();
AbstractFunctionIF function = (AbstractFunctionIF) systemScope
.functionWithName(functionName);
if (function == null)
throw new SyntaxException(expr, "Unknown abstract function: "
+ functionName);
return evaluatedFunction(scope, function, expr.getParamList());
}
private EvaluatedFunctionExpressionIF evaluatedFunction(ScopeIF scope,
AbstractFunctionIF function, List<ASTExpressionIF> actuals)
throws SyntaxException {
EvaluatedFunctionExpressionIF result;
int numArgs = actuals.size();
ExpressionIF[] arguments = new ExpressionIF[numArgs];
for (int i = 0; i < numArgs; i++)
arguments[i] = processExpression(scope, actuals.get(i));
result = this.factory.evaluatedFunctionExpression(function, arguments);
return result;
}
/* Array subscript expression */
private ExpressionIF processArraySubExpr(ScopeIF scope,
ASTArraySubscriptExpression expr) throws SyntaxException {
ExpressionIF baseArray, index, result;
baseArray = processExpression(scope, expr.getBaseArray());
baseArray.setSource(expr.getBaseArray().getSource());
index = processExpression(scope, expr.getArrayIndex());
index.setSource(expr.getArrayIndex().getSource());
result = this.factory.subscriptExpression((LHSExpressionIF) baseArray,
index);
result.setSource(expr.getSource());
return result;
}
/* Binary expression */
private ExpressionIF processBinaryExpr(ScopeIF scope,
ASTBinaryExpression expr) throws SyntaxException {
ExpressionIF result;
ExpressionIF left = processExpression(scope, expr.getLeft());
ExpressionIF right = processExpression(scope, expr.getRight());
switch (expr.getOperator()) {
case PLUS:
if (expr.isPointerOp()) {
if (expr.getLeft().getType() instanceof ASTPointerType) {
result = this.factory.pointerAddExpression(left, right);
} else {
result = this.factory.pointerAddExpression(right, left);
}
} else {
result = this.factory.addExpression(left, right);
}
break;
case SUB:
result = this.factory.subtractExpression(left, right);
break;
case MUL:
result = this.factory.multiplyExpression(left, right);
break;
case DIV:
result = this.factory.divideExpression(left, right);
break;
case MOD:
result = this.factory.moduloExpression(left, right);
break;
case EQ:
result = this.factory.equalsExpression(left, right);
break;
/* Convert x != y to !(x==y) */
case NEQ:
result = this.factory.notExpression(this.factory.equalsExpression(
left, right));
break;
case LT:
result = this.factory.lessThanExpression(left, right);
break;
/* Convert x <= y to (x<y || x==y) */
case LTE:
result = this.factory.lessThanOrEqualsExpression(left, right);
break;
/* Convert x>y to !(x<y) && !(x==y) */
case GT:
result = this.factory.lessThanExpression(right, left);
break;
/* Convert x>=y to !(x<y) */
case GTE:
result = this.factory.lessThanOrEqualsExpression(right, left);
break;
case OR:
result = this.factory.orExpression(left, right);
break;
case AND:
result = this.factory.andExpression(left, right);
break;
default:
throw new SyntaxException("Unknown binary operator: "
+ expr.getOperator());
}
result.setSource(expr.getSource());
return result;
}
/* if-then-else expression */
private ExpressionIF processIfThenElseExpr(ScopeIF scope,
ASTIfThenElseExpression expr) throws SyntaxException {
ExpressionIF predicate = processExpression(scope, expr.getPredicate());
ExpressionIF trueExpr = processExpression(scope, expr.getTrueExpr());
ExpressionIF falseExpr = processExpression(scope, expr.getFalseExpr());
ExpressionIF result = this.factory.ifThenElseExpression(predicate,
trueExpr, falseExpr);
result.setSource(expr.getSource());
return result;
}
private ProcessIF getProcess(ScopeIF scope) throws SyntaxException {
if (scope instanceof ProcessScopeIF)
return ((ProcessScopeIF) scope).process();
if (scope.parent() == null)
throw new SyntaxException("Not in a process scope");
return getProcess(scope.parent());
}
private FunctionIF getFunction(ScopeIF scope) {
if (scope instanceof LocalScopeIF)
return ((LocalScopeIF) scope).function();
if (scope.parent() == null)
return null;
return getFunction(scope.parent());
}
/* Literal expression */
private ExpressionIF processLiteralExpr(ScopeIF scope,
ASTLiteralExpression expr) throws SyntaxException {
ExpressionIF result;
TypeIF literalType = this.processType(scope, expr.getType());
/* boolean constant */
if (expr instanceof ASTBoolLiteral) {
result = this.factory.literalExpression(((ASTBoolLiteral) expr)
.toString());
}
/* integer constant */
else if (expr instanceof ASTIntegerLiteral) {
result = this.factory
.integerLiteralExpression(((ASTIntegerLiteral) expr)
.getValue());
}
/* rational constant */
else if (expr instanceof ASTRealLiteral) {
result = this.factory.realLiteralExpression(((ASTRealLiteral) expr)
.getValue());
}
/* char constant */
else if (expr instanceof ASTCharLiteral) {
result = this.factory
.characterLiteralExpression(((ASTCharLiteral) expr)
.getValue());
} else if (expr instanceof ASTNullLiteral) {
result = this.factory.nullExpression();
}
/* System variable */
else if (expr instanceof ASTSystemVariable) {
SYS_VAR name = ((ASTSystemVariable) expr).getName();
if (name == SYS_VAR.PID) {
ProcessIF process = getProcess(scope);
result = this.factory.literalExpression(String.valueOf(process
.pid()));
} else if (name == SYS_VAR.NPROCS) {
result = this.factory.literalExpression(String.valueOf(scope
.model().numProcs()));
} else {
throw new SyntaxException(expr, "Unknown system variable: "
+ name);
}
} else if (expr instanceof ASTArrayLiteral) {
LiteralExpressionIF[] literalArray = new LiteralExpressionIF[((ASTArrayLiteral) expr)
.numLiteral()];
for (int i = 0; i < literalArray.length; i++) {
ASTExpressionIF temp = ((ASTArrayLiteral) expr).getLiteral(i);
if (temp != null) {
literalArray[i] = (LiteralExpressionIF) (this
.processLiteralExpr(scope,
(ASTLiteralExpression) temp));
} else {
literalArray[i] = null;
}
}
result = this.factory.arrayLiteralExpression(
(ArrayTypeIF) literalType, literalArray);
} else if (expr instanceof ASTStructLiteral) {
edu.udel.cis.vsl.tass.model.IF.expression.LiteralExpressionIF[] literalArray = new edu.udel.cis.vsl.tass.model.IF.expression.LiteralExpressionIF[((ASTStructLiteral) expr)
.numValues()];
for (int i = 0; i < literalArray.length; i++) {
ASTExpressionIF temp = ((ASTStructLiteral) expr)
.getFieldValue(i);
if (temp != null) {
literalArray[i] = (LiteralExpressionIF) (this
.processLiteralExpr(scope,
(ASTLiteralExpression) temp));
} else {
literalArray[i] = null;
}
}
result = this.factory.recordLiteralExpression(
(RecordTypeIF) literalType, literalArray);
} else {
throw new SyntaxException(expr, "Unknown constant type: " + expr);
}
// Set source
result.setSource(expr.getSource());
return result;
}
/* Unary expression */
private ExpressionIF processUnaryExpr(ScopeIF scope, ASTUnaryExpression expr)
throws SyntaxException {
ExpressionIF result;
ExpressionIF operand = processExpression(scope, expr.getOperand());
switch (expr.getOperator()) {
case PLUS:
result = operand;
break;
case MINUS:
result = this.factory.negativeExpression(operand);
break;
case NOT:
result = this.factory.notExpression(operand);
break;
// '*' operator to dereference pointer
case DEREFERENCE:
result = this.factory.dereferenceExpression(operand);
break;
// '&' operator to get the address of an expression
case ADDRESS_OF:
if (operand instanceof edu.udel.cis.vsl.tass.model.IF.expression.LHSExpressionIF) {
result = this.factory
.addressOfExpression((edu.udel.cis.vsl.tass.model.IF.expression.LHSExpressionIF) operand);
break;
} else {
throw new SyntaxException(operand,
"The operand of address of expression must be a left hand side expression "
+ "instead of " + operand.kind());
}
default:
throw new SyntaxException(expr, "Unknown operator: "
+ expr.getOperator());
}
// Set source
result.setSource(expr.getSource());
return result;
}
/* Variable expression */
private ExpressionIF processVariableExpr(ScopeIF scope,
ASTVariableExpression expr) throws SyntaxException {
String name = expr.getVariable().toString();
VariableIF variable = scope.getLexicalVariable(name);
ExpressionIF result = factory.variableExpression(variable);
result.setSource(expr.getSource());
return result;
}
/* Spec expression */
// arguments......need to indicate function, scope, etc.....
private ExpressionIF processSpecExpr(ScopeIF scope, ASTSpecExpression expr)
throws SyntaxException {
String name = expr.getName().toString();
VariableIF variable = null;
FunctionIF implFunction = getFunction(scope);
if (implFunction != null) {
String functionName = implFunction.name();
ProcessScopeIF specScope = specModel.process(0).scope();
FunctionIF specFunction = specScope.functionWithName(functionName);
if (specFunction != null)
variable = specFunction.outermostScope().getLexicalVariable(
name);
}
if (variable == null) {
if (scope instanceof ProcessScopeIF) {
ProcessScopeIF specScope = specModel.process(0).scope();
variable = specScope.getLexicalVariable(name);
} else if (scope instanceof ModelScopeIF) {
variable = specModel.scope().getLexicalVariable(name);
}
}
if (variable == null) {
throw new SyntaxException(expr, "There is no variable named "
+ name + " in model " + this.specModel.name() + ".");
}
return factory.variableExpression(variable);
}
/* Struct member reference expression */
private ExpressionIF processStructMemberRefExpr(ScopeIF scope,
ASTStructMemberRefExpression expr) throws SyntaxException {
ExpressionIF result = null;
ASTExpressionIF baseExpression = expr.getBaseExpr();
/*
* First check if this is really a reference to another process.
* PROC[pid].x
*/
if (baseExpression instanceof ASTArraySubscriptExpression) {
ASTArraySubscriptExpression subscriptExpression = (ASTArraySubscriptExpression) baseExpression;
ASTExpressionIF baseArray = subscriptExpression.getBaseArray();
if (baseArray.toString().equals("PROC")
|| baseArray instanceof ASTSpecExpression) {
ExpressionIF procPid = processExpression(scope,
subscriptExpression.getArrayIndex());
String variableName = expr.getFieldName();
ModelIF variableModel = (baseArray instanceof ASTSpecExpression ? specModel
: scope.model());
ProcessScopeIF proc0Scope = variableModel.process(0).scope();
TypeIF type;
result = factory.processReferenceExpression(variableModel,
procPid, variableName);
// now need to find the type of this expression.
// try to find representative variable in process 0...
if (variableName.contains("@")) {
Scanner sc = new Scanner(variableName);
sc.useDelimiter("@");
String shortName = sc.next();
String functionName = sc.next();
FunctionIF function = proc0Scope
.functionWithName(functionName);
VariableIF variable;
sc.close();
if (function == null)
throw new SyntaxException(expr, "Unknown function: "
+ functionName);
variable = function.outermostScope().variableWithName(
shortName);
if (variable == null)
throw new SyntaxException(expr,
"No variable with name " + shortName
+ " found in function " + functionName);
type = variable.type();
} else {
VariableIF proc0Variable = proc0Scope
.variableWithName(variableName);
if (proc0Variable == null)
throw new SyntaxException(expr, "Unknown variable: "
+ variableName);
type = proc0Variable.type();
}
((ProcessReferenceExpressionIF) result).setType(type);
}
}
if (result == null) {
LHSExpressionIF structExpr = (LHSExpressionIF) (this
.processExpression(scope, baseExpression));
String fieldName = expr.getFieldName();
result = this.factory.recordNavigationExpression(structExpr,
fieldName);
}
result.setSource(expr.getSource());
return result;
}
/* Sizeof expression */
private ExpressionIF processSizeofExpr(ScopeIF scope,
ASTSizeofExpression expr) throws SyntaxException {
TypeIF operand = this.processType(scope, expr.getOperand());
ExpressionIF result = this.factory.sizeOfExpression(operand);
result.setSource(expr.getSource());
return result;
}
/* Self change expression */
/*
* private ExpressionIF processSelfchangeExpr( ModelIF model, int pid,
* FunctionIF function, Map<String, BoundVariableIF> boundVariables,
* SelfChangeExpression expr) {
*
* }
*/
/* Set the main function */
private void setMainFunction(ModelIF model) throws SyntaxException {
for (int i = 0; i < model.numProcs(); i++) {
boolean hasMainFunction = false;
ProcessIF proc = model.process(i);
Iterator<FunctionIF> iterator = proc.scope().functions().iterator();
while (iterator.hasNext()) {
FunctionIF function = iterator.next();
if (function.name().equals("main")) {
model.setMainFunction(proc, function);
hasMainFunction = true;
break;
}
}
if (hasMainFunction == false) {
throw new SyntaxException(
"The program must have a main function as an entry point.");
}
}
}
/* Set the target locations for each statement */
private void setTargetLocation(ModelIF model) throws SyntaxException {
List<StatementIF> stmtList = null;
if (this.lastStmt.empty()) {
this.unsetLoc.pop();
return;
}
if (this.unsetBranchLoc != null) {
model.setExitLocation(this.unsetBranchLoc, this.unsetLoc.peek());
// True branch
stmtList = this.lastStmt.pop();
for (StatementIF stmt : stmtList) {
model.setTargetLocation(stmt, this.unsetLoc.peek());
}
/*
* //False branch stmtList = this.lastStmt.pop();
* for(edu.udel.cis.vsl.minimp.model.IF.statement.StatementIF stmt:
* stmtList) { model.setTargetLocation(stmt, this.unsetLoc.peek());
* }
*/
if (!this.unsetBranchLocStack.empty()) {
while (!this.unsetBranchLocStack.empty()) {
model.setExitLocation(this.unsetBranchLocStack.pop(),
this.unsetLoc.peek());
// model.setTargetLocation(this.lastStmt.pop(),
// this.unsetLoc.peek());
// model.setTargetLocation(this.lastStmt.pop(),
// this.unsetLoc.peek());
}
}
this.unsetBranchLoc = null;
}
/*
* else if (this.hasWildcardExpr == true) { for (int i = 0; i <
* model.numProcs() - 1; i++) {
* model.setTargetLocation(this.lastStmt.pop(), this.unsetLoc.peek()); }
* model.setTargetLocation(this.lastStmt.pop(), this.unsetLoc.pop());
* this.hasWildcardExpr = false; }
*/
else {
stmtList = this.lastStmt.pop();
for (StatementIF stmt : stmtList) {
model.setTargetLocation(stmt, this.unsetLoc.peek());
}
}
/*
* if (this.loopLocSet == false && !this.lastStmt.empty()) { int count =
* this.factorCount.pop().intValue(); for (int i = 0; i < count; i++) {
* model.setTargetLocation(this.lastStmt.pop(), this.unsetLoc.peek()); }
* this.unsetLoc.pop(); this.loopLocSet = true; }
*/
}
// Find the skew factors
private void findSkewFactors() throws SyntaxException {
for (ASTFunctionDeclaration decl : impl.getFunctionList()) {
List<ASTStatementIF> stmtList = decl.getBody().getStatementList();
for (ASTStatementIF stmt : stmtList) {
if (stmt instanceof ASTWhileStatement) {
ASTWhileStatement temp = (ASTWhileStatement) stmt;
if (temp.getInvariant() != null) {
if (temp.getInvariant().getSpecFactor() != 1) {
String name = temp.getInvariant().getLabel();
String functionName = temp.getInvariant()
.getFunctionName();
ASTStatementIF specStmt = null;
if (this.spec.getStatement(functionName, name) != null) {
specStmt = this.spec.getStatement(functionName,
name);
} else {
throw new SyntaxException(temp.getInvariant(),
"There is no statement label " + name
+ " in function "
+ functionName
+ " in the spec program.");
}
this.specSkewMap.put(specStmt, new Integer(temp
.getInvariant().getSpecFactor()));
}
if (temp.getInvariant().getImplFactor() != 1) {
this.implSkewMap.put(stmt, new Integer(temp
.getInvariant().getImplFactor()));
}
}
} else if (stmt instanceof ASTCompoundStatement) {
findSkewFactorInCompoundStmt((ASTCompoundStatement) stmt);
}
}
}
}
private void findSkewFactorInCompoundStmt(ASTCompoundStatement compoundStmt)
throws SyntaxException {
for (ASTStatementIF stmt : compoundStmt.getBody()) {
if (stmt instanceof ASTWhileStatement) {
ASTWhileStatement temp = (ASTWhileStatement) stmt;
if (temp.getInvariant() != null) {
if (temp.getInvariant().getSpecFactor() != 1) {
String name = temp.getInvariant().getLabel();
String functionName = temp.getInvariant()
.getFunctionName();
ASTStatementIF specStmt = null;
if (this.spec.getStatement(functionName, name) != null) {
specStmt = this.spec.getStatement(functionName,
name);
} else {
throw new SyntaxException(temp.getInvariant(),
"There is no statement label " + name
+ " in function " + functionName
+ " in the spec program.");
}
this.specSkewMap.put(specStmt, new Integer(temp
.getInvariant().getSpecFactor()));
}
if (temp.getInvariant().getImplFactor() != 1) {
this.implSkewMap.put(stmt, new Integer(temp
.getInvariant().getImplFactor()));
}
}
} else if (stmt instanceof ASTCompoundStatement) {
findSkewFactorInCompoundStmt((ASTCompoundStatement) stmt);
}
}
}
}