The Checker Framework Manual:
Custom pluggable types for Java

Chapter 11 Index Checker for sequence bounds (arrays and strings)

The Index Checker warns about potentially out-of-bounds accesses to sequence data structures, such as arrays and strings.

The Index Checker prevents IndexOutOfBoundsExceptions that result from an index expression that might be negative or might be equal to or larger than the sequence’s length. It also prevents NegativeArraySizeExceptions that result from a negative array dimension in an array creation expression. (A caveat: the Index Checker does not check for arithmetic overflow. If an expression overflows, the Index Checker might fail to warn about a possible exception. This is unlikely to be a problem in practice unless you have an array whose length is Integer.MAX_VALUE.)

The programmer can write annotations that indicate which expressions are indices for which sequences. The Index Checker prohibits any operation that may violate these properties, and the Index Checker takes advantage of these properties when verifying indexing operations. Typically, a programmer writes few annotations, because the Index Checker infers properties of indexes from the code around them. For example, it will infer that x is positive within the then block of an if (x > 0) statement. The programmer does need to write field types and method pre-conditions or post-conditions. For instance, if a method’s formal parameter is used as an index for myArray, the programmer might need to write an @IndexFor( "myArray") annotation on the formal parameter’s type.

The Index Checker checks fixed-size data structures, whose size is never changed after creation. A fixed-size data structure has no add or remove operation. Examples are strings and arrays, and you can add support for other fixed-size data structures (see Section 11.9).

To run the Index Checker, run either of these commands:

  javac -processor index MyJavaFile.java
  javac -processor org.checkerframework.checker.index.IndexChecker MyJavaFile.java

Recall that in Java, type annotations are written before the type; in particular, array annotations appear immediately before “[]”. Here is how to declare a length-9 array of positive integers:

    @Positive int @ArrayLen(9) []

Multi-dimensional arrays are similar. Here is how to declare a length-2 array of length-4 arrays:

    String @ArrayLen(2) [] @ArrayLen(4) []

11.1 Index Checker structure and annotations

Internally, the Index Checker computes information about integers that might be indices:

• the lower bound on an integer, such as whether it is known to be positive (Section 11.2)
• the upper bound on an integer, such as whether it is less than the length of a given sequence (Section 11.3)
• whether an integer came from calling the JDK’s binary search routine on an array (Section 11.6)
• whether an integer came from calling a string search routine (Section 11.7)

and about sequence lengths:

• the minimum length of a sequence, such as “myArray contains at least 3 elements” (Section 11.4)
• whether two sequences have the same length (Section 11.5)

The Index Checker checks all these properties at once, but this manual discusses each type system in a different section. There are some annotations that are shorthand for writing multiple annotations, each from a different type system:

@IndexFor(String[] names)

The value is a valid index for the named sequences. For example, the String.charAt(int) method is declared as

    class String {
      char charAt(@IndexFor("this") int index) { ... }
    }

More generally, a variable declared as @IndexFor("someArray") int i has type @IndexFor("someArray") int and its run-time value is guaranteed to be non-negative and less than the length of someArray. You could also express this as @NonNegative @LTLengthOf( "someArray") int i, but @IndexFor("someArray") int i is more concise.

@IndexOrHigh(String[] names)

The value is non-negative and is less than or equal to the length of each named sequence. This type combines @NonNegative and @LTEqLengthOf.

For example, the Arrays.fill method is declared as

    class Arrays {
      void fill(Object[] a, @IndexFor("#1") int fromIndex, @IndexOrHigh("#1") int toIndex, Object val)
    }

@LengthOf(String[] names)

The value is exactly equal to the length of the named sequences. In the implementation, this type aliases @IndexOrHigh, so writing it only adds documentation (although future versions of the Index Checker may use it to improve precision).

@IndexOrLow(String[] names)

The value is -1 or is a valid index for each named sequence. This type combines @GTENegativeOne and @LTLengthOf.

@PolyIndex

indicates qualifier polymorphism. This type combines @PolyLowerBound and @PolyUpperBound. For a description of qualifier polymorphism, see Section 32.2.

@PolyLength

