Error handling cleanup in solvers/flattening

Files boolbv_quantifier.cpp to boolbv_typecast.cpp

Author: danpoe

src/solvers/flattening/boolbv_quantifier.cpp

@@ -8,9 +8,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <cassert>
-
 #include <util/arith_tools.h>
+#include <util/invariant.h>
 #include <util/replace_expr.h>
 #include <util/simplify_expr.h>
 
@@ -32,8 +31,8 @@ exprt get_quantifier_var_min(
   const exprt &var_expr,
   const exprt &quantifier_expr)
 {
-  assert(quantifier_expr.id()==ID_or ||
-         quantifier_expr.id()==ID_and);
+  PRECONDITION(quantifier_expr.id() == ID_or || quantifier_expr.id() == ID_and);
+
   exprt res;
   res.make_false();
   if(quantifier_expr.id()==ID_or)
@@ -80,8 +79,7 @@ exprt get_quantifier_var_max(
   const exprt &var_expr,
   const exprt &quantifier_expr)
 {
-  assert(quantifier_expr.id()==ID_or ||
-         quantifier_expr.id()==ID_and);
+  PRECONDITION(quantifier_expr.id() == ID_or || quantifier_expr.id() == ID_and);
   exprt res;
   res.make_false();
   if(quantifier_expr.id()==ID_or)
@@ -140,11 +138,14 @@ exprt get_quantifier_var_max(
 bool instantiate_quantifier(exprt &expr,
                             const namespacet &ns)
 {
-  if(!(expr.id()==ID_forall || expr.id()==ID_exists))
-    return true;
+  PRECONDITION(expr.id() == ID_forall || expr.id() == ID_exists);
 
-  assert(expr.operands().size()==2);
-  assert(expr.op0().id()==ID_symbol);
+  DATA_INVARIANT(
+    expr.operands().size() == 2,
+    "quantifier expressions shall have two operands");
+
+  DATA_INVARIANT(
+    expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
 
   exprt var_expr=expr.op0();
 
@@ -203,6 +204,8 @@ bool instantiate_quantifier(exprt &expr,
 
 literalt boolbvt::convert_quantifier(const exprt &src)
 {
+  PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
+
   exprt expr(src);
   if(!instantiate_quantifier(expr, ns))
     return SUB::convert_rest(src);

src/solvers/flattening/boolbv_reduction.cpp

@@ -13,8 +13,9 @@ literalt boolbvt::convert_reduction(const unary_exprt &expr)
 {
   const bvt &op_bv=convert_bv(expr.op());
 
-  if(op_bv.empty())
-    throw "reduction operators take one non-empty operand";
+  INVARIANT(
+    !op_bv.empty(),
+    "reduction operand bitvector shall have width at least one");
 
   enum { O_OR, O_AND, O_XOR } op;
 
@@ -27,7 +28,7 @@ literalt boolbvt::convert_reduction(const unary_exprt &expr)
   else if(id==ID_reduction_xor || id==ID_reduction_xnor)
     op=O_XOR;
   else
-    throw "unexpected reduction operator";
+    UNREACHABLE;
 
   literalt l=op_bv[0];
 
@@ -53,8 +54,9 @@ bvt boolbvt::convert_bv_reduction(const unary_exprt &expr)
 {
   const bvt &op_bv=convert_bv(expr.op());
 
-  if(op_bv.empty())
-    throw "reduction operators take one non-empty operand";
+  INVARIANT(
+    !op_bv.empty(),
+    "reduction operand bitvector shall have width at least one");
 
   enum { O_OR, O_AND, O_XOR } op;
 
@@ -67,7 +69,7 @@ bvt boolbvt::convert_bv_reduction(const unary_exprt &expr)
   else if(id==ID_reduction_xor || id==ID_reduction_xnor)
     op=O_XOR;
   else
-    throw "unexpected reduction operator";
+    UNREACHABLE;
 
   const typet &op_type=expr.op().type();
 

src/solvers/flattening/boolbv_replication.cpp

@@ -17,30 +17,29 @@ bvt boolbvt::convert_replication(const replication_exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
-  mp_integer times;
-  if(to_integer(expr.op0(), times))
-    throw "replication takes constant as first parameter";
+  mp_integer times = numeric_cast_v<mp_integer>(expr.times());
 
   bvt bv;
   bv.resize(width);
 
   const std::size_t u_times=integer2unsigned(times);
-  const bvt &op=convert_bv(expr.op1());
-  std::size_t offset=0;
+  const bvt &op = convert_bv(expr.op());
 
-  for(std::size_t i=0; i<u_times; i++)
-  {
-    if(op.size()+offset>width)
-      throw "replication operand width too big";
+  INVARIANT(
+    op.size() * u_times == bv.size(),
+    "result bitvector width shall be equal to the operand bitvector width times"
+    "the number of replications");
 
-    for(std::size_t i=0; i<op.size(); i++)
-      bv[i+offset]=op[i];
+  std::size_t bit_idx = 0;
 
-    offset+=op.size();
+  for(std::size_t i = 0; i < u_times; i++)
+  {
+    for(const auto &bit : op)
+    {
+      bv[bit_idx] = bit;
+      bit_idx++;
+    }
   }
 
-  if(offset!=bv.size())
-    throw "replication operand width too small";
-
   return bv;
 }

src/solvers/flattening/boolbv_shift.cpp

@@ -30,10 +30,7 @@ bvt boolbvt::convert_shift(const binary_exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
-  const bvt &op=convert_bv(expr.op0());
-
-  if(op.size()!=width)
-    throw "convert_shift: unexpected operand 0 width";
+  const bvt &op = convert_bv(expr.op0(), width);
 
   bv_utilst::shiftt shift;
 
@@ -48,15 +45,13 @@ bvt boolbvt::convert_shift(const binary_exprt &expr)
   else if(expr.id()==ID_ror)
     shift=bv_utilst::shiftt::ROTATE_RIGHT;
   else
-    throw "unexpected shift operator";
+    UNREACHABLE;
 
   // we allow a constant as shift distance
 
   if(expr.op1().is_constant())
   {
-    mp_integer i;
-    if(to_integer(expr.op1(), i))
-      throw "convert_shift: failed to convert constant";
+    mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
 
     std::size_t distance;
 

src/solvers/flattening/boolbv_struct.cpp

@@ -19,53 +19,52 @@ bvt boolbvt::convert_struct(const struct_exprt &expr)
 
   const struct_typet::componentst &components=struct_type.components();
 
-  if(expr.operands().size()!=components.size())
-  {
-    error().source_location=expr.find_source_location();
-    error() << "struct: wrong number of arguments" << eom;
-    throw 0;
-  }
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    expr.operands().size() == components.size(),
+    "number of operands of a struct expression shall equal the number of"
+    "components as indicated by its type",
+    expr.find_source_location());
 
   bvt bv;
   bv.resize(width);
 
-  std::size_t offset=0;
+  std::size_t bit_idx = 0;
 
   exprt::operandst::const_iterator op_it=expr.operands().begin();
   for(const auto &comp : components)
   {
     const typet &subtype=comp.type();
     const exprt &op=*op_it;
 
-    if(!base_type_eq(subtype, op.type(), ns))
-    {
-      error().source_location=expr.find_source_location();
-      error() << "struct: component type does not match: "
-              << subtype.pretty() << " vs. "
-              << op.type().pretty() << eom;
-      throw 0;
-    }
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      base_type_eq(subtype, op.type(), ns),
+      "type of a struct expression operand shall equal the type of the "
+      "corresponding struct component",
+      expr.find_source_location(),
+      subtype.pretty(),
+      op.type().pretty());
 
     std::size_t subtype_width=boolbv_width(subtype);
 
     if(subtype_width!=0)
     {
-      const bvt &op_bv=convert_bv(op);
-
-      assert(offset<width);
-      assert(op_bv.size()==subtype_width);
-      assert(offset+op_bv.size()<=width);
+      const bvt &op_bv = convert_bv(op, subtype_width);
 
-      for(std::size_t j=0; j<op_bv.size(); j++)
-        bv[offset+j]=op_bv[j];
+      INVARIANT(
+        bit_idx + op_bv.size() <= width, "bit index shall be within bounds");
 
-      offset+=op_bv.size();
+      for(const auto &bit : op_bv)
+      {
+        bv[bit_idx] = bit;
+        bit_idx++;
+      }
     }
 
     ++op_it;
   }
 
-  assert(offset==width);
+  INVARIANT(
+    bit_idx == width, "all bits in the bitvector shall have been assigned");
 
   return bv;
 }

src/solvers/flattening/boolbv_typecast.cpp

@@ -93,7 +93,10 @@ bool boolbvt::type_conversion(
         upper,
         ns.follow(dest_type.subtype()),
         upper_res);
-      assert(lower_res.size()+upper_res.size()==dest_width);
+      INVARIANT(
+        lower_res.size() + upper_res.size() == dest_width,
+        "lower result bitvector size plus upper result bitvector size shall "
+        "equal the destination bitvector size");
       dest=lower_res;
       dest.insert(dest.end(), upper_res.begin(), upper_res.end());
       return false;
@@ -102,7 +105,10 @@ bool boolbvt::type_conversion(
 
   if(src_type.id()==ID_complex)
   {
-    assert(dest_type.id()!=ID_complex);
+    INVARIANT(
+      dest_type.id() == ID_complex,
+      "destination type shall be of complex type when source type is of "
+      "complex type");
     if(dest_type.id()==ID_signedbv ||
        dest_type.id()==ID_unsignedbv ||
        dest_type.id()==ID_floatbv ||
@@ -187,7 +193,9 @@ bool boolbvt::type_conversion(
         return false;
 
       case bvtypet::IS_BV:
-        assert(src_width==dest_width);
+        INVARIANT(
+          src_width == dest_width,
+          "source bitvector size shall equal the destination bitvector size");
         dest=src;
         return false;
 
@@ -202,7 +210,8 @@ bool boolbvt::type_conversion(
 
           dest=convert_bv(f.to_expr());
 
-          assert(src_width==1);
+          INVARIANT(
+            src_width == 1, "bitvector of type boolean shall have width one");
 
           Forall_literals(it, dest)
             *it=prop.land(*it, src[0]);
@@ -245,7 +254,7 @@ bool boolbvt::type_conversion(
       {
         // position in bv
         std::size_t p=dest_fraction_bits+i;
-        assert(p<dest_width);
+        INVARIANT(p < dest_width, "bit index shall be within bounds");
 
         if(i<op_int_bits)
           dest[p]=src[i+op_fraction_bits];
@@ -257,7 +266,9 @@ bool boolbvt::type_conversion(
     }
     else if(src_bvtype==bvtypet::IS_BV)
     {
-      assert(src_width==dest_width);
+      INVARIANT(
+        src_width == dest_width,
+        "source bitvector with shall equal the destination bitvector width");
       dest=src;
       return false;
     }
@@ -299,7 +310,8 @@ bool boolbvt::type_conversion(
       std::size_t fraction_bits=
         to_fixedbv_type(dest_type).get_fraction_bits();
 
-      assert(src_width==1);
+      INVARIANT(
+        src_width == 1, "bitvector of type boolean shall have width one");
 
       for(std::size_t i=0; i<dest_width; i++)
       {
@@ -416,7 +428,8 @@ bool boolbvt::type_conversion(
       {
         // bool to integer
 
-        assert(src_width==1);
+        INVARIANT(
+          src_width == 1, "bitvector of type boolean shall have width one");
 
         for(std::size_t i=0; i<dest_width; i++)
         {
@@ -483,7 +496,9 @@ bool boolbvt::type_conversion(
     break;
 
   case bvtypet::IS_BV:
-    assert(src_width==dest_width);
+    INVARIANT(
+      src_width == dest_width,
+      "source bitvector width shall equal the destination bitvector width");
     dest=src;
     return false;
 
@@ -590,20 +605,18 @@ bool boolbvt::type_conversion(
 /// conversion from bitvector types to boolean
 literalt boolbvt::convert_typecast(const typecast_exprt &expr)
 {
-  assert(expr.operands().size()==1);
-
-  if(expr.op0().type().id()==ID_range)
+  if(expr.op().type().id() == ID_range)
   {
-    mp_integer from=string2integer(expr.op0().type().get_string(ID_from));
-    mp_integer to=string2integer(expr.op0().type().get_string(ID_to));
+    mp_integer from = string2integer(expr.op().type().get_string(ID_from));
+    mp_integer to = string2integer(expr.op().type().get_string(ID_to));
 
     if(from==1 && to==1)
       return const_literal(true);
     else if(from==0 && to==0)
       return const_literal(false);
   }
 
-  const bvt &bv=convert_bv(expr.op0());
+  const bvt &bv = convert_bv(expr.op());
 
   if(!bv.empty())
     return prop.lor(bv);

src/util/std_expr.h

@@ -4585,6 +4585,9 @@ inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
 {
   DATA_INVARIANT(expr.operands().size()==2,
                  "quantifier expressions must have two operands");
+  DATA_INVARIANT(
+    expr.op0().id() == ID_symbol,
+    "quantified variable shall be a symbol");
   return static_cast<const quantifier_exprt &>(expr);
 }
 
@@ -4593,6 +4596,9 @@ inline quantifier_exprt &to_quantifier_expr(exprt &expr)
 {
   DATA_INVARIANT(expr.operands().size()==2,
                  "quantifier expressions must have two operands");
+  DATA_INVARIANT(
+    expr.op0().id() == ID_symbol,
+    "quantified variable shall be a symbol");
   return static_cast<quantifier_exprt &>(expr);
 }