[CN] iterating over multidimensional arrays in inconvenient order is difficult

[peterohanley]

This is probably related to #357 and #320.

#include <stdint.h>
void explode_block(uint8_t *t);
/*$ spec explode_block(pointer t);
    requires take ti = Block<uint8_t[8][4]>(t);

    ensures take to = each(u64 j; j < (u64)(4u64*8u64)) {Block<uint8_t>(array_shift<uint8_t>(t, j))};
$*/
void implode_owned(uint8_t *t);
/*$ spec implode_owned(pointer t);
    requires take to = each(u64 j; j < (u64)(4u64*8u64)) {Owned<uint8_t>(array_shift<uint8_t>(t, j))};
    ensures take ti = Owned<uint8_t[8][4]>(t);
$*/
static void
f(uint8_t test[8][4])
/*$
  requires take ttestin = each(u64 i; i < 8u64) {Block<uint8_t[4]>(array_shift(test, i))};
  ensures take ttestout = each(u64 i; i < 8u64) {Owned<uint8_t[4]>(array_shift(test, i))};
$*/
{
    explode_block((uint8_t*)test);
    for (int i = 0; i < 4; ++i)
    /*$ inv 0i32 <= i; i <= 4i32;

        take testinvlo = each(u64 j; j < (u64)(4u64*8u64) && mod_uf(j, 4u64) < (u64)i) {Owned<uint8_t>(array_shift<uint8_t>(test, j))};
        take testinvhi = each(u64 j; j < (u64)(4u64*8u64) && mod_uf(j, 4u64) >= (u64)i) {Block<uint8_t>(array_shift<uint8_t>(test, j))};

        {test} unchanged;
    $*/
    {
        for(int c = 0; c < 8; ++c)
        /*$ inv 0i32 <= c; c <= 3i32;
            0i32 <= i; i < 4i32;

            take testinvlo = each(u64 j; j < (u64)(4u64*8u64) && mod_uf(j , 4u64) < (u64)i) {Owned<uint8_t>(array_shift<uint8_t>(test, j))};
            take testinvhi = each(u64 j; j < (u64)(4u64*8u64) && mod_uf(j , 4u64) > (u64)i) {Block<uint8_t>(array_shift<uint8_t>(test, j))};

            take testinvcurlo = each(u64 j; j < (u64)(4u64*8u64) && mod_uf(j , 4u64) == (u64)i && (j/ 8u64) < (u64)c) {Owned<uint8_t>(array_shift<uint8_t>(test, j))};
            take testinvcurhi = each(u64 j; j < (u64)(4u64*8u64) && mod_uf(j , 4u64) == (u64)i && (j/ 8u64) >= (u64)c) {Block<uint8_t>(array_shift<uint8_t>(test, j))};
            {test} unchanged;
        $*/
        {
            /*$ extract Block<uint8_t>, (u64)i + (u64)(c*4i32); $*/
            /*$ extract Owned<uint8_t>, (u64)i + (u64)(c*4i32); $*/
            test[c][i] = i;
        }
    }

    implode_owned((uint8_t*)test);
}

The idea of this code is to convert the nested arrays to a single array over all indices, use the each predicates to recover multidimensional array indexing, and express the block/owned predicates on the multidimensional arrays as directly as possible. The loops have a lot of invariants but they are just walking the array in the inconvenient order.

% cn --magic-comment-char-dollar array_init_mwe.c
[1/1]: f
array_init_mwe.c:48:5: error: Missing resource for calling function implode_owned
    implode_owned((uint8_t*)test);
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
Resource needed: each(u64 j; j < (4u64 * 8u64))
{Owned<unsigned ichar>(test + j * 1u64)}
      array_init_mwe.c:10:19: (arg to)
Consider the state in ...

That state looks like this (one step before the last):

Requested resource

each(u64 j; j < (4u64 * 8u64)) {Owned<unsigned ichar>(test + j * 1u64)}

Available resources

each(u64 j; (j < (4u64 * 8u64)) && ((mod_uf(j, 4u64)) < ((u64)O_i0))) {Owned<unsigned ichar>(test + j * 1u64)}(testinvlo) (same type)
each(u64 j; (j < (4u64 * 8u64)) && (((u64)O_i0) <= (mod_uf(j, 4u64)))) {Block<unsigned ichar>(test + j * 1u64)}(testinvhi)
Owned<unsigned ichar[4]*>(&test)(test)

Terms

variable    value
__cn_alloc_history  const({ .base = 0, .len = 0 })
ttestin const(const(0u8))
testinvlo   const(0u8)
testinvhi   const(0u8)
O_i0    4i32
j   0u64
4u64 * 8u64 32u64 /* 0x20 */

Constraints

true
!(!(!(!(!(O_i0 < 4i32)))))
0i32 <= O_i0
O_i0 <= 4i32
O_test0 == test
aligned(test, 1u64)

Substituting in the known value of O_i0 the Owned predicate matches and the Block predicate is empty, but instead there is another step and the Owned predicate is gone but it's still requested. This might just be a problem with mod_uf (used due to #231) but I'm also not clear on why it just vanished without satisfying the request.

[peterohanley]

Also, I haven't been able to actually write an implode and explode function, but they should be amenable to a lemma. They can be generic over the size but not the type or predicate atm which is sufficient.

[dc-mak]

@cp526 Can you triage this?

[dc-mak]

@cp526 Reminder

[cp526]

I put this under priority asap, but if this is blocking you, @peterohanley , we should record that and make it more urgent.

[dc-mak]

Related to #357, #320, #311, #256