[CN] Difficult to work with multiple multidimensional arrays that share indices

[peterohanley]

This may just be working as intended but it seems surprising. These functions process arrays and access them in the same way, and each works fine isolated but if they're in the same loop body it doesn't work. I thought this should work because the extracts are given different types so they could not interact.

#include <stdint.h>

extern uint8_t three[2][2][2];

void handle_three(void)
/*@
    accesses three;
@*/
{
    for (int c = 0; c < 2; ++c)
    /*@ inv c >= 0i32; c <= 2i32;
    @*/
    {
        for (int s = 0; s < 2; ++s)
        /*@ inv s >= 0i32; s <= 2i32;
            c < 2i32;
            c >= 0i32;
         @*/
        {
            /*@ extract Owned<uint8_t[2][2]>, (u64)c; @*/
            /*@ extract Owned<uint8_t[2]>, (u64)s; @*/
            /*@ extract Owned<uint8_t>, 0u64; @*/
            /*@ extract Owned<uint8_t>, 1u64; @*/

            three[c][s][0] = 0;
            three[c][s][1] = 0;
        }
    }
}

extern uint8_t two[2][2];

void handle_two(void)
/*@
    accesses two;
@*/
{
    for (int c = 0; c < 2; ++c)
    /*@ inv c >= 0i32; c <= 2i32;
     @*/
    {
        for (int s = 0; s < 2; ++s)
        /*@ inv s >= 0i32; s <= 2i32;
                c < 2i32;
                c >= 0i32;
        @*/
        {
            /*@ extract Owned<uint8_t[2]>, (u64)c; @*/
            /*@ extract Owned<uint8_t>, (u64)s; @*/

            two[c][s] = 0;
        }
    }
}
void handle_both(void)
/*@
    accesses two;
    accesses three;
@*/
{
    for (int c = 0; c < 2; ++c)
    /*@ inv c >= 0i32; c <= 2i32;
    @*/
    {
        for (int s = 0; s < 2; ++s)
        /*@ inv s >= 0i32; s <= 2i32;
            c < 2i32;
            c >= 0i32;
         @*/
        {
            // either block is ok by itself but if both are in it fails
            /*@ extract Owned<uint8_t[2]>, (u64)c; @*/
            /*@ extract Owned<uint8_t>, (u64)s; @*/
            two[c][s] = 0;

            /*@ extract Owned<uint8_t[2][2]>, (u64)c; @*/
            /*@ extract Owned<uint8_t[2]>, (u64)s; @*/
            /*@ extract Owned<uint8_t>, 0u64; @*/
            /*@ extract Owned<uint8_t>, 1u64; @*/
            three[c][s][0] = 0;
            three[c][s][1] = 0;
        }
    }
}

[dc-mak]

Potentially related #320, #311, #256

[cp526]

Here's a version that works.

void handle_both(void)
/*@
    accesses two;
    accesses three;
@*/
{
    for (int c = 0; c < 2; ++c)
    /*@ inv c >= 0i32; c <= 2i32;
    @*/
    {
        for (int s = 0; s < 2; ++s)
        /*@ inv s >= 0i32; s <= 2i32;
            c < 2i32;
            c >= 0i32;
         @*/
        {
            // either block is ok by itself but if both are in it fails
            /*@ extract Owned<uint8_t[2]>, (u64)c; @*/
            /*@ extract Owned<uint8_t>, (u64)s; @*/
            two[c][s] = 0;

            /*@ extract Owned<uint8_t[2][2]>, (u64)c; @*/
            /*@ extract Owned<uint8_t[2]>, (u64)s; @*/
            /*@ extract Owned<uint8_t>, 0u64; @*/
            /*@ extract Owned<uint8_t>, 1u64; @*/
            /*@ split_case (c == s); @*/
            /*@ split_case (s == 0i32); @*/
            three[c][s][0] = 0;
            three[c][s][1] = 0;
        }
    }
}

(note the split_case instructions).

The trigger for this problem seems to indeed be interference between different extract's. The upper extract's are meant to affect only two, the lower ones only three, but because extract only takes the resource type and the index as arguments (not the array base pointer), they have this unintended "side effect" here. In this instance this would be addressed by https://github.com/rems-project/cerberus/issues/311 .

What's happening here is maybe easiest illustrated with this example:

extern int arr[10];

void f (unsigned long i, unsigned long j)
/*@ accesses arr;
    requires i < 10u64;
             j < 10u64; 
@*/
{
  /*@ extract Owned<int>, i; @*/
  /*@ extract Owned<int>, j; @*/
  arr[i];
  arr[j];
}

As-is, CN rejects this:

17:53 % cn verify ~/Desktop/extract-problem.c
/Users/christopher/Desktop/extract-problem.c:10:7: warning: extract: index added, no resources (yet) extracted.
  /*@ extract Owned<int>, j; @*/
      ^~~~~~~~~~~~~~~~~~~~~~
[1/1]: f -- fail
/Users/christopher/Desktop/extract-problem.c:12:3: error: Missing resource for reading
  arr[j];
  ^~~~~~
Resource needed: Owned<signed int>(&(&&arr[(u64)0'i32])[j])

The precondition ensures that i and j are valid array indices, but CN cannot tell whether they are equal or distinct. The first extract moves ownership for i out of the each, but for the second one, CN can't prove that ownership for j is available to be extracted, because it does not know how i and j relate. (We have to somehow make CN better explain this error.)

Adding a /*@ split_case (i == j); @*/ before the array accesses fixes the problem by analysing both situations (i == j and i != j) separately, and in both cases the required ownership can be obtained.

Going back to the nested array example, this adds split_case for any pair of indices for which there's previous extract statements at the same C-type. First pair: /*@ extract Owned<uint8_t[2]>, (u64)c; @*/ and /*@ extract Owned<uint8_t[2]>, (u64)s; @*/ Second pair: /*@ extract Owned<uint8_t>, (u64)s; @*/ and /*@ extract Owned<uint8_t>, 0u64; @*/.

In principle there's also a third pair, which is the same as the second but with 1u64. That doesn't need another case split because s can only be either 0 or 1, so the previous split already handles that.

We should do https://github.com/rems-project/cerberus/issues/311, or avoid the need for extract altogether, if possible, to make this less of a problem.

[dc-mak]

Can I close this because #311 exists?

[septract]

Noting that @lwli11 at BAE experienced an instance of this issue.