is a special polymorphic qualifier that combines @PolySameLen and @PolyValue from the Constant Value Checker (see Chapter 24). @PolyLength exists as a shorthand for these two annotations, since they often appear together.

11.2 Lower bounds

The Index Checker issues an error when a sequence is indexed by an integer that might be negative. The Lower Bound Checker uses a type system (Figure 11.1) with the following qualifiers:

@Positive: The value is 1 or greater, so it is not too low to be used as an index. Note that this annotation is trusted by the Constant Value Checker, so if the Constant Value Checker is run on code containing this annotation, the Lower Bound Checker must be run on the same code in order to guarantee soundness.
@NonNegative: The value is 0 or greater, so it is not too low to be used as an index.
@GTENegativeOne: The value is -1 or greater. It may not be used as an index for a sequence, because it might be too low. (“GTE” stands for “Greater Than or Equal to”.)
@PolyLowerBound: indicates qualifier polymorphism. For a description of qualifier polymorphism, see Section 32.2.
@LowerBoundUnknown: There is no information about the value. It may not be used as an index for a sequence, because it might be too low.
@LowerBoundBottom: There are no values of this type. This is the bottom type, which should never need to be written by the programmer.

11.3 Upper bounds

The Index Checker issues an error when a sequence index might be too high. To do this, it maintains information about which expressions are safe indices for which sequences. The length of a sequence is arr.length for arrays and str.length() for strings. It issues an error when a sequence arr is indexed by an integer that is not of type @LTLengthOf("arr") or @LTOMLengthOf("arr").

It uses a type system (Figure 11.1) with the following qualifiers:

@LTLengthOf(String[] names, String[] offset)

An expression with this type has value less than the length of each sequence listed in names. The expression may be used as an index into any of those sequences, if it is non-negative. For example, an expression of type @LTLengthOf("a") int might be used as an index to a. The type @LTLengthOf({"a", "b"}) is a subtype of both @LTLengthOf("a") and @LTLengthOf("b"). (“LT” stands for “Less Than”.)

@LTLengthOf takes an optional offset element, meaning that the annotated expression plus the offset is less than the length of the given sequence. For example, suppose expression e has type @LTLengthOf(value = {"a", "b"}, offset = {"-1", "x"}). Then e - 1 is less than a.length, and e + x is less than b.length. This helps to make the checker more precise. Programmers rarely need to write the offset element.

@LTEqLengthOf(String[] names)

An expression with this type has value less than or equal to the length of each sequence listed in names. It may not be used as an index for these sequences, because it might be too high. @LTEqLengthOf({"a", "b"}) is a subtype of both @LTEqLengthOf("a") and @LTEqLengthOf("b"). (“LTEq” stands for “Less Than or Equal to”.)

@LTEqLengthOf({"a"}) = @LTLengthOf(value={"a"}, offset=-1), and
@LTEqLengthOf(value={"a"}, offset=x) = @LTLengthOf(value={"a"}, offset=x-1) for any x.

@LTOMLengthOf(String[] names)

An expression with this type has value at least 2 less than the length of each sequence listed in names. It may always be used as an index for a sequence listed in names, if it is non-negative.

This type exists to allow the checker to infer the safety of loops of the form:

    for (int i = 0; i < array.length - 1; ++i) {
      arr[i] = arr[i+1];
    }

This annotation should rarely (if ever) be written by the programmer; usually @LTLengthOf(String[] names) should be written instead. @LTOMLengthOf({"a", "b"}) is a subtype of both @LTOMLengthOf("a") and @LTOMLengthOf("b"). (“LTOM” stands for “Less Than One Minus”, because another way of saying “at least 2 less than a.length” is “less than a.length-1”.)

@LTOMLengthOf({"a"}) = @LTLengthOf(value={"a"}, offset=1), and
@LTOMLengthOf(value={"a"}, offset=x) = @LTLengthOf(value={"a"}, offset=x+1) for any x.

@UpperBoundLiteral

represents a constant value, typically a literal written in source code. Its subtyping relationship is: @UpperBoundLiteral(lit) <: @LTLengthOf(value="myArray", offset=off) if lit+off ≤ -1.

@PolyUpperBound

