Class UpperBoundAnnotatedTypeFactory
- java.lang.Object
-
- org.checkerframework.framework.type.AnnotatedTypeFactory
-
- org.checkerframework.framework.type.GenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis>
-
- org.checkerframework.common.basetype.BaseAnnotatedTypeFactory
-
- org.checkerframework.checker.index.BaseAnnotatedTypeFactoryForIndexChecker
-
- org.checkerframework.checker.index.upperbound.UpperBoundAnnotatedTypeFactory
-
- All Implemented Interfaces:
AnnotationProvider
public class UpperBoundAnnotatedTypeFactory extends BaseAnnotatedTypeFactoryForIndexChecker
Implements the introduction rules for the Upper Bound Checker.Rules implemented by this class:
- 1. Math.min has unusual semantics that combines annotations for the UBC.
- 2. The return type of Random.nextInt depends on the argument, but is not equal to it, so a polymorphic qualifier is insufficient.
- 3. Unary negation on a NegativeIndexFor (from the SearchIndex Checker) results in a LTLengthOf for the same arrays.
- 4. Right shifting by a constant between 0 and 30 preserves the type of the left side expression.
- 5. If either argument to a bitwise and expression is non-negative, the and expression retains that argument's upperbound type. If both are non-negative, the result of the expression is the GLB of the two.
- 6. if numerator ≥ 0, then numerator % divisor ≤ numerator
- 7. if divisor ≥ 0, then numerator % divisor < divisor
- 8. If the numerator is an array length access of an array with non-zero length, and the divisor is greater than one, glb the result with an LTL of the array.
- 9. if numeratorTree is a + b and divisor greater than 1, and a and b are less than the length of some sequence, then (a + b) / divisor is less than the length of that sequence.
- 10. Special handling for Math.random: Math.random() * array.length is LTL array.
-
-
Nested Class Summary
Nested Classes Modifier and Type Class Description protected class
UpperBoundAnnotatedTypeFactory.UpperBoundQualifierHierarchy
The qualifier hierarchy for the upperbound type system.protected class
UpperBoundAnnotatedTypeFactory.UpperBoundTreeAnnotator
-
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 javax.lang.model.element.AnnotationMirror
BOTTOM
The @UpperBoundBottom
annotation.javax.lang.model.element.ExecutableElement
ltLengthOfOffsetElement
The LTLengthOf.offset element/field.javax.lang.model.element.ExecutableElement
ltLengthOfValueElement
The LTLengthOf.value element/field.javax.lang.model.element.ExecutableElement
negativeIndexForValueElement
The NegativeIndexFor.value element/field.javax.lang.model.element.AnnotationMirror
NEGATIVEONE
The @UpperBoundLiteral
(-1) annotation.javax.lang.model.element.AnnotationMirror
ONE
The @UpperBoundLiteral
(1) annotation.javax.lang.model.element.AnnotationMirror
POLY
The @PolyUpperBound
annotation.javax.lang.model.element.ExecutableElement
sameLenValueElement
The SameLen.value element/field.javax.lang.model.element.AnnotationMirror
UNKNOWN
The @UpperBoundUnknown
annotation.javax.lang.model.element.AnnotationMirror
ZERO
The @UpperBoundLiteral
(0) annotation.-
Fields inherited from class org.checkerframework.checker.index.BaseAnnotatedTypeFactoryForIndexChecker
hasSubsequenceFromElement, hasSubsequenceSubsequenceElement, hasSubsequenceToElement
-
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 Constructor Description UpperBoundAnnotatedTypeFactory(BaseTypeChecker checker)
Create a new UpperBoundAnnotatedTypeFactory.
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description void
addComputedTypeAnnotations(com.sun.source.tree.Tree tree, AnnotatedTypeMirror type, boolean iUseFlow)
void
addComputedTypeAnnotations(javax.lang.model.element.Element element, AnnotatedTypeMirror type)
To add annotations to the type of method or constructor parameters, add aTypeAnnotator
usingGenericAnnotatedTypeFactory.createTypeAnnotator()
and see the comment inTypeAnnotator.visitExecutable(org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType, Void)
.javax.lang.model.element.AnnotationMirror
convertUBQualifierToAnnotation(UBQualifier qualifier)
Convert the internal representation to an annotation.protected DependentTypesHelper
createDependentTypesHelper()
Creates aDependentTypesHelper
and returns it.javax.lang.model.element.AnnotationMirror
createLiteral(int i)
Creates a @UpperBoundLiteral
annotation.protected QualifierHierarchy
createQualifierHierarchy()
Returns theQualifierHierarchy
to be used by this checker.protected java.util.Set<java.lang.Class<? extends java.lang.annotation.Annotation>>
createSupportedTypeQualifiers()
Returns a mutable set of annotation classes that are supported by a checker.TreeAnnotator
createTreeAnnotator()
Returns aTreeAnnotator
that adds annotations to a type based on the contents of a tree.protected TypeAnnotator
createTypeAnnotator()
Returns aDefaultForTypeAnnotator
that adds annotations to a type based on the content of the type itself.LessThanAnnotatedTypeFactory
getLessThanAnnotatedTypeFactory()
Returns the LessThan Checker's annotated type factory.boolean
hasLowerBoundTypeByClass(Node node, java.lang.Class<? extends java.lang.annotation.Annotation> classOfType)
Returns true iff the given node has the passed Lower Bound qualifier according to the LBC.boolean
isMathMin(com.sun.source.tree.Tree methodTree)
boolean
isRandomNextInt(com.sun.source.tree.Tree methodTree)
Returns true if the tree is forRandom.nextInt(int)
.@Nullable javax.lang.model.element.AnnotationMirror
sameLenAnnotationFromTree(com.sun.source.tree.Tree tree)
Queries the SameLen Checker to return the type that the SameLen Checker associates with the given tree.-
Methods inherited from class org.checkerframework.checker.index.BaseAnnotatedTypeFactoryForIndexChecker
hasSubsequenceFromValue, hasSubsequenceSubsequenceValue, hasSubsequenceToValue
-
Methods inherited from class org.checkerframework.common.basetype.BaseAnnotatedTypeFactory
createFlowAnalysis
-
Methods inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory
addAnnotationsFromDefaultForType, addCheckedCodeDefaults, addCheckedStandardDefaults, addComputedTypeAnnotations, addDefaultAnnotations, addSharedCFGForTree, addUncheckedStandardDefaults, analyze, annotationsForIrrelevantJavaType, applyInferredAnnotations, applyQualifierParameterDefaults, applyQualifierParameterDefaults, checkAndPerformFlowAnalysis, checkForDefaultQualifierInHierarchy, constructorFromUse, constructorFromUsePreSubstitution, createAndInitQualifierDefaults, createCFGVisualizer, createContractsFromMethod, createDefaultForTypeAnnotator, createDefaultForUseTypeAnnotator, createFlowTransferFunction, createQualifierDefaults, createQualifierPolymorphism, createRequiresOrEnsuresQualifier, 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, 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
-
UNKNOWN
public final javax.lang.model.element.AnnotationMirror UNKNOWN
The @UpperBoundUnknown
annotation.
-
BOTTOM
public final javax.lang.model.element.AnnotationMirror BOTTOM
The @UpperBoundBottom
annotation.
-
POLY
public final javax.lang.model.element.AnnotationMirror POLY
The @PolyUpperBound
annotation.
-
NEGATIVEONE
public final javax.lang.model.element.AnnotationMirror NEGATIVEONE
The @UpperBoundLiteral
(-1) annotation.
-
ZERO
public final javax.lang.model.element.AnnotationMirror ZERO
The @UpperBoundLiteral
(0) annotation.
-
ONE
public final javax.lang.model.element.AnnotationMirror ONE
The @UpperBoundLiteral
(1) annotation.
-
negativeIndexForValueElement
public final javax.lang.model.element.ExecutableElement negativeIndexForValueElement
The NegativeIndexFor.value element/field.
-
sameLenValueElement
public final javax.lang.model.element.ExecutableElement sameLenValueElement
The SameLen.value element/field.
-
ltLengthOfValueElement
public final javax.lang.model.element.ExecutableElement ltLengthOfValueElement
The LTLengthOf.value element/field.
-
ltLengthOfOffsetElement
public final javax.lang.model.element.ExecutableElement ltLengthOfOffsetElement
The LTLengthOf.offset element/field.
-
-
Constructor Detail
-
UpperBoundAnnotatedTypeFactory
public UpperBoundAnnotatedTypeFactory(BaseTypeChecker checker)
Create a new UpperBoundAnnotatedTypeFactory.
-
-
Method Detail
-
createSupportedTypeQualifiers
protected java.util.Set<java.lang.Class<? extends java.lang.annotation.Annotation>> createSupportedTypeQualifiers()
Description copied from class:AnnotatedTypeFactory
Returns a mutable set of annotation classes that are supported by a checker.Subclasses may override this method to return a mutable set of their supported type qualifiers through one of the 5 approaches shown below.
Subclasses should not call this method; they should call
AnnotatedTypeFactory.getSupportedTypeQualifiers()
instead.By default, a checker supports all annotations located in a subdirectory called qual that's located in the same directory as the checker. Note that only annotations defined with the
@Target({ElementType.TYPE_USE})
meta-annotation (and optionally with the additional value ofElementType.TYPE_PARAMETER
, but no otherElementType
values) are automatically considered as supported annotations.To support a different set of annotations than those in the qual subdirectory, or that have other
ElementType
values, see examples below.In total, there are 5 ways to indicate annotations that are supported by a checker:
- Only support annotations located in a checker's qual directory:
This is the default behavior. Simply place those annotations within the qual directory.
- Support annotations located in a checker's qual directory and a list of
other annotations:
Place those annotations within the qual directory, and override
AnnotatedTypeFactory.createSupportedTypeQualifiers()
by callingAnnotatedTypeFactory.getBundledTypeQualifiers(Class...)
with a varargs parameter list of the other annotations. Code example:@Override protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() { return getBundledTypeQualifiers(Regex.class, PartialRegex.class, RegexBottom.class, UnknownRegex.class); }
- Supporting only annotations that are explicitly listed: Override
AnnotatedTypeFactory.createSupportedTypeQualifiers()
and return a mutable set of the supported annotations. Code example:@Override protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() { return new HashSet<Class<? extends Annotation>>( Arrays.asList(A.class, B.class)); }
AnnotatedTypeFactory.createSupportedTypeQualifiers()
must be a fresh, mutable set. The methodsAnnotatedTypeFactory.getBundledTypeQualifiers(Class...)
must return a fresh, mutable set
- Overrides:
createSupportedTypeQualifiers
in classAnnotatedTypeFactory
- Returns:
- the type qualifiers supported this processor, or an empty set if none
- Only support annotations located in a checker's qual directory:
-
getLessThanAnnotatedTypeFactory
public LessThanAnnotatedTypeFactory getLessThanAnnotatedTypeFactory()
Returns the LessThan Checker's annotated type factory.
-
addComputedTypeAnnotations
public void addComputedTypeAnnotations(javax.lang.model.element.Element element, AnnotatedTypeMirror type)
Description copied from class:GenericAnnotatedTypeFactory
To add annotations to the type of method or constructor parameters, add aTypeAnnotator
usingGenericAnnotatedTypeFactory.createTypeAnnotator()
and see the comment inTypeAnnotator.visitExecutable(org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType, Void)
.- Overrides:
addComputedTypeAnnotations
in classGenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis>
- Parameters:
element
- an elementtype
- the type obtained fromelt
-
addComputedTypeAnnotations
public void addComputedTypeAnnotations(com.sun.source.tree.Tree tree, AnnotatedTypeMirror type, boolean iUseFlow)
Description copied from class:GenericAnnotatedTypeFactory
LikeGenericAnnotatedTypeFactory.addComputedTypeAnnotations(Tree, AnnotatedTypeMirror)
. Overriding implementations typically simply pass the boolean to calls to super.- Overrides:
addComputedTypeAnnotations
in classGenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis>
- Parameters:
tree
- an AST nodetype
- the type obtained from treeiUseFlow
- whether to use information from dataflow analysis
-
createTypeAnnotator
protected TypeAnnotator createTypeAnnotator()
Description copied from class:GenericAnnotatedTypeFactory
Returns aDefaultForTypeAnnotator
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:IrrelevantTypeAnnotator
: Adds top to types not listed in the@
RelevantJavaTypes
annotation on the checker.PropagationTypeAnnotator
: Propagates annotation onto wildcards.
- Overrides:
createTypeAnnotator
in classGenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis>
- Returns:
- a type annotator
-
createDependentTypesHelper
protected DependentTypesHelper createDependentTypesHelper()
Description copied from class:GenericAnnotatedTypeFactory
Creates aDependentTypesHelper
and returns it. UseGenericAnnotatedTypeFactory.getDependentTypesHelper()
to access the value.- Overrides:
createDependentTypesHelper
in classGenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis>
- Returns:
- a new
DependentTypesHelper
-
sameLenAnnotationFromTree
public @Nullable javax.lang.model.element.AnnotationMirror sameLenAnnotationFromTree(com.sun.source.tree.Tree tree)
Queries the SameLen Checker to return the type that the SameLen Checker associates with the given tree.
-
isMathMin
public boolean isMathMin(com.sun.source.tree.Tree methodTree)
-
isRandomNextInt
public boolean isRandomNextInt(com.sun.source.tree.Tree methodTree)
Returns true if the tree is forRandom.nextInt(int)
.- Parameters:
methodTree
- a tree to check- Returns:
- true iff the tree is for
Random.nextInt(int)
-
hasLowerBoundTypeByClass
public boolean hasLowerBoundTypeByClass(Node node, java.lang.Class<? extends java.lang.annotation.Annotation> classOfType)
Returns true iff the given node has the passed Lower Bound qualifier according to the LBC. The last argument should be Positive.class, NonNegative.class, or GTENegativeOne.class.- Parameters:
node
- the given nodeclassOfType
- one of Positive.class, NonNegative.class, or GTENegativeOne.class- Returns:
- true iff the given node has the passed Lower Bound qualifier according to the LBC
-
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
-
createTreeAnnotator
public 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<CFValue,CFStore,CFTransfer,CFAnalysis>
- Returns:
- a tree annotator
-
createLiteral
public javax.lang.model.element.AnnotationMirror createLiteral(int i)
Creates a @UpperBoundLiteral
annotation.- Parameters:
i
- the integer- Returns:
- a @
UpperBoundLiteral
annotation
-
convertUBQualifierToAnnotation
public javax.lang.model.element.AnnotationMirror convertUBQualifierToAnnotation(UBQualifier qualifier)
Convert the internal representation to an annotation.- Parameters:
qualifier
- a UBQualifier- Returns:
- an annotation corresponding to the given qualifier
-
-