org.checkerframework.dataflow.analysis

Class TransferInput<V extends AbstractValue<V>,S extends Store<S>>

java.lang.Object

org.checkerframework.dataflow.analysis.TransferInput<V,S>

Type Parameters:

V - type of the abstract value that is tracked

S - the store type used in the analysis

public class TransferInput<V extends AbstractValue<V>,S extends Store<S>>
extends Object

TransferInput is used as the input type of the individual transfer functions of a ForwardTransferFunction or a BackwardTransferFunction. It also contains a reference to the node for which the transfer function will be applied.

A TransferInput contains one or two stores. If two stores are present, one belongs to 'then', and the other to 'else'.

Field Summary

Fields

Modifier and Type	Field and Description
protected Analysis<V,S,?>	analysis The corresponding analysis class to get intermediate flow results.
protected S	elseStore The 'else' result store (or null if none is present).
protected @Nullable Node	node The corresponding node.
protected S	store The regular result store (or null if none is present, because thenStore and elseStore are set).
protected S	thenStore The 'then' result store (or null if none is present).

Constructor Summary

Constructors

Modifier	Constructor and Description
	TransferInput(@Nullable Node n, Analysis<V,S,?> analysis, S s) Create a TransferInput, given a store and a node-value mapping.
	TransferInput(@Nullable Node n, Analysis<V,S,?> analysis, S s1, S s2) Create a TransferInput, given two stores and a node-value mapping.
	TransferInput(Node n, Analysis<V,S,?> analysis, TransferResult<V,S> to) Create a TransferInput, given a TransferResult and a node-value mapping.
protected	TransferInput(TransferInput<V,S> from) Copy constructor.

Method Summary

Modifier and Type	Method and Description
boolean	containsTwoStores() Returns true if and only if this transfer input contains two stores that are potentially not equal.
TransferInput<V,S>	copy() Returns an exact copy of this store.
boolean	equals(@Nullable Object o)
S	getElseStore() Returns the result store produced if the Node this result belongs to evaluates to false.
@Nullable Node	getNode() Returns the Node for this TransferInput.
S	getRegularStore() Returns the regular result store produced if no exception is thrown by the Node corresponding to this transfer function result.
S	getThenStore() Returns the result store produced if the Node this result belongs to evaluates to true.
V	getValueOfSubNode(Node n) Returns the abstract value of node n, which is required to be a 'sub-node' (that is, a direct or indirect child) of the node this transfer input is associated with.
int	hashCode()
TransferInput<V,S>	leastUpperBound(TransferInput<V,S> other) Compute the least upper bound of two stores.
String	toString()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

node

protected @Nullable Node node

The corresponding node.

store

protected final S extends Store<S> store

The regular result store (or null if none is present, because thenStore and elseStore are set). The following invariant is maintained:

 store == null ⇔ thenStore != null && elseStore != null
 

thenStore

protected final S extends Store<S> thenStore

The 'then' result store (or null if none is present). See invariant at store.

elseStore

protected final S extends Store<S> elseStore

The 'else' result store (or null if none is present). See invariant at store.

analysis

protected final Analysis<V extends AbstractValue<V>,S extends Store<S>,?> analysis

The corresponding analysis class to get intermediate flow results.

Constructor Detail

TransferInput

public TransferInput(Node n,
                     Analysis<V,S,?> analysis,
                     TransferResult<V,S> to)

Create a TransferInput, given a TransferResult and a node-value mapping.

Aliasing: The stores returned by any methods of to will be stored internally and are not allowed to be used elsewhere. Full control of them is transferred to this object.

The node-value mapping nodeValues is provided by the analysis and is only read from within this TransferInput.

Parameters:

n - node

analysis - analysis

to - a transfer result

TransferInput

public TransferInput(@Nullable Node n,
                     Analysis<V,S,?> analysis,
                     S s)

Create a TransferInput, given a store and a node-value mapping.

Aliasing: The store s will be stored internally and is not allowed to be used elsewhere. Full control over s is transferred to this object.

The node-value mapping nodeValues is provided by the analysis and is only read from within this TransferInput.

Parameters:

n - node

analysis - analysis

s - store

TransferInput

public TransferInput(@Nullable Node n,
                     Analysis<V,S,?> analysis,
                     S s1,
                     S s2)

Create a TransferInput, given two stores and a node-value mapping.

Aliasing: The two stores s1 and s2 will be stored internally and are not allowed to be used elsewhere. Full control of them is transferred to this object.

Parameters:

n - a node

analysis - analysis

s1 - thenStore

s2 - elseStore

TransferInput

protected TransferInput(TransferInput<V,S> from)

Copy constructor.

Parameters:

from - a TransferInput to copy

Method Detail

getNode

public @Nullable Node getNode()

Returns the Node for this TransferInput.

Returns:

the Node for this TransferInput

getValueOfSubNode

public V getValueOfSubNode(Node n)

Returns the abstract value of node n, which is required to be a 'sub-node' (that is, a direct or indirect child) of the node this transfer input is associated with. Furthermore, n cannot be a l-value node. Returns null if no value is available.

Parameters:

n - a node

Returns:

the abstract value of node n, or null if no value is available

getRegularStore

public S getRegularStore()

Returns the regular result store produced if no exception is thrown by the Node corresponding to this transfer function result.

Returns:

the regular result store produced if no exception is thrown by the Node corresponding to this transfer function result

getThenStore

public S getThenStore()

Returns the result store produced if the Node this result belongs to evaluates to true.

Returns:

the result store produced if the Node this result belongs to evaluates to true

getElseStore

public S getElseStore()

Returns the result store produced if the Node this result belongs to evaluates to false.

Returns:

the result store produced if the Node this result belongs to evaluates to false

containsTwoStores

public boolean containsTwoStores()

Returns true if and only if this transfer input contains two stores that are potentially not equal. Note that the result true does not imply that getRegularStore cannot be called (or vice versa for false). Rather, it indicates that getThenStore or getElseStore can be used to give more precise results. Otherwise, if the result is false, then all three methods getRegularStore, getThenStore, and getElseStore return equivalent stores.

Returns:

true if and only if this transfer input contains two stores that are potentially not equal

copy

public TransferInput<V,S> copy()

Returns an exact copy of this store.

Returns:

an exact copy of this store

leastUpperBound

public TransferInput<V,S> leastUpperBound(TransferInput<V,S> other)

Compute the least upper bound of two stores.

Important: This method must fulfill the same contract as leastUpperBound of Store.

Parameters:

other - a transfer input

Returns:

the least upper bound of this and other

equals

public boolean equals(@Nullable Object o)

Overrides:

equals in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object

toString

public String toString()

Overrides:

toString in class Object