Package 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
All Implemented Interfaces:
org.plumelib.util.UniqueId
public class TransferInput<V extends AbstractValue<V>,S extends Store<S>> extends 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 Details

    • node

      protected @Nullable Node node
      The corresponding node.

    • 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 Details

    • 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 Details

    • getUid

      public long getUid(@UnknownInitialization TransferInput<V extends AbstractValue<V>,S extends Store<S>> this)
      Specified by:
      getUid in interface org.plumelib.util.UniqueId

    • getNode

      public @Nullable Node getNode()
      Returns the Node for this TransferInput.
      Returns:
      the Node for this TransferInput

    • 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 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