Using IndexFor with a dynamically increasing variable inside a loop

93 views
Skip to first unread message

tazpic...@gmail.com

unread,
Feb 6, 2021, 11:41:25 AM2/6/21
to checker-framework-gsoc
Consider the following code snippet

final Transformer<? super I, ? extends O>[] trs = new Transformer[size];
final Predicate<I>[] preds = new Predicate[size];

int i = 0;
for (final Map.Entry<I, Transformer<I, O>> entry : objectsAndTransformers.entrySet())
{
preds[i] = EqualPredicate.<I>equalPredicate(entry.getKey());
trs[i++] = entry.getValue();
}


When I run the file containing this snippet, I get the following 2 errors

error: [array.access.unsafe.high.range] Potentially unsafe array access: the index could be larger than the array's bound
preds[i] = EqualPredicate.<I>equalPredicate(entry.getKey());
^
index type found: @IntRange(from=-2147483648) int
array type found: @UnknownVal Predicate<I extends @UnknownVal Object> @UnknownVal []
required : index of type @IndexFor("preds") or @LTLengthOf("preds"), or array of type @MinLen(-9223372036854775808)

error: [array.access.unsafe.high.range] Potentially unsafe array access: the index could be larger than the array's bound
trs[i++] = entry.getValue();
^
index type found: @IntRange(from=-2147483648) int
array type found: @UnknownVal Transformer<? extends @UnknownVal Object super I extends @UnknownVal Object, ? extends O extends @UnknownVal Object> @UnknownVal []
required : index of type @IndexFor("trs") or @LTLengthOf("trs"), or array of type @MinLen(-9223372036854775808)


The problem that I’m facing

It is intended to use the same index 'i' for both the arrays ‘preds’ and ‘trs’ and it also has to be dynamically incremented inside the loop to keep the functionality of Java Transformers.


What I have tried

1. I tried annotating the index variable 'i' using IndexFor as follows

final IndexFor({"preds", "trs"}) int i = 0;

But the issue I face here is that, since I've made ‘i’ as final, I won't be able to increment it afterward inside the loop which is necessary here.
If I remove the final and keep the annotation, it gives me 'incompatible types in assignment' errors and I can’t initialize ‘i’ with 0.
Also, I read in the manual that it is not a good practice to annotate local variables unless really needed.

2. I've also tried annotating both the arrays ‘preds’ and ‘trs’ using MinLen but since ‘i’ keeps on incrementing on every iteration and is not a compile-time constant, it doesn't work.

3. I haven't tried to suppress these errors as these are not false positives.


I have tried searching the manual as well but couldn’t find anything that could drive me in the right direction. Any help or tips in the right directione would be very helpful.

Thank you, 
Yash Dekate

Utkarsh Rai

unread,
Feb 7, 2021, 1:50:11 PM2/7/21
to checker-framework-gsoc
Since this is not a false positive and i can become greater than or equal to
size, you can just add a check on i inside your for-each loop.
This program shows no errors when run with the index checker.

public class Dummy {
    public static void main(String [] args) {
        final int size = 10;
        final int[] a = new int[size];
        final int[] b = new int[size];
        int i = 0, j = size-1;
        while(j-- > 0)
        {
            if(i >= size) // remove this check and the same two errors appear.
                break;
            a[i] = 2;
            b[i++] = 3;
        }
    }
}

That being said, I haven't used the Index Checker, but no matter what annotation
you decide to use, I don't see any way of preventing these warnings without
introducing bounds on the value of i.

tazpic...@gmail.com

unread,
Feb 8, 2021, 11:42:52 AM2/8/21
to checker-framework-gsoc
This solved the problem. Thanks alot!
Reply all
Reply to author
Forward
0 new messages