__CPROVER_array_replace updates the wrong addresses

[remi-delmas-3000]

cbmc 5.62.0 (cbmc-5.62.0-41-g4680c5f48c-dirty)

Here is the spec for the operations that I reverse engineered from comments and code:

__CPROVER_array_set(dest, value) overwrites all of *dest using the given value. So it should update size bytes starting from dest where size is computed as follows:

ssize_t size =
    __CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest);

__CPROVER_array_copy(dest, ...) overwrites all of *dest (possibly using nondet values), even when *src is smaller. So it should update update size bytes starting from dest where size is computed as follows:

ssize_t size = 
     __CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest);

__CPROVER_array_replace(dest, src) replaces at most size-of-*src bytes in *dest. So it should update size bytes in the destination where size is defined as follows:

ssize_t src_size =
    __CPROVER_OBJECT_SIZE(src) - __CPROVER_POINTER_OFFSET(src);
ssize_t dest_size =
    __CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest);
ssize_t size = dest_size < src_size ? dest_size : src_size;

However, as shown in the example below it seems that the start address that actually gets used to perform the update can be some amount of bytes before dest.

It seems like an unexpected behaviour. (The same is observed with __CPROVER_array_copy and __CPROVER_array_set).

In this example we try to update 3 bytes starting at address &(arr[1].c[2]), which corresponds to an array embedded in a struct, the struct being itself embedded in an array of structs.

The update seems to start at &(arr[1]) in the array of structs instead of the expected &(arr[1].c[2]):

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

typedef struct my_struct {
  char a;
  char b;
  char c[5];
} my_struct;

int main() {
  my_struct arr[3] = {0};
  char *ptr = &(arr[1].c[2]);
  char nondet[3];

  __CPROVER_array_replace(ptr, &nondet[0]);

    // expected valid and proved
  assert(arr[0].a == 0);
  assert(arr[0].b == 0);
  assert(arr[0].c[0] == 0);
  assert(arr[0].c[1] == 0);
  assert(arr[0].c[2] == 0);
  assert(arr[0].c[3] == 0);
  assert(arr[0].c[4] == 0);

  assert(arr[1].a == 0);      // expected valid, falsified
  assert(arr[1].b == 0);      // expected valid, falsified
  assert(arr[1].c[0] == 0); // expected valid, falsified
  assert(arr[1].c[1] == 0); // expected valid, proved
  assert(arr[1].c[2] == 0); // expected falsifiable, proved  
  assert(arr[1].c[3] == 0); // expected falsifiable, proved
  assert(arr[1].c[4] == 0); // expected falsifiable, proved

    // expected valid and proved
  assert(arr[2].a == 0);
  assert(arr[2].b == 0);
  assert(arr[2].c[0] == 0);
  assert(arr[2].c[1] == 0);
  assert(arr[2].c[2] == 0);
  assert(arr[2].c[3] == 0);
  assert(arr[2].c[4] == 0);

  return 0;
}

results in this:

** Results:
array_replace_bug.c function main
[main.assertion.1] line 18 assertion arr[0].a == 0: SUCCESS
[main.assertion.2] line 19 assertion arr[0].b == 0: SUCCESS
[main.assertion.3] line 20 assertion arr[0].c[0] == 0: SUCCESS
[main.assertion.4] line 21 assertion arr[0].c[1] == 0: SUCCESS
[main.assertion.5] line 22 assertion arr[0].c[2] == 0: SUCCESS
[main.assertion.6] line 23 assertion arr[0].c[3] == 0: SUCCESS
[main.assertion.7] line 24 assertion arr[0].c[4] == 0: SUCCESS
[main.assertion.8] line 26 assertion arr[1].a == 0: FAILURE
[main.assertion.9] line 27 assertion arr[1].b == 0: FAILURE
[main.assertion.10] line 28 assertion arr[1].c[0] == 0: FAILURE
[main.assertion.11] line 29 assertion arr[1].c[1] == 0: SUCCESS
[main.assertion.12] line 30 assertion arr[1].c[2] == 0: SUCCESS
[main.assertion.13] line 31 assertion arr[1].c[3] == 0: SUCCESS
[main.assertion.14] line 32 assertion arr[1].c[4] == 0: SUCCESS
[main.assertion.15] line 35 assertion arr[2].a == 0: SUCCESS
[main.assertion.16] line 36 assertion arr[2].b == 0: SUCCESS
[main.assertion.17] line 37 assertion arr[2].c[0] == 0: SUCCESS
[main.assertion.18] line 38 assertion arr[2].c[1] == 0: SUCCESS
[main.assertion.19] line 39 assertion arr[2].c[2] == 0: SUCCESS
[main.assertion.20] line 40 assertion arr[2].c[3] == 0: SUCCESS
[main.assertion.21] line 41 assertion arr[2].c[4] == 0: SUCCESS

** 3 of 21 failed (2 iterations)
VERIFICATION FAILED

If we implement __CPROVER_array_replace as follows:

