Branch data     Line data    Source code

       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                 :  263374017 : #define s2n_likely(x)   __builtin_expect(!!(x), 1)
      19                 : 9968413477 : #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) \
      34                 : 8321091615 :     do {                           \
      35                 : 8320582834 :         if (!(cond)) {             \
      36                 :   12809281 :             action;                \
      37                 :    9274901 :         }                          \
      38                 : 8320582834 :     } while (0)
      39                 :            : 
      40                 :            : #define __S2N_ENSURE_LIKELY(cond, action) \
      41                 : 8984464210 :     do {                                  \
      42                 : 8984464210 :         if (s2n_unlikely(!(cond))) {      \
      43                 :         36 :             action;                       \
      44                 :          6 :         }                                 \
      45                 : 8984464210 :     } while (0)
      46                 :            : 
      47                 :            : #ifdef NDEBUG
      48                 :            :     #define __S2N_ENSURE_DEBUG(cond, action) \
      49                 :            :         do {                                 \
      50                 :            :         } while (0)
      51                 :            : #else
      52                 : 8984464210 :     #define __S2N_ENSURE_DEBUG(cond, action) __S2N_ENSURE_LIKELY((cond), action)
      53                 :            : #endif
      54                 :            : 
      55                 :            : #define __S2N_ENSURE_PRECONDITION(result) (s2n_likely(s2n_result_is_ok(result)) ? S2N_RESULT_OK : S2N_RESULT_ERROR)
      56                 :            : 
      57                 :            : #ifdef NDEBUG
      58                 :            :     #define __S2N_ENSURE_POSTCONDITION(result) (S2N_RESULT_OK)
      59                 :            : #else
      60                 :            :     #define __S2N_ENSURE_POSTCONDITION(result) (s2n_likely(s2n_result_is_ok(result)) ? S2N_RESULT_OK : S2N_RESULT_ERROR)
      61                 :            : #endif
      62                 :            : 
      63                 :            : #define __S2N_ENSURE_SAFE_MEMMOVE(d, s, n, guard)                    \
      64                 :  132478704 :     do {                                                             \
      65                 :  132478704 :         __typeof(n) __tmp_n = (n);                                   \
      66                 :  132478704 :         if (s2n_likely(__tmp_n)) {                                   \
      67                 :  118439941 :             void *r = s2n_ensure_memmove_trace((d), (s), (__tmp_n)); \
      68                 :  118439941 :             guard(r);                                                \
      69                 :  118439941 :         }                                                            \
      70                 :  132478704 :     } while (0)
      71                 :            : 
      72                 :            : #define __S2N_ENSURE_SAFE_MEMSET(d, c, n, guard) \
      73                 :  130895313 :     do {                                         \
      74                 :  203844158 :         __typeof(n) __tmp_n = (n);               \
      75                 :  130895313 :         if (s2n_likely(__tmp_n)) {               \
      76                 :   30438363 :             __typeof(d) __tmp_d = (d);           \
      77                 :   30438363 :             guard(__tmp_d);                      \
      78                 :   30438363 :             memset(__tmp_d, (c), __tmp_n);       \
      79                 :   30438363 :         }                                        \
      80                 :  130895313 :     } while (0)
      81                 :            : 
      82                 :            : #if defined(S2N_DIAGNOSTICS_PUSH_SUPPORTED) && defined(S2N_DIAGNOSTICS_POP_SUPPORTED)
      83                 :            :     #define __S2N_ENSURE_CHECKED_RETURN(v)                                     \
      84                 :     664896 :         do {                                                                   \
      85                 :     664896 :             _Pragma("GCC diagnostic push")                                     \
      86                 :     664896 :                     _Pragma("GCC diagnostic error \"-Wconversion\"") return v; \
      87                 :     664896 :             _Pragma("GCC diagnostic pop")                                      \
      88                 :     664896 :         } while (0)
      89                 :            : #else
      90                 :            :     #define __S2N_ENSURE_CHECKED_RETURN(v) return v
      91                 :            : #endif
      92                 :            : 
      93                 :            : void *s2n_ensure_memmove_trace(void *to, const void *from, size_t size);
      94                 :            : 
      95                 :            : /**
      96                 :            :  * These macros should not be used in validate functions.
      97                 :            :  * All validate functions are also used in assumptions for CBMC proofs,
      98                 :            :  * which should not contain __CPROVER_*_ok primitives. The use of these primitives
      99                 :            :  * in assumptions may lead to spurious results.
     100                 :            :  * When the code is being verified using CBMC, these properties are formally verified;
     101                 :            :  * When the code is built in debug mode, they are checked as much as possible using assertions.
     102                 :            :  * When the code is built in production mode, non-fatal properties are not checked.
     103                 :            :  * Violations of these properties are undefined behaviour.
     104                 :            :  */
     105                 :            : #ifdef CBMC
     106                 :            :     #define S2N_MEM_IS_READABLE_CHECK(base, len) (((len) == 0) || __CPROVER_r_ok((base), (len)))
     107                 :            :     #define S2N_MEM_IS_WRITABLE_CHECK(base, len) (((len) == 0) || __CPROVER_w_ok((base), (len)))
     108                 :            : #else
     109                 :            :     /* the C runtime does not give a way to check these properties,
     110                 :            :  * but we can at least check for nullness. */
     111                 :            :     #define S2N_MEM_IS_READABLE_CHECK(base, len) (((len) == 0) || (base) != NULL)
     112                 :            :     #define S2N_MEM_IS_WRITABLE_CHECK(base, len) (((len) == 0) || (base) != NULL)
     113                 :            : #endif /* CBMC */
     114                 :            : 
     115                 :            : /**
     116                 :            :  * These macros can safely be used in validate functions.
     117                 :            :  */
     118                 :     786196 : #define S2N_MEM_IS_READABLE(base, len)  (((len) == 0) || (base) != NULL)
     119                 :            : #define S2N_MEM_IS_WRITABLE(base, len)  (((len) == 0) || (base) != NULL)
     120                 :            : #define S2N_OBJECT_PTR_IS_READABLE(ptr) ((ptr) != NULL)
     121                 :            : #define S2N_OBJECT_PTR_IS_WRITABLE(ptr) ((ptr) != NULL)
     122                 :            : 
     123                 :            : /**
     124                 :            :  * If `a` is true, then `b` must be true.
     125                 :            :  */
     126                 :            : #define S2N_IMPLIES(a, b) (!(a) || (b))
     127                 :            : /**
     128                 :            :  * If and only if (iff) is a biconditional logical connective between statements a and b.
     129                 :            :  * Equivalent to (S2N_IMPLIES(a, b) && S2N_IMPLIES(b, a)).
     130                 :            :  */
     131                 :            : #define S2N_IFF(a, b) (!!(a) == !!(b))
     132                 :            : 
     133                 :            : /**
     134                 :            :  * These macros are used to specify code contracts in CBMC proofs.
     135                 :            :  * Define function contracts.
     136                 :            :  * When the code is being verified using CBMC, these contracts are formally verified;
     137                 :            :  * When the code is built in production mode, contracts are not checked.
     138                 :            :  * Violations of the function contracts are undefined behaviour.
     139                 :            :  */
     140                 :            : #ifdef CBMC
     141                 :            :     #define CONTRACT_ASSERT(...)      __CPROVER_assert(__VA_ARGS__)
     142                 :            :     #define CONTRACT_ASSIGNS(...)     __CPROVER_assigns(__VA_ARGS__)
     143                 :            :     #define CONTRACT_ASSIGNS_ERR(...) CONTRACT_ASSIGNS(__VA_ARGS__, _s2n_debug_info, s2n_errno)
     144                 :            :     #define CONTRACT_ASSUME(...)      __CPROVER_assume(__VA_ARGS__)
     145                 :            :     #define CONTRACT_REQUIRES(...)    __CPROVER_requires(__VA_ARGS__)
     146                 :            :     #define CONTRACT_ENSURES(...)     __CPROVER_ensures(__VA_ARGS__)
     147                 :            :     #define CONTRACT_INVARIANT(...)   __CPROVER_loop_invariant(__VA_ARGS__)
     148                 :            :     #define CONTRACT_RETURN_VALUE     (__CPROVER_return_value)
     149                 :            : #else
     150                 :            :     #define CONTRACT_ASSERT(...)
     151                 :            :     #define CONTRACT_ASSIGNS(...)
     152                 :            :     #define CONTRACT_ASSIGNS_ERR(...)
     153                 :            :     #define CONTRACT_ASSUME(...)
     154                 :            :     #define CONTRACT_REQUIRES(...)
     155                 :            :     #define CONTRACT_ENSURES(...)
     156                 :            :     #define CONTRACT_INVARIANT(...)
     157                 :            :     #define CONTRACT_RETURN_VALUE
     158                 :            : #endif