Spurious malloc behavior for large allocations

[feliperodri]

CBMC version: develop
Operating system: macOs Majave
Exact command line resulting in the issue: cbmc main.c --malloc-may-fail --malloc-fail-null --pointer-overflow-check --pointer-check
What behaviour did you expect: Consistent behaviour using malloc for large allocations.
What happened instead:

Consider the following example.

     1  #include <stdlib.h>
     2  #include <stdint.h>
     3  #include <assert.h>
     4
     5  int main () {
     6      size_t size;
     7      //size = SIZE_MAX;
     8      uint8_t *ptr = malloc(size);
     9      __CPROVER_assume(ptr != NULL);
    10      uint8_t *ptr_end = ptr + size;
    11      assert(ptr <= ptr_end);
    12  }

Running this example with cbmc main.c --malloc-may-fail --malloc-fail-null --pointer-overflow-check --pointer-check leads to verification failure.

...
[main.pointer_arithmetic.16] line 11 pointer relation: dead object in ptr_end: SUCCESS
[main.pointer_arithmetic.17] line 11 pointer relation: pointer outside object bounds in ptr_end: FAILURE
[main.pointer_arithmetic.18] line 11 pointer relation: invalid integer address in ptr_end: SUCCESS

** 1 of 22 failed (2 iterations)
VERIFICATION FAILED

Running this example with cbmc main.c --pointer-overflow-check --pointer-check leads to another kind of verification failure.

...
[main.pointer_arithmetic.4] line 10 pointer arithmetic: dead object in ptr + (signed long int)size: SUCCESS
[main.pointer_arithmetic.5] line 10 pointer arithmetic: pointer outside object bounds in ptr + (signed long int)size: FAILURE
[main.pointer_arithmetic.6] line 10 pointer arithmetic: invalid integer address in ptr + (signed long int)size: SUCCESS
...
[main.pointer_arithmetic.16] line 11 pointer relation: dead object in ptr_end: SUCCESS
[main.pointer_arithmetic.17] line 11 pointer relation: pointer outside object bounds in ptr_end: FAILURE
[main.pointer_arithmetic.18] line 11 pointer relation: invalid integer address in ptr_end: SUCCESS

** 2 of 22 failed (3 iterations)
VERIFICATION FAILED

If we include line 7, we get different results too.
Using cbmc main.c --malloc-may-fail --malloc-fail-null --pointer-overflow-check --pointer-check.

...
[main.pointer_arithmetic.14] line 11 pointer relation: pointer invalid in ptr_end: SUCCESS
[main.pointer_arithmetic.15] line 11 pointer relation: deallocated dynamic object in ptr_end: SUCCESS
[main.pointer_arithmetic.16] line 11 pointer relation: dead object in ptr_end: SUCCESS
[main.pointer_arithmetic.17] line 11 pointer relation: pointer outside object bounds in ptr_end: SUCCESS
[main.pointer_arithmetic.18] line 11 pointer relation: invalid integer address in ptr_end: SUCCESS

** 0 of 22 failed (1 iterations)
VERIFICATION SUCCESSFUL

Using cbmc main.c --pointer-overflow-check --pointer-check.

CBMC version 5.30.1 (cbmc-5.21.0-1027-g64974b018-dirty) 64-bit x86_64 linux
Parsing main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00208319s
size of program expression: 87 steps
simple slicing removed 5 assignments
Generated 20 VCC(s), 3 remaining after simplification
Runtime Postprocess Equation: 1.2301e-05s
Passing problem to propositional reduction
converting SSA
array too large for flattening

Why do we have completely different results here? Am I missing something? What is CBMC behaviour for allocation attempts where size is larger than __CPROVER_max_malloc_size? What is the definition of __CPROVER_max_malloc_size?

Often, we need to use in our proofs the following trick

/**
 * CBMC has an internal representation in which each object has an index and a (signed) offset
 * A buffer cannot be larger than the max size of the offset
 * The Makefile is expected to set CBMC_OBJECT_BITS to the value of --object-bits
 */
#define MAX_MALLOC (SIZE_MAX >> (CBMC_OBJECT_BITS + 1))

size_t size;
__CPROVER_assume(size < MAX_MALLOC);
void *ptr = malloc(size);

Why should this be even necessary here? Wouldn't malloc take care of such cases?

