Class CFAbstractStore<V extends CFAbstractValue<V>,​S extends CFAbstractStore<V,​S>>

  • All Implemented Interfaces:
    Store<S>, org.plumelib.util.UniqueId
    Direct Known Subclasses:
    AccumulationStore, CFStore, InitializationStore, KeyForStore, LockStore, NullnessNoInitStore

    public abstract class CFAbstractStore<V extends CFAbstractValue<V>,​S extends CFAbstractStore<V,​S>>
    extends java.lang.Object
    implements Store<S>, org.plumelib.util.UniqueId
    A store for the Checker Framework analysis. It tracks the annotations of memory locations such as local variables and fields.

    When adding a new field to track values for a code construct (similar to localVariableValues and thisValue), it is important to review all constructors and methods in this class for locations where the new field must be handled (such as the copy constructor and clearValue), as well as all constructors/methods in subclasses of {code CFAbstractStore}. Note that this includes not only overridden methods in the subclasses, but new methods in the subclasses as well. Also check if BaseTypeVisitor#getJavaExpressionContextFromNode(Node) needs to be updated. Failing to do so may result in silent failures that are time consuming to debug.

    • Field Detail

      • localVariableValues

        protected final java.util.Map<LocalVariable,​V extends CFAbstractValue<V>> localVariableValues
        Information collected about local variables (including method parameters).
      • thisValue

        protected V extends CFAbstractValue<V> thisValue
        Information collected about the current object.
      • methodValues

        protected final java.util.Map<MethodCall,​V extends CFAbstractValue<V>> methodValues
        Information collected about method calls, using the internal representation MethodCall.
      • classValues

        protected final java.util.Map<ClassName,​V extends CFAbstractValue<V>> classValues
        Information collected about classname.class values, using the internal representation ClassName.
      • sequentialSemantics

        protected final boolean sequentialSemantics
        Should the analysis use sequential Java semantics (i.e., assume that only one thread is running at all times)?
    • Constructor Detail

      • CFAbstractStore

        protected CFAbstractStore​(CFAbstractAnalysis<V,​S,​?> analysis,
                                  boolean sequentialSemantics)
        Creates a new CFAbstractStore.
        Parameters:
        analysis - the analysis class this store belongs to
        sequentialSemantics - should the analysis use sequential Java semantics?
      • CFAbstractStore

        protected CFAbstractStore​(CFAbstractStore<V,​S> other)
        Copy constructor.
        Parameters:
        other - a CFAbstractStore to copy into this
    • Method Detail

      • getFieldValues

        public java.util.Map<FieldAccess,​V> getFieldValues()
        Returns information about fields. Clients should not side-effect the returned value, which is aliased to internal state.
        Returns:
        information about fields
      • getUid

        public long getUid()
        Specified by:
        getUid in interface org.plumelib.util.UniqueId
      • initializeMethodParameter

        public void initializeMethodParameter​(LocalVariableNode p,
                                              @Nullable V value)
        Set the abstract value of a method parameter (only adds the information to the store, does not remove any other knowledge). Any previous information is erased; this method should only be used to initialize the abstract value.
      • initializeThisValue

        public void initializeThisValue​(javax.lang.model.element.AnnotationMirror a,
                                        javax.lang.model.type.TypeMirror underlyingType)
        Set the value of the current object. Any previous information is erased; this method should only be used to initialize the value.
      • isSideEffectFree

        @Deprecated
        protected boolean isSideEffectFree​(AnnotatedTypeFactory atypeFactory,
                                           javax.lang.model.element.ExecutableElement method)
        Indicates whether the given method is side-effect-free as far as the current store is concerned. In some cases, a store for a checker allows for other mechanisms to specify whether a method is side-effect-free. For example, unannotated methods may be considered side-effect-free by default.
        Parameters:
        atypeFactory - the type factory used to retrieve annotations on the method element
        method - the method element
        Returns:
        whether the method is side-effect-free
      • updateForMethodCall

        public void updateForMethodCall​(MethodInvocationNode methodInvocationNode,
                                        GenericAnnotatedTypeFactory<V,​S,​?,​?> atypeFactory,
                                        V val)
        Remove any information that might not be valid any more after a method call, and add information guaranteed by the method.
        1. If the method is side-effect-free (as indicated by SideEffectFree or Pure), then no information needs to be removed.
        2. Otherwise, all information about field accesses a.f needs to be removed, except if the method n cannot modify a.f. This holds if a is a local variable or this, and f is final, or if a.f has a MonotonicQualifier in the current store. Subclasses can change this behavior by overriding newFieldValueAfterMethodCall(FieldAccess, GenericAnnotatedTypeFactory, CFAbstractValue).
        3. Furthermore, if the field has a monotonic annotation, then its information can also be kept.
        Furthermore, if the method is deterministic, we store its result val in the store.
        Parameters:
        methodInvocationNode - method whose information is being updated
        atypeFactory - the type factory of the associated checker
        val - abstract value of the method call
      • newMonotonicFieldValueAfterMethodCall

        protected V newMonotonicFieldValueAfterMethodCall​(FieldAccess fieldAccess,
                                                          GenericAnnotatedTypeFactory<V,​S,​?,​?> atypeFactory,
                                                          V value)
        Computes the value of a field whose declaration has a monotonic annotation, or returns null if the field has no monotonic annotation.

        Used by newFieldValueAfterMethodCall(FieldAccess, GenericAnnotatedTypeFactory, CFAbstractValue) to handle fields with monotonic annotations.

        Parameters:
        fieldAccess - the field whose value to compute
        atypeFactory - AnnotatedTypeFactory of the associated checker
        value - the field's value before the method call
        Returns:
        the field's value after the method call, or null if the field has no monotonic annotation
      • insertValue

        public void insertValue​(JavaExpression expr,
                                javax.lang.model.element.AnnotationMirror a)
        Add the annotation a for the expression expr (correctly deciding where to store the information depending on the type of the expression expr).

        This method does not take care of removing other information that might be influenced by changes to certain parts of the state.

        If there is already a value v present for expr, then the stronger of the new and old value are taken (according to the lattice). Note that this happens per hierarchy, and if the store already contains information about a hierarchy other than as hierarchy, that information is preserved.

        If expr is nondeterministic, this method does not insert value into the store.

        Parameters:
        expr - an expression
        a - an annotation for the expression
      • insertOrRefine

        public final void insertOrRefine​(JavaExpression expr,
                                         javax.lang.model.element.AnnotationMirror newAnno)
        Add the annotation newAnno for the expression expr (correctly deciding where to store the information depending on the type of the expression expr).

        This method does not take care of removing other information that might be influenced by changes to certain parts of the state.

        If there is already a value v present for expr, then the greatest lower bound of the new and old value is inserted into the store.

        Note that this happens per hierarchy, and if the store already contains information about a hierarchy other than newAnno's hierarchy, that information is preserved.

        If expr is nondeterministic, this method does not insert value into the store.

        Parameters:
        expr - an expression
        newAnno - the expression's annotation
      • canInsertJavaExpression

        public static boolean canInsertJavaExpression​(JavaExpression expr)
        Returns true if expr can be stored in this store.
      • insertValue

        public final void insertValue​(JavaExpression expr,
                                      @Nullable V value)
        Add the abstract value value for the expression expr (correctly deciding where to store the information depending on the type of the expression expr).

        This method does not take care of removing other information that might be influenced by changes to certain parts of the state.

        If there is already a value v present for expr, then the stronger of the new and old value are taken (according to the lattice). Note that this happens per hierarchy, and if the store already contains information about a hierarchy for which value does not contain information, then that information is preserved.

        If expr is nondeterministic, this method does not insert value into the store.

        Parameters:
        expr - the expression to insert in the store
        value - the value of the expression
      • insertValuePermitNondeterministic

        public final void insertValuePermitNondeterministic​(JavaExpression expr,
                                                            @Nullable V value)
        Like insertValue(JavaExpression, CFAbstractValue), but updates the store even if expr is nondeterministic.

        Usually, nondeterministic JavaExpressions should not be stored in a Store. For example, in the body of if (nondet() == 3) {...}, the store should not record that the value of nondet() is 3, because it might not be 3 the next time nondet() is executed.

        However, contracts can mention a nondeterministic JavaExpression. For example, a contract might have a postcondition thatnondet() is odd. This means that the next call tonondet() will return odd. Such a postcondition may be evicted from the store by calling a side-effecting method.

        Parameters:
        expr - the expression to insert in the store
        value - the value of the expression
      • shouldInsert

        @EnsuresNonNullIf(expression="#2",
                          result=true)
        protected boolean shouldInsert​(JavaExpression expr,
                                       @Nullable V value,
                                       boolean permitNondeterministic)
        Returns true if the given (expression, value) pair can be inserted in the store, namely if the value is non-null and the expression does not contain unknown or a nondeterministic expression.

        This method returning true does not guarantee that the value will be inserted; the implementation of insertValue( JavaExpression, CFAbstractValue, boolean) might still not insert it.

        Parameters:
        expr - the expression to insert in the store
        value - the value of the expression
        permitNondeterministic - if false, returns false if expr is nondeterministic; if true, permits nondeterministic expressions to be placed in the store
        Returns:
        true if the given (expression, value) pair can be inserted in the store
      • computeNewValueAndInsert

        protected void computeNewValueAndInsert​(JavaExpression expr,
                                                @Nullable V value,
                                                java.util.function.BinaryOperator<V> merger,
                                                boolean permitNondeterministic)
        Inserts the result of applying merger to value and the previous value for expr.
        Parameters:
        expr - the JavaExpression
        value - the value of the JavaExpression
        merger - the function used to merge value and the previous value of expr
        permitNondeterministic - if false, does nothing if expr is nondeterministic; if true, permits nondeterministic expressions to be placed in the store
      • isMonotonicUpdate

        protected boolean isMonotonicUpdate​(FieldAccess fieldAcc,
                                            V value)
        Return true if fieldAcc is an update of a monotonic qualifier to its target qualifier. (e.g. @MonotonicNonNull to @NonNull). Always returns false if sequentialSemantics is true.
        Returns:
        true if fieldAcc is an update of a monotonic qualifier to its target qualifier (e.g. @MonotonicNonNull to @NonNull)
      • insertThisValue

        public void insertThisValue​(javax.lang.model.element.AnnotationMirror a,
                                    javax.lang.model.type.TypeMirror underlyingType)
      • replaceValue

        public void replaceValue​(JavaExpression expr,
                                 @Nullable V value)
        Completely replaces the abstract value value for the expression expr (correctly deciding where to store the information depending on the type of the expression expr). Any previous information is discarded.

        This method does not take care of removing other information that might be influenced by changes to certain parts of the state.

      • clearValue

        public void clearValue​(JavaExpression expr)
        Remove any knowledge about the expression expr (correctly deciding where to remove the information depending on the type of the expression expr).
      • getValue

        public @Nullable V getValue​(JavaExpression expr)
        Returns the current abstract value of a Java expression, or null if no information is available.
        Returns:
        the current abstract value of a Java expression, or null if no information is available
      • getValue

        public @Nullable V getValue​(FieldAccessNode n)
        Returns the current abstract value of a field access, or null if no information is available.
        Parameters:
        n - the node whose abstract value to return
        Returns:
        the current abstract value of a field access, or null if no information is available
      • getFieldValue

        public @Nullable V getFieldValue​(FieldAccess fieldAccess)
        Returns the current abstract value of a field access, or null if no information is available.
        Parameters:
        fieldAccess - the field access to look up in this store
        Returns:
        current abstract value of a field access, or null if no information is available
      • getValue

        public @Nullable V getValue​(MethodInvocationNode n)
        Returns the current abstract value of a method call, or null if no information is available.
        Parameters:
        n - a method call
        Returns:
        the current abstract value of a method call, or null if no information is available
      • getValue

        public @Nullable V getValue​(ArrayAccessNode n)
        Returns the current abstract value of a field access, or null if no information is available.
        Parameters:
        n - the node whose abstract value to return
        Returns:
        the current abstract value of a field access, or null if no information is available
      • updateForAssignment

        public void updateForAssignment​(Node n,
                                        @Nullable V val)
        Update the information in the store by considering an assignment with target n.
        Parameters:
        n - the left-hand side of an assignment
        val - the right-hand value of an assignment
      • updateForFieldAccessAssignment

        protected void updateForFieldAccessAssignment​(FieldAccess fieldAccess,
                                                      @Nullable V val)
        Update the information in the store by considering a field assignment with target n, where the right hand side has the abstract value val.
        Parameters:
        val - the abstract value of the value assigned to n (or null if the abstract value is not known).
      • updateForLocalVariableAssignment

        protected void updateForLocalVariableAssignment​(LocalVariable receiver,
                                                        @Nullable V val)
        Set the abstract value of a local variable in the store. Overwrites any value that might have been available previously.
        Parameters:
        val - the abstract value of the value assigned to n (or null if the abstract value is not known).
      • removeConflicting

        protected void removeConflicting​(FieldAccess fieldAccess,
                                         @Nullable V val)
        Remove any information in this store that might not be true any more after fieldAccess has been assigned a new value (with the abstract value val). This includes the following steps (assume that fieldAccess is of the form a.f for some a.
        1. Update the abstract value of other field accesses b.g where the field is equal (that is, f=g), and the receiver b might alias the receiver of fieldAccess, a. This update will raise the abstract value for such field accesses to at least val (or the old value, if that was less precise). However, this is only necessary if the field g is not final.
        2. Remove any abstract values for field accesses b.g where fieldAccess might alias any expression in the receiver b.
        3. Remove any information about method calls.
        4. Remove any abstract values an array access b[i] where fieldAccess might alias any expression in the receiver a or index i.
        Parameters:
        val - the abstract value of the value assigned to n (or null if the abstract value is not known).
      • removeConflicting

        protected void removeConflicting​(ArrayAccess arrayAccess,
                                         @Nullable V val)
        Remove any information in the store that might not be true any more after arrayAccess has been assigned a new value (with the abstract value val). This includes the following steps (assume that arrayAccess is of the form a[i] for some a.
        1. Remove any abstract value for other array access b[j] where a and b can be aliases, or where either b or j contains a modifiable alias of a[i].
        2. Remove any abstract values for field accesses b.g where a[i] might alias any expression in the receiver b and there is an array expression somewhere in the receiver.
        3. Remove any information about method calls.
        Parameters:
        val - the abstract value of the value assigned to n (or null if the abstract value is not known).
      • removeConflicting

        protected void removeConflicting​(LocalVariable var)
        Remove any information in this store that might not be true any more after localVar has been assigned a new value. This includes the following steps:
        1. Remove any abstract values for field accesses b.g where localVar might alias any expression in the receiver b.
        2. Remove any abstract values for array accesses a[i] where localVar might alias the receiver a.
        3. Remove any information about method calls where the receiver or any of the parameters contains localVar.
      • canAlias

        public boolean canAlias​(JavaExpression a,
                                JavaExpression b)
        Can the objects a and b be aliases? Returns a conservative answer (i.e., returns true if not enough information is available to determine aliasing).
        Specified by:
        canAlias in interface Store<V extends CFAbstractValue<V>>
      • getValue

        public @Nullable V getValue​(LocalVariableNode n)
        Returns the current abstract value of a local variable, or null if no information is available.
        Parameters:
        n - the local variable
        Returns:
        the current abstract value of a local variable, or null if no information is available
      • getValue

        public @Nullable V getValue​(ThisNode n)
        Returns the current abstract value of the current object, or null if no information is available.
        Parameters:
        n - a reference to "this"
        Returns:
        the current abstract value of the current object, or null if no information is available
      • copy

        public S copy()
        Description copied from interface: Store
        Returns an exact copy of this store.
        Specified by:
        copy in interface Store<V extends CFAbstractValue<V>>
        Returns:
        an exact copy of this store
      • leastUpperBound

        public S leastUpperBound​(S other)
        Description copied from interface: Store
        Compute the least upper bound of two stores.

        Important: This method must fulfill the following contract:

        • Does not change this.
        • Does not change other.
        • Returns a fresh object which is not aliased yet.
        • Returns an object of the same (dynamic) type as this, even if the signature is more permissive.
        • Is commutative.
        Specified by:
        leastUpperBound in interface Store<V extends CFAbstractValue<V>>
      • widenedUpperBound

        public S widenedUpperBound​(S previous)
        Description copied from interface: Store
        Compute an upper bound of two stores that is wider than the least upper bound of the two stores. Used to jump to a higher abstraction to allow faster termination of the fixed point computations in Analysis. previous must be the previous store.

        A particular analysis might not require widening and should implement this method by calling leastUpperBound.

        Important: This method must fulfill the following contract:

        • Does not change this.
        • Does not change previous.
        • Returns a fresh object which is not aliased yet.
        • Returns an object of the same (dynamic) type as this, even if the signature is more permissive.
        • Is commutative.
        Specified by:
        widenedUpperBound in interface Store<V extends CFAbstractValue<V>>
        Parameters:
        previous - must be the previous store
      • supersetOf

        protected boolean supersetOf​(CFAbstractStore<V,​S> other)
        Returns true iff this CFAbstractStore contains a superset of the map entries of the argument CFAbstractStore. Note that we test the entry keys and values by Java equality, not by any subtype relationship. This method is used primarily to simplify the equals predicate.
      • equals

        public boolean equals​(@Nullable java.lang.Object o)
        Description copied from interface: Store
        Returns true if this is equal to the given argument.
        Specified by:
        equals in interface Store<V extends CFAbstractValue<V>>
        Overrides:
        equals in class java.lang.Object
        Parameters:
        o - the object to compare against this
        Returns:
        true if this is equal to the given argument
      • hashCode

        public int hashCode()
        Overrides:
        hashCode in class java.lang.Object
      • toString

        @SideEffectFree
        public java.lang.String toString()
        Overrides:
        toString in class java.lang.Object
      • visualize

        public java.lang.String visualize​(CFGVisualizer<?,​S,​?> viz)
        Description copied from interface: Store
        Delegate visualization responsibility to a visualizer.
        Specified by:
        visualize in interface Store<V extends CFAbstractValue<V>>
        Parameters:
        viz - the visualizer to visualize this store
        Returns:
        the String representation of this store
      • internalVisualize

        protected java.lang.String internalVisualize​(CFGVisualizer<V,​S,​?> viz)
        Adds a representation of the internal information of this Store to visualizer viz.
        Parameters:
        viz - the visualizer
        Returns:
        a representation of the internal information of this Store