Pointer validity checks on `__CPROVER_allocated_memory`

[SaswatPadhi]

CBMC version: 3410558
Operating system: Linux, MacOS

Test case:

int main() {
    char *ptr;

    ptr = 0xFF;
    *ptr = '0';                                           // PASS: write succeeds without alloc?
    __CPROVER_allocated_memory(ptr, 0xFFFFFFFFFFFFFE);    // PASS: but overflow in offset space!
         assert(__CPROVER_w_ok(ptr, 0xFFFFFFFFFFFFFE));   // PASS: well, consistent with above
         assert(__CPROVER_w_ok(ptr, 0xFFFFFFFFFFFFFF00)); // FAIL: beyond alloc
         assert(__CPROVER_w_ok(ptr, 0xFFFFFFFFFFFFFF01)); // PASS: overflow beyond 64 bits!

    ptr = 0xFFFFFFFFFFFFFE;    // object bits unset
    *ptr = '0';                                   // PASS: write succeeds without alloc?
    __CPROVER_allocated_memory(ptr, 0xFF);        // PASS: but overflow in offset space!
         assert(__CPROVER_w_ok(ptr, 0xFF));       // PASS: well, consistent with above
         assert(__CPROVER_w_ok(ptr, 0xFFFF));     // PASS: but beyond alloc!
    
    ptr = 0xFFFFFFFFFFFFFFE;   // object bits set to 00001111
    *ptr = '0';                                   // PASS: write succeeds without alloc?
    __CPROVER_allocated_memory(ptr, 0xFF);        // PASS: but overflow in offset space!
         assert(__CPROVER_w_ok(ptr, 0xFF));       // PASS: well, consistent with above
         assert(__CPROVER_w_ok(ptr, 0xFFFF));     // PASS: but beyond alloc!
    
    assert(0);
}

Exact command line resulting in the issue:

cbmc --64 \
     --pointer-check --pointer-overflow-check --pointer-primitive-check \
     --signed-overflow-check --unsigned-overflow-check --conversion-check \
     --bounds-check \
     test.c

What behaviour did you expect:

I was expecting CBMC to flag the w_ok checks on regions beyond the allocated region.

I think there are at least 3 different issues here:

1. @tautschnig pointed out on Slack that __CPROVER_allocated_memory is flow insensitive. I think that explains why the before alloc succeed in the test case above
2. The __CPROVER_allocated_memory addresses break the (object id, offset) model for pointers. CBMC doesn't raise overflows on large allocations (overflowing into object bits) there, which matches my intuition, but I am not sure if it's for the right reasons. It looks like arithmetic on these pointers still takes object id and offset into account.
3. Finally, I think there might be a separate issue with __CPROVER_w_ok, because it succeeds on regions beyond the allocated regions. If this somehow succeeds because of overflows into object bits, the overflows should be reported in some way.

I also tried checking each of the 3 blocks above independently, since the current flow insensitive __CPROVER_allocated_memory implementation would lead to overlapping allocations above. I don't see much of a difference though. The 1st and 3rd blocks behave exactly as before, only the __CPROVER_w_ok check in the 2nd block works as expected now.

1st block

int main() {
    char *ptr;

    ptr = 0xFF;
    *ptr = '0';                                           // PASS: write succeeds without alloc?
    __CPROVER_allocated_memory(ptr, 0xFFFFFFFFFFFFFE);    // PASS: but overflow in offset space!
         assert(__CPROVER_w_ok(ptr, 0xFFFFFFFFFFFFFE));   // PASS: well, consistent with above
         assert(__CPROVER_w_ok(ptr, 0xFFFFFFFFFFFFFF00)); // FAIL: beyond alloc
         assert(__CPROVER_w_ok(ptr, 0xFFFFFFFFFFFFFF01)); // PASS: overflow beyond 64 bits!

    assert(0);
}

2nd block

int main() {
    char *ptr;

    ptr = 0xFFFFFFFFFFFFFE;    // object bits unset
    *ptr = '0';                                   // PASS: write succeeds without alloc?
    __CPROVER_allocated_memory(ptr, 0xFF);        // PASS: but overflow in offset space!
         assert(__CPROVER_w_ok(ptr, 0xFF));       // PASS: well, consistent with above
         assert(__CPROVER_w_ok(ptr, 0xFFFF));     // FAIL: beyond alloc

    assert(0);
}

3rd block

int main() {
    char *ptr;

    ptr = 0xFFFFFFFFFFFFFFE;   // object bits set to 00001111
    *ptr = '0';                                   // PASS: write succeeds without alloc?
    __CPROVER_allocated_memory(ptr, 0xFF);        // PASS: but overflow in offset space!
         assert(__CPROVER_w_ok(ptr, 0xFF));       // PASS: well, consistent with above
         assert(__CPROVER_w_ok(ptr, 0xFFFF));     // PASS: but beyond alloc!
    
    assert(0);
}

[thomasspriggs]

The __CPROVER_allocated_memory intrinsic is undocumented which makes it more difficult to say what the sound or expected behaviour of it should be. I have raised a separate issue for the documentation. #6870

[thomasspriggs]

The maximum size of the offsets (and the general encoding of pointers) is defined in the decision procedure, but the offset overflow checks are added/defined in the front end. The definitions of the of offset overflow checks should be done in the decision procedure are per this issue - #6842

This re-structuring should be handled before further investigation into pointer offset related issues. This is because what the correct checks are depends on the form of pointer encoding used in the decision procedure.

[thomasspriggs]

As @tautschnig said, __CPROVER_allocated_memory is flow insensitive. This means that it functions as a specification that the memory at the given address is allocated for the entirety of the analysis. Therefore the __CPROVER_allocated_memory(ptr, 0xFF); in your example will mean that the *ptr = '0'; assignment on the previous line is valid, because this specification applies to the whole of the program, not just the lines of code which would be executed after it is reached.

Because __CPROVER_allocated_memory is flow insensitive, multiple instances of this intrinsic for the same hardware style memory address should be considered invalid input to cbmc, because that is introducing conflicting specifications of how much memory is allocated. cbmc should check for and reject this type of input. #6871

[thomasspriggs]

Attempting to de-reference pointers with excessively large offsets will not currently cause an unsound analysis because the input will be rejected with an array too large for flattening error.
The following example will introduce such an error -

#include <assert.h>
#include <stdlib.h>

int main() {
    char *ptr = malloc(0xFFFFFFFFFFFFFE);
    assert(__CPROVER_w_ok(ptr, 0xFFFFFFFFFFFFFE));
    *(ptr + 0xFFFFFFFFFFFFFE - 1) = 0; // "Array to large for flattening" error.
    assert(0);
}

[TGWDB]

Should this be closed now that #6876 is merged?

[SaswatPadhi]

Thanks for the update.

It looks like #6876 is merged, but #6747 is still unmerged. Can we wait until that PR is merged, and then close this PR with a comment that demonstrates (1) how to invoke CBMC with the new flag instead, and (2) the pointer overflows reported here are either rejected with array too large ... or an OOB assertion failure.