org.checkerframework.dataflow.analysis

Class ForwardAnalysisImpl<V extends AbstractValue<V>,S extends Store<S>,T extends ForwardTransferFunction<V,S>>

java.lang.Object

org.checkerframework.dataflow.analysis.AbstractAnalysis<V,S,T>

org.checkerframework.dataflow.analysis.ForwardAnalysisImpl<V,S,T>

Type Parameters:

V - the abstract value type to be tracked by the analysis

S - the store type used in the analysis

T - the transfer function type that is used to approximate runtime behavior

All Implemented Interfaces:

Analysis<V,S,T>, ForwardAnalysis<V,S,T>

Direct Known Subclasses:

CFAbstractAnalysis

public class ForwardAnalysisImpl<V extends AbstractValue<V>,S extends Store<S>,T extends ForwardTransferFunction<V,S>>
extends AbstractAnalysis<V,S,T>
implements ForwardAnalysis<V,S,T>

An implementation of a forward analysis to solve a org.checkerframework.dataflow problem given a control flow graph and a forward transfer function.

Nested Class Summary

Nested classes/interfaces inherited from class org.checkerframework.dataflow.analysis.AbstractAnalysis

AbstractAnalysis.Worklist

Nested classes/interfaces inherited from interface org.checkerframework.dataflow.analysis.Analysis

Analysis.BeforeOrAfter, Analysis.Direction

Field Summary

Fields

Modifier and Type	Field and Description
protected @Nullable IdentityHashMap<Block,Integer>	blockCount Number of times each block has been analyzed since the last time widening was applied.
protected IdentityHashMap<Block,S>	elseStores Else stores before every basic block (assumed to be 'no information' if not present).
protected int	maxCountBeforeWidening Number of times a block can be analyzed before widening.
protected IdentityHashMap<ReturnNode,TransferResult<V,S>>	storesAtReturnStatements The stores after every return statement.
protected IdentityHashMap<Block,S>	thenStores Then stores before every basic block (assumed to be 'no information' if not present).

Fields inherited from class org.checkerframework.dataflow.analysis.AbstractAnalysis

cfg, currentInput, currentNode, currentTree, direction, finalLocalValues, inputs, isRunning, nodeValues, transferFunction, worklist

Constructor Summary

Constructors

Constructor and Description
ForwardAnalysisImpl(int maxCountBeforeWidening) Construct an object that can perform a org.checkerframework.dataflow forward analysis over a control flow graph.
ForwardAnalysisImpl(T transfer) Construct an object that can perform a org.checkerframework.dataflow forward analysis over a control flow graph given a transfer function.

Method Summary

Modifier and Type	Method and Description
protected void	addStoreBefore(Block b, @Nullable Node node, S s, Store.Kind kind, boolean addBlockToWorklist) Add a store before the basic block b by merging with the existing stores for that location.
protected TransferResult<V,S>	callTransferFunction(Node node, TransferInput<V,S> input) Call the transfer function for node node, and set that node as current node first.
@Nullable TransferInput<V,S>	getInput(Block b) Get the transfer input of a given Block b.
protected @Nullable TransferInput<V,S>	getInputBefore(Block b) Returns the transfer input corresponding to the location right before the basic block b.
List<Pair<ReturnNode,TransferResult<V,S>>>	getReturnStatementStores() Get stores at return statements.
protected S	getStoreBefore(Block b, Store.Kind kind) Return the store corresponding to the location right before the basic block b.
protected void	initFields(ControlFlowGraph cfg) Initialize fields of this object based on a given control flow graph.
protected void	initInitialInputs() Initialize the transfer inputs of every basic block before performing the analysis.
void	performAnalysis(ControlFlowGraph cfg) Perform the actual analysis.
void	performAnalysisBlock(Block b) Perform the actual analysis on one block.
protected void	propagateStoresTo(Block succ, @Nullable Node node, TransferInput<V,S> currentInput, Store.FlowRule flowRule, boolean addToWorklistAgain) Propagate the stores in currentInput to the next block in the direction of analysis, according to the flowRule.
S	runAnalysisFor(Node node, Analysis.BeforeOrAfter preOrPost, TransferInput<V,S> blockTransferInput, IdentityHashMap<Node,V> nodeValues, Map<TransferInput<V,S>,IdentityHashMap<Node,TransferResult<V,S>>> analysisCaches) Runs the analysis again within the block of node and returns the store at the location of node.

