[CN] Hang when passing pointer to struct with multiple array elements

[peterohanley]

struct struc {
  int a[1];
  #ifdef GO_SLOW
  int b[1];
  #endif
};

int g(struct struc *p);
/*@ spec g(pointer p);
  requires take pi = Owned<struct struc>(p);
  ensures take po = Owned<struct struc>(p);
@*/

void f(struct struc *p);
/*@ spec f(pointer p);
  requires take pi = each(u64 j; j < 2u64) {Owned<struct struc>(array_shift<struct struc>(p,j))};
  ensures take po = each(u64 j; j < 2u64) {Owned<struct struc>(array_shift<struct struc>(p,j))};
@*/

void f(struct struc *p)
{
  /*@ extract Owned<struct struc>, 0u64; @*/
  g(&p[0]);
}

% cn --version
git-13c264c52 [2024-10-06 19:32:33 +0100]

With one element it finishes quickly.

% time cn verify super_long.c          
[1/1]: f -- pass
cn verify super_long.c  0.04s user 0.03s system 13% cpu 0.500 total

% time cn verify -DGO_SLOW super_long.c

At least three minutes, I'll update if it ever finishes. I suspect this is a hang.

[peterohanley]

This feels like #399 to me

[peterohanley]

It spun for 9 hours and I finally killed it.

The last output with -p 30 is

