Preconditions of cbmc library function memcpy are too strong

[qinheping]

I got failure "memcpy source region readable" when I call memcpy(p,q,0) where q is an overflowing pointer (this happened in a c-common benchmark https://github.com/awslabs/aws-c-common/blob/main/source/array_list.c#L187). However, as the number of bytes we want to copy is 0, this call will not cause any memory safety problem.

When I looked the cbmc library function memcpy, I found that, even though the function body will be executed only when n (the number of bytes we want to copy) is greater than 0, the preconditions do not exclude the case of n==0.

cbmc/src/ansi-c/library/string.c

Line 609 in d8296bd

void *memcpy(void *dst, const void *src, size_t n)

cbmc/src/ansi-c/library/string.c

Line 655 in d8296bd

void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __CPROVER_size_t size)

Modifying the preconditions to implications with premise n != 0 can avoid such false-negative error. For example, the preconditions of memcpy can be following.

  __CPROVER_precondition(
    n == 0 || (__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(
    n == 0 || (__CPROVER_r_ok(src, n)), "memcpy source region readable");
  __CPROVER_precondition(
    n == 0 || (__CPROVER_w_ok(dst, n)), "memcpy destination region writeable");

[kroening]

I am afraid that the behaviour of memcpy is undefined when either p or q are invalid, irrespectively of the value of n.

[kroening]

The wording in C99 is as follows (7.21.1 par 2):

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.

[jimgrundy]

Hey @Herbping, can you give us trace to look at or an example complete enough for us to reproduce so we can see just how messed up the pointer in question is? Maybe it's right at that knife edge where it is 1 past the size of the array, or the array is of size 0, in which case we might want allow that.

[qinheping]

The failure can be reproduced by running unbounded proof for the benchmark array_list_swap.
To run the unbounded proof, you need to

1. Clone the branch https://github.com/Herbping/aws-c-common/tree/unbounded_proofs/verification/cbmc/proofs/aws_array_list_swap., update all submodules;
2. make veryclean && make at the directory verification/cbmc/proofs/aws_array_list_swap

In the unbounded proof, I annotated the loop https://github.com/Herbping/aws-c-common/blob/unbounded_proofs/source/array_list.c#L178 with invariants and apply the invariants. I also removed the bound of length of array list, and set the bound of item_size to be 128 to make sure that we enter the loop.

In the trace that violated the check "memcpy source region readable", the length of array is 281474976710656ul, which is 2^48. Upon the entry of the loop, the pointer item1 was 128 bytes from overflowing.

State 1071 file /Users/qinhh/Repos/aws-c-common/source/array_list.c function aws_array_list_swap line 211 thread 0
----------------------------------------------------
  item1=(const void *)(dynamic_object1 + 36028797018963840l) (00000111 01111111 11111111 11111111 11111111 11111111 11111111 10000000)

State 1072 file /Users/qinhh/Repos/aws-c-common/source/array_list.c function aws_array_list_swap line 211 thread 0
----------------------------------------------------
  item2=(const void *)(dynamic_object1 + 27021597764222848l) (00000111 01011111 11111111 11111111 11111111 11111111 11111111 10000000)

State 1073 file /Users/qinhh/Repos/aws-c-common/source/array_list.c function aws_array_list_swap line 211 thread 0
----------------------------------------------------
  item_size=128ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 10000000)

State 1076 file /Users/qinhh/Repos/aws-c-common/source/array_list.c function aws_array_list_mem_swap line 176 thread 0
----------------------------------------------------
  slice_count=0ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1077 file /Users/qinhh/Repos/aws-c-common/source/array_list.c function aws_array_list_mem_swap line 176 thread 0
----------------------------------------------------
  slice_count=1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)

In the loop body, we add a slice (128) to both pointers item1 and item2. So, when we exited the loop, the pointer item1 overflowed and became invalid, and hence failed the preconditions in memcmp.

State 1117 file /Users/qinhh/Repos/aws-c-common/source/array_list.c function aws_array_list_mem_swap line 178 thread 0
----------------------------------------------------
  item1=(const void *)(dynamic_object1 + -36028797018963968l) (00000111 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1119 file /Users/qinhh/Repos/aws-c-common/source/array_list.c function aws_array_list_mem_swap line 178 thread 0
----------------------------------------------------
  item2=(const void *)(dynamic_object1 + 27021597764222976l) (00000111 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1121 file /Users/qinhh/Repos/aws-c-common/source/array_list.c function aws_array_list_mem_swap line 178 thread 0
----------------------------------------------------
  i=1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)

Violated property:
  file /Users/qinhh/Repos/aws-c-common/source/array_list.c function aws_array_list_mem_swap line 178 thread 0
  pointer outside object bounds in POINTER_OBJECT(item1)
  i <= slice_count ==> POINTER_OBJECT(NULL) == POINTER_OBJECT(item1) || POINTER_OFFSET(item1) >= 0l && OBJECT_SIZE(item1) >= (unsigned long int)POINTER_OFFSET(item1) + 1ul


Assumption:
  file /Users/qinhh/Repos/aws-c-common/source/array_list.c line 178 function aws_array_list_mem_swap
  i <= slice_count && POINTER_OBJECT(item1) == POINTER_OBJECT(tmp_cc) && POINTER_OBJECT(item2) == POINTER_OBJECT(tmp_cc$0) && item1 == tmp_cc + (signed long int)(i * (unsigned long int)128) && item2 == tmp_cc$0 + (signed long int)(i * (unsigned long int)128)

State 1156 file /Users/qinhh/Repos/aws-c-common/source/array_list.c function aws_array_list_mem_swap line 192 thread 0
----------------------------------------------------
  remainder=0ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1157 file /Users/qinhh/Repos/aws-c-common/source/array_list.c function aws_array_list_mem_swap line 192 thread 0
----------------------------------------------------
  remainder=0ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

Violated property:
  file /Users/qinhh/Repos/aws-c-common/source/array_list.c function aws_array_list_mem_swap line 193 thread 0
  memcpy source region readable
  (FALSE || !(POINTER_OBJECT((void *)item1) == POINTER_OBJECT(NULL))) && !IS_INVALID_POINTER((void *)item1) && (FALSE || !(POINTER_OBJECT((void *)item1) == POINTER_OBJECT(__CPROVER_deallocated))) && (FALSE || !(POINTER_OBJECT((void *)item1) == POINTER_OBJECT(__CPROVER_dead_object))) && (FALSE || !(POINTER_OFFSET((void *)item1) < 0l || (size_t)POINTER_OFFSET((void *)item1) + remainder > OBJECT_SIZE((void *)item1))) && (POINTER_OBJECT(NULL) == POINTER_OBJECT((void *)item1) && NULL != (void *)item1 ==> FALSE)

[jimgrundy]

So, I think the following....
1/ You should be able to remove the "n == 0" clauses from this precondition.
2/ I wish there was a way to say that the src and dst fields must be valid pointers, but we kind of don't need to because wether you add "is_valid_pointer(src)" to the precondition or not the effect is the same - an error (precondition violation or touching a bad pointer).
3/ I think you are going to have to go back and add preconditions/invariants to keep the pointers from overflowing.
Does that seem possible?

[qinheping]

I created a pull request awslabs/aws-c-common#874 to avoid calling memcpy when pointers one past the boundaries.