Introduce exceptions for all conversion steps.

Author: thk123

src/goto-symex/equation_conversion_exceptions.h

@@ -13,17 +13,21 @@ Author: Diffblue Ltd.
 #define CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
 
 #include <ostream>
+
 #include <util/namespace.h>
+
 #include <langapi/language_util.h>
+
 #include "symex_target_equation.h"
 
-class guard_conversion_exceptiont : public std::runtime_error
+class equation_conversion_exceptiont : public std::runtime_error
 {
 public:
-  guard_conversion_exceptiont(
+  equation_conversion_exceptiont(
+    const std::string &message,
     const symex_target_equationt::SSA_stept &step,
     const namespacet &ns)
-    : runtime_error("Error converting guard for step"), step(step)
+    : runtime_error(message), step(step)
   {
     std::ostringstream error_msg;
     error_msg << runtime_error::what();
@@ -34,9 +38,10 @@ class guard_conversion_exceptiont : public std::runtime_error
     error_message = error_msg.str();
   }
 
-  explicit guard_conversion_exceptiont(
+  explicit equation_conversion_exceptiont(
+    const std::string &message,
     const symex_target_equationt::SSA_stept &step)
-    : guard_conversion_exceptiont(step, namespacet{symbol_tablet{}})
+    : equation_conversion_exceptiont(message, step, namespacet{symbol_tablet{}})
   {
   }
 
@@ -50,4 +55,24 @@ class guard_conversion_exceptiont : public std::runtime_error
   std::string error_message;
 };
 
+class guard_conversion_exceptiont : public equation_conversion_exceptiont
+{
+public:
+  guard_conversion_exceptiont(
+    const symex_target_equationt::SSA_stept &step,
+    const namespacet &ns)
+    : equation_conversion_exceptiont(
+        "Error converting guard for step",
+        step,
+        ns)
+  {
+  }
+
+  explicit guard_conversion_exceptiont(
+    const symex_target_equationt::SSA_stept &step)
+    : guard_conversion_exceptiont(step, namespacet{symbol_tablet{}})
+  {
+  }
+};
+
 #endif // CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H

src/goto-symex/symex_target_equation.cpp

@@ -375,21 +375,20 @@ void symex_target_equationt::convert(
   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(guard_conversion_exceptiont &guard_conversion_exception)
+  catch(const equation_conversion_exceptiont &conversion_exception)
   {
     // unwrap the except and throw like normal
-    const std::string full_error = unwrap_exception(guard_conversion_exception);
+    const std::string full_error = unwrap_exception(conversion_exception);
     throw full_error;
   }
-
-  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);
 }
 
 /// converts assignments
@@ -416,7 +415,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, ns));
+      }
     }
   }
 }
@@ -438,7 +446,9 @@ void symex_target_equationt::convert_guards(
       }
       catch(const bitvector_conversion_exceptiont &conversion_exception)
       {
-        util_throw_with_nested(guard_conversion_exceptiont(step, ns));
+        util_throw_with_nested(
+          equation_conversion_exceptiont(
+            "Error converting guard for step", step, ns));
       }
     }
   }
@@ -456,7 +466,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, ns));
+        }
+      }
     }
   }
 }
@@ -473,7 +494,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, ns));
+        }
+      }
     }
   }
 }
@@ -542,7 +574,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, ns));
+      }
 
       // store disjunct
       disjuncts.push_back(literal_exprt(!step.cond_literal));