Description
I wrote this to try to generate offset values that would overflow in the bitwidth allocated for offsets in pointers but still land within objects.
cbmc --object-bits 16 --arrays-uf-always falsifies the last assertion, generating a trace with a very large value for offset that allows to land in the first half of the object when added to a pointer that is already at the middle of the object (because of an overflow on the 48bit offset addition)
#include <stdlib.h>
#include <assert.h>
int main() {
size_t size = (1ULL << 47)-1;
assert(size < __CPROVER_max_malloc_size);
size_t half_size = size / 2;
char *a_start = malloc(size);
// 00000000 00000010 00000000 00000000 00000000 00000000 00000000 00000000
char *a_mid = a_start + half_size;
// 00000000 00000010 00111111 11111111 11111111 11111111 11111111 11111111
char *a_end = a_start + size;
// 00000000 00000010 01111111 11111111 11111111 11111111 11111111 11111111
size_t offset;
// 00000000 00000000 11000000 00000000 00000000 00001000 00000000 00000000
if(half_size < offset && offset < (1ULL << 48) - 1) {
// take some nondet offset in range of half_size and max malloc size
// add that offset to the mid pointer
char *c = a_mid + offset;
// assert that is after the middle. if falsified, this gives us a value that
// when added to mid, overflows the pointer representation and lands back at the beginning of the object.
size_t large = offset + half_size; // this overflows into the object bits
// in c the offset is truncated to 48 bits and lands before the middle
// a_mid = 00000000 00000010 00111111 11111111 11111111 11111111 11111111 11111111
// offset = 00000000 00000000 11000000 00000000 00000000 00001000 00000000 00000000
// c = 00000000 00000010 00000000 00000000 00000000 00000111 11111111 11111111
// large = 00000000 00000001 00000000 00000000 00000000 00000111 11111111 11111111
assert(c >= a_mid);
}
}If I extract the value from the counter example and plug it back in the code:
size_t offset = 211106233057280ul;The assertion c >= mid is not falsified anymore.
** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 31 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 36 max allocation may fail: SUCCESS
ptr_sub.c function main
[main.assertion.1] line 7 assertion size < __CPROVER_max_malloc_size: SUCCESS
[main.assertion.2] line 33 assertion c >= a_mid: SUCCESS
** 0 of 4 failed (1 iterations)
VERIFICATION SUCCESSFUL
If I add an assert(false) at the end to generate a trace with that constant plugged in, I see that all values computed in the trace are the same as before. So CBMC tells me that offset = 211106233057280ul falsifies an assertion and also tells me that it doesn't.
Reassuringly, the pointer checks and pointer overflow checks are falsified in both cases
[main.pointer_arithmetic.17] line 23 pointer arithmetic: pointer outside object bounds in a_mid + (signed long int)offset: FAILURE
[main.pointer_arithmetic.23] line 33 pointer relation: pointer outside object bounds in c: FAILURE
CBMC version: 5.91.0
Operating system: macOS
Exact command line resulting in the issue: cbmc --object-bits 16 --arrays-uf-always main.c
What behaviour did you expect:
What happened instead: