Invariant macros with diagnostic information

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;
 }

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$

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$

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$

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$

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$

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';
+}

src/util/invariant.h

@@ -9,10 +9,11 @@ Author: Martin Brain, [email protected]
 #ifndef CPROVER_UTIL_INVARIANT_H
 #define CPROVER_UTIL_INVARIANT_H
 
+#include <cstdlib>
 #include <stdexcept>
-#include <type_traits>
 #include <string>
-#include <cstdlib>
+#include <tuple>
+#include <type_traits>
 
 /*
 ** 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<n> (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 <cassert>
 // 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<invariant_failedt>(
     file, function, line, condition, reason);
@@ -201,16 +249,54 @@ 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<n> (with 1 <= n <= 6) and calls
+// them with the arguments in __VA_ARGS__. The invocation of GET_MACRO() selects
+// MACRO<n> 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))                                                           \
       invariant_violated_string(                                               \
         __FILE__,                                                              \
         __this_function__,                                                     \
         __LINE__,                                                              \
+        #CONDITION,                                                            \
+        (REASON)); /* NOLINT */                                                \
+  } while(false)
+
+#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS)                             \
+  do /* NOLINT */                                                              \
+  {                                                                            \
+    if(!(CONDITION))                                                           \
+      invariant_violated_structured<invariant_with_diagnostics_failedt>(       \
+        __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