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