Refactoring in boolbvt::convert_mult

Author: romainbrenguier

src/solvers/flattening/boolbv_mult.cpp

@@ -12,53 +12,40 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_mult(const exprt &expr)
 {
-  std::size_t width=boolbv_width(expr.type());
-
+  const std::size_t width = boolbv_width(expr.type());
   if(width==0)
     return conversion_failed(expr);
-
   bvt bv;
   bv.resize(width);
 
   const exprt::operandst &operands=expr.operands();
-  if(operands.empty())
-    throw "mult without operands";
-
+  DATA_INVARIANT(!operands.empty(), "mult must have operands");
   const exprt &op0=expr.op0();
-
-  bool no_overflow=expr.id()=="no-overflow-mult";
+  const bool no_overflow = expr.id() == "no-overflow-mult";
 
   if(expr.type().id()==ID_fixedbv)
   {
-    if(op0.type()!=expr.type())
-      throw "multiplication with mixed types";
-
+    DATA_INVARIANT(op0.type() == expr.type(), "multiplication with mixed types");
     bv=convert_bv(op0);
 
-    if(bv.size()!=width)
-      throw "convert_mult: unexpected operand width";
-
-    std::size_t fraction_bits=
+    DATA_INVARIANT(bv.size() == width, "convert_mult: unexpected operand width");
+    const std::size_t fraction_bits =
       to_fixedbv_type(expr.type()).get_fraction_bits();
 
     for(exprt::operandst::const_iterator it=operands.begin()+1;
         it!=operands.end(); it++)
     {
-      if(it->type()!=expr.type())
-        throw "multiplication with mixed types";
+      DATA_INVARIANT(
+        it->type() == expr.type(),
+        "multiplication should have uniform operand types");
 
       // do a sign extension by fraction_bits bits
       bv=bv_utils.sign_extension(bv, bv.size()+fraction_bits);
-
       bvt op=convert_bv(*it);
 
-      if(op.size()!=width)
-        throw "convert_mult: unexpected operand width";
-
+      INVARIANT(op.size() == width, "convert_mult: unexpected operand width");
       op=bv_utils.sign_extension(op, bv.size());
-
       bv=bv_utils.signed_multiplier(bv, op);
-
       // cut it down again
       bv.erase(bv.begin(), bv.begin()+fraction_bits);
     }
@@ -68,37 +55,25 @@ bvt boolbvt::convert_mult(const exprt &expr)
   else if(expr.type().id()==ID_unsignedbv ||
           expr.type().id()==ID_signedbv)
   {
-    if(op0.type()!=expr.type())
-      throw "multiplication with mixed types";
-
+    DATA_INVARIANT(
+      op0.type() == expr.type(), "multiplication with mixed types");
     bv_utilst::representationt rep=
       expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
                                     bv_utilst::representationt::UNSIGNED;
 
     bv=convert_bv(op0);
-
-    if(bv.size()!=width)
-      throw "convert_mult: unexpected operand width";
-
+    INVARIANT(bv.size() == width, "convert_mult: unexpected operand width");
     for(exprt::operandst::const_iterator it=operands.begin()+1;
         it!=operands.end(); it++)
     {
-      if(it->type()!=expr.type())
-        throw "multiplication with mixed types";
-
+      INVARIANT(it->type() == expr.type(), "multiplication with mixed types");
       const bvt &op=convert_bv(*it);
+      CHECK_RETURN(op.size() == width);
 
-      if(op.size()!=width)
-        throw "convert_mult: unexpected operand width";
-
-      if(no_overflow)
-        bv=bv_utils.multiplier_no_overflow(bv, op, rep);
-      else
-        bv=bv_utils.multiplier(bv, op, rep);
+      bv = no_overflow ? bv_utils.multiplier_no_overflow(bv, op, rep)
+                       : bv_utils.multiplier(bv, op, rep);
     }
-
     return bv;
   }
-
   return conversion_failed(expr);
 }