memcpy/strncpy/strncat overlap check now allows single object

Fixes #3482
2018-11-30 07:30:16 -08:00 · 2018-11-30 07:30:16 -08:00 · e0946d17af
parent c0ff0d0353
commit e0946d17af
4 changed files with 255 additions and 200 deletions
--- a/regression/cbmc-library/memcpy-02/memcpy4.c
+++ b/regression/cbmc-library/memcpy-02/memcpy4.c
@ -0,0 +1,18 @@
+#include <string.h>
+
+int main()
+{
+  char bufferA[10], bufferB[10];
+
+  // ok
+  memcpy(bufferA, bufferB, 10);
+
+  // not ok, overlap, should use memmove
+  memcpy(bufferA, bufferA + 1, 9);
+
+  // ok, no overlap
+  memcpy(bufferA, bufferA + 5, 5);
+
+  // out of bounds
+  memcpy(bufferA + 1, bufferB, 10);
+}
--- a/regression/cbmc-library/memcpy-02/memcpy4.desc
+++ b/regression/cbmc-library/memcpy-02/memcpy4.desc
@ -0,0 +1,13 @@
+CORE
+memcpy4.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^\[.*] line 8 memcpy src/dst overlap: SUCCESS$
+^\[.*] line 11 memcpy src/dst overlap: FAILURE$
+^\[.*] line 14 memcpy src/dst overlap: SUCCESS$
+^\[.*] line 17 memcpy src/dst overlap: SUCCESS$
+^\[.*] line 17 memcpy destination region writeable: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
--- a/scripts/delete_failing_smt2_solver_tests
+++ b/scripts/delete_failing_smt2_solver_tests
@ -139,6 +139,7 @@ rm havoc_object1/test.desc
 rm hex_trace/test.desc
 rm integer-assignments1/test.desc
 rm little-endian-array1/test.desc
+rm memcpy/memcpy4.desc
 rm memory_allocation1/test.desc
 rm memset1/test.desc
 rm mm_io1/test.desc
--- a/src/ansi-c/library/string.c
+++ b/src/ansi-c/library/string.c
@ -3,19 +3,22 @@
 inline char *__builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t s)
 {
 __CPROVER_HIDE:;
+
 #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_precondition(__CPROVER_is_zero_string(src),
-                         "strcpy zero-termination of 2nd argument");
-  __CPROVER_precondition(__CPROVER_buffer_size(dst)>__CPROVER_zero_string_length(src),
+  __CPROVER_precondition(
+    __CPROVER_is_zero_string(src), "strcpy zero-termination of 2nd argument");
+  __CPROVER_precondition(
+    __CPROVER_buffer_size(dst) > __CPROVER_zero_string_length(src),
    "strcpy buffer overflow");
-  __CPROVER_precondition(__CPROVER_buffer_size(dst)==s,
-                         "builtin object size");
+  __CPROVER_precondition(
+    __CPROVER_buffer_size(dst) == s, "builtin object size");
  dst[__CPROVER_zero_string_length(src)] = 0;
  __CPROVER_is_zero_string(dst) = 1;
  __CPROVER_zero_string_length(dst) = __CPROVER_zero_string_length(src);
 #else
-  __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
-                         __CPROVER_POINTER_OBJECT(src),
+  __CPROVER_precondition(
+    __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
+      (src >= dst + s) || (dst >= src + s),
    "strcpy src/dst overlap");
  __CPROVER_size_t i = 0;
  char ch;
@ -24,8 +27,7 @@ inline char *__builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t
    ch = src[i];
    dst[i] = ch;
    i++;
-  }
-  while(i<s && ch!=(char)0);
+  } while(i < s && ch != (char)0);
 #endif
  return dst;
 }
