org.checkerframework.checker.index

Class IndexChecker

java.lang.Object

javax.annotation.processing.AbstractProcessor

org.checkerframework.javacutil.AbstractTypeProcessor

org.checkerframework.framework.source.SourceChecker

org.checkerframework.common.basetype.BaseTypeChecker

org.checkerframework.checker.index.upperbound.UpperBoundChecker

org.checkerframework.checker.index.IndexChecker

All Implemented Interfaces:

Processor, BaseTypeContext, BaseContext, CFContext, OptionConfiguration, ErrorHandler

public class IndexChecker
extends UpperBoundChecker

A type checker for preventing out-of-bounds accesses on arrays. Contains four subcheckers that do all of the actual work, which are described here. First, the order the checkers are run in is described, and then what each checker requests from the checkers that run before it is described. The Index Checker itself is just an alias for the Upper Bound Checker, which runs last.

The checkers run in this order:

SameLen Checker, MinLen Checker, Lower Bound Checker, Upper Bound Checker

The SameLen Checker has no dependencies.

The MinLen Checker has no dependencies on the SameLen checker, so they may actually be run in any order.

The Lower Bound Checker depends only on the MinLen Checker. It uses the MinLen checker to:

• in a subtraction expression of the form `a.length - x`, if x is a compile time constant, the LBC queries the MLC for the min length of a. If MinLen(a) > x, the resulting expression is non-negative.
• when typing an array length (i.e. `a.length`), if the MinLen is >= 1, then the type is @Positive; if its MinLen is zero, then the type is @NonNegative.

The Upper Bound Checker depends on all three other checkers.

MinLen dependencies in the UBC:

• The UBC has relaxed assignment rules: it allows assignments where the right hand side is a value known at compile time and the type of the left hand side is annotated with LT*LengthOf("a"). If the min length of a is in the correct relationship with the value on the right hand side, then the assignment is legal.
• When checking whether an array access is legal, the UBC first checks the upper bound type of the index. If that fails, it checks if the index is a compile time constant. If it is, then it queries the MinLen Checker to determine if the array is longer than the value of the constant. If it is, the access is safe.

SameLen dependencies in the UBC:

• When checking whether an array access is legal, the UBC first checks the upper bound type. If it's an LTL (or LTOM/LTEL), then it collects, from the SameLen Checker, the list of arrays that are known to be the same length as the array being accessed. Then the annotation is checked to see if it is valid for any of the arrays in question.

Lower Bound dependencies in UBC:

• When an array is created with length equal to the sum of two quantities, if one of the quantities is non-negative, the other becomes LTEL of the new array. If one is positive, the other becomes LTL.
• When a non-negative is subtracted from an LTL, it stays LTL.

Proposed possible dependencies:

The MinLen Checker would like to depend on the Lower Bound Checker. This would allow the following case:

• When an array is created with a positive length argument, the array has @MinLen(1).

See the Checker Framework Manual:

Index Checker

Nested Class Summary

Nested classes/interfaces inherited from class org.checkerframework.framework.source.SourceChecker

SourceChecker.CheckerError

Field Summary

Fields inherited from class org.checkerframework.framework.source.SourceChecker

currentRoot, DETAILS_SEPARATOR, errsOnLastExit, messager, messages, MSGS_FILE, parentChecker, SUPPRESS_ALL_KEY, trees, upstreamCheckerNames, visitor

Fields inherited from class javax.annotation.processing.AbstractProcessor

processingEnv

Constructor Summary

Constructors

Constructor and Description
IndexChecker()

Method Summary

Methods inherited from class org.checkerframework.checker.index.upperbound.UpperBoundChecker

getImmediateSubcheckerClasses

Methods inherited from class org.checkerframework.common.basetype.BaseTypeChecker

createSourceVisitor, getAnnotationProvider, getChecker, getContext, getOptions, getSubchecker, getSupportedLintOptions, getSupportedOptions, getTypeFactory, getTypeFactoryOfSubchecker, getVisitor, initChecker, invokeConstructorFor, printMessage, processArg, shouldAddShutdownHook, shouldResolveReflection, shutdownHook, typeProcess, typeProcessingOver

Methods inherited from class org.checkerframework.framework.source.SourceChecker

addOptions, createSupportedLintOptions, errorAbort, errorAbort, expandCFOptions, formatStackTrace, fullMessageOf, getElementUtils, getLintOption, getLintOption, getMessages, getOption, getOption, getOptionConfiguration, getProcessingEnvironment, getProperties, getStandardSuppressWarningsKeys, getSupportedAnnotationTypes, getSupportedSourceVersion, getSuppressWarningsKeys, getTreeUtils, getTypeUtils, getUpstreamCheckerNames, hasOption, init, message, message, printStats, report, setLintOption, setParentChecker, setProcessingEnvironment, setSupportedLintOptions, shouldSkipDefs, shouldSkipDefs, shouldSkipUses, shouldSkipUses, shouldSuppressWarnings, shouldSuppressWarnings, treeToFilePositionString, typeProcessingStart, userErrorAbort, useUncheckedCodeDefault

Methods inherited from class org.checkerframework.javacutil.AbstractTypeProcessor

process

Methods inherited from class javax.annotation.processing.AbstractProcessor

getCompletions, isInitialized

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.checkerframework.framework.util.BaseContext

getElementUtils, getOptionConfiguration, getProcessingEnvironment, getTreeUtils, getTypeUtils

Constructor Detail

IndexChecker

public IndexChecker()