cc. @tautschnig @SaswatPadhi

[feliperodri]

The counterexample when running cbmc main.c --malloc-may-fail --malloc-fail-null --pointer-overflow-check --pointer-check --trace on this example also raise some questions.

State 70 file main.c function main line 10 thread 0
----------------------------------------------------
  ptr_end=dynamic_object1 + -36028797018963968l (00000010 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

Violated property:
  file main.c function main line 11 thread 0
  pointer relation: pointer outside object bounds in ptr_end
  POINTER_OFFSET(ptr_end) >= 0l && OBJECT_SIZE(ptr_end) >= (unsigned long int)POINTER_OFFSET(ptr_end)

Why does CBMC have a negative number as offset in this case?

[SaswatPadhi]

IMO, the most worrying issue here is the crash. CBMC should never crash.

This PR looks related: #5210.
When using --malloc-fail-assert, as used in regression/cbmc/malloc-too-large introduced in this PR, CBMC doesn't crash:

$ cat ~/test.c
#include <stdlib.h>
#include <stdint.h>
#include <assert.h>

int main () {
    size_t size;
    size = SIZE_MAX;
    uint8_t *ptr = malloc(size);
    __CPROVER_assume(ptr != NULL);
    uint8_t *ptr_end = ptr + size;
    assert(ptr <= ptr_end);
}

$ cbmc ~/test.c
CBMC version 5.30.0 (cbmc-5.24.0-606-g0ea7f13c4-dirty) 64-bit x86_64 macos
Parsing /Users/saspadhi/test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.0242014s
size of program expression: 85 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 5.2114e-05s
Passing problem to propositional reduction
converting SSA
array too large for flattening

$ cbmc --malloc-fail-assert ~/test.c | tail
** Results:
/Users/saspadhi/test.c function main
[main.assertion.1] line 11 assertion ptr <= ptr_end: SUCCESS

<builtin-library-malloc> function malloc
[malloc.assertion.1] line 26 max allocation size exceeded: FAILURE
[malloc.assertion.2] line 31 max allocation may fail: SUCCESS

** 1 of 3 failed (2 iterations)
VERIFICATION FAILED

[feliperodri]

Without the flag --malloc-fail-assert, I wouldn’t expect [malloc.assertion.1] line 26 max allocation size exceeded: FAILURE. malloc should fail to allocate a huge chunk of memory, and return NULL.

[tautschnig]

@SaswatPadhi Could you please elaborate on the following:

IMO, the most worrying issue here is the crash. CBMC should never crash.

Which of the examples provided above results in some kind of "crash?"

[tautschnig]

@feliperodri @SaswatPadhi Thank you for the detailed report. Apart from my above question: I'll try to figure out whether there are bugs hidden in here that aren't just down to the object:offset encoding. That I'm trying to get rid of in #1086, which I'm (very slowly) making progress on.

[SaswatPadhi]

Which of the examples provided above results in some kind of "crash?"

I meant when running CBMC without --malloc-fail-assert flag:

cbmc ~/test.c

$ cat ~/test.c
#include <stdlib.h>
#include <stdint.h>
#include <assert.h>

int main () {
    size_t size;
    size = SIZE_MAX;
    uint8_t *ptr = malloc(size);
    __CPROVER_assume(ptr != NULL);
    uint8_t *ptr_end = ptr + size;
    assert(ptr <= ptr_end);
}

$ cbmc ~/test.c
CBMC version 5.30.0 (cbmc-5.24.0-606-g0ea7f13c4-dirty) 64-bit x86_64 macos
Parsing /Users/saspadhi/test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.0242014s
size of program expression: 85 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 5.2114e-05s
Passing problem to propositional reduction
converting SSA
array too large for flattening

May be "crash" is the wrong word here, but this does look like an internal exception or a crash ...

An assertion failure on whatever property we expect malloc to always satisfy, may be some size bound in this case, would be a much better output.

[tautschnig]

May be "crash" is the wrong word here, but this does look like an internal exception or a crash ...

Ah, understood. That would be fixed by #2108, which we should perhaps merge (after rebasing) as-is and not wait for #1874 to be fixed first.

[SaswatPadhi]

Thanks for looking into this!

Yes, if #1874 is an optimization PR (which it looks like, from the title), then let's please merge #2108 first.