context resources
resources:
each(u64 i; 0'u64 <= i && i < 1'u64)
{Owned<signed int>(&(&p[8'u64 * 0'u64])->a + i * 4'u64)}(pi[0'u64].a),
each(u64 i; 0'u64 <= i && i < 1'u64)
{Owned<signed int>(&(&p[8'u64 * 0'u64])->b + i * 4'u64)}(pi[0'u64].b),
Owned<struct struc*>(&ARG0)(p), Alloc(&ARG0)(allocs[(alloc_id)&ARG0])
...
[0.051474] resource was not found
[0.051613] attempting to pack compound resource:
take value = each(u64 i; 0'u64 <= i && i < 1'u64) {Owned<signed int>(&p->b + i * 4'u64)}; resource
[0.051626] Cn__ResourceInference.General.qpredicate_request_aux:
each(u64 i; 0'u64 <= i && i < 1'u64)
{Owned<signed int>(&p->b + i * 4'u64)}
<nothing further...>

These are the relevant resources

{Owned<signed int>(&(&p[8'u64 * 0'u64])->a + i * 4'u64)}(pi[0'u64].a),
{Owned<signed int>(&(&p[8'u64 * 0'u64])->b + i * 4'u64)}(pi[0'u64].b), <-- b
{Owned<signed int>(&p->b + i * 4'u64)} <-- goal

If we simplify multiplication and &p[0] -> p these are equal syntactically so this looks fine to me.

Here it is from the working case:

resources:
each(u64 i; 0'u64 <= i && i < 1'u64)
{Owned<signed int>(&(&p[4'u64 * 0'u64])->a + i * 4'u64)}(pi[0'u64].a),
...
[0.054471] attempting to pack compound resource:
take value = each(u64 i; 0'u64 <= i && i < 1'u64) {Owned<signed int>(&p->a + i * 4'u64)}; resource
[0.054544] Cn__ResourceInference.General.qpredicate_request_aux:
each(u64 i; 0'u64 <= i && i < 1'u64)
{Owned<signed int>(&p->a + i * 4'u64)}
[0.054680] used resource:
each(u64 i; 0'u64 <= i && i < 1'u64)
{Owned<signed int>(&(&p[4'u64 * 0'u64])->a + i * 4'u64)}
....

It looks the same so I am at the limit of black box investigation.

[peterohanley]

Here is the problem:

[0.049348] Cn__ResourceInference.General.predicate_request: <-- need a struc
Owned<struct struc>(p)
[0.049354] resource was not found
[0.049362] attempting to pack compound resource: <- need to grab the parts
take a = Owned<signed int[1]>(&p->a); take b = Owned<signed int[1]>(&p->b); resource
[0.049369] Cn__ResourceInference.General.predicate_request:
Owned<signed int[1]>(&p->a)
[0.049373] resource was not found
[0.049381] attempting to pack compound resource: <-- need to find an exploded array
take value = each(u64 i; 0'u64 <= i && i < 1'u64) {Owned<signed int>(&p->a + i * 4'u64)}; resource
[0.049392] Cn__ResourceInference.General.qpredicate_request_aux: <-- ask for p->a resource
each(u64 i; 0'u64 <= i && i < 1'u64)
{Owned<signed int>(&p->a + i * 4'u64)}
[0.049559] couldn't use q-resource: <-- can't use p->b
each(u64 i; 0'u64 <= i && i < 1'u64)
{Owned<signed int>(&(&p[8'u64 * 0'u64])->b + i * 4'u64)}
[0.049569] counterexample, expanding:
&p->a == &(&p[8'u64 * 0'u64])->b
[0.049771] /* {@2; 0x1000000087fffff8} */&/* {@2; 0x1000000087fffff8} */p->a
== /* {@2; 0x1000000087fffffc} */&/* {@2; 0x1000000087fffff8} */(
  &/* {@2; 0x1000000087fffff8} */p[/* 0'u64 *//* 8'u64 */8'u64 * /* 0'u64 */0'u64]
)->b
[0.049942] used resource: <-- but can use p->a
each(u64 i; 0'u64 <= i && i < 1'u64)
{Owned<signed int>(&(&p[8'u64 * 0'u64])->a + i * 4'u64)}
[0.050017] checking resource remainder:
forall(i, u64). !(0'u64 <= i && i < 1'u64 && !(0'u64 <= i && i < 1'u64))
[0.050080] Cn__ResourceInference.General.predicate_request:
Owned<signed int[1]>(&p->b)
[0.050087] resource was not found
[0.050231] attempting to pack compound resource: <-- need exploded array again
take value = each(u64 i; 0'u64 <= i && i < 1'u64) {Owned<signed int>(&p->b + i * 4'u64)}; resource
[0.050242] Cn__ResourceInference.General.qpredicate_request_aux: <-- ask for p->b resource
each(u64 i; 0'u64 <= i && i < 1'u64)
{Owned<signed int>(&p->b + i * 4'u64)}
... <-- apparently we do *not* consider p->b this time, nor do we fail, just spin

Is it possible that the search for struct elements is consuming rejected resources instead of restoring them to the context? That would explain this pattern.

[cp526]

This seems to be a performance bug in z3. When I run this with cvc5 it finishes instantly:

12:59 % time cn verify --solver-type cvc5 ~/Desktop/array-problem.c
[1/1]: f -- pass
cn verify --solver-type cvc5 ~/Desktop/array-problem.c  0.07s user 0.04s system 14% cpu 0.809 total

[cp526]

Something odd is happening with z3. Setting "sat.smt=true" to improve performance results in a verification failure (where the same C code passes using cvc5:

14:28 % cn verify --solver-type z3 ~/Desktop/array-problem.c
[1/1]: f -- fail
/Users/christopher/Desktop/array-problem.c:20:5: error: `&p[(u64)0'i32]` out of bounds
  g(&p[0]);
    ^~~~~
(UB missing short message): UB_CERB004_unspecified__pointer_add
State file: file:///var/folders/_v/ndl32wpj4bb3y9dg11rvc8ph0000gn/T/state__array-problem.c__f.html
14:28 %
14:28 % cn verify --solver-type cvc5 ~/Desktop/array-problem.c
[1/1]: f -- pass

for array-problem.c:

struct s {
  int a[1];
  int b[1];
};

int g(struct s *p);
/*@ spec g(pointer p);
  requires take pi = Owned<struct s>(p);
  ensures take po = Owned<struct s>(p);
@*/

void f(struct s *p)
/*@
  requires take pi = each(u64 j; j < 2u64) {Owned<struct s>(array_shift<struct s>(p,j))};
  ensures take po = each(u64 j; j < 2u64) {Owned<struct s>(array_shift<struct s>(p,j))};
@*/
{
  /*@ extract Owned<struct s>, 0u64; @*/
  //assert(0);
  g(&p[0]);
}

[cp526]

z3 bug filed: Z3Prover/z3#7438

[cp526]

Fixed in current build Z3Prover/z3#7438 (comment) , so we can switch on sat.smt=true when that next makes it into a z3 release.