From b1bb5dce292ee9f5d8f6f11aa843457052669501 Mon Sep 17 00:00:00 2001 From: Lindsay Stewart Date: Tue, 12 Mar 2024 16:03:18 -0700 Subject: [PATCH] refactor: make memmove vs memcpy behavior clearer (#4447) --- scripts/s2n_safety_macros.py | 2 +- tests/cbmc/proofs/s2n_alloc/Makefile | 2 +- tests/cbmc/proofs/s2n_array_init/Makefile | 2 +- tests/cbmc/proofs/s2n_array_new/Makefile | 2 +- tests/cbmc/proofs/s2n_set_new/Makefile | 2 +- tests/cbmc/proofs/s2n_stuffer_alloc/Makefile | 2 +- .../s2n_stuffer_growable_alloc/Makefile | 2 +- .../s2n_stuffer_resize_if_empty/Makefile | 2 +- tests/cbmc/stubs/s2n_ensure.c | 2 +- tests/features/S2N___RESTRICT__SUPPORTED.c | 27 ---------------- .../features/S2N___RESTRICT__SUPPORTED.flags | 1 - tests/sidetrail/working/stubs/s2n_ensure.h | 5 ++- utils/s2n_ensure.c | 2 +- utils/s2n_ensure.h | 32 +++++-------------- utils/s2n_safety_macros.h | 6 ++-- 15 files changed, 25 insertions(+), 66 deletions(-) delete mode 100644 tests/features/S2N___RESTRICT__SUPPORTED.c delete mode 100644 tests/features/S2N___RESTRICT__SUPPORTED.flags diff --git a/scripts/s2n_safety_macros.py b/scripts/s2n_safety_macros.py index fbd5a5d977b..9ca973eeca8 100644 --- 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 index 92c2fd07206..7b6c5821968 100644 --- 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 index 8f740b51045..48477fd21be 100644 --- 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 index 389c7f0192c..6cd64107a73 100644 --- 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 index 6322ae4ce0e..5cf2f575ea5 100644 --- 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 index 59795b1e168..db954284f82 100644 --- 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 index 48ca5bebc0a..4a11bcc8189 100644 --- 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 index daac401569b..41b69d86b55 100644 --- 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 index 01ff888062f..ae0e5a82c47 100644 --- 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 deleted file mode 100644 index b29c32ef9ad..00000000000 --- a/tests/features/S2N___RESTRICT__SUPPORTED.c +++ /dev/null @@ -1,27 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * - * Licensed under the Apache License, Version 2.0 (the "License"). - * You may not use this file except in compliance with the License. - * A copy of the License is located at - * - * http://aws.amazon.com/apache2.0 - * - * or in the "license" file accompanying this file. This file is distributed - * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either - * express or implied. See the License for the specific language governing - * permissions and limitations under the License. - */ - -void swap(int *__restrict__ left, int *__restrict__ right) { - int temp = *left; - *left = *right; - *right = temp; -} - -int main() { - int a = 1, b = 2; - swap(&a, &b); - return 0; -} - diff --git a/tests/features/S2N___RESTRICT__SUPPORTED.flags b/tests/features/S2N___RESTRICT__SUPPORTED.flags deleted file mode 100644 index 2f41be663b2..00000000000 --- a/tests/features/S2N___RESTRICT__SUPPORTED.flags +++ /dev/null @@ -1 +0,0 @@ --Werror diff --git a/tests/sidetrail/working/stubs/s2n_ensure.h b/tests/sidetrail/working/stubs/s2n_ensure.h index 521e3e56f55..179f5a52b19 100644 --- 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 index 5824f9b6186..c2350740462 100644 --- 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 index c072d93e952..890cca162b5 100644 --- 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 index 33e5133dca4..e3896e8c360 100644 --- 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.