Package org.checkerframework.framework.flow

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

java.lang.Object
org.checkerframework.framework.flow.CFAbstractStore<V,S>
All Implemented Interfaces:
Store<S>, org.plumelib.util.UniqueId
Direct Known Subclasses:
AccumulationStore, CFStore, InitializationStore, KeyForStore, LockStore
public abstract class CFAbstractStore<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>> extends 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 Details

    • analysis

      protected final CFAbstractAnalysis<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,?> analysis
      The analysis class this store belongs to.

    • localVariableValues

      protected final 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.

    • fieldValues

      protected Map<FieldAccess,V extends CFAbstractValue<V>> fieldValues
      Information collected about fields, using the internal representation FieldAccess.

    • arrayValues

      protected final Map<ArrayAccess,V extends CFAbstractValue<V>> arrayValues
      Information collected about array elements, using the internal representation ArrayAccess.

    • methodValues

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

    • classValues

      protected final 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 Details

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

    • getFieldValues

      public 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(AnnotationMirror a, 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, ExecutableElement method)
      Deprecated.
      use AnnotationProvider.isSideEffectFree(javax.lang.model.element.ExecutableElement)
      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, AnnotatedTypeFactory 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 unmodifiability property 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

    • newFieldValueAfterMethodCall

      protected V newFieldValueAfterMethodCall(FieldAccess fieldAccess, GenericAnnotatedTypeFactory<V,S,?,?> atypeFactory, V value)
      Returns the new value of a field after a method call, or null if the field should be removed from the store.

      In this default implementation, the field's value is preserved if it is either unassignable (see FieldAccess.isUnassignableByOtherCode()) or has a monotonic qualifier (see newMonotonicFieldValueAfterMethodCall(FieldAccess, GenericAnnotatedTypeFactory, CFAbstractValue)). Otherwise, it is removed from the store.

      Parameters:
      fieldAccess - the field whose value to update
      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 should be removed from the store

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

    • insertValuePermitNondeterministic

      public void insertValuePermitNondeterministic(JavaExpression expr, AnnotationMirror a)
      Like insertValue(JavaExpression, AnnotationMirror), but permits nondeterministic expressions to be stored.

      For an explanation of when to permit nondeterministic expressions, see insertValuePermitNondeterministic(JavaExpression, CFAbstractValue).

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

    • insertOrRefine

      public final void insertOrRefine(JavaExpression expr, 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

    • insertOrRefinePermitNondeterministic

      public final void insertOrRefinePermitNondeterministic(JavaExpression expr, AnnotationMirror newAnno)
      Like insertOrRefine(JavaExpression, AnnotationMirror), but permits nondeterministic expressions to be inserted.

      For an explanation of when to permit nondeterministic expressions, see insertValuePermitNondeterministic(JavaExpression, CFAbstractValue).

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

    • insertOrRefine

      protected void insertOrRefine(JavaExpression expr, AnnotationMirror newAnno, boolean permitNondeterministic)
      Helper function for insertOrRefine(JavaExpression, AnnotationMirror) and insertOrRefinePermitNondeterministic(org.checkerframework.dataflow.expression.JavaExpression, javax.lang.model.element.AnnotationMirror).
      Parameters:
      expr - an expression
      newAnno - the expression's annotation
      permitNondeterministic - whether nondeterministic expressions may be inserted into the store

    • 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 that nondet() is odd. This means that the next call to nondet() 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

    • insertValue

      protected void insertValue(JavaExpression expr, @Nullable V value, boolean permitNondeterministic)
      Helper method for insertValue(JavaExpression, CFAbstractValue) and insertValuePermitNondeterministic(org.checkerframework.dataflow.expression.JavaExpression, javax.lang.model.element.AnnotationMirror).

      Every overriding implementation should start with 

      
 if (!shouldInsert) {
   return;
 }
      Parameters:
      expr - the expression to insert in the store
      value - the value of the expression
      permitNondeterministic - if false, does nothing if expr is nondeterministic; if true, permits nondeterministic expressions to be placed in the store

    • computeNewValueAndInsert

      protected void computeNewValueAndInsert(JavaExpression expr, @Nullable V value, 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(AnnotationMirror a, 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).

    • updateForArrayAssignment

      protected void updateForArrayAssignment(ArrayAccess arrayAccess, @Nullable V val)
      Update the information in the store by considering an assignment with target n, where the target is an array access.

      See removeConflicting(ArrayAccess,CFAbstractValue), as it is called first by this method.

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

    • toString

      @SideEffectFree public String toString()
      Overrides:
      toString in class Object

    • visualize

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