diff --git a/regression/invariants/driver.cpp b/regression/invariants/driver.cpp index 3531955372e..aadfac36fd5 100644 --- a/regression/invariants/driver.cpp +++ b/regression/invariants/driver.cpp @@ -56,6 +56,31 @@ class structured_error_testt: public invariant_failedt } }; +struct DiagnosticA +{ +}; +struct DiagnosticB +{ +}; + +template <> +struct diagnostics_helpert +{ + static std::string diagnostics_as_string(const DiagnosticA &) + { + return "Diagnostic A"; + } +}; + +template <> +struct diagnostics_helpert +{ + static std::string diagnostics_as_string(const DiagnosticB &) + { + return "Diagnostic B"; + } +}; + /// Causes an invariant failure dependent on first argument value. /// One ignored argument is accepted to conform with the test.pl script, /// which would be the input source file for other cbmc driver programs. @@ -92,21 +117,38 @@ int main(int argc, char** argv) else if(arg=="irep") INVARIANT_WITH_IREP(false, "error with irep", pointer_type(void_typet())); else if(arg == "invariant-diagnostics") - INVARIANT( + INVARIANT_WITH_DIAGNOSTICS( false, "invariant with diagnostics failure", "invariant diagnostics information"); else if(arg == "precondition-diagnostics") - PRECONDITION(false, "precondition diagnostics information"); + PRECONDITION_WITH_DIAGNOSTICS( + false, "precondition diagnostics information"); else if(arg == "postcondition-diagnostics") - POSTCONDITION(false, "postcondition diagnostics information"); + POSTCONDITION_WITH_DIAGNOSTICS( + false, "postcondition diagnostics information"); else if(arg == "check-return-diagnostics") - CHECK_RETURN(false, "check return diagnostics information"); + CHECK_RETURN_WITH_DIAGNOSTICS( + false, "check return diagnostics information"); else if(arg == "data-invariant-diagnostics") - DATA_INVARIANT( + DATA_INVARIANT_WITH_DIAGNOSTICS( false, "data invariant with diagnostics failure", "data invariant diagnostics information"); + else if(arg == "invariant-with-lots-of-diagnostics") + INVARIANT_WITH_DIAGNOSTICS( + false, + "an invariant that fails", + "diagnostic 1", + "diagnostic 2", + "diagnostic 3", + "diagnostic 4"); + else if(arg == "invariant-with-custom-diagnostics") + INVARIANT_WITH_DIAGNOSTICS( + false, + "an invariant with some custom diagnostics", + DiagnosticA{}, + DiagnosticB{}); else return 1; } diff --git a/regression/invariants/invariant-failure19/test.desc b/regression/invariants/invariant-failure19/test.desc new file mode 100644 index 00000000000..f3c73ce0854 --- /dev/null +++ b/regression/invariants/invariant-failure19/test.desc @@ -0,0 +1,11 @@ +CORE +dummy_parameter.c +invariant-with-lots-of-diagnostics +^EXIT=(0|127|134|137)$ +^SIGNAL=0$ +--- begin invariant violation report --- +Invariant check failed +diagnostic 1 +diagnostic 2 +diagnostic 3 +diagnostic 4 diff --git a/regression/invariants/invariant-failure20/test.desc b/regression/invariants/invariant-failure20/test.desc new file mode 100644 index 00000000000..13f296c2cf4 --- /dev/null +++ b/regression/invariants/invariant-failure20/test.desc @@ -0,0 +1,9 @@ +CORE +dummy_parameter.c +invariant-with-custom-diagnostics +^EXIT=(0|127|134|137)$ +^SIGNAL=0$ +--- begin invariant violation report --- +Invariant check failed +Diagnostic A +Diagnostic B diff --git a/src/util/dstring.h b/src/util/dstring.h index 7e72f543fd7..a7b7eccba56 100644 --- a/src/util/dstring.h +++ b/src/util/dstring.h @@ -13,7 +13,9 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_DSTRING_H #include +#include +#include "invariant.h" #include "string_container.h" /// \ref dstringt has one field, an unsigned integer \ref no which is an index @@ -198,4 +200,13 @@ struct hash // NOLINT(readability/identifiers) }; } +template <> +struct diagnostics_helpert +{ + static std::string diagnostics_as_string(const dstringt &dstring) + { + return as_string(dstring); + } +}; + #endif // CPROVER_UTIL_DSTRING_H diff --git a/src/util/invariant.h b/src/util/invariant.h index 06ac7a8f36e..0586a0e7aac 100644 --- a/src/util/invariant.h +++ b/src/util/invariant.h @@ -10,6 +10,7 @@ Author: Martin Brain, martin.brain@diffblue.com #define CPROVER_UTIL_INVARIANT_H #include +#include #include #include #include @@ -132,17 +133,21 @@ class invariant_with_diagnostics_failedt : public invariant_failedt } }; -// The macros MACRO (e.g., INVARIANT2) are for internal use in this file -// only. The corresponding macros that take a variable number of arguments (see -// further below) should be used instead, which in turn call those with a fixed -// number of arguments. For example, if INVARIANT(...) is called with two -// arguments, it calls INVARIANT2(). +#ifdef __GNUC__ +#define CBMC_NORETURN __attribute((noreturn)) +#elif defined(_MSV_VER) +#define CBMC_NORETURN __declspec(noreturn) +#elif __cplusplus >= 201703L +#define CBMC_NORETURN [[noreturn]] +#else +#define CBMC_NORETURN +#endif #if defined(CPROVER_INVARIANT_CPROVER_ASSERT) // Used to allow CPROVER to check itself -#define INVARIANT2(CONDITION, REASON) \ +#define INVARIANT(CONDITION, REASON) \ __CPROVER_assert((CONDITION), "Invariant : " REASON) -#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \ +#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \ __CPROVER_assert((CONDITION), "Invariant : " REASON) #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ @@ -153,11 +158,11 @@ class invariant_with_diagnostics_failedt : public invariant_failedt // This is *not* recommended as it can result in unpredictable behaviour // including silently reporting incorrect results. // This is also useful for checking side-effect freedom. -#define INVARIANT2(CONDITION, REASON) \ +#define INVARIANT(CONDITION, REASON) \ do \ { \ } while(false) -#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \ +#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \ do \ { \ } while(false) @@ -167,8 +172,8 @@ class invariant_with_diagnostics_failedt : public invariant_failedt // Not recommended but provided for backwards compatability #include // NOLINTNEXTLINE(*) -#define INVARIANT2(CONDITION, REASON) assert((CONDITION) && ((REASON), true)) -#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \ +#define INVARIANT(CONDITION, REASON) assert((CONDITION) && ((REASON), true)) +#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \ assert((CONDITION) && ((REASON), true)) /* NOLINT */ // NOLINTNEXTLINE(*) #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) assert((CONDITION)) @@ -191,16 +196,14 @@ void report_exception_to_stderr(const invariant_failedt &); /// \param params : (variadic) parameters to forward to ET's constructor /// its backtrace member will be set before it is used. template -#ifdef __GNUC__ -__attribute__((noreturn)) -#endif -typename std::enable_if::value>::type -invariant_violated_structured( - const std::string &file, - const std::string &function, - const int line, - const std::string &condition, - Params &&... params) +CBMC_NORETURN + typename std::enable_if::value>::type + invariant_violated_structured( + const std::string &file, + const std::string &function, + const int line, + const std::string &condition, + Params &&... params) { std::string backtrace=get_backtrace(); ET to_throw( @@ -224,9 +227,7 @@ invariant_violated_structured( /// \param line : The line number of the invariant /// \param reason : brief description of the invariant violation. /// \param condition : the condition this invariant is checking. -#ifdef __GNUC__ -__attribute__((noreturn)) -#endif +CBMC_NORETURN inline void invariant_violated_string( const std::string &file, @@ -239,84 +240,170 @@ invariant_violated_string( file, function, line, condition, reason); } +namespace detail +{ +template +struct always_falset : public std::false_type +{ +}; +} // namespace detail + +/// Helper to give us some diagnostic in a usable form on assertion failure. +/// For now only provides string output +/// Must be specialised for all types that should be useable as diagnostics +template +struct diagnostics_helpert +{ + // silly construct because C++ won't let us write static_assert(false,...) + static_assert( + detail::always_falset::value, + "to avoid unintended strangeness, diagnostics_helpert needs to be " + "specialised for each diagnostic type"); + static std::string diagnostics_as_string(const T &); +}; + +// Standard string specialisations for diagnostics_helper +// (character arrays, character pointers and std::string) + +template +struct diagnostics_helpert +{ + static std::string diagnostics_as_string(const char (&string)[N]) + { + return string; + } +}; +template <> +struct diagnostics_helpert +{ + static std::string diagnostics_as_string(const char *string) + { + return string; + } +}; + +template <> +struct diagnostics_helpert +{ + // This is deliberately taking a copy instead of a reference + // to avoid making an extra copy when passing a temporary string + // as a diagnostic + static std::string diagnostics_as_string(std::string string) + { + return string; + } +}; + +namespace detail +{ +inline std::string assemble_diagnostics() +{ + return ""; +} + +template +std::string diagnostic_as_string(T &&val) +{ + return diagnostics_helpert< + typename std::remove_cv::type>::type>:: + diagnostics_as_string(std::forward(val)); +} + +inline void write_rest_diagnostics(std::ostream &) +{ +} + +template +void write_rest_diagnostics(std::ostream &out, T &&next, Ts &&... rest) +{ + out << "\n" << diagnostic_as_string(std::forward(next)); + write_rest_diagnostics(out, std::forward(rest)...); +} + +template +std::string assemble_diagnostics(Diagnostics &&... args) +{ + std::ostringstream out; + out << "\n<< EXTRA DIAGNOSTICS >>"; + write_rest_diagnostics(out, std::forward(args)...); + out << "\n<< END EXTRA DIAGNOSTICS >>"; + return out.str(); +} +} // namespace detail + +template +CBMC_NORETURN void report_invariant_failure( + const std::string &file, + const std::string &function, + int line, + std::string reason, + std::string condition, + Diagnostics &&... diagnostics) +{ + invariant_violated_structured( + file, + function, + line, + reason, + condition, + detail::assemble_diagnostics(std::forward(diagnostics)...)); +} + +#define EXPAND_MACRO(x) x + // These require a trailing semicolon by the user, such that INVARIANT // behaves syntactically like a function call. // NOLINT as macro definitions confuse the linter it seems. #ifdef _MSC_VER -#define __this_function__ __FUNCTION__ +#define CURRENT_FUNCTION_NAME __FUNCTION__ #else -#define __this_function__ __func__ +#define CURRENT_FUNCTION_NAME __func__ #endif -// We wrap macros that take __VA_ARGS__ as an argument with EXPAND_MACRO(). This -// is to account for the behaviour of msvc, which otherwise would not expand -// __VA_ARGS__ to multiple arguments in the outermost macro invocation. -#define EXPAND_MACRO(x) x - -#define GET_MACRO(X1, X2, X3, X4, X5, X6, MACRO, ...) MACRO - -// This macro dispatches to the macros MACRO (with 1 <= n <= 6) and calls -// them with the arguments in __VA_ARGS__. The invocation of GET_MACRO() selects -// MACRO when __VA_ARGS__ consists of n arguments. -#define REDIRECT(MACRO, ...) \ - do \ - { \ - EXPAND_MACRO( \ - GET_MACRO( \ - __VA_ARGS__, \ - MACRO##6, \ - MACRO##5, \ - MACRO##4, \ - MACRO##3, \ - MACRO##2, \ - MACRO##1, \ - DUMMY_MACRO_ARG)(__VA_ARGS__)); \ - } while(false) - -#define INVARIANT2(CONDITION, REASON) \ +#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ do /* NOLINT */ \ { \ if(!(CONDITION)) \ - invariant_violated_string( \ + invariant_violated_structured( \ __FILE__, \ - __this_function__, \ + CURRENT_FUNCTION_NAME, \ __LINE__, \ #CONDITION, \ - (REASON)); /* NOLINT */ \ + __VA_ARGS__); /* NOLINT */ \ } while(false) -#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \ - do /* NOLINT */ \ +#endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block + +// Short hand macros. The variants *_STRUCTURED below allow to specify a custom +// exception, and are equivalent to INVARIANT_STRUCTURED. +#define INVARIANT(CONDITION, REASON) \ + do \ { \ if(!(CONDITION)) \ - invariant_violated_structured( \ - __FILE__, \ - __this_function__, \ - __LINE__, \ - #CONDITION, \ - (REASON), \ - (DIAGNOSTICS)); /* NOLINT */ \ + { \ + invariant_violated_string( \ + __FILE__, CURRENT_FUNCTION_NAME, __LINE__, REASON, #CONDITION); \ + } \ } while(false) -#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ - do /* NOLINT */ \ +/// Same as invariant, with one or more diagnostics attached +/// Diagnostics can be of any type that has a specialisation for +/// invariant_helpert +#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \ + do \ { \ if(!(CONDITION)) \ - invariant_violated_structured( \ + { \ + report_invariant_failure( \ __FILE__, \ - __this_function__, \ + CURRENT_FUNCTION_NAME, \ __LINE__, \ + REASON, \ #CONDITION, \ - __VA_ARGS__); /* NOLINT */ \ + __VA_ARGS__); \ + } \ } while(false) -#endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block - -// Short hand macros. The variants *_STRUCTURED below allow to specify a custom -// exception, and are equivalent to INVARIANT_STRUCTURED. - -#define INVARIANT(...) EXPAND_MACRO(REDIRECT(INVARIANT, __VA_ARGS__)) - // The condition should only contain (unmodified) inputs to the method. Inputs // include arguments passed to the function, as well as member variables that // the function may read. @@ -325,11 +412,10 @@ invariant_violated_string( // // The PRECONDITION documents / checks assumptions about the inputs // that is the caller's responsibility to make happen before the call. -#define PRECONDITION1(CONDITION) INVARIANT2(CONDITION, "Precondition") -#define PRECONDITION2(CONDITION, DIAGNOSTICS) \ - INVARIANT3(CONDITION, "Precondition", DIAGNOSTICS) -#define PRECONDITION(...) EXPAND_MACRO(REDIRECT(PRECONDITION, __VA_ARGS__)) +#define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition") +#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION, ...) \ + INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Precondition", __VA_ARGS__) #define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) @@ -342,11 +428,10 @@ invariant_violated_string( // output when it returns, given that it was called with valid inputs. // Outputs include the return value of the function, as well as member // variables that the function may write. -#define POSTCONDITION1(CONDITION) INVARIANT2(CONDITION, "Postcondition") -#define POSTCONDITION2(CONDITION, DIAGNOSTICS) \ - INVARIANT3(CONDITION, "Postcondition", DIAGNOSTICS) -#define POSTCONDITION(...) EXPAND_MACRO(REDIRECT(POSTCONDITION, __VA_ARGS__)) +#define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition") +#define POSTCONDITION_WITH_DIAGNOSTICS(CONDITION, ...) \ + INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Postcondition", __VA_ARGS__) #define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) @@ -359,28 +444,25 @@ invariant_violated_string( // A difference between CHECK_RETURN and POSTCONDITION is that CHECK_RETURN is // a statement about what the caller expects from a function, whereas a // POSTCONDITION is a statement about guarantees made by the function itself. -#define CHECK_RETURN1(CONDITION) INVARIANT2(CONDITION, "Check return value") -#define CHECK_RETURN2(CONDITION, DIAGNOSTICS) \ - INVARIANT3(CONDITION, "Check return value", DIAGNOSTICS) -#define CHECK_RETURN(...) EXPAND_MACRO(REDIRECT(CHECK_RETURN, __VA_ARGS__)) +#define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value") +#define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION, ...) \ + INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Check return value", __VA_ARGS__) #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \ EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) -// This should be used to mark dead code -#define UNREACHABLE INVARIANT2(false, "Unreachable") +/// This should be used to mark dead code +#define UNREACHABLE INVARIANT(false, "Unreachable") #define UNREACHABLE_STRUCTURED(TYPENAME, ...) \ EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)) -// This condition should be used to document that assumptions that are -// made on goto_functions, goto_programs, exprts, etc. being well formed. -// "The data structure is not corrupt or malformed" -#define DATA_INVARIANT2(CONDITION, REASON) INVARIANT2(CONDITION, REASON) -#define DATA_INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \ - INVARIANT3(CONDITION, REASON, DIAGNOSTICS) - -#define DATA_INVARIANT(...) EXPAND_MACRO(REDIRECT(DATA_INVARIANT, __VA_ARGS__)) +/// This condition should be used to document that assumptions that are +/// made on goto_functions, goto_programs, exprts, etc. being well formed. +/// "The data structure is not corrupt or malformed" +#define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON) +#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \ + INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, __VA_ARGS__) #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) @@ -389,8 +471,8 @@ invariant_violated_string( // The following should not be used in new code and are only intended // to migrate documentation and "error handling" in older code. -#define TODO INVARIANT2(false, "Todo") -#define UNIMPLEMENTED INVARIANT2(false, "Unimplemented") -#define UNHANDLED_CASE INVARIANT2(false, "Unhandled case") +#define TODO INVARIANT(false, "Todo") +#define UNIMPLEMENTED INVARIANT(false, "Unimplemented") +#define UNHANDLED_CASE INVARIANT(false, "Unhandled case") #endif // CPROVER_UTIL_INVARIANT_H diff --git a/src/util/source_location.h b/src/util/source_location.h index d09f8f2e36f..c7ea9daf804 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -10,9 +10,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_SOURCE_LOCATION_H #define CPROVER_UTIL_SOURCE_LOCATION_H +#include "invariant.h" #include "irep.h" #include "prefix.h" +#include + class source_locationt:public irept { public: @@ -188,4 +191,14 @@ class source_locationt:public irept std::ostream &operator <<(std::ostream &, const source_locationt &); +template <> +struct diagnostics_helpert +{ + static std::string + diagnostics_as_string(const source_locationt &source_location) + { + return "source location: " + source_location.as_string(); + } +}; + #endif // CPROVER_UTIL_SOURCE_LOCATION_H