Package org.checkerframework.framework.flow

Class CFAbstractValue<V extends CFAbstractValue<V>>

  • Type Parameters:
    V - the values that this CFAbstractValue wraps
    All Implemented Interfaces:
    AbstractValue<V>
    Direct Known Subclasses:
    AccumulationValue, CFValue, KeyForValue, NullnessNoInitValue
    public abstract class CFAbstractValue<V extends CFAbstractValue<V>>
extends java.lang.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 Detail

      • underlyingType

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

      • annotations

        protected final AnnotationMirrorSet annotations
        The annotations in this abstract value.

    • Constructor Detail

      • CFAbstractValue

        protected CFAbstractValue​(CFAbstractAnalysis<V,​?,​?> analysis,
                          AnnotationMirrorSet annotations,
                          javax.lang.model.type.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 Detail

      • validateSet

        public static boolean validateSet​(AnnotationMirrorSet annos,
                                  javax.lang.model.type.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

      • getUnderlyingType

        @Pure
public javax.lang.model.type.TypeMirror getUnderlyingType()

      • equals

        public boolean equals​(@Nullable java.lang.Object obj)
        Overrides:
        equals in class java.lang.Object

      • hashCode

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

      • toStringFullyQualified

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

      • toStringSimple

        @SideEffectFree
public java.lang.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 java.lang.String toString()
        Returns the string representation.
        Overrides:
        toString in class java.lang.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