gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution

Class SubstitutionVisitor

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

gov.nasa.jpf.symbc.veritesting.ast.visitors.FixedPointAstMapVisitor

gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

All Implemented Interfaces:

AstVisitor<Stmt>, ExprVisitor<za.ac.sun.cs.green.expr.Expression>

public class SubstitutionVisitor
extends FixedPointAstMapVisitor

The Substitution Transformation is responsible for replacing all vars with their symbolic values if found, as well as the substitution of all constant vars. Substitution Transformation is done in a general way depending on the type of the StaticRegion. Mainly by allowing the substitution to replace variables with values by looking up the ValueSymbolTable, where the ValueSymbolTable is filled depending on the type of the region. If the region is not a method region, the ValueSymbolTable is filled by a priori pass where all "input" var values are discovered by inquiring SPF for their stack slot attribute. If the region is a method region then the ValueSymbolTable is filled up by the caller by filling up vars/values of the parameters. In this transformation, constants are also discovered as part of the process.

Field Summary

Fields

Modifier and Type	Field and Description
DynamicRegion	dynRegion
private ExprVisitorAdapter<za.ac.sun.cs.green.expr.Expression>	eva
private java.util.ArrayList<com.ibm.wala.types.MethodReference>	invocationStack
private static java.util.Set<com.ibm.wala.types.MethodReference>	noFurtherInlines
private Pair<com.ibm.wala.types.MethodReference,java.lang.Integer>	recursiveScope
private boolean	spfCasePath This is used to identify if a path had spfCase instruction that requires prouning the path.
gov.nasa.jpf.vm.ThreadInfo	ti
private boolean	useVarTable

Fields inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.FixedPointAstMapVisitor

firstException, instantiatedRegion, somethingChanged

Fields inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

exprVisitor

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SubstitutionVisitor(gov.nasa.jpf.vm.ThreadInfo ti, DynamicRegion dynRegion, DynamicTable valueSymbolTable, boolean useVarTable, java.util.ArrayList<com.ibm.wala.types.MethodReference> invocationStack)

Method Summary

Modifier and Type	Method and Description
private Pair<Stmt,DynamicTable>	attemptHighOrderRegion(DynamicRegion methodRegion, DynamicTable hgOrdValueSymbolTable) Attempts to substitute in a high order region.
private java.lang.String	convertToJavaName(java.lang.String currClassName)
static SubstitutionVisitor	create(gov.nasa.jpf.vm.ThreadInfo ti, DynamicRegion dynRegion, int iterationNumber, boolean useVarTable)
DynamicRegion	execute() Executes substitution over a non-method region.
private static DynamicTable	fillValueSymbolTable(gov.nasa.jpf.vm.ThreadInfo ti, DynamicRegion dynRegion) Fills out the values of all vars that could be discovered in the region.
private Pair<java.lang.String,StaticRegion>	findMethodRegion(gov.nasa.jpf.vm.ThreadInfo ti, InvokeInstruction c) Attempts to find a mapping MethodRegion.
boolean	getChange()
private Pair<Stmt,za.ac.sun.cs.green.expr.Expression>	getStmtRetExp(Stmt stmt) Iterates over the Stmt to get the return statement seperated out of the reset of the statements.
DynamicTable	getValueSymbolTable()
private boolean	isAllowedRecursiveCall(com.ibm.wala.types.MethodReference calledTarget)
private boolean	isRecursiveCall(com.ibm.wala.types.MethodReference calledTarget)
private Pair<java.lang.String,StaticRegion>	jitFindMethodRegion(gov.nasa.jpf.vm.ThreadInfo ti, InvokeInstruction c) Attempts to find a mapping MethodRegion.
void	setSomethingChanged(boolean change)
void	setValueSymbolTable(DynamicTable valueSymbolTable)
Stmt	visit(ArrayLengthInstruction c)
Stmt	visit(ArrayLoadInstruction c)
Stmt	visit(ArrayStoreInstruction c)
Stmt	visit(AssignmentStmt a)
Stmt	visit(GetInstruction c)
Stmt	visit(IfThenElseStmt c) While visiting IfThenElse, it is responsible for resetting the spfCasePath, if on one path of its branches an SPFCase instruction was discoverd, such as throw or object creation, if this happens then along that path, there should be no high order regions inlined.
Stmt	visit(InvokeInstruction c) Visits an InvokeInstruction by attempting to inline static method regions.
Stmt	visit(NewInstruction c)
Stmt	visit(PhiInstruction c)
Stmt	visit(ReturnInstruction c)
Stmt	visit(ThrowInstruction c)

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.FixedPointAstMapVisitor

getFirstException

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit, visit, visit, visit, visit, visit, visit

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

invocationStack

private final java.util.ArrayList<com.ibm.wala.types.MethodReference> invocationStack

eva

private ExprVisitorAdapter<za.ac.sun.cs.green.expr.Expression> eva

dynRegion

public final DynamicRegion dynRegion

ti

