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
23AWS_EXTERN_C_BEGIN
24
25AWS_COMMON_API
26AWS_DECLSPEC_NORETURN
27void aws_fatal_assert(const char *cond_str, const char *file, int line) AWS_ATTRIBUTE_NORETURN;
28
29AWS_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