Error handling cleanup in solvers/flattening

Author: danpoe

src/solvers/flattening/boolbv_add_sub.cpp

@@ -15,6 +15,10 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_add_sub(const exprt &expr)
 {
+  PRECONDITION(
+    expr.id() == ID_plus || expr.id() == ID_minus ||
+    expr.id() == "no-overflow-plus" || expr.id() == "no-overflow-minus");
+
   const typet &type=ns.follow(expr.type());
 
   if(type.id()!=ID_unsignedbv &&
@@ -33,17 +37,20 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
   const exprt::operandst &operands=expr.operands();
 
-  if(operands.empty())
-    throw "operator "+expr.id_string()+" takes at least one operand";
+  DATA_INVARIANT(
+    !operands.empty(),
+    "operator " + expr.id_string() + " takes at least one operand");
 
   const exprt &op0=expr.op0();
   DATA_INVARIANT(
     op0.type() == type, "add/sub with mixed types:\n" + expr.pretty());
 
   bvt bv=convert_bv(op0);
 
-  if(bv.size()!=width)
-    throw "convert_add_sub: unexpected operand 0 width";
+  INVARIANT(
+    bv.size() == width,
+    "the width of the bitvector resulting from the first operand should be "
+    "equal to the width indicated by the expression type");
 
   bool subtract=(expr.id()==ID_minus ||
                  expr.id()=="no-overflow-minus");
@@ -69,17 +76,21 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
     const bvt &op=convert_bv(*it);
 
-    if(op.size()!=width)
-      throw "convert_add_sub: unexpected operand width";
+    INVARIANT(
+      op.size() == width,
+      "the width of the bitvector resulting from the expression operand should"
+      "be equal to the width indicated by the expression type");
 
     if(type.id()==ID_vector || type.id()==ID_complex)
     {
       const typet &subtype=ns.follow(type.subtype());
 
       std::size_t sub_width=boolbv_width(subtype);
 
-      if(sub_width==0 || width%sub_width!=0)
-        throw "convert_add_sub: unexpected vector operand width";
+      INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
+      INVARIANT(
+        width % sub_width == 0,
+        "total vector bit width shall be a multiple of the element bit width");
 
       std::size_t size=width/sub_width;
       bv.resize(width);
@@ -91,7 +102,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
         for(std::size_t j=0; j<tmp_op.size(); j++)
         {
-          assert(i*sub_width+j<op.size());
+          INVARIANT(
+            i * sub_width + j < op.size(), "bit index shall be within bounds");
           tmp_op[j]=op[i*sub_width+j];
         }
 
@@ -100,7 +112,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
         for(std::size_t j=0; j<tmp_result.size(); j++)
         {
-          assert(i*sub_width+j<bv.size());
+          INVARIANT(
+            i * sub_width + j < bv.size(), "bit index shall be within bounds");
           tmp_result[j]=bv[i*sub_width+j];
         }
 
@@ -113,11 +126,14 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
         else
           tmp_result=bv_utils.add_sub(tmp_result, tmp_op, subtract);
 
-        assert(tmp_result.size()==sub_width);
+        INVARIANT(
+          tmp_result.size() == sub_width,
+          "applying the add/sub operation shall not change the bitwidth");
 
         for(std::size_t j=0; j<tmp_result.size(); j++)
         {
-          assert(i*sub_width+j<bv.size());
+          INVARIANT(
+            i * sub_width + j < bv.size(), "bit index shall be within bounds");
           bv[i*sub_width+j]=tmp_result[j];
         }
       }

src/solvers/flattening/boolbv_array.cpp

@@ -6,9 +6,10 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-
 #include "boolbv.h"
 
+#include <util/invariant.h>
+
 bvt boolbvt::convert_array(const exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
@@ -18,9 +19,11 @@ bvt boolbvt::convert_array(const exprt &expr)
 
   if(expr.type().id()==ID_array)
   {
-    assert(expr.has_operands());
+    DATA_INVARIANT(
+      expr.has_operands(),
+      "the bit width being nonzero implies that the array has a nonzero size "
+      "in which case the array shall have operands");
     const exprt::operandst &operands=expr.operands();
-    assert(!operands.empty());
     std::size_t op_width=width/operands.size();
 
     bvt bv;
@@ -30,8 +33,10 @@ bvt boolbvt::convert_array(const exprt &expr)
     {
       const bvt &tmp=convert_bv(*it);
 
-      if(tmp.size()!=op_width)
-        throw "convert_array: unexpected operand width";
+      INVARIANT(
+        tmp.size() == op_width,
+        "bit width of an operand bitvector shall be equal to the total bit "
+        "width of the array divided by the number of elements");
 
       forall_literals(it2, tmp)
         bv.push_back(*it2);

src/solvers/flattening/boolbv_array_of.cpp

@@ -9,12 +9,13 @@ Author: Daniel Kroening, [email protected]
 #include "boolbv.h"
 
 #include <util/arith_tools.h>
+#include <util/invariant.h>
 #include <util/std_types.h>
 
 bvt boolbvt::convert_array_of(const array_of_exprt &expr)
 {
-  if(expr.type().id()!=ID_array)
-    throw "array_of must be array-typed";
+  DATA_INVARIANT(
+    expr.type().id() == ID_array, "array_of expression shall have array type");
 
   const array_typet &array_type=to_array_type(expr.type());
 
@@ -45,8 +46,10 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
   bvt bv;
   bv.resize(width);
 
-  if(size*tmp.size()!=width)
-    throw "convert_array_of: unexpected operand width";
+  INVARIANT(
+    size * tmp.size() == width,
+    "total array bit width shall equal the number of elements times the "
+    "element bit with");
 
   std::size_t offset=0;
 
@@ -56,7 +59,8 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
       bv[offset]=tmp[j];
   }
 
-  assert(offset==bv.size());
+  INVARIANT(
+    offset == bv.size(), "we shall have iterated over all the bit indices");
 
   return bv;
 }

src/solvers/flattening/boolbv_byte_update.cpp

@@ -9,17 +9,18 @@ Author: Daniel Kroening, [email protected]
 #include "boolbv.h"
 
 #include <iostream>
-#include <cassert>
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
+#include <util/invariant.h>
 
 #include "bv_endianness_map.h"
 
 bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 {
-  if(expr.operands().size()!=3)
-    throw "byte_update takes three operands";
+  DATA_INVARIANT(
+    expr.operands().size() == 3,
+    "byte_update expression shall have three operands");
 
   const exprt &op=expr.op0();
   const exprt &offset_expr=expr.offset();
@@ -70,8 +71,11 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
           size_t index_op=map_op.map_bit(offset_i+i);
           size_t index_value=map_value.map_bit(i);
 
-          assert(index_op<bv.size());
-          assert(index_value<value_bv.size());
+          INVARIANT(
+            index_op < bv.size(), "bit vector index shall be within bounds");
+          INVARIANT(
+            index_value < value_bv.size(),
+            "bit vector index shall be within bounds");
 
           bv[index_op]=value_bv[index_value];
         }

src/solvers/flattening/boolbv_case.cpp

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_case(const exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_case);
+
   const std::vector<exprt> &operands=expr.operands();
 
   std::size_t width=boolbv_width(expr.type());
@@ -26,11 +28,11 @@ bvt boolbvt::convert_case(const exprt &expr)
   Forall_literals(it, bv)
     *it=prop.new_variable();
 
-  if(operands.size()<3)
-    throw "case takes at least three operands";
+  DATA_INVARIANT(
+    operands.size() >= 3, "case should have at least three operands");
 
-  if((operands.size()%2)!=1)
-    throw "number of case operands must be odd";
+  DATA_INVARIANT(
+    operands.size() % 2 == 1, "number of case operands should be odd");
 
   enum { FIRST, COMPARE, VALUE } what=FIRST;
   bvt compare_bv;
@@ -81,7 +83,7 @@ bvt boolbvt::convert_case(const exprt &expr)
       break;
 
     default:
-      assert(false);
+      UNREACHABLE;
     }
   }
 

src/solvers/flattening/boolbv_complex.cpp

@@ -6,11 +6,14 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-
 #include "boolbv.h"
 
+#include <util/invariant.h>
+
 bvt boolbvt::convert_complex(const exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_complex);
+
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
@@ -31,8 +34,10 @@ bvt boolbvt::convert_complex(const exprt &expr)
       {
         const bvt &tmp=convert_bv(*it);
 
-        if(tmp.size()!=op_width)
-          throw "convert_complex: unexpected operand width";
+        INVARIANT(
+          tmp.size() == op_width,
+          "bit width of operand bitvector shall be equal to the total bit "
+          "width divided by the number of operands");
 
         forall_literals(it2, tmp)
           bv.push_back(*it2);
@@ -47,29 +52,31 @@ bvt boolbvt::convert_complex(const exprt &expr)
 
 bvt boolbvt::convert_complex_real(const complex_real_exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_complex_real);
+
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
     return conversion_failed(expr);
 
-  bvt bv = convert_bv(expr.op());
+  bvt bv = convert_bv(expr.op(), width * 2);
 
-  assert(bv.size()==width*2);
   bv.resize(width); // chop
 
   return bv;
 }
 
 bvt boolbvt::convert_complex_imag(const complex_imag_exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_complex_imag);
+
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
     return conversion_failed(expr);
 
-  bvt bv = convert_bv(expr.op());
+  bvt bv = convert_bv(expr.op(), width * 2);
 
-  assert(bv.size()==width*2);
   bv.erase(bv.begin(), bv.begin()+width);
 
   return bv;

src/solvers/flattening/boolbv_concatenation.cpp

@@ -6,20 +6,23 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-
 #include "boolbv.h"
 
+#include <util/invariant.h>
+
 bvt boolbvt::convert_concatenation(const exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_concatenation);
+
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
     return conversion_failed(expr);
 
   const exprt::operandst &operands=expr.operands();
 
-  if(operands.empty())
-    throw "concatenation takes at least one operand";
+  DATA_INVARIANT(
+    !operands.empty(), "concatentation shall have at least one operand");
 
   std::size_t offset=width;
   bvt bv;
@@ -29,17 +32,20 @@ bvt boolbvt::convert_concatenation(const exprt &expr)
   {
     const bvt &op=convert_bv(*it);
 
-    if(op.size()>offset)
-      throw "concatenation operand width too big";
+    INVARIANT(
+      op.size() <= offset,
+      "concatentation operand must fit into the result bitvector");
 
     offset-=op.size();
 
     for(std::size_t i=0; i<op.size(); i++)
       bv[offset+i]=op[i];
   }
 
-  if(offset!=0)
-    throw "concatenation operand width too small";
+  INVARIANT(
+    offset == 0,
+    "all bits in the result bitvector must have been filled up by the "
+    "concatentation operands");
 
   return bv;
 }