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

Class DynamicRegion

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicRegion

All Implemented Interfaces:

Region

public class DynamicRegion
extends java.lang.Object
implements Region

This class represents a DynamicRegion, that is, a StaticRegion that has been processed dynamically, this is done initially through uniquness transformation then later with the substitution and other transformations. A main difference in this data structure than the StaticRegion is that, the dynamic region now holds environment tables that have a unique name for every variable used.

Field Summary

Fields

Modifier and Type	Field and Description
ArrayExpressions	arrayOutputs Holds output expressions to be written into arrays
DynamicTable<za.ac.sun.cs.green.expr.Expression>	constantsTable
Stmt	dynStmt A statement that represents the region after instantiation.
RemoveEarlyReturns.ReturnResult	earlyReturnResult
int	endIns Identifies the End Position that the region is summarizing and which also SPF to resume from.
FieldRefTypeTable	fieldRefTypeTable An environment table that holds the types of all field variables, referenced by FieldRefVarExpr objects, in the region.
DynamicTable	inputTable A table that holds inputs to the region.
com.ibm.wala.ssa.IR	ir This holds the static version of the region that is matching this instantiation.
boolean	isMethodRegion Identifies if the dynamic region corresponds to a region that starts with a condition, or is it enclosing the summary of the whole method.
int	maxDepth Holds the total number of IfThenElseStmts present in this static region
DynamicOutputTable	outputTable An environment able that holds the vars that needs to be populate their summarized output to SPF.
FieldSubscriptMap	psm Holds path subscript map for field references in the region
za.ac.sun.cs.green.expr.Expression	regionSummary This holds the region greeen expression after all transformations are done.
DynamicTable	slotParamTable A table that holds the mapping of vars in the dynamic statement to their corresponding stack slot.
SPFCaseList	spfCaseList Holds all SPFCases predicates that are not statically summarized and are left for SPF to explore.
za.ac.sun.cs.green.expr.Expression	spfPredicateSummary This carries the green expression under which partial evaluation will be done with SPF.
WalaVarExpr	stackOutput Holds the expression that should be written out to the stack
long	totalNumPaths Holds the total number of execution paths that can be taken through this region
static int	uniqueCounter unique counter used to maintain uniqueness among vars in case a region was used multiple times, like in a loop.
DynamicTable	varTypeTable An environment table that holds the types of all Wala vars in the region.

Constructor Summary

Constructors

Constructor and Description
DynamicRegion(DynamicRegion oldDynRegion, Stmt dynStmt, SPFCaseList spfCaseList, za.ac.sun.cs.green.expr.Expression regionSummary, za.ac.sun.cs.green.expr.Expression spfRegionSummary, RemoveEarlyReturns.ReturnResult earlyReturnResult)
DynamicRegion(StaticRegion staticRegion, Stmt dynStmt, int uniqueNum, RemoveEarlyReturns.ReturnResult returnResult) Constructor that is used to create a dynamic region out of a static region.

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

uniqueCounter

public static int uniqueCounter

unique counter used to maintain uniqueness among vars in case a region was used multiple times, like in a loop.

dynStmt

public final Stmt dynStmt

A statement that represents the region after instantiation.

slotParamTable

public final DynamicTable slotParamTable

A table that holds the mapping of vars in the dynamic statement to their corresponding stack slot.

inputTable

public final DynamicTable inputTable

A table that holds inputs to the region.

outputTable

public final DynamicOutputTable outputTable

An environment able that holds the vars that needs to be populate their summarized output to SPF.

ir

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

This holds the static version of the region that is matching this instantiation.

varTypeTable

public final DynamicTable varTypeTable

An environment table that holds the types of all Wala vars in 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

fieldRefTypeTable

public final FieldRefTypeTable fieldRefTypeTable

An environment table that holds the types of all field variables, referenced by FieldRefVarExpr objects, in the region. This table also holds the types of all array references, referenced by ArrayRefVarExpr objects, in the region.

psm

public FieldSubscriptMap psm

Holds path subscript map for field references in the region

endIns

public final int endIns

Identifies the End Position that the region is summarizing and which also SPF to resume from.

isMethodRegion

public final boolean isMethodRegion

Identifies if the dynamic region corresponds to a region that starts with a condition, or is it enclosing the summary of the whole method.

spfCaseList

public final SPFCaseList spfCaseList

Holds all SPFCases predicates that are not statically summarized and are left for SPF to explore.

regionSummary

public final za.ac.sun.cs.green.expr.Expression regionSummary

This holds the region greeen expression after all transformations are done.

spfPredicateSummary

public final za.ac.sun.cs.green.expr.Expression spfPredicateSummary

This carries the green expression under which partial evaluation will be done with SPF.

arrayOutputs

public ArrayExpressions arrayOutputs

Holds output expressions to be written into arrays

constantsTable

public DynamicTable<za.ac.sun.cs.green.expr.Expression> constantsTable

earlyReturnResult

public RemoveEarlyReturns.ReturnResult earlyReturnResult

stackOutput

public WalaVarExpr stackOutput

Holds the expression that should be written out to the stack

Constructor Detail

DynamicRegion

public DynamicRegion(DynamicRegion oldDynRegion,
                     Stmt dynStmt,
                     SPFCaseList spfCaseList,
                     za.ac.sun.cs.green.expr.Expression regionSummary,
                     za.ac.sun.cs.green.expr.Expression spfRegionSummary,
                     RemoveEarlyReturns.ReturnResult earlyReturnResult)

DynamicRegion

public DynamicRegion(StaticRegion staticRegion,
                     Stmt dynStmt,
                     int uniqueNum,
                     RemoveEarlyReturns.ReturnResult returnResult)
              throws StaticRegionException,
                     java.lang.CloneNotSupportedException

Constructor that is used to create a dynamic region out of a static region.

Parameters:

staticRegion -

dynStmt -

uniqueNum -

Throws:

StaticRegionException

java.lang.CloneNotSupportedException