From 8a37a2dd73d48d508ab0bf7a096fa0d1cd6db681 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 15 Aug 2018 14:41:46 +0100 Subject: [PATCH 1/3] Invariant macros with diagnostic information This overloads the invariant macros to take an additional optional argument to include diagnostic information. This can e.g. be useful when debugging an invariant violation without having access to the goto binary on which cbmc was run on. For example, one can now do both of DATA_INVARIANT(expr.operands().size() == 2, "binary expression") DATA_INVARIANT(expr.operands().size() == 2, "binary expression", expr.pretty()) --- src/util/invariant.cpp | 10 +++ src/util/invariant.h | 150 ++++++++++++++++++++++++++++++++++------- 2 files changed, 136 insertions(+), 24 deletions(-) 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..3aca1a1b00a 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,27 @@ invariant_violated_string( #define __this_function__ __func__ #endif -#define INVARIANT(CONDITION, REASON) \ +#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 \ + { \ + 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 +277,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,19 +308,25 @@ 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. + +#define INVARIANT(...) REDIRECT(INVARIANT, __VA_ARGS__) -// 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. +// 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 PRECONDITION1(CONDITION) INVARIANT2(CONDITION, "Precondition") +#define PRECONDITION2(CONDITION, DIAGNOSTICS) \ + INVARIANT3(CONDITION, "Precondition", DIAGNOSTICS) + +#define PRECONDITION(...) REDIRECT(PRECONDITION, __VA_ARGS__) + #define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) @@ -251,7 +338,12 @@ 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 POSTCONDITION1(CONDITION) INVARIANT2(CONDITION, "Postcondition") +#define POSTCONDITION2(CONDITION, DIAGNOSTICS) \ + INVARIANT3(CONDITION, "Postcondition", DIAGNOSTICS) + +#define POSTCONDITION(...) REDIRECT(POSTCONDITION, __VA_ARGS__) + #define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) @@ -263,19 +355,29 @@ 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_RETURN1(CONDITION) INVARIANT2(CONDITION, "Check return value") +#define CHECK_RETURN2(CONDITION, DIAGNOSTICS) \ + INVARIANT3(CONDITION, "Check return value", DIAGNOSTICS) + +#define CHECK_RETURN(...) REDIRECT(CHECK_RETURN, __VA_ARGS__) + #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \ INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) // This should be used to mark dead code -#define UNREACHABLE INVARIANT(false, "Unreachable") +#define UNREACHABLE INVARIANT2(false, "Unreachable") #define UNREACHABLE_STRUCTURED(TYPENAME, ...) \ 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_INVARIANT2(CONDITION, REASON) INVARIANT2(CONDITION, REASON) +#define DATA_INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \ + INVARIANT3(CONDITION, REASON, DIAGNOSTICS) + +#define DATA_INVARIANT(...) REDIRECT(DATA_INVARIANT, __VA_ARGS__) + #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) @@ -283,8 +385,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 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 From f2f2156c729aa16c121f62575279e8f21525dd95 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 16 Aug 2018 12:23:06 +0100 Subject: [PATCH 2/3] Tests for invariant macros with diagnostic output --- regression/invariants/driver.cpp | 16 ++++++++++++++++ .../invariants/invariant-failure14/test.desc | 12 ++++++++++++ .../invariants/invariant-failure15/test.desc | 11 +++++++++++ .../invariants/invariant-failure16/test.desc | 11 +++++++++++ .../invariants/invariant-failure17/test.desc | 11 +++++++++++ .../invariants/invariant-failure18/test.desc | 11 +++++++++++ 6 files changed, 72 insertions(+) create mode 100644 regression/invariants/invariant-failure14/test.desc create mode 100644 regression/invariants/invariant-failure15/test.desc create mode 100644 regression/invariants/invariant-failure16/test.desc create mode 100644 regression/invariants/invariant-failure17/test.desc create mode 100644 regression/invariants/invariant-failure18/test.desc 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$ From 1e2fda3e5da701e2b8df289cdd6a83dc32a754d8 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 16 Aug 2018 13:55:05 +0100 Subject: [PATCH 3/3] Workaround for Visual Studio not expanding __VA_ARGS__ on macro invocation --- src/util/invariant.h | 55 ++++++++++++++++++++++++-------------------- 1 file changed, 30 insertions(+), 25 deletions(-) diff --git a/src/util/invariant.h b/src/util/invariant.h index 3aca1a1b00a..11dd82e036f 100644 --- a/src/util/invariant.h +++ b/src/util/invariant.h @@ -249,6 +249,11 @@ invariant_violated_string( #define __this_function__ __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 @@ -257,16 +262,16 @@ invariant_violated_string( #define REDIRECT(MACRO, ...) \ do \ { \ - GET_MACRO( \ - __VA_ARGS__, \ - MACRO##6, \ - MACRO##5, \ - MACRO##4, \ - MACRO##3, \ - MACRO##2, \ - MACRO##1, \ - DUMMY_MACRO_ARG) \ - (__VA_ARGS__); \ + 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) \ @@ -311,7 +316,7 @@ invariant_violated_string( // Short hand macros. The variants *_STRUCTURED below allow to specify a custom // exception, and are equivalent to INVARIANT_STRUCTURED. -#define INVARIANT(...) REDIRECT(INVARIANT, __VA_ARGS__) +#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 @@ -325,10 +330,10 @@ invariant_violated_string( #define PRECONDITION2(CONDITION, DIAGNOSTICS) \ INVARIANT3(CONDITION, "Precondition", DIAGNOSTICS) -#define PRECONDITION(...) REDIRECT(PRECONDITION, __VA_ARGS__) +#define PRECONDITION(...) EXPAND_MACRO(REDIRECT(PRECONDITION, __VA_ARGS__)) -#define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ - INVARIANT_STRUCTURED(CONDITION, TYPENAME, __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. @@ -342,10 +347,10 @@ invariant_violated_string( #define POSTCONDITION2(CONDITION, DIAGNOSTICS) \ INVARIANT3(CONDITION, "Postcondition", DIAGNOSTICS) -#define POSTCONDITION(...) REDIRECT(POSTCONDITION, __VA_ARGS__) +#define POSTCONDITION(...) EXPAND_MACRO(REDIRECT(POSTCONDITION, __VA_ARGS__)) -#define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ - INVARIANT_STRUCTURED(CONDITION, TYPENAME, __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. @@ -359,15 +364,15 @@ invariant_violated_string( #define CHECK_RETURN2(CONDITION, DIAGNOSTICS) \ INVARIANT3(CONDITION, "Check return value", DIAGNOSTICS) -#define CHECK_RETURN(...) REDIRECT(CHECK_RETURN, __VA_ARGS__) +#define CHECK_RETURN(...) EXPAND_MACRO(REDIRECT(CHECK_RETURN, __VA_ARGS__)) -#define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \ - INVARIANT_STRUCTURED(CONDITION, TYPENAME, __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") -#define UNREACHABLE_STRUCTURED(TYPENAME, ...) \ - INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__) +#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. @@ -376,10 +381,10 @@ invariant_violated_string( #define DATA_INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \ INVARIANT3(CONDITION, REASON, DIAGNOSTICS) -#define DATA_INVARIANT(...) REDIRECT(DATA_INVARIANT, __VA_ARGS__) +#define DATA_INVARIANT(...) EXPAND_MACRO(REDIRECT(DATA_INVARIANT, __VA_ARGS__)) -#define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ - INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) +#define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ + EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) // Legacy annotations