How to write index annotations on index ranges?

[panacekcz]

This applies to both strings and arrays. There are several methods that take a string or array and a range expressed as a pair of integers.

Begin and End

For example, Arrays.sort(char[] a, int fromIndex, int toIndex), or String.substring(int beginIndex, int endIndex).

• The exact precondition is 0 <= from && from <= to && to <= a.length.
• The current annotation is @IndexFor("#1") int fromIndex, @IndexOrHigh("#1") int toIndex. This disallows valid Arrays.sort(a, a.length, a.length) and allows invalid Arrays.sort(a, 1, 0) for char @MinLen(1)[] a.
• Arrays.sort and Arrays.fill throw IllegalArgumentException if from > to.
• The condition from <= to cannot be expressed using current index annotations.
• In typetools#1413, I relaxed the lower index annotation on String methods to @IndexOrHigh, to reduce false positives.

Offset and Length

For example, String(char[] value, int offset, int count).

• The exact precondition is 0 <= offset && 0 <= count && offset + count <= value.length.
• The current way to annotate these methods is @IndexFor("#1") int offset, @IndexOrHigh("#1") int count. This disallows valid new String(a, a.length, 0) and allows invalid new String(a, 1, a.length) for char @MinLen(1)[] a.
• The precondition can be expressed precisely by (char[] value, @NonNegative @LTLengthOf(value="#1", offset="#3-1") int offset, @NonNegative @LTLengthOf(value="#1", offset="#2-1") int count)

Conversion to Begin and End

If a method takes offset and length and calls a method taking begin and end, it calls it like s.substring(offset, offset + length). Using the current annotations, it is not guaranteed that the second index will be valid.

For example in plume-lib, CountingPrintWriter.java, the index checker warns about such call:

src/plume/CountingPrintWriter.java:408: warning: [argument.type.incompatible] incompatible types in argument.
    writtenBytes += countBytes(s.substring(off, off + len));
                                                    ^
  found   : @LTLengthOf(value={"s", "s"}, offset={"-len", "-off - 1"}) int
  required: @LTEqLengthOf("s") int

[panacekcz]

System.arraycopy uses offsets on the length parameter: typetools#1076