[TG-2922] Improve logging for byte flatten exceptions

regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.java

@@ -0,0 +1,7 @@
+public class TestClass {
+  public static void f(int y) {
+    float[][] a1 = new float[y][3];
+    int j = 0;
+    a1[j][0] = 34.5f;
+  }
+}

regression/cbmc-java/dynamic-multi-dimensional-array/test.desc

@@ -0,0 +1,10 @@
+CORE
+TestClass.class
+--function TestClass.f --cover location --unwind 2
+Source GOTO statement: .*
+(^ exception: Can't convert byte_extraction|Nested exception printing not supported on Windows)
+^EXIT=6$
+--
+--
+The exception thrown in this test is the symptom of a bug; the purpose of this
+test is the validate the output of that exception

src/goto-symex/equation_conversion_exceptions.h

@@ -0,0 +1,47 @@
+/*******************************************************************\
+
+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/format_expr.h>
+
+#include "symex_target_equation.h"
+
+class equation_conversion_exceptiont : public std::runtime_error
+{
+public:
+  equation_conversion_exceptiont(
+    const std::string &message,
+    const symex_target_equationt::SSA_stept &step)
+    : runtime_error(message), step(step)
+  {
+    std::ostringstream error_msg;
+    error_msg << runtime_error::what();
+    error_msg << "\nSource GOTO statement: " << format(step.source.pc->code);
+    error_msg << "\nStep:\n";
+    step.output(error_msg);
+    error_message = error_msg.str();
+  }
+
+  const char *what() const optional_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

@@ -11,13 +11,20 @@ Author: Daniel Kroening, [email protected]
 
 #include "symex_target_equation.h"
 
+#include <util/format_expr.h>
 #include <util/std_expr.h>
+#include <util/throw_with_nested.h>
+#include <util/unwrap_nested_exception.h>
 
+// Can be removed once deprecated SSA_stept::output is removed
 #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,14 +375,23 @@ void symex_target_equationt::constraint(
 void symex_target_equationt::convert(
   prop_convt &prop_conv)
 {
-  convert_guards(prop_conv);
-  convert_assignments(prop_conv);
-  convert_decls(prop_conv);
-  convert_assumptions(prop_conv);
-  convert_assertions(prop_conv);
-  convert_goto_instructions(prop_conv);
-  convert_io(prop_conv);
-  convert_constraints(prop_conv);
+  try
+  {
+    convert_guards(prop_conv);
+    convert_assignments(prop_conv);
+    convert_decls(prop_conv);
+    convert_assumptions(prop_conv);
+    convert_assertions(prop_conv);
+    convert_goto_instructions(prop_conv);
+    convert_io(prop_conv);
+    convert_constraints(prop_conv);
+  }
+  catch(const equation_conversion_exceptiont &conversion_exception)
+  {
+    // unwrap the except and throw like normal
+    const std::string full_error = unwrap_exception(conversion_exception);
+    throw full_error;
+  }
 }
 
 /// converts assignments
@@ -402,7 +418,16 @@ void symex_target_equationt::convert_decls(
     {
       // The result is not used, these have no impact on
       // the satisfiability of the formula.
-      prop_conv.convert(step.cond_expr);
+      try
+      {
+        prop_conv.convert(step.cond_expr);
+      }
+      catch(const bitvector_conversion_exceptiont &conversion_exception)
+      {
+        util_throw_with_nested(
+          equation_conversion_exceptiont(
+            "Error converting decls for step", step));
+      }
     }
   }
 }
@@ -417,7 +442,18 @@ 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)
+      {
+        util_throw_with_nested(
+          equation_conversion_exceptiont(
+            "Error converting guard for step", step));
+      }
+    }
   }
 }
 
@@ -433,7 +469,18 @@ void symex_target_equationt::convert_assumptions(
       if(step.ignore)
         step.cond_literal=const_literal(true);
       else
-        step.cond_literal=prop_conv.convert(step.cond_expr);
+      {
+        try
+        {
+          step.cond_literal = prop_conv.convert(step.cond_expr);
+        }
+        catch(const bitvector_conversion_exceptiont &conversion_exception)
+        {
+          util_throw_with_nested(
+            equation_conversion_exceptiont(
+              "Error converting assumptions for step", step));
+        }
+      }
     }
   }
 }
@@ -450,7 +497,18 @@ void symex_target_equationt::convert_goto_instructions(
       if(step.ignore)
         step.cond_literal=const_literal(true);
       else
-        step.cond_literal=prop_conv.convert(step.cond_expr);
+      {
+        try
+        {
+          step.cond_literal = prop_conv.convert(step.cond_expr);
+        }
+        catch(const bitvector_conversion_exceptiont &conversion_exception)
+        {
+          util_throw_with_nested(
+            equation_conversion_exceptiont(
+              "Error converting goto instructions for step", step));
+        }
+      }
     }
   }
 }
@@ -519,7 +577,16 @@ void symex_target_equationt::convert_assertions(
         step.cond_expr);
 
       // do the conversion
-      step.cond_literal=prop_conv.convert(implication);
+      try
+      {
+        step.cond_literal = prop_conv.convert(implication);
+      }
+      catch(const bitvector_conversion_exceptiont &conversion_exception)
+      {
+        util_throw_with_nested(
+          equation_conversion_exceptiont(
+            "Error converting assertions for step", step));
+      }
 
       // store disjunct
       disjuncts.push_back(literal_exprt(!step.cond_literal));
@@ -703,3 +770,118 @@ void symex_target_equationt::SSA_stept::output(
 
   out << "Guard: " << from_expr(ns, source.pc->function, guard) << '\n';
 }
+
+void symex_target_equationt::SSA_stept::output(std::ostream &out) const
+{
+  if(source.is_set)
+  {
+    out << "Thread " << source.thread_nr;
+
+    if(source.pc->source_location.is_not_nil())
+      out << " " << source.pc->source_location << '\n';
+    else
+      out << '\n';
+  }
+
+  switch(type)
+  {
+  case goto_trace_stept::typet::ASSERT:
+    out << "ASSERT " << format(cond_expr) << '\n';
+    break;
+  case goto_trace_stept::typet::ASSUME:
+    out << "ASSUME " << format(cond_expr) << '\n';
+    break;
+  case goto_trace_stept::typet::LOCATION:
+    out << "LOCATION" << '\n';
+    break;
+  case goto_trace_stept::typet::INPUT:
+    out << "INPUT" << '\n';
+    break;
+  case goto_trace_stept::typet::OUTPUT:
+    out << "OUTPUT" << '\n';
+    break;
+
+  case goto_trace_stept::typet::DECL:
+    out << "DECL" << '\n';
+    out << format(ssa_lhs) << '\n';
+    break;
+
+  case goto_trace_stept::typet::ASSIGNMENT:
+    out << "ASSIGNMENT (";
+    switch(assignment_type)
+    {
+    case assignment_typet::HIDDEN:
+      out << "HIDDEN";
+      break;
+    case assignment_typet::STATE:
+      out << "STATE";
+      break;
+    case assignment_typet::VISIBLE_ACTUAL_PARAMETER:
+      out << "VISIBLE_ACTUAL_PARAMETER";
+      break;
+    case assignment_typet::HIDDEN_ACTUAL_PARAMETER:
+      out << "HIDDEN_ACTUAL_PARAMETER";
+      break;
+    case assignment_typet::PHI:
+      out << "PHI";
+      break;
+    case assignment_typet::GUARD:
+      out << "GUARD";
+      break;
+    default:
+    {
+    }
+    }
+
+    out << ")\n";
+    break;
+
+  case goto_trace_stept::typet::DEAD:
+    out << "DEAD\n";
+    break;
+  case goto_trace_stept::typet::FUNCTION_CALL:
+    out << "FUNCTION_CALL\n";
+    break;
+  case goto_trace_stept::typet::FUNCTION_RETURN:
+    out << "FUNCTION_RETURN\n";
+    break;
+  case goto_trace_stept::typet::CONSTRAINT:
+    out << "CONSTRAINT\n";
+    break;
+  case goto_trace_stept::typet::SHARED_READ:
+    out << "SHARED READ\n";
+    break;
+  case goto_trace_stept::typet::SHARED_WRITE:
+    out << "SHARED WRITE\n";
+    break;
+  case goto_trace_stept::typet::ATOMIC_BEGIN:
+    out << "ATOMIC_BEGIN\n";
+    break;
+  case goto_trace_stept::typet::ATOMIC_END:
+    out << "AUTOMIC_END\n";
+    break;
+  case goto_trace_stept::typet::SPAWN:
+    out << "SPAWN\n";
+    break;
+  case goto_trace_stept::typet::MEMORY_BARRIER:
+    out << "MEMORY_BARRIER\n";
+    break;
+  case goto_trace_stept::typet::GOTO:
+    out << "IF " << format(cond_expr) << " GOTO\n";
+    break;
+
+  default:
+    UNREACHABLE;
+  }
+
+  if(is_assert() || is_assume() || is_assignment() || is_constraint())
+    out << format(cond_expr) << '\n';
+
+  if(is_assert() || is_constraint())
+    out << comment << '\n';
+
+  if(is_shared_read() || is_shared_write())
+    out << format(ssa_lhs) << '\n';
+
+  out << "Guard: " << format(guard) << '\n';
+}

src/goto-symex/symex_target_equation.h

@@ -32,7 +32,6 @@ class prop_convt;
 class symex_target_equationt:public symex_targett
 {
 public:
-  symex_target_equationt() = default;
   virtual ~symex_target_equationt() = default;
 
   // read event
@@ -257,9 +256,12 @@ class symex_target_equationt:public symex_targett
     {
     }
 
+    DEPRECATED("Use output without ns param")
     void output(
       const namespacet &ns,
       std::ostream &out) const;
+
+    void output(std::ostream &out) const;
   };
 
   std::size_t count_assertions() const

src/solvers/flattening/boolbv.cpp

@@ -152,6 +152,14 @@ bvt boolbvt::conversion_failed(const exprt &expr)
   return prop.new_variables(width);
 }
 
+/// Converts an expression into its gate-level representation and returns a
+/// vector of literals corresponding to the outputs of the Boolean circuit.
+/// \param expr: Expression to convert
+/// \return A vector of literals corresponding to the outputs of the Boolean
+///   circuit
+/// \throws bitvector_conversion_exceptiont raised if converting byte_extraction
+/// goes wrong.
+/// TODO: extend for other types of conversion exception (diffblue/cbmc#2103).
 bvt boolbvt::convert_bitvector(const exprt &expr)
 {
   if(expr.type().id()==ID_bool)