Index Checker does not recognize swapping index and offset

[panacekcz]

In @LTLengthOf, the offset and the index can be swapped (index+offset<length is equivalent to offset+index<length). However, the Index Checker does not recognize this equivalence.

Example of code that is safe:

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

public class SwapOffsetIndex {
	public void m(Object[] a, int offset, @LTLengthOf(value="#1", offset="#2") int index) {
		@LTLengthOf("a") int i = offset + index; // OK
		@LTLengthOf(value="a", offset="offset") int i1 = index; // OK
		@LTLengthOf(value="a", offset="index") int i2 = offset; // false positive
	}
}

Current output:

SwapOffsetIndex.java:7: error: [assignment.type.incompatible] incompatible types in assignment.
		@LTLengthOf(value="a", offset="index") int i2 = offset; // false positive
		                                                ^
  found   : @UpperBoundUnknown int
  required: @LTLengthOf(value="a", offset="index") int
1 error

In this example from Guava, count is known to be @LTLengthOf(value="array", offset="values.length - 1") because of a postcondition, but the method call requires that values.length is @LTLengthOf(value="array", offset="count - 1").

import org.checkerframework.checker.index.qual.EnsuresLTLengthOf;
import org.checkerframework.checker.index.qual.IndexOrHigh;
import org.checkerframework.checker.index.qual.NonNegative;

public class Arraycopy {

	long[] array;
	@IndexOrHigh("array") int count;

	@SuppressWarnings("contracts.postcondition.not.satisfied")
	@EnsuresLTLengthOf(value = "count", targetValue = "array", offset = "#1 - 1")
	private void ensureRoomFor(@NonNegative int numberToAdd) {
	}

	public void addAll(long[] values) {
		ensureRoomFor(values.length);
		System.arraycopy(values, 0, array, count, values.length); // false positive
	}
}

Output:

Arraycopy.java:17: error: [argument.type.incompatible] incompatible types in argument.
		System.arraycopy(values, 0, array, count, values.length); // false positive
		                                                ^
  found   : @LTEqLengthOf("values") int
  required: @LTLengthOf(value={"values", "this.array"}, offset={"-1", "this.count - 1"}) int
1 error