Package 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, OptionConfiguration
public class IndexChecker extends UpperBoundChecker
A type checker for preventing out-of-bounds accesses on fixed-length sequences, such as arrays and strings. Contains five 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:

Constant Value Checker, SameLen Checker, SearchIndex Checker, Lower Bound Checker, Upper Bound Checker

The Constant Value Checker has no dependencies, but it does trust Positive annotations from the Lower Bound Checker. This means that if the Value Checker is run on code containing Positive annotations, then the Lower Bound Checker also needs to be run to guarantee soundness.

The SameLen Checker has no dependencies.

The SearchIndex Checker depends only on the Value Checker, which it uses to refine SearchIndexFor types to NegativeIndexFor types by comparing to compile-time constants of zero or negative one.

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

  • give appropriate types to compile time constants. For example, the type of 7 is Positive, 0 is NonNegative, etc.
  • in a subtraction expression of the form a.length - x, if x is a compile-time constant, and if the minimum length of a > x, the resulting expression is non-negative.
  • when typing an array length (i.e. a.length), if the minimum length of the array 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.

Value dependencies in the UBC:

  • When computing offsets, the UBC replaces compile-time constants with their known values (though it also keeps an offset with the variable's name, if applicable).
  • 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 minimum 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 Value Checker to determine if the array is guaranteed to be longer than the value of the constant. If it is, the access is safe.
  • When compile time constants would improve the precision of reasoning about arithmetic, the UBC queries the Value Checker for their values. For instance, dividing a value with type LTLengthOf by a compile-time constant of 1 is guaranteed to result in another LTLengthOf for the same arrays.

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.
See the Checker Framework Manual:
Index Checker

  • Constructor Details

    • IndexChecker

      public IndexChecker()
      Creates the Index Checker.