org.checkerframework.dataflow.analysis

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

java.lang.Object

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

Type Parameters:

S - the Store used to keep track of intermediate results

public class TransferInput<A extends AbstractValue<A>,S extends Store<S>>
extends java.lang.Object

TransferInput is used as the input type of the individual transfer functions of a TransferFunction. 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'.

Author:

Stefan Heule

Field Summary

Fields

Modifier and Type	Field and Description
protected Analysis<A,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 Node	node The corresponding node.
protected S	store The regular result store (or null if none is present).
protected S	thenStore The 'then' result store (or null if none is present).

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method and Description
boolean	containsTwoStores()
TransferInput<A,S>	copy()
boolean	equals(java.lang.Object o)
S	getElseStore()
Node	getNode()
S	getRegularStore()
S	getThenStore()
A	getValueOfSubNode(Node n)
int	hashCode()
TransferInput<A,S>	leastUpperBound(TransferInput<A,S> other) Compute the least upper bound of two stores.
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

node

protected Node node

The corresponding node.

store

protected final S extends Store<S> store

The regular result store (or null if none is present). 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). The following invariant is maintained:

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

elseStore

protected final S extends Store<S> elseStore

The 'else' result store (or null if none is present). The following invariant is maintained:

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

analysis

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

The corresponding analysis class to get intermediate flow results.

Constructor Detail

TransferInput

public TransferInput(Node n,
                     Analysis<A,S,?> analysis,
                     TransferResult<A,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 transfered to this object.

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

TransferInput

public TransferInput(Node n,
                     Analysis<A,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 transfered to this object.

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

TransferInput

public TransferInput(Node n,
                     Analysis<A,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 transfered to this object.

TransferInput

protected TransferInput(TransferInput<A,S> from)

Copy constructor.

Method Detail

getNode

public Node getNode()

Returns:

the Node for this TransferInput.

getValueOfSubNode

public A 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 if 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

getThenStore

public S getThenStore()

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.

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.

copy

public TransferInput<A,S> copy()

Returns:

an exact copy of this store.

leastUpperBound

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

Compute the least upper bound of two stores.

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

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object