org.checkerframework.dataflow.analysis

Class Analysis<A extends AbstractValue<A>,S extends Store<S>,T extends TransferFunction<A,S>>

java.lang.Object

org.checkerframework.dataflow.analysis.Analysis<A,S,T>

Type Parameters:

A - 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 approximated runtime behavior

Direct Known Subclasses:

CFAbstractAnalysis

public class Analysis<A extends AbstractValue<A>,S extends Store<S>,T extends TransferFunction<A,S>>
extends java.lang.Object

An implementation of an iterative algorithm to solve a org.checkerframework.dataflow problem, given a control flow graph and a transfer function.

Author:

Stefan Heule

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected static class	Analysis.Worklist A worklist is a priority queue of blocks in which the order is given by depth-first ordering to place non-loop predecessors ahead of successors.

Field Summary

Fields

Modifier and Type	Field and Description
protected java.util.IdentityHashMap<Block,java.lang.Integer>	blockCount Number of times every block has been analyzed since the last time widening was applied.
protected ControlFlowGraph	cfg The control flow graph to perform the analysis on.
protected TransferInput<A,S>	currentInput The current transfer input when the analysis is running.
protected Node	currentNode The node that is currently handled in the analysis (if it is running).
protected com.sun.source.tree.Tree	currentTree The tree that is currently being looked at.
protected java.util.IdentityHashMap<Block,S>	elseStores Else stores before every basic block (assumed to be 'no information' if not present).
protected javax.annotation.processing.ProcessingEnvironment	env The associated processing environment
java.util.HashMap<javax.lang.model.element.Element,A>	finalLocalValues Map from (effectively final) local variable elements to their abstract value.
protected java.util.IdentityHashMap<Block,TransferInput<A,S>>	inputs The transfer inputs before every basic block (assumed to be 'no information' if not present).
protected boolean	isRunning Is the analysis currently running?
protected int	maxCountBeforeWidening Number of times a block can be analyzed before widening.
protected java.util.IdentityHashMap<Node,A>	nodeValues Abstract values of nodes.
protected java.util.IdentityHashMap<ReturnNode,TransferResult<A,S>>	storesAtReturnStatements The stores after every return statement.
protected java.util.IdentityHashMap<Block,S>	thenStores Then stores before every basic block (assumed to be 'no information' if not present).
protected T	transferFunction The transfer function for regular nodes.
protected javax.lang.model.util.Types	types Instance of the types utility.
protected Analysis.Worklist	worklist The worklist used for the fix-point iteration.

Constructor Summary

Constructors

Constructor and Description
Analysis(javax.annotation.processing.ProcessingEnvironment env) Construct an object that can perform a org.checkerframework.dataflow analysis over a control flow graph.
Analysis(javax.annotation.processing.ProcessingEnvironment env, T transfer) Construct an object that can perform a org.checkerframework.dataflow analysis over a control flow graph, given a transfer function.
Analysis(javax.annotation.processing.ProcessingEnvironment env, T transfer, int maxCountBeforeWidening) Construct an object that can perform a org.checkerframework.dataflow analysis over a control flow graph, given a transfer function.

Method Summary

