[CN] The state file has one state for every element of a function-local array and no way to skip through them

[peterohanley]

int f(void) {
    char line[4096] = {0};
    for (int d = 0; d < 2; ++d)
    /*@ inv d >=0i32; d <= 2i32;
        take l = Owned<char[4096]>(&line);
    @*/
    {
    }

    return 0;
}

% cn very_long_debug_state.c
[1/1]: f
other location (Dune__exe__Check.check_expr.(fun))  warning: good/value_check of array of large size: 4096

very_long_debug_state.c:3:5: error: Missing resource for loop
    for (int d = 0; d < 2; ++d)
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~ 
Resource needed: Owned<char[4096]>(&line)
      very_long_debug_state.c:5:14: (arg l)
  which requires: each(u64 i; (0u64 <= i) && (i < 4096u64 /* 0x1000 */))
{Owned<char>(&line + i * 1u64)}
      other location (Dune__exe__ResourceInference.General.predicate_request)  (arg value)
State file: file:///var/folders/tz/g0kxkm2915xdtm6qgv8rff000000gp/T/state_3d290c.html

In that state file:

first prev next last [4096 / 4107] ...

The states that seem to be initializing the array also do not display a source location, although the ones before and after do.

If the array is not initialized the extra states are not created. Currently it must be initialized due to #254.

It seems likely these states need to be created, but if first prev next last can be changed to do AST-walking with first prevstmt prev next nextstmt last or something like that it would help.

[peterohanley]

Also, the state prints the value of line like this:

each(u64 i; (0u64 <= i) && (i < 256u64 /* 0x100 */)) {Owned<char>(&line + i * 1u64)}((
( ( <around 256 more> (
const(default(u8)) )[0u64 = 0u8] )[1u64 = 0u8] <elided by me, very much present in the actual dump>
[254u64 /* 0xfe */ = 0u8] )[255u64 /* 0xff */ = 0u8])

[dc-mak]

This particular example comes up as inconsistent assumptions because of https://github.com/rems-project/cerberus/pull/385

Do you have an example which shows this without inconsistent assumptions? We can of course check an out earlier version of CN, but this would make it much easier to investigate and add tests.

other location (Dune__exe__Check.check_expr.(fun)) warning: good/value_check of array of large size: 4096

I think this warning was put in because we're aware our current scheme doesn't scale very well but we haven't figured out a better one yet.

[peterohanley]

I haven't been able to get the big state file with minor tweaks to this example. Pass or fail it has a very small number of steps. I initially minified this example from an occurrence in the wild, I'll see if it still happens there.

[peterohanley]

I have another reproduction:

void stack_heap(void)
{
    int stack[4096] = {0};
    /*@ extract Owned<int>, 0u64; @*/
    /*@ assert (false); @*/
}

% cn --version
git-392e19d27 [2024-08-29 11:27:12 -0400]

[dc-mak]