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.lowerbound.LowerBoundAnnotatedTypeFactory

All Implemented Interfaces:

AnnotationProvider

public class LowerBoundAnnotatedTypeFactory
extends BaseAnnotatedTypeFactory

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 and Description
AnnotationMirror	BOTTOM The bottom annotation.
AnnotationMirror	GTEN1 The canonical @GTENegativeOne annotation.
AnnotationMirror	NN The canonical @NonNegative annotation.
AnnotationMirror	POLY The canonical @PolyLowerBound annotation.
AnnotationMirror	POS The canonical @Positive annotation.
AnnotationMirror	UNKNOWN The canonical @LowerBoundUnknown annotation.

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

analysis, cfgVisualizer, defaults, dependentTypesHelper, emptyStore, exceptionalExitStores, flowByDefault, flowResult, flowResultAnalysisCaches, initializationStaticStore, initializationStore, methodInvocationStores, poly, regularExitStores, returnStatementStores, scannedClasses, transfer, treeAnnotator, typeAnnotator

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

artificialTreeToEnclosingElementMap, checker, elements, fromExpressionTreeCache, fromMemberTreeCache, fromTypeTreeCache, ignoreUninferredTypeArguments, loader, objectGetClass, processingEnv, qualHierarchy, qualifierUpperBounds, reflectionResolver, root, shouldCache, stubTypes, trees, typeArgumentInference, typeFormatter, typeHierarchy, types, typeVarSubstitutor, uid, visitorState

Constructor Summary

Constructors

Constructor and Description
LowerBoundAnnotatedTypeFactory(BaseTypeChecker checker)

Method Summary

Modifier and Type	Method and Description
void	addComputedTypeAnnotations(Element element, AnnotatedTypeMirror type) Handles cases 1, 2, and 3.
void	addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, boolean iUseFlow) 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.common.basetype.BaseAnnotatedTypeFactory

createFlowAnalysis

Methods inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory

addAnnotationsFromDefaultForType, addCheckedCodeDefaults, addCheckedStandardDefaults, addComputedTypeAnnotations, addDefaultAnnotations, addUncheckedStandardDefaults, analyze, applyInferredAnnotations, applyQualifierParameterDefaults, applyQualifierParameterDefaults, checkAndPerformFlowAnalysis, checkForDefaultQualifierInHierarchy, constructorFromUse, constructorFromUsePreSubstitution, createAndInitQualifierDefaults, createCFGVisualizer, createDefaultForTypeAnnotator, createDefaultForUseTypeAnnotator, createDependentTypesHelper, createFlowTransferFunction, createQualifierDefaults, createQualifierPolymorphism, createTypeAnnotator, fromNewClass, getAnnotatedTypeLhs, getAnnotatedTypeLhsNoTypeVarDefault, getAnnotatedTypeRhsUnaryAssign, getAnnotatedTypeVarargsArray, getAnnotationFromJavaExpressionString, getAnnotationFromReceiver, getAnnotationMirrorFromJavaExpressionString, getCFGVisualizer, getDependentTypesHelper, getEmptyStore, getExceptionalExitStore, getFinalLocalValues, getFirstNodeOfKindForTree, getInferredValueFor, getMethodReturnType, getMethodReturnType, getNodesForTree, getQualifierPolymorphism, getReceiverAndOffsetFromJavaExpressionString, getReceiverFromJavaExpressionString, getRegularExitStore, getResultingTypeOfConstructorMemberReference, getReturnStatementStores, getShouldDefaultTypeVarLocals, getSortedQualifierNames, getStoreAfter, getStoreAfter, getStoreAfter, getStoreBefore, getStoreBefore, getStoreBefore, getSupportedMonotonicTypeQualifiers, getTypeFactoryOfSubchecker, handleCFGViz, methodFromUse, methodFromUsePreSubstitution, performFlowAnalysis, postAnalyze, postAsMemberOf, postDirectSuperTypes, postInit, preProcessClassTree, setRoot, typeVariablesFromUse

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

adaptGetClassReturnTypeToReceiver, addAliasedAnnotation, addAliasedAnnotation, addAliasedAnnotation, addAliasedAnnotation, addAliasedDeclAnnotation, addAnnotationFromFieldInvariant, addInheritedAnnotation, applyUnboxing, areSameByClass, binaryTreeArgTypes, canonicalAnnotation, checkInvalidOptionsInferSignatures, containsSameByClass, createAnnotatedTypeFormatter, createAnnotationClassLoader, createAnnotationFormatter, createQualifierHierarchy, createQualifierHierarchyWithMultiGraphFactory, createQualifierUpperBounds, createTypeArgumentInference, createTypeHierarchy, createTypeVariableSubstitutor, declarationFromElement, fromElement, fromElement, fromElement, getAnnotatedNullType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedTypeFormatter, getAnnotatedTypeFromTypeTree, getAnnotationByClass, getAnnotationFormatter, getAnnotationMirror, getAnnotationWithMetaAnnotation, getBoxedType, getBundledTypeQualifiers, getCacheSize, getContext, getCurrentClassTree, getCurrentClassType, getCurrentMethodReceiver, getDeclAnnotation, getDeclAnnotationNoAliases, getDeclAnnotations, getDeclAnnotationWithMetaAnnotation, getDefaultTypeDeclarationBounds, getDummyAssignedTo, getElementUtils, getEnclosingClassOrMethod, getEnclosingElementForArtificialTree, getEnclosingType, getExpressionAndOffset, getFieldInvariantAnnotationTree, getFieldInvariantDeclarationAnnotations, getFieldInvariants, getFnInterfaceFromTree, getFunctionTypeFromTree, getFunctionTypeFromTree, getImplicitReceiverType, getNarrowedPrimitive, getPath, getProcessingEnv, getQualifierHierarchy, getQualifierParameterHierarchies, getQualifierParameterHierarchies, getQualifierUpperBounds, getReceiverType, getSelfType, getStringType, getSupportedTypeQualifierNames, getSupportedTypeQualifiers, getTreeUtils, getTypeArgumentInference, getTypeDeclarationBounds, getTypeHierarchy, getTypeOfExtendsImplements, getTypeVarSubstitutor, getUnboxedType, getUninferredWildcardType, getVisitorState, getWholeProgramInference, getWidenedAnnotations, getWidenedType, hasExplicitNoQualifierParameterInHierarchy, hasExplicitQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, initializeReflectionResolution, isFromByteCode, isFromStubFile, isSupportedQualifier, isSupportedQualifier, isSupportedQualifier, isWithinConstructor, mergeStubsIntoType, methodFromUse, negateConstant, parseStubFiles, postProcessClassTree, postTypeVarSubstitution, setEnclosingElementForArtificialTree, shouldWarnIfStubRedundantWithBytecode, toAnnotatedType, toString, type, widenToUpperBound

Methods inherited from class java.lang.Object

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

Field Detail

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 Detail

LowerBoundAnnotatedTypeFactory

public LowerBoundAnnotatedTypeFactory(BaseTypeChecker checker)

Method Detail

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.