Package org.checkerframework.dataflow.analysis

Class TransferResult<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
    Direct Known Subclasses:
    ConditionalTransferResult, RegularTransferResult
    public abstract class TransferResult<V extends AbstractValue<V>,​S extends Store<S>>
extends java.lang.Object
    TransferResult is used as the result type of the individual transfer functions of a TransferFunction. It always belongs to the result of the individual transfer function for a particular Node, even though that org.checkerframework.dataflow.cfg.node.Node is not explicitly stored in TransferResult.

    A TransferResult consists of a result value, plus one or more stores. It contains one or two stores (for 'then' and 'else'), and zero or more stores with a cause (TypeMirror).

    • Field Summary

      Fields 
      Modifier and Type Field Description
      protected @Nullable java.util.Map<javax.lang.model.type.TypeMirror,​S> exceptionalStores
      The stores in case the basic block throws an exception (or null if the corresponding Node does not throw any exceptions).
      protected @Nullable V resultValue
      The abstract value of the Node associated with this TransferResult, or null if no value has been produced.

    • Method Summary

      All Methods Instance Methods Abstract Methods Concrete Methods 
      Modifier and Type Method Description
      abstract boolean containsTwoStores()
      Returns true if and only if this transfer result contains two stores that are potentially not equal.
      abstract S getElseStore()
      Returns the result store produced if the Node this result belongs to evaluates to false.
      @Nullable S getExceptionalStore​(javax.lang.model.type.TypeMirror exception)
      Returns the store that flows along the outgoing exceptional edge labeled with exception (or null if no special handling is required for exceptional edges).
      @Nullable java.util.Map<javax.lang.model.type.TypeMirror,​S> getExceptionalStores()
      Returns a Map of TypeMirror to Store, null otherwise.
      abstract S getRegularStore()
      Returns the regular result store produced if no exception is thrown by the Node corresponding to this transfer function result.
      @Nullable V getResultValue()
      Returns the abstract value produced by the transfer function, null otherwise.
      abstract S getThenStore()
      Returns the result store produced if the Node this result belongs to evaluates to true.
      void setResultValue​(V resultValue)
      Set the value of resultValue.
      abstract boolean storeChanged()
      Returns true if and only if the transfer function returning this transfer result changed the regularStore, elseStore, or thenStore.

      • Methods inherited from class java.lang.Object

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

    • Field Detail

      • exceptionalStores

        protected final @Nullable java.util.Map<javax.lang.model.type.TypeMirror,​S extends Store<S>> exceptionalStores
        The stores in case the basic block throws an exception (or null if the corresponding Node does not throw any exceptions). Does not necessarily contain a store for every exception, in which case the in-store will be used.

    • Constructor Detail

      • TransferResult

        protected TransferResult​(@Nullable V resultValue,
                         @Nullable java.util.Map<javax.lang.model.type.TypeMirror,​S> exceptionalStores)
        Create a new TransferResult, given resultValue and exceptionalStores.
        Parameters:
        resultValue - the abstract value of the Node associated with this TransferResult
        exceptionalStores - the stores in case the basic block throws an exception (or null if the corresponding Node does not throw any exceptions)

    • Method Detail

      • getResultValue

        public @Nullable V getResultValue()
        Returns the abstract value produced by the transfer function, null otherwise.
        Returns:
        the abstract value produced by the transfer function, null otherwise

      • setResultValue

        public void setResultValue​(V resultValue)
        Set the value of resultValue.
        Parameters:
        resultValue - the abstract value of the Node associated with this TransferResult

      • getRegularStore

        public abstract 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 abstract 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 abstract 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

      • getExceptionalStore

        public @Nullable S getExceptionalStore​(javax.lang.model.type.TypeMirror exception)
        Returns the store that flows along the outgoing exceptional edge labeled with exception (or null if no special handling is required for exceptional edges).
        Parameters:
        exception - an exception type
        Returns:
        the store that flows along the outgoing exceptional edge labeled with exception (or null if no special handling is required for exceptional edges)

      • getExceptionalStores

        public @Nullable java.util.Map<javax.lang.model.type.TypeMirror,​S> getExceptionalStores()
        Returns a Map of TypeMirror to Store, null otherwise.
        Returns:
        a Map of TypeMirror to Store, null otherwise
        See Also:
        getExceptionalStore(TypeMirror)

      • containsTwoStores

        public abstract boolean containsTwoStores()
        Returns true if and only if this transfer result 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 result contains two stores that are potentially not equal

      • storeChanged

        public abstract boolean storeChanged()
        Returns true if and only if the transfer function returning this transfer result changed the regularStore, elseStore, or thenStore.
        Returns:
        true if and only if the transfer function returning this transfer result changed the regularStore, elseStore, or thenStore