Methods inherited from class org.checkerframework.dataflow.analysis.AbstractAnalysis

addToWorklist, getContainingClass, getContainingMethod, getCurrentTree, getDirection, getExceptionalExitStore, getNodesForTree, getNodeValues, getRegularExitStore, getResult, getTransferFunction, getValue, getValue, init, isRunning, readFromStore, setCurrentNode, setCurrentTree, updateNodeValues

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.checkerframework.dataflow.analysis.Analysis

getDirection, getExceptionalExitStore, getRegularExitStore, getResult, getTransferFunction, getValue, getValue, isRunning

Field Detail

blockCount

protected final @Nullable IdentityHashMap<Block,Integer> blockCount

Number of times each block has been analyzed since the last time widening was applied. Null if maxCountBeforeWidening is -1, which implies widening isn't used for this analysis.

maxCountBeforeWidening

protected final int maxCountBeforeWidening

Number of times a block can be analyzed before widening. -1 implies that widening shouldn't be used.

thenStores

protected final IdentityHashMap<Block,S extends Store<S>> thenStores

Then stores before every basic block (assumed to be 'no information' if not present).

elseStores

protected final IdentityHashMap<Block,S extends Store<S>> elseStores

Else stores before every basic block (assumed to be 'no information' if not present).

storesAtReturnStatements

protected final IdentityHashMap<ReturnNode,TransferResult<V extends AbstractValue<V>,S extends Store<S>>> storesAtReturnStatements

The stores after every return statement.

Constructor Detail

ForwardAnalysisImpl

public ForwardAnalysisImpl(int maxCountBeforeWidening)

Construct an object that can perform a org.checkerframework.dataflow forward analysis over a control flow graph. When using this constructor, the transfer function is set later by the subclass, e.g., org.checkerframework.framework.flow.CFAbstractAnalysis.

Parameters:

maxCountBeforeWidening - number of times a block can be analyzed before widening

ForwardAnalysisImpl

public ForwardAnalysisImpl(T transfer)

Construct an object that can perform a org.checkerframework.dataflow forward analysis over a control flow graph given a transfer function.

Parameters:

transfer - the transfer function

Method Detail

performAnalysis

public void performAnalysis(ControlFlowGraph cfg)

Description copied from interface: Analysis

Perform the actual analysis.

Specified by:

performAnalysis in interface Analysis<V extends AbstractValue<V>,S extends Store<S>,T extends ForwardTransferFunction<V,S>>

Parameters:

cfg - the control flow graph

performAnalysisBlock

public void performAnalysisBlock(Block b)

Description copied from interface: Analysis

Perform the actual analysis on one block.

Specified by:

performAnalysisBlock in interface Analysis<V extends AbstractValue<V>,S extends Store<S>,T extends ForwardTransferFunction<V,S>>

Parameters:

b - the block to analyze

getInput

public @Nullable TransferInput<V,S> getInput(Block b)

Description copied from interface: Analysis

Get the transfer input of a given Block b.

Specified by:

getInput in interface Analysis<V extends AbstractValue<V>,S extends Store<S>,T extends ForwardTransferFunction<V,S>>

Parameters:

b - a given Block

Returns:

the transfer input of this Block

getReturnStatementStores

@RequiresNonNull(value="cfg")
public List<Pair<ReturnNode,TransferResult<V,S>>> getReturnStatementStores()

Description copied from interface: ForwardAnalysis

Get stores at return statements. These stores are transfer results at return node. Thus for a forward analysis, these stores contain the analyzed flow information from entry nodes to return nodes.

Specified by:

getReturnStatementStores in interface ForwardAnalysis<V extends AbstractValue<V>,S extends Store<S>,T extends ForwardTransferFunction<V,S>>

Returns:

the transfer results for each return node in the CFG

runAnalysisFor

