ModelBuilder.java
package edu.udel.cis.vsl.tass.ast2model.impl;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Vector;
import java.util.Iterator;
import edu.udel.cis.vsl.tass.ast.IF.ASTTransformerIF;
import edu.udel.cis.vsl.tass.ast.IF.AbstractSyntaxTreeIF;
import edu.udel.cis.vsl.tass.ast.IF.GlobalScopeNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.LabelNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.PairNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.PragmaParserIF;
import edu.udel.cis.vsl.tass.ast.IF.RootNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.SequenceNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.SideEffectRemoverIF;
import edu.udel.cis.vsl.tass.ast.IF.declaration.FormalVariableDeclarationNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.declaration.FunctionDeclarationNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.declaration.GlobalVariableDeclarationNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.declaration.VariableDeclarationNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.ArrayInitializerNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.AssignmentNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.BindingExpressionNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.BindingExpressionNodeIF.Quantifier;
import edu.udel.cis.vsl.tass.ast.IF.expression.CastNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.CharacterLiteralNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.DereferenceNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.ExpressionNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.FieldReferenceNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.FunctionApplicationNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.FunctionInvocationNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.FunctionReferenceNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.IntegerLiteralNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.LHSExpressionNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.LiteralNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.OperatorNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.ProcessReferenceNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.PureExpressionNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.RealLiteralNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.StartOfNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.StringLiteralNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.StructInitializerNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.SubscriptNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.expression.VariableReferenceNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.statement.AssertStatementNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.statement.AssumeStatementNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.statement.BlockNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.statement.ForLoopNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.statement.GotoNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.statement.IfThenElseStatementNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.statement.NoopNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.statement.ReturnNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.statement.StatementNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.statement.WhileLoopNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.type.ArrayTypeNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.type.IntegerTypeNodeIF;
import edu.udel.cis.vsl.tass.ast.IF.type.TypeNodeIF;
import edu.udel.cis.vsl.tass.ast.impl.PragmaParser;
import edu.udel.cis.vsl.tass.ast.impl.SideEffectRemover;
import edu.udel.cis.vsl.tass.ast.impl.StartOfFinder;
import edu.udel.cis.vsl.tass.ast2model.IF.CollectivePredecessorIF;
import edu.udel.cis.vsl.tass.ast2model.IF.ExitStatementPairIF;
import edu.udel.cis.vsl.tass.ast2model.IF.ModelBuilderIF;
import edu.udel.cis.vsl.tass.ast2model.IF.StatementSetIF;
import edu.udel.cis.vsl.tass.ast2model.IF.TypeBuilderIF;
import edu.udel.cis.vsl.tass.config.CompareConfiguration;
import edu.udel.cis.vsl.tass.config.VerifyConfiguration;
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.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.ProcessReferenceExpressionIF;
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.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.ScopeIF;
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.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.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.ModelFactory;
import edu.udel.cis.vsl.tass.util.Source;
public class ModelBuilder implements ModelBuilderIF {
private ModelFactoryIF factory;
private TypeBuilderIF typeBuilder;
// Map from the name of a function to its declaration node for all functions
// (whether used or not).
private Map<String, FunctionDeclarationNodeIF> declarations;
// Reachable functions that have not been processed.
private Vector<FunctionDefinitionPair<FunctionIF, FunctionDeclarationNodeIF>> worklist;
// Map from model functions to AST declaration. Used to get information from
// the AST for processing the function.
private Map<FunctionDeclarationNodeIF, FunctionIF>[] functions;
// Map from labels to the corresponding locations
private Map<LabelNodeIF, LocationIF> labelledLocations;
// Map from model goto statements to their original AST nodes.
// Used to set target locations after the whole AST has been processed.
private Map<NoopStatementIF, GotoNodeIF> gotoStatements;
private ScopeIF systemScope;
private Map<String, CollectiveAssertionIF> collectiveAssertionMap;
public ModelBuilder() {
collectiveAssertionMap = new HashMap<String, CollectiveAssertionIF>();
}
// Allocation of space for the Map functions is unchecked
@SuppressWarnings("unchecked")
@Override
public ModelIF buildModel(VerifyConfiguration configuration,
AbstractSyntaxTreeIF ast) throws SyntaxException {
System.out.println("Building the model");
factory = new ModelFactory(configuration);
systemScope = factory.systemScope();
typeBuilder = new TypeBuilder(factory);
ModelIF model = factory.newModel(configuration.modelName(),
configuration.numProcs());
functions = new Map[model.numProcs()];
declarations = new HashMap<String, FunctionDeclarationNodeIF>();
labelledLocations = new HashMap<LabelNodeIF, LocationIF>();
SideEffectRemoverIF sideEffectRemover = new SideEffectRemover();
ASTTransformerIF startOfFinder = new StartOfFinder();
PragmaParserIF pragmaParser = new PragmaParser();
for (int i = 0; i < model.numProcs(); i++) {
functions[i] = new HashMap<FunctionDeclarationNodeIF, FunctionIF>();
}
worklist = new Vector<FunctionDefinitionPair<FunctionIF, FunctionDeclarationNodeIF>>();
gotoStatements = new HashMap<NoopStatementIF, GotoNodeIF>();
pragmaParser.transform(ast);
sideEffectRemover.transform(ast);
startOfFinder.transform(ast);
processGlobalScopeNodes(model, ast.rootNode());
processFunctions();
completeGotos();
if (!declarations.containsKey("main")) {
throw new SyntaxException(
"The model must have a main function as an entry point.");
}
for (int i = 0; i < model.numProcs(); i++) {
model.setMainFunction(model.process(i),
functions[i].get(declarations.get("main")));
}
model.complete();
return model;
}
// Allocation of space for the Map functions is unchecked
@SuppressWarnings("unchecked")
@Override
public ModelIF[] buildModel(CompareConfiguration configuration,
AbstractSyntaxTreeIF[] ast) throws SyntaxException {
ModelIF[] models = new ModelIF[2];
if (ast.length != 2) {
throw new SyntaxException("There must be exactly two programs.");
}
factory = new ModelFactory(configuration);
systemScope = factory.systemScope();
typeBuilder = new TypeBuilder(factory);
models[0] = factory.newModel(configuration.specModelName(),
configuration.specNumProcs());
models[1] = factory.newModel(configuration.implModelName(),
configuration.implNumProcs());
// Process the spec
functions = new Map[models[0].numProcs()];
declarations = new HashMap<String, FunctionDeclarationNodeIF>();
labelledLocations = new HashMap<LabelNodeIF, LocationIF>();
PragmaParserIF pragmaParser = new PragmaParser();
SideEffectRemoverIF sideEffectRemover = new SideEffectRemover();
ASTTransformerIF startOfFinder = new StartOfFinder();
for (int i = 0; i < models[0].numProcs(); i++) {
functions[i] = new HashMap<FunctionDeclarationNodeIF, FunctionIF>();
}
worklist = new Vector<FunctionDefinitionPair<FunctionIF, FunctionDeclarationNodeIF>>();
gotoStatements = new HashMap<NoopStatementIF, GotoNodeIF>();
pragmaParser.transform(ast[0]);
sideEffectRemover.transform(ast[0]);
startOfFinder.transform(ast[0]);
processGlobalScopeNodes(models[0], ast[0].rootNode());
processFunctions();
completeGotos();
if (!declarations.containsKey("main")) {
throw new SyntaxException(
"The model must have a main function as an entry point.");
}
for (int i = 0; i < models[0].numProcs(); i++) {
models[0].setMainFunction(models[0].process(i),
functions[i].get(declarations.get("main")));
}
models[0].complete();
// Process the impl
functions = new Map[models[1].numProcs()];
declarations = new HashMap<String, FunctionDeclarationNodeIF>();
labelledLocations = new HashMap<LabelNodeIF, LocationIF>();
pragmaParser = new PragmaParser();
sideEffectRemover = new SideEffectRemover();
startOfFinder = new StartOfFinder();
for (int i = 0; i < models[1].numProcs(); i++) {
functions[i] = new HashMap<FunctionDeclarationNodeIF, FunctionIF>();
}
worklist = new Vector<FunctionDefinitionPair<FunctionIF, FunctionDeclarationNodeIF>>();
gotoStatements = new HashMap<NoopStatementIF, GotoNodeIF>();
pragmaParser.transform(ast[1]);
sideEffectRemover.transform(ast[1]);
startOfFinder.transform(ast[1]);
processGlobalScopeNodes(models[1], ast[1].rootNode());
processFunctions();
completeGotos();
if (!declarations.containsKey("main")) {
throw new SyntaxException(
"The model must have a main function as an entry point.");
}
for (int i = 0; i < models[1].numProcs(); i++) {
models[0].setMainFunction(models[1].process(i),
functions[i].get(declarations.get("main")));
}
models[1].complete();
/*
* Check that all input/output variables in the spec have corresponding
* variables in the impl.
*/
for (VariableIF variable : models[0].scope().variables()) {
SharedVariableIF var = (SharedVariableIF) variable;
String name = var.name();
if (var.isInput() || var.isOutput()) {
if (var.correspondingVariable() == null) {
if (models[1].scope().variableWithName(name) != null) {
SharedVariableIF temp = models[1].scope()
.variableWithName(name);
if (var.isInput()) {
if (temp.isInput()) {
if (temp.correspondingVariable() == null) {
models[0].setCorrespondingVariable(var,
temp);
models[1].setCorrespondingVariable(temp,
var);
} else {
throw new SyntaxException(var,
"No corresponding variable in model "
+ models[1].name()
+ " with variable "
+ var.name() + " in model "
+ models[0].name());
}
} else {
throw new SyntaxException(var,
"The variable with name " + var.name()
+ " in model "
+ models[1].name()
+ " is not an input variable.");
}
} else if (var.isOutput()) {
if (temp.isOutput()) {
if (temp.correspondingVariable() == null) {
models[0].setCorrespondingVariable(var,
temp);
models[1].setCorrespondingVariable(temp,
var);
} else {
throw new SyntaxException(var,
"No corresponding variable in model "
+ models[1].name()
+ " with variable "
+ var.name() + " in model "
+ models[0].name());
}
} else {
throw new SyntaxException(var,
"The variable with name " + var.name()
+ " in model "
+ models[1].name()
+ " is not an output variable.");
}
}
} else {
throw new SyntaxException(var,
"No possible corresponding variables in model "
+ models[1].name() + " with variable "
+ var.name() + " exist.");
}
}
}
}
return models;
}
/**
* Process function definitions and global variable declarations.
*/
private void processGlobalScopeNodes(ModelIF model, RootNodeIF root)
throws SyntaxException {
for (int i = 0; i < root.globalScopeNodes().numChildren(); i++) {
GlobalScopeNodeIF node = (GlobalScopeNodeIF) root
.globalScopeNodes().child(i);
if (node instanceof FunctionDeclarationNodeIF) {
String name = ((FunctionDeclarationNodeIF) node).identifier()
.name();
if (!declarations.containsKey(name)) {
declarations.put(name, (FunctionDeclarationNodeIF) node);
}
// Initially add main in each process to the worklist
if (name.equals("main")) {
// Main has no prototype. Also, as of r2289 the definition
// field was not being set for main.
FunctionDeclarationNodeIF definition = (FunctionDeclarationNodeIF) node;
for (int j = 0; j < model.numProcs(); j++) {
ProcessIF process = model.process(j);
TypeNodeIF outputType = definition.outputType();
TypeIF returnType = typeBuilder
.getModelType(outputType);
SequenceNodeIF<FormalVariableDeclarationNodeIF> formals = definition
.formals();
int numFormals = formals.numChildren();
if (numFormals != 0 && numFormals != 2) {
throw new SyntaxException(definition,
"Main must have either 0 or 2 arguments.");
}
FunctionIF function = model.newFunction(process, name,
returnType, numFormals);
// Create and add the formal parameters
for (int k = 0; k < numFormals; k++) {
FormalVariableDeclarationNodeIF currentFormal = (FormalVariableDeclarationNodeIF) formals
.child(k);
TypeIF formalType = null;
FormalVariableIF formal;
// TODO: Check that the declared types of main are
// equivalent to these types.
if (k == 0) {
// First argument must be equivalent to an
// integer.
formalType = factory.integerType();
} else if (k == 1) {
// Second argument must be equivalent to
// *char[].
formalType = factory.arrayType(factory
.pointerType(factory.characterType()));
}
formal = model.newFormalVariable(function,
formalType, currentFormal.identifier()
.name(), k);
formal.setSource(currentFormal.getSource());
}
function.setSource(definition.getSource());
functions[j].put(definition, function);
worklist.add(new FunctionDefinitionPair<FunctionIF, FunctionDeclarationNodeIF>(
function, definition));
}
}
} else if (node instanceof GlobalVariableDeclarationNodeIF) {
GlobalVariableDeclarationNodeIF declaration = (GlobalVariableDeclarationNodeIF) node;
TypeIF type = typeBuilder.getModelType(declaration.type());
String name = declaration.identifier().name();
VariableIF variable;
ExpressionIF assumption;
if (declaration.isInput()) {
variable = model.newInputVariable(type, name);
if (declaration.inputAssumption() != null) {
assumption = processExpression(model.scope(),
declaration.inputAssumption());
model.setAssumption((SharedVariableIF) variable,
assumption);
}
} else if (declaration.isOutput()) {
variable = model.newOutputVariable(type, name);
} else {
variable = model.newVariable(model.scope(), type, name);
}
if (declaration.initializer() != null) {
ExpressionIF expression = processExpression(model.scope(),
declaration.initializer());
model.setInitializationExpression(variable, expression);
}
if (declaration.type() instanceof ArrayTypeNodeIF) {
model.setArrayDimensions(
variable,
processDimensions(model.scope(),
(ArrayTypeNodeIF) declaration.type()));
}
variable.setSource(declaration.getSource());
}
}
}
/**
* Process functions until the worklist is empty.
*
* @throws SyntaxException
* when there is a syntax error anywhere in a function body.
*/
private void processFunctions() throws SyntaxException {
while (!worklist.isEmpty()) {
FunctionIF function = worklist.firstElement().function();
FunctionDeclarationNodeIF definition = worklist.firstElement()
.definition();
processFunctionBody(function, definition.body());
worklist.remove(0);
}
}
/**
* Takes a previously created model function and an AST block node and
* processes the body.
*
* @throws SyntaxException
* when there is a syntax error anywhere in the function body.
*/
private void processFunctionBody(FunctionIF function, BlockNodeIF body)
throws SyntaxException {
LocalScopeIF scope = function.outermostScope();
processLocalVariables(scope, body.variables());
processBody(scope, body.statements(), body.getSource());
}
/**
* Adds variables to the given scope.
*
* @throws SyntaxException
* when a variable declaration is invalid.
*/
private void processLocalVariables(ScopeIF scope,
SequenceNodeIF<VariableDeclarationNodeIF> variables)
throws SyntaxException {
ModelIF model = scope.model();
for (int i = 0; i < variables.numChildren(); i++) {
VariableDeclarationNodeIF declaration = (VariableDeclarationNodeIF) variables
.child(i);
TypeIF type = typeBuilder.getModelType(declaration.type());
String name = declaration.identifier().name();
VariableIF variable;
variable = model.newVariable(scope, type, name);
if (declaration.initializer() != null) {
ExpressionIF expression = processExpression(
(LocalScopeIF) scope, declaration.initializer());
model.setInitializationExpression(variable, expression);
}
if (declaration.type() instanceof ArrayTypeNodeIF
&& ((ArrayTypeNodeIF) declaration.type()).extent() != null) {
model.setArrayDimensions(
variable,
processDimensions(scope,
(ArrayTypeNodeIF) declaration.type()));
}
variable.setSource(declaration.getSource());
}
}
/**
* Processes the statements in a sequence of statements. Any local variables
* are presumed to have already been added to the scope.
*
* @throws SyntaxException
* when a statement contains a syntax error.
*/
private void processBody(LocalScopeIF scope,
SequenceNodeIF<StatementNodeIF> statements, Source bodySource)
throws SyntaxException {
StatementIF statement = null;
LocationIF terminalLocation;
ModelIF model = scope.model();
for (int i = 0; i < statements.numChildren(); i++) {
statement = processStatement(statement, scope,
(StatementNodeIF) statements.child(i));
}
// Functions with void return type need a dummy location added.
if (!(statement instanceof ReturnStatementIF)) {
ReturnLocationIF returnLocation = model.newReturnLocation(scope);
Source source = new Source(bodySource.file(),
bodySource.lastLine(), bodySource.lastLine(),
bodySource.lastColumn(), bodySource.lastColumn());
source.setText("}");
setTargetLocation(statement, returnLocation);
statement = model.newReturnStatement(returnLocation, null);
statement.setSource(source);
}
terminalLocation = model.newTerminalLocation(scope);
setTargetLocation(statement, terminalLocation);
}
/**
* Processes an AST statement node by calling the appropriate method for the
* type of node. The lastStatement argument is used for setting the target
* location of statements. It should be null for the first call of this
* while processing a function body, or else the result of the last call to
* processStatement.
*
* This method returns a model statement representing the AST statement.
*
* @throws SyntaxException
* when any component of the AST statement contains a syntax
* error or when the type of statement is unimplemented in the
* model builder.
*/
private StatementIF processStatement(StatementIF lastStatement,
ScopeIF scope, StatementNodeIF statement) throws SyntaxException {
if (statement instanceof AssignmentNodeIF) {
return processAssignment(lastStatement, scope,
(AssignmentNodeIF) statement);
} else if (statement instanceof BlockNodeIF) {
return processBlock(lastStatement, scope, (BlockNodeIF) statement);
} else if (statement instanceof ForLoopNodeIF) {
return processForLoop(lastStatement, scope,
(ForLoopNodeIF) statement);
} else if (statement instanceof FunctionInvocationNodeIF) {
return processFunctionInvocation(lastStatement, scope,
(FunctionInvocationNodeIF) statement, null);
} else if (statement instanceof IfThenElseStatementNodeIF) {
return processIfThenElse(lastStatement, scope,
(IfThenElseStatementNodeIF) statement);
} else if (statement instanceof AssertStatementNodeIF) {
return processAssert(lastStatement, scope,
(AssertStatementNodeIF) statement);
} else if (statement instanceof AssumeStatementNodeIF) {
return processAssume(lastStatement, scope,
(AssumeStatementNodeIF) statement);
} else if (statement instanceof ReturnNodeIF) {
return processReturn(lastStatement, scope, (ReturnNodeIF) statement);
} else if (statement instanceof WhileLoopNodeIF) {
return processWhileLoop(lastStatement, scope,
(WhileLoopNodeIF) statement);
} else if (statement instanceof NoopNodeIF) {
return processNoop(lastStatement, scope, (NoopNodeIF) statement);
} else if (statement instanceof GotoNodeIF) {
return processGoto(lastStatement, scope, (GotoNodeIF) statement);
}
throw new SyntaxException(statement, "Unimplemented statement type.");
}
/**
* Returns a noop statement. The noop should transition to the location with
* the goto target.
*
* @throws SyntaxException
* when there is an error creating the noop statement.
*/
private StatementIF processGoto(StatementIF lastStatement, ScopeIF scope,
GotoNodeIF statement) throws SyntaxException {
ChoiceLocationIF noopLocation = scope.model().newChoiceLocation(
(LocalScopeIF) scope);
NoopStatementIF noopStatement = scope.model().newChoiceStatement(
noopLocation, factory.booleanLiteralExpression(true));
noopLocation.setSource(statement.getSource());
noopStatement.setSource(statement.getSource());
processLabels(statement, noopLocation);
gotoStatements.put(noopStatement, statement);
return noopStatement;
}
/**
* Returns a model noop statement.
*
* @throws SyntaxException
* if there is a problem setting the target location for the
* last statement.
*/
private StatementIF processNoop(StatementIF lastStatement, ScopeIF scope,
NoopNodeIF statement) throws SyntaxException {
ChoiceLocationIF noopLocation = scope.model().newChoiceLocation(
(LocalScopeIF) scope);
NoopStatementIF noopStatement = scope.model().newChoiceStatement(
noopLocation, factory.booleanLiteralExpression(true));
setTargetLocation(lastStatement, noopLocation);
noopLocation.setSource(statement.getSource());
noopStatement.setSource(statement.getSource());
processLabels(statement, noopLocation);
return noopStatement;
}
/**
* Returns the model representation of an if-then-else statement. The else
* might be null.
*
* @throws SyntaxException
* when the condition or either branch contains a syntax error.
*/
private StatementIF processIfThenElse(StatementIF lastStatement,
ScopeIF scope, IfThenElseStatementNodeIF ifThenElse)
throws SyntaxException {
ModelIF model = scope.model();
ExpressionIF condition = processExpression(scope,
ifThenElse.condition());
BranchLocationIF branchLocation = model.newBranchLocation(
(LocalScopeIF) scope, condition);
NoopStatementIF trueBranch = model
.newTrueBranchStatement(branchLocation);
NoopStatementIF falseBranch = model
.newFalseBranchStatement(branchLocation);
// {true,false}BranchExit is the final statement in the {true,false}
// branch.
StatementIF trueBranchExit;
StatementIF falseBranchExit;
ExitStatementPairIF exitPair;
setTargetLocation(lastStatement, branchLocation);
branchLocation.setSource(ifThenElse.getSource());
trueBranch.setSource(ifThenElse.getSource());
falseBranch.setSource(ifThenElse.getSource());
trueBranchExit = processStatement(trueBranch, scope,
ifThenElse.trueBranch());
if (ifThenElse.falseBranch() != null) {
falseBranchExit = processStatement(falseBranch, scope,
ifThenElse.falseBranch());
} else {
falseBranchExit = falseBranch;
}
// Wrap the two exits so they can be handled by setTargetLocation().
exitPair = new ExitStatementPair(trueBranchExit, falseBranchExit);
processLabels(ifThenElse, branchLocation);
return exitPair;
}
/**
* Returns the model representation of a for loop. Any of the initializer,
* condition, or incrementer could be null. A null condition will be
* replaced with "true".
*
* @throws SyntaxException
* when any of the initializer, condition, incrementer, or loop
* body contain a syntax error.
*/
private StatementIF processForLoop(StatementIF lastStatement,
ScopeIF scope, ForLoopNodeIF forLoop) throws SyntaxException {
ModelIF model = scope.model();
StatementIF statement;
ExpressionIF condition;
LoopLocationIF loopLocation;
NoopStatementIF trueBranch;
NoopStatementIF falseBranch;
// Process the for loop initialization statement, if present.
if (forLoop.initializer() != null) {
statement = processStatement(lastStatement, scope,
forLoop.initializer());
} else {
statement = lastStatement;
}
// Process the for loop condition, if present.
if (forLoop.condition() != null) {
condition = processExpression(scope, forLoop.condition());
} else {
condition = factory.booleanLiteralExpression(true);
}
loopLocation = model
.newForLoopLocation((LocalScopeIF) scope, condition);
setTargetLocation(statement, loopLocation);
loopLocation.setSource(forLoop.condition().getSource());
trueBranch = model.newLoopTrueBranchStatement(loopLocation);
falseBranch = model.newLoopFalseBranchStatement(loopLocation);
trueBranch.setSource(forLoop.condition().getSource());
falseBranch.setSource(forLoop.condition().getSource());
// Process the body, which is executed when the true branch is taken.
statement = processStatement(trueBranch, scope, forLoop.body());
// Update might be null. If not, add it to the end of the body.
if (forLoop.incrementer() != null) {
statement = processStatement(statement, scope,
forLoop.incrementer());
statement.setSource(forLoop.incrementer().getSource());
}
// The last statement in the loop body (or update) needs to return
// execution to the top of the loop.
setTargetLocation(statement, loopLocation);
processLabels(forLoop, loopLocation);
// The last statement in the loop from the perspective of the next line
// of code is the false branch
return falseBranch;
}
/**
* Returns the model representation of a while loop. The condition could be
* null. A null condition will be replaced with "true".
*
* @throws SyntaxException
* when the condition or body contain a syntax error.
*/
private StatementIF processWhileLoop(StatementIF lastStatement,
ScopeIF scope, WhileLoopNodeIF whileLoop) throws SyntaxException {
ModelIF model = scope.model();
StatementIF statement;
ExpressionIF condition;
LoopLocationIF loopLocation;
NoopStatementIF trueBranch;
NoopStatementIF falseBranch;
SequenceNodeIF<PureExpressionNodeIF> invariants;
String assertionName;
CollectiveAssertionIF assertion = null;
// Process the for loop condition, if present.
if (whileLoop.condition() != null) {
condition = processExpression(scope, whileLoop.condition());
} else {
condition = factory.booleanLiteralExpression(true);
}
loopLocation = model
.newForLoopLocation((LocalScopeIF) scope, condition);
setTargetLocation(lastStatement, loopLocation);
loopLocation.setSource(whileLoop.condition().getSource());
trueBranch = model.newLoopTrueBranchStatement(loopLocation);
falseBranch = model.newLoopFalseBranchStatement(loopLocation);
trueBranch.setSource(whileLoop.getSource());
falseBranch.setSource(whileLoop.getSource());
// Process the body, which is executed when the true branch is taken.
statement = processStatement(trueBranch, scope, whileLoop.body());
// The last statement in the loop body needs to return
// execution to the top of the loop.
setTargetLocation(statement, loopLocation);
processLabels(whileLoop, loopLocation);
invariants = whileLoop.invariants();
// Handle any collective assertions and invariants
if (invariants != null) {
for (Iterator<PureExpressionNodeIF> it = invariants.iterator();
it.hasNext();) {
PureExpressionNodeIF expression = it.next();
assertionName = (String) expression.annotation("name");
if (expression.annotation("collective") != null
|| expression.annotation("joint") != null) {
// This must be a collective or joint invariant.
// If it has already been seen, use the one in the map.
if (collectiveAssertionMap.containsKey(assertionName)) {
assertion = collectiveAssertionMap.get(assertionName);
} else {
boolean isJoint = false;
ProcessIF[] processes = new ProcessIF[model.numProcs()];
if (expression.annotation("joint") != null) {
isJoint = true;
}
for (int i = 0; i < model.numProcs(); i++) {
processes[i] = model.process(i);
}
model.newCollectiveAssertion(expression, processes,
assertionName, true, isJoint);
}
} else {
// This must be a regular invariant.
ExpressionIF invariant = processExpression(scope,
expression);
model.setLabel(loopLocation, assertionName);
loopLocation.putAnnotation(invariant.toString(), invariant);
}
model.addToLocation(loopLocation, assertion,
processExpression(scope, expression));
}
}
// The last statement in the loop from the perspective of the next line
// of code is the false branch
return falseBranch;
}
/**
* Creates a new scope and processes all statements in the block. Returns
* the last statement in the block.
*
* @throws SyntaxException
* when any statement in the block contains a syntax error.
*/
private StatementIF processBlock(StatementIF lastStatement, ScopeIF scope,
BlockNodeIF block) throws SyntaxException {
ScopeIF blockScope = scope.model().newLocalScope((LocalScopeIF) scope);
SequenceNodeIF<StatementNodeIF> statements = block.statements();
StatementIF statement = lastStatement;
processLocalVariables(blockScope, block.variables());
for (int i = 0; i < statements.numChildren(); i++) {
statement = processStatement(statement, blockScope,
(StatementNodeIF) statements.child(i));
}
return statement;
}
/**
* A function invocation may or may not be the right hand side of an
* assignment. If it is, the left hand side is given as the argument lhs.
* Otherwise lhs is null.
*
* @throws SyntaxException
*/
private StatementIF processFunctionInvocation(StatementIF lastStatement,
ScopeIF scope, FunctionInvocationNodeIF invocation,
LHSExpressionNodeIF lhsNode) throws SyntaxException {
LHSExpressionIF lhs = null;
String name = ((FunctionReferenceNodeIF) invocation.function())
.referent().identifier().name();
ModelIF model = scope.model();
InvocationLocationIF location;
InvocationStatementIF statement;
List<ExpressionIF> parameterList = new Vector<ExpressionIF>();
FunctionIF callee;
/* MPI_Comm_rank and MPI_Comm_size need to be handled. */
if (name.equals("MPI_Comm_rank")) {
AssignmentStatementIF result;
AssignmentLocationIF assignmentLocation = model
.newAssignmentLocation((LocalScopeIF) scope);
assignmentLocation.setSource(invocation.getSource());
setTargetLocation(lastStatement, assignmentLocation);
if (invocation.arguments().numChildren() != 2) {
throw new SyntaxException(invocation,
"MPI_Comm_rank takes exactly 2 arguments.");
} else if (!(invocation.arguments().child(0) instanceof VariableReferenceNodeIF)
|| !((VariableReferenceNodeIF) invocation.arguments()
.child(0)).name().equals("MPI_Comm_world")) {
throw new SyntaxException(
invocation,
"Sorry, MPI_Comm_world is currently the only MPI communicator supported by TASS.");
}
lhs = factory.dereferenceExpression(processExpression(scope,
(ExpressionNodeIF) invocation.arguments().child(1)));
result = model.newAssignmentStatement(
assignmentLocation,
lhs,
factory.literalExpression(lastStatement.process().pid()
+ ""));
result.setSource(invocation.getSource());
return result;
} else if (name.equals("MPI_Comm_size")) {
AssignmentStatementIF result;
AssignmentLocationIF assignmentLocation = model
.newAssignmentLocation((LocalScopeIF) scope);
assignmentLocation.setSource(invocation.getSource());
setTargetLocation(lastStatement, assignmentLocation);
if (invocation.arguments().numChildren() != 2) {
throw new SyntaxException(invocation,
"MPI_Comm_size takes exactly 2 arguments.");
} else if (!(invocation.arguments().child(0) instanceof VariableReferenceNodeIF)
|| !((VariableReferenceNodeIF) invocation.arguments()
.child(0)).name().equals("MPI_Comm_world")) {
throw new SyntaxException(
invocation,
"Sorry, MPI_Comm_world is currently the only MPI communicator supported by TASS.");
}
lhs = factory.dereferenceExpression(processExpression(scope,
(ExpressionNodeIF) invocation.arguments().child(1)));
result = model.newAssignmentStatement(assignmentLocation, lhs,
factory.literalExpression(model.numProcs() + ""));
result.setSource(invocation.getSource());
return result;
}
/* "send" and "recv" are special functions. Catch and handle them. */
if (name.equals("send")) {
return processSend(lastStatement, scope, invocation);
} else if (name.equals("recv")) {
return processRecv(lastStatement, scope, invocation);
}
addFunction((LocalScopeIF) scope,
((FunctionReferenceNodeIF) invocation.function()).referent());
for (int i = 0; i < invocation.arguments().numChildren(); i++) {
parameterList.add(processExpression(scope,
(ExpressionNodeIF) invocation.arguments().child(0)));
}
callee = scope.getLexicalFunction(name);
/* Figure out left-hand side, if non-null */
if (lhsNode != null) {
ExpressionIF temp = processExpression(scope, lhsNode);
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;
}
// TODO: Handle libraries (does this need to be different?), system, and
// abstract functions
location = model.newInvocationLocation((LocalScopeIF) scope);
setTargetLocation(lastStatement, location);
location.setSource(invocation.getSource());
statement = model.newInvocationStatement(location, lhs, callee,
parameterList);
statement.setSource(invocation.getSource());
return statement;
}
/**
* Returns the model representation of a "recv" statement. While this is a
* normal function invocation in the AST, the model has a special
* representation.
*
* @throws SyntaxException
* if any of the buffer, source, tag, or size (if present) have
* a syntax exception, or if there are the wrong number of
* arguments.
*/
private StatementIF processRecv(StatementIF lastStatement, ScopeIF scope,
FunctionInvocationNodeIF invocation) throws SyntaxException {
ModelIF model = scope.model();
ReceiveLocationIF receiveLocation = null;
ExpressionNodeIF tagNode, sourceNode;
ExpressionIF source, tag;
LHSExpressionIF buffer, sizeExpression = null;
StatementIF statement = null;
if (invocation.arguments().numChildren() < 3
|| invocation.arguments().numChildren() > 4) {
throw new SyntaxException(invocation,
"Receive statements must have 3 or 4 arguments.");
}
buffer = (LHSExpressionIF) processExpression(scope, invocation
.arguments().getSequenceChild(0));
tagNode = invocation.arguments().getSequenceChild(2);
// Check if the tag is an any() expression
if (tagNode instanceof FunctionInvocationNodeIF
&& ((FunctionReferenceNodeIF) ((FunctionInvocationNodeIF) tagNode)
.function()).referent().identifier().name()
.equals("any")) {
ExpressionIF argument = processExpression(scope,
((FunctionInvocationNodeIF) tagNode).arguments()
.getSequenceChild(0));
if (!(argument instanceof LHSExpressionIF)) {
throw new SyntaxException(argument,
"The expression in any tag must be a left-hand side expression.");
}
tag = factory.anyExpression((LHSExpressionIF) argument);
} else {
tag = processExpression(scope, tagNode);
}
// Handle size expression if present.
if (invocation.arguments().numChildren() == 4) {
sizeExpression = (LHSExpressionIF) processExpression(scope,
invocation.arguments().getSequenceChild(3));
}
// Process source expression.
sourceNode = invocation.arguments().getSequenceChild(2);
// First check if this is an any() expression.
if (sourceNode instanceof FunctionInvocationNodeIF
&& ((FunctionReferenceNodeIF) ((FunctionInvocationNodeIF) tagNode)
.function()).referent().identifier().name()
.equals("any")) {
ExpressionIF argument = processExpression(scope,
((FunctionInvocationNodeIF) tagNode).arguments()
.getSequenceChild(0));
statement = new StatementSet();
receiveLocation = model
.newAnySourceReceiveLocation((LocalScopeIF) scope);
receiveLocation.setSource(invocation.getSource());
if (!(argument instanceof LHSExpressionIF)) {
throw new SyntaxException(argument,
"The expression in any tag must be a left-hand side expression.");
}
for (int i = 0; i < model.numProcs(); i++) {
ExpressionIF sourceArgument = factory.literalExpression(String
.valueOf(i));
StatementIF receiveStatement = null, assignStatement;
AssignmentLocationIF assignLocation;
if (sizeExpression == null) {
receiveStatement = model.newReceiveStatement(
receiveLocation, buffer, sourceArgument, tag);
} else {
receiveStatement = model.newReceiveStatement(
receiveLocation, buffer, sourceArgument, tag,
sizeExpression);
}
assignLocation = model
.newAssignmentLocation((LocalScopeIF) scope);
assignStatement = model.newAssignmentStatement(assignLocation,
(LHSExpressionIF) argument, sourceArgument);
setTargetLocation(receiveStatement, assignLocation);
assignLocation.setSource(sourceNode.getSource());
assignStatement.setSource(sourceNode.getSource());
receiveStatement.setSource(invocation.getSource());
((StatementSetIF) statement).add(assignStatement);
}
} else {
// Single source
receiveLocation = model
.newStandardReceiveLocation((LocalScopeIF) scope);
source = processExpression(scope, sourceNode);
if (sizeExpression == null) {
statement = model.newReceiveStatement(receiveLocation, buffer,
source, tag);
} else {
statement = model.newReceiveStatement(receiveLocation, buffer,
source, tag, sizeExpression);
}
statement.setSource(invocation.getSource());
}
setTargetLocation(lastStatement, receiveLocation);
return statement;
}
/**
* Returns the model representation of a "send" statement. While this is a
* normal function invocation in the AST, the model has a special
* representation.
*
* @throws SyntaxException
* if any of the buffer, destination, or tag have a syntax
* exception, or if there are the wrong number of arguments.
*/
private StatementIF processSend(StatementIF lastStatement, ScopeIF scope,
FunctionInvocationNodeIF invocation) throws SyntaxException {
ModelIF model = scope.model();
SendLocationIF sendLocation = model
.newSendLocation((LocalScopeIF) scope);
SendStatementIF send = null;
LHSExpressionIF buffer;
ExpressionIF destination;
ExpressionIF tag;
setTargetLocation(lastStatement, sendLocation);
sendLocation.setSource(invocation.getSource());
if (invocation.arguments().numChildren() != 3) {
throw new SyntaxException(invocation,
"Send statements must have exactly 3 arguments.");
}
buffer = (LHSExpressionIF) processExpression(scope, invocation
.arguments().getSequenceChild(0));
destination = processExpression(scope, invocation.arguments()
.getSequenceChild(1));
tag = processExpression(scope,
invocation.arguments().getSequenceChild(2));
send = model.newSendStatement(sendLocation, buffer, destination, tag);
send.setSource(invocation.getSource());
return send;
}
/**
* Returns the model representation of an assert statement.
*
* @throws SyntaxException
* when the assertion predicate contains a syntax error.
*/
private StatementIF processAssert(StatementIF lastStatement, ScopeIF scope,
AssertStatementNodeIF assertNode) throws SyntaxException {
ModelIF model = scope.model();
AssertionLocationIF location;
AssertionStatementIF statement = null;
if (assertNode.annotation("collective") != null
|| assertNode.annotation("joint") != null) {
CollectivePredecessorIF predecessorStatement = null;
Collection<CollectiveAssertionIF> assertions;
CollectiveAssertionIF assertion;
if (lastStatement instanceof CollectivePredecessorIF) {
predecessorStatement = (CollectivePredecessorIF) lastStatement;
assertions = ((CollectivePredecessorIF) lastStatement)
.assertions();
} else {
assertions = new HashSet<CollectiveAssertionIF>();
}
if (collectiveAssertionMap.containsKey(assertNode
.annotation("name"))) {
assertion = collectiveAssertionMap.get(assertNode
.annotation("name"));
} else {
boolean isJoint = false;
ProcessIF[] processes = new ProcessIF[model.numProcs()];
for (int i = 0; i < model.numProcs(); i++) {
processes[i] = model.process(i);
}
assertion = model.newCollectiveAssertion(assertNode, processes,
(String) assertNode.annotation("name"), false, isJoint);
}
assertions.add(assertion);
if (predecessorStatement == null) {
predecessorStatement = new CollectivePredecessor(lastStatement,
assertions);
} else {
predecessorStatement.setAssertions(assertions);
}
predecessorStatement.setExpression(assertion,
processExpression(scope, assertNode.predicate()));
return predecessorStatement;
}
location = model.newAssertionLocation((LocalScopeIF) scope);
setTargetLocation(lastStatement, location);
location.setSource(assertNode.getSource());
ExpressionIF assertion = processExpression(scope,
assertNode.predicate());
if (assertNode.annotation("message") != null) {
statement = model.newAssertionStatement(location, assertion,
(String) assertNode.annotation("message"));
} else {
statement = model.newAssertionStatement(location, assertion);
}
statement.setSource(assertNode.getSource());
processLabels(assertNode, location);
return statement;
}
/**
* Returns the model representation of an assume statement.
*
* @throws SyntaxException
* when the assume predicate contains a syntax error.
*/
private StatementIF processAssume(StatementIF lastStatement, ScopeIF scope,
AssumeStatementNodeIF assumeNode) throws SyntaxException {
ModelIF model = scope.model();
AssumeLocationIF location = model
.newAssumeLocation((LocalScopeIF) scope);
AssumeStatementIF statement = null;
ExpressionIF assumption;
setTargetLocation(lastStatement, location);
location.setSource(assumeNode.getSource());
assumption = processExpression(scope, assumeNode.predicate());
statement = model.newAssumeStatement(location, assumption);
statement.setSource(assumeNode.getSource());
processLabels(assumeNode, location);
return statement;
}
/**
* Returns the model representation of a return statement.
*
* @throws SyntaxException
* when the returned expression has a syntax error.
*/
private StatementIF processReturn(StatementIF lastStatement, ScopeIF scope,
ReturnNodeIF returnNode) throws SyntaxException {
ModelIF model = scope.model();
ExpressionIF expression = null;
ReturnLocationIF location = model
.newReturnLocation((LocalScopeIF) scope);
setTargetLocation(lastStatement, location);
location.setSource(returnNode.getSource());
if (returnNode.expression() != null) {
expression = processExpression(scope, returnNode.expression());
}
ReturnStatementIF statement = model.newReturnStatement(location,
expression);
statement.setSource(returnNode.getSource());
processLabels(returnNode, location);
return statement;
}
/**
* Returns the model representation of an assignment statement. If the right
* hand side is an invocation statement, a model function invocation is
* returned. Otherwise, a model assignment statement is returned.
*
* @throws SyntaxException
* when the assignment contains a syntax error.
*/
private StatementIF processAssignment(StatementIF lastStatement,
ScopeIF scope, AssignmentNodeIF assignment) throws SyntaxException {
ModelIF model = scope.model();
/*
* Check if this is an assignment where the right hand side is an
* invocation. If so, process it as an invocation.
*/
if (assignment.rhs() instanceof FunctionInvocationNodeIF) {
return processFunctionInvocation(lastStatement, scope,
(FunctionInvocationNodeIF) assignment.rhs(),
(LHSExpressionNodeIF) assignment.lhs());
}
/* Create a new location */
AssignmentLocationIF location = model
.newAssignmentLocation((LocalScopeIF) scope);
ExpressionIF lhs = processExpression(scope, assignment.lhs());
ExpressionIF rhs = processExpression(scope, assignment.rhs());
// TODO: Handle all types of assignments
switch (assignment.assignmentType()) {
case SIMPLE:
break;
case MULTIPLICATION:
rhs = factory.multiplyExpression(lhs, rhs);
break;
case DIVISION:
rhs = factory.divideExpression(lhs, rhs);
break;
case REMAINDER:
throw new SyntaxException(assignment,
"Remainder assignment not implemented.");
case ADDITION:
rhs = factory.addExpression(lhs, rhs);
break;
case SUBTRACTION:
rhs = factory.subtractExpression(lhs, rhs);
break;
case LEFT_SHIFT:
throw new SyntaxException(assignment,
"Left shift assignment not implemented.");
case RIGHT_SHIFT:
throw new SyntaxException(assignment,
"Right shift assignment not implemented.");
case AND:
rhs = factory.andExpression(lhs, rhs);
break;
case XOR:
throw new SyntaxException(assignment,
"Xor assignment not implemented.");
case OR:
rhs = factory.orExpression(lhs, rhs);
}
// rhs = processExpression(scope, assignment.rhs());
AssignmentStatementIF statement;
setTargetLocation(lastStatement, location);
location.setSource(assignment.getSource());
if (!(lhs instanceof LHSExpressionIF)) {
throw new SyntaxException(
lhs,
"Type error: the left hand side of an invocation statement must be a LHSExpressionIF.");
}
statement = model.newAssignmentStatement(location,
(LHSExpressionIF) lhs, rhs);
statement.setSource(assignment.getSource());
return statement;
}
/**
* Processes an AST expression node by calling the appropriate method for
* the type of node.
*
* @throws SyntaxException
* when the expression type is unknown or when the expression
* contains a syntax error.
*/
private ExpressionIF processExpression(ScopeIF scope,
ExpressionNodeIF expressionNode) throws SyntaxException {
if (expressionNode instanceof ArrayInitializerNodeIF) {
return processArrayInitializer(scope,
(ArrayInitializerNodeIF) expressionNode);
} else if (expressionNode instanceof StructInitializerNodeIF) {
return processStructInitializer(scope,
(StructInitializerNodeIF) expressionNode);
} else if (expressionNode instanceof BindingExpressionNodeIF) {
return processBindingExpression(scope,
(BindingExpressionNodeIF) expressionNode);
} else if (expressionNode instanceof CastNodeIF) {
return processCast(scope, (CastNodeIF) expressionNode);
} else if (expressionNode instanceof DereferenceNodeIF) {
return processDereference(scope, (DereferenceNodeIF) expressionNode);
} else if (expressionNode instanceof FieldReferenceNodeIF) {
return processFieldReference(scope,
(FieldReferenceNodeIF) expressionNode);
} else if (expressionNode instanceof FunctionApplicationNodeIF) {
return processFunctionApplication(scope,
(FunctionApplicationNodeIF) expressionNode);
} else if (expressionNode instanceof OperatorNodeIF) {
return processOperator(scope, (OperatorNodeIF) expressionNode);
} else if (expressionNode instanceof VariableReferenceNodeIF) {
return processVariableReference(scope,
(VariableReferenceNodeIF) expressionNode);
} else if (expressionNode instanceof LiteralNodeIF) {
return processLiteral(scope, (LiteralNodeIF) expressionNode);
} else if (expressionNode instanceof SubscriptNodeIF) {
return processSubscript(scope, (SubscriptNodeIF) expressionNode);
} else if (expressionNode instanceof StartOfNodeIF) {
return processStartOf(scope, (StartOfNodeIF) expressionNode);
} else if (expressionNode instanceof ProcessReferenceNodeIF) {
return processProcessReference(scope,
(ProcessReferenceNodeIF) expressionNode);
}
throw new SyntaxException(expressionNode, "Unknown expression type.");
}
/**
* Returns the address of the 0th element of the array in this StartOfNode.
*
* @throws SyntaxException
* if there is an error in the array expression of the
* StartOfNode.
*/
private ExpressionIF processStartOf(ScopeIF scope, StartOfNodeIF startof)
throws SyntaxException {
ExpressionIF zero = factory.integerLiteralExpression(0);
LHSExpressionIF array;
LHSExpressionIF arrayStart = null;
ExpressionIF result;
if (!(startof.arrayExpression() instanceof VariableReferenceNodeIF)) {
throw new SyntaxException(startof,
"Array expression in a startof must be a reference to an array.");
}
array = processVariableReference(scope,
(VariableReferenceNodeIF) startof.arrayExpression());
arrayStart = factory.subscriptExpression(array, zero);
result = factory.addressOfExpression(arrayStart);
result.setSource(startof.getSource());
return result;
}
/**
* Returns an array subscript expression.
*
* @throws SyntaxException
* when the array or the index contain a syntax error.
*/
private LHSExpressionIF processSubscript(ScopeIF scope,
SubscriptNodeIF expressionNode) throws SyntaxException {
LHSExpressionIF array = (LHSExpressionIF) processExpression(scope,
expressionNode.arrayExpression());
ExpressionIF index = processExpression(scope,
expressionNode.indexExpression());
LHSExpressionIF subscriptExpression = factory.subscriptExpression(
array, index);
subscriptExpression.setSource(expressionNode.getSource());
return subscriptExpression;
}
/**
* Returns a record literal expression to be used for initializing a struct.
*
* @throws SyntaxException
* when any element of the struct contains a syntax error, or
* when the initializer is empty.
*/
private ExpressionIF processStructInitializer(ScopeIF scope,
StructInitializerNodeIF struct) throws SyntaxException {
SequenceNodeIF<PairNodeIF<FieldReferenceNodeIF, ExpressionNodeIF>> elements = struct
.elements();
ExpressionNodeIF expression;
List<ExpressionIF> expressions = new Vector<ExpressionIF>();
ArrayTypeIF structType;
ExpressionIF structLiteral;
// TODO: This seems to be what the standard says, but double-check.
if (elements.numChildren() == 0) {
throw new SyntaxException(struct, "Initializer may not be empty.");
}
structType = factory.arrayType(expressionType(struct));
for (int i = 0; i < elements.numChildren(); i++) {
expression = elements.getSequenceChild(i).right();
expressions.add(processExpression(scope, expression));
}
structLiteral = factory.arrayLiteralExpression(structType,
expressions.toArray(new ExpressionIF[expressions.size()]));
structLiteral.setSource(struct.getSource());
return structLiteral;
}
/**
* Returns a quantified expression in the model.
*
* @throws SyntaxException
* when the bound variable type, restriction expression, or
* predicate contain an error, or when the quantifier is
* unknown.
*/
private ExpressionIF processBindingExpression(ScopeIF scope,
BindingExpressionNodeIF expressionNode) throws SyntaxException {
Quantifier quantifier = expressionNode.quantifier();
BoundVariableIF variable;
ExpressionIF constraint, expression, result;
BoundScopeIF boundScope = factory.newBoundScope(scope);
TypeIF type = typeBuilder.getModelType(expressionNode.boundVariable()
.type());
variable = factory.newBoundVariable(expressionNode.boundVariable()
.identifier().name(), type, boundScope);
variable.setSource(expressionNode.boundVariable().getSource());
if (expressionNode.constraint() != null) {
constraint = processExpression(boundScope,
expressionNode.constraint());
} else {
constraint = factory.booleanLiteralExpression(true);
}
expression = processExpression(boundScope, expressionNode.expression());
expression.setSource(expressionNode.expression().getSource());
if (quantifier == Quantifier.EXISTS) {
result = factory.existsExpression(variable, constraint, expression);
} else if (quantifier == Quantifier.FORALL) {
result = factory.forallExpression(variable, constraint, expression);
} else {
// TODO Implement SUM, LAMBDA, UNIFORM in model
throw new SyntaxException(expressionNode,
"Unknown quantifier type.");
}
result.setSource(expressionNode.getSource());
return result;
}
/**
* Returns an array literal expression to be used for initializing an array.
*
* @throws SyntaxException
* when any element of the array contains a syntax error, or
* when the initializer is empty.
*/
private ExpressionIF processArrayInitializer(ScopeIF scope,
ArrayInitializerNodeIF array) throws SyntaxException {
SequenceNodeIF<ExpressionNodeIF> elements = array.elements();
ExpressionNodeIF expression;
List<ExpressionIF> expressions = new Vector<ExpressionIF>();
ArrayTypeIF arrayType;
ExpressionIF arrayLiteral;
// TODO: This seems to be what the standard says, but double-check.
if (elements.numChildren() == 0) {
throw new SyntaxException(array, "Initializer may not be empty.");
}
arrayType = factory.arrayType(expressionType(elements
.getSequenceChild(0)));
for (int i = 0; i < elements.numChildren(); i++) {
expression = elements.getSequenceChild(i);
expressions.add(processExpression(scope, expression));
}
arrayLiteral = factory.arrayLiteralExpression(arrayType,
expressions.toArray(new ExpressionIF[expressions.size()]));
arrayLiteral.setSource(array.getSource());
return arrayLiteral;
}
/**
* Takes an AST expression and returns the model type in limited cases.
*
* @throws SyntaxException
* when the method cannot handle the given type.
*/
private TypeIF expressionType(ExpressionNodeIF expression)
throws SyntaxException {
// TODO Handle more complicated expressions.
if (expression instanceof ArrayInitializerNodeIF) {
if (((ArrayInitializerNodeIF) expression).elements().numChildren() == 0) {
throw new SyntaxException(expression,
"Initializer may not be empty");
}
return factory
.arrayType(expressionType(((ArrayInitializerNodeIF) expression)
.elements().getSequenceChild(0)));
} else if (expression instanceof StructInitializerNodeIF) {
List<String> fieldNames = new Vector<String>();
List<TypeIF> fieldTypes = new Vector<TypeIF>();
List<ExpressionIF[]> dimensionExpressions = new Vector<ExpressionIF[]>();
SequenceNodeIF<PairNodeIF<FieldReferenceNodeIF, ExpressionNodeIF>> elements = ((StructInitializerNodeIF) expression)
.elements();
PairNodeIF<FieldReferenceNodeIF, ExpressionNodeIF> currentElement;
TypeIF currentType;
if (((StructInitializerNodeIF) expression).elements().numChildren() == 0) {
throw new SyntaxException(expression,
"Initializer may not be empty");
}
for (int i = 0; i < elements.numChildren(); i++) {
currentElement = elements.getSequenceChild(i);
fieldNames.add(currentElement.left().name());
currentType = expressionType(currentElement.right());
fieldTypes.add(currentType);
if (currentType instanceof ArrayTypeIF) {
// dimensionExpressions.add(((ArrayTypeIF) currentType).)
}
}
// TODO Finish initializing literals
return factory.recordType("", fieldNames
.toArray(new String[fieldNames.size()]), fieldTypes
.toArray(new TypeIF[fieldTypes.size()]),
dimensionExpressions
.toArray(new ExpressionIF[dimensionExpressions
.size()][]));
} else if (expression instanceof CharacterLiteralNodeIF) {
return factory.characterType();
} else if (expression instanceof IntegerLiteralNodeIF) {
return factory.integerType();
} else if (expression instanceof RealLiteralNodeIF) {
return factory.rationalType();
} else if (expression instanceof StringLiteralNodeIF) {
return factory.arrayType(factory.characterType());
} else {
throw new SyntaxException(expression,
"Unable to determine expression type.");
}
}
/**
* Returns a model evaluated function expression.
*
* @throws SyntaxException
* when the function is unknown or when any argument contains a
* syntax error.
*/
private ExpressionIF processFunctionApplication(ScopeIF scope,
FunctionApplicationNodeIF function) throws SyntaxException {
FunctionReferenceNodeIF functionReference = (FunctionReferenceNodeIF) function
.function();
AbstractFunctionIF abstractFunction = (AbstractFunctionIF) systemScope
.functionWithName(functionReference.referent().identifier()
.name());
List<ExpressionIF> arguments = new Vector<ExpressionIF>();
EvaluatedFunctionExpressionIF result;
if (abstractFunction == null) {
throw new SyntaxException(function, "Unknown abstract function.");
}
for (int i = 0; i < function.arguments().numChildren(); i++) {
arguments.add(processExpression(scope, function.arguments()
.getSequenceChild(i)));
}
result = factory.evaluatedFunctionExpression(abstractFunction,
arguments.toArray(new ExpressionIF[arguments.size()]));
return result;
}
/**
* Returns a struct / union field reference.
*
* @throws SyntaxException
* when the struct / union being referenced is unknown.
*/
private LHSExpressionIF processFieldReference(ScopeIF scope,
FieldReferenceNodeIF expressionNode) throws SyntaxException {
LHSExpressionIF result = null;
LHSExpressionIF variable = (LHSExpressionIF) processLHS(scope,
expressionNode.struct());
result = factory.recordNavigationExpression(variable, expressionNode
.field().name());
result.setSource(expressionNode.getSource());
return result;
}
/**
* Checks the type of the lhsNode, calls the appropriate method to process
* it, and returns the result.
*
* @throws SyntaxException
* if the LHS node type isn't handled.
*/
private LHSExpressionIF processLHS(ScopeIF scope, LHSExpressionNodeIF lhsNode) throws SyntaxException {
if (lhsNode instanceof VariableReferenceNodeIF) {
return processVariableReference(scope, (VariableReferenceNodeIF) lhsNode);
} else if (lhsNode instanceof FieldReferenceNodeIF) {
return processFieldReference(scope, (FieldReferenceNodeIF) lhsNode);
} else if (lhsNode instanceof SubscriptNodeIF) {
return processSubscript(scope, (SubscriptNodeIF) lhsNode);
} else {
throw new SyntaxException(lhsNode, "LHS expression node type not handled.");
}
}
/**
* Returns a reference to a variable in a different process.
*
* @throws SyntaxException
* when the variable name, pid, or (optional) function are
* invalid.
*/
private ExpressionIF processProcessReference(ScopeIF scope,
ProcessReferenceNodeIF processReference) throws SyntaxException {
ProcessReferenceExpressionIF result = null;
FunctionIF function = null;
ModelIF model = scope.model();
ExpressionIF pid = processExpression(scope, processReference.pid());
String variableName = processReference.variable().name();
TypeIF type = null;
if (processReference.function() != null) {
function = model.scope().functionWithName(
processReference.function().name());
try {
type = function.outermostScope().variableWithName(variableName)
.type();
} catch (NullPointerException e) {
throw new SyntaxException(processReference, "No variable "
+ variableName + " found in function "
+ function.name());
}
variableName += "@" + function.name();
} else {
try {
type = model.process(0).scope().variableWithName(variableName)
.type();
} catch (NullPointerException e) {
throw new SyntaxException(processReference, "Unknown variable "
+ variableName);
}
}
result = factory.processReferenceExpression(model, pid,
variableName);
result.setType(type);
result.setSource(processReference.getSource());
return result;
}
/**
* Returns a derefererence expression.
*
* @throws SyntaxException
* when the pointer being dereferenced is unknown.
*/
private ExpressionIF processDereference(ScopeIF scope,
DereferenceNodeIF expressionNode) throws SyntaxException {
ExpressionIF result;
ExpressionIF pointerExpression = processExpression(scope,
expressionNode.pointerExpression());
result = factory.dereferenceExpression(pointerExpression);
result.setSource(expressionNode.getSource());
return result;
}
/**
* Returns a model cast expression.
*
* @throws SyntaxException
* when the expression being cast has a syntax error or when
* there is an error in the cast type.
*/
private ExpressionIF processCast(ScopeIF scope, CastNodeIF expressionNode)
throws SyntaxException {
ExpressionIF result;
TypeIF type = typeBuilder.getModelType(expressionNode.newType());
ExpressionIF baseExpression = processExpression(scope,
expressionNode.expression());
result = factory.castExpression(type, baseExpression);
result.setSource(expressionNode.getSource());
return result;
}
/**
* Returns a model literal expression.
*
* @param scope
*
* @throws SyntaxException
* when the literal type is not known.
*/
private ExpressionIF processLiteral(ScopeIF scope, LiteralNodeIF literalNode)
throws SyntaxException {
ExpressionIF literal;
/*
* This literal might be a named literal expression, (ie. from a
* #define) or an input variable (i.e. from a #define with an input
* pragma). Note: such variables must be in the model scope, not local.
*/
if (literalNode.identifier() != null) {
if (scope.model().scope()
.getLexicalVariable(literalNode.identifier().name()) != null) {
return factory.variableExpression(scope.model().scope()
.getLexicalVariable(literalNode.identifier().name()));
}
return processNamedLiteral(literalNode);
}
// TODO: Handle arrays, structs, null, strings, etc.
/* char constant */
if (literalNode instanceof CharacterLiteralNodeIF) {
literal = factory
.characterLiteralExpression(((CharacterLiteralNodeIF) literalNode)
.characterValue());
}
/* integer constant */
else if (literalNode instanceof IntegerLiteralNodeIF) {
IntegerLiteralNodeIF integerNode = (IntegerLiteralNodeIF) literalNode;
// One of the integer types is CHAR. We need to handle this case
// differently.
if (((IntegerTypeNodeIF) integerNode.type()).intType() == IntegerTypeNodeIF.IntType.CHAR) {
literal = factory.characterLiteralExpression((char) integerNode
.integerValue().intValue());
} else {
literal = factory.integerLiteralExpression(integerNode
.integerValue().intValue());
}
}
/* real constant */
else if (literalNode instanceof RealLiteralNodeIF) {
literal = factory
.realLiteralExpression(((RealLiteralNodeIF) literalNode)
.realValue().toString());
} else {
throw new SyntaxException(literalNode, "Unknown literal type: "
+ literalNode);
}
// Set source
literal.setSource(literalNode.getSource());
return literal;
}
/**
* Returns the model representation of a named literal. i.e. a literal that
* comes from a #define
*
* @throws SyntaxException
* when the literal type is unknown.
*/
private ExpressionIF processNamedLiteral(LiteralNodeIF literalNode)
throws SyntaxException {
ExpressionIF literal;
// TODO: Handle arrays, structs, null, strings, etc.
/* Named char literal */
if (literalNode instanceof CharacterLiteralNodeIF) {
literal = factory.namedCharacterLiteralExpression(
((CharacterLiteralNodeIF) literalNode).characterValue(),
literalNode.identifier().name());
}
/* Named integer literal */
else if (literalNode instanceof IntegerLiteralNodeIF) {
IntegerLiteralNodeIF integerNode = (IntegerLiteralNodeIF) literalNode;
// One of the integer types is CHAR. We need to handle this case
// differently.
if (((IntegerTypeNodeIF) integerNode.type()).intType() == IntegerTypeNodeIF.IntType.CHAR) {
literal = factory.namedCharacterLiteralExpression(
(char) integerNode.integerValue().intValue(),
integerNode.identifier().name());
} else {
literal = factory.namedIntegerLiteralExpression(integerNode
.integerValue().intValue(), integerNode.identifier()
.name());
}
}
/* Named real literal */
else if (literalNode instanceof RealLiteralNodeIF) {
literal = factory.namedRealLiteralExpression(
((RealLiteralNodeIF) literalNode).realValue().toString(),
literalNode.identifier().name());
} else {
throw new SyntaxException(literalNode,
"Unknown named literal type: " + literalNode);
}
// Set source
literal.setSource(literalNode.getSource());
return literal;
}
/**
* Returns a variable expression for the referenced variable.
*/
private LHSExpressionIF processVariableReference(ScopeIF scope,
VariableReferenceNodeIF variableNode) {
String name = variableNode.name();
// FIXME: This shouldn't be necessary. The name
// should be set before getting here.
if (name == null) {
name = variableNode.referent().identifier().name();
}
VariableIF variable = scope.getLexicalVariable(name);
LHSExpressionIF variableExpression = factory
.variableExpression(variable);
variableExpression.setSource(variableNode.getSource());
return variableExpression;
}
/**
* Returns a model expression for this unary, binary, or ternary operator.
*
* @throws SyntaxException
* when the operator type is unknown.
*/
private ExpressionIF processOperator(ScopeIF scope,
OperatorNodeIF operatorNode) throws SyntaxException {
ExpressionIF arg0;
ExpressionIF arg1;
ExpressionIF arg2;
ExpressionIF operator = null;
// Unary Ops
arg0 = processExpression(scope, operatorNode.getArgument(0));
if (operatorNode.numChildren() == 2) {
switch (operatorNode.getOperator()) {
case BIT_NOT:
// TODO: add support for bitwise operations
break;
case LOGICAL_NOT:
operator = factory.notExpression(arg0);
break;
case NEGATIVE:
operator = factory.negativeExpression(arg0);
break;
}
}
// Binary Ops
arg1 = processExpression(scope, operatorNode.getArgument(1));
if (operatorNode.numChildren() == 3) {
switch (operatorNode.getOperator()) {
case ADD:
operator = factory.addExpression(arg0, arg1);
break;
case ADD_POINTER_INT:
operator = factory.pointerAddExpression(arg0, arg1);
break;
case BIT_AND:
case BIT_OR:
case BIT_XOR:
// TODO: Add support for bitwise operations
break;
case DIVIDE:
operator = factory.divideExpression(arg0, arg1);
break;
case EQUALS:
operator = factory.equalsExpression(arg0, arg1);
break;
case GREATER_THAN:
operator = factory.lessThanExpression(arg1, arg0);
break;
case GTE:
operator = factory.lessThanOrEqualsExpression(arg1, arg0);
break;
case LEQ:
operator = factory.lessThanOrEqualsExpression(arg0, arg1);
break;
case LESS_THAN:
operator = factory.lessThanExpression(arg0, arg1);
break;
case LOGICAL_AND:
operator = factory.andExpression(arg0, arg1);
break;
case LOGICAL_OR:
operator = factory.orExpression(arg0, arg1);
break;
case MODULO:
operator = factory.moduloExpression(arg0, arg1);
break;
case MULTIPLY:
operator = factory.multiplyExpression(arg0, arg1);
break;
case NOT_EQUALS:
case SHIFT_LEFT:
case SHIFT_RIGHT:
// TODO: factory needs a notEqualsExpression() method and
// support for bit shifts
break;
case SUBTRACT:
operator = factory.subtractExpression(arg0, arg1);
break;
case SUBTRACT_POINTER_INT:
case SUBTRACT_POINTER_POINTER:
// TODO: Add support for pointer subtraction
break;
}
}
// Ternary Ops
if (operatorNode.numChildren() == 4) {
arg2 = processExpression(scope, operatorNode.getArgument(2));
operator = factory.ifThenElseExpression(arg0, arg1, arg2);
}
if (operator != null) {
operator.setSource(operatorNode.getSource());
} else {
throw new SyntaxException(operatorNode, "Unknown operator: "
+ operatorNode);
}
return operator;
}
/**
* Checks if a FunctionIF has already been created for this function and
* process. If not, one is created and added to the worklist.
*/
private void addFunction(LocalScopeIF scope,
FunctionDeclarationNodeIF functionNode) throws SyntaxException {
int pid = scope.function().process().pid();
ModelIF model = scope.model();
// TODO Fix this: definitions don't seem to be getting set. It should be
// definition = functionNode.defintion
FunctionDeclarationNodeIF definition = functionNode;
if (!functions[pid].containsKey(definition)) {
TypeIF returnType = typeBuilder.getModelType(definition
.outputType());
String name = definition.identifier().name();
SequenceNodeIF<FormalVariableDeclarationNodeIF> formals = definition
.formals();
int numFormals = formals.numChildren();
FunctionIF function = model.newFunction(model.process(pid), name,
returnType, numFormals);
// Create and add the formal parameters
for (int j = 0; j < numFormals; j++) {
FormalVariableDeclarationNodeIF currentFormal = (FormalVariableDeclarationNodeIF) formals
.child(j);
FormalVariableIF formal = model.newFormalVariable(function,
typeBuilder.getModelType(currentFormal.type()),
currentFormal.identifier().name(), j);
formal.setSource(currentFormal.getSource());
}
function.setSource(definition.getSource());
functions[pid].put(definition, function);
worklist.add(new FunctionDefinitionPair<FunctionIF, FunctionDeclarationNodeIF>(
function, definition));
}
}
/**
* Sets the target location for a statement. This is used when symbolically
* executing the model. If the statement argument is null, the location is
* assumed to be the start location for the function.
*
* @throws SyntaxException
* when there is a problem with the target location.
*/
private void setTargetLocation(StatementIF statement,
LocationIF targetLocation) throws SyntaxException {
// Statement is only null for the first statement in a function body
if (statement == null) {
targetLocation.model().setStartLocation(targetLocation.function(),
targetLocation);
} else if (statement instanceof ExitStatementPairIF) {
// If...then...else... statements can have two branches, the ends of
// which have the same target location. These end statements are
// wrapped in an ExitStatementPair.
ExitStatementPairIF exitStatement = (ExitStatementPairIF) statement;
exitStatement.model().setTargetLocation(
exitStatement.trueBranchExit(), targetLocation);
if (exitStatement.falseBranchExit() != null) {
exitStatement.model().setTargetLocation(
exitStatement.falseBranchExit(), targetLocation);
}
} else if (statement instanceof StatementSetIF) {
for (StatementIF stmt : ((StatementSetIF) statement).statements()) {
stmt.model().setTargetLocation(stmt, targetLocation);
}
} else if (statement instanceof CollectivePredecessorIF) {
CollectivePredecessorIF predecessor = (CollectivePredecessorIF) statement;
predecessor.model().setTargetLocation(predecessor.statement(),
targetLocation);
for (CollectiveAssertionIF assertion : predecessor.assertions()) {
predecessor.model().addToLocation(targetLocation, assertion,
predecessor.getExpression(assertion));
}
} else {
statement.model().setTargetLocation(statement, targetLocation);
}
}
/**
* Takes a multi-dimensional array in the AST (arrays of arrays) and returns
* the appropriate extents for the equivalent multi-dimensional array in the
* model.
*
* @throws SyntaxException
* when any array extent contains a syntax error.
*/
private ExpressionIF[] processDimensions(ScopeIF scope,
ArrayTypeNodeIF arrayTypeNodeIF) throws SyntaxException {
List<ExpressionIF> result = new Vector<ExpressionIF>();
TypeNodeIF type = arrayTypeNodeIF;
// In the AST, multidimensional arrays are arrays of arrays. Dig through
// these to get the extents in each dimension.
while (type instanceof ArrayTypeNodeIF) {
result.add(processExpression(scope,
((ArrayTypeNodeIF) type).extent()));
type = ((ArrayTypeNodeIF) type).elementType();
}
return result.toArray(new ExpressionIF[result.size()]);
}
/**
* Takes a statement and the origin location, and associates labels with the
* location.
*/
private void processLabels(StatementNodeIF statement, LocationIF location) {
LabelNodeIF label;
if (statement.labels() != null) {
for (int i = 0; i < statement.labels().numChildren(); i++) {
label = statement.labels().getSequenceChild(i);
labelledLocations.put(label, location);
}
}
}
/**
* Make each goto transition to the appropriate location.
*
* @throws SyntaxException
* when there is a problem setting the target location.
*/
private void completeGotos() throws SyntaxException {
LocationIF location;
for (NoopStatementIF noop : gotoStatements.keySet()) {
location = labelledLocations.get(gotoStatements.get(noop).label()
.reference());
setTargetLocation(noop, location);
}
}
}