[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.