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

Class StaticRegion

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.StaticRegion

All Implemented Interfaces:

Region

public class StaticRegion
extends java.lang.Object
implements Region

A class that represents a Static Region. That is a region that has been statically analyzed but has not been instantiated yet.

Field Summary

Fields

Modifier and Type	Field and Description
RemoveEarlyReturns.ReturnResult	earlyReturnResult Holds the early return result that is computed by the RemoveEarlyReturns pass called in VeritestingListener
int	endIns this is the last instruction where SPF needs to start from after the region
Table	inputTable An environment table that defines the input vars to the region.
com.ibm.wala.ssa.IR	ir IR of the method that the StaticRegion belongs to.
boolean	isMethodRegion A boolean that indicates whether this is a conditional region,i.e, a region that begins with an if instruction, or a method region, i.e., a region that is summarizing the whole method.
int	maxDepth Holds the total number of IfThenElseStmts present in this static region
Table	outputTable An Environment table that holds the output of the region that needs to be popluated later to SPF upon successful veritesting.
Table	slotParamTable An Environment table that holds a mapping from vars to either their stack slot position, in case of conditional regions, or to their parameter number in case of a MethodRegion.
WalaVarExpr	stackOutput Holds the expression that should be written out to the stack
Stmt	staticStmt Statement of the region.
long	totalNumPaths Holds the total number of execution paths that can be taken through this region
VarTypeTable	varTypeTable An environment table that holds the types of local variables defined inside the region.

Constructor Summary

Constructors

Constructor and Description
StaticRegion(Stmt staticStmt, com.ibm.wala.ssa.IR ir, java.lang.Boolean isMethodRegion, int endIns, com.ibm.wala.ssa.ISSABasicBlock startingBlock, com.ibm.wala.ssa.ISSABasicBlock terminus, RemoveEarlyReturns.ReturnResult returnResult)
StaticRegion(Stmt staticStmt, StaticRegion staticRegion, RemoveEarlyReturns.ReturnResult returnResult)

Method Summary

Modifier and Type	Method and Description
private RegionBoundaryOutput	computeRegionBoundary(Stmt stmt) This computes the region boundary in case of conditional region, to determine the first use and the first and last def variables inside the region.
private java.lang.Integer	findLastVar(java.lang.Integer firstDef, java.lang.Integer firstUse, java.lang.Integer lastDef, java.lang.Integer lastUse)

Methods inherited from class java.lang.Object

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

Field Detail

staticStmt

public final Stmt staticStmt

Statement of the region.

ir

public final com.ibm.wala.ssa.IR ir

IR of the method that the StaticRegion belongs to.

slotParamTable

public final Table slotParamTable

An Environment table that holds a mapping from vars to either their stack slot position, in case of conditional regions, or to their parameter number in case of a MethodRegion.

outputTable

public final Table outputTable

An Environment table that holds the output of the region that needs to be popluated later to SPF upon successful veritesting. The output is computed as the last Phi for every stack slot.

endIns

public final int endIns

this is the last instruction where SPF needs to start from after the region

isMethodRegion

public final boolean isMethodRegion

A boolean that indicates whether this is a conditional region,i.e, a region that begins with an if instruction, or a method region, i.e., a region that is summarizing the whole method.

inputTable

public final Table inputTable

An environment table that defines the input vars to the region. it defines the mapping from slot/param to var

varTypeTable

public final VarTypeTable varTypeTable

An environment table that holds the types of local variables defined inside the region.

maxDepth

public int maxDepth

Holds the total number of IfThenElseStmts present in this static region

totalNumPaths

public long totalNumPaths

Holds the total number of execution paths that can be taken through this region

earlyReturnResult

public RemoveEarlyReturns.ReturnResult earlyReturnResult

Holds the early return result that is computed by the RemoveEarlyReturns pass called in VeritestingListener

stackOutput

public WalaVarExpr stackOutput

Holds the expression that should be written out to the stack

Constructor Detail

StaticRegion

public StaticRegion(Stmt staticStmt,
                    com.ibm.wala.ssa.IR ir,
                    java.lang.Boolean isMethodRegion,
                    int endIns,
                    com.ibm.wala.ssa.ISSABasicBlock startingBlock,
                    com.ibm.wala.ssa.ISSABasicBlock terminus,
                    RemoveEarlyReturns.ReturnResult returnResult)
             throws StaticRegionException

Parameters:

staticStmt: - Ranger IR statement that summarizes this static region

ir: - Wala IR for the method which contains this StaticRegion

isMethodRegion: - boolean value that if true indicates that this StaticRegion is for a method summary

endIns: - Ending instruction's bytecode offset for this static region

startingBlock: - if given, startingBlock is used for constructing definitions for variables used in the condition of the staticStmt, if the StaticRegion is for a multi-path region. startingBlock should correspond to the beginning block of the region. If unavailable, it can be given a null value.

Throws:

StaticRegionException

StaticRegion

public StaticRegion(Stmt staticStmt,
                    StaticRegion staticRegion,
                    RemoveEarlyReturns.ReturnResult returnResult)
             throws StaticRegionException

Throws:

StaticRegionException

Method Detail

findLastVar

private java.lang.Integer findLastVar(java.lang.Integer firstDef,
                                      java.lang.Integer firstUse,
                                      java.lang.Integer lastDef,
                                      java.lang.Integer lastUse)

computeRegionBoundary

private RegionBoundaryOutput computeRegionBoundary(Stmt stmt)

This computes the region boundary in case of conditional region, to determine the first use and the first and last def variables inside the region.

Parameters:

stmt - Statement of the region.

Returns:

A pair of pairs, ( (first-use, last-use), (first-def, last-def) ) variables in the region.