1 | #ifndef AWS_COMMON_ASSERT_H |
2 | #define AWS_COMMON_ASSERT_H |
3 | |
4 | /* |
5 | * Copyright 2010-2018 Amazon.com, Inc. or its affiliates. All Rights Reserved. |
6 | * |
7 | * Licensed under the Apache License, Version 2.0 (the "License"). |
8 | * You may not use this file except in compliance with the License. |
9 | * A copy of the License is located at |
10 | * |
11 | * http://aws.amazon.com/apache2.0 |
12 | * |
13 | * or in the "license" file accompanying this file. This file is distributed |
14 | * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either |
15 | * express or implied. See the License for the specific language governing |
16 | * permissions and limitations under the License. |
17 | */ |
18 | |
19 | #include <aws/common/exports.h> |
20 | #include <aws/common/macros.h> |
21 | #include <stdio.h> |
22 | |
23 | AWS_EXTERN_C_BEGIN |
24 | |
25 | AWS_COMMON_API |
26 | AWS_DECLSPEC_NORETURN |
27 | void aws_fatal_assert(const char *cond_str, const char *file, int line) AWS_ATTRIBUTE_NORETURN; |
28 | |
29 | AWS_EXTERN_C_END |
30 | |
31 | #if defined(CBMC) |
32 | # define AWS_ASSUME(cond) __CPROVER_assume(cond) |
33 | #elif defined(_MSC_VER) |
34 | # define AWS_ASSUME(cond) __assume(cond) |
35 | # define AWS_UNREACHABLE() __assume(0) |
36 | #elif defined(__clang__) |
37 | # define AWS_ASSUME(cond) \ |
38 | do { \ |
39 | bool _result = (cond); \ |
40 | __builtin_assume(_result); \ |
41 | } while (false) |
42 | # define AWS_UNREACHABLE() __builtin_unreachable() |
43 | #elif defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 5)) |
44 | # define AWS_ASSUME(cond) ((cond) ? (void)0 : __builtin_unreachable()) |
45 | # define AWS_UNREACHABLE() __builtin_unreachable() |
46 | #else |
47 | # define AWS_ASSUME(cond) |
48 | # define AWS_UNREACHABLE() |
49 | #endif |
50 | |
51 | #if defined(CBMC) |
52 | # include <assert.h> |
53 | # define AWS_ASSERT(cond) assert(cond) |
54 | #elif defined(DEBUG_BUILD) || __clang_analyzer__ |
55 | # define AWS_ASSERT(cond) AWS_FATAL_ASSERT(cond) |
56 | #else |
57 | # define AWS_ASSERT(cond) |
58 | #endif /* defined(CBMC) */ |
59 | |
60 | #if defined(CBMC) |
61 | # define AWS_FATAL_ASSERT(cond) AWS_ASSERT(cond) |
62 | #elif __clang_analyzer__ |
63 | # define AWS_FATAL_ASSERT(cond) \ |
64 | if (!(cond)) { \ |
65 | abort(); \ |
66 | } |
67 | #else |
68 | # if defined(_MSC_VER) |
69 | # define AWS_FATAL_ASSERT(cond) \ |
70 | __pragma(warning(push)) __pragma(warning(disable : 4127)) /* conditional expression is constant */ \ |
71 | if (!(cond)) { \ |
72 | aws_fatal_assert(#cond, __FILE__, __LINE__); \ |
73 | } \ |
74 | __pragma(warning(pop)) |
75 | # else |
76 | # define AWS_FATAL_ASSERT(cond) \ |
77 | if (!(cond)) { \ |
78 | aws_fatal_assert(#cond, __FILE__, __LINE__); \ |
79 | } |
80 | # endif /* defined(_MSC_VER) */ |
81 | #endif /* defined(CBMC) */ |
82 | |
83 | /** |
84 | * Define function contracts. |
85 | * When the code is being verified using CBMC these contracts are formally verified; |
86 | * When the code is built in debug mode, they are checked as much as possible using assertions |
87 | * When the code is built in production mode, non-fatal contracts are not checked. |
88 | * Violations of the function contracts are undefined behaviour. |
89 | */ |
90 | #ifdef CBMC |
91 | # define AWS_PRECONDITION2(cond, explanation) __CPROVER_precondition((cond), (explanation)) |
92 | # define AWS_PRECONDITION1(cond) __CPROVER_precondition((cond), # cond " check failed") |
93 | # define AWS_FATAL_PRECONDITION2(cond, explanation) __CPROVER_precondition((cond), (explanation)) |
94 | # define AWS_FATAL_PRECONDITION1(cond) __CPROVER_precondition((cond), # cond " check failed") |
95 | # define AWS_POSTCONDITION2(cond, explanation) __CPROVER_assert((cond), (explanation)) |
96 | # define AWS_POSTCONDITION1(cond) __CPROVER_assert((cond), # cond " check failed") |
97 | # define AWS_FATAL_POSTCONDITION2(cond, explanation) __CPROVER_assert((cond), (explanation)) |
98 | # define AWS_FATAL_POSTCONDITION1(cond) __CPROVER_assert((cond), # cond " check failed") |
99 | # define AWS_MEM_IS_READABLE(base, len) __CPROVER_r_ok((base), (len)) |
100 | # define AWS_MEM_IS_WRITABLE(base, len) __CPROVER_w_ok((base), (len)) |
101 | #else |
102 | # define AWS_PRECONDITION2(cond, expl) AWS_ASSERT(cond) |
103 | # define AWS_PRECONDITION1(cond) AWS_ASSERT(cond) |
104 | # define AWS_FATAL_PRECONDITION2(cond, expl) AWS_FATAL_ASSERT(cond) |
105 | # define AWS_FATAL_PRECONDITION1(cond) AWS_FATAL_ASSERT(cond) |
106 | # define AWS_POSTCONDITION2(cond, expl) AWS_ASSERT(cond) |
107 | # define AWS_POSTCONDITION1(cond) AWS_ASSERT(cond) |
108 | # define AWS_FATAL_POSTCONDITION2(cond, expl) AWS_FATAL_ASSERT(cond) |
109 | # define AWS_FATAL_POSTCONDITION1(cond) AWS_FATAL_ASSERT(cond) |
110 | |
111 | /* the C runtime does not give a way to check these properties, |
112 | * but we can at least check that the pointer is valid */ |
113 | # define AWS_MEM_IS_READABLE(base, len) (((len) == 0) || (base)) |
114 | # define AWS_MEM_IS_WRITABLE(base, len) (((len) == 0) || (base)) |
115 | #endif /* CBMC */ |
116 | |
117 | #define AWS_RETURN_ERROR_IF_IMPL(type, cond, err, explanation) \ |
118 | do { \ |
119 | if (!(cond)) { \ |
120 | return aws_raise_error(err); \ |
121 | } \ |
122 | } while (0) |
123 | |
124 | #define AWS_RETURN_ERROR_IF3(cond, err, explanation) AWS_RETURN_ERROR_IF_IMPL("InternalCheck", cond, err, explanation) |
125 | #define AWS_RETURN_ERROR_IF2(cond, err) AWS_RETURN_ERROR_IF3(cond, err, #cond " check failed") |
126 | #define AWS_RETURN_ERROR_IF(...) CALL_OVERLOAD(AWS_RETURN_ERROR_IF, __VA_ARGS__) |
127 | |
128 | #define AWS_ERROR_PRECONDITION3(cond, err, explanation) AWS_RETURN_ERROR_IF_IMPL("Precondition", cond, err, explanation) |
129 | #define AWS_ERROR_PRECONDITION2(cond, err) AWS_ERROR_PRECONDITION3(cond, err, #cond " check failed") |
130 | #define AWS_ERROR_PRECONDITION1(cond) AWS_ERROR_PRECONDITION2(cond, AWS_ERROR_INVALID_ARGUMENT) |
131 | |
132 | #define AWS_ERROR_POSTCONDITION3(cond, err, explanation) \ |
133 | AWS_RETURN_ERROR_IF_IMPL("Postcondition", cond, err, explanation) |
134 | #define AWS_ERROR_POSTCONDITION2(cond, err) AWS_ERROR_POSTCONDITION3(cond, err, #cond " check failed") |
135 | #define AWS_ERROR_POSTCONDITION1(cond) AWS_ERROR_POSTCONDITION2(cond, AWS_ERROR_INVALID_ARGUMENT) |
136 | |
137 | // The UNUSED is used to silence the complains of GCC for zero arguments in variadic macro |
138 | #define AWS_PRECONDITION(...) CALL_OVERLOAD(AWS_PRECONDITION, __VA_ARGS__) |
139 | #define AWS_FATAL_PRECONDITION(...) CALL_OVERLOAD(AWS_FATAL_PRECONDITION, __VA_ARGS__) |
140 | #define AWS_POSTCONDITION(...) CALL_OVERLOAD(AWS_POSTCONDITION, __VA_ARGS__) |
141 | #define AWS_FATAL_POSTCONDITION(...) CALL_OVERLOAD(AWS_FATAL_POSTCONDITION, __VA_ARGS__) |
142 | #define AWS_ERROR_PRECONDITION(...) CALL_OVERLOAD(AWS_ERROR_PRECONDITION, __VA_ARGS__) |
143 | #define AWS_ERROR_POSTCONDITION(...) CALL_OVERLOAD(AWS_ERROR_PRECONDITION, __VA_ARGS__) |
144 | |
145 | #define AWS_RETURN_WITH_POSTCONDITION(_rval, ...) \ |
146 | do { \ |
147 | AWS_POSTCONDITION(__VA_ARGS__); \ |
148 | return _rval; \ |
149 | } while (0) |
150 | |
151 | #define AWS_SUCCEED_WITH_POSTCONDITION(...) AWS_RETURN_WITH_POSTCONDITION(AWS_OP_SUCCESS, __VA_ARGS__) |
152 | |
153 | #define AWS_OBJECT_PTR_IS_READABLE(ptr) AWS_MEM_IS_READABLE((ptr), sizeof(*(ptr))) |
154 | #define AWS_OBJECT_PTR_IS_WRITABLE(ptr) AWS_MEM_IS_WRITABLE((ptr), sizeof(*(ptr))) |
155 | |
156 | #endif /* AWS_COMMON_ASSERT_H */ |
157 | |