__CPROVER_w_ok has weird behaviour

[danielsn]

Since y > x, it should be true that !__CPROVER_w_ok(a, y) is always false. However, if you assert this fact, you get an assertion violation.

#include<assert.h>
#include<stdlib.h>
#include<stdint.h>

int main() {
  size_t x;
  size_t y;
  uint8_t* a;

  __CPROVER_assume(x > 0);
  __CPROVER_assume(y > x);

  a = malloc(sizeof(*(a)) * (x));

  assert(!__CPROVER_w_ok(a, y));
}

~/temp $ cbmc *.c --trace --pointer-check --bounds-check
CBMC version 5.12 (cbmc-5.12-d8598f8-1008-gfab409d18) 64-bit x86_64 macos
Parsing 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
size of program expression: 70 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
874 variables, 2035 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.00674373s
Building error trace

** Results:
test.c function main
[main.assertion.1] line 15 assertion !__CPROVER_w_ok(a, y): FAILURE

Trace for main.assertion.1:

State 21 file test.c function main line 6 thread 0
----------------------------------------------------
  x=35235878141952ul (00000000 00000000 00100000 00001011 11111110 00000000 00000000 00000000)

State 22 file test.c function main line 7 thread 0
----------------------------------------------------
  y=36028814198833152ul (00000000 10000000 00000000 00000100 00000000 00000000 00000000 00000000)

