refactor: make memmove vs memcpy behavior clearer (#4447)

lrstewart · web-flow · commit b1bb5dce292e · 2024-03-12T16:03:18.000-07:00
diff --git a/scripts/s2n_safety_macros.py b/scripts/s2n_safety_macros.py
@@ -539,7 +539,7 @@ def cmp_check(op):
         * The size of the data pointed to by both the `destination` and `source` parameters,
           shall be at least `len` bytes.
         ''',
-        impl='__S2N_ENSURE_SAFE_MEMCPY((destination), (source), (len), {prefix}ENSURE_REF)',
+        impl='__S2N_ENSURE_SAFE_MEMMOVE((destination), (source), (len), {prefix}ENSURE_REF)',
         harness='''
         static {ret} {prefix}CHECKED_MEMCPY_harness(uint32_t* dest, uint32_t* source, size_t len)
         {{
diff --git a/tests/cbmc/proofs/s2n_alloc/Makefile b/tests/cbmc/proofs/s2n_alloc/Makefile
@@ -40,7 +40,7 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
 # We abstract these functions because manual inspection demonstrates they are unreachable.
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
 REMOVE_FUNCTION_BODY += s2n_blob_slice
-REMOVE_FUNCTION_BODY += s2n_ensure_memcpy_trace
+REMOVE_FUNCTION_BODY += s2n_ensure_memmove_trace
 
 UNWINDSET +=
 
diff --git a/tests/cbmc/proofs/s2n_array_init/Makefile b/tests/cbmc/proofs/s2n_array_init/Makefile
@@ -35,7 +35,7 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 # We abstract these functions because manual inspection demonstrates they are unreachable.
 REMOVE_FUNCTION_BODY += s2n_blob_slice
-REMOVE_FUNCTION_BODY += s2n_ensure_memcpy_trace
+REMOVE_FUNCTION_BODY += s2n_ensure_memmove_trace
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
 
 UNWINDSET +=
diff --git a/tests/cbmc/proofs/s2n_array_new/Makefile b/tests/cbmc/proofs/s2n_array_new/Makefile
@@ -38,7 +38,7 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 # We abstract these functions because manual inspection demonstrates they are unreachable.
 REMOVE_FUNCTION_BODY += s2n_blob_slice
-REMOVE_FUNCTION_BODY += s2n_ensure_memcpy_trace
+REMOVE_FUNCTION_BODY += s2n_ensure_memmove_trace
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
 
 UNWINDSET +=
diff --git a/tests/cbmc/proofs/s2n_set_new/Makefile b/tests/cbmc/proofs/s2n_set_new/Makefile
@@ -42,7 +42,7 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_set.c
 
 # We abstract these functions because manual inspection demonstrates they are unreachable.
 REMOVE_FUNCTION_BODY += s2n_blob_slice
-REMOVE_FUNCTION_BODY += s2n_ensure_memcpy_trace
+REMOVE_FUNCTION_BODY += s2n_ensure_memmove_trace
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
 
 UNWINDSET +=
diff --git a/tests/cbmc/proofs/s2n_stuffer_alloc/Makefile b/tests/cbmc/proofs/s2n_stuffer_alloc/Makefile
@@ -40,7 +40,7 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 # We abstract these functions because manual inspection demonstrates they are unreachable.
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
 REMOVE_FUNCTION_BODY += s2n_blob_slice
-REMOVE_FUNCTION_BODY += s2n_ensure_memcpy_trace
+REMOVE_FUNCTION_BODY += s2n_ensure_memmove_trace
 
 UNWINDSET +=
 
diff --git a/tests/cbmc/proofs/s2n_stuffer_growable_alloc/Makefile b/tests/cbmc/proofs/s2n_stuffer_growable_alloc/Makefile
@@ -38,7 +38,7 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 # We abstract these functions because manual inspection demonstrates they are unreachable.
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
 REMOVE_FUNCTION_BODY += s2n_blob_slice
-REMOVE_FUNCTION_BODY += s2n_ensure_memcpy_trace
+REMOVE_FUNCTION_BODY += s2n_ensure_memmove_trace
 
 UNWINDSET +=
 
diff --git a/tests/cbmc/proofs/s2n_stuffer_resize_if_empty/Makefile b/tests/cbmc/proofs/s2n_stuffer_resize_if_empty/Makefile
@@ -35,7 +35,7 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
 # We abstract these functions because manual inspection demonstrates they are unreachable.
 REMOVE_FUNCTION_BODY += s2n_calculate_stacktrace
 REMOVE_FUNCTION_BODY += s2n_blob_slice
-REMOVE_FUNCTION_BODY += s2n_ensure_memcpy_trace
+REMOVE_FUNCTION_BODY += s2n_ensure_memmove_trace
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
 
 UNWINDSET +=
diff --git a/tests/cbmc/stubs/s2n_ensure.c b/tests/cbmc/stubs/s2n_ensure.c
@@ -15,7 +15,7 @@
 
 #include "utils/s2n_safety.h"
 
-void* s2n_ensure_memcpy_trace(void *restrict to, const void *restrict from, size_t size)
+void* s2n_ensure_memmove_trace(void *to, const void *from, size_t size)
 {
     if (to == NULL || from == NULL) {
         return NULL;
diff --git a/tests/features/S2N___RESTRICT__SUPPORTED.c b/tests/features/S2N___RESTRICT__SUPPORTED.c
diff --git a/tests/features/S2N___RESTRICT__SUPPORTED.flags b/tests/features/S2N___RESTRICT__SUPPORTED.flags
diff --git a/tests/sidetrail/working/stubs/s2n_ensure.h b/tests/sidetrail/working/stubs/s2n_ensure.h
@@ -31,7 +31,10 @@ void *s2n_sidetrail_memset(void * ptr, int value, size_t num);
 #define __S2N_ENSURE_PRECONDITION( result )                S2N_RESULT_OK
 #define __S2N_ENSURE_POSTCONDITION( result )               S2N_RESULT_OK
 
-#define __S2N_ENSURE_SAFE_MEMCPY( d , s , n , guard )      do { memcpy((d), (s), (n)); } while(0)
+/* memmove isn't supported, so use memcpy instead.
+ * For the purposes of these proofs, there should be no useful difference.
+ */
+#define __S2N_ENSURE_SAFE_MEMMOVE( d , s , n , guard )      do { memcpy((d), (s), (n)); } while(0)
 
 #define __S2N_ENSURE_SAFE_MEMSET( d , c , n , guard )      \
   do {                                                     \
diff --git a/utils/s2n_ensure.c b/utils/s2n_ensure.c
@@ -15,7 +15,7 @@
 
 #include "utils/s2n_safety.h"
 
-void *s2n_ensure_memcpy_trace(void *restrict to, const void *restrict from, size_t size)
+void *s2n_ensure_memmove_trace(void *to, const void *from, size_t size)
 {
     PTR_ENSURE_REF(to);
     PTR_ENSURE_REF(from);
diff --git a/utils/s2n_ensure.h b/utils/s2n_ensure.h
@@ -60,13 +60,13 @@
     #define __S2N_ENSURE_POSTCONDITION(result) (s2n_likely(s2n_result_is_ok(result)) ? S2N_RESULT_OK : S2N_RESULT_ERROR)
 #endif
 
-#define __S2N_ENSURE_SAFE_MEMCPY(d, s, n, guard)                    \
-    do {                                                            \
-        __typeof(n) __tmp_n = (n);                                  \
-        if (s2n_likely(__tmp_n)) {                                  \
-            void *r = s2n_ensure_memcpy_trace((d), (s), (__tmp_n)); \
-            guard(r);                                               \
-        }                                                           \
+#define __S2N_ENSURE_SAFE_MEMMOVE(d, s, n, guard)                    \
+    do {                                                             \
+        __typeof(n) __tmp_n = (n);                                   \
+        if (s2n_likely(__tmp_n)) {                                   \
+            void *r = s2n_ensure_memmove_trace((d), (s), (__tmp_n)); \
+            guard(r);                                                \
+        }                                                            \
     } while (0)
 
 #define __S2N_ENSURE_SAFE_MEMSET(d, c, n, guard) \
@@ -90,23 +90,7 @@
     #define __S2N_ENSURE_CHECKED_RETURN(v) return v
 #endif
 
-/**
- * `restrict` is a part of the c99 standard and will work with any C compiler. If you're trying to
- * compile with a C++ compiler `restrict` is invalid. However some C++ compilers support the behavior
- * of `restrict` using the `__restrict__` keyword. Therefore if the compiler supports `__restrict__`
- * use it.
- *
- * This is helpful for the benchmarks in tests/benchmark which use Google's Benchmark library and
- * are all written in C++.
- *
- * https://gcc.gnu.org/onlinedocs/gcc/Restricted-Pointers.html
- *
- */
-#if defined(S2N___RESTRICT__SUPPORTED)
-void *s2n_ensure_memcpy_trace(void *__restrict__ to, const void *__restrict__ from, size_t size);
-#else
-void *s2n_ensure_memcpy_trace(void *restrict to, const void *restrict from, size_t size);
-#endif
+void *s2n_ensure_memmove_trace(void *to, const void *from, size_t size);
 
 /**
  * These macros should not be used in validate functions.
diff --git a/utils/s2n_safety_macros.h b/utils/s2n_safety_macros.h
@@ -161,7 +161,7 @@
  * * The size of the data pointed to by both the `destination` and `source` parameters,
  *   shall be at least `len` bytes.
  */
-#define RESULT_CHECKED_MEMCPY(destination, source, len)        __S2N_ENSURE_SAFE_MEMCPY((destination), (source), (len), RESULT_ENSURE_REF)
+#define RESULT_CHECKED_MEMCPY(destination, source, len)        __S2N_ENSURE_SAFE_MEMMOVE((destination), (source), (len), RESULT_ENSURE_REF)
 
 /**
  * Performs a safer memset
@@ -357,7 +357,7 @@
  * * The size of the data pointed to by both the `destination` and `source` parameters,
  *   shall be at least `len` bytes.
  */
-#define POSIX_CHECKED_MEMCPY(destination, source, len)        __S2N_ENSURE_SAFE_MEMCPY((destination), (source), (len), POSIX_ENSURE_REF)
+#define POSIX_CHECKED_MEMCPY(destination, source, len)        __S2N_ENSURE_SAFE_MEMMOVE((destination), (source), (len), POSIX_ENSURE_REF)
 
 /**
  * DEPRECATED: all methods (except those in s2n.h) should return s2n_result.
@@ -563,7 +563,7 @@
  * * The size of the data pointed to by both the `destination` and `source` parameters,
  *   shall be at least `len` bytes.
  */
-#define PTR_CHECKED_MEMCPY(destination, source, len)          __S2N_ENSURE_SAFE_MEMCPY((destination), (source), (len), PTR_ENSURE_REF)
+#define PTR_CHECKED_MEMCPY(destination, source, len)          __S2N_ENSURE_SAFE_MEMMOVE((destination), (source), (len), PTR_ENSURE_REF)
 
 /**
  * DEPRECATED: all methods (except those in s2n.h) should return s2n_result.

Original file line number	Diff line number	Diff line change
`@@ -15,7 +15,7 @@`
`15`	`15`
`16`	`16`	`#include "utils/s2n_safety.h"`
`17`	`17`
`18`		`-void* s2n_ensure_memcpy_trace(void restrict to, const void restrict from, size_t size)`
	`18`	`+void* s2n_ensure_memmove_trace(void to, const void from, size_t size)`
`19`	`19`	`{`
`20`	`20`	`if (to == NULL \|\| from == NULL) {`
`21`	`21`	`return NULL;`