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

Class CreateStaticRegions

java.lang.Object

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

public class CreateStaticRegions
extends java.lang.Object

This class creates our structure IR from the WALA SSA form, this is basically done by decompiling DAGs within a Java program.

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Map<PhiEdge,java.util.List<PhiCondition>>	blockConditionMap This is used for Phi instructions, where each edge in the graph is mapped to a list of conditions that represents the path up till that edge.
private java.util.Deque<PhiCondition>	currentCondition Keeps track of the current conditions/depth while visiting nodes in the graph.
private com.ibm.wala.util.graph.Graph<com.ibm.wala.ssa.ISSABasicBlock>	domTree
private java.util.Map<com.ibm.wala.ssa.ISSABasicBlock,com.ibm.wala.ssa.ISSABasicBlock>	elseSuccessor
private com.ibm.wala.ssa.IR	ir
(package private) java.util.Deque<PhiCondition>	jitCurrentCondition
private java.util.Set<com.ibm.wala.ssa.ISSABasicBlock>	jitVisitedBlocks
private java.util.HashSet<x10.wala.util.NatLoop>	loops
private java.util.HashMap<com.ibm.wala.ssa.ISSABasicBlock,java.lang.Integer>	seenLoopStartSet
private java.util.Map<com.ibm.wala.ssa.ISSABasicBlock,za.ac.sun.cs.green.expr.Expression>	thenCondition for complex conditions, we want to record the then condition and successors.
private java.util.Map<com.ibm.wala.ssa.ISSABasicBlock,Stmt>	thenConditionSetup
private java.util.Map<com.ibm.wala.ssa.ISSABasicBlock,com.ibm.wala.ssa.ISSABasicBlock>	thenSuccessor
private java.util.HashMap<java.lang.String,StaticRegion>	veritestingRegions
private java.util.Set<com.ibm.wala.ssa.ISSABasicBlock>	visitedBlocks For memoization, so we don't visit the same blocks over and over.

Constructor Summary

Constructors

Constructor and Description
CreateStaticRegions(com.ibm.wala.ssa.IR ir, java.util.HashSet<x10.wala.util.NatLoop> loops)

Method Summary

