Package org.checkerframework.dataflow.analysis

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

  • Type Parameters:
    V - type of the abstract value that is tracked
    S - the store type used in the analysis
    All Implemented Interfaces:
    org.plumelib.util.UniqueId
    public class TransferInput<V extends AbstractValue<V>,​S extends Store<S>>
extends java.lang.Object
implements org.plumelib.util.UniqueId
    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 Detail

      • store

        protected final @Nullable 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 @Nullable S extends Store<S> thenStore
        The 'then' result store (or null if none is present). See invariant at store.

      • elseStore

        protected final @Nullable 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

    • Method Detail

      • getValueOfSubNode

        public @Nullable 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 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