public final gov.nasa.jpf.vm.ThreadInfo ti

useVarTable

private boolean useVarTable

recursiveScope

private Pair<com.ibm.wala.types.MethodReference,java.lang.Integer> recursiveScope

noFurtherInlines

private static java.util.Set<com.ibm.wala.types.MethodReference> noFurtherInlines

spfCasePath

private boolean spfCasePath

This is used to identify if a path had spfCase instruction that requires prouning the path. The flag is used to stop embedding high order region along that path.

Constructor Detail

SubstitutionVisitor

private SubstitutionVisitor(gov.nasa.jpf.vm.ThreadInfo ti,
                            DynamicRegion dynRegion,
                            DynamicTable valueSymbolTable,
                            boolean useVarTable,
                            java.util.ArrayList<com.ibm.wala.types.MethodReference> invocationStack)

Method Detail

setSomethingChanged

public void setSomethingChanged(boolean change)

getChange

public boolean getChange()

Overrides:

getChange in class FixedPointAstMapVisitor

setValueSymbolTable

public void setValueSymbolTable(DynamicTable valueSymbolTable)

getValueSymbolTable

public DynamicTable getValueSymbolTable()

visit

public Stmt visit(AssignmentStmt a)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(ArrayLoadInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(ArrayStoreInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(GetInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(ArrayLengthInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(NewInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(ThrowInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(IfThenElseStmt c)

While visiting IfThenElse, it is responsible for resetting the spfCasePath, if on one path of its branches an SPFCase instruction was discoverd, such as throw or object creation, if this happens then along that path, there should be no high order regions inlined. And when the branch returns the flag needs to be reset and we need to explore the other side of the branch.

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

Parameters:

c -

Returns:

visit

public Stmt visit(ReturnInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(PhiInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(InvokeInstruction c)

Visits an InvokeInstruction by attempting to inline static method regions.

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

Parameters:

c - Invoke Instruction to be visited.

Returns:

A new statement that might include an inlined method region for static invocations.

isRecursiveCall

private boolean isRecursiveCall(com.ibm.wala.types.MethodReference calledTarget)

isAllowedRecursiveCall

private boolean isAllowedRecursiveCall(com.ibm.wala.types.MethodReference calledTarget)

attemptHighOrderRegion

private Pair<Stmt,DynamicTable> attemptHighOrderRegion(DynamicRegion methodRegion,
                                                       DynamicTable hgOrdValueSymbolTable)
                                                throws StaticRegionException

Attempts to substitute in a high order region.

Parameters:

methodRegion - MethodRegion where the substitution is going to be attempted.

hgOrdValueSymbolTable - Value symbol table for te MethodRegion, usually populated with the parameters.

Returns:

A pair of substituted statement for the high order region as well as its VarTypeTable.

Throws:

StaticRegionException

getStmtRetExp

private Pair<Stmt,za.ac.sun.cs.green.expr.Expression> getStmtRetExp(Stmt stmt)

Iterates over the Stmt to get the return statement seperated out of the reset of the statements.

Parameters:

stmt - A statement that ends with a return expression.

Returns:

A pair of Statement and retrun Statment.

jitFindMethodRegion

private Pair<java.lang.String,StaticRegion> jitFindMethodRegion(gov.nasa.jpf.vm.ThreadInfo ti,
                                                                InvokeInstruction c)
                                                         throws StaticRegionException

Attempts to find a mapping MethodRegion.

Parameters:

c - Current invoke instruction.

Returns:

A pair of the key and the methodRegion if a matching could be found.

Throws:

StaticRegionException

findMethodRegion

private Pair<java.lang.String,StaticRegion> findMethodRegion(gov.nasa.jpf.vm.ThreadInfo ti,
                                                             InvokeInstruction c)

Attempts to find a mapping MethodRegion.

Parameters:

c - Current invoke instruction.

Returns:

A pair of the key and the methodRegion if a matching could be found.

convertToJavaName

private java.lang.String convertToJavaName(java.lang.String currClassName)

fillValueSymbolTable

private static DynamicTable fillValueSymbolTable(gov.nasa.jpf.vm.ThreadInfo ti,
                                                 DynamicRegion dynRegion)
                                          throws StaticRegionException

Fills out the values of all vars that could be discovered in the region.

Parameters:

ti - Current executing thread.

dynRegion - DynamicRegion for which the ValueSymbolTable is going to be created.

Returns:

Populated ValueSymbolTable for variables in the static region.

Throws:

StaticRegionException

execute

public DynamicRegion execute()

Executes substitution over a non-method region.

Specified by:

execute in class FixedPointAstMapVisitor

Returns:

A Dynamic Region that has been substituted by symbolic or concerete values for inputs as well as constants being substituted.

create

public static SubstitutionVisitor create(gov.nasa.jpf.vm.ThreadInfo ti,
                                         DynamicRegion dynRegion,
                                         int iterationNumber,
                                         boolean useVarTable)