Class LowerBoundAnnotatedTypeFactory
- 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.lowerbound.LowerBoundAnnotatedTypeFactory
-
- All Implemented Interfaces:
AnnotationProvider
public class LowerBoundAnnotatedTypeFactory extends BaseAnnotatedTypeFactoryForIndexChecker
Implements the introduction rules for the Lower Bound Checker.The type hierarchy is: Top = lbu ("Lower Bound Unknown") | gte-1 ("Greater than or equal to -1") | nn ("NonNegative") | pos ("Positive")
In general, check whether the constant Value Checker can determine the value of a variable; if it can, use that; if not, use more specific rules based on expression type. This class implements the following type rules:- 1. If the value checker type for any expression is ≥ 1, refine that expression's type to positive.
- 2. If the value checker type for any expression is ≥ 0 and case 1 did not apply, then refine that expression's type to non-negative.
- 3. If the value checker type for any expression is ≥ -1 and cases 1 and 2 did not apply, then refine that expression's type to GTEN1.
- 4. A unary prefix decrement shifts the type "down" in the hierarchy (i.e.
--i
wheni
is non-negative implies thati
will be GTEN1 afterwards). Should this be 3 rules? - 5. A unary prefix increment shifts the type "up" in the hierarchy (i.e.
++i
wheni
is non-negative implies thati
will be positive afterwards). Should this be 3 rules? - 6. Unary negation on a NegativeIndexFor from the SearchIndex type system results in a non-negative.
- 7. The result of a call to Math.max is the GLB of its arguments.
- 8. If an array has a MinLen type ≥ 1 and its length is accessed, the length expression is positive.
-
-
Nested Class Summary
-
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 bottom annotation.javax.lang.model.element.AnnotationMirror
GTEN1
The canonical @GTENegativeOne
annotation.javax.lang.model.element.AnnotationMirror
NN
The canonical @NonNegative
annotation.javax.lang.model.element.AnnotationMirror
POLY
The canonical @PolyLowerBound
annotation.javax.lang.model.element.AnnotationMirror
POS
The canonical @Positive
annotation.javax.lang.model.element.AnnotationMirror
UNKNOWN
The canonical @LowerBoundUnknown
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 LowerBoundAnnotatedTypeFactory(BaseTypeChecker checker)
Create a new LowerBoundAnnotatedTypeFactory.
-
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)
Handles cases 1, 2, and 3.void
addComputedTypeAnnotations(javax.lang.model.element.Element element, AnnotatedTypeMirror type)
Handles cases 1, 2, and 3.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.LessThanAnnotatedTypeFactory
getLessThanAnnotatedTypeFactory()
Returns the LessThan Checker's annotated type factory.SearchIndexAnnotatedTypeFactory
getSearchIndexAnnotatedTypeFactory()
Returns the SearchIndexFor Checker's annotated type factory.ValueAnnotatedTypeFactory
getValueAnnotatedTypeFactory()
Returns the Value Checker's annotated type factory.boolean
isNonNegative(com.sun.source.tree.Tree tree)
Checks if the expression is non-negative, i.e.-
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, createDependentTypesHelper, 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, createQualifierHierarchy, 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
-
GTEN1
public final javax.lang.model.element.AnnotationMirror GTEN1
The canonical @GTENegativeOne
annotation.
-
NN
public final javax.lang.model.element.AnnotationMirror NN
The canonical @NonNegative
annotation.
-
POS
public final javax.lang.model.element.AnnotationMirror POS
The canonical @Positive
annotation.
-
BOTTOM
public final javax.lang.model.element.AnnotationMirror BOTTOM
The bottom annotation.
-
UNKNOWN
public final javax.lang.model.element.AnnotationMirror UNKNOWN
The canonical @LowerBoundUnknown
annotation.
-
POLY
public final javax.lang.model.element.AnnotationMirror POLY
The canonical @PolyLowerBound
annotation.
-
-
Constructor Detail
-
LowerBoundAnnotatedTypeFactory
public LowerBoundAnnotatedTypeFactory(BaseTypeChecker checker)
Create a new LowerBoundAnnotatedTypeFactory.- Parameters:
checker
- the type-checker
-
-
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:
-
addComputedTypeAnnotations
public void addComputedTypeAnnotations(javax.lang.model.element.Element element, AnnotatedTypeMirror type)
Handles cases 1, 2, and 3.- 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)
Handles cases 1, 2, and 3.- 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
-
getValueAnnotatedTypeFactory
public ValueAnnotatedTypeFactory getValueAnnotatedTypeFactory()
Returns the Value Checker's annotated type factory.
-
getSearchIndexAnnotatedTypeFactory
public SearchIndexAnnotatedTypeFactory getSearchIndexAnnotatedTypeFactory()
Returns the SearchIndexFor Checker's annotated type factory.
-
getLessThanAnnotatedTypeFactory
public LessThanAnnotatedTypeFactory getLessThanAnnotatedTypeFactory()
Returns the LessThan Checker's annotated type factory.
-
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
-
isNonNegative
public boolean isNonNegative(com.sun.source.tree.Tree tree)
Checks if the expression is non-negative, i.e. it has Positive on NonNegative annotation.
-
-