Memory primitives should handle invalid pointers

[feliperodri]

CBMC version: 5.27.0 (cbmc-5.26.0-148-g7ced011bd-dirty)
Operating system: macOS Mojave 10.14.6
Exact command line resulting in the issue: cbmc main.c --malloc-may-fail --malloc-fail-null --trace
What behaviour did you expect: line 7 assertion __CPROVER_r_ok(ptr, 0): FAILURE
What happened instead: VERIFICATION SUCCESSFUL

To explain the behavior, let's consider the following example.

// main.c
#include <stdlib.h>
#include <assert.h>

int main() {
  void *ptr = malloc(0);
  __CPROVER_assume(ptr != NULL);
  assert(__CPROVER_r_ok(ptr, 0));
}

I expect the assertion to fail, because ptr could be an invalid pointer; however, it succeeds.

CBMC version 5.27.0 (cbmc-5.26.0-148-g7ced011bd-dirty) 64-bit x86_64 macos
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.0034956s
size of program expression: 94 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.1753e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000522958s
Running propositional reduction
Post-processing
Runtime Post-process: 8.1631e-05s
Solving with MiniSAT 2.2.1 with simplifier
437 variables, 313 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 9.8288e-05s
Runtime decision procedure: 0.000650914s

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

main.c function main
[main.assertion.1] line 8 assertion __CPROVER_r_ok(ptr, 0): SUCCESS

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

I expect that the first thing __CPROVER_r_ok would check is whether the pointer is valid or not. If not valid, return false.
I also try to verify this program using --pointer-primitive-check flag, but I got another unexpected behavior.
Command line: cbmc main.c --malloc-may-fail --malloc-fail-null --pointer-primitive-check --trace

CBMC version 5.27.0 (cbmc-5.26.0-148-g7ced011bd-dirty) 64-bit x86_64 macos
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.00497527s
size of program expression: 99 steps
simple slicing removed 5 assignments
Generated 6 VCC(s), 6 remaining after simplification
Runtime Postprocess Equation: 1.4961e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000804849s
Running propositional reduction
Post-processing
Runtime Post-process: 0.000148184s
Solving with MiniSAT 2.2.1 with simplifier
508 variables, 679 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00109353s
Runtime decision procedure: 0.00196439s
Building error trace
Running propositional reduction
Solving with MiniSAT 2.2.1 with simplifier
508 variables, 372 clauses
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 1.8796e-05s
Runtime decision procedure: 3.933e-05s

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

main.c function main
[main.assertion.1] line 8 assertion __CPROVER_r_ok(ptr, 0): SUCCESS
[main.pointer_primitives.1] line 8 pointer invalid in R_OK(ptr, (__CPROVER_size_t)0): SUCCESS
[main.pointer_primitives.2] line 8 deallocated dynamic object in R_OK(ptr, (__CPROVER_size_t)0): SUCCESS
[main.pointer_primitives.3] line 8 dead object in R_OK(ptr, (__CPROVER_size_t)0): SUCCESS
[main.pointer_primitives.4] line 8 pointer outside dynamic object bounds in R_OK(ptr, (__CPROVER_size_t)0): FAILURE
[main.pointer_primitives.5] line 8 pointer outside object bounds in R_OK(ptr, (__CPROVER_size_t)0): SUCCESS

Trace for main.pointer_primitives.4:

