array index off by one

[mgudemann]

This program is verified by CBMC

class incr
{
  int[] nums=new int[]{1,2,3};
  void f(int n)
  {
    if(n==0)
      assert(nums[n++]==2);
  }
  public static void main(String[] args)
  {
    new incr().f(0);
  }
}    

as

[java::incr.f:(I)V.assertion.1] assertion at file incr.java line 7 function java::incr.f:(I)V bytecode_index 13: SUCCESS

but java -ea incr correctly fails

Exception in thread "main" java.lang.AssertionError
	at incr.f(incr.java:7)
	at incr.main(incr.java:13)

the problem is that the array access index in the GOTO program is incremented before the access is done

[mgudemann]

found by @reuk in java/util/ArrayList.java

[mgudemann]

There seems to be a problem with the ?load implementation. In the example the bytecodes in question are

        14: iload_1
        15: iinc          1, 1
        18: iaload

where local variable 1 corresponds to n. This is supposed to 1) put the content of local variable 1 onto the stack 2) increase the local variable 1, and 3) access an array at the index on the stack (in this case the old value of n).

The ?load implementation puts the variable itself in the result (and therefore on the stack) and therefore the increment applies to the access index of the array, too.

[mgudemann]

So this seems to be a slightly more complex problem. In short, on the stack are values of local variables or fields. When the local variable or field is changes, the value of the stack must not change at the same time. The current implementation of ?load pushes the variable instead of its value and getfield / getstatic push a reference to the field.
This can be solved by introducing a temporary variable for each such case, where the temporary variable holds the value of the variable or field at the time of the push.

[mgudemann]

cf. #931

[tautschnig]

This will be addressed by #951.

[tautschnig]

#951 has been merged several months ago.