Modifier and Type	Method and Description
private Stmt	attemptConditionalSubregion(com.ibm.wala.ssa.SSACFG cfg, com.ibm.wala.ssa.ISSABasicBlock startingBlock, com.ibm.wala.ssa.ISSABasicBlock terminus) Attempts to translate conditional region and translates it to RangerIR statement
Stmt	attemptMethodAndMultiPathRegions(com.ibm.wala.ssa.SSACFG cfg, com.ibm.wala.ssa.ISSABasicBlock currentBlock, com.ibm.wala.ssa.ISSABasicBlock endingBlock) This methods attempt to connect discover multi-path regions and connecting them to recover the method as well.
private Stmt	attemptMethodSubregion(com.ibm.wala.ssa.SSACFG cfg, com.ibm.wala.ssa.ISSABasicBlock startingBlock, com.ibm.wala.ssa.ISSABasicBlock endingBlock) Attempts to translate a method region to a RangerIR statement.
Stmt	attemptSubregionRec(com.ibm.wala.ssa.SSACFG cfg, com.ibm.wala.ssa.ISSABasicBlock currentBlock, com.ibm.wala.ssa.ISSABasicBlock endingBlock) Translates from current block but does not include the ending block.
private Stmt	conditionalBranch(com.ibm.wala.ssa.SSACFG cfg, com.ibm.wala.ssa.ISSABasicBlock currentBlock, com.ibm.wala.ssa.ISSABasicBlock terminus) Attempts to translate a conditional part of the cfg to IfThenElse statement in RangerIR.
Stmt	conjoin(Stmt stmt1, Stmt stmt2) This creates a composition statement between two statements
static java.lang.String	constructMethodIdentifier(com.ibm.wala.ssa.ISSABasicBlock blk)
static java.lang.String	constructMethodIdentifier(java.lang.String methodSignature) Create the key of a Method region.
static java.lang.String	constructRegionIdentifier(com.ibm.wala.ssa.IR ir, com.ibm.wala.ssa.ISSABasicBlock blk) Create the key of a conditional region, by using the name as well as the bytecode offset of the last instruction in the first block that starts the region.
static java.lang.String	constructRegionIdentifier(java.lang.String methodSignature, int offset)
private Pair<za.ac.sun.cs.green.expr.Expression,Stmt>	createComplexIfCondition(com.ibm.wala.ssa.ISSABasicBlock child, com.ibm.wala.ssa.ISSABasicBlock entry) Re-constructs a complex condition for an if/then/else condition.
void	createStructuredConditionalRegions(java.util.HashMap<java.lang.String,StaticRegion> veritestingRegions)
private void	createStructuredConditionalRegions(com.ibm.wala.ssa.ISSABasicBlock currentBlock, com.ibm.wala.ssa.ISSABasicBlock endingBlock, java.util.HashMap<java.lang.String,StaticRegion> veritestingRegions) This class walks through method, attempting to find conditional veritesting regions
void	createStructuredMethodRegion(java.util.HashMap<java.lang.String,StaticRegion> veritestingRegions) This class walks through method, attempting to find method regions veritesting regions
private void	findConditionalSuccessors(com.ibm.wala.ssa.ISSABasicBlock entry, com.ibm.wala.ssa.ISSABasicBlock terminus) Attempts to discover conditional successors on the then or the else side of a conditional block.
private void	findSelfContainedSubgraphs(com.ibm.wala.ssa.ISSABasicBlock entry, com.ibm.wala.ssa.ISSABasicBlock current, com.ibm.wala.ssa.ISSABasicBlock terminus, java.util.Set<com.ibm.wala.ssa.ISSABasicBlock> subgraphs) This searches a self contained subgraph inside the region.
private com.ibm.wala.ssa.ISSABasicBlock	getIDom(com.ibm.wala.ssa.ISSABasicBlock elem) Gets the immediate dominator of a block.
boolean	isBranch(com.ibm.wala.ssa.SSACFG cfg, com.ibm.wala.ssa.ISSABasicBlock block)
private boolean	isSelfContainedSubgraph(com.ibm.wala.ssa.ISSABasicBlock entry, com.ibm.wala.ssa.ISSABasicBlock terminus) This method checks to see whether each node in a subgraph up to a terminus has a subgraph.
private Stmt	jitAttemptConditionalSubregion(com.ibm.wala.ssa.SSACFG cfg, com.ibm.wala.ssa.ISSABasicBlock startingBlock, com.ibm.wala.ssa.ISSABasicBlock terminus)
Pair<Stmt,java.util.Map<PhiEdge,java.util.List<PhiCondition>>>	jitAttemptSubregionRec(com.ibm.wala.ssa.SSACFG cfg, com.ibm.wala.ssa.ISSABasicBlock currentBlock, com.ibm.wala.ssa.ISSABasicBlock endingBlock) Translates from current block but does not include the ending block.
private Stmt	jitConditionalBranch(com.ibm.wala.ssa.SSACFG cfg, com.ibm.wala.ssa.ISSABasicBlock currentBlock, com.ibm.wala.ssa.ISSABasicBlock terminus, java.util.Map<PhiEdge,java.util.List<PhiCondition>> insertedBlockConditionMap) Attempts to translate a conditional part of the cfg to IfThenElse statement in RangerIR.
void	jitCreateStructuredRegion(java.util.HashMap<java.lang.String,StaticRegion> veritestingRegions) This class walks through method, attempting to recover a method region and also recover all multi-path regions inside of it.
private Stmt	jitTranslateTruncatedConditionalBlock(com.ibm.wala.ssa.ISSABasicBlock currentBlock)
private Stmt	jitTranslateTruncatedFinalBlock(com.ibm.wala.ssa.ISSABasicBlock currentBlock)
private Stmt	jitTranslateTruncatedFinalBlock2(com.ibm.wala.ssa.ISSABasicBlock currentBlock, java.util.Map<PhiEdge,java.util.List<PhiCondition>> insertedBlockConditionMap, java.util.Deque<PhiCondition> insertedCurrentCondition)
private boolean	phiBlock(com.ibm.wala.ssa.ISSABasicBlock currentBlock)
private void	populateMissedRegions(com.ibm.wala.ssa.SSACFG cfg, com.ibm.wala.ssa.ISSABasicBlock currentBlock, com.ibm.wala.ssa.ISSABasicBlock endingBlock)
private void	reset()
private Stmt	translateInternalBlock(com.ibm.wala.ssa.ISSABasicBlock currentBlock) This translates "internal" blocks inside the region, these are blocks that are not the begining or the end of the region.
private Stmt	translateTruncatedFinalBlock(com.ibm.wala.ssa.ISSABasicBlock currentBlock) This translate the last block in an identified region by visiting all its instructions and creating a Gamma if a Phi instruction was found.

Methods inherited from class java.lang.Object

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

Field Detail

seenLoopStartSet

private java.util.HashMap<com.ibm.wala.ssa.ISSABasicBlock,java.lang.Integer> seenLoopStartSet

veritestingRegions

private java.util.HashMap<java.lang.String,StaticRegion> veritestingRegions

