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. Also supports rawness as a type-system for tracking initialization, though FBC is preferred.

Author:

Stefan Heule

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected class	InitializationAnnotatedTypeFactory.CommitmentTreeAnnotator
protected class	InitializationAnnotatedTypeFactory.CommitmentTypeAnnotator
protected class	InitializationAnnotatedTypeFactory.InitializationQualifierHierarchy The QualifierHierarchy for the initialization type system.

Nested classes/interfaces inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory

GenericAnnotatedTypeFactory.ScanState

Nested classes/interfaces inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory

AnnotatedTypeFactory.InheritedFromClassAnnotator

Field Summary

Fields

Modifier and Type	Field and Description
protected AnnotationMirror	COMMITTED Initialized or NonRaw
protected AnnotationMirror	FBCBOTTOM FBCBottom or NonRaw
protected AnnotationMirror	FREE UnderInitialization or null
protected Set<Class<? extends Annotation>>	initAnnos
protected AnnotationMirror	NOT_ONLY_COMMITTED NotOnlyInitialized or null
protected AnnotationMirror	UNCLASSIFIED UnknownInitialization or Raw
protected boolean	useFbc Should the initialization type system be FBC? If not, the rawness type system is used for initialization.

Fields inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory

analyses, cfgVisualizer, defaults, dependentTypesHelper, FLOW_BY_DEFAULT, flowResult, initializationStaticStore, initializationStore, methodInvocationStores, poly, regularExitStores, returnStatementStores, scannedClasses, treeAnnotator, typeAnnotator

Fields inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory

checker, elements, fromTreeCache, loader, processingEnv, qualHierarchy, reflectionResolver, root, shouldCache, trees, typeArgumentInference, typeFormatter, typeHierarchy, types, typeVarSubstitutor, uid, visitorState

Constructor Summary

Constructors

Constructor and Description
InitializationAnnotatedTypeFactory(BaseTypeChecker checker, boolean useFbc)

Method Summary

