[CN] constants are not folded in each conditions in the state file

[peterohanley]

Previously: #351 #389

typedef __cerbty_size_t size_t;
typedef signed int int32_t;
typedef unsigned char uint8_t;
typedef unsigned short uint16_t;
void *_malloc(size_t n);
/*@ spec _malloc(u64 n);
    requires true;
    ensures take o = each(u64 i; i >= 0u64 && i < n) {Owned<uint8_t>(array_shift<uint8_t>(return,i))};
@*/

int _read(void* buf, size_t count);
/*@ spec _read(pointer buf, u64 count);
    requires take bufi = each(u64 i; i >= 0u64 && i < count) {Block<uint8_t>(array_shift<uint8_t>(buf,i))};
    ensures
     return >= -1i32 && return <= (i32)count;
     take bufo = each(u64 i; (return == -1i32) ? false : (0u64 <= i && i <(u64)return)) {Owned<uint8_t>(array_shift<uint8_t>(buf, i))};
     take bufb = each(u64 i; (return == -1i32) ? (0u64 <= i && i < count) : ((u64)return <= i && i < count)) {Block<uint8_t>(array_shift<uint8_t>(buf, i))};
@*/

uint16_t any_u16(void);
/*@ spec any_u16();
  requires true;
  ensures true;
@*/

void f(void)
{
    int ret;
    uint16_t data_size = any_u16();
    uint8_t* buf = _malloc(data_size);
    ret = _read(buf, data_size);
    if (ret == data_size) {
        buf + data_size;
    }
}

% cn verify no_simplify.c
[1/1]: f -- fail
no_simplify.c:33:9: error: Pointer `&call__malloc0.return[(u64)call_any_u160.return]` out of bounds
        buf + data_size;
        ~~~~^~~~~~~~~~~ 
(UB missing short message): UB_CERB004_unspecified__pointer_add

I think this should be allowed because it's 1 past the allocation but that's not the actual issue here.

In the state file the condition of the ternaries in the eaches has a value:

Unproven constraint (simplified)

allocs[(alloc_id)&call__malloc0.return[(u64)call_any_u160.return]].base <= (u64)&call__malloc0.return[(u64)call_any_u160.return]
&& (u64)&call__malloc0.return[(u64)call_any_u160.return] <= allocs[(alloc_id)&call__malloc0.return[(u64)call_any_u160.return]].base + allocs[(alloc_id)&call__malloc0.return[(u64)call_any_u160.return]].size

Available Resources

Owned<signed int>(&ret)(call_read_exact0.return)
each(u64 i; call_read_exact0.return == -1'i32 ? 0'u64 <= i && i < (u64)call_any_u160.return : (u64)call_read_exact0.return <= i && i < (u64)call_any_u160.return) {Block<unsigned ichar>(call__malloc0.return + i * 1'u64)}(call_read_exact0.bufb)
each(u64 i; call_read_exact0.return == -1'i32 ? false : 0'u64 <= i && i < (u64)call_read_exact0.return) {Owned<unsigned ichar>(call__malloc0.return + i * 1'u64)}(call_read_exact0.bufo)

Terms

a	b
call_any_u160.return	51200'u16 /* 0xc800 */
(u64)call_any_u160.return	51200'u64 /* 0xc800 */

Constraints

call_read_exact0.return == (i32)call_any_u160.return

This should allow evaluating the ternary resulting in these owned resources:

each(u64 i; (u64)call_any_u160.return <= i && i < (u64)call_any_u160.return) {Block(call__malloc0.return + i * 1'u64)}(call_read_exact0.bufb)
each(u64 i; 0'u64 <= i && i < (u64)call_any_u160.return) {Owned(call__malloc0.return + i * 1'u64)}(call_read_exact0.bufo)

In particular that means the uninitialized resource disappears.