@ -35,17 +37,19 @@ inline char *__builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t
 __inline char *__builtin___strcat_chk(char *dst, const char *src, __CPROVER_size_t s)
 {
 __CPROVER_HIDE:;
+
 #ifdef __CPROVER_STRING_ABSTRACTION
  __CPROVER_size_t new_size;
-  __CPROVER_precondition(__CPROVER_is_zero_string(dst),
-                         "strcat zero-termination of 1st argument");
-  __CPROVER_precondition(__CPROVER_is_zero_string(src),
-                         "strcat zero-termination of 2nd argument");
-  __CPROVER_precondition(__CPROVER_buffer_size(dst)==s,
-                         "builtin object size");
-  new_size=__CPROVER_zero_string_length(dst)+__CPROVER_zero_string_length(src);
-  __CPROVER_assert(__CPROVER_buffer_size(dst)>new_size,
-                   "strcat buffer overflow");
+  __CPROVER_precondition(
+    __CPROVER_is_zero_string(dst), "strcat zero-termination of 1st argument");
+  __CPROVER_precondition(
+    __CPROVER_is_zero_string(src), "strcat zero-termination of 2nd argument");
+  __CPROVER_precondition(
+    __CPROVER_buffer_size(dst) == s, "builtin object size");
+  new_size =
+    __CPROVER_zero_string_length(dst) + __CPROVER_zero_string_length(src);
+  __CPROVER_assert(
+    __CPROVER_buffer_size(dst) > new_size, "strcat buffer overflow");
  __CPROVER_size_t old_size = __CPROVER_zero_string_length(dst);
  //"  for(size_t i=0; i<__CPROVER_zero_string_length(src); i++)
  //"    dst[old_size+i];
@ -53,11 +57,13 @@ __inline char *__builtin___strcat_chk(char *dst, const char *src, __CPROVER_size
  __CPROVER_is_zero_string(dst) = 1;
  __CPROVER_zero_string_length(dst) = new_size;
 #else
-  __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
-                         __CPROVER_POINTER_OBJECT(src),
+  __CPROVER_precondition(
+    __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
+      (src >= dst + s) || (dst >= src + s),
    "strcat src/dst overlap");
  __CPROVER_size_t i = 0;
-  while(dst[i]!=0) i++;
+  while(dst[i] != 0)
+    i++;

  __CPROVER_size_t j = 0;
  char ch = 1;
@ -79,17 +85,19 @@ __inline char *__builtin___strncat_chk(
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
  __CPROVER_size_t additional, new_size;
-  __CPROVER_precondition(__CPROVER_is_zero_string(dst),
-                         "strncat zero-termination of 1st argument");
-  __CPROVER_precondition(__CPROVER_is_zero_string(src) ||
-                         __CPROVER_buffer_size(src)>=n,
+  __CPROVER_precondition(
+    __CPROVER_is_zero_string(dst), "strncat zero-termination of 1st argument");
+  __CPROVER_precondition(
+    __CPROVER_is_zero_string(src) || __CPROVER_buffer_size(src) >= n,
    "strncat zero-termination of 2nd argument");
-  __CPROVER_precondition(__CPROVER_buffer_size(dst)==s,
-                         "builtin object size");
-  additional=(n<__CPROVER_zero_string_length(src))?n:__CPROVER_zero_string_length(src);
+  __CPROVER_precondition(
+    __CPROVER_buffer_size(dst) == s, "builtin object size");
+  additional = (n < __CPROVER_zero_string_length(src))
+                 ? n
+                 : __CPROVER_zero_string_length(src);
  new_size = __CPROVER_is_zero_string(dst) + additional;
-  __CPROVER_assert(__CPROVER_buffer_size(dst)>new_size,
-                   "strncat buffer overflow");
+  __CPROVER_assert(
+    __CPROVER_buffer_size(dst) > new_size, "strncat buffer overflow");
  __CPROVER_size_t dest_len = __CPROVER_zero_string_length(dst);
  __CPROVER_size_t i;
  for(i = 0; i < n && i < __CPROVER_zero_string_length(src); i++)
@ -98,8 +106,9 @@ __inline char *__builtin___strncat_chk(
  __CPROVER_is_zero_string(dst) = 1;
  __CPROVER_zero_string_length(dst) = new_size;
 #else
-  __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
-                         __CPROVER_POINTER_OBJECT(src),
+  __CPROVER_precondition(
+    __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
+      (src >= dst + s) || (dst >= src + s),
    "strncat src/dst overlap");

  __CPROVER_size_t i = 0;
@ -131,17 +140,17 @@ inline char *strcpy(char *dst, const char *src)
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_precondition(__CPROVER_is_zero_string(src),
-                         "strcpy zero-termination of 2nd argument");
-  __CPROVER_precondition(__CPROVER_buffer_size(dst)>
-                         __CPROVER_zero_string_length(src),
+  __CPROVER_precondition(
+    __CPROVER_is_zero_string(src), "strcpy zero-termination of 2nd argument");
+  __CPROVER_precondition(
+    __CPROVER_buffer_size(dst) > __CPROVER_zero_string_length(src),
    "strcpy buffer overflow");
  dst[__CPROVER_zero_string_length(src)] = 0;
  __CPROVER_is_zero_string(dst) = 1;
  __CPROVER_zero_string_length(dst) = __CPROVER_zero_string_length(src);
 #else
-  __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
-                         __CPROVER_POINTER_OBJECT(src),
+  __CPROVER_precondition(
+    __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src),
    "strcpy src/dst overlap");
  __CPROVER_size_t i = 0;
  char ch;
@ -150,8 +159,7 @@ inline char *strcpy(char *dst, const char *src)
    ch = src[i];
    dst[i] = ch;
    i++;
-  }
-  while(ch!=(char)0);
+  } while(ch != (char)0);
 #endif
  return dst;
 }
@ -169,15 +177,16 @@ inline char *strncpy(char *dst, const char *src, size_t n)
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_precondition(__CPROVER_is_zero_string(src),
-                         "strncpy zero-termination of 2nd argument");
-  __CPROVER_precondition(__CPROVER_buffer_size(dst)>=n,
-                         "strncpy buffer overflow");
+  __CPROVER_precondition(
+    __CPROVER_is_zero_string(src), "strncpy zero-termination of 2nd argument");
+  __CPROVER_precondition(
+    __CPROVER_buffer_size(dst) >= n, "strncpy buffer overflow");
  __CPROVER_is_zero_string(dst) = __CPROVER_zero_string_length(src) < n;
  __CPROVER_zero_string_length(dst) = __CPROVER_zero_string_length(src);
 #else
-  __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
-                         __CPROVER_POINTER_OBJECT(src),
+  __CPROVER_precondition(
+    __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
+      (src >= dst + n) || (dst >= src + n),
    "strncpy src/dst overlap");
  __CPROVER_size_t i = 0;
  char ch;
@ -206,17 +215,18 @@ inline char *__builtin___strncpy_chk(char *dst, const char *src, size_t n, size_
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_precondition(__CPROVER_is_zero_string(src),
-                         "strncpy zero-termination of 2nd argument");
-  __CPROVER_precondition(__CPROVER_buffer_size(dst)>=n,
-                         "strncpy buffer overflow");
-  __CPROVER_precondition(__CPROVER_buffer_size(dst)==object_size,
-                         "strncpy object size");
+  __CPROVER_precondition(
+    __CPROVER_is_zero_string(src), "strncpy zero-termination of 2nd argument");
+  __CPROVER_precondition(
+    __CPROVER_buffer_size(dst) >= n, "strncpy buffer overflow");
+  __CPROVER_precondition(
+    __CPROVER_buffer_size(dst) == object_size, "strncpy object size");
  __CPROVER_is_zero_string(dst) = __CPROVER_zero_string_length(src) < n;
  __CPROVER_zero_string_length(dst) = __CPROVER_zero_string_length(src);
 #else
-  __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
-                         __CPROVER_POINTER_OBJECT(src),
+  __CPROVER_precondition(
+    __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
+      (src >= dst + n) || (dst >= src + n),
    "strncpy src/dst overlap");
  __CPROVER_size_t i = 0;
  char ch;
@ -263,11 +273,12 @@ inline char *strcat(char *dst, const char *src)
  __CPROVER_is_zero_string(dst)=1;
  __CPROVER_zero_string_length(dst)=new_size;
 #else
-  __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
-                         __CPROVER_POINTER_OBJECT(src),
+  __CPROVER_precondition(
+    __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src),
    "strcat src/dst overlap");
  __CPROVER_size_t i = 0;
-  while(dst[i]!=0) i++;
+  while(dst[i] != 0)
+    i++;

  __CPROVER_size_t j = 0;
  char ch = 1;
@ -295,15 +306,17 @@ inline char *strncat(char *dst, const char *src, size_t n)
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
  __CPROVER_size_t additional, new_size;
-  __CPROVER_precondition(__CPROVER_is_zero_string(dst),
-                         "strncat zero-termination of 1st argument");
-  __CPROVER_precondition(__CPROVER_is_zero_string(src) ||
-                         __CPROVER_buffer_size(src)>=n,
+  __CPROVER_precondition(
+    __CPROVER_is_zero_string(dst), "strncat zero-termination of 1st argument");
+  __CPROVER_precondition(
+    __CPROVER_is_zero_string(src) || __CPROVER_buffer_size(src) >= n,
    "strncat zero-termination of 2nd argument");
-  additional=(n<__CPROVER_zero_string_length(src))?n:__CPROVER_zero_string_length(src);
+  additional = (n < __CPROVER_zero_string_length(src))
+                 ? n
+                 : __CPROVER_zero_string_length(src);
  new_size = __CPROVER_is_zero_string(dst) + additional;
-  __CPROVER_assert(__CPROVER_buffer_size(dst)>new_size,
-                   "strncat buffer overflow");
+  __CPROVER_assert(
+    __CPROVER_buffer_size(dst) > new_size, "strncat buffer overflow");
  __CPROVER_size_t dest_len = __CPROVER_zero_string_length(dst);
  __CPROVER_size_t i;
  for(i = 0; i < n && i < __CPROVER_zero_string_length(src); i++)
@ -312,8 +325,9 @@ inline char *strncat(char *dst, const char *src, size_t n)
  __CPROVER_is_zero_string(dst) = 1;
  __CPROVER_zero_string_length(dst) = new_size;
 #else
-  __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
-                         __CPROVER_POINTER_OBJECT(src),
+  __CPROVER_precondition(
+    __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
+      (src >= dst + n) || (dst >= src + n),
    "strncat src/dst overlap");

  __CPROVER_size_t i = 0;
@ -577,30 +591,35 @@ inline char *strdup(const char *str)

 void *memcpy(void *dst, const void *src, size_t n)
 {
-  __CPROVER_HIDE:
+__CPROVER_HIDE:;
+
 #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_precondition(__CPROVER_buffer_size(src)>=n,
-                         "memcpy buffer overflow");
-  __CPROVER_precondition(__CPROVER_buffer_size(dst)>=n,
-                         "memcpy buffer overflow");
+  __CPROVER_precondition(
+    __CPROVER_buffer_size(src) >= n, "memcpy buffer overflow");
+  __CPROVER_precondition(
+    __CPROVER_buffer_size(dst) >= n, "memcpy buffer overflow");
  //  for(size_t i=0; i<n ; i++) dst[i]=src[i];
-  if(__CPROVER_is_zero_string(src) &&
-     n > __CPROVER_zero_string_length(src))
+  if(__CPROVER_is_zero_string(src) && n > __CPROVER_zero_string_length(src))
  {
    __CPROVER_is_zero_string(dst) = 1;
    __CPROVER_zero_string_length(dst) = __CPROVER_zero_string_length(src);
  }
  else if(!(__CPROVER_is_zero_string(dst) &&
            n <= __CPROVER_zero_string_length(dst)))
+  {
    __CPROVER_is_zero_string(dst) = 0;
+  }
+
 #else
-  __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
-                         __CPROVER_POINTER_OBJECT(src),
+  __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");
+  __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)
  {
@ -610,6 +629,7 @@ void *memcpy(void *dst, const void *src, size_t n)
    __CPROVER_array_replace((char *)dst, src_n);
  }
 #endif
+
  return dst;
 }

@ -619,30 +639,33 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C
 {
 __CPROVER_HIDE:
 #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_precondition(__CPROVER_buffer_size(src)>=n,
-                         "memcpy buffer overflow");
-  __CPROVER_precondition(__CPROVER_buffer_size(dst)>=n,
-                         "memcpy buffer overflow");
-  __CPROVER_precondition(__CPROVER_buffer_size(dst)==s,
-                         "builtin object size");
+  __CPROVER_precondition(
+    __CPROVER_buffer_size(src) >= n, "memcpy buffer overflow");
+  __CPROVER_precondition(
+    __CPROVER_buffer_size(dst) >= n, "memcpy buffer overflow");
+  __CPROVER_precondition(
+    __CPROVER_buffer_size(dst) == s, "builtin object size");
  //  for(size_t i=0; i<n ; i++) dst[i]=src[i];
-  if(__CPROVER_is_zero_string(src) &&
-     n > __CPROVER_zero_string_length(src))
+  if(__CPROVER_is_zero_string(src) && n > __CPROVER_zero_string_length(src))
  {
    __CPROVER_is_zero_string(dst) = 1;
    __CPROVER_zero_string_length(dst) = __CPROVER_zero_string_length(src);
  }
  else if(!(__CPROVER_is_zero_string(dst) &&
            n <= __CPROVER_zero_string_length(dst)))
+  {
    __CPROVER_is_zero_string(dst) = 0;
+  }
 #else
-  __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!=
-                         __CPROVER_POINTER_OBJECT(src),
+  __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");
+  __CPROVER_precondition(
+    __CPROVER_r_ok(src, n), "memcpy source region readable");
+  __CPROVER_precondition(
+    __CPROVER_w_ok(dst, n), "memcpy destination region writeable");
  (void)size;

  if(n > 0)