Class UpperBoundAnnotatedTypeFactory
- All Implemented Interfaces:
AnnotationProvider
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 ClassesModifier and TypeClassDescriptionprotected final classThe qualifier hierarchy for the upperbound type system.protected classNested classes/interfaces inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory
GenericAnnotatedTypeFactory.ScanStateNested classes/interfaces inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory
AnnotatedTypeFactory.CapturedTypeVarSubstitutor, AnnotatedTypeFactory.ParameterizedExecutableType -
Field Summary
FieldsModifier and TypeFieldDescriptionfinal AnnotationMirrorThe @UpperBoundBottomannotation.final ExecutableElementThe LTLengthOf.offset element/field.final ExecutableElementThe LTLengthOf.value element/field.final ExecutableElementThe NegativeIndexFor.value element/field.final AnnotationMirrorThe @UpperBoundLiteral(-1) annotation.final AnnotationMirrorThe @UpperBoundLiteral(1) annotation.final AnnotationMirrorThe @PolyUpperBoundannotation.final ExecutableElementThe SameLen.value element/field.final AnnotationMirrorThe @UpperBoundUnknownannotation.final AnnotationMirrorThe @UpperBoundLiteral(0) annotation.Fields inherited from class org.checkerframework.checker.index.BaseAnnotatedTypeFactoryForIndexChecker
hasSubsequenceFromElement, hasSubsequenceSubsequenceElement, hasSubsequenceToElementFields 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, typeAnnotatorFields 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
ConstructorsConstructorDescriptionCreate a new UpperBoundAnnotatedTypeFactory. -
Method Summary
Modifier and TypeMethodDescriptionvoidaddComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, boolean iUseFlow) voidaddComputedTypeAnnotations(Element element, AnnotatedTypeMirror type) To add annotations to the type of method or constructor parameters, add aTypeAnnotatorusingGenericAnnotatedTypeFactory.createTypeAnnotator()and see the comment inTypeAnnotator.visitExecutable(org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType, Void).convertUBQualifierToAnnotation(UBQualifier qualifier) Convert the internal representation to an annotation.protected DependentTypesHelperCreates aDependentTypesHelperand returns it.createLiteral(int i) Creates a @UpperBoundLiteralannotation.protected QualifierHierarchyReturns theQualifierHierarchyto be used by this checker.protected Set<Class<? extends Annotation>> Returns a mutable set of annotation classes that are supported by a checker.Returns aTreeAnnotatorthat adds annotations to a type based on the contents of a tree.protected TypeAnnotatorReturns aDefaultForTypeAnnotatorthat adds annotations to a type based on the content of the type itself.Returns the LessThan Checker's annotated type factory.booleanhasLowerBoundTypeByClass(Node node, Class<? extends Annotation> classOfType) Returns true iff the given node has the passed Lower Bound qualifier according to the LBC.booleanbooleanisRandomNextInt(Tree methodTree) Returns true if the tree is forRandom.nextInt(int).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, hasSubsequenceToValueMethods inherited from class org.checkerframework.common.basetype.BaseAnnotatedTypeFactory
createFlowAnalysisMethods inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory
addAnnotationsFromDefaultForType, addCheckedCodeDefaults, addCheckedStandardDefaults, addComputedTypeAnnotations, addComputedTypeAnnotationsForWarnRedundant, addDefaultAnnotations, addSharedCFGForTree, addUncheckedStandardDefaults, analyze, annotationsForIrrelevantJavaType, applyInferredAnnotations, applyQualifierParameterDefaults, applyQualifierParameterDefaults, checkAndPerformFlowAnalysis, checkForDefaultQualifierInHierarchy, constructorFromUse, constructorFromUsePreSubstitution, createAndInitQualifierDefaults, createCFGVisualizer, createContractsFromMethod, createDefaultForTypeAnnotator, createDefaultForUseTypeAnnotator, createFlowTransferFunction, createQualifierDefaults, createQualifierPolymorphism, createRequiresOrEnsuresQualifier, 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, typeVariablesFromUseMethods 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, 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
-
UNKNOWN
The @UpperBoundUnknownannotation. -
BOTTOM
The @UpperBoundBottomannotation. -
POLY
The @PolyUpperBoundannotation. -
NEGATIVEONE
The @UpperBoundLiteral(-1) annotation. -
ZERO
The @UpperBoundLiteral(0) annotation. -
ONE
The @UpperBoundLiteral(1) annotation. -
negativeIndexForValueElement
The NegativeIndexFor.value element/field. -
sameLenValueElement
The SameLen.value element/field. -
ltLengthOfValueElement
The LTLengthOf.value element/field. -
ltLengthOfOffsetElement
The LTLengthOf.offset element/field.
-
-
Constructor Details
-
UpperBoundAnnotatedTypeFactory
Create a new UpperBoundAnnotatedTypeFactory.
-
-
Method Details
-
createSupportedTypeQualifiers
Description copied from class:AnnotatedTypeFactoryReturns 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 otherElementTypevalues) are automatically considered as supported annotations.To support a different set of annotations than those in the qual subdirectory, or that have other
ElementTypevalues, 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:
The set of qualifiers returned by@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:
createSupportedTypeQualifiersin 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
Returns the LessThan Checker's annotated type factory. -
addComputedTypeAnnotations
Description copied from class:GenericAnnotatedTypeFactoryTo add annotations to the type of method or constructor parameters, add aTypeAnnotatorusingGenericAnnotatedTypeFactory.createTypeAnnotator()and see the comment inTypeAnnotator.visitExecutable(org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType, Void).- Overrides:
addComputedTypeAnnotationsin classGenericAnnotatedTypeFactory<CFValue,CFStore, CFTransfer, CFAnalysis> - Parameters:
element- an elementtype- the type obtained fromelt
-
addComputedTypeAnnotations
Description copied from class:GenericAnnotatedTypeFactoryLikeGenericAnnotatedTypeFactory.addComputedTypeAnnotations(Tree, AnnotatedTypeMirror). Overriding implementations typically simply pass the boolean to calls to super.- Overrides:
addComputedTypeAnnotationsin classGenericAnnotatedTypeFactory<CFValue,CFStore, CFTransfer, CFAnalysis> - Parameters:
tree- an AST nodetype- the type obtained from treeiUseFlow- whether to use information from dataflow analysis
-
createTypeAnnotator
Description copied from class:GenericAnnotatedTypeFactoryReturns aDefaultForTypeAnnotatorthat adds annotations to a type based on the content of the type itself.Subclass may override this method. The default type annotator is a
ListTypeAnnotatorof the following:IrrelevantTypeAnnotator: Adds top to types not listed in the@RelevantJavaTypesannotation on the checker.PropagationTypeAnnotator: Propagates annotation onto wildcards.
- Overrides:
createTypeAnnotatorin classGenericAnnotatedTypeFactory<CFValue,CFStore, CFTransfer, CFAnalysis> - Returns:
- a type annotator
-
createDependentTypesHelper
Description copied from class:GenericAnnotatedTypeFactoryCreates aDependentTypesHelperand returns it. UseGenericAnnotatedTypeFactory.getDependentTypesHelper()to access the value.- Overrides:
createDependentTypesHelperin classGenericAnnotatedTypeFactory<CFValue,CFStore, CFTransfer, CFAnalysis> - Returns:
- a new
DependentTypesHelper
-
sameLenAnnotationFromTree
Queries the SameLen Checker to return the type that the SameLen Checker associates with the given tree. -
isMathMin
-
isRandomNextInt
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
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
Description copied from class:AnnotatedTypeFactoryReturns theQualifierHierarchyto 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:
createQualifierHierarchyin classAnnotatedTypeFactory- Returns:
- a QualifierHierarchy for this type system
-
createTreeAnnotator
Description copied from class:GenericAnnotatedTypeFactoryReturns aTreeAnnotatorthat adds annotations to a type based on the contents of a tree.The default tree annotator is a
ListTreeAnnotatorof the following:PropagationTreeAnnotator: Propagates annotations from subtreesLiteralTreeAnnotator: Adds annotations based onQualifierForLiteralsmeta-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:
createTreeAnnotatorin classGenericAnnotatedTypeFactory<CFValue,CFStore, CFTransfer, CFAnalysis> - Returns:
- a tree annotator
-
createLiteral
Creates a @UpperBoundLiteralannotation.- Parameters:
i- the integer- Returns:
- a @
UpperBoundLiteralannotation
-
convertUBQualifierToAnnotation
Convert the internal representation to an annotation.- Parameters:
qualifier- a UBQualifier- Returns:
- an annotation corresponding to the given qualifier
-