public S runAnalysisFor(@FindDistinct
                        Node node,
                        Analysis.BeforeOrAfter preOrPost,
                        TransferInput<V,S> blockTransferInput,
                        IdentityHashMap<Node,V> nodeValues,
                        Map<TransferInput<V,S>,IdentityHashMap<Node,TransferResult<V,S>>> analysisCaches)

Description copied from interface: Analysis

Runs the analysis again within the block of node and returns the store at the location of node. If before is true, then the store immediately before the Node node is returned. Otherwise, the store immediately after node is returned. If analysisCaches is not null, this method uses a cache. analysisCaches is a map of a block of node to the cached analysis result. If the cache for transferInput is not in analysisCaches, this method creates new cache and stores it in analysisCaches. The cache is a map of nodes to the analysis results of the nodes.

Specified by:

runAnalysisFor in interface Analysis<V extends AbstractValue<V>,S extends Store<S>,T extends ForwardTransferFunction<V,S>>

Parameters:

node - the node to analyze

preOrPost - which store to return: the store immediately before node or the store after node

blockTransferInput - the transfer input of the block of this node

nodeValues - abstract values of nodes

analysisCaches - caches of analysis results

Returns:

the store before or after node (depends on the value of before) after running the analysis

initFields

protected void initFields(ControlFlowGraph cfg)

Description copied from class: AbstractAnalysis

Initialize fields of this object based on a given control flow graph. Sub-class may override this method to initialize customized fields.

Overrides:

initFields in class AbstractAnalysis<V extends AbstractValue<V>,S extends Store<S>,T extends ForwardTransferFunction<V,S>>

Parameters:

cfg - a given control flow graph

initInitialInputs

@RequiresNonNull(value="cfg")
protected void initInitialInputs()

Description copied from class: AbstractAnalysis

Initialize the transfer inputs of every basic block before performing the analysis.

Specified by:

initInitialInputs in class AbstractAnalysis<V extends AbstractValue<V>,S extends Store<S>,T extends ForwardTransferFunction<V,S>>

callTransferFunction

protected TransferResult<V,S> callTransferFunction(Node node,
                                                   TransferInput<V,S> input)

Description copied from class: AbstractAnalysis

Call the transfer function for node node, and set that node as current node first. This method requires a transferInput that the method can modify.

Overrides:

callTransferFunction in class AbstractAnalysis<V extends AbstractValue<V>,S extends Store<S>,T extends ForwardTransferFunction<V,S>>

Parameters:

node - the given node

input - the transfer input

Returns:

the output of the transfer function

propagateStoresTo

protected void propagateStoresTo(Block succ,
                                 @Nullable Node node,
                                 TransferInput<V,S> currentInput,
                                 Store.FlowRule flowRule,
                                 boolean addToWorklistAgain)

Description copied from class: AbstractAnalysis

Propagate the stores in currentInput to the next block in the direction of analysis, according to the flowRule.

Specified by:

propagateStoresTo in class AbstractAnalysis<V extends AbstractValue<V>,S extends Store<S>,T extends ForwardTransferFunction<V,S>>

Parameters:

succ - the target block to propagate the stores to

node - the node of the target block

currentInput - the current transfer input

flowRule - the flow rule being used

addToWorklistAgain - whether the block should be added to AbstractAnalysis.worklist again

addStoreBefore

protected void addStoreBefore(Block b,
                              @Nullable Node node,
                              S s,
                              Store.Kind kind,
                              boolean addBlockToWorklist)

Add a store before the basic block b by merging with the existing stores for that location.

Parameters:

b - a basic block

node - the node of the basic block b

s - the store being added

kind - the kind of store s

addBlockToWorklist - whether the basic block b should be added back to Worklist

getStoreBefore

protected S getStoreBefore(Block b,
                           Store.Kind kind)

Return the store corresponding to the location right before the basic block b.

Parameters:

b - a block

kind - the kind of store which will be returned

Returns:

the store corresponding to the location right before the basic block b

getInputBefore

protected @Nullable TransferInput<V,S> getInputBefore(Block b)

Returns the transfer input corresponding to the location right before the basic block b.

Parameters:

b - a block

Returns:

the transfer input corresponding to the location right before the basic block b