Class AccumulationAnnotatedTypeFactory
- All Implemented Interfaces:
AnnotationProvider
- Direct Known Subclasses:
CalledMethodsAnnotatedTypeFactory
,InitializedFieldsAnnotatedTypeFactory
New accumulation checkers should extend this class and implement a constructor, which should
take a BaseTypeChecker
and call both the constructor defined in this class and GenericAnnotatedTypeFactory.postInit()
.
-
Nested Class Summary
Modifier and TypeClassDescriptionprotected class
All accumulation analyses share a similar type hierarchy.protected class
This tree annotator implements the following rule(s): RRA If a method returns its receiver, and the receiver has an accumulation type, then the default type of the method's return value is the type of the receiver.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.CapturedTypeVarSubstitutor, AnnotatedTypeFactory.ParameterizedExecutableType
-
Field Summary
Modifier and TypeFieldDescriptionfinal AccumulationChecker
The typechecker associated with this factory.final AnnotationMirror
The canonical bottom annotation for this accumulation checker.final AnnotationMirror
The canonical top annotation for this accumulation checker: an instance of the accumulator annotation with no arguments.Fields inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory
analysis, arraysAreRelevant, cfgVisualizer, contractsUtils, defaults, dependentTypesHelper, emptyStore, exceptionalExitStores, flowByDefault, flowResult, flowResultAnalysisCaches, formalParameterPattern, hasOrIsSubchecker, initializationStaticStore, initializationStore, methodInvocationStores, poly, regularExitStores, relevantJavaTypes, returnStatementStores, scannedClasses, shouldClearSubcheckerSharedCFGs, sideEffectsUnrefineAliases, subcheckerSharedCFG, transfer, treeAnnotator, typeAnnotator
Fields inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory
ajavaTypes, annotatedForValueElement, artificialTreeToEnclosingElementMap, capturedTypeVarSubstitutor, checker, currentFileAjavaTypes, elements, ensuresQualifierExpressionElement, ensuresQualifierIfExpressionElement, ensuresQualifierIfListTM, ensuresQualifierIfListValueElement, ensuresQualifierIfResultElement, ensuresQualifierIfTM, ensuresQualifierListTM, ensuresQualifierListValueElement, ensuresQualifierTM, fieldInvariantFieldElement, fieldInvariantQualifierElement, fromExpressionTreeCache, fromMemberTreeCache, fromTypeTreeCache, hasQualifierParameterValueElement, ignoreRawTypeArguments, loader, methodValClassNameElement, methodValMethodNameElement, methodValParamsElement, noQualifierParameterValueElement, objectGetClass, processingEnv, qualHierarchy, qualifierUpperBounds, reflectionResolver, requiresQualifierExpressionElement, requiresQualifierListTM, requiresQualifierListValueElement, requiresQualifierTM, root, shouldCache, stubTypes, trees, typeArgumentInference, typeFormatter, typeHierarchy, typeInformationPresenter, types, typeVarSubstitutor, uid, wpiOutputFormat
-
Constructor Summary
ModifierConstructorDescriptionprotected
AccumulationAnnotatedTypeFactory
(BaseTypeChecker checker, Class<? extends Annotation> accumulator, Class<? extends Annotation> bottom) Create an annotated type factory for an accumulation checker.protected
AccumulationAnnotatedTypeFactory
(BaseTypeChecker checker, Class<? extends Annotation> accumulator, Class<? extends Annotation> bottom, @Nullable Class<? extends Annotation> predicate) Create an annotated type factory for an accumulation checker. -
Method Summary
Modifier and TypeMethodDescriptionprotected String
Converts the given annotation mirror to a predicate.Creates a new instance of the accumulator annotation that contains exactly one value.createAccumulatorAnnotation
(List<String> values) Creates a new instance of the accumulator annotation that contains the elements ofvalues
.protected AnnotationMirror
Creates a new predicate annotation from the given string.protected QualifierHierarchy
Returns theQualifierHierarchy
to be used by this checker.protected TreeAnnotator
Returns aTreeAnnotator
that adds annotations to a type based on the contents of a tree.protected boolean
evaluatePredicate
(List<String> trueVariables, String pred) Evaluates whether treating the variables intrueVariables
astrue
literals (and all other names asfalse
literals) makes the predicatepred
evaluate to true.protected boolean
evaluatePredicate
(AnnotationMirror subAnno, String pred) Evaluates whether the accumulator annotationsubAnno
makes the predicatepred
true.getAccumulatedValues
(Tree tree) Returns the accumulated values on the given (expression, usually) tree.Returns all the values that anno has accumulated.boolean
Is the given annotation an accumulator annotation? Returns false if the argument isbottom
.protected boolean
isPredicate
(AnnotationMirror anno) Returns true if anno is a predicate annotation.protected boolean
isPredicateSubtype
(String p, String q) Extension point for subtyping behavior between predicates.boolean
Returns true if the return type of the given method invocation tree has an @This annotation from the Returns Receiver Checker.Methods inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory
addAnnotationsFromDefaultForType, addCheckedCodeDefaults, addCheckedStandardDefaults, addComputedTypeAnnotations, addComputedTypeAnnotations, addComputedTypeAnnotations, addComputedTypeAnnotationsForWarnRedundant, addDefaultAnnotations, addSharedCFGForTree, addUncheckedStandardDefaults, analyze, annotationsForIrrelevantJavaType, applyInferredAnnotations, applyQualifierParameterDefaults, applyQualifierParameterDefaults, checkAndPerformFlowAnalysis, checkForDefaultQualifierInHierarchy, constructorFromUse, constructorFromUsePreSubstitution, createAndInitQualifierDefaults, createCFGVisualizer, createContractsFromMethod, createDefaultForTypeAnnotator, createDefaultForUseTypeAnnotator, createDependentTypesHelper, createFlowAnalysis, createFlowTransferFunction, createQualifierDefaults, createQualifierPolymorphism, createRequiresOrEnsuresQualifier, createTypeAnnotator, getAnnotatedTypeLhs, getAnnotatedTypeLhsNoTypeVarDefault, getAnnotatedTypeRhsUnaryAssign, getAnnotatedTypeVarargsArray, getAnnotationFromJavaExpression, getAnnotationFromJavaExpressionString, getAnnotationMirrorFromJavaExpressionString, getAnnotationsFromJavaExpression, getCFGVisualizer, getContractAnnotations, getContractAnnotations, getContractExpressions, getContractsFromMethod, getDefaultAnnotations, getDefaultAnnotationsForWarnRedundant, getDefaultForTypeAnnotator, getDefaultValueAnnotatedType, getDependentTypesHelper, getEmptyStore, getEnsuresQualifierIfResult, getExceptionalExitStore, getExplicitNewClassAnnos, getExplicitNewClassClassTypeArgs, getExpressionAndOffsetFromJavaExpressionString, getFinalLocalValues, getFirstNodeOfKindForTree, getInferredValueFor, getMethodReturnType, getNodesForTree, getPostconditionAnnotations, getPostconditionAnnotations, getPostconditionAnnotations, getPreconditionAnnotations, getPreconditionAnnotations, getPreconditionAnnotations, getPreOrPostconditionAnnotations, getQualifierPolymorphism, getRegularExitStore, getReturnStatementStores, getSharedCFGForTree, getShouldDefaultTypeVarLocals, getSortedQualifierNames, getStoreAfter, getStoreAfter, getStoreAfter, getStoreBefore, getStoreBefore, getStoreBefore, getSupportedMonotonicTypeQualifiers, getTypeFactoryOfSubchecker, getTypeFactoryOfSubcheckerOrNull, handleCFGViz, irrelevantExtraMessage, isIgnoredExceptionType, isRelevant, isRelevant, isRelevantImpl, isUnreachable, methodFromUse, methodFromUsePreSubstitution, parseJavaExpressionString, performFlowAnalysis, postAnalyze, postAsMemberOf, postDirectSuperTypes, postInit, preProcessClassTree, setRoot, typeVariablesFromUse
Methods inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory
adaptGetClassReturnTypeToReceiver, addAliasedDeclAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAnnotationFromFieldInvariant, addInheritedAnnotation, applyCaptureConversion, applyCaptureConversion, applyUnboxing, areSameByClass, binaryTreeArgTypes, binaryTreeArgTypes, canonicalAnnotation, checkInvalidOptionsInferSignatures, compoundAssignmentTreeArgTypes, constructorFromUse, constructorFromUseWithoutTypeArgInference, containsCapturedTypes, containsSameByClass, createAnnotatedTypeFormatter, createAnnotationClassLoader, createAnnotationFormatter, createQualifierUpperBounds, createSupportedTypeQualifiers, createTypeArgumentInference, createTypeHierarchy, createTypeInformationPresenter, createTypeVariableSubstitutor, declarationFromElement, doesAnnotatedForApplyToThisChecker, fromElement, fromElement, fromElement, getAnnotatedNullType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedTypeFormatter, getAnnotatedTypeFromTypeTree, getAnnotationByClass, getAnnotationFormatter, getAnnotationMirror, getAnnotationWithMetaAnnotation, getBoxedType, getBundledTypeQualifiers, getCacheSize, getChecker, getCheckerNames, getContractExpressions, getContractListValues, getDeclAnnotation, getDeclAnnotationNoAliases, getDeclAnnotations, getDeclAnnotationWithMetaAnnotation, getDefaultTypeDeclarationBounds, getDummyAssignedTo, getElementUtils, getEnclosingClassOrMethod, getEnclosingElementForArtificialTree, getEnclosingSubType, getEnclosingType, getEnumConstructorQualifiers, getExpressionAndOffset, getFieldInvariantAnnotationTree, getFieldInvariantDeclarationAnnotations, getFieldInvariants, getFnInterfaceFromTree, getFunctionTypeFromTree, getFunctionTypeFromTree, getImplicitReceiverType, getIterableElementType, getIterableElementType, getMethodReturnType, getNarrowedAnnotations, getNarrowedPrimitive, getPath, getProcessingEnv, getQualifierHierarchy, getQualifierParameterHierarchies, getQualifierParameterHierarchies, getQualifierUpperBounds, getReceiverType, getResultingTypeOfConstructorMemberReference, getSelfType, getStringType, getSupportedTypeQualifierNames, getSupportedTypeQualifiers, getTreeUtils, getTypeArgumentInference, getTypeDeclarationBounds, getTypeHierarchy, getTypeOfExtendsImplements, getTypeVarSubstitutor, getUnboxedType, getVisitorTreePath, getWholeProgramInference, getWidenedAnnotations, getWidenedType, getWidenedType, hasExplicitNoQualifierParameterInHierarchy, hasExplicitQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, initializeAtm, initializeReflectionResolution, isDeterministic, isFromByteCode, isFromStubFile, isImmutable, isSideEffectFree, isSupportedQualifier, isSupportedQualifier, isSupportedQualifier, isTop, isWithinConstructor, logGat, makeConditionConsistentWithOtherMethod, mergeAnnotationFileAnnosIntoType, methodFromUse, methodFromUse, methodFromUse, methodFromUseWithoutTypeArgInference, methodFromUseWithoutTypeArgInference, negateConstant, order, parseAnnotationFiles, postProcessClassTree, replaceAnnotations, replaceAnnotations, setEnclosingElementForArtificialTree, setVisitorTreePath, shouldWarnIfStubRedundantWithBytecode, toAnnotatedType, toString, type, wpiAdjustForUpdateField, wpiAdjustForUpdateNonField, wpiPrepareMethodForWriting, wpiPrepareMethodForWriting, wpiShouldInferTypesForReceivers
-
Field Details
-
accumulationChecker
The typechecker associated with this factory. -
top
The canonical top annotation for this accumulation checker: an instance of the accumulator annotation with no arguments. -
bottom
The canonical bottom annotation for this accumulation checker.
-
-
Constructor Details
-
AccumulationAnnotatedTypeFactory
protected AccumulationAnnotatedTypeFactory(BaseTypeChecker checker, Class<? extends Annotation> accumulator, Class<? extends Annotation> bottom, @Nullable Class<? extends Annotation> predicate) Create an annotated type factory for an accumulation checker.- Parameters:
checker
- the checkeraccumulator
- the accumulator type in the hierarchy. Must be an annotation with a single argument named "value" whose type is a String array.bottom
- the bottom type in the hierarchy, which must be a subtype ofaccumulator
. The bottom type should be an annotation with no arguments.predicate
- the predicate annotation. Either null (if predicates are not supported), or an annotation with a single element named "value" whose type is a String.
-
AccumulationAnnotatedTypeFactory
protected AccumulationAnnotatedTypeFactory(BaseTypeChecker checker, Class<? extends Annotation> accumulator, Class<? extends Annotation> bottom) Create an annotated type factory for an accumulation checker.- Parameters:
checker
- the checkeraccumulator
- the accumulator type in the hierarchy. Must be an annotation with a single argument named "value" whose type is a String array.bottom
- the bottom type in the hierarchy, which must be a subtype ofaccumulator
. The bottom type should be an annotation with no arguments.
-
-
Method Details
-
createAccumulatorAnnotation
Creates a new instance of the accumulator annotation that contains the elements ofvalues
.- Parameters:
values
- the arguments to the annotation. The values can contain duplicates and can be in any order.- Returns:
- an annotation mirror representing the accumulator annotation with
values
's arguments; this is top ifvalues
is empty
-
createAccumulatorAnnotation
Creates a new instance of the accumulator annotation that contains exactly one value.- Parameters:
value
- the argument to the annotation- Returns:
- an annotation mirror representing the accumulator annotation with
value
as its argument
-
returnsThis
Returns true if the return type of the given method invocation tree has an @This annotation from the Returns Receiver Checker.- Parameters:
tree
- a method invocation tree- Returns:
- true if the method being invoked returns its receiver
-
isAccumulatorAnnotation
Is the given annotation an accumulator annotation? Returns false if the argument isbottom
.- Parameters:
anm
- an annotation mirror- Returns:
- true if the annotation mirror is an instance of this factory's accumulator annotation
-
createTreeAnnotator
Description copied from class:GenericAnnotatedTypeFactory
Returns aTreeAnnotator
that adds annotations to a type based on the contents of a tree.The default tree annotator is a
ListTreeAnnotator
of the following:PropagationTreeAnnotator
: Propagates annotations from subtreesLiteralTreeAnnotator
: Adds annotations based onQualifierForLiterals
meta-annotationsDependentTypesTreeAnnotator
: 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 classGenericAnnotatedTypeFactory<AccumulationValue,
AccumulationStore, AccumulationTransfer, AccumulationAnalysis> - Returns:
- a tree annotator
-
createQualifierHierarchy
Description copied from class:AnnotatedTypeFactory
Returns theQualifierHierarchy
to be used by this checker.The implementation builds the type qualifier hierarchy for the
AnnotatedTypeFactory.getSupportedTypeQualifiers()
using the meta-annotations found in them. The current implementation returns an instance ofNoElementQualifierHierarchy
.Subclasses must override this method if their qualifiers have elements; the method must return an implementation of
QualifierHierarchy
, such asElementQualifierHierarchy
.- Overrides:
createQualifierHierarchy
in classAnnotatedTypeFactory
- Returns:
- a QualifierHierarchy for this type system
-
getAccumulatedValues
Returns all the values that anno has accumulated.- Parameters:
anno
- an accumulator annotation; must not be bottom- Returns:
- the list of values the annotation has accumulated; it is a new list, so it is safe for clients to side-effect
-
getAccumulatedValues
Returns the accumulated values on the given (expression, usually) tree. This differs from callingAnnotatedTypeFactory.getAnnotatedType(Tree)
, because this version takes into account accumulated methods that are stored on the value. This is useful when dealing with accumulated facts on variables whose types are type variables (because type variable types cannot be refined directly, due to the quirks of subtyping between type variables and its interactions with the qualified type system).The returned collection may be either a list or a set.
- Parameters:
tree
- a tree- Returns:
- the accumulated values for the given tree, including those stored on the value
-
isPredicateSubtype
Extension point for subtyping behavior between predicates. This implementation conservatively returns true only if the predicates are equal, or if the prospective supertype (q) is equivalent to top (that is, the empty string).- Parameters:
p
- a predicateq
- another predicate- Returns:
- true if p is a subtype of q
-
evaluatePredicate
Evaluates whether the accumulator annotationsubAnno
makes the predicatepred
true.- Parameters:
subAnno
- an accumulator annotationpred
- a predicate- Returns:
- whether the accumulator annotation satisfies the predicate
-
evaluatePredicate
Evaluates whether treating the variables intrueVariables
astrue
literals (and all other names asfalse
literals) makes the predicatepred
evaluate to true.- Parameters:
trueVariables
- a list of names that should be replaced withtrue
pred
- a predicate- Returns:
- whether the true variables satisfy the predicate
-
createPredicateAnnotation
Creates a new predicate annotation from the given string.- Parameters:
p
- a valid predicate- Returns:
- an annotation representing that predicate
-
convertToPredicate
Converts the given annotation mirror to a predicate.- Parameters:
anno
- an annotation- Returns:
- the predicate, as a String, that is equivalent to that annotation. May return the empty string.
-
isPredicate
Returns true if anno is a predicate annotation.- Parameters:
anno
- an annotation- Returns:
- true if anno is a predicate annotation
-