#ifndef AWS_COMMON_ASSERT_H #define AWS_COMMON_ASSERT_H /* * Copyright 2010-2018 Amazon.com, Inc. or its affiliates. All Rights Reserved. * * Licensed under the Apache License, Version 2.0 (the "License"). * You may not use this file except in compliance with the License. * A copy of the License is located at * * http://aws.amazon.com/apache2.0 * * or in the "license" file accompanying this file. This file is distributed * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either * express or implied. See the License for the specific language governing * permissions and limitations under the License. */ #include #include #include 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_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 # define AWS_ASSERT(cond) assert(cond) #elif defined(DEBUG_BUILD) || __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 __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) \ if (!(cond)) { \ aws_fatal_assert(#cond, __FILE__, __LINE__); \ } # 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 # 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(base, len) __CPROVER_r_ok((base), (len)) # define AWS_MEM_IS_WRITABLE(base, len) __CPROVER_w_ok((base), (len)) #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) /* 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(base, len) (((len) == 0) || (base)) # define AWS_MEM_IS_WRITABLE(base, len) (((len) == 0) || (base)) #endif /* CBMC */ #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))) #endif /* AWS_COMMON_ASSERT_H */