loops

private final java.util.HashSet<x10.wala.util.NatLoop> loops

ir

private com.ibm.wala.ssa.IR ir

domTree

private com.ibm.wala.util.graph.Graph<com.ibm.wala.ssa.ISSABasicBlock> domTree

blockConditionMap

private java.util.Map<PhiEdge,java.util.List<PhiCondition>> blockConditionMap

This is used for Phi instructions, where each edge in the graph is mapped to a list of conditions that represents the path up till that edge.

jitCurrentCondition

java.util.Deque<PhiCondition> jitCurrentCondition

jitVisitedBlocks

private java.util.Set<com.ibm.wala.ssa.ISSABasicBlock> jitVisitedBlocks

currentCondition

private java.util.Deque<PhiCondition> currentCondition

Keeps track of the current conditions/depth while visiting nodes in the graph.

thenCondition

private java.util.Map<com.ibm.wala.ssa.ISSABasicBlock,za.ac.sun.cs.green.expr.Expression> thenCondition

for complex conditions, we want to record the then condition and successors.

thenSuccessor

private java.util.Map<com.ibm.wala.ssa.ISSABasicBlock,com.ibm.wala.ssa.ISSABasicBlock> thenSuccessor

elseSuccessor

private java.util.Map<com.ibm.wala.ssa.ISSABasicBlock,com.ibm.wala.ssa.ISSABasicBlock> elseSuccessor

thenConditionSetup

private java.util.Map<com.ibm.wala.ssa.ISSABasicBlock,Stmt> thenConditionSetup

visitedBlocks

private java.util.Set<com.ibm.wala.ssa.ISSABasicBlock> visitedBlocks

For memoization, so we don't visit the same blocks over and over.

Constructor Detail

CreateStaticRegions

public CreateStaticRegions(com.ibm.wala.ssa.IR ir,
                           java.util.HashSet<x10.wala.util.NatLoop> loops)

Method Detail

constructRegionIdentifier

public static java.lang.String constructRegionIdentifier(java.lang.String methodSignature,
                                                         int offset)

constructRegionIdentifier

public static java.lang.String constructRegionIdentifier(com.ibm.wala.ssa.IR ir,
                                                         com.ibm.wala.ssa.ISSABasicBlock blk)

Create the key of a conditional region, by using the name as well as the bytecode offset of the last instruction in the first block that starts the region.

Parameters:

ir - IR of the staticRegion.

blk - The first block that identifies the begining of the region.

Returns:

A string that is used as a key for the region.

constructMethodIdentifier

public static java.lang.String constructMethodIdentifier(java.lang.String methodSignature)

Create the key of a Method region.

Parameters:

methodSignature - Signature of a method.

Returns:

A string that is used as a key for the region.

constructMethodIdentifier

public static java.lang.String constructMethodIdentifier(com.ibm.wala.ssa.ISSABasicBlock blk)

reset

private void reset()

isBranch

public boolean isBranch(com.ibm.wala.ssa.SSACFG cfg,
                        com.ibm.wala.ssa.ISSABasicBlock block)

conjoin

public Stmt conjoin(Stmt stmt1,
                    Stmt stmt2)

This creates a composition statement between two statements

Parameters:

stmt1 - First statement to be used in a composition.

stmt2 - Second statement to be used in a composition.

Returns:

A composition statement in RangerIR.

translateTruncatedFinalBlock

private Stmt translateTruncatedFinalBlock(com.ibm.wala.ssa.ISSABasicBlock currentBlock)
                                   throws StaticRegionException

This translate the last block in an identified region by visiting all its instructions and creating a Gamma if a Phi instruction was found.

Parameters:

currentBlock - The last block in the region.

Returns:

A statement in RangerIR that represents the last block in the region.

Throws:

StaticRegionException

jitTranslateTruncatedFinalBlock2

private Stmt jitTranslateTruncatedFinalBlock2(com.ibm.wala.ssa.ISSABasicBlock currentBlock,
                                              java.util.Map<PhiEdge,java.util.List<PhiCondition>> insertedBlockConditionMap,
                                              java.util.Deque<PhiCondition> insertedCurrentCondition)
                                       throws StaticRegionException

Throws:

StaticRegionException

translateInternalBlock

private Stmt translateInternalBlock(com.ibm.wala.ssa.ISSABasicBlock currentBlock)
                             throws StaticRegionException

This translates "internal" blocks inside the region, these are blocks that are not the begining or the end of the region.

Parameters:

currentBlock - Current block that needs to be translated.

Returns:

A statement in RangerIR that represents the translated statement.

Throws:

StaticRegionException - An exception that indicates a problem in the translation.

