Merge pull request #2940 from danpoe/refactor/error-handling-solvers-flattening-from-boolbv-with

Error handling cleanup in solvers/flattening 6

Author: tautschnig

src/solvers/flattening/bv_minimize.cpp

@@ -8,8 +8,6 @@ Author: Georg Weissenbacher, [email protected]
 
 #include "bv_minimize.h"
 
-#include <cassert>
-
 #include <solvers/prop/minimize.h>
 
 void bv_minimizet::add_objective(

src/solvers/flattening/bv_pointers.cpp

@@ -11,12 +11,12 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/exception_utils.h>
 #include <util/pointer_offset_size.h>
 
 literalt bv_pointerst::convert_rest(const exprt &expr)
 {
-  if(expr.type().id()!=ID_bool)
-    throw "bv_pointerst::convert_rest got non-boolean operand";
+  PRECONDITION(expr.type().id() == ID_bool);
 
   const exprt::operandst &operands=expr.operands();
 
@@ -112,9 +112,6 @@ bool bv_pointerst::convert_address_of_rec(
   }
   else if(expr.id()==ID_index)
   {
-    if(expr.operands().size()!=2)
-      throw "index takes two operands";
-
     const index_exprt &index_expr=to_index_expr(expr);
     const exprt &array=index_expr.array();
     const exprt &index=index_expr.index();
@@ -182,12 +179,13 @@ bool bv_pointerst::convert_address_of_rec(
       // add offset
       offset_arithmetic(bv, offset);
     }
-    else if(struct_op_type.id()==ID_union)
+    else
     {
+      INVARIANT(
+        struct_op_type.id() == ID_union,
+        "member expression should operate on struct or union");
       // nothing to do, all members have offset 0
     }
-    else
-      throw "member takes struct or union operand";
 
     return false;
   }
@@ -222,8 +220,7 @@ bool bv_pointerst::convert_address_of_rec(
 
 bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 {
-  if(expr.type().id()!=ID_pointer)
-    throw "convert_pointer_type got non-pointer type";
+  PRECONDITION(expr.type().id() == ID_pointer);
 
   // make sure the config hasn't been changed
   PRECONDITION(bits==boolbv_width(expr.type()));
@@ -252,10 +249,9 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   }
   else if(expr.id()==ID_typecast)
   {
-    if(expr.operands().size()!=1)
-      throw "typecast takes one operand";
+    const typecast_exprt &typecast_expr = to_typecast_expr(expr);
 
-    const exprt &op=expr.op0();
+    const exprt &op = typecast_expr.op();
     const typet &op_type=ns.follow(op.type());
 
     if(op_type.id()==ID_pointer)
@@ -288,15 +284,14 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   }
   else if(expr.id()==ID_address_of)
   {
-    if(expr.operands().size()!=1)
-      throw expr.id_string()+" takes one operand";
+    const address_of_exprt &address_of_expr = to_address_of_expr(expr);
 
     bvt bv;
     bv.resize(bits);
 
-    if(convert_address_of_rec(expr.op0(), bv))
+    if(convert_address_of_rec(address_of_expr.op(), bv))
     {
-      conversion_failed(expr, bv);
+      conversion_failed(address_of_expr, bv);
       return bv;
     }
 
@@ -324,15 +319,14 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   {
     // this has to be pointer plus integer
 
-    if(expr.operands().size()<2)
-      throw "operator + takes at least two operands";
+    const plus_exprt &plus_expr = to_plus_expr(expr);
 
     bvt bv;
 
     mp_integer size=0;
     std::size_t count=0;
 
-    forall_operands(it, expr)
+    forall_operands(it, plus_expr)
     {
       if(it->type().id()==ID_pointer)
       {
@@ -356,14 +350,13 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       }
     }
 
-    if(count==0)
-      throw "found no pointer in pointer-type sum";
-    else if(count!=1)
-      throw "found more than one pointer in sum";
+    INVARIANT(
+      count == 1,
+      "there should be exactly one pointer-type operand in a pointer-type sum");
 
     bvt sum=bv_utils.build_constant(0, bits);
 
-    forall_operands(it, expr)
+    forall_operands(it, plus_expr)
     {
       if(it->type().id()==ID_pointer)
         continue;
@@ -372,7 +365,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
          it->type().id()!=ID_signedbv)
       {
         bvt bv;
-        conversion_failed(expr, bv);
+        conversion_failed(plus_expr, bv);
         return bv;
       }
 
@@ -381,9 +374,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
                                      bv_utilst::representationt::UNSIGNED;
 
       bvt op=convert_bv(*it);
-
-      if(op.empty())
-        throw "unexpected pointer arithmetic operand width";
+      CHECK_RETURN(!op.empty());
 
       // we cut any extra bits off
 
@@ -403,27 +394,28 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   {
     // this is pointer-integer
 
-    if(expr.operands().size()!=2)
-      throw "operator "+expr.id_string()+" takes two operands";
+    const minus_exprt &minus_expr = to_minus_expr(expr);
 
-    if(expr.op0().type().id()!=ID_pointer)
-      throw "found no pointer in pointer type in difference";
+    INVARIANT(
+      minus_expr.op0().type().id() == ID_pointer,
+      "first operand should be of pointer type");
 
     bvt bv;
 
-    if(expr.op1().type().id()!=ID_unsignedbv &&
-       expr.op1().type().id()!=ID_signedbv)
+    if(
+      minus_expr.op1().type().id() != ID_unsignedbv &&
+      minus_expr.op1().type().id() != ID_signedbv)
     {
       bvt bv;
-      conversion_failed(expr, bv);
+      conversion_failed(minus_expr, bv);
       return bv;
     }
 
-    const unary_minus_exprt neg_op1(expr.op1());
+    const unary_minus_exprt neg_op1(minus_expr.op1());
 
-    bv=convert_bv(expr.op0());
+    bv = convert_bv(minus_expr.op0());
 
-    typet pointer_sub_type=expr.op0().type().subtype();
+    typet pointer_sub_type = minus_expr.op0().type().subtype();
     mp_integer element_size;
 
     if(pointer_sub_type.id()==ID_empty)
@@ -462,11 +454,15 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   {
     return SUB::convert_byte_extract(to_byte_extract_expr(expr));
   }
-  else if(
-    expr.id() == ID_byte_update_little_endian ||
-    expr.id() == ID_byte_update_big_endian)
+  else
   {
-    throw "byte-wise updates of pointers are unsupported";
+    INVARIANT(
+      expr.id() != ID_byte_update_little_endian,
+      "byte-wise pointer updates are unsupported");
+
+    INVARIANT(
+      expr.id() != ID_byte_update_big_endian,
+      "byte-wise pointer updates are unsupported");
   }
 
   return conversion_failed(expr);
@@ -723,11 +719,13 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
   std::size_t a=pointer_logic.add_object(expr);
 
   const std::size_t max_objects=std::size_t(1)<<object_bits;
+
   if(a==max_objects)
-    throw
-      "too many addressed objects: maximum number of objects is set to 2^n="+
-      std::to_string(max_objects)+" (with n="+std::to_string(object_bits)+"); "+
-      "use the `--object-bits n` option to increase the maximum number";
+    throw analysis_exceptiont(
+      "too many addressed objects: maximum number of objects is set to 2^n=" +
+      std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
+      "); " +
+      "use the `--object-bits n` option to increase the maximum number");
 
   encode(a, bv);
 }