Package org.checkerframework.checker.initialization

Class InitializationAnnotatedTypeFactory<Value extends CFAbstractValue<Value>,Store extends InitializationStore<Value,Store>,Transfer extends InitializationTransfer<Value,Transfer,Store>,Flow extends CFAbstractAnalysis<Value,Store,Transfer>>

java.lang.Object
org.checkerframework.framework.type.AnnotatedTypeFactory
org.checkerframework.framework.type.GenericAnnotatedTypeFactory<Value,Store,Transfer,Flow>
org.checkerframework.checker.initialization.InitializationAnnotatedTypeFactory<Value,Store,Transfer,Flow>
All Implemented Interfaces:
AnnotationProvider
Direct Known Subclasses:
NullnessAnnotatedTypeFactory
public abstract class InitializationAnnotatedTypeFactory<Value extends CFAbstractValue<Value>,Store extends InitializationStore<Value,Store>,Transfer extends InitializationTransfer<Value,Transfer,Store>,Flow extends CFAbstractAnalysis<Value,Store,Transfer>> extends GenericAnnotatedTypeFactory<Value,Store,Transfer,Flow>
The annotated type factory for the freedom-before-commitment type-system. The freedom-before-commitment type-system and this class are abstract and need to be combined with another type-system whose safe initialization should be tracked. For an example, see the NullnessChecker.

  • Field Details

  • Constructor Details

    • InitializationAnnotatedTypeFactory

      protected InitializationAnnotatedTypeFactory(BaseTypeChecker checker)
      Create a new InitializationAnnotatedTypeFactory.
      Parameters:
      checker - the checker to which the new type factory belongs

  • Method Details

    • getInitializationAnnotations

      public Set<Class<? extends Annotation>> getInitializationAnnotations()

    • isInitializationAnnotation

      protected boolean isInitializationAnnotation(AnnotationMirror anno)
      Is the annotation anno an initialization qualifier?
      Parameters:
      anno - the annotation to check
      Returns:
      true if the argument is an initialization qualifier

    • getInvalidConstructorReturnTypeAnnotations

      public Set<Class<? extends Annotation>> getInvalidConstructorReturnTypeAnnotations()
      Returns the list of annotations that is forbidden for the constructor return type.
      Returns:
      the list of annotations that is forbidden for the constructor return type

    • getFieldInvariantAnnotation

      public abstract AnnotationMirror getFieldInvariantAnnotation()
      Returns the annotation that makes up the invariant of this commitment type system, such as @NonNull.
      Returns:
      the invariant annotation for this type system

    • hasFieldInvariantAnnotation

      protected final boolean hasFieldInvariantAnnotation(VariableTree field)
      Returns whether or not field has the invariant annotation.

      This method is a convenience method for hasFieldInvariantAnnotation(AnnotatedTypeMirror, VariableElement).

      If the field is a type variable, this method returns true if any possible instantiation of the type parameter could have the invariant annotation. See hasFieldInvariantAnnotation(VariableTree) for an example.

      Parameters:
      field - field that might have invariant annotation
      Returns:
      whether or not field has the invariant annotation

    • hasFieldInvariantAnnotation

      protected abstract boolean hasFieldInvariantAnnotation(AnnotatedTypeMirror type, VariableElement fieldElement)
      Returns whether or not type has the invariant annotation.

      If the type is a type variable, this method returns true if any possible instantiation of the type parameter could have the invariant annotation. See hasFieldInvariantAnnotation(VariableTree) for an example.

      Parameters:
      type - of field that might have invariant annotation
      fieldElement - the field element, which can be used to check annotations on the declaration
      Returns:
      whether or not the type has the invariant annotation

    • createUnderInitializationAnnotation

      public AnnotationMirror createUnderInitializationAnnotation(TypeMirror typeFrame)
      Creates a UnderInitialization annotation with the given type as its type frame argument.
      Parameters:
      typeFrame - the type down to which some value has been initialized
      Returns:
      an UnderInitialization annotation with the given argument

    • createUnderInitializationAnnotation

      public AnnotationMirror createUnderInitializationAnnotation(Class<?> typeFrame)
      Creates a UnderInitialization annotation with the given type frame.
      Parameters:
      typeFrame - the type down to which some value has been initialized
      Returns:
      an UnderInitialization annotation with the given argument

    • createUnknownInitializationAnnotation

      public AnnotationMirror createUnknownInitializationAnnotation(Class<?> typeFrame)
      Creates a UnknownInitialization annotation with a given type frame.
      Parameters:
      typeFrame - the type down to which some value has been initialized
      Returns:
      an UnknownInitialization annotation with the given argument

    • createUnknownInitializationAnnotation

      public AnnotationMirror createUnknownInitializationAnnotation(TypeMirror typeFrame)
      Creates an UnknownInitialization annotation with a given type frame.
      Parameters:
      typeFrame - the type down to which some value has been initialized
      Returns:
      an UnknownInitialization annotation with the given argument

    • getTypeFrameFromAnnotation

      public TypeMirror getTypeFrameFromAnnotation(AnnotationMirror annotation)
      Returns the type frame (that is, the argument) of a given initialization annotation.
      Parameters:
      annotation - a UnderInitialization or UnknownInitialization annotation
      Returns:
      the annotation's argument

    • isUnderInitialization

      public boolean isUnderInitialization(AnnotationMirror anno)
      Is anno the UnderInitialization annotation (with any type frame)?
      Parameters:
      anno - the annotation to check
      Returns:
      true if anno is UnderInitialization

    • isUnknownInitialization

      public boolean isUnknownInitialization(AnnotationMirror anno)
      Is anno the UnknownInitialization annotation (with any type frame)?
      Parameters:
      anno - the annotation to check
      Returns:
      true if anno is UnknownInitialization

    • isFbcBottom

      public boolean isFbcBottom(AnnotationMirror anno)
      Is anno the bottom annotation?
      Parameters:
      anno - the annotation to check
      Returns:
      true if anno is FBCBottom

    • isInitialized

      public boolean isInitialized(AnnotationMirror anno)
      Is anno the Initialized annotation?
      Parameters:
      anno - the annotation to check
      Returns:
      true if anno is Initialized

    • isUnderInitialization

      public boolean isUnderInitialization(AnnotatedTypeMirror anno)
      Does anno have the annotation UnderInitialization (with any type frame)?
      Parameters:
      anno - the annotation to check
      Returns:
      true if anno has UnderInitialization

    • isUnknownInitialization

      public boolean isUnknownInitialization(AnnotatedTypeMirror anno)
      Does anno have the annotation UnknownInitialization (with any type frame)?
      Parameters:
      anno - the annotation to check
      Returns:
      true if anno has UnknownInitialization

    • isFbcBottom

      public boolean isFbcBottom(AnnotatedTypeMirror anno)
      Does anno have the bottom annotation?
      Parameters:
      anno - the annotation to check
      Returns:
      true if anno has FBCBottom

    • isInitialized

      public boolean isInitialized(AnnotatedTypeMirror anno)
      Does anno have the annotation Initialized?
      Parameters:
      anno - the annotation to check
      Returns:
      true if anno has Initialized

    • areAllFieldsInitializedOnly

      protected boolean areAllFieldsInitializedOnly(ClassTree classTree)
      Are all fields initialized-only?
      Parameters:
      classTree - the class to query
      Returns:
      true if all fields are initialized-only

    • postAsMemberOf

      public void postAsMemberOf(AnnotatedTypeMirror type, AnnotatedTypeMirror owner, Element element)
      A callback method for the AnnotatedTypeFactory subtypes to customize AnnotatedTypes.asMemberOf(). Overriding methods should merely change the annotations on the subtypes, without changing the types.

      In most cases, subclasses want to call this method first because it may clear all annotations and use the hierarchy's root annotations.

      Overrides:
      postAsMemberOf in class GenericAnnotatedTypeFactory<Value extends CFAbstractValue<Value>,Store extends InitializationStore<Value,Store>,Transfer extends InitializationTransfer<Value,Transfer,Store>,Flow extends CFAbstractAnalysis<Value,Store,Transfer>>
      Parameters:
      type - the annotated type of the element
      owner - the annotated type of the receiver of the accessing tree
      element - the element of the field or method

    • getAnnotatedTypeLhs

      public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree)
      Description copied from class: GenericAnnotatedTypeFactory
      Returns the type of a left-hand side of an assignment.

      The default implementation returns the type without considering dataflow type refinement. Subclass can override this method and add additional logic for computing the type of a LHS.

      Overrides:
      getAnnotatedTypeLhs in class GenericAnnotatedTypeFactory<Value extends CFAbstractValue<Value>,Store extends InitializationStore<Value,Store>,Transfer extends InitializationTransfer<Value,Transfer,Store>,Flow extends CFAbstractAnalysis<Value,Store,Transfer>>
      Parameters:
      lhsTree - left-hand side of an assignment
      Returns:
      AnnotatedTypeMirror of lhsTree

    • getSelfType

      public @Nullable AnnotatedTypeMirror.AnnotatedDeclaredType getSelfType(Tree tree)
      Description copied from class: AnnotatedTypeFactory
      Returns the type of this at the location of tree. Returns null if tree is in a location where this has no meaning, such as the body of a static method.

      The parameter is an arbitrary tree and does not have to mention "this", neither explicitly nor implicitly. This method can be overridden for type-system specific behavior.

      Overrides:
      getSelfType in class AnnotatedTypeFactory
      Parameters:
      tree - location used to decide the type of this
      Returns:
      the type of this at the location of tree

    • setSelfTypeInInitializationCode

      protected void setSelfTypeInInitializationCode(Tree tree, AnnotatedTypeMirror.AnnotatedDeclaredType selfType, TreePath path)
      Side-effects argument selfType to make it @Initialized or @UnderInitialization, depending on whether all fields have been set.
      Parameters:
      tree - a tree
      selfType - the type to side-effect
      path - a path

    • getUnderInitializationAnnotationOfSuperType

      protected AnnotationMirror getUnderInitializationAnnotationOfSuperType(TypeMirror type)
      Returns an UnderInitialization annotation that has the superclass of type as type frame.
      Parameters:
      type - a type
      Returns:
      true an UnderInitialization for the supertype of type

    • getUninitializedFields

      public org.plumelib.util.IPair<List<VariableTree>,List<VariableTree>> getUninitializedFields(Store store, TreePath path, boolean isStatic, Collection<? extends AnnotationMirror> receiverAnnotations)
      Returns the fields that are not yet initialized in a given store. The result is a pair of lists:
      • fields that are not yet initialized and have the invariant annotation
      • fields that are not yet initialized and do not have the invariant annotation
      Parameters:
      store - a store
      path - the current path, used to determine the current class
      isStatic - whether to report static fields or instance fields
      receiverAnnotations - the annotations on the receiver
      Returns:
      the fields that are not yet initialized in a given store (a pair of lists)

    • getUninitializedInvariantFields

      public final List<VariableTree> getUninitializedInvariantFields(Store store, TreePath path, boolean isStatic, List<? extends AnnotationMirror> receiverAnnotations)
      Returns the fields that have the invariant annotation and are not yet initialized in a given store.
      Parameters:
      store - a store
      path - the current path, used to determine the current class
      isStatic - whether to report static fields or instance fields
      receiverAnnotations - the annotations on the receiver
      Returns:
      the fields that have the invariant annotation and are not yet initialized in a given store (a pair of lists)

    • getInitializedInvariantFields

      public List<VariableTree> getInitializedInvariantFields(Store store, TreePath path)
      Returns the fields that have the invariant annotation and are initialized in a given store.
      Parameters:
      store - a store
      path - the current path; used to compute the current class
      Returns:
      the fields that have the invariant annotation and are initialized in a given store

    • isInitializedForFrame

      public boolean isInitializedForFrame(AnnotatedTypeMirror type, TypeMirror frame)
      Return true if the type is initialized with respect to the given frame -- that is, all of the fields of the frame are initialized.
      Parameters:
      type - the type whose initialization type qualifiers to check
      frame - a class in type's class hierarchy
      Returns:
      true if the type is initialized for the given frame

    • createTypeAnnotator

      protected TypeAnnotator createTypeAnnotator()
      Description copied from class: GenericAnnotatedTypeFactory
      Returns a DefaultForTypeAnnotator that adds annotations to a type based on the content of the type itself.

      Subclass may override this method. The default type annotator is a ListTypeAnnotator of the following:

      1. IrrelevantTypeAnnotator: Adds top to types not listed in the @RelevantJavaTypes annotation on the checker.
      2. PropagationTypeAnnotator: Propagates annotation onto wildcards.
      Overrides:
      createTypeAnnotator in class GenericAnnotatedTypeFactory<Value extends CFAbstractValue<Value>,Store extends InitializationStore<Value,Store>,Transfer extends InitializationTransfer<Value,Transfer,Store>,Flow extends CFAbstractAnalysis<Value,Store,Transfer>>
      Returns:
      a type annotator

    • createTreeAnnotator

      protected TreeAnnotator createTreeAnnotator()
      Description copied from class: GenericAnnotatedTypeFactory
      Returns a TreeAnnotator that adds annotations to a type based on the contents of a tree.

      The default tree annotator is a ListTreeAnnotator of the following:

      1. PropagationTreeAnnotator: Propagates annotations from subtrees
      2. LiteralTreeAnnotator: Adds annotations based on QualifierForLiterals meta-annotations
      3. DependentTypesTreeAnnotator: Adapts dependent annotations based on context

      Subclasses may override this method to specify additional tree annotators, for example: 

       new ListTreeAnnotator(super.createTreeAnnotator(), new KeyLookupTreeAnnotator(this));
      Overrides:
      createTreeAnnotator in class GenericAnnotatedTypeFactory<Value extends CFAbstractValue<Value>,Store extends InitializationStore<Value,Store>,Transfer extends InitializationTransfer<Value,Transfer,Store>,Flow extends CFAbstractAnalysis<Value,Store,Transfer>>
      Returns:
      a tree annotator