Use case for "variable < variable"

[mernst]

The Index Checker intentionally does not express "variable < variable", because anything derivable from this fact is usually derivable from other facts. Here is an example where I don't see how to express the safety of the code in terms of other Index Checker annotations. The output is:

$ch/bin/javac -processor index VarLteVar.java
VarLteVar.java:13: error: [array.access.unsafe.high] Potentially unsafe array access: the index could be larger than the array's bound
                intermediate[length++] = seq1[i];
                                   ^
  found   : @UpperBoundUnknown int
  required: an integer less than intermediate's length (@LTLengthOf("intermediate"))
VarLteVar.java:16: error: [argument.type.incompatible] incompatible types in argument.
        return subarray(intermediate, 0, length);
                                         ^
  found   : @UpperBoundUnknown int
  required: @LTEqLengthOf("intermediate") int
2 errors

and here is the code:

// Test case for https://github.com/kelloggm/checker-framework/issues/158
// It is easy to see that:
//   * i is an index for intermediate
//   * length <= i (or, at least length <= i+1)
// but I don't see how to verif that length is an index for intermediate.

// @skip-test

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

public class VarLteVar {

    /** Returns an array that is equivalent to the set difference of seq1 and seq2. */
    public static boolean[] setDiff(boolean[] seq1, boolean[] seq2) {
        boolean[] intermediate = new boolean[seq1.length];
        int length = 0;
        for (int i = 0; i < seq1.length; i++) {
            if (!memberOf(seq1[i], seq2)) {
                intermediate[length++] = seq1[i];
            }
        }
        return subarray(intermediate, 0, length);
    }

    public static boolean memberOf(boolean elt, boolean[] arr) {
        for (int i = 0; i < arr.length; i++) {
            if (arr[i] == elt) {
                return true;
            }
        }
        return false;
    }

    @SuppressWarnings("index") // not relevant to this test case
    public static boolean[] subarray(
            boolean[] a, @IndexOrHigh("#1") int startindex, @IndexOrHigh("#1") int length) {
        boolean[] result = new boolean[length];
        System.arraycopy(a, startindex, result, 0, length);
        return result;
    }
}

[kelloggm]

This is related to #132 and #43, and any solution for it should address both of those, as well. I view this as a feature request for either:

• Adding offsets to SameLen in the same way that we did for LTLengthOf, or
• Adding new types to the Same Len Checker of the form ShorterThan and LongerThan, both of which would take a list of arrays as arguments

Of the two, I would prefer the second approach. I don't think I have time to implement it right now, and I don't have a good feeling for how it would complicate type checking (probably not that much), but it should remain on the table as an option. If this continues to be an issue, we should implement something like this.

[JasonMrX]

Hi @mernst,

Would you mind elaborating "because anything derivable from this fact is usually derivable from other facts" a bit more? I am still confused with why Index Checker intentionally does not express "variable < variable".

Thanks!

Jason

[mernst]

Up until now, we had never needed a "variable < variable" annotation -- we could always find a way to make correct code typecheck using other, existing annotations. To keep the number of annotations small, we didn't add this feature when it was not necessary.

The point of this issue is to point out that we may need to expand the set of annotations after all.

[JasonMrX]

I see. I will try the second approach (@ShorterThan and @LongerThan) first proposed by @kelloggm first as I think the qualifiers are more intuitive. Should not be difficult to switch over to the first approach if we think it's better later on.

[JasonMrX]

Hi @kelloggm,

After a closer look at this issue I found that the proposed solutions (either @SameLen with offset or @ShorterThan) is just trying to establish a finer relation between arrays, however, to address issues exposed by this code example, we also need some kind of relation between variables, i.e., the checker should be able to infer that length <= i in order to express the safety of the code.

@SameLen with offset or @ShorterThan should indeed be able to resolve #132 and #43, but could only partially address this issue IMHO.

Jason

[kelloggm]

There are five examples of this problem in plume-lib's Intern.java, where the correctness of the code depends on the fact that a variable start is smaller than a variable end, so subtracting them should produce a non-negative.