indicates qualifier polymorphism. For a description of qualifier polymorphism, see Section 32.2.

@UpperBoundUnknown

There is no information about the upper bound on the value of an expression with this type. It may not be used as an index for a sequence, because it might be too high. This type is the top type, and should never need to be written by the programmer.

@UpperBoundBottom

This is the bottom type for the upper bound type system. It should never need to be written by the programmer.

The following method annotations can be used to establish a method postcondition that ensures that a certain expression is a valid index for a sequence:

@EnsuresLTLengthOf(String[] value, String[] targetValue, String[] offset): When the method with this annotation returns, the expression (or all the expressions) given in the value element is less than the length of the given sequences with the given offsets. More precisely, the expression has the @LTLengthOf qualifier with the value and offset arguments taken from the targetValue and offset elements of this annotation.
@EnsuresLTLengthOfIf(String[] expression, boolean result, String[] targetValue, String[] offset): If the method with this annotation returns the given boolean value, then the given expression (or all the given expressions) is less than the length of the given sequences with the given offsets.

There is one declaration annotation that indicates the relationship between two sequences:

@HasSubsequence(String[] value, String[] from, String[] to)

indicates that a subsequence (from from to to) of the annotated sequence is equal to some other sequence, named by value.

For example, to indicate that shorter is a subsequence of longer:

    int start;
    int end;
    int[] shorter;
    @HasSubsequence(value="shorter", from="this.start", to="this.end")
    int[] longer;

Thus, a valid index into shorter is also a valid index (between start and end-1 inclusive) into longer. More generally, if x is @IndexFor("shorter") in the example above, then start + x is @IndexFor("longer"). If y is @IndexFor("longer") and @LessThan("end"), then y - start is @IndexFor("shorter"). Finally, end - start is @IndexOrHigh("shorter").

This annotation is in part checked and in part trusted. When an array is assigned to longer, three facts are checked: that start is non-negative, that start is less than or equal to end, and that end is less than or equal to the length of longer. This ensures that the indices are valid. The programmer must manually verify that the value of shorter equals the subsequence that the annotation describes.

11.4 Sequence minimum lengths

The Index Checker estimates, for each sequence expression, how long its value might be at run time by computing a minimum length that the sequence is guaranteed to have. This enables the Index Checker to verify indices that are compile-time constants. For example, this code:

    String getThirdElement(String[] arr) {
      return arr[2];
    }

is legal if arr has at least three elements, which can be indicated in this way:

    String getThirdElement(String @MinLen(3) [] arr) {
      return arr[2];
    }

When the index is not a compile-time constant, as in arr[i], then the Index Checker depends not on a @MinLen annotation but on i being annotated as @LTLengthOf("arr").

The MinLen type qualifier is implemented in practice by the Constant Value Checker, using @ArrayLenRange annotations (see Chapter 24). This means that errors related to the minimum lengths of arrays must be suppressed using the “value” argument to @SuppressWarnings. @ArrayLenRange and @ArrayLen annotations can also be used to establish the minimum length of a sequence, if a more precise estimate of length is known. For example, if arr is known to have exactly three elements:

    String getThirdElement(String @ArrayLen(3) [] arr) {
      return arr[2];
    }

The following type qualifiers (from Chapter 24) can establish the minimum length of a sequence:

@MinLen(int value): The value of an expression of this type is a sequence with at least value elements. The default annotation is @MinLen(0), and it may be applied to non-sequences. @MinLen(x) is a subtype of @MinLen(x-1). A @MinLen annotation is treated internally as an @ArrayLenRange with only its from field filled.
@ArrayLen(int[] value): The value of an expression of this type is a sequence whose length is exactly one of the integers listed in its argument. The argument can contain at most 10 integers; larger collections of integers are converted to @ArrayLenRange annotations. The minimum length of a sequence with this annotation is the smallest element of the argument.
@ArrayLenRange(int from, int to): The value of an expression of this type is a sequence whose length is bounded by its arguments, inclusive. The minimum length of a sequence with this annotation is its from argument.

The following method annotation can be used to establish a method postcondition that ensures that a certain sequence has a minimum length:

