Description
CBMC version: CBMC version 5.12 (cbmc-5.12-d8598f8-979-gfc0a0cd57) 64-bit x86_64 macos
Operating system: MacOS
Exact command line resulting in the issue: cbmc --object-bits 7 --32 --trace demo.c
What behaviour did you expect: verification successful
What happened instead: verification failure
The final __CPROVER_w_ok assertion in the attached demo.c fails when run with cbmc --object-bits 7 --32 demo.c.
#include <stdlib.h>
void main() {
char* buffer;
char* buffer_next;
char* buffer_end;
// Running cbmc with --object-bits 7 --32
// Top 7 bits of pointer are object id
// Bottom 32-7 bits of pointer are object offset
// Ensure all valid offsets fit within 32-7 bits.
uint32_t buffer_length;
__CPROVER_assume(buffer_length < 0x02000000);
buffer = malloc(buffer_length);
size_t offset1;
size_t offset2;
__CPROVER_assume(offset1 < offset2);
__CPROVER_assume(offset1 < buffer_length);
__CPROVER_assume(offset2 < buffer_length);
buffer_next = buffer + offset1;
buffer_end = buffer + offset2;
uint32_t length;
__CPROVER_assume(length < (buffer_end - buffer_next));
__CPROVER_size_t show_buffer_object = __CPROVER_POINTER_OBJECT(buffer_next);
__CPROVER_ssize_t show_buffer_offset = __CPROVER_POINTER_OFFSET(buffer_next);
__CPROVER_size_t show_buffer_size = __CPROVER_OBJECT_SIZE(buffer_next);
__CPROVER_assert(__CPROVER_w_ok(buffer_next, length), "buffer length");
}
The arguments to cbmc ask for the top 7 bits of a pointer to be used for the object id, and the bottom 25 bits to be used for the object offset.
The trace (summarized below) shows that the bytes buffer_next through buffer_next + length fit within the buffer, so the assertion should be true: offset1 + length = 20125093u + 668989u = 20794082 < 25545442u = buffer_length
cbmc --object-bits 7 --32 --trace demo.c
CBMC version 5.12 (cbmc-5.12-d8598f8-979-gfc0a0cd57) 64-bit x86_64 macos
buffer_length=25545442u (00000001 10000101 11001010 11100010)
buffer=(char *)dynamic_object1 (00000100 00000000 00000000 00000000)
offset1=20125093u (00000001 00110011 00010101 10100101)
offset2=20826850u (00000001 00111101 11001010 11100010)
buffer_next=(char *)(dynamic_object1 + -13429339) (00000101 00110011 00010101 10100101)
buffer_end=(char *)(dynamic_object1 + -12727582) (00000101 00111101 11001010 11100010)
length=668989u (00000000 00001010 00110101 00111101)
show_buffer_object=2u (00000000 00000000 00000000 00000010)
show_buffer_offset=-13429339 (11111111 00110011 00010101 10100101)
show_buffer_size=25545442u (00000001 10000101 11001010 11100010)
Violated property:
file demo.c function main line 31 thread 0
buffer length
It seems significant to me that in these offsets into buffer, the top bit of the 25 offset bits is
set to 1. It surprised me that __CPROVER_POINTER_OFFSET displays the offset of buffer_next
with sign extension making to first byte 0xFF. It surprised me that the type of __CPROVER_POINTER_OFFSET in cprover_builtin_headers.h is __CPROVER_ssize_t and not __CPROVER_size_t.
If I replace
__CPROVER_assume(buffer_length < 0x02000000);
with
__CPROVER_assume(buffer_length < 0x01000000);
to ensure that the top bit in all offsets is 0, then the problem goes away.