Description
Fixed this already; skip to the bottom for the fix.
Example from https://github.com/diffblue/verification-engine-utils/issues/216
The following test-case fails with --no-propagation, even though Java initialises the array with null members:
public class test {
static test readback;
public static void main(int c) {
// a must be a VLA (new test[1] works)
// The read must happen via a temporary intermediate (assert(a[0]==null) works)
if(c!=1) return;
test[] a = new test[c];
readback=a[0];
assert(readback==null);
}
}Cause: the array-read expression is:
test.readback#2 == (struct test { struct java.lang.Object { __CPROVER_string @class_identifier; _Bool @lock; } @java.lang.Object; } *)dynamic_2_array#4[0l]
And the array initialisation is:
dynamic_2_array#1 == dynamic_2_array#0 WITH [(8l * (signed long int)tmp_index$2!0@1#2 + POINTER_OFFSET(dynamic_object1#2.data)) / 8l:=NULL]
These are textually different; it's up to the array-numbering pass to relate them by converting each index expression to a fresh variable and generating equality constraints. It generates constraints like x == y ==> arr[x] == arr[y] for every index x and y present in the program.
Every time an array-indexing expression is compiled a fresh variable is generated, and we rely on the conversion cache to pair them up. For example, the use of dynamic_2_array#4[0l] in the actual VCC should make a fresh variable (or rather a vector of booleans), then the array logic should re-use them every time it refers to the same expression, or vice versa.
Unfortunately for the particular case where an array expression is typecast, converting the expression (A*)x[y] checks the cache for (A*)x[y] but then recursively calls bv_pointerst::convert_pointer_type(x[y]) without re-checking the cache. Thus (A*)x[y] and x[y] generate independent fresh variables, the constraints generated by the array-numbering pass only catch x[y] and (A*)x[y] is left a dangling nondet.
There are probably more cases in there where the cache is accidentally bypassed like this. If the intent is that an expression referred to by the array logic must always have been compiled elsewhere then it should probably assert that it is in the cache. In the meantime I'll submit a PR for this particular case.