Package org.checkerframework.checker.index.upperbound

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 final 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.CapturedTypeVarSubstitutor, AnnotatedTypeFactory.ParameterizedExecutableType

Field Summary

Fields

Modifier and Type	Field	Description
final AnnotationMirror	BOTTOM	The @UpperBoundBottom annotation.
final ExecutableElement	ltLengthOfOffsetElement	The LTLengthOf.offset element/field.
final ExecutableElement	ltLengthOfValueElement	The LTLengthOf.value element/field.
final ExecutableElement	negativeIndexForValueElement	The NegativeIndexFor.value element/field.
final AnnotationMirror	NEGATIVEONE	The @UpperBoundLiteral(-1) annotation.
final AnnotationMirror	ONE	The @UpperBoundLiteral(1) annotation.
final AnnotationMirror	POLY	The @PolyUpperBound annotation.
final ExecutableElement	sameLenValueElement	The SameLen.value element/field.
final AnnotationMirror	UNKNOWN	The @UpperBoundUnknown annotation.
final 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, methodInvocationStores, poly, regularExitStores, relevantJavaTypes, returnStatementStores, scannedClasses, shouldClearSubcheckerSharedCFGs, sideEffectsUnrefineAliases, subcheckerSharedCFG, transfer, treeAnnotator, typeAnnotator

Fields 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, types, typeVarSubstitutor, uid, wpiOutputFormat

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method	Description
void	addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, boolean iUseFlow)	Like GenericAnnotatedTypeFactory.addComputedTypeAnnotations(Tree, AnnotatedTypeMirror).
void	addComputedTypeAnnotations(Element element, AnnotatedTypeMirror type)	To add annotations to the type of method or constructor parameters, add a TypeAnnotator using GenericAnnotatedTypeFactory.createTypeAnnotator() and see the comment in TypeAnnotator.visitExecutable(org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType, Void).
AnnotationMirror	convertUBQualifierToAnnotation(UBQualifier qualifier)	Convert the internal representation to an annotation.
protected DependentTypesHelper	createDependentTypesHelper()	Creates a DependentTypesHelper and returns it.
AnnotationMirror	createLiteral(int i)	Creates a @UpperBoundLiteral annotation.
protected QualifierHierarchy	createQualifierHierarchy()	Returns the QualifierHierarchy to be used by this checker.
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.
protected TypeAnnotator	createTypeAnnotator()	Returns a DefaultForTypeAnnotator 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, Class<? extends Annotation> classOfType)	Returns true iff the given node has the passed Lower Bound qualifier according to the LBC.
boolean	isMathMin(Tree methodTree)
boolean	isRandomNextInt(Tree methodTree)	Returns true if the tree is for Random.nextInt(int).
@Nullable AnnotationMirror	sameLenAnnotationFromTree(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, 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, 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, constructorFromUse, constructorFromUseWithoutTypeArgInference, containsCapturedTypes, containsSameByClass, createAnnotatedTypeFormatter, createAnnotationClassLoader, createAnnotationFormatter, createQualifierUpperBounds, createTypeArgumentInference, createTypeHierarchy, 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

Methods inherited from class java.lang.Object

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

Field Details

UNKNOWN

public final AnnotationMirror UNKNOWN

The @UpperBoundUnknown annotation.

BOTTOM

public final AnnotationMirror BOTTOM

The @UpperBoundBottom annotation.

POLY

public final AnnotationMirror POLY

The @PolyUpperBound annotation.

NEGATIVEONE

public final AnnotationMirror NEGATIVEONE

The @UpperBoundLiteral(-1) annotation.

ZERO

public final AnnotationMirror ZERO

The @UpperBoundLiteral(0) annotation.

ONE

public final AnnotationMirror ONE

The @UpperBoundLiteral(1) annotation.

negativeIndexForValueElement

public final ExecutableElement negativeIndexForValueElement

The NegativeIndexFor.value element/field.

sameLenValueElement

public final ExecutableElement sameLenValueElement

The SameLen.value element/field.

ltLengthOfValueElement

public final ExecutableElement ltLengthOfValueElement

The LTLengthOf.value element/field.

ltLengthOfOffsetElement

public final ExecutableElement ltLengthOfOffsetElement

The LTLengthOf.offset element/field.

Constructor Details

UpperBoundAnnotatedTypeFactory

public UpperBoundAnnotatedTypeFactory(BaseTypeChecker checker)

Create a new UpperBoundAnnotatedTypeFactory.

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

getLessThanAnnotatedTypeFactory

public LessThanAnnotatedTypeFactory getLessThanAnnotatedTypeFactory()

Returns the LessThan Checker's annotated type factory.

addComputedTypeAnnotations

public void addComputedTypeAnnotations(Element element,
 AnnotatedTypeMirror type)

Description copied from class: GenericAnnotatedTypeFactory

To add annotations to the type of method or constructor parameters, add a TypeAnnotator using GenericAnnotatedTypeFactory.createTypeAnnotator() and see the comment in TypeAnnotator.visitExecutable(org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType, Void).

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)

Description copied from class: GenericAnnotatedTypeFactory

Like GenericAnnotatedTypeFactory.addComputedTypeAnnotations(Tree, AnnotatedTypeMirror). Overriding implementations typically simply pass the boolean to calls to super.

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

createTypeAnnotator

protected TypeAnnotator createTypeAnnotator()

Description copied from class: GenericAnnotatedTypeFactory

Returns a DefaultForTypeAnnotator 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:

1. IrrelevantTypeAnnotator: Adds top to types not listed in the @RelevantJavaTypes annotation on the checker.
2. PropagationTypeAnnotator: Propagates annotation onto wildcards.

Overrides:

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

Returns:

a type annotator

createDependentTypesHelper

protected DependentTypesHelper createDependentTypesHelper()

Description copied from class: GenericAnnotatedTypeFactory

Creates a DependentTypesHelper and returns it. Use GenericAnnotatedTypeFactory.getDependentTypesHelper() to access the value.

Overrides:

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

Returns:

a new DependentTypesHelper

sameLenAnnotationFromTree

public @Nullable AnnotationMirror sameLenAnnotationFromTree(Tree tree)

Queries the SameLen Checker to return the type that the SameLen Checker associates with the given tree.

isMathMin

public boolean isMathMin(Tree methodTree)

isRandomNextInt

public boolean isRandomNextInt(Tree methodTree)

Returns true if the tree is for Random.nextInt(int).

Parameters:

methodTree - a tree to check

Returns:

true iff the tree is for Random.nextInt(int)

hasLowerBoundTypeByClass

public boolean hasLowerBoundTypeByClass(Node node,
 Class<? extends 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 node

classOfType - 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 the QualifierHierarchy 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 of NoElementQualifierHierarchy.

Subclasses must override this method if their qualifiers have elements; the method must return an implementation of QualifierHierarchy, such as ElementQualifierHierarchy.

Overrides:

createQualifierHierarchy in class AnnotatedTypeFactory

Returns:

a QualifierHierarchy for this type system

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

createLiteral

public AnnotationMirror createLiteral(int i)

Creates a @UpperBoundLiteral annotation.

Parameters:

i - the integer

Returns:

a @UpperBoundLiteral annotation

convertUBQualifierToAnnotation

public AnnotationMirror convertUBQualifierToAnnotation(UBQualifier qualifier)

Convert the internal representation to an annotation.

Parameters:

qualifier - a UBQualifier

Returns:

an annotation corresponding to the given qualifier