Merge pull request #4691 from tautschnig/remove-flattening-exceptions

Remove now-unused bitvector conversion exceptions

Author: tautschnig

src/goto-symex/equation_conversion_exceptions.h

@@ -14,13 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/format_expr.h>
 #include <util/std_expr.h>
-#include <util/throw_with_nested.h>
-#include <util/unwrap_nested_exception.h>
 
 #include <solvers/decision_procedure.h>
-#include <solvers/flattening/bv_conversion_exceptions.h>
 
-#include "equation_conversion_exceptions.h"
 #include "goto_symex_state.h"
 #include "ssa_step.h"
 
@@ -329,24 +325,15 @@ void symex_target_equationt::constraint(
 
 void symex_target_equationt::convert(decision_proceduret &decision_procedure)
 {
-  try
-  {
-    convert_guards(decision_procedure);
-    convert_assignments(decision_procedure);
-    convert_decls(decision_procedure);
-    convert_assumptions(decision_procedure);
-    convert_assertions(decision_procedure);
-    convert_goto_instructions(decision_procedure);
-    convert_function_calls(decision_procedure);
-    convert_io(decision_procedure);
-    convert_constraints(decision_procedure);
-  }
-  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;
-  }
+  convert_guards(decision_procedure);
+  convert_assignments(decision_procedure);
+  convert_decls(decision_procedure);
+  convert_assumptions(decision_procedure);
+  convert_assertions(decision_procedure);
+  convert_goto_instructions(decision_procedure);
+  convert_function_calls(decision_procedure);
+  convert_io(decision_procedure);
+  convert_constraints(decision_procedure);
 }
 
 void symex_target_equationt::convert_assignments(
@@ -376,17 +363,8 @@ void symex_target_equationt::convert_decls(
     {
       // The result is not used, these have no impact on
       // the satisfiability of the formula.
-      try
-      {
-        decision_procedure.handle(step.cond_expr);
-        step.converted = true;
-      }
-      catch(const bitvector_conversion_exceptiont &)
-      {
-        util_throw_with_nested(
-          equation_conversion_exceptiont(
-            "Error converting decls for step", step));
-      }
+      decision_procedure.handle(step.cond_expr);
+      step.converted = true;
     }
   }
 }
@@ -405,16 +383,7 @@ void symex_target_equationt::convert_guards(
         mstream << messaget::eom;
       });
 
-      try
-      {
-        step.guard_handle = decision_procedure.handle(step.guard);
-      }
-      catch(const bitvector_conversion_exceptiont &)
-      {
-        util_throw_with_nested(
-          equation_conversion_exceptiont(
-            "Error converting guard for step", step));
-      }
+      step.guard_handle = decision_procedure.handle(step.guard);
     }
   }
 }
@@ -436,16 +405,7 @@ void symex_target_equationt::convert_assumptions(
             mstream << messaget::eom;
           });
 
-        try
-        {
-          step.cond_handle = decision_procedure.handle(step.cond_expr);
-        }
-        catch(const bitvector_conversion_exceptiont &)
-        {
-          util_throw_with_nested(
-            equation_conversion_exceptiont(
-              "Error converting assumptions for step", step));
-        }
+        step.cond_handle = decision_procedure.handle(step.cond_expr);
       }
     }
   }
@@ -468,16 +428,7 @@ void symex_target_equationt::convert_goto_instructions(
             mstream << messaget::eom;
           });
 
-        try
-        {
-          step.cond_handle = decision_procedure.handle(step.cond_expr);
-        }
-        catch(const bitvector_conversion_exceptiont &)
-        {
-          util_throw_with_nested(
-            equation_conversion_exceptiont(
-              "Error converting goto instructions for step", step));
-        }
+        step.cond_handle = decision_procedure.handle(step.cond_expr);
       }
     }
   }
@@ -495,16 +446,8 @@ void symex_target_equationt::convert_constraints(
         mstream << messaget::eom;
       });
 
-      try
-      {
-        decision_procedure.set_to_true(step.cond_expr);
-        step.converted = true;
-      }
-      catch(const bitvector_conversion_exceptiont &)
-      {
-        util_throw_with_nested(equation_conversion_exceptiont(
-          "Error converting constraints for step", step));
-      }
+      decision_procedure.set_to_true(step.cond_expr);
+      step.converted = true;
     }
   }
 }
@@ -569,16 +512,7 @@ void symex_target_equationt::convert_assertions(
         step.cond_expr);
 
       // do the conversion
-      try
-      {
-        step.cond_handle = decision_procedure.handle(implication);
-      }
-      catch(const bitvector_conversion_exceptiont &)
-      {
-        util_throw_with_nested(
-          equation_conversion_exceptiont(
-            "Error converting assertions for step", step));
-      }
+      step.cond_handle = decision_procedure.handle(implication);
 
       // store disjunct
       disjuncts.push_back(not_exprt(step.cond_handle));

src/goto-symex/symex_target_equation.cpp

@@ -171,9 +171,6 @@ bvt boolbvt::conversion_failed(const exprt &expr)
 /// \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)

src/solvers/flattening/boolbv.cpp

@@ -15,12 +15,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr_util.h>
 #include <util/pointer_offset_size.h>
 #include <util/std_expr.h>
-#include <util/throw_with_nested.h>
 
 #include <solvers/lowering/expr_lowering.h>
-#include <solvers/lowering/flatten_byte_extract_exceptions.h>
 
-#include "bv_conversion_exceptions.h"
 #include "bv_endianness_map.h"
 
 bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
@@ -45,15 +42,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   // unbounded arrays
   if(is_unbounded_array(expr.op().type()))
   {
-    try
-    {
-      return convert_bv(lower_byte_extract(expr, ns));
-    }
-    catch(const flatten_byte_extract_exceptiont &)
-    {
-      util_throw_with_nested(
-        bitvector_conversion_exceptiont("Can't convert byte_extraction", expr));
-    }
+    return convert_bv(lower_byte_extract(expr, ns));
   }
 
   const std::size_t width = boolbv_width(expr.type());

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -12,12 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/byte_operators.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
-#include <util/throw_with_nested.h>
 
 #include <solvers/lowering/expr_lowering.h>
-#include <solvers/lowering/flatten_byte_extract_exceptions.h>
 
-#include "bv_conversion_exceptions.h"
 #include "bv_endianness_map.h"
 
 bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
@@ -28,15 +25,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
     is_unbounded_array(expr.op().type()) ||
     is_unbounded_array(expr.value().type()))
   {
-    try
-    {
-      return convert_bv(lower_byte_update(expr, ns));
-    }
-    catch(const flatten_byte_extract_exceptiont &byte_extract_flatten_exception)
-    {
-      util_throw_with_nested(
-        bitvector_conversion_exceptiont("Can't convert byte_update", expr));
-    }
+    return convert_bv(lower_byte_update(expr, ns));
   }
 
   const exprt &op = expr.op();

src/solvers/flattening/boolbv_byte_update.cpp

@@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <solvers/lowering/expr_lowering.h>
 
-#include "bv_conversion_exceptions.h"
-
 literalt boolbvt::convert_equality(const equal_exprt &expr)
 {
   const bool equality_types_match = expr.lhs().type() == expr.rhs().type();

src/solvers/flattening/boolbv_equality.cpp

@@ -21,8 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/string_constant.h>
 
-#include "flatten_byte_extract_exceptions.h"
-
 static exprt bv_to_expr(
   const exprt &bitvector_expr,
   const typet &target_type,