__CPROVER_forall fails when dealing with flattening of nested structure

[hanno-becker]

I'm observing unexpected behaviour when trying to use __CPROVER_forall to access the fields of a nested array structure when cast as a flat array of cells. cc @tautschnig @remi-delmas-3000

Minimal example:

/* instructions

foo:
	goto-cc harness.c --function foo_harness -o a.out
	goto-instrument --dfcc foo_harness --enforce-contract foo a.out b.out
	cbmc b.out --bitwuzla
*/

#include <stdint.h>

typedef struct __attribute__((packed)) {
    int data[2];
} arr;

typedef struct __attribute__((packed)) {
    arr vec[2];
} arrvec;

void foo(arrvec *x)
  __CPROVER_requires(__CPROVER_is_fresh(x, sizeof(arrvec)))
  __CPROVER_requires(x->vec[1].data[0] < 42)
{
    // OK:
    __CPROVER_assert(((int*)x)[2] < 42, "");
    // NOT OK:
    __CPROVER_assert(__CPROVER_forall {unsigned k; k == 2 ==> ((int*)x)[k] < 42}, "");
    // OK:
    __CPROVER_assert(__CPROVER_forall {unsigned k; k == 2 ==> ((int (*)[2])x)[k/2][k % 2] < 42}, "");
}

void foo_harness(void) {
    arr *x;
    foo(x);
}

[tautschnig]

Taking a look. Here is a simplified version that equally fails and neither uses contracts nor requires the use of an SMT solver - cbmc harness.c will do:

typedef struct __attribute__((packed)) {
    int data[2];
} arr;

typedef struct __attribute__((packed)) {
    arr vec[2];
} arrvec;

int main() {
    arrvec A;
    arrvec *x = &A;
    __CPROVER_assume(x->vec[1].data[0] < 42);
    // OK:
    __CPROVER_assert(((int*)x)[2] < 42, "");
    // NOT OK:
    __CPROVER_assert(__CPROVER_forall {unsigned k; k == 2 ==> ((int*)x)[k] < 42}, "");
    // OK:
    __CPROVER_assert(__CPROVER_forall {unsigned k; k == 2 ==> ((int (*)[2])x)[k/2][k % 2] < 42}, "");
}

[tautschnig]

Turns out this isn't a problem related to quantifiers. The following further simplification (still equivalent to the original one) also fails:

typedef struct __attribute__((packed)) {
    int data[2];
} arr;

typedef struct __attribute__((packed)) {
    arr vec[2];
} arrvec;

int main() {
    arrvec A;
    arrvec *x = &A;
    __CPROVER_assume(x->vec[1].data[0] < 42);
    unsigned k;
    __CPROVER_assert(k != 2 || ((int*)x)[k] < 42, "");
}

It seems the problem is with field sensitivity during symbolic execution, where we appear to (spuriously) turn ((int*)x)k effectively into A.vec[0].data[k].