Merge pull request #1231 from smowton/smowton/feature/invariant_with_irep

Add standard invariant subclass with irep member

Author: smowton

regression/invariants/Makefile

@@ -4,7 +4,8 @@ SRC = driver.cpp
 
 INCLUDES = -I ../../src
 
-OBJ += ../../src/util/util$(LIBEXT)
+OBJ += ../../src/big-int/big-int$(LIBEXT) \
+      ../../src/util/util$(LIBEXT)
 
 include ../../src/config.inc
 include ../../src/common

regression/invariants/driver.cpp

@@ -12,6 +12,8 @@ Author: Chris Smowton, [email protected]
 #include <string>
 #include <sstream>
 #include <util/invariant.h>
+#include <util/invariant_utils.h>
+#include <util/std_types.h>
 
 /// An example of structured invariants-- this contains fields to
 /// describe the error to a catcher, and also produces a human-readable
@@ -83,6 +85,8 @@ int main(int argc, char** argv)
     DATA_INVARIANT_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
   else if(arg=="data-invariant-string")
     DATA_INVARIANT(false, "Test invariant failure");
+  else if(arg=="irep")
+    INVARIANT_WITH_IREP(false, "error with irep", pointer_typet(void_typet()));
   else
     return 1;
 }

regression/invariants/invariant-failure13/test.desc

@@ -0,0 +1,14 @@
+CORE
+dummy_parameter.c
+irep
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+error with irep
+pointer
+0: empty
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

src/util/Makefile

@@ -31,6 +31,7 @@ SRC = arith_tools.cpp \
       irep_hash_container.cpp \
       irep_ids.cpp \
       irep_serialization.cpp \
+      invariant_utils.cpp \
       json.cpp \
       json_expr.cpp \
       json_irep.cpp \

src/util/invariant.cpp

@@ -129,7 +129,7 @@ std::string invariant_failedt::get_invariant_failed_message(
       << " function " << function
       << " line " << line << '\n'
       << "Reason: " << reason
-      << "Backtrace:\n"
+      << "\nBacktrace:\n"
       << backtrace << '\n';
   return out.str();
 }

src/util/invariant_utils.cpp

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: Invariant helper utilities
+
+Author: Chris Smowton, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Invariant helper utilities
+
+#include "invariant_utils.h"
+
+std::string pretty_print_invariant_with_irep(
+  const irept &problem_node,
+  const std::string &description)
+{
+  if(problem_node.is_nil())
+    return description;
+  else
+  {
+    std::string ret=description;
+    ret+="\nProblem irep:\n";
+    ret+=problem_node.pretty(0,0);
+    return ret;
+  }
+}

src/util/invariant_utils.h

@@ -0,0 +1,48 @@
+/*******************************************************************\
+
+Module: Invariant helper utilities
+
+Author: Chris Smowton, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_INVARIANT_TYPES_H
+#define CPROVER_UTIL_INVARIANT_TYPES_H
+
+#include "invariant.h"
+
+#include <util/irep.h>
+
+#include <string>
+
+/// Produces a plain string error description from an irep and some
+/// explanatory text. If `problem_node` is nil, returns `description`.
+/// \param problem_node: irep to pretty-print
+/// \param description: descriptive text to prepend
+/// \return error message
+std::string pretty_print_invariant_with_irep(
+  const irept &problem_node,
+  const std::string &description);
+
+/// Equivalent to
+/// `INVARIANT_STRUCTURED(CONDITION, invariant_failedt,
+///   pretty_print_invariant_with_irep(IREP, DESCRIPTION))`
+#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)               \
+  INVARIANT_STRUCTURED(                                                 \
+    CONDITION,                                                          \
+    invariant_failedt,                                                  \
+    pretty_print_invariant_with_irep((IREP), (DESCRIPTION)))
+
+/// See `INVARIANT_WITH_IREP`
+#define PRECONDITION_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
+  INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
+#define POSTCONDITION_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
+  INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
+#define CHECK_RETURN_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
+  INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
+#define UNREACHABLE_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
+  INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
+#define DATA_INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
+  INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
+
+#endif