Package org.checkerframework.checker.index.lowerbound

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 when i is non-negative implies that i will be GTEN1 afterwards). Should this be 3 rules?
• 5. A unary prefix increment shifts the type "up" in the hierarchy (i.e. ++i when i is non-negative implies that i 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
final AnnotationMirror	BOTTOM	The bottom annotation.
final AnnotationMirror	GTEN1	The canonical @GTENegativeOne annotation.
final AnnotationMirror	NN	The canonical @NonNegative annotation.
final AnnotationMirror	POLY	The canonical @PolyLowerBound annotation.
final AnnotationMirror	POS	The canonical @Positive annotation.
final 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, methodInvocationStores, poly, regularExitStores, relevantJavaTypes, returnStatementStores, scannedClasses, shouldClearSubcheckerSharedCFGs, sideEffectsUnrefineAliases, subcheckerSharedCFG, transfer, treeAnnotator, typeAnnotator

Fields inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory

ajavaTypes, annotatedForValueElement, artificialTreeToEnclosingElementMap, 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, wpiOutputFormat

Constructor Summary

Constructors

Constructor	Description
LowerBoundAnnotatedTypeFactory(BaseTypeChecker checker)	Create a new LowerBoundAnnotatedTypeFactory.

Method Summary

Modifier and Type	Method	Description
void	addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, boolean iUseFlow)	Handles cases 1, 2, and 3.
void	addComputedTypeAnnotations(Element element, AnnotatedTypeMirror type)	Handles cases 1, 2, and 3.
protected Set<Class<? extends Annotation>>	createSupportedTypeQualifiers()	Returns a mutable set of annotation classes that are supported by a checker.
TreeAnnotator	createTreeAnnotator()	Returns a TreeAnnotator 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(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, addComputedTypeAnnotationsForWarnRedundant, addDefaultAnnotations, addSharedCFGForTree, addUncheckedStandardDefaults, analyze, annotationsForIrrelevantJavaType, applyInferredAnnotations, applyQualifierParameterDefaults, applyQualifierParameterDefaults, checkAndPerformFlowAnalysis, checkForDefaultQualifierInHierarchy, constructorFromUse, constructorFromUsePreSubstitution, createAndInitQualifierDefaults, createCFGVisualizer, createContractsFromMethod, createDefaultForTypeAnnotator, createDefaultForUseTypeAnnotator, createDependentTypesHelper, 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, getResultingTypeOfConstructorMemberReference, 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, containsSameByClass, containsUninferredTypeArguments, createAnnotatedTypeFormatter, createAnnotationClassLoader, createAnnotationFormatter, createQualifierHierarchy, createQualifierUpperBounds, createTypeArgumentInference, createTypeHierarchy, createTypeVariableSubstitutor, declarationFromElement, doesAnnotatedForApplyToThisChecker, fromElement, fromElement, fromElement, fromNewClass, getAnnotatedNullType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedTypeFormatter, getAnnotatedTypeFromTypeTree, getAnnotationByClass, getAnnotationFormatter, getAnnotationMirror, getAnnotationWithMetaAnnotation, getBoxedType, getBundledTypeQualifiers, getCacheSize, getChecker, getCheckerNames, getContractExpressions, getContractListValues, getCurrentClassTree, getCurrentMethodReceiver, 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, getSelfType, getStringType, getSupportedTypeQualifierNames, getSupportedTypeQualifiers, getTreeUtils, getTypeArgumentInference, getTypeDeclarationBounds, getTypeHierarchy, getTypeOfExtendsImplements, getTypeVarSubstitutor, getUnboxedType, getUninferredWildcardType, getVisitorTreePath, getWholeProgramInference, getWidenedAnnotations, getWidenedType, getWidenedType, hasExplicitNoQualifierParameterInHierarchy, hasExplicitQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, initializeReflectionResolution, isDeterministic, isFromByteCode, isFromStubFile, isImmutable, isSideEffectFree, isSupportedQualifier, isSupportedQualifier, isSupportedQualifier, isWithinConstructor, logGat, makeConditionConsistentWithOtherMethod, mergeAnnotationFileAnnosIntoType, methodFromUse, negateConstant, order, parseAnnotationFiles, postProcessClassTree, replaceAnnotations, replaceAnnotations, setEnclosingElementForArtificialTree, setVisitorTreePath, shouldWarnIfStubRedundantWithBytecode, toAnnotatedType, toString, type, wpiAdjustForUpdateField, wpiAdjustForUpdateNonField, wpiPrepareMethodForWriting, wpiPrepareMethodForWriting, wpiShouldInferTypesForReceivers

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Details

GTEN1

public final AnnotationMirror GTEN1

The canonical @GTENegativeOne annotation.

NN

public final AnnotationMirror NN

The canonical @NonNegative annotation.

POS

public final AnnotationMirror POS

The canonical @Positive annotation.

BOTTOM

public final AnnotationMirror BOTTOM

The bottom annotation.

UNKNOWN

public final AnnotationMirror UNKNOWN

The canonical @LowerBoundUnknown annotation.

POLY

public final AnnotationMirror POLY

The canonical @PolyLowerBound annotation.

Constructor Details

LowerBoundAnnotatedTypeFactory

public LowerBoundAnnotatedTypeFactory(BaseTypeChecker checker)

Create a new LowerBoundAnnotatedTypeFactory.

Parameters:

checker - the type-checker

Method Details

createSupportedTypeQualifiers

protected Set<Class<? extends 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 of ElementType.TYPE_PARAMETER, but no other ElementType 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:

1. Only support annotations located in a checker's qual directory:

   This is the default behavior. Simply place those annotations within the qual directory.

2. 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 calling AnnotatedTypeFactory.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);
     } 
    

3. 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));
     } 
    

   The set of qualifiers returned by AnnotatedTypeFactory.createSupportedTypeQualifiers() must be a fresh, mutable set. The methods AnnotatedTypeFactory.getBundledTypeQualifiers(Class...) must return a fresh, mutable set

Overrides:

createSupportedTypeQualifiers in class AnnotatedTypeFactory

Returns:

the type qualifiers supported this processor, or an empty set if none

addComputedTypeAnnotations

public void addComputedTypeAnnotations(Element element,
 AnnotatedTypeMirror type)

Handles cases 1, 2, and 3.

Overrides:

addComputedTypeAnnotations in class GenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis>

Parameters:

element - an element

type - the type obtained from elt

addComputedTypeAnnotations

public void addComputedTypeAnnotations(Tree tree,
 AnnotatedTypeMirror type,
 boolean iUseFlow)

Handles cases 1, 2, and 3.

Overrides:

addComputedTypeAnnotations in class GenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis>

Parameters:

tree - an AST node

type - the type obtained from tree

iUseFlow - 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 a TreeAnnotator that adds annotations to a type based on the contents of a tree.

The default tree annotator is a ListTreeAnnotator of the following:

1. PropagationTreeAnnotator: Propagates annotations from subtrees
2. LiteralTreeAnnotator: Adds annotations based on QualifierForLiterals meta-annotations
3. DependentTypesTreeAnnotator: 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 class GenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis>

Returns:

a tree annotator

isNonNegative

public boolean isNonNegative(Tree tree)

Checks if the expression is non-negative, i.e. it has Positive on NonNegative annotation.