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 - 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 V leastUpperBound(@Nullable V other)
      Description copied from interface: AbstractValue
      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.
      Specified by:
      leastUpperBound in interface AbstractValue<V extends CFAbstractValue<V>>

    • widenUpperBound

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

    • 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