@EnsuresMinLenIf(String[] expression, boolean result, int targetValue): If the method with this annotation returns the given boolean value, then the given expression (or all the given expressions) is a sequence with at least targetValue elements.

11.5 Sequences of the same length

The Index Checker determines whether two or more sequences have the same length. This enables it to verify that all the indexing operations are safe in code like the following:

    boolean lessThan(double[] arr1, double @SameLen("#1") [] arr2) {
      for (int i = 0; i < arr1.length; i++) {
        if (arr1[i] < arr2[i]) {
          return true;
        } else if (arr1[i] > arr2[i]) {
          return false;
        }
      }
      return false;
    }

When needed, you can specify which sequences have the same length using the following type qualifiers (Figure 11.2):

@SameLen(String[] names): An expression with this type represents a sequence that has the same length as the other sequences named in names. In general, @SameLen types that have non-intersecting sets of names are not subtypes of each other. However, if at least one sequence is named by both types, the types are actually the same, because all the named sequences must have the same length.
@PolySameLen: indicates qualifier polymorphism. For a description of qualifier polymorphism, see Section 32.2.
@SameLenUnknown: No information is known about which other sequences have the same length as this one. This is the top type, and programmers should never need to write it.
@SameLenBottom: This is the bottom type, and programmers should rarely need to write it. null has this type.

11.6 Binary search indices

The JDK’s Arrays.binarySearch method returns either where the value was found, or a negative value indicating where the value could be inserted. The Search Index Checker represents this concept.

The Search Index Checker’s type hierarchy (Figure 11.3) has four type qualifiers:

@SearchIndexFor(String[] names): An expression with this type represents an integer that could have been produced by calling Arrays.binarySearch: for each array a specified in the annotation, the annotated integer is between -a.length-1 and a.length-1, inclusive.
@NegativeIndexFor(String[] names): An expression with this type represents a “negative index” that is between -a.length-1 and -1, inclusive; that is, a value that is both a @SearchIndexFor and negative. Applying the bitwise complement operator (~) to an expression of this type produces an expression of type @IndexOrHigh.
@SearchIndexBottom: This is the bottom type, and programmers should rarely need to write it.
@SearchIndexUnknown: No information is known about whether this integer is a search index. This is the top type, and programmers should rarely need to write it.

11.7 Substring indices

The methods String.indexOf and String.lastIndexOf return an index of a given substring within a given string, or -1 if no such substring exists. The index i returned from receiver.indexOf(substring) satisfies the following property, which is stated here in three equivalent ways:

i == -1 || ( i >= 0       && i <= receiver.length() - substring.length()                   )
i == -1 || ( @NonNegative && @LTLengthOf(value="receiver", offset="substring.length()-1") )
@SubstringIndexFor(value="receiver", offset="substring.length()-1")

The return type of methods String.indexOf and String.lastIndexOf has the annotation @SubstringIndexFor(value="this", offset="#1.length()-1"). This allows writing code such as the following with no warnings from the Index Checker:

    public static String removeSubstring(String original, String removed) {
      int i = original.indexOf(removed);
      if (i != -1) {
        return original.substring(0, i) + original.substring(i + removed.length());
      }
      return original;
    }

The @SubstringIndexFor annotation is implemented in a Substring Index Checker that runs together with the Index Checker and has its own type hierarchy (Figure 11.4) with three type qualifiers:

@SubstringIndexFor(String[] value, String[] offset): An expression with this type represents an integer that could have been produced by calling String.indexOf: the annotated integer is either -1, or it is non-negative and is less than receiver.length() - offset (where the sequence receiver and the offset offset are corresponding elements of the annotation’s arguments).
@SubstringIndexBottom: This is the bottom type, and programmers should rarely need to write it.
@SubstringIndexUnknown: No information is known about whether this integer is a substring index. This is the top type, and programmers should rarely need to write it.

11.7.1 The need for the `@SubstringIndexFor` annotation

No other annotation supported by the Index Checker precisely represents the possible return values of methods String.indexOf and String.lastIndexOf. The reason is the methods’ special cases for empty strings and for failed matches.

Consider the result i of receiver.indexOf(substring):