Modifier and Type	Method and Description
protected void	addStoreBefore(Block b, 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 void	addToWorklist(Block b) Add a basic block to the worklist.
protected TransferResult<A,S>	callTransferFunction(Node node, TransferInput<A,S> store) Call the transfer function for node node, and set that node as current node first.
@Nullable com.sun.source.tree.ClassTree	getContainingClass(com.sun.source.tree.Tree t) Get the ClassTree of the current CFG if the argument Tree maps to a Node in the CFG or null otherwise.
@Nullable com.sun.source.tree.MethodTree	getContainingMethod(com.sun.source.tree.Tree t) Get the MethodTree of the current CFG if the argument Tree maps to a Node in the CFG or null otherwise.
com.sun.source.tree.Tree	getCurrentTree()
javax.annotation.processing.ProcessingEnvironment	getEnv()
S	getExceptionalExitStore()
@Nullable TransferInput<A,S>	getInput(Block b) Read the TransferInput for a particular basic block (or null if none exists yet).
protected @Nullable TransferInput<A,S>	getInputBefore(Block b)
Node	getNodeForTree(com.sun.source.tree.Tree t) Get the Node for a given Tree.
S	getRegularExitStore()
AnalysisResult<A,S>	getResult()
java.util.List<Pair<ReturnNode,TransferResult<A,S>>>	getReturnStatementStores()
protected S	getStoreBefore(Block b, Store.Kind kind)
T	getTransferFunction()
javax.lang.model.util.Types	getTypes()
A	getValue(Node n)
A	getValue(com.sun.source.tree.Tree t)
protected void	init(ControlFlowGraph cfg) Initialize the analysis with a new control flow graph.
boolean	isRunning() Is the analysis currently running?
void	performAnalysis(ControlFlowGraph cfg) Perform the actual analysis.
protected void	propagateStoresTo(Block succ, Node node, TransferInput<A,S> currentInput, Store.FlowRule flowRule, boolean addToWorklistAgain) Propagate the stores in currentInput to the successor block, succ, according to the flowRule.
protected static <S> S	readFromStore(java.util.Map<Block,S> stores, Block b) Read the Store for a particular basic block from a map of stores (or null if none exists yet).
void	setCurrentTree(com.sun.source.tree.Tree currentTree)
void	setTransferFunction(T transfer)
protected boolean	updateNodeValues(Node node, TransferResult<A,S> transferResult) Updates the value of node node to the value of the transferResult.

Methods inherited from class java.lang.Object

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

Field Detail

isRunning

protected boolean isRunning

Is the analysis currently running?

transferFunction

protected T extends TransferFunction<A,S> transferFunction

The transfer function for regular nodes.

cfg

protected ControlFlowGraph cfg

The control flow graph to perform the analysis on.

env

protected final javax.annotation.processing.ProcessingEnvironment env

The associated processing environment

types

protected final javax.lang.model.util.Types types

Instance of the types utility.

thenStores

protected java.util.IdentityHashMap<Block,S extends Store<S>> thenStores

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

elseStores

protected java.util.IdentityHashMap<Block,S extends Store<S>> elseStores

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

blockCount

protected java.util.IdentityHashMap<Block,java.lang.Integer> blockCount

Number of times every 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.

inputs

protected java.util.IdentityHashMap<Block,TransferInput<A extends AbstractValue<A>,S extends Store<S>>> inputs

The transfer inputs before every basic block (assumed to be 'no information' if not present).

storesAtReturnStatements

protected java.util.IdentityHashMap<ReturnNode,TransferResult<A extends AbstractValue<A>,S extends Store<S>>> storesAtReturnStatements

The stores after every return statement.

worklist

protected Analysis.Worklist worklist

The worklist used for the fix-point iteration.

nodeValues

protected java.util.IdentityHashMap<Node,A extends AbstractValue<A>> nodeValues

Abstract values of nodes.

finalLocalValues

public java.util.HashMap<javax.lang.model.element.Element,A extends AbstractValue<A>> finalLocalValues

Map from (effectively final) local variable elements to their abstract value.

currentNode

protected Node currentNode

The node that is currently handled in the analysis (if it is running). The following invariant holds:

   !isRunning ⇒ (currentNode == null)
 

currentTree

protected com.sun.source.tree.Tree currentTree

The tree that is currently being looked at. The transfer function can set this tree to make sure that calls to getValue will not return information for this given tree.

currentInput

protected TransferInput<A extends AbstractValue<A>,S extends Store<S>> currentInput

The current transfer input when the analysis is running.

Constructor Detail

Analysis

public Analysis(javax.annotation.processing.ProcessingEnvironment env)

Construct an object that can perform a org.checkerframework.dataflow analysis over a control flow graph. The transfer function is set later using setTransferFunction.

Analysis

public Analysis(javax.annotation.processing.ProcessingEnvironment env,
                T transfer)

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

Analysis

public Analysis(javax.annotation.processing.ProcessingEnvironment env,
                T transfer,
                int maxCountBeforeWidening)

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

Method Detail

getCurrentTree

public com.sun.source.tree.Tree getCurrentTree()

setCurrentTree

public void setCurrentTree(com.sun.source.tree.Tree currentTree)

setTransferFunction

public void setTransferFunction(T transfer)

getTransferFunction

public T getTransferFunction()

getTypes

public javax.lang.model.util.Types getTypes()

getEnv

public javax.annotation.processing.ProcessingEnvironment getEnv()

performAnalysis

public void performAnalysis(ControlFlowGraph cfg)

Perform the actual analysis. Should only be called once after the object has been created.

propagateStoresTo

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

Propagate the stores in currentInput to the successor block, succ, according to the flowRule.

updateNodeValues

protected boolean updateNodeValues(Node node,
                                   TransferResult<A,S> transferResult)

Updates the value of node node to the value of the transferResult. Returns true if the node's value changed, or a store was updated.

callTransferFunction

protected TransferResult<A,S> callTransferFunction(Node node,
                                                   TransferInput<A,S> store)

Call the transfer function for node node, and set that node as current node first.

init

protected void init(ControlFlowGraph cfg)

Initialize the analysis with a new control flow graph.

addToWorklist

protected void addToWorklist(Block b)

Add a basic block to the worklist. If b is already present, the method does nothing.

addStoreBefore

protected void addStoreBefore(Block b,
                              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.

getInput

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

Read the TransferInput for a particular basic block (or null if none exists yet).

getInputBefore

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

Returns:

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

getStoreBefore

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

Returns:

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

readFromStore

protected static <S> S readFromStore(java.util.Map<Block,S> stores,
                                     Block b)

Read the Store for a particular basic block from a map of stores (or null if none exists yet).

isRunning

public boolean isRunning()

Is the analysis currently running?

getValue

public A getValue(Node n)

Returns:

the abstract value for Node n, or null if no information is available. Note that if the analysis has not finished yet, this value might not represent the final value for this node.

getValue

public A getValue(com.sun.source.tree.Tree t)

Returns:

the abstract value for Tree t, or null if no information is available. Note that if the analysis has not finished yet, this value might not represent the final value for this node.

getNodeForTree

public Node getNodeForTree(com.sun.source.tree.Tree t)

Get the Node for a given Tree.

getContainingMethod

public @Nullable com.sun.source.tree.MethodTree getContainingMethod(com.sun.source.tree.Tree t)

Get the MethodTree of the current CFG if the argument Tree maps to a Node in the CFG or null otherwise.

getContainingClass

public @Nullable com.sun.source.tree.ClassTree getContainingClass(com.sun.source.tree.Tree t)

Get the ClassTree of the current CFG if the argument Tree maps to a Node in the CFG or null otherwise.

getReturnStatementStores

public java.util.List<Pair<ReturnNode,TransferResult<A,S>>> getReturnStatementStores()

getResult

public AnalysisResult<A,S> getResult()

getRegularExitStore

public S getRegularExitStore()

Returns:

the regular exit store, or null, if there is no such store (because the method cannot exit through the regular exit block).

getExceptionalExitStore

public S getExceptionalExitStore()