Class AccumulationAnnotatedTypeFactory
- java.lang.Object
-
- org.checkerframework.framework.type.AnnotatedTypeFactory
-
- org.checkerframework.framework.type.GenericAnnotatedTypeFactory<AccumulationValue,AccumulationStore,AccumulationTransfer,AccumulationAnalysis>
-
- org.checkerframework.common.accumulation.AccumulationAnnotatedTypeFactory
-
- All Implemented Interfaces:
AnnotationProvider
- Direct Known Subclasses:
CalledMethodsAnnotatedTypeFactory
,InitializedFieldsAnnotatedTypeFactory
public abstract class AccumulationAnnotatedTypeFactory extends GenericAnnotatedTypeFactory<AccumulationValue,AccumulationStore,AccumulationTransfer,AccumulationAnalysis>
An annotated type factory for an accumulation checker.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 andGenericAnnotatedTypeFactory.postInit()
.
-
-
Nested Class Summary
Nested Classes Modifier and Type Class Description protected class
AccumulationAnnotatedTypeFactory.AccumulationQualifierHierarchy
All accumulation analyses share a similar type hierarchy.protected class
AccumulationAnnotatedTypeFactory.AccumulationTreeAnnotator
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.ParameterizedExecutableType
-
-
Field Summary
Fields Modifier and Type Field Description AccumulationChecker
accumulationChecker
The typechecker associated with this factory.javax.lang.model.element.AnnotationMirror
bottom
The canonical bottom annotation for this accumulation checker.javax.lang.model.element.AnnotationMirror
top
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, poly, regularExitStores, relevantJavaTypes, returnStatementStores, scannedClasses, shouldClearSubcheckerSharedCFGs, sideEffectsUnrefineAliases, subcheckerSharedCFG, transfer, treeAnnotator, typeAnnotator
-
Fields inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory
ajavaTypes, annotatedForValueElement, checker, currentFileAjavaTypes, elements, ensuresQualifierExpressionElement, ensuresQualifierIfExpressionElement, ensuresQualifierIfListTM, ensuresQualifierIfListValueElement, ensuresQualifierIfResultElement, ensuresQualifierIfTM, ensuresQualifierListTM, ensuresQualifierListValueElement, ensuresQualifierTM, fieldInvariantFieldElement, fieldInvariantQualifierElement, fromExpressionTreeCache, fromMemberTreeCache, fromTypeTreeCache, hasQualifierParameterValueElement, ignoreUninferredTypeArguments, loader, methodValClassNameElement, methodValMethodNameElement, methodValParamsElement, noQualifierParameterValueElement, objectGetClass, processingEnv, qualHierarchy, qualifierUpperBounds, reflectionResolver, requiresQualifierExpressionElement, requiresQualifierListTM, requiresQualifierListValueElement, requiresQualifierTM, root, shouldCache, stubTypes, trees, typeArgumentInference, typeFormatter, typeHierarchy, types, typeVarSubstitutor, uid, viewpointAdapter
-
-
Constructor Summary
Constructors Modifier Constructor Description protected
AccumulationAnnotatedTypeFactory(BaseTypeChecker checker, java.lang.Class<? extends java.lang.annotation.Annotation> accumulator, java.lang.Class<? extends java.lang.annotation.Annotation> bottom)
Create an annotated type factory for an accumulation checker.protected
AccumulationAnnotatedTypeFactory(BaseTypeChecker checker, java.lang.Class<? extends java.lang.annotation.Annotation> accumulator, java.lang.Class<? extends java.lang.annotation.Annotation> bottom, @Nullable java.lang.Class<? extends java.lang.annotation.Annotation> predicate)
Create an annotated type factory for an accumulation checker.
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description protected java.lang.String
convertToPredicate(javax.lang.model.element.AnnotationMirror anno)
Converts the given annotation mirror to a predicate.javax.lang.model.element.AnnotationMirror
createAccumulatorAnnotation(java.lang.String value)
Creates a new instance of the accumulator annotation that contains exactly one value.javax.lang.model.element.AnnotationMirror
createAccumulatorAnnotation(java.util.List<java.lang.String> values)
Creates a new instance of the accumulator annotation that contains the elements ofvalues
.protected javax.lang.model.element.AnnotationMirror
createPredicateAnnotation(java.lang.String p)
Creates a new predicate annotation from the given string.protected QualifierHierarchy
createQualifierHierarchy()
Returns theQualifierHierarchy
to be used by this checker.protected TreeAnnotator
createTreeAnnotator()
Returns aTreeAnnotator
that adds annotations to a type based on the contents of a tree.protected boolean
evaluatePredicate(java.util.List<java.lang.String> trueVariables, java.lang.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(javax.lang.model.element.AnnotationMirror subAnno, java.lang.String pred)
Evaluates whether the accumulator annotationsubAnno
makes the predicatepred
true.java.util.Collection<java.lang.String>
getAccumulatedValues(com.sun.source.tree.Tree tree)
Returns the accumulated values on the given (expression, usually) tree.java.util.List<java.lang.String>
getAccumulatedValues(javax.lang.model.element.AnnotationMirror anno)
Returns all the values that anno has accumulated.boolean
isAccumulatorAnnotation(javax.lang.model.element.AnnotationMirror anm)
Is the given annotation an accumulator annotation? Returns false if the argument isbottom
.protected boolean
isPredicate(javax.lang.model.element.AnnotationMirror anno)
Returns true if anno is a predicate annotation.protected boolean
isPredicateSubtype(java.lang.String p, java.lang.String q)
Extension point for subtyping behavior between predicates.boolean
returnsThis(com.sun.source.tree.MethodInvocationTree tree)
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, addDefaultAnnotations, addSharedCFGForTree, addUncheckedStandardDefaults, analyze, annotationsForIrrelevantJavaType, applyInferredAnnotations, applyQualifierParameterDefaults, applyQualifierParameterDefaults, checkAndPerformFlowAnalysis, checkForDefaultQualifierInHierarchy, constructorFromUse, constructorFromUsePreSubstitution, createAndInitQualifierDefaults, createCFGVisualizer, createContractsFromMethod, createDefaultForTypeAnnotator, createDefaultForUseTypeAnnotator, createDependentTypesHelper, createFlowAnalysis, createFlowTransferFunction, createQualifierDefaults, createQualifierPolymorphism, createRequiresOrEnsuresQualifier, createTypeAnnotator, getAnnotatedTypeBefore, getAnnotatedTypeLhs, getAnnotatedTypeLhsNoTypeVarDefault, getAnnotatedTypeRhsUnaryAssign, getAnnotatedTypeVarargsArray, getAnnotationFromJavaExpression, getAnnotationFromJavaExpressionString, getAnnotationMirrorFromJavaExpressionString, getAnnotationsFromJavaExpression, getCFGVisualizer, getContractExpressions, getContractsFromMethod, getDefaultAnnotations, getDefaultForTypeAnnotator, getDefaultValueAnnotatedType, getDependentTypesHelper, getEmptyStore, getEnsuresQualifierIfResult, getExceptionalExitStore, getExplicitNewClassAnnos, getExplicitNewClassClassTypeArgs, getExpressionAndOffsetFromJavaExpressionString, getFinalLocalValues, getFirstNodeOfKindForTree, getInferredValueFor, getMethodReturnType, getNodesForTree, getQualifierPolymorphism, getRegularExitStore, getResultingTypeOfConstructorMemberReference, getReturnStatementStores, getSharedCFGForTree, getShouldDefaultTypeVarLocals, getSortedQualifierNames, getStoreAfter, getStoreAfter, getStoreAfter, getStoreBefore, getStoreBefore, getStoreBefore, getSupportedMonotonicTypeQualifiers, getTypeFactoryOfSubchecker, getTypeFactoryOfSubcheckerOrNull, handleCFGViz, irrelevantExtraMessage, isComputingAnnotatedTypeMirrorOfLhs, isNotFullyInitializedReceiver, isRelevant, isRelevant, isRelevantImpl, methodFromUse, methodFromUsePreSubstitution, parseJavaExpressionString, performFlowAnalysis, postAnalyze, postAsMemberOf, postDirectSuperTypes, postInit, preProcessClassTree, setRoot, typeVariablesFromUse
-
Methods inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory
adaptGetClassReturnTypeToReceiver, addAliasedDeclAnnotation, addAliasedDeclAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAnnotationFromFieldInvariant, addInheritedAnnotation, applyCaptureConversion, applyCaptureConversion, applyUnboxing, areSameByClass, binaryTreeArgTypes, binaryTreeArgTypes, binaryTreeArgTypes, canonicalAnnotation, compoundAssignmentTreeArgTypes, containsSameByClass, containsUninferredTypeArguments, createAnnotatedTypeFormatter, createAnnotationClassLoader, createAnnotationFormatter, createQualifierUpperBounds, createSupportedTypeQualifiers, createTypeArgumentInference, createTypeHierarchy, createTypeVariableSubstitutor, createViewpointAdapter, declarationFromElement, doesAnnotatedForApplyToThisChecker, fromElement, fromElement, fromElement, fromNewClass, getAnnotatedNullType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedTypeFormatter, getAnnotatedTypeFromTypeTree, getAnnotationByClass, getAnnotationFormatter, getAnnotationMirror, getAnnotationOrTypeDeclarationBound, getAnnotationWithMetaAnnotation, getBoxedType, getBundledTypeQualifiers, getCacheSize, getChecker, getCheckerNames, getContractExpressions, getContractListValues, getCurrentClassTree, getCurrentMethodReceiver, getDeclAnnotation, getDeclAnnotationNoAliases, getDeclAnnotations, getDeclAnnotationWithMetaAnnotation, getDefaultTypeDeclarationBounds, getDummyAssignedTo, getElementUtils, getEnclosingClassOrMethod, getEnclosingSubType, getEnclosingType, getEnumConstructorQualifiers, getExpressionAndOffset, getFieldInvariantAnnotationTree, getFieldInvariantDeclarationAnnotations, getFieldInvariants, getFnInterfaceFromTree, getFunctionTypeFromTree, getFunctionTypeFromTree, getImplicitReceiverType, getIterableElementType, getIterableElementType, getMethodReturnType, getNarrowedAnnotations, getNarrowedPrimitive, getPath, getProcessingEnv, getQualifierHierarchy, getQualifierParameterHierarchies, getQualifierParameterHierarchies, getQualifierUpperBounds, getReceiverType, getSelfType, getStringType, getSupportedTypeQualifierNames, getSupportedTypeQualifiers, getTreeUtils, getTypeArgumentInference, getTypeDeclarationBounds, getTypeHierarchy, getTypeOfExtendsImplements, getTypeVarSubstitutor, getUnboxedType, getUninferredWildcardType, getVisitorTreePath, getWidenedAnnotations, getWidenedType, getWidenedType, hasExplicitNoQualifierParameterInHierarchy, hasExplicitQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, initializeReflectionResolution, isFromByteCode, isFromStubFile, isImmutable, isSideEffectFree, isSupportedQualifier, isSupportedQualifier, isSupportedQualifier, isWithinConstructor, mergeAnnotationFileAnnosIntoType, methodFromUse, negateConstant, order, parseAnnotationFiles, postProcessClassTree, replaceAnnotations, replaceAnnotations, setPathForArtificialTree, setVisitorTreePath, shouldWarnIfStubRedundantWithBytecode, toAnnotatedType, toString, type
-
-
-
-
Field Detail
-
accumulationChecker
public final AccumulationChecker accumulationChecker
The typechecker associated with this factory.
-
top
public final javax.lang.model.element.AnnotationMirror top
The canonical top annotation for this accumulation checker: an instance of the accumulator annotation with no arguments.
-
bottom
public final javax.lang.model.element.AnnotationMirror bottom
The canonical bottom annotation for this accumulation checker.
-
-
Constructor Detail
-
AccumulationAnnotatedTypeFactory
protected AccumulationAnnotatedTypeFactory(BaseTypeChecker checker, java.lang.Class<? extends java.lang.annotation.Annotation> accumulator, java.lang.Class<? extends java.lang.annotation.Annotation> bottom, @Nullable java.lang.Class<? extends java.lang.annotation.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, java.lang.Class<? extends java.lang.annotation.Annotation> accumulator, java.lang.Class<? extends java.lang.annotation.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 Detail
-
createAccumulatorAnnotation
public javax.lang.model.element.AnnotationMirror createAccumulatorAnnotation(java.util.List<java.lang.String> values)
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
public javax.lang.model.element.AnnotationMirror createAccumulatorAnnotation(java.lang.String value)
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
public boolean returnsThis(com.sun.source.tree.MethodInvocationTree tree)
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
public boolean isAccumulatorAnnotation(javax.lang.model.element.AnnotationMirror anm)
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
protected TreeAnnotator 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
protected QualifierHierarchy 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
public java.util.List<java.lang.String> getAccumulatedValues(javax.lang.model.element.AnnotationMirror anno)
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
public java.util.Collection<java.lang.String> getAccumulatedValues(com.sun.source.tree.Tree tree)
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
protected boolean isPredicateSubtype(java.lang.String p, java.lang.String q)
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
protected boolean evaluatePredicate(javax.lang.model.element.AnnotationMirror subAnno, java.lang.String pred)
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
protected boolean evaluatePredicate(java.util.List<java.lang.String> trueVariables, java.lang.String pred)
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
protected javax.lang.model.element.AnnotationMirror createPredicateAnnotation(java.lang.String p)
Creates a new predicate annotation from the given string.- Parameters:
p
- a valid predicate- Returns:
- an annotation representing that predicate
-
convertToPredicate
protected java.lang.String convertToPredicate(javax.lang.model.element.AnnotationMirror anno)
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
protected boolean isPredicate(javax.lang.model.element.AnnotationMirror anno)
Returns true if anno is a predicate annotation.- Parameters:
anno
- an annotation- Returns:
- true if anno is a predicate annotation
-
-