--pointer-primitive-check fails on __CPROVER_r_ok(ptr, 0) when ptr = malloc(0) #7064
Description
CBMC version: 5.62
Operating system: linux/macos
Exact command line resulting in the issue: `cbmc --pointer-check --pointer-overflow-check --pointer-primitive-check"
What behaviour did you expect: success
What happened instead: failed proof obligations
I ran into this issue while writing a custom stub for memcpy, by copying the CPROVER library function and modifying it slightly :
#include <stdlib.h>
#include <string.h>
#undef memcpy
void *memcpy(void *dst, const void *src, size_t n)
{
__CPROVER_precondition(
__CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
((const char *)src >= (const char *)dst + n) ||
((const char *)dst >= (const char *)src + n),
"memcpy src/dst overlap");
__CPROVER_precondition(
__CPROVER_r_ok(src, n), "memcpy source region readable");
__CPROVER_precondition(
__CPROVER_w_ok(dst, n), "memcpy destination region writeable");
if(n > 0)
{
// library code
// char src_n[n];
// __CPROVER_array_copy(src_n, (char *)src);
// __CPROVER_array_replace((char *)dst, src_n);
// modified code
__CPROVER_havoc_slice(dst, n);
}
return dst;
}
int main() {
size_t src_size;
size_t dest_size;
__CPROVER_assume(dest_size >= src_size);
char *src = malloc(src_size);
__CPROVER_assume(src);
char *dest = malloc(dest_size);
__CPROVER_assume(dest);
memcpy(dest,src,src_size);
}cbmc memcpy.c
** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 28 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 33 max allocation may fail: SUCCESS
memcpy.c function main
[main.precondition_instance.1] line 39 memcpy src/dst overlap: SUCCESS
[main.precondition_instance.2] line 39 memcpy source region readable: SUCCESS
[main.precondition_instance.3] line 39 memcpy destination region writeable: SUCCESS
memcpy.c function memcpy
[memcpy.assertion.1] line 25 assertion havoc_slice W_OK(dst, n): SUCCESS
** 0 of 6 failed (1 iterations)
VERIFICATION SUCCESSFUL
VS this with pointer primitive checks enabled
cbmc memcpy.c --pointer-primitive-check
** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 28 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 33 max allocation may fail: SUCCESS
memcpy.c function main
[main.precondition_instance.1] line 39 memcpy src/dst overlap: SUCCESS
[main.precondition_instance.2] line 39 memcpy source region readable: SUCCESS
[main.precondition_instance.3] line 39 memcpy destination region writeable: SUCCESS
memcpy.c function memcpy
[memcpy.pointer_primitives.1] line 13 pointer invalid in R_OK((const void *)src, src_size): SUCCESS
[memcpy.pointer_primitives.2] line 13 deallocated dynamic object in R_OK((const void *)src, src_size): SUCCESS
[memcpy.pointer_primitives.3] line 13 dead object in R_OK((const void *)src, src_size): SUCCESS
[memcpy.pointer_primitives.4] line 13 pointer outside object bounds in R_OK((const void *)src, src_size): FAILURE
[memcpy.pointer_primitives.5] line 15 pointer invalid in W_OK((void *)dest, src_size): SUCCESS
[memcpy.pointer_primitives.6] line 15 deallocated dynamic object in W_OK((void *)dest, src_size): SUCCESS
[memcpy.pointer_primitives.7] line 15 dead object in W_OK((void *)dest, src_size): SUCCESS
[memcpy.pointer_primitives.8] line 15 pointer outside object bounds in W_OK((void *)dest, src_size): FAILURE
[memcpy.assertion.1] line 25 assertion havoc_slice W_OK(dst, n): SUCCESS
** 2 of 14 failed (3 iterations)
VERIFICATION FAILED
All CPROVER library functions check pointer validity using __CPROVER_r_ok(src,n). These preconditions do not seem to trigger --pointer-primitive-checks (likely because the library is linked after pointer primitive checks instantiation)
However, the preconditions written in user stubs (or function and loop contracts) do trigger --pointer-primitive-checks and cause failures.
The failures are due to pointers resulting from char *src = malloc(0); causing pointer outside object bounds errors on statements like __CPROVER_precondition(__CPROVER_r_ok(src, 0));.
This is what the C11 standard says in section 7.21.1 about string function conventions:
Where an argument declared as size_t n specifies the length of the array for a
function, n can have the value zero on a call to that function. Unless explicitly stated
otherwise in the description of a particular function in this subclause, pointer arguments
on such a call shall still have valid values, as described in 7.1.4. On such a call, a
function that locates a character finds no occurrence, a function that compares two
character sequences returns zero, and a function that copies characters copies zero
characters.
And 7.1.4 says the following:
If an argument to a function has an invalid value (such as a value outside the domain
of the function, or a pointer outside the address space of the program, or a null pointer,
or a pointer to non-modifiable storage when the corresponding parameter is not const-qualified)
or a type (after promotion) not expected by a function with variable number of arguments,
the behavior is undefined.
If I understand the standard correctly, if malloc(0) does not return NULL, the pointer should be considered as valid and should not cause UB in string functions as long as the n parameter is 0.
This in turn leads me to think that pointer primitive checks should not fail on __CPROVER_r_ok(ptr, 0) when ptr is a non-NULL value returned by malloc(0).
One way around it could be to disable the checks using #pragmas CPROVER disable "pointer-primitive" or writing preconditions as size == 0 || __CPROVER_r_ok(src, size) everywhere, but this is very cumbersome.
How about modifying pointer primitive checks to accept cases that the C standard says are acceptable ?