• i is @GTENegativeOne, because i >= -1.
• i is @LTEqLengthOf("receiver"), because i <= receiver.length().
• i is not @IndexOrLow("receiver"), because for receiver = "", substring = "", i = 0, the property i >= -1 && i < receiver.length() does not hold.
• i is not @IndexOrHigh("receiver"), because for receiver = "", substring = "b", i = -1, the property i >= 0 && i <= receiver.length() does not hold.
• i is not @LTLengthOf(value = "receiver", offset = "substring.length()-1"), because for receiver = "", substring = "abc", i = -1, the property i + substring.length() - 1 < receiver.length() does not hold.

The last annotation in the list above, @LTLengthOf(value = "receiver", offset = "substring.length()-1"), is the correct and precise upper bound for all values of i except -1. The offset expresses the fact that we can add substring.length() to this index and still get a valid index for receiver. That is useful for type-checking code that adds the length of the substring to the found index, in order to obtain the rest of the string. However, the upper bound applies only after the index is explicitly checked not to be -1:

    int i = receiver.indexOf(substring);
    // i is @GTENegativeOne and @LTEqLengthOf("receiver")
    // i is not @LTLengthOf(value = "receiver", offset = "substring.length()-1")
    if (i != -1) {
      // i is @NonNegative and @LTLengthOf(value = "receiver", offset = "substring.length()-1")
      int j = i + substring.length();
      // j is @IndexOrHigh("receiver")
      return receiver.substring(j); // this call is safe
    }

The property of the result of indexOf cannot be expressed by any combination of lower-bound (Section 11.2) and upper-bound (Section 11.3) annotations, because the upper-bound annotations apply independently of the lower-bound annotations, but in this case, the upper bound i <= receiver.length() - substring.length() holds only if i >= 0. Therefore, to express this property and make the example type-check without false positives, a new annotation such as @SubstringIndexFor(value = "receiver", offset = "substring.length()-1") is necessary.

11.8 Inequalities

The Index Checker estimates which expressions’ values are less than other expressions’ values.

@LessThan(String[] values)

An expression with this type has a value that is less than the value of each expression listed in values. The expressions in values must be composed of final or effectively final variables and constants.

@LessThanUnknown

There is no information about the value of an expression of this type relative to other expressions. This is the top type, and should not be written by the programmer.

@LessThanBottom

This is the bottom type for the less-than type system. It should never need to be written by the programmer.

11.9 Annotating your own fixed-size datatypes

The Index Checker has built-in support for Strings and arrays. You can add support for additional fixed-size data structures by writing annotations. This allows the Index Checker to type-check the data structure’s implementation and to type-check uses of the class.

This section gives an example: a fixed-length collection.

/** ArrayWrapper is a fixed-size generic collection. */
public class ArrayWrapper<T> {
    private final Object @SameLen("this") [] delegate;

    @SuppressWarnings("index") // constructor creates object of size @SameLen(this) by definition
    ArrayWrapper(@NonNegative int size) {
        delegate = new Object[size];
    }

    public @LengthOf("this") int size() {
        return delegate.length;
    }

    public void set(@IndexFor("this") int index, T obj) {
        delegate[index] = obj;
    }

    @SuppressWarnings("unchecked") // required for normal Java compilation due to unchecked cast
    public T get(@IndexFor("this") int index) {
        return (T) delegate[index];
    }
}

The Index Checker treats a call to a method annotated with @LengthOf("this") like arr.length for arrays and str.length() for strings.

With these annotations, client code like the following type-checks with no warnings:

    public static void clearIndex1(ArrayWrapper<? extends Object> a, @IndexFor("#1") int i) {
      a.set(i, null);
    }

    public static void clearIndex2(ArrayWrapper<? extends Object> a, int i) {
      if (0 <= i && i < a.size()) {
        a.set(i, null);
      }
    }

11.10 Technical papers

The paper “Lightweight Verification of Array Indexing” (ISSTA 2018, https://homes.cs.washington.edu/~mernst/pubs/array-indexing-issta2018-abstract.html) gives more details about the Index Checker. “Enforcing correct array indexes with a type system” [San16] (FSE 2016) describes an earlier version.

The Checker Framework Manual: Custom pluggable types for Java