State 26 file main.c function main line 6 thread 0
----------------------------------------------------
  ptr=NULL (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 30 file main.c function main line 6 thread 0
----------------------------------------------------
  malloc_size=0ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 59 file main.c function main line 6 thread 0
----------------------------------------------------
  ptr=(const void *)dynamic_object1 (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

Assumption:
  file main.c line 7 function main
  ptr != (void *)0

Violated property:
  file main.c function main line 8 thread 0
  pointer outside dynamic object bounds in R_OK(ptr, (__CPROVER_size_t)0)
  POINTER_OBJECT(NULL) == POINTER_OBJECT(ptr) || !IS_DYNAMIC_OBJECT(ptr) || POINTER_OFFSET(ptr) >= 0l && OBJECT_SIZE(ptr) >= (unsigned long int)POINTER_OFFSET(ptr) + 1ul



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

Again, if cbmc checked for validity first, I think we'd also avoid this problem.

[feliperodri]

cc. @SaswatPadhi

[feliperodri]

In fact, why does cbmc return dynamic_object1 for malloc(0)?

[SaswatPadhi]

Quoting from https://stackoverflow.com/a/2022402:

The C standard (C17 7.22.3/1) says:

If the size of the space requested is zero, the behavior is implementation defined: either a null pointer is returned, or the behavior is as if the size were some nonzero value, except that the returned pointer shall not be used to access an object.

malloc(0) could return NULL or a valid memory location which shouldn't be dereferenced.

So, I think there are two issues raised by this bug report:

1. What does __CPROVER_r_ok do without --pointer-primitive-check flag?
2. malloc(0) shouldn't return a new dynamic object, as Felipe already pointed out.

Here is a clear soundness bug, even without using __CPROVER_r_ok:

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

int main() {
  char *a = malloc(0);
  char *b = malloc(0);
  
  __CPROVER_assume(a != NULL && b != NULL);
  
  assert(a != b);
}

$ cbmc --malloc-may-fail --malloc-fail-null --pointer-check test.c | tail
** Results:
/Users/saspadhi/test.c function main
[main.assertion.1] line 10 assertion a != b: SUCCESS

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

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

According to C standard, this should fail because a and b could actually be the same location!

malloc(0) should be treated just like a non-deterministic pointer.

[tautschnig]

[...]

1. What does `__CPROVER_r_ok` do without `--pointer-primitive-check` flag?

See http://cprover.diffblue.com/memory-primitives.html.

2. `malloc(0)` shouldn't return a new dynamic object, as Felipe already pointed out.

Why not?

Here is a clear soundness bug, even without using __CPROVER_r_ok:

[...]

According to C standard, this should fail because a and b could actually be the same location!

I don't think "According to the C standard, this should fail" is correct. The C standard says that the behaviour is implementation-defined. If, however, we want to simulate all permitted implementations, then, yes, we would also have to consider the case where multiple calls to malloc return the same address. This is something we currently don't do, and it's a limitation not restricted to the case of zero-sized allocations.

malloc(0) should be treated just like a non-deterministic pointer.

Why?

[SaswatPadhi]

Hi Michael,

According to C standard, this should fail because a and b could actually be the same location!

I don't think "According to the C standard, this should fail" is correct. The C standard says that the behaviour is implementation-defined.

You're right, I should have said, "according to the C standard, this could fail." Are we currently verifying all properties assuming a particular compiler implementation?

This is something we currently don't do, and it's a limitation not restricted to the case of zero-sized allocations.

I don't know enough about malloc -- can different calls to malloc for non-zero-sized allocations actually return the same address (within the same process)?

malloc(0) should be treated just like a non-deterministic pointer.

Why?

I suggested this to "simulate all platforms", as you mentioned. The standard says it's implementation-defined, so on an arbitrary implementation it would be a non-deterministic pointer.

[tautschnig]

[...]

Are we currently verifying all properties assuming a particular compiler implementation?

We do honor the system compiler at times, but here it's not just the compiler: also the C library matters. And, no, we don't consistently consider all possible cases or all the specifics of an existing implementation. We should strive to fix this and make sure all such aspects are configurable.

This is something we currently don't do, and it's a limitation not restricted to the case of zero-sized allocations.

I don't know enough about malloc -- can different calls to malloc for non-zero-sized allocations actually return the same address (within the same process)?

Yes:

$ cat re-malloc.c
#include <stdio.h>
#include <stdlib.h>
#include <inttypes.h>

int main()
{
  int *p = malloc(sizeof(int));
  uintptr_t p_int = (uintptr_t)p;
  free(p);
  int *q = malloc(sizeof(int));
  uintptr_t q_int = (uintptr_t)q;
  free(q);

  printf("p = %lx\n", p_int);
  printf("q = %lx\n", q_int);
}

$ gcc re-malloc.c && ./a.out
p = 556dc9aa3260
q = 556dc9aa3260

malloc(0) should be treated just like a non-deterministic pointer.

Why?

I suggested this to "simulate all platforms", as you mentioned. The standard says it's implementation-defined, so on an arbitrary implementation it would be a non-deterministic pointer.

But a non-deterministic pointer would include pointers to existing objects, resulting dereferencing suddenly becoming valid for such cases.

So, yes, our modeling of malloc could perhaps be made more elaborate. But let's take a few steps back first: what problem are you seeking to solve?

[SaswatPadhi]

Thanks a lot for the detailed explanation.

malloc could reuse freed addresses, so I see now how different calls to it could return the same address.

But a non-deterministic pointer would include pointers to existing objects, resulting dereferencing suddenly becoming valid for such cases.

Ah yes, so perhaps a non-deterministic pointer that's invalid, i.e. either NULL or doesn't map to any existing object.

But let's take a few steps back first: what problem are you seeking to solve?

May be @feliperodri can comment on this. He was debugging some s2n issue. (I was just digging deep into the bug report.)