memcpy fails to warn when called on invalid pointer

[danielsn]

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


int main (void) {
  int d;
  void* s = malloc(0);
  memcpy(&d,s,0);
  memcpy(s,&d,0);
}

╰─$ cbmc test.c                                                                                                                                      10 ↵
CBMC version 5.14.1 (cbmc-5.14.1) 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
file test.c line 8 function main: function 'memcpy' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-memcpy> line 9: error: implicit function declaration 'memcpy'
old definition in module 'test' file test.c line 8 function main
signed int (void)
new definition in module '<built-in-library>' file <builtin-library-memcpy> line 9
void * (void *dst, const void *src, size_t n)
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: 111 steps
simple slicing removed 0 assignments
Generated 6 VCC(s), 0 remaining after simplification

** 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

test.c function main
[main.precondition_instance.1] line 8 memcpy src/dst overlap: SUCCESS
[main.precondition_instance.2] line 8 memcpy source region readable: SUCCESS
[main.precondition_instance.3] line 8 memcpy destination region writeable: SUCCESS
[main.precondition_instance.4] line 9 memcpy src/dst overlap: SUCCESS
[main.precondition_instance.5] line 9 memcpy source region readable: SUCCESS
[main.precondition_instance.6] line 9 memcpy destination region writeable: SUCCESS

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

I expected that the result of malloc(0) would be either null, or an invalid pointer, and that memcpy would reject it as per https://www.imperialviolet.org/2016/06/26/nonnull.html

Instead, it passes.

[martin-cs]

I think the key point is ISO-9899 (1999) 7.20.3(1):

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.

I don't think that CBMC ever specifies which choice it implements but in practice it is the second. I would hope that turning on --pointer-check would catch attempts to dereference the pointer. I think __CPROVER_w_ok and __CPROVER_r_ok should fail for an allocated object of zero size but at the moment they don't.

I think there is a separate question, as discussed by the link, of whether memcpy(p,q,0) should actually do the checks or if it should just exit.

[hannes-steffenhagen-diffblue]

As @martin-cs says malloc does return a non-null pointer but it’s not writable or readable. The library checks don’t check for this by default. memcpy passes here because you’re reading and writing nothing, which is a valid thing to do even if a non-zero read or write would not be.

This reports failures like you’d expect:

#include <stdlib.h>
#include <string.h>

int main(void) {
  int* mem = malloc(0);
  *mem = 10;
  int x = 10;
  memcpy(mem, &x, sizeof(int));
  memcpy(&x, mem, sizeof(int));
  free(mem);
  return 0;
}

@danielsn I’d expect things to behave this way, can you elaborate on what you think the erroneous behaviour is and what you’d want to happen instead?

[feliperodri]

@danielsn is that still a problem since #5518 got merged? @hannes-steffenhagen-diffblue any updates? Should we close this issue?

[jimgrundy]

This seems OK as is to me. This example dates from a time when our malloc always returned non-null pointers. These days the example would (should?) fail because I expect that we check that the source and destination pointers are non-null (the readable and writable check should do that even if size is 0). Assuming that they are non-null I would expect that they should also be considered to be readable (writable) for a range of 0 bytes and all would be considered good.

[jimgrundy]

Agreed that this isn't an issue. We may file a documentation issue.