jitTranslateTruncatedFinalBlock

private Stmt jitTranslateTruncatedFinalBlock(com.ibm.wala.ssa.ISSABasicBlock currentBlock)
                                      throws StaticRegionException

Throws:

StaticRegionException

jitTranslateTruncatedConditionalBlock

private Stmt jitTranslateTruncatedConditionalBlock(com.ibm.wala.ssa.ISSABasicBlock currentBlock)
                                            throws StaticRegionException

Parameters:

currentBlock -

Returns:

Throws:

StaticRegionException

getIDom

private com.ibm.wala.ssa.ISSABasicBlock getIDom(com.ibm.wala.ssa.ISSABasicBlock elem)

Gets the immediate dominator of a block.

Parameters:

elem - Block for which we want to find its immediate dominator.

Returns:

Immediate dominator of a block.

isSelfContainedSubgraph

private boolean isSelfContainedSubgraph(com.ibm.wala.ssa.ISSABasicBlock entry,
                                        com.ibm.wala.ssa.ISSABasicBlock terminus)
                                 throws StaticRegionException

This method checks to see whether each node in a subgraph up to a terminus has a subgraph.

Parameters:

entry - Entry block, from which a search/check starts.

terminus - End block, where search/check should terminates.

Returns:

True if the entry to the terminus is a self contained subregion.

Throws:

StaticRegionException - Exception that indicates something went wrong during computation.

findSelfContainedSubgraphs

private void findSelfContainedSubgraphs(com.ibm.wala.ssa.ISSABasicBlock entry,
                                        com.ibm.wala.ssa.ISSABasicBlock current,
                                        com.ibm.wala.ssa.ISSABasicBlock terminus,
                                        java.util.Set<com.ibm.wala.ssa.ISSABasicBlock> subgraphs)
                                 throws StaticRegionException

This searches a self contained subgraph inside the region.

Throws:

StaticRegionException

createComplexIfCondition

private Pair<za.ac.sun.cs.green.expr.Expression,Stmt> createComplexIfCondition(com.ibm.wala.ssa.ISSABasicBlock child,
                                                                               com.ibm.wala.ssa.ISSABasicBlock entry)
                                                                        throws StaticRegionException

Re-constructs a complex condition for an if/then/else condition.

MWW: 9/10/2018. The assertion: (child.getNumber() > entry.getNumber()) at the top of this function is too restrictive. The issue is that we assume all parents are within the path between entry and child. This is true for "top-level" Java if/then/else expressions, but if we wish to construct regions from within complex conditions, it no longer holds.

There are two ways to examine this case: we can

Throws:

StaticRegionException

findConditionalSuccessors

private void findConditionalSuccessors(com.ibm.wala.ssa.ISSABasicBlock entry,
                                       com.ibm.wala.ssa.ISSABasicBlock terminus)
                                throws StaticRegionException

Attempts to discover conditional successors on the then or the else side of a conditional block.

Parameters:

entry - Entry block.

terminus - End blcok where search needs to stop

Throws:

StaticRegionException - An Exception that indicates that something went wrong during computation.

attemptSubregionRec

public Stmt attemptSubregionRec(com.ibm.wala.ssa.SSACFG cfg,
                                com.ibm.wala.ssa.ISSABasicBlock currentBlock,
                                com.ibm.wala.ssa.ISSABasicBlock endingBlock)
                         throws StaticRegionException

Translates from current block but does not include the ending block.

Parameters:

cfg - Control flow graph.

currentBlock - Current block

endingBlock - End block, this is not included in this translation.

Returns:

a statement that represents this part of cfg in RangerIR.

Throws:

StaticRegionException

conditionalBranch

private Stmt conditionalBranch(com.ibm.wala.ssa.SSACFG cfg,
                               com.ibm.wala.ssa.ISSABasicBlock currentBlock,
                               com.ibm.wala.ssa.ISSABasicBlock terminus)
                        throws StaticRegionException

Attempts to translate a conditional part of the cfg to IfThenElse statement in RangerIR.

Parameters:

cfg - Current control flow graph.

currentBlock - current block

terminus - End block.

Returns:

A RangerIR IfThenElse statement.

Throws:

StaticRegionException

jitConditionalBranch

private Stmt jitConditionalBranch(com.ibm.wala.ssa.SSACFG cfg,
                                  com.ibm.wala.ssa.ISSABasicBlock currentBlock,
                                  com.ibm.wala.ssa.ISSABasicBlock terminus,
                                  java.util.Map<PhiEdge,java.util.List<PhiCondition>> insertedBlockConditionMap)
                           throws StaticRegionException

