1 /* 2 * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. 3 * 4 * Licensed under the Apache License, Version 2.0 (the "License"). 5 * You may not use this file except in compliance with the License. 6 * A copy of the License is located at 7 * 8 * http://aws.amazon.com/apache2.0 9 * 10 * or in the "license" file accompanying this file. This file is distributed 11 * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either 12 * express or implied. See the License for the specific language governing 13 * permissions and limitations under the License. 14 */ 15 16 #pragma once 17 18 #define s2n_likely(x) __builtin_expect(!!(x), 1) 19 #define s2n_unlikely(x) __builtin_expect(!!(x), 0) 20 21 /** 22 * s2n_ensure provides low-level safety check functionality 23 * 24 * This should only consumed directly by s2n_safety. 25 * 26 * Note: This module can be replaced by static analyzer implementation 27 * to insert additional safety checks. 28 */ 29 30 /** 31 * Ensures `cond` is true, otherwise `action` will be performed 32 */ 33 #define __S2N_ENSURE( cond, action ) do {if ( !(cond) ) { action; }} while (0) 34 35 #define __S2N_ENSURE_LIKELY( cond, action ) do {if ( s2n_unlikely( !(cond) ) ) { action; }} while (0) 36 37 #ifdef NDEBUG 38 #define __S2N_ENSURE_DEBUG( cond, action ) do {} while (0) 39 #else 40 #define __S2N_ENSURE_DEBUG( cond, action ) __S2N_ENSURE_LIKELY((cond), action) 41 #endif 42 43 #define __S2N_ENSURE_PRECONDITION( result ) (s2n_likely(s2n_result_is_ok(result)) ? S2N_RESULT_OK : S2N_RESULT_ERROR) 44 45 #ifdef NDEBUG 46 #define __S2N_ENSURE_POSTCONDITION( result ) (S2N_RESULT_OK) 47 #else 48 #define __S2N_ENSURE_POSTCONDITION( result ) (s2n_likely(s2n_result_is_ok(result)) ? S2N_RESULT_OK : S2N_RESULT_ERROR) 49 #endif 50 51 #define __S2N_ENSURE_SAFE_MEMCPY( d , s , n , guard ) \ 52 do { \ 53 __typeof( n ) __tmp_n = ( n ); \ 54 if ( s2n_likely( __tmp_n ) ) { \ 55 void *r = s2n_ensure_memcpy_trace( (d), (s) , (__tmp_n), _S2N_DEBUG_LINE); \ 56 guard(r); \ 57 } \ 58 } while(0) 59 60 #define __S2N_ENSURE_SAFE_MEMSET( d , c , n , guard ) \ 61 do { \ 62 __typeof( n ) __tmp_n = ( n ); \ 63 if ( s2n_likely( __tmp_n ) ) { \ 64 __typeof( d ) __tmp_d = ( d ); \ 65 guard( __tmp_d ); \ 66 memset( __tmp_d, (c), __tmp_n); \ 67 } \ 68 } while(0) 69 70 /** 71 * `restrict` is a part of the c99 standard and will work with any C compiler. If you're trying to 72 * compile with a C++ compiler `restrict` is invalid. However some C++ compilers support the behavior 73 * of `restrict` using the `__restrict__` keyword. Therefore if the compiler supports `__restrict__` 74 * use it. 75 * 76 * This is helpful for the benchmarks in tests/benchmark which use Google's Benchmark library and 77 * are all written in C++. 78 * 79 * https://gcc.gnu.org/onlinedocs/gcc/Restricted-Pointers.html 80 * 81 */ 82 #if defined(S2N___RESTRICT__SUPPORTED) 83 extern void* s2n_ensure_memcpy_trace(void *__restrict__ to, const void *__restrict__ from, size_t size, const char *debug_str); 84 #else 85 extern void* s2n_ensure_memcpy_trace(void *restrict to, const void *restrict from, size_t size, const char *debug_str); 86 #endif 87 88 /** 89 * These macros should not be used in validate functions. 90 * All validate functions are also used in assumptions for CBMC proofs, 91 * which should not contain __CPROVER_*_ok primitives. The use of these primitives 92 * in assumptions may lead to spurious results. 93 * When the code is being verified using CBMC, these properties are formally verified; 94 * When the code is built in debug mode, they are checked as much as possible using assertions. 95 * When the code is built in production mode, non-fatal properties are not checked. 96 * Violations of these properties are undefined behaviour. 97 */ 98 #ifdef CBMC 99 # define S2N_MEM_IS_READABLE_CHECK(base, len) (((len) == 0) || __CPROVER_r_ok((base), (len))) 100 # define S2N_MEM_IS_WRITABLE_CHECK(base, len) (((len) == 0) || __CPROVER_w_ok((base), (len))) 101 #else 102 /* the C runtime does not give a way to check these properties, 103 * but we can at least check for nullness. */ 104 # define S2N_MEM_IS_READABLE_CHECK(base, len) (((len) == 0) || (base) != NULL) 105 # define S2N_MEM_IS_WRITABLE_CHECK(base, len) (((len) == 0) || (base) != NULL) 106 #endif /* CBMC */ 107 108 /** 109 * These macros can safely be used in validate functions. 110 */ 111 #define S2N_MEM_IS_READABLE(base, len) (((len) == 0) || (base) != NULL) 112 #define S2N_MEM_IS_WRITABLE(base, len) (((len) == 0) || (base) != NULL) 113 #define S2N_OBJECT_PTR_IS_READABLE(ptr) ((ptr) != NULL) 114 #define S2N_OBJECT_PTR_IS_WRITABLE(ptr) ((ptr) != NULL) 115 116 #define S2N_IMPLIES(a, b) (!(a) || (b)) 117 /** 118 * If and only if (iff) is a biconditional logical connective between statements a and b. 119 * Equivalent to (S2N_IMPLIES(a, b) && S2N_IMPLIES(b, a)). 120 */ 121 #define S2N_IFF(a, b) (!!(a) == !!(b)) 122 123 /** 124 * These macros are used to specify code contracts in CBMC proofs. 125 * Define function contracts. 126 * When the code is being verified using CBMC, these contracts are formally verified; 127 * When the code is built in production mode, contracts are not checked. 128 * Violations of the function contracts are undefined behaviour. 129 */ 130 #ifdef CBMC 131 # define CONTRACT_ASSIGNS(...) __CPROVER_assigns(__VA_ARGS__) 132 # define CONTRACT_ASSIGNS_ERR(...) CONTRACT_ASSIGNS(__VA_ARGS__, s2n_debug_str, s2n_errno) 133 # define CONTRACT_REQUIRES(...) __CPROVER_requires(__VA_ARGS__) 134 # define CONTRACT_ENSURES(...) __CPROVER_ensures(__VA_ARGS__) 135 # define CONTRACT_INVARIANT(...) __CPROVER_loop_invariant(__VA_ARGS__) 136 # define CONTRACT_RETURN_VALUE (__CPROVER_return_value) 137 #else 138 # define CONTRACT_ASSIGNS(...) 139 # define CONTRACT_ASSIGNS_ERR(...) 140 # define CONTRACT_REQUIRES(...) 141 # define CONTRACT_ENSURES(...) 142 # define CONTRACT_INVARIANT(...) 143 # define CONTRACT_RETURN_VALUE 144 #endif 145