diff --git a/regression/invariants/driver.cpp b/regression/invariants/driver.cpp index 58285dcc89d..3531955372e 100644 --- a/regression/invariants/driver.cpp +++ b/regression/invariants/driver.cpp @@ -91,6 +91,22 @@ int main(int argc, char** argv) DATA_INVARIANT(false, "Test invariant failure"); else if(arg=="irep") INVARIANT_WITH_IREP(false, "error with irep", pointer_type(void_typet())); + else if(arg == "invariant-diagnostics") + INVARIANT( + false, + "invariant with diagnostics failure", + "invariant diagnostics information"); + else if(arg == "precondition-diagnostics") + PRECONDITION(false, "precondition diagnostics information"); + else if(arg == "postcondition-diagnostics") + POSTCONDITION(false, "postcondition diagnostics information"); + else if(arg == "check-return-diagnostics") + CHECK_RETURN(false, "check return diagnostics information"); + else if(arg == "data-invariant-diagnostics") + DATA_INVARIANT( + false, + "data invariant with diagnostics failure", + "data invariant diagnostics information"); else return 1; } diff --git a/regression/invariants/invariant-failure14/test.desc b/regression/invariants/invariant-failure14/test.desc new file mode 100644 index 00000000000..75ad09ba644 --- /dev/null +++ b/regression/invariants/invariant-failure14/test.desc @@ -0,0 +1,12 @@ +CORE +dummy_parameter.c +invariant-diagnostics +^EXIT=(0|127|134|137)$ +^SIGNAL=0$ +--- begin invariant violation report --- +invariant with diagnostics failure +invariant diagnostics information +^(Backtrace)|(Backtraces not supported)$ +-- +^warning: ignoring +^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure15/test.desc b/regression/invariants/invariant-failure15/test.desc new file mode 100644 index 00000000000..e9fb9eebab5 --- /dev/null +++ b/regression/invariants/invariant-failure15/test.desc @@ -0,0 +1,11 @@ +CORE +dummy_parameter.c +precondition-diagnostics +^EXIT=(0|127|134|137)$ +^SIGNAL=0$ +--- begin invariant violation report --- +precondition diagnostics information +^(Backtrace)|(Backtraces not supported)$ +-- +^warning: ignoring +^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure16/test.desc b/regression/invariants/invariant-failure16/test.desc new file mode 100644 index 00000000000..261e7d51177 --- /dev/null +++ b/regression/invariants/invariant-failure16/test.desc @@ -0,0 +1,11 @@ +CORE +dummy_parameter.c +postcondition-diagnostics +^EXIT=(0|127|134|137)$ +^SIGNAL=0$ +--- begin invariant violation report --- +postcondition diagnostics information +^(Backtrace)|(Backtraces not supported)$ +-- +^warning: ignoring +^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure17/test.desc b/regression/invariants/invariant-failure17/test.desc new file mode 100644 index 00000000000..430a01274a4 --- /dev/null +++ b/regression/invariants/invariant-failure17/test.desc @@ -0,0 +1,11 @@ +CORE +dummy_parameter.c +check-return-diagnostics +^EXIT=(0|127|134|137)$ +^SIGNAL=0$ +--- begin invariant violation report --- +check return diagnostics information +^(Backtrace)|(Backtraces not supported)$ +-- +^warning: ignoring +^VERIFICATION SUCCESSFUL$ diff --git a/regression/invariants/invariant-failure18/test.desc b/regression/invariants/invariant-failure18/test.desc new file mode 100644 index 00000000000..94e1ba42e64 --- /dev/null +++ b/regression/invariants/invariant-failure18/test.desc @@ -0,0 +1,11 @@ +CORE +dummy_parameter.c +data-invariant-diagnostics +^EXIT=(0|127|134|137)$ +^SIGNAL=0$ +--- begin invariant violation report --- +data invariant diagnostics information +^(Backtrace)|(Backtraces not supported)$ +-- +^warning: ignoring +^VERIFICATION SUCCESSFUL$ diff --git a/src/util/invariant.cpp b/src/util/invariant.cpp index 0461d3b012a..a4ede14e9d7 100644 --- a/src/util/invariant.cpp +++ b/src/util/invariant.cpp @@ -125,3 +125,13 @@ std::string invariant_failedt::what() const noexcept << backtrace << '\n'; return out.str(); } + +std::string invariant_with_diagnostics_failedt::what() const noexcept +{ + std::string s(invariant_failedt::what()); + + if(!s.empty() && s.back() != '\n') + s += '\n'; + + return s + "Diagnostics: " + diagnostics + '\n'; +} diff --git a/src/util/invariant.h b/src/util/invariant.h index 3fc491e96f8..11dd82e036f 100644 --- a/src/util/invariant.h +++ b/src/util/invariant.h @@ -9,10 +9,11 @@ Author: Martin Brain, martin.brain@diffblue.com #ifndef CPROVER_UTIL_INVARIANT_H #define CPROVER_UTIL_INVARIANT_H +#include #include -#include #include -#include +#include +#include /* ** Invariants document conditions that the programmer believes to @@ -83,7 +84,7 @@ class invariant_failedt const std::string reason; public: - std::string what() const noexcept; + virtual std::string what() const noexcept; invariant_failedt( const std::string &_file, @@ -102,9 +103,47 @@ class invariant_failedt } }; +/// A class that includes diagnostic information related to an invariant +/// violation. +class invariant_with_diagnostics_failedt : public invariant_failedt +{ +private: + const std::string diagnostics; + +public: + virtual std::string what() const noexcept; + + invariant_with_diagnostics_failedt( + const std::string &_file, + const std::string &_function, + int _line, + const std::string &_backtrace, + const std::string &_condition, + const std::string &_reason, + const std::string &_diagnostics) + : invariant_failedt( + _file, + _function, + _line, + _backtrace, + _condition, + _reason), + diagnostics(_diagnostics) + { + } +}; + +// 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(). + #if defined(CPROVER_INVARIANT_CPROVER_ASSERT) // Used to allow CPROVER to check itself -#define INVARIANT(CONDITION, REASON) \ +#define INVARIANT2(CONDITION, REASON) \ + __CPROVER_assert((CONDITION), "Invariant : " REASON) +#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \ __CPROVER_assert((CONDITION), "Invariant : " REASON) #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ @@ -115,14 +154,23 @@ class 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 INVARIANT(CONDITION, REASON) do {} while(false) +#define INVARIANT2(CONDITION, REASON) \ + do \ + { \ + } while(false) +#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \ + do \ + { \ + } while(false) #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) do {} while(false) #elif defined(CPROVER_INVARIANT_ASSERT) // Not recommended but provided for backwards compatability #include // NOLINTNEXTLINE(*) -#define INVARIANT(CONDITION, REASON) assert((CONDITION) && ((REASON), true)) +#define INVARIANT2(CONDITION, REASON) assert((CONDITION) && ((REASON), true)) +#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \ + assert((CONDITION) && ((REASON), true)) /* NOLINT */ // NOLINTNEXTLINE(*) #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) assert((CONDITION)) #else @@ -185,8 +233,8 @@ invariant_violated_string( const std::string &file, const std::string &function, const int line, - const std::string &reason, - const std::string &condition) + const std::string &condition, + const std::string &reason) { invariant_violated_structured( file, function, line, condition, reason); @@ -201,7 +249,32 @@ invariant_violated_string( #define __this_function__ __func__ #endif -#define INVARIANT(CONDITION, REASON) \ +// 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) \ do /* NOLINT */ \ { \ if(!(CONDITION)) \ @@ -209,8 +282,21 @@ invariant_violated_string( __FILE__, \ __this_function__, \ __LINE__, \ + #CONDITION, \ + (REASON)); /* NOLINT */ \ + } while(false) + +#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \ + do /* NOLINT */ \ + { \ + if(!(CONDITION)) \ + invariant_violated_structured( \ + __FILE__, \ + __this_function__, \ + __LINE__, \ + #CONDITION, \ (REASON), \ - #CONDITION); /* NOLINT */ \ + (DIAGNOSTICS)); /* NOLINT */ \ } while(false) #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ @@ -227,21 +313,27 @@ invariant_violated_string( #endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block -// Short hand macros. The second variant of each one permits including an -// explanation or structured exception, in which case they are synonyms -// for INVARIANT. +// Short hand macros. The variants *_STRUCTURED below allow to specify a custom +// exception, and are equivalent to INVARIANT_STRUCTURED. -// The condition should only contain (unmodified) arguments to the method. -// Inputs include arguments passed to the function, as well as member -// variables that the function may read. +#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. // "The design of the system means that the arguments to this method // will always meet this condition". // // The PRECONDITION documents / checks assumptions about the inputs // that is the caller's responsibility to make happen before the call. -#define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition") -#define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ - INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) +#define PRECONDITION1(CONDITION) INVARIANT2(CONDITION, "Precondition") +#define PRECONDITION2(CONDITION, DIAGNOSTICS) \ + INVARIANT3(CONDITION, "Precondition", DIAGNOSTICS) + +#define PRECONDITION(...) EXPAND_MACRO(REDIRECT(PRECONDITION, __VA_ARGS__)) + +#define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ + EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) // The condition should only contain variables that will be returned / // output without further modification. @@ -251,9 +343,14 @@ 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 POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition") -#define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ - INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) +#define POSTCONDITION1(CONDITION) INVARIANT2(CONDITION, "Postcondition") +#define POSTCONDITION2(CONDITION, DIAGNOSTICS) \ + INVARIANT3(CONDITION, "Postcondition", DIAGNOSTICS) + +#define POSTCONDITION(...) EXPAND_MACRO(REDIRECT(POSTCONDITION, __VA_ARGS__)) + +#define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ + EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) // The condition should only contain (unmodified) values that were // changed by a previous method call. @@ -263,28 +360,38 @@ 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_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value") -#define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \ - INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) +#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_STRUCTURED(CONDITION, TYPENAME, ...) \ + EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) // This should be used to mark dead code -#define UNREACHABLE INVARIANT(false, "Unreachable") -#define UNREACHABLE_STRUCTURED(TYPENAME, ...) \ - INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__) +#define UNREACHABLE INVARIANT2(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 corrupt or malformed" -#define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON) -#define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ - INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) +#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__)) + +#define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ + EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) // Legacy annotations // The following should not be used in new code and are only intended // to migrate documentation and "error handling" in older code. -#define TODO INVARIANT(false, "Todo") -#define UNIMPLEMENTED INVARIANT(false, "Unimplemented") -#define UNHANDLED_CASE INVARIANT(false, "Unhandled case") +#define TODO INVARIANT2(false, "Todo") +#define UNIMPLEMENTED INVARIANT2(false, "Unimplemented") +#define UNHANDLED_CASE INVARIANT2(false, "Unhandled case") #endif // CPROVER_UTIL_INVARIANT_H