State 23 file test.c function main line 8 thread 0
----------------------------------------------------
  a=((uint8_t *)NULL) (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

Assumption:
  file test.c line 10 function main
  x > (unsigned long int)0

Assumption:
  file test.c line 11 function main
  y > x

State 29 file test.c function main line 13 thread 0
----------------------------------------------------
  malloc_size=35235878141952ul (00000000 00000000 00100000 00001011 11111110 00000000 00000000 00000000)

State 48 file test.c function main line 13 thread 0
----------------------------------------------------
  a=dynamic_object1 (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

Violated property:
  file test.c function main line 15 thread 0
  assertion !__CPROVER_w_ok(a, y)
  !((signed long int)(signed long int)!(!((FALSE || !(POINTER_OBJECT((const void *)a) == POINTER_OBJECT(NULL))) && !IS_INVALID_POINTER((const void *)a) && (FALSE || !(POINTER_OBJECT((const void *)a) == POINTER_OBJECT(__CPROVER_deallocated))) && (FALSE || !(POINTER_OBJECT((const void *)a) == POINTER_OBJECT(__CPROVER_dead_object))) && (FALSE || (POINTER_OBJECT((const void *)a) == POINTER_OBJECT(__CPROVER_malloc_object) ==> !(POINTER_OFFSET((const void *)a) < 0l || (size_t)POINTER_OFFSET((const void *)a) + y > __CPROVER_malloc_size))) && (FALSE || (!IS_DYNAMIC_OBJECT((const void *)a) ==> !(POINTER_OFFSET((const void *)a) < 0l || (size_t)POINTER_OFFSET((const void *)a) + y > OBJECT_SIZE((const void *)a)))) && (POINTER_OBJECT(NULL) == POINTER_OBJECT((const void *)a) && NULL != (const void *)a ==> FALSE))) != 0l)



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

~/temp $ cbmc --version
5.12 (cbmc-5.12-d8598f8-1008-gfab409d18)
~/temp $ sw_vers
ProductName:	Mac OS X
ProductVersion:	10.14.6
BuildVersion:	18G1012

[danielsn]

Most likely related to the issue in https://github.com/danielsn/s2n/tree/cbmc_issue_5194 on the s2n/tests/cbmc/proofs/s2n_stuffer_init proof
@tautschnig

[thk123]

This is tracked internally by ADA-450

[danpoe]

This behavior is due to how bounds checking for dynamically allocated memory is implemented in cbmc.

The model for malloc() in cbmc looks essentially as follows:

void *malloc(__CPROVER_size_t malloc_size)
{
  void *malloc_res = __CPROVER_allocate(malloc_size, 0);

  if(nondet_bool()) {
    __CPROVER_malloc_object = malloc_res;
    __CPROVER_malloc_size = malloc_size;
  }

  return malloc_res;
}

The nondeterministic switch controls whether the address and size of the memory block allocated in this particular invocation of malloc() are recorded.

The condition __CPROVER_r_ok(a, size) checks the following (simplified):

POINTER_OBJECT(a) == POINTER_OBJECT(__CPROVER_malloc_object) ==>
POINTER_OFFSET(a) + size <= __CPROVER_malloc_size

To illustrate how the bounds checking works, consider the following example program:

int main()
{
  char *p1 = malloc(1);
  char *p2 = malloc(2);

  assert(__CPROVER_r_ok(p1, 2));
}

Here the assertion should fail. In the approach outlined above it indeed can, as one can choose true for nondet_bool() in the first call to malloc(), and false for nondet_bool() in the second call to malloc(). Thus, the object address and size of the first call to malloc() are recorded in __CPROVER_malloc_object and __CPROVER_malloc_size respectively. Thus, the premise of the implication above is true, while the conclusion is false, hence __CPROVER_r_ok() is false.

This approach for bounds checking is also the reason for why there is (almost) always a trace for which !__CPROVER_r_ok(a, size) is false. The negated condition checks the following (simplified):

POINTER_OBJECT(a) == POINTER_OBJECT(__CPROVER_malloc_object) &&
POINTER_OFFSET(a) + size > __CPROVER_malloc_size

If choosing false for nondet_bool() for the malloc() call that allocated the memory pointed to by a, then the first conjunct and thus the whole condition will be false.

In summary, this behavior is not a bug but due to how cbmc implements bounds checking for dynamically allocated memory. Also while the negative version !__CPROVER_r_ok() is imprecise, the positive version __CPROVER_r_ok() is precise. Maybe in the future we should remove __CPROVER_r_ok() and provide a primitive __CPROVER_assert_r_ok() instead.

[karkhaz]

Here's another example that @danielsn and I came up with:

#include <stdlib.h>

int main()
{
  int *x = malloc(2), *y = malloc(2);
  assert(__CPROVER_r_ok(x, 3) == __CPROVER_r_ok(y, 3));
}

This assertion fails. It also fails if you change the == into !=.

[danpoe]

This behavior is due to how __CPROVER_r_ok() is implemented. At present, the only useful way to use the primitive is as assert(__CPROVER_r_ok(x, size)). That's why we should probably at some point replace __CPROVER_r_ok() with a new primitive __CPROVER_assert_r_ok() which directly asserts the condition (instead of just returning a boolean).

[danielsn]

The example I mentioned today:

#include <assert.h>
#include <stdlib.h>
#include <stdint.h>
#include <stdio.h>
#include <stdbool.h>


int main() {
    char* foo;
    __CPROVER_assume(__CPROVER_r_ok(foo, 10));
    foo[20];
    return 1;
}

~/temp $ cbmc --pointer-check --bounds-check test.c
CBMC version 5.12 (cbmc-5.12-d8598f8-1407-ga7f5ebd05-dirty) 64-bit x86_64 macos
Parsing 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
size of program expression: 38 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
89 variables, 9 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime decision procedure: 0.00186795s

** Results:
/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/stdio.h function __sputc
[__sputc.pointer_dereference.1] line 265 dereference failure: pointer NULL in _p->_w: SUCCESS
[__sputc.pointer_dereference.2] line 265 dereference failure: pointer invalid in _p->_w: SUCCESS
[__sputc.pointer_dereference.3] line 265 dereference failure: deallocated dynamic object in _p->_w: SUCCESS
[__sputc.pointer_dereference.4] line 265 dereference failure: dead object in _p->_w: SUCCESS
[__sputc.pointer_dereference.5] line 265 dereference failure: pointer outside dynamic object bounds in _p->_w: SUCCESS
[__sputc.pointer_dereference.6] line 265 dereference failure: pointer outside object bounds in _p->_w: SUCCESS
[__sputc.pointer_dereference.7] line 265 dereference failure: invalid integer address in _p->_w: SUCCESS
[__sputc.pointer_dereference.8] line 265 dereference failure: pointer NULL in _p->_w: SUCCESS
[__sputc.pointer_dereference.9] line 265 dereference failure: pointer invalid in _p->_w: SUCCESS
[__sputc.pointer_dereference.10] line 265 dereference failure: deallocated dynamic object in _p->_w: SUCCESS
[__sputc.pointer_dereference.11] line 265 dereference failure: dead object in _p->_w: SUCCESS
[__sputc.pointer_dereference.12] line 265 dereference failure: pointer outside dynamic object bounds in _p->_w: SUCCESS
[__sputc.pointer_dereference.13] line 265 dereference failure: pointer outside object bounds in _p->_w: SUCCESS
[__sputc.pointer_dereference.14] line 265 dereference failure: invalid integer address in _p->_w: SUCCESS
[__sputc.pointer_dereference.15] line 265 dereference failure: pointer NULL in _p->_w: SUCCESS
[__sputc.pointer_dereference.16] line 265 dereference failure: pointer invalid in _p->_w: SUCCESS
[__sputc.pointer_dereference.17] line 265 dereference failure: deallocated dynamic object in _p->_w: SUCCESS
[__sputc.pointer_dereference.18] line 265 dereference failure: dead object in _p->_w: SUCCESS
[__sputc.pointer_dereference.19] line 265 dereference failure: pointer outside dynamic object bounds in _p->_w: SUCCESS
[__sputc.pointer_dereference.20] line 265 dereference failure: pointer outside object bounds in _p->_w: SUCCESS
[__sputc.pointer_dereference.21] line 265 dereference failure: invalid integer address in _p->_w: SUCCESS
[__sputc.pointer_dereference.22] line 265 dereference failure: pointer outside dynamic object bounds in _p->_lbfsize: SUCCESS
[__sputc.pointer_dereference.23] line 265 dereference failure: pointer outside object bounds in _p->_lbfsize: SUCCESS
[__sputc.pointer_dereference.24] line 265 dereference failure: invalid integer address in _p->_lbfsize: SUCCESS
[__sputc.pointer_dereference.25] line 266 dereference failure: pointer NULL in _p->_p: SUCCESS
[__sputc.pointer_dereference.26] line 266 dereference failure: pointer invalid in _p->_p: SUCCESS
[__sputc.pointer_dereference.27] line 266 dereference failure: deallocated dynamic object in _p->_p: SUCCESS
[__sputc.pointer_dereference.28] line 266 dereference failure: dead object in _p->_p: SUCCESS
[__sputc.pointer_dereference.29] line 266 dereference failure: pointer outside dynamic object bounds in _p->_p: SUCCESS
[__sputc.pointer_dereference.30] line 266 dereference failure: pointer outside object bounds in _p->_p: SUCCESS
[__sputc.pointer_dereference.31] line 266 dereference failure: invalid integer address in _p->_p: SUCCESS
[__sputc.pointer_dereference.32] line 266 dereference failure: pointer NULL in *tmp_post: SUCCESS
[__sputc.pointer_dereference.33] line 266 dereference failure: pointer invalid in *tmp_post: SUCCESS
[__sputc.pointer_dereference.34] line 266 dereference failure: deallocated dynamic object in *tmp_post: SUCCESS
[__sputc.pointer_dereference.35] line 266 dereference failure: dead object in *tmp_post: SUCCESS
[__sputc.pointer_dereference.36] line 266 dereference failure: pointer outside dynamic object bounds in *tmp_post: SUCCESS
[__sputc.pointer_dereference.37] line 266 dereference failure: pointer outside object bounds in *tmp_post: SUCCESS
[__sputc.pointer_dereference.38] line 266 dereference failure: invalid integer address in *tmp_post: SUCCESS
[__sputc.pointer_dereference.39] line 266 dereference failure: pointer NULL in *tmp_post: SUCCESS
[__sputc.pointer_dereference.40] line 266 dereference failure: pointer invalid in *tmp_post: SUCCESS
[__sputc.pointer_dereference.41] line 266 dereference failure: deallocated dynamic object in *tmp_post: SUCCESS
[__sputc.pointer_dereference.42] line 266 dereference failure: dead object in *tmp_post: SUCCESS
[__sputc.pointer_dereference.43] line 266 dereference failure: pointer outside dynamic object bounds in *tmp_post: SUCCESS
[__sputc.pointer_dereference.44] line 266 dereference failure: pointer outside object bounds in *tmp_post: SUCCESS
[__sputc.pointer_dereference.45] line 266 dereference failure: invalid integer address in *tmp_post: SUCCESS

test.c function main
[main.pointer_dereference.1] line 11 dereference failure: pointer uninitialized in foo[(signed long int)20]: SUCCESS

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

[danpoe]

Thanks for the example. After looking further into this, it turns out that all uses of __CPROVER_r_ok(p, size) other than assert(__CPROVER_r_ok(p, size)) are not expected to work at the moment due to the way it is implemented. In most cases, it should be possible to model the behavior using other CPROVER primitives, e.g. for the provided example:

#include <stdlib.h>

void main()
{
  size_t size;
  __CPROVER_assume(size >= 10);
  char *foo = malloc(size);
  __CPROVER_assume(foo != NULL);

  foo[20];
}

[mww-aws]

It is obvious this is how it is currently implemented, so whether you consider it a bug or not depends on whether you consider design issues.

To me, this is not a useful definition in full generality. What is required here is a mechanism for getting the size of an allocated pointer. Rather than __CPROVER_malloc_size, we need __CPROVER_malloc_size(a) where a is a pointer in the program. If a is not an allocated pointer, this call should lead to an error. The metadata for size must exist in CBMC already. What we need is a mechanism to pull it out. Then we could drop the global variables and do a proper comparison:
POINTER_OFFSET(a) + size > __CPROVER_malloc_size(a)

There are many useful problems that could be solved by supporting such a macro, including using the __CPROVER_r_ok in negative contexts (it is not just assumptions, it is under any negation where it will fail, so the renaming trick is not sufficient).

[karkhaz]

@danpoe is this something that somebody at Diffblue could work on implementing, or give me some pointers on how to get started? This is feature is vital to us–we'll need a predicate that does the right thing when used in an assume (so __CPROVER_assert_r_ok() wouldn't work, we do need something that returns a boolean).

So the required behavior would be: if we assume that a pointer p points to a valid object, then CBMC should actually mint that object and then use it for future accesses to *p. If we assert that p points to a valid object, then CBMC should turn that into a disjunction over all of the objects that have been allocated during symbolic execution.

The broader context is the function contracts work: we need to be able to say that a function parameter is backed by valid memory in a function precondition. This needs to work in the case where we're checking a function independently of its calling context; since nobody has called the function, there isn't a real object that was passed into the function, so we need to assume that the object exists in the function precondition.