__CPROVER_w_ok is wrong with large object offsets

[markrtuttle]

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.

[tautschnig]

I do wonder whether this actually is a bug. Pointer offsets are signed in general (in C) as subtraction from a pointer is well-defined (while within an object). That said, a negative object in CBMC's pointer representation not necessarily makes sense. @chrisr-diffblue Would you be able to kick off a discussion with @kroening to figure out whether treating offsets in the object:offset model as signed really is the intended behaviour? If it is, then users need to make sure they only use bitwidth-objectbits-1 bits for object sizes.

[markrtuttle]

Any progress? The effect of this issue is that proofs are weaker (hold for smaller objects).

[kroening]

There is significant value in negative offsets in the representation: they enable you to neatly distinguish the case where a pointer gets decremented too much from the one where it gets incremented too much.

The real fix for this issue should be to remove the limitation to anything less than the width of pointers for offsets.

[hannes-steffenhagen-diffblue]

Tracked internally as ADA-566. Currently not planning to fix this as we don’t know of a reasonable way to remove this limitation.

[feliperodri]

@hannes-steffenhagen-diffblue @markrtuttle @kroening is there any updates from this issue? Should we close it?

[markrtuttle]

The example still performs as described with cbmc 3.37, but running with the new flag --pointer-primitive-check now generates "pointer outside object bounds" errors for the value initializing the three show_buffer_* definitions at the end of the example.

[markrtuttle]

Closing as a known consequence of offsets being modeled as a signed integer.