Introduce throwing a guard conversion exception

Throw the unwrapped exception as a string

Author: thk123

src/goto-symex/equation_conversion_exceptions.h

@@ -0,0 +1,50 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+/// \file
+/// Exceptions that can be raised during the equation conversion phase
+
+#ifndef CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
+#define CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
+
+#include <ostream>
+#include <util/namespace.h>
+#include "symex_target_equation.h"
+
+class guard_conversion_exceptiont : public std::runtime_error
+{
+public:
+  guard_conversion_exceptiont(
+    const symex_target_equationt::SSA_stept &step,
+    const namespacet &ns)
+    : runtime_error("Error converting guard for step"), step(step)
+  {
+    std::ostringstream error_msg;
+    error_msg << runtime_error::what();
+    error_msg << "\nStep:\n";
+    step.output(ns, error_msg);
+    error_message = error_msg.str();
+  }
+
+  explicit guard_conversion_exceptiont(
+    const symex_target_equationt::SSA_stept &step)
+    : guard_conversion_exceptiont(step, namespacet{symbol_tablet{}})
+  {
+  }
+
+  const char *what() const noexcept override
+  {
+    return error_message.c_str();
+  }
+
+private:
+  symex_target_equationt::SSA_stept step;
+  std::string error_message;
+};
+
+#endif // CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H

src/goto-symex/symex_target_equation.cpp

@@ -12,12 +12,15 @@ Author: Daniel Kroening, [email protected]
 #include "symex_target_equation.h"
 
 #include <util/std_expr.h>
+#include <util/unwrap_nested_exception.h>
 
 #include <langapi/language_util.h>
-#include <solvers/prop/prop_conv.h>
-#include <solvers/prop/prop.h>
+#include <solvers/flattening/bv_conversion_exceptions.h>
 #include <solvers/prop/literal_expr.h>
+#include <solvers/prop/prop.h>
+#include <solvers/prop/prop_conv.h>
 
+#include "equation_conversion_exceptions.h"
 #include "goto_symex_state.h"
 
 /// read from a shared variable
@@ -368,7 +371,17 @@ void symex_target_equationt::constraint(
 void symex_target_equationt::convert(
   prop_convt &prop_conv)
 {
-  convert_guards(prop_conv);
+  try
+  {
+    convert_guards(prop_conv);
+  }
+  catch(guard_conversion_exceptiont &guard_conversion_exception)
+  {
+    // unwrap the except and throw like normal
+    const std::string full_error = unwrap_exception(guard_conversion_exception);
+    throw full_error;
+  }
+
   convert_assignments(prop_conv);
   convert_decls(prop_conv);
   convert_assumptions(prop_conv);
@@ -417,7 +430,16 @@ void symex_target_equationt::convert_guards(
     if(step.ignore)
       step.guard_literal=const_literal(false);
     else
-      step.guard_literal=prop_conv.convert(step.guard);
+    {
+      try
+      {
+        step.guard_literal = prop_conv.convert(step.guard);
+      }
+      catch(const bitvector_conversion_exceptiont &conversion_exception)
+      {
+        std::throw_with_nested(guard_conversion_exceptiont(step));
+      }
+    }
   }
 }