Pointer_offset misuse in value_set_dereference.cpp?

[smowton]

It appears the logic in value_set_dereferencet::build_reference_to can produce incorrect pointer_offset expressions, leading to wrong offsets in array accesses.

Example:

struct java_style_array {
  int length;
  void** data;
}

data will sometimes be treated generically (as void**) and sometimes with a specific type (e.g. struct java.lang.String**.

Array accesses are currently generated using expressions like:

(java.lang.String*)*(array->data + 2) (pretty-printed as array->data[2])

Suppose the symex phase identifies the actual allocation stored in data as dynamic_1_array and the struct as a whole dynamic_object_2. Then in response to this access it will notice (a) the actual-allocation and reference types don't match, so it must use the byte-extract path at value_set_dereference.cpp:585, and (b) the actual referent is dynamic_1_array.

So far so good: we'd like to see it emit something like (java.lang.String*)dynamic_1_array[2] or less optimistically byte_extract(java.lang.String*, 2 * sizeof(java.lang.String*), dynamic_1_array).

Instead of that offset however we get pointer_offset(dynamic_object_2.data + 2). This is incorrect, as it evaluates to pointer_offset(dynamic_object_2.data) + (2 * sizeof(void*)) = 24, producing an off-by-one error indexing the array.

In its most general terms, I think the problem is that the value-set analysis can walk across object boundaries, thus mapping array.data[2] to the underlying allocation for data not array, but the pointer_offset expression built at value_set_dereference.cpp:590 does not take this into account. In this case it needed to follow the recursive walk over the expression performed by value_sett::get_value_set_rec et al and note that since we had:

array -> dynamic_object_2
array->data -> dynamic_1_array
array->data[2] -> dynamic_1_array

...then we need to output dynamic_1_array + 2 rather than what amounts to dynamic_1_array + (&array->data - array) + 2.

My test cases for this are based on my work in progress on Java arrays, so can't be run against master, but I will follow up with a C test-case if I can reproduce the same behaviour there.

[smowton]

Successfully reproduced in C++:

struct java_array {
  int length;
  void** ptrs;
};

struct A {
  int x;
};

extern int nondet();

void test() {

  A** array_init = new A*[2];
  for(int i = 0; i < 2; ++i) {
    array_init[i] = new A();
    array_init[i]->x = nondet();
  }

  java_array* j = new java_array();
  j->length = 2;
  j->ptrs = (void**)array_init;

  assert(!(((A*)j->ptrs[0])->x == 10 &&  ((A*)j->ptrs[1])->x == 20));

}

Running with --program-only reveals key guards (removed switch over possible dynamic objects for readability):

\guard#1 == ((struct A*)byte_extract_little_endian(dynamic_object1#2, POINTER_OFFSET(dynamic_object4#2.ptrs), const void *)->x == 10
tmp_if_expr$5!0@1#2 == ((struct A*)byte_extract_little_endian(dynamic_object1#2, 8l + POINTER_OFFSET(dynamic_object4#2.ptrs), const void *).x == 20

dynamic_object_1 is the A** array while dynamic_object_4 is the java_array object. The POINTER_OFFSET statements will both evaluate to ((char*)&do4.ptrs) - ((char*)&do4) == 8, and thus we erroneously read from offsets 1 and 2 (note the + 8l in the second guard) instead of 0 and 1 as intended.

[smowton]

Suggested workaround: use temporary symbols to avoid expressions that may walk over an object boundary. So use:

void** ptrs = j->ptrs;
A* ptr = (A*)ptrs[1]

This change produces guards with POINTER_OFFSET(ptrs) == 0 as expected.

[smowton]

...but this doesn't reproduce the actual problem. I think while the pointer-offset expression is dubious, we might be getting away with it by using it on both sides of an assignment? For example in the trace I see things like real_array[bad_ptr_offset] = array_of_constants[bad_ptr_offset], where the offset is out of bounds (one past the end of the array in this case) but the trace result is still correct. I only seem to be able to reproduce this in Java when the length of the array is itself nondet. Continuing to investigate...

[smowton]

Amended C++ program:

#include <assert.h>

struct java_array {
  int length;
  void** ptrs;
};

struct A {
  int x;
};

extern int nondet();

void test() {

  int arraylen=nondet();

  A** array_init = new A*[arraylen];
  for(int i = 0; i < arraylen; ++i) {
    array_init[i] = new A();
    array_init[i]->x = nondet();
  }

  java_array* j = new java_array();
  j->length = arraylen;
  j->ptrs = (void**)array_init;

  assert(!(arraylen == 2 && ((A*)j->ptrs[0])->x == 10 && ((A*)j->ptrs[1])->x == 20));

}

Extract from the trace demonstrating a bad solution:

dynamic_object1[0l]=&dynamic_object2.x
dynamic_object2.x=20
dynamic_object1[1l]=&dynamic_object3.x
dynamic_object3.x=10

That is, the true solution (that hits the assert) is { .x=10, .x=20 } and the proposed solution by CBMC is { .x=20, .x=10 }. Note that specifically rotating the array this way doesn't seem to be universal; I have seen examples where it would propose something like { .x=0, .x=10 } instead. The first member appears to be nondeterministic; the second one always has the value expected of the first.

This also persists if we avoid the double-deref expression I suspected above. I tried replacing the assert with:

void** access=j->ptrs;
assert(!(arraylen == 2 && ((A*)access[0])->x == 10 && ((A*)access[1])->x == 20));

In this case CBMC proposed the solution { .x=4, .x=10 }

Finally if we remove all casting (i.e. define java_array with member A** ptrs) then the correct solution is proposed.

The correct solution is also found if we cast the array not the member. So ((A**)ptrs)[1]->x works but ((A*)ptrs[1])->x does not.

[smowton]

To conclude, the dubious pointer-offset use mentioned above is probably worth a glance as the out-of-bounds array accesses it implies may be a problem elsewhere, but don't seem to be causing this particular problem. I'll open a new issue for the true problem if I find it.

[smowton]

Possible hint: accesses involving aliasing result in byte_extract operators, whose flattening at flatten_byte_operators.cpp:102 assumes that the access may stray into the successor element. Thus the byte-extract gets lowered into byte_extract(concat(array[0], array[1]), offset, void*). Remove the ++num_elements at flatten_byte_operators.cpp:102 (and thus assume clean alignment) and the bug disappears.

I don't completely understand the constraints that get introduced in flattening/arrays.cpp, but my current guess is that assertions about these array ops may need to be guarded by the possibility that the alignment was correct. For example, if alignment is good then an array-write operation will overwrite one index and leave the others the same; otherwise it will clobber two.

This suggests a workaround: avoid introducing byte_extract when array members are suitable for a straightforward typecast.

[smowton]

Opened #189 to track the possible byte-extract / array-constraint problem; keeping this one regarding pointer_offset_exprt usage.

[kroening]

Here is a further reduced version, plain C:

#include <assert.h>
#include <stdlib.h>

extern int nondet();

void test() {

  int arraylen=nondet();

  if(arraylen==3)
  {
    int** array_init = malloc(sizeof(int *)*arraylen);

    int a0, a1, a2;

    array_init[0] = &a0;
    array_init[1] = &a1;
    array_init[2] = &a2;

    void **local_array=(void**)array_init;

    int *address=(int *)local_array[0];
    assert(address==&a0);
  }

}

[kroening]

Added as regression/cbmc/Pointer_array5 with 4da8871

[smowton]

Having reviewed flatten_byte_operators.cpp, the only sole transformation turns

byte_extract(void*, dynamic_object1#3, 0) into:

byte_extract(void*, concat(dynamic_object1#3[0], dynamic_object1#3[1]), 0).

This is unnecessary considering the access is aligned, but is correct. Therefore my suspicion lies with the array theory realised in flattening/arrays.cpp.

[kroening]

Please check 7d78d58.