Attempts to translate a conditional part of the cfg to IfThenElse statement in RangerIR.

Parameters:

cfg - Current control flow graph.

currentBlock - current block

terminus - End block.

Returns:

A RangerIR IfThenElse statement.

Throws:

StaticRegionException

jitAttemptSubregionRec

public Pair<Stmt,java.util.Map<PhiEdge,java.util.List<PhiCondition>>> jitAttemptSubregionRec(com.ibm.wala.ssa.SSACFG cfg,
                                                                                             com.ibm.wala.ssa.ISSABasicBlock currentBlock,
                                                                                             com.ibm.wala.ssa.ISSABasicBlock endingBlock)
                                                                                      throws StaticRegionException

Translates from current block but does not include the ending block.

Parameters:

cfg - Control flow graph.

currentBlock - Current block

endingBlock - End block, this is not included in this translation.

Returns:

a statement that represents this part of cfg in RangerIR.

Throws:

StaticRegionException

attemptConditionalSubregion

private Stmt attemptConditionalSubregion(com.ibm.wala.ssa.SSACFG cfg,
                                         com.ibm.wala.ssa.ISSABasicBlock startingBlock,
                                         com.ibm.wala.ssa.ISSABasicBlock terminus)
                                  throws StaticRegionException

Attempts to translate conditional region and translates it to RangerIR statement

Parameters:

cfg - Control flow graph

startingBlock - Starting block that is a branch instruction.

terminus - End of the region.

Returns:

Translated statement in RangerIR that has decompiled the CFG.

Throws:

StaticRegionException

jitAttemptConditionalSubregion

private Stmt jitAttemptConditionalSubregion(com.ibm.wala.ssa.SSACFG cfg,
                                            com.ibm.wala.ssa.ISSABasicBlock startingBlock,
                                            com.ibm.wala.ssa.ISSABasicBlock terminus)
                                     throws StaticRegionException

Throws:

StaticRegionException

attemptMethodSubregion

private Stmt attemptMethodSubregion(com.ibm.wala.ssa.SSACFG cfg,
                                    com.ibm.wala.ssa.ISSABasicBlock startingBlock,
                                    com.ibm.wala.ssa.ISSABasicBlock endingBlock)
                             throws StaticRegionException

Attempts to translate a method region to a RangerIR statement.

Parameters:

cfg -

startingBlock -

endingBlock -

Returns:

Throws:

StaticRegionException

createStructuredConditionalRegions

private void createStructuredConditionalRegions(com.ibm.wala.ssa.ISSABasicBlock currentBlock,
                                                com.ibm.wala.ssa.ISSABasicBlock endingBlock,
                                                java.util.HashMap<java.lang.String,StaticRegion> veritestingRegions)
                                         throws StaticRegionException

This class walks through method, attempting to find conditional veritesting regions

Parameters:

currentBlock -

endingBlock -

veritestingRegions -

Throws:

StaticRegionException

createStructuredConditionalRegions

public void createStructuredConditionalRegions(java.util.HashMap<java.lang.String,StaticRegion> veritestingRegions)
                                        throws StaticRegionException

Throws:

StaticRegionException

createStructuredMethodRegion

public void createStructuredMethodRegion(java.util.HashMap<java.lang.String,StaticRegion> veritestingRegions)
                                  throws StaticRegionException

This class walks through method, attempting to find method regions veritesting regions

Throws:

StaticRegionException

attemptMethodAndMultiPathRegions

public Stmt attemptMethodAndMultiPathRegions(com.ibm.wala.ssa.SSACFG cfg,
                                             com.ibm.wala.ssa.ISSABasicBlock currentBlock,
                                             com.ibm.wala.ssa.ISSABasicBlock endingBlock)
                                      throws StaticRegionException

This methods attempt to connect discover multi-path regions and connecting them to recover the method as well.

Parameters:

cfg -

currentBlock -

endingBlock -

Returns:

Throws:

StaticRegionException

populateMissedRegions

private void populateMissedRegions(com.ibm.wala.ssa.SSACFG cfg,
                                   com.ibm.wala.ssa.ISSABasicBlock currentBlock,
                                   com.ibm.wala.ssa.ISSABasicBlock endingBlock)
                            throws StaticRegionException

Throws:

StaticRegionException

phiBlock

private boolean phiBlock(com.ibm.wala.ssa.ISSABasicBlock currentBlock)

jitCreateStructuredRegion

public void jitCreateStructuredRegion(java.util.HashMap<java.lang.String,StaticRegion> veritestingRegions)
                               throws StaticRegionException

This class walks through method, attempting to recover a method region and also recover all multi-path regions inside of it.

Throws:

StaticRegionException