Package org.checkerframework.framework.flow

Class CFAbstractValue<V extends CFAbstractValue<V>>

java.lang.Object
org.checkerframework.framework.flow.CFAbstractValue<V>
Type Parameters:
V - the values that this CFAbstractValue wraps
All Implemented Interfaces:
AbstractValue<V>
Direct Known Subclasses:
AccumulationValue, CFValue, KeyForValue, NullnessValue
public abstract class CFAbstractValue<V extends CFAbstractValue<V>> extends Object implements AbstractValue<V>
An implementation of an abstract value used by the Checker Framework org.checkerframework.dataflow analysis.

A value holds a set of annotations and a type mirror. The set of annotations represents the primary annotation on a type; therefore, the set of annotations must have an annotation for each hierarchy unless the type mirror is a type variable or a wildcard that extends a type variable. Both type variables and wildcards may be missing a primary annotation. For this set of annotations, there is an additional constraint that only wildcards that extend type variables can be missing annotations.

In order to compute leastUpperBound(CFAbstractValue) and mostSpecific(CFAbstractValue, CFAbstractValue), the case where one value has an annotation in a hierarchy and the other does not must be handled. For type variables, the AnnotatedTypeMirror.AnnotatedTypeVariable for the declaration of the type variable is used. The AnnotatedTypeMirror.AnnotatedTypeVariable is computed using the type mirror. For wildcards, it is not always possible to get the AnnotatedTypeMirror.AnnotatedWildcardType for the type mirror. However, a CFAbstractValue's type mirror is only a wildcard if the type of some expression is a wildcard. The type of an expression is only a wildcard because the Checker Framework does not implement capture conversion. For these uses of uncaptured wildcards, only the primary annotation on the upper bound is ever used. So, the set of annotations represents the primary annotation on the wildcard's upper bound. If that upper bound is a type variable, then the set of annotations could be missing an annotation in a hierarchy.

  • Field Details

    • analysis

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

    • atypeFactory

      protected final AnnotatedTypeFactory atypeFactory
      The type factory.

    • qualHierarchy

      protected final QualifierHierarchy qualHierarchy
      The qualifier hierarchy.

    • underlyingType

      protected final TypeMirror underlyingType
      The underlying (Java) type in this abstract value.

    • annotations

      protected final AnnotationMirrorSet annotations
      The annotations in this abstract value.

  • Constructor Details

    • CFAbstractValue

      protected CFAbstractValue(CFAbstractAnalysis<V,?,?> analysis, AnnotationMirrorSet annotations, TypeMirror underlyingType)
      Creates a new CFAbstractValue.
      Parameters:
      analysis - the analysis class this value belongs to
      annotations - the annotations in this abstract value
      underlyingType - the underlying (Java) type in this abstract value

  • Method Details

    • validateSet

      public static boolean validateSet(AnnotationMirrorSet annos, TypeMirror typeMirror, AnnotatedTypeFactory atypeFactory)
      Returns true if the set has an annotation from every hierarchy (or if it doesn't need to); returns false if the set is missing an annotation from some hierarchy.
      Parameters:
      annos - a set of annotations
      typeMirror - where the annotations are written
      atypeFactory - the type factory
      Returns:
      true if no annotations are missing

    • canBeMissingAnnotations

      public boolean canBeMissingAnnotations()
      Returns whether or not the set of annotations can be missing an annotation for any hierarchy.
      Returns:
      whether or not the set of annotations can be missing an annotation

    • getAnnotations

      @Pure public AnnotationMirrorSet getAnnotations()
      Returns a set of annotations. If canBeMissingAnnotations() returns true, then the set of annotations may not have an annotation for every hierarchy.

      To get the single annotation in a particular hierarchy, use QualifierHierarchy.findAnnotationInHierarchy(java.util.Collection<? extends javax.lang.model.element.AnnotationMirror>, javax.lang.model.element.AnnotationMirror).

      Returns:
      a set of annotations

    • getUnderlyingType

      @Pure public TypeMirror getUnderlyingType()

    • equals

      public boolean equals(@Nullable Object obj)
      Overrides:
      equals in class Object

    • hashCode

      @Pure public int hashCode()
      Overrides:
      hashCode in class Object

    • toStringFullyQualified

      @SideEffectFree public String toStringFullyQualified()
      Returns the string representation, using fully-qualified names.
      Returns:
      the string representation, using fully-qualified names

    • toStringSimple

      @SideEffectFree public String toStringSimple()
      Returns the string representation, using simple (not fully-qualified) names.
      Returns:
      the string representation, using simple (not fully-qualified) names

    • toString

      @SideEffectFree public String toString()
      Returns the string representation.
      Overrides:
      toString in class Object
      Returns:
      the string representation

    • mostSpecific

      public V mostSpecific(@Nullable V other, @Nullable V backup)
      Returns the more specific of two values this and other. If they do not contain information for all hierarchies, then it is possible that information from both this and other are taken.

      If neither of the two is more specific for one of the hierarchies (i.e., if the two are incomparable as determined by QualifierHierarchy.isSubtypeShallow(AnnotationMirror, TypeMirror, AnnotationMirror, TypeMirror), then the respective value from backup is used.

      Parameters:
      other - the other value to obtain information from
      backup - the value to use if this and other are incomparable
      Returns:
      the more specific of two values this and other

    • leastUpperBound

      public final V leastUpperBound(@Nullable V other)
      Compute the least upper bound of two values.

      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.

      Subclasses should override upperBound(CFAbstractValue, TypeMirror, boolean) instead of this method.

      Specified by:
      leastUpperBound in interface AbstractValue<V extends CFAbstractValue<V>>
      Parameters:
      other - the other value
      Returns:
      the least upper bound of the two values

    • leastUpperBound

      public final V leastUpperBound(@Nullable V other, TypeMirror typeMirror)
      Compute the least upper bound of two abstract values. The returned value has a Java type of typeMirror. typeMirror should be an upper bound of the Java types of this an other, but it does not have be to the least upper bound.

      Subclasses should override upperBound(CFAbstractValue, TypeMirror, boolean) instead of this method.

      Parameters:
      other - another value
      typeMirror - the underlying Java type of the returned value, which may or may not be the least upper bound
      Returns:
      the least upper bound of two abstract values

    • widenUpperBound

      public final V widenUpperBound(@Nullable V previous)
      Compute an upper bound of two values that is wider than the least upper bound of the two values. Used to jump to a higher abstraction to allow faster termination of the fixed point computations in Analysis.

      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.
      Subclasses should override upperBound(CFAbstractValue, TypeMirror, boolean) instead of this method.
      Parameters:
      previous - must be the previous value
      Returns:
      an upper bound of two values that is wider than the least upper bound of the two values

    • upperBound

      protected V upperBound(@Nullable V other, TypeMirror upperBoundTypeMirror, boolean shouldWiden)
      Returns an upper bound of this and other. The underlying type of the value returned is upperBoundTypeMirror. If shouldWiden is false, this method returns the least upper bound of this and other.

      This is the implementation of leastUpperBound(CFAbstractValue, TypeMirror), leastUpperBound(CFAbstractValue), widenUpperBound(CFAbstractValue), and upperBound(CFAbstractValue, boolean). Subclasses may override it.

      Parameters:
      other - an abstract value
      upperBoundTypeMirror - the underlying type of the returned value
      shouldWiden - true if the method should perform widening
      Returns:
      an upper bound of this and other

    • greatestLowerBound

      public V greatestLowerBound(@Nullable V other)
      Compute the greatest lower bound of two values.

      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.
      Parameters:
      other - another value
      Returns:
      the greatest lower bound of two values