Modifier and Type	Method and Description
protected boolean	areAllFieldsCommittedOnly(ClassTree classTree) Are all fields committed-only?
AnnotationMirror	createFreeAnnotation(Class<?> typeFrame) Returns a UnderInitialization annotation with a given type frame.
AnnotationMirror	createFreeAnnotation(TypeMirror typeFrame) Returns a UnderInitialization annotation with a given type frame.
protected MultiGraphQualifierHierarchy.MultiGraphFactory	createQualifierHierarchyFactory() Factory method to easily change what Factory is used to create a QualifierHierarchy.
protected TreeAnnotator	createTreeAnnotator() Returns a TreeAnnotator that adds annotations to a type based on the contents of a tree.
protected TypeAnnotator	createTypeAnnotator() Returns a ImplicitsTypeAnnotator that adds annotations to a type based on the content of the type itself.
AnnotationMirror	createUnclassifiedAnnotation(Class<?> typeFrame) Returns a UnknownInitialization or Raw annotation with a given type frame.
AnnotationMirror	createUnclassifiedAnnotation(TypeMirror typeFrame) Returns a UnknownInitialization annotation with a given type frame.
AnnotatedTypeMirror	getAnnotatedTypeLhs(Tree lhsTree) Returns the type of a left-hand side of an assignment.
abstract AnnotationMirror	getFieldInvariantAnnotation() Returns the annotation that makes up the invariant of this commitment type system, such as @NonNull.
protected AnnotationMirror	getFreeOrRawAnnotationOfSuperType(TypeMirror type) Returns a UnderInitialization annotation (or UnknownInitialization if rawness is used) that has the supertype of type as type frame.
Set<Class<? extends Annotation>>	getInitializationAnnotations()
List<VariableTree>	getInitializedInvariantFields(Store store, TreePath path) Returns the (non-static) fields that have the invariant annotation and are initialized in a given store.
Set<Class<? extends Annotation>>	getInvalidConstructorReturnTypeAnnotations()
AnnotatedTypeMirror.AnnotatedDeclaredType	getSelfType(Tree tree) Returns the type of this in the current location, which can be used if this has a special semantics (e.g.
TypeMirror	getTypeFrameFromAnnotation(AnnotationMirror annotation) Returns the type frame of a given annotation.
List<VariableTree>	getUninitializedInvariantFields(Store store, TreePath path, boolean isStatic, List<? extends AnnotationMirror> receiverAnnotations) Returns the (non-static) fields that have the invariant annotation and are not yet initialized in a given store.
protected abstract boolean	hasFieldInvariantAnnotation(VariableTree field) Returns whether or not field has the invariant annotation.
boolean	isCommitted(AnnotatedTypeMirror anno) Does anno have the annotation Initialized? If useFbc is false, then NonRaw is used in the comparison.
boolean	isCommitted(AnnotationMirror anno) Is anno the Initialized annotation? If useFbc is false, then NonRaw is used in the comparison.
boolean	isFbcBottom(AnnotatedTypeMirror anno) Does anno have the bottom annotation?
boolean	isFbcBottom(AnnotationMirror anno) Is anno the bottom annotation?
boolean	isFree(AnnotatedTypeMirror anno) Does anno have the annotation UnderInitialization (with any type frame)? Always returns false if useFbc is false.
boolean	isFree(AnnotationMirror anno) Is anno the UnderInitialization annotation (with any type frame)? Always returns false if useFbc is false.
protected boolean	isInitializationAnnotation(AnnotationMirror anno) Is the annotation anno an initialization qualifier?
boolean	isInitializedForFrame(AnnotatedTypeMirror type, TypeMirror frame)
boolean	isUnclassified(AnnotatedTypeMirror anno) Does anno have the annotation UnknownInitialization (with any type frame)? If useFbc is false, then Raw is used in the comparison.
boolean	isUnclassified(AnnotationMirror anno) Is anno the UnknownInitialization annotation (with any type frame)? If useFbc is false, then Raw is used in the comparison.
void	postAsMemberOf(AnnotatedTypeMirror type, AnnotatedTypeMirror owner, Element element) A callback method for the AnnotatedTypeFactory subtypes to customize AnnotatedTypes.asMemberOf().
protected void	setSelfTypeInInitializationCode(Tree tree, AnnotatedTypeMirror.AnnotatedDeclaredType selfType, TreePath path)

Methods inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory

addCheckedCodeDefaults, addCheckedStandardDefaults, addComputedTypeAnnotations, addComputedTypeAnnotations, addComputedTypeAnnotations, addTypeNameImplicit, addUncheckedCodeDefaults, addUncheckedStandardDefaults, analyze, analyze, applyInferredAnnotations, checkAndPerformFlowAnalysis, checkForDefaultQualifierInHierarchy, constructorFromUse, createCFGVisualizer, createDependentTypesHelper, createFlowAnalysis, createFlowTransferFunction, createQualifierDefaults, createQualifierPolymorphism, fromNewClass, getAnnotatedTypeLhsNoTypeVarDefault, getAnnotationFromJavaExpressionString, getCFGVisualizer, getDependentTypesHelper, getEmptyStore, getFinalLocalValues, getInferredValueFor, getMethodReturnType, getMethodReturnType, getNodeForTree, getReceiverFromJavaExpressionString, getRegularExitStore, getResultingTypeOfConstructorMemberReference, getReturnStatementStores, getShouldDefaultTypeVarLocals, getSortedQualifierNames, getStoreAfter, getStoreBefore, getStoreBefore, getSupportedMonotonicTypeQualifiers, getTypeFactoryOfSubchecker, handleCFGViz, methodFromUse, performFlowAnalysis, postDirectSuperTypes, postInit, preProcessClassTree, setRoot, typeVariablesFromUse

Methods inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory

adaptGetClassReturnTypeToReceiver, addAliasedAnnotation, addAliasedDeclAnnotation, addInheritedAnnotation, aliasedAnnotation, annotateInheritedFromClass, annotateInheritedFromClass, checkInvalidOptionsInferSignatures, createAnnotatedTypeFormatter, createAnnotationFormatter, createQualifierHierarchy, createQualifierHierarchy, createQualifierHierarchy, createSupportedTypeQualifiers, createTypeArgumentInference, createTypeHierarchy, createTypeVariableSubstitutor, declarationFromElement, fromElement, fromElement, fromElement, getAnnotatedNullType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedTypeFormatter, getAnnotatedTypeFromTypeTree, getAnnotationFormatter, getAnnotationMirror, getAnnotationWithMetaAnnotation, getBoxedType, getBundledTypeQualifiersWithoutPolyAll, getBundledTypeQualifiersWithPolyAll, getContext, getCurrentClassTree, getCurrentClassType, getCurrentMethodReceiver, getDeclAnnotation, getDeclAnnotationNoAliases, getDeclAnnotations, getDeclAnnotationWithMetaAnnotation, getElementUtils, getEnclosingMethod, getEnclosingType, getFnInterfaceFromTree, getFnInterfaceFromTree, getImplicitReceiverType, getNarrowedPrimitive, getPath, getProcessingEnv, getQualifierHierarchy, getReceiverType, getStringType, getSupportedTypeQualifiers, getTreeUtils, getTypeArgumentInference, getTypeHierarchy, getTypeVarSubstitutor, getUnboxedType, getUninferredWildcardType, getVisitorState, getWholeProgramInference, initializeReflectionResolution, isAnyEnclosingThisDeref, isFromByteCode, isFromStubFile, isMostEnclosingThisDeref, isSupportedQualifier, isWithinConstructor, methodFromUse, parseStubFiles, postProcessClassTree, postTypeVarSubstitution, setPathHack, toAnnotatedType, toString, type, widenToUpperBound

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

UNCLASSIFIED

protected final AnnotationMirror UNCLASSIFIED

UnknownInitialization or Raw

COMMITTED

protected final AnnotationMirror COMMITTED

Initialized or NonRaw

FREE

protected final AnnotationMirror FREE

UnderInitialization or null

NOT_ONLY_COMMITTED

protected final AnnotationMirror NOT_ONLY_COMMITTED

NotOnlyInitialized or null

FBCBOTTOM

protected final AnnotationMirror FBCBOTTOM

FBCBottom or NonRaw

useFbc

protected final boolean useFbc

Should the initialization type system be FBC? If not, the rawness type system is used for initialization.

initAnnos

protected final Set<Class<? extends Annotation>> initAnnos

Constructor Detail

InitializationAnnotatedTypeFactory

public InitializationAnnotatedTypeFactory(BaseTypeChecker checker,
                                          boolean useFbc)

Method Detail

getInitializationAnnotations

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

isInitializationAnnotation

protected boolean isInitializationAnnotation(AnnotationMirror anno)

Is the annotation anno an initialization qualifier?

getInvalidConstructorReturnTypeAnnotations

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

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.

hasFieldInvariantAnnotation

protected abstract boolean hasFieldInvariantAnnotation(VariableTree field)

Returns whether or not field has the invariant annotation.

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 NullnessAnnotatedTypeFactory.hasFieldInvariantAnnotation(VariableTree) for an example.

Parameters:

field - field that might have invariant annotation

Returns:

whether or not field has the invariant annotation

createFreeAnnotation

public AnnotationMirror createFreeAnnotation(TypeMirror typeFrame)

Returns a UnderInitialization annotation with a given type frame.

createFreeAnnotation

public AnnotationMirror createFreeAnnotation(Class<?> typeFrame)

Returns a UnderInitialization annotation with a given type frame.

createUnclassifiedAnnotation

public AnnotationMirror createUnclassifiedAnnotation(Class<?> typeFrame)

Returns a UnknownInitialization or Raw annotation with a given type frame.

createUnclassifiedAnnotation

public AnnotationMirror createUnclassifiedAnnotation(TypeMirror typeFrame)

Returns a UnknownInitialization annotation with a given type frame.

getTypeFrameFromAnnotation

public TypeMirror getTypeFrameFromAnnotation(AnnotationMirror annotation)

Returns the type frame of a given annotation. The annotation must either be UnderInitialization or UnknownInitialization.

isFree

public boolean isFree(AnnotationMirror anno)

Is anno the UnderInitialization annotation (with any type frame)? Always returns false if useFbc is false.

isUnclassified

public boolean isUnclassified(AnnotationMirror anno)

Is anno the UnknownInitialization annotation (with any type frame)? If useFbc is false, then Raw is used in the comparison.

isFbcBottom

public boolean isFbcBottom(AnnotationMirror anno)

Is anno the bottom annotation?

isCommitted

public boolean isCommitted(AnnotationMirror anno)

Is anno the Initialized annotation? If useFbc is false, then NonRaw is used in the comparison.

isFree

public boolean isFree(AnnotatedTypeMirror anno)

Does anno have the annotation UnderInitialization (with any type frame)? Always returns false if useFbc is false.

isUnclassified

public boolean isUnclassified(AnnotatedTypeMirror anno)

Does anno have the annotation UnknownInitialization (with any type frame)? If useFbc is false, then Raw is used in the comparison.

isFbcBottom

public boolean isFbcBottom(AnnotatedTypeMirror anno)

Does anno have the bottom annotation?

isCommitted

public boolean isCommitted(AnnotatedTypeMirror anno)

Does anno have the annotation Initialized? If useFbc is false, then NonRaw is used in the comparison.

createQualifierHierarchyFactory

protected MultiGraphQualifierHierarchy.MultiGraphFactory createQualifierHierarchyFactory()

Description copied from class: AnnotatedTypeFactory

Factory method to easily change what Factory is used to create a QualifierHierarchy.

Overrides:

createQualifierHierarchyFactory in class AnnotatedTypeFactory

areAllFieldsCommittedOnly

protected boolean areAllFieldsCommittedOnly(ClassTree classTree)

Are all fields committed-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 AnnotatedTypeFactory

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 AnnotatedTypeMirror.AnnotatedDeclaredType getSelfType(Tree tree)

Description copied from class: AnnotatedTypeFactory

Returns the type of this in the current location, which can be used if this has a special semantics (e.g. this is non-null).

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

TODO: in 1.8.2, handle all receiver type annotations. TODO: handle enclosing classes correctly.

Overrides:

getSelfType in class AnnotatedTypeFactory

setSelfTypeInInitializationCode

protected void setSelfTypeInInitializationCode(Tree tree,
                                               AnnotatedTypeMirror.AnnotatedDeclaredType selfType,
                                               TreePath path)

getFreeOrRawAnnotationOfSuperType

protected AnnotationMirror getFreeOrRawAnnotationOfSuperType(TypeMirror type)

Returns a UnderInitialization annotation (or UnknownInitialization if rawness is used) that has the supertype of type as type frame.

getUninitializedInvariantFields

public List<VariableTree> getUninitializedInvariantFields(Store store,
                                                          TreePath path,
                                                          boolean isStatic,
                                                          List<? extends AnnotationMirror> receiverAnnotations)

Returns the (non-static) fields that have the invariant annotation and are not yet initialized in a given store.

getInitializedInvariantFields

public List<VariableTree> getInitializedInvariantFields(Store store,
                                                        TreePath path)

Returns the (non-static) fields that have the invariant annotation and are initialized in a given store.

isInitializedForFrame

public boolean isInitializedForFrame(AnnotatedTypeMirror type,
                                     TypeMirror frame)

createTypeAnnotator

protected TypeAnnotator createTypeAnnotator()

Description copied from class: GenericAnnotatedTypeFactory

Returns a ImplicitsTypeAnnotator 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
3. ImplicitsTypeAnnotator: Adds annotations based on ImplicitFor meta-annotations

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.

Subclasses may override this method to specify a more appropriate TreeAnnotator. The default tree annotator is a ListTreeAnnotator of the following:

1. PropagationTreeAnnotator: Propagates annotations from subtrees.
2. ImplicitsTreeAnnotator: Adds annotations based on ImplicitFor meta-annotations

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