/// what __CPROVER_array_replace is meant to do
void my_array_replace(void *dest, void *src) {
  __CPROVER_ssize_t src_size =
      __CPROVER_OBJECT_SIZE(src) - __CPROVER_POINTER_OFFSET(src);
  __CPROVER_ssize_t dest_size =
      __CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest);
  __CPROVER_ssize_t size = dest_size < src_size ? dest_size : src_size;
  char *csrc = src;
  char *cdest = dest;
  __CPROVER_ssize_t i = 0;
  while (i < size) {
    *(cdest) = *(csrc);
    cdest++;
    csrc++;
    i++;
  }
}

We get the expected results:

** Results:
array_replace_bug.c function main
[main.assertion.1] line 31 assertion arr[0].a == 0: SUCCESS
[main.assertion.2] line 32 assertion arr[0].b == 0: SUCCESS
[main.assertion.3] line 33 assertion arr[0].c[0] == 0: SUCCESS
[main.assertion.4] line 34 assertion arr[0].c[1] == 0: SUCCESS
[main.assertion.5] line 35 assertion arr[0].c[2] == 0: SUCCESS
[main.assertion.6] line 36 assertion arr[0].c[3] == 0: SUCCESS
[main.assertion.7] line 37 assertion arr[0].c[4] == 0: SUCCESS
[main.assertion.8] line 39 assertion arr[1].a == 0: SUCCESS
[main.assertion.9] line 40 assertion arr[1].b == 0: SUCCESS
[main.assertion.10] line 41 assertion arr[1].c[0] == 0: SUCCESS
[main.assertion.11] line 42 assertion arr[1].c[1] == 0: SUCCESS
[main.assertion.12] line 43 assertion arr[1].c[2] == 0: FAILURE
[main.assertion.13] line 44 assertion arr[1].c[3] == 0: FAILURE
[main.assertion.14] line 45 assertion arr[1].c[4] == 0: FAILURE
[main.assertion.15] line 48 assertion arr[2].a == 0: SUCCESS
[main.assertion.16] line 49 assertion arr[2].b == 0: SUCCESS
[main.assertion.17] line 50 assertion arr[2].c[0] == 0: SUCCESS
[main.assertion.18] line 51 assertion arr[2].c[1] == 0: SUCCESS
[main.assertion.19] line 52 assertion arr[2].c[2] == 0: SUCCESS
[main.assertion.20] line 53 assertion arr[2].c[3] == 0: SUCCESS
[main.assertion.21] line 54 assertion arr[2].c[4] == 0: SUCCESS

** 3 of 21 failed (2 iterations)
VERIFICATION FAILED

Last,
the problem does not occur if the struct is declared as its own object

int main() {
  my_struct s = {0};
  char nondet[3];
  __CPROVER_array_replace(&(s.c[2]), &nondet[0]);
  assert(s.a == 0);
  assert(s.b == 0);
  assert(s.c[0] == 0);
  assert(s.c[1] == 0);
  assert(s.c[2] == 0);
  assert(s.c[3] == 0);
  assert(s.c[4] == 0);
  return 0;
}

We get the expected results:

** Results:
array_replace_bug.c function main
[main.assertion.1] line 67 assertion s.a == 0: SUCCESS
[main.assertion.2] line 68 assertion s.b == 0: SUCCESS
[main.assertion.3] line 69 assertion s.c[0] == 0: SUCCESS
[main.assertion.4] line 70 assertion s.c[1] == 0: SUCCESS
[main.assertion.5] line 71 assertion s.c[2] == 0: FAILURE
[main.assertion.6] line 72 assertion s.c[3] == 0: FAILURE
[main.assertion.7] line 73 assertion s.c[4] == 0: FAILURE

** 3 of 7 failed (2 iterations)
VERIFICATION FAILED

The problem also disappears if the array is heap allocated and not stack allocated

int main() {
  my_struct *arr = calloc(3, sizeof(*arr));
  char nondet[3];
  __CPROVER_array_replace(&(arr[1].c[2]), &nondet[0]);
  assert(arr[1].a == 0);
  assert(arr[1].b == 0);
  assert(arr[1].c[0] == 0);
  assert(arr[1].c[1] == 0);
  assert(arr[1].c[2] == 0);
  assert(arr[1].c[3] == 0);
  assert(arr[1].c[4] == 0);
  return 0;
}

we get the expected results

array_replace_bug.c function main
[main.assertion.1] line 81 assertion arr[1].a == 0: SUCCESS
[main.assertion.2] line 82 assertion arr[1].b == 0: SUCCESS
[main.assertion.3] line 83 assertion arr[1].c[0] == 0: SUCCESS
[main.assertion.4] line 84 assertion arr[1].c[1] == 0: SUCCESS
[main.assertion.5] line 85 assertion arr[1].c[2] == 0: FAILURE
[main.assertion.6] line 86 assertion arr[1].c[3] == 0: FAILURE
[main.assertion.7] line 87 assertion arr[1].c[4] == 0: FAILURE

** 3 of 9 failed (2 iterations)
VERIFICATION FAILED

[tautschnig]

The problem here is that the assignment to ptr is rewritten into pointer arithmetic over arr (ptr!0@1#2 == (char *)arr!0@1 + 11l), which is not something that process_array_expr is ready to deal with. We'd need to teach the latter to look at the offset properly and check whether that's within a nested array.

[TGWDB]

Assigning this to @tautschnig since he has a PR to fix it. Please remove if this assignment is unreasonable.