Line data Source code
1 : #ifndef AWS_COMMON_ASSERT_H
2 : #define AWS_COMMON_ASSERT_H
3 :
4 : /**
5 : * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
6 : * SPDX-License-Identifier: Apache-2.0.
7 : */
8 :
9 : #include <aws/common/exports.h>
10 : #include <aws/common/macros.h>
11 : #include <stdio.h>
12 :
13 : AWS_EXTERN_C_BEGIN
14 :
15 : AWS_COMMON_API
16 : AWS_DECLSPEC_NORETURN
17 : void aws_fatal_assert(const char *cond_str, const char *file, int line) AWS_ATTRIBUTE_NORETURN;
18 :
19 : AWS_EXTERN_C_END
20 :
21 : #if defined(CBMC)
22 : # define AWS_ASSUME(cond) __CPROVER_assume(cond)
23 : #elif defined(_MSC_VER)
24 : # define AWS_ASSUME(cond) __assume(cond)
25 : # define AWS_UNREACHABLE() __assume(0)
26 : #elif defined(__clang__)
27 : # define AWS_ASSUME(cond) \
28 : do { \
29 : bool _result = (cond); \
30 : __builtin_assume(_result); \
31 : } while (false)
32 : # define AWS_UNREACHABLE() __builtin_unreachable()
33 : #elif defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 5))
34 : # define AWS_ASSUME(cond) ((cond) ? (void)0 : __builtin_unreachable())
35 : # define AWS_UNREACHABLE() __builtin_unreachable()
36 : #else
37 : # define AWS_ASSUME(cond)
38 : # define AWS_UNREACHABLE()
39 : #endif
40 :
41 : #if defined(CBMC)
42 : # include <assert.h>
43 : # define AWS_ASSERT(cond) assert(cond)
44 : #elif defined(DEBUG_BUILD) || __clang_analyzer__
45 22548554 : # define AWS_ASSERT(cond) AWS_FATAL_ASSERT(cond)
46 : #else
47 : # define AWS_ASSERT(cond)
48 : #endif /* defined(CBMC) */
49 :
50 : #if defined(CBMC)
51 : # define AWS_FATAL_ASSERT(cond) AWS_ASSERT(cond)
52 : #elif __clang_analyzer__
53 : # define AWS_FATAL_ASSERT(cond) \
54 : if (!(cond)) { \
55 : abort(); \
56 : }
57 : #else
58 : # if defined(_MSC_VER)
59 : # define AWS_FATAL_ASSERT(cond) \
60 : __pragma(warning(push)) __pragma(warning(disable : 4127)) /* conditional expression is constant */ \
61 : if (!(cond)) { \
62 : aws_fatal_assert(#cond, __FILE__, __LINE__); \
63 : } \
64 : __pragma(warning(pop))
65 : # else
66 : # define AWS_FATAL_ASSERT(cond) \
67 32794784 : if (!(cond)) { \
68 0 : aws_fatal_assert(#cond, __FILE__, __LINE__); \
69 0 : }
70 : # endif /* defined(_MSC_VER) */
71 : #endif /* defined(CBMC) */
72 :
73 : /**
74 : * Define function contracts.
75 : * When the code is being verified using CBMC these contracts are formally verified;
76 : * When the code is built in debug mode, they are checked as much as possible using assertions
77 : * When the code is built in production mode, non-fatal contracts are not checked.
78 : * Violations of the function contracts are undefined behaviour.
79 : */
80 : #ifdef CBMC
81 : # define AWS_PRECONDITION2(cond, explanation) __CPROVER_precondition((cond), (explanation))
82 : # define AWS_PRECONDITION1(cond) __CPROVER_precondition((cond), # cond " check failed")
83 : # define AWS_FATAL_PRECONDITION2(cond, explanation) __CPROVER_precondition((cond), (explanation))
84 : # define AWS_FATAL_PRECONDITION1(cond) __CPROVER_precondition((cond), # cond " check failed")
85 : # define AWS_POSTCONDITION2(cond, explanation) __CPROVER_assert((cond), (explanation))
86 : # define AWS_POSTCONDITION1(cond) __CPROVER_assert((cond), # cond " check failed")
87 : # define AWS_FATAL_POSTCONDITION2(cond, explanation) __CPROVER_assert((cond), (explanation))
88 : # define AWS_FATAL_POSTCONDITION1(cond) __CPROVER_assert((cond), # cond " check failed")
89 : # define AWS_MEM_IS_READABLE_CHECK(base, len) (((len) == 0) || (__CPROVER_r_ok((base), (len))))
90 : # define AWS_MEM_IS_WRITABLE_CHECK(base, len) (((len) == 0) || (__CPROVER_r_ok((base), (len))))
91 : #else
92 2448913 : # define AWS_PRECONDITION2(cond, expl) AWS_ASSERT(cond)
93 12464531 : # define AWS_PRECONDITION1(cond) AWS_ASSERT(cond)
94 : # define AWS_FATAL_PRECONDITION2(cond, expl) AWS_FATAL_ASSERT(cond)
95 5625609 : # define AWS_FATAL_PRECONDITION1(cond) AWS_FATAL_ASSERT(cond)
96 0 : # define AWS_POSTCONDITION2(cond, expl) AWS_ASSERT(cond)
97 7466654 : # define AWS_POSTCONDITION1(cond) AWS_ASSERT(cond)
98 : # define AWS_FATAL_POSTCONDITION2(cond, expl) AWS_FATAL_ASSERT(cond)
99 1520 : # define AWS_FATAL_POSTCONDITION1(cond) AWS_FATAL_ASSERT(cond)
100 : /**
101 : * These macros should not be used in is_valid functions.
102 : * All validate functions are also used in assumptions for CBMC proofs,
103 : * which should not contain __CPROVER_*_ok primitives. The use of these primitives
104 : * in assumptions may lead to spurious results.
105 : * The C runtime does not give a way to check these properties,
106 : * but we can at least check that the pointer is valid. */
107 : # define AWS_MEM_IS_READABLE_CHECK(base, len) (((len) == 0) || (base))
108 : # define AWS_MEM_IS_WRITABLE_CHECK(base, len) (((len) == 0) || (base))
109 : #endif /* CBMC */
110 :
111 : /**
112 : * These macros can safely be used in validate functions.
113 : */
114 22392493 : #define AWS_MEM_IS_READABLE(base, len) (((len) == 0) || (base))
115 15392719 : #define AWS_MEM_IS_WRITABLE(base, len) (((len) == 0) || (base))
116 :
117 : /* Logical consequence. */
118 22584672 : #define AWS_IMPLIES(a, b) (!(a) || (b))
119 :
120 : /**
121 : * If and only if (iff) is a biconditional logical connective between statements a and b.
122 : * We need double negations (!!) here to work correctly for non-Boolean a and b values.
123 : * Equivalent to (AWS_IMPLIES(a, b) && AWS_IMPLIES(b, a)).
124 : */
125 : #define AWS_IFF(a, b) (!!(a) == !!(b))
126 :
127 : #define AWS_RETURN_ERROR_IF_IMPL(type, cond, err, explanation) \
128 837472 : do { \
129 837472 : if (!(cond)) { \
130 0 : return aws_raise_error(err); \
131 0 : } \
132 837472 : } while (0)
133 :
134 : #define AWS_RETURN_ERROR_IF3(cond, err, explanation) AWS_RETURN_ERROR_IF_IMPL("InternalCheck", cond, err, explanation)
135 : #define AWS_RETURN_ERROR_IF2(cond, err) AWS_RETURN_ERROR_IF3(cond, err, #cond " check failed")
136 : #define AWS_RETURN_ERROR_IF(...) CALL_OVERLOAD(AWS_RETURN_ERROR_IF, __VA_ARGS__)
137 :
138 837472 : #define AWS_ERROR_PRECONDITION3(cond, err, explanation) AWS_RETURN_ERROR_IF_IMPL("Precondition", cond, err, explanation)
139 837472 : #define AWS_ERROR_PRECONDITION2(cond, err) AWS_ERROR_PRECONDITION3(cond, err, #cond " check failed")
140 830854 : #define AWS_ERROR_PRECONDITION1(cond) AWS_ERROR_PRECONDITION2(cond, AWS_ERROR_INVALID_ARGUMENT)
141 :
142 : #define AWS_ERROR_POSTCONDITION3(cond, err, explanation) \
143 : AWS_RETURN_ERROR_IF_IMPL("Postcondition", cond, err, explanation)
144 : #define AWS_ERROR_POSTCONDITION2(cond, err) AWS_ERROR_POSTCONDITION3(cond, err, #cond " check failed")
145 : #define AWS_ERROR_POSTCONDITION1(cond) AWS_ERROR_POSTCONDITION2(cond, AWS_ERROR_INVALID_ARGUMENT)
146 :
147 : // The UNUSED is used to silence the complains of GCC for zero arguments in variadic macro
148 14913444 : #define AWS_PRECONDITION(...) CALL_OVERLOAD(AWS_PRECONDITION, __VA_ARGS__)
149 5625609 : #define AWS_FATAL_PRECONDITION(...) CALL_OVERLOAD(AWS_FATAL_PRECONDITION, __VA_ARGS__)
150 7466654 : #define AWS_POSTCONDITION(...) CALL_OVERLOAD(AWS_POSTCONDITION, __VA_ARGS__)
151 1520 : #define AWS_FATAL_POSTCONDITION(...) CALL_OVERLOAD(AWS_FATAL_POSTCONDITION, __VA_ARGS__)
152 837472 : #define AWS_ERROR_PRECONDITION(...) CALL_OVERLOAD(AWS_ERROR_PRECONDITION, __VA_ARGS__)
153 : #define AWS_ERROR_POSTCONDITION(...) CALL_OVERLOAD(AWS_ERROR_PRECONDITION, __VA_ARGS__)
154 :
155 : #define AWS_RETURN_WITH_POSTCONDITION(_rval, ...) \
156 993133 : do { \
157 844694 : AWS_POSTCONDITION(__VA_ARGS__); \
158 844694 : return _rval; \
159 844694 : } while (0)
160 :
161 148439 : #define AWS_SUCCEED_WITH_POSTCONDITION(...) AWS_RETURN_WITH_POSTCONDITION(AWS_OP_SUCCESS, __VA_ARGS__)
162 :
163 0 : #define AWS_OBJECT_PTR_IS_READABLE(ptr) AWS_MEM_IS_READABLE((ptr), sizeof(*(ptr)))
164 450000 : #define AWS_OBJECT_PTR_IS_WRITABLE(ptr) AWS_MEM_IS_WRITABLE((ptr), sizeof(*(ptr)))
165 :
166 : #endif /* AWS_COMMON_ASSERT_H */
|