Index checker support for CharSequence

Support for String is being added to the index checker. One feature is to check that String.charAt is called with a valid index. This property is expressed by the @IndexFor(this) annotation on the index parameter.

Because, String implements CharSequence, the method String.charAt can also be called through the CharSequence interface. So to guarantee calling this method with a correct index, calls to CharSequence methods should also be checked.

This generalizes to:

calls to methods of CharSequence taking indices as paremeters, for example CharSequence.subSequence(int start, int end)
calls to methods taking CharSequence and indices, for example StringBuilder.append(CharSequence s, int start, int end)
Solution 1 (ignore mutation)

Support index annotations equally on both String and CharSequence. Problems (both false positives and false negatives) will arise when using mutable classes implementing CharSequence, such as StringBuilder. The length of these sequences may change, for example:

void m(int i) {
    StringBuilder sb = new StringBuilder("0123456789");
    CharSequence cs = sb;
    if(i>=0 && i<cs.length()) { // Refines i to IndexFor("cs")
        sb.setLength(0); // Changes length of cs
        cs.charAt(i); // No warning, but causes StringIndexOutOfBoundsException
    }
}

There is currently a similar situation with applying @StringVal to char[], where the array can be mutated to have a different value than specified by the annotation.

Solution 2 (ignore CharSequence)

Use index annotations on String but not on CharSequence. This approach is not sound with respect to checking correct invocations of String.charAt, because if a string is converted to CharSequence, calls to charAt through this interface are not checked.

public void unsound(String str) {
    str.charAt(100); // argument.type.incompatible
    CharSequence cs = str;
    cs.charAt(100); // no warning, but may cause StringIndexOutOfBoundsException 
}

This solution in code would look like this:

import org.checkerframework.checker.index.qual.IndexFor;

interface CharSequence{
    char charAt(int i);
}

class String implements CharSequence{
    @Override
    public char charAt(@IndexFor("this") int i) {
        throw new RuntimeException("not implemented");
    }
}

This solution does not follow the principle that an overriding method should have weaker or equal preconditions and stronger or equal postconditions. The index checker warns about this if run on the code above:

String.java:9: error: [override.param.invalid] Incompatible parameter type.
    public char charAt(@IndexFor("this") int i) {
                                             ^
  Method
    @LowerBoundUnknown char charAt(@LowerBoundUnknown String this, @NonNegative int p0) in String
    cannot override
    @LowerBoundUnknown char charAt(@LowerBoundUnknown CharSequence this, @LowerBoundUnknown int p0) in CharSequence
  found   : @NonNegative int
  required: @LowerBoundUnknown int
String.java:9: error: [override.param.invalid] Incompatible parameter type.
    public char charAt(@IndexFor("this") int i) {
                                             ^
  Method
    @UpperBoundUnknown char charAt(@UpperBoundUnknown String this, @LTLengthOf("this") int p0) in String
    cannot override
    @UpperBoundUnknown char charAt(@UpperBoundUnknown CharSequence this, @UpperBoundUnknown int p0) in CharSequence
  found   : @LTLengthOf("this") int
  required: @UpperBoundUnknown int
2 errors

Solution 3 (always warn)

The simplest sound solution would be to warn at all invocations methods involving CharSequence. This can be achieved by annotating the parameter with an @UpperBoundBottom annotations:

interface CharSequence{
    char charAt(@NonNegative @UpperBoundBottom int i);
}

Every call to CharSequence.charAt would get a warning like this:

error: [argument.type.incompatible] incompatible types in argument.
        cs.charAt(100);
                  ^
  found   : @UpperBoundUnknown int
  required: @UpperBoundBottom int

Solution 4 (warn on using mutable sequences)

This is an attempt at a compromise solution. The idea is to allow indices to be used only with fixed-length sequences. That means if there is an index for a variable of type CharSequence, then the variable must contain an instance of String (or other fixed-length implementation).

The principles would be:

do not infer IndexFor annotations for sequences of type CharSequence or any non-fixed-length sequence
specify preconditions but not postconditions for CharSequence indices

The downside of this solution is that false positives will be reported when calling the methods in question with mutable sequences such as StringBuilder.

Solution 5 (support mutation)

Add full support for sequences with mutable length to the index checker. This would be the most complex solution. The checker would have to deal with aliasing and side effects.

panacekcz / checker-framework