Merge pull request #6752 from thomasspriggs/tas/refactor_convert_overflow

Refactor `boolbvt::convert_overflow`

Author: thomasspriggs

src/solvers/flattening/boolbv.cpp

@@ -417,10 +417,16 @@ literalt boolbvt::convert_rest(const exprt &expr)
   else if(expr.id()==ID_onehot || expr.id()==ID_onehot0)
     return convert_onehot(to_unary_expr(expr));
   else if(
-    can_cast_expr<binary_overflow_exprt>(expr) ||
-    can_cast_expr<unary_minus_overflow_exprt>(expr))
+    const auto binary_overflow =
+      expr_try_dynamic_cast<binary_overflow_exprt>(expr))
   {
-    return convert_overflow(expr);
+    return convert_binary_overflow(*binary_overflow);
+  }
+  else if(
+    const auto unary_overflow =
+      expr_try_dynamic_cast<unary_overflow_exprt>(expr))
+  {
+    return convert_unary_overflow(*unary_overflow);
   }
   else if(expr.id()==ID_isnan)
   {

src/solvers/flattening/boolbv.h

@@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "arrays.h"
 
 class array_comprehension_exprt;
+class binary_overflow_exprt;
 class bitreverse_exprt;
 class bswap_exprt;
 class byte_extract_exprt;
@@ -38,6 +39,7 @@ class floatbv_typecast_exprt;
 class ieee_float_op_exprt;
 class member_exprt;
 class replication_exprt;
+class unary_overflow_exprt;
 class union_typet;
 
 class boolbvt:public arrayst
@@ -140,7 +142,8 @@ class boolbvt:public arrayst
   virtual literalt convert_reduction(const unary_exprt &expr);
   virtual literalt convert_onehot(const unary_exprt &expr);
   virtual literalt convert_extractbit(const extractbit_exprt &expr);
-  virtual literalt convert_overflow(const exprt &expr);
+  virtual literalt convert_binary_overflow(const binary_overflow_exprt &expr);
+  virtual literalt convert_unary_overflow(const unary_overflow_exprt &expr);
   virtual literalt convert_equality(const equal_exprt &expr);
   virtual literalt convert_verilog_case_equality(
     const binary_relation_exprt &expr);

src/solvers/flattening/boolbv_overflow.cpp

@@ -7,55 +7,49 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 #include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
 #include <util/invariant.h>
 
 #include "boolbv.h"
 
-literalt boolbvt::convert_overflow(const exprt &expr)
+literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr)
 {
-  const auto plus_or_minus_conversion =
-    [&](
-      const binary_overflow_exprt &overflow_expr,
-      const std::function<literalt(
-        bv_utilst *, const bvt &, const bvt &, bv_utilst::representationt)>
-        &bv_util_overflow) {
-      const bvt &bv0 = convert_bv(overflow_expr.lhs());
-      const bvt &bv1 = convert_bv(overflow_expr.rhs());
-
-      if(bv0.size() != bv1.size())
-        return SUB::convert_rest(expr);
-
-      bv_utilst::representationt rep =
-        overflow_expr.lhs().type().id() == ID_signedbv
-          ? bv_utilst::representationt::SIGNED
-          : bv_utilst::representationt::UNSIGNED;
-
-      return bv_util_overflow(&bv_utils, bv0, bv1, rep);
-    };
+  const bvt &bv0 = convert_bv(expr.lhs());
+  const bvt &bv1 = convert_bv(
+    expr.rhs(),
+    can_cast_expr<mult_overflow_exprt>(expr)
+      ? optionalt<std::size_t>{bv0.size()}
+      : nullopt);
+
+  const bv_utilst::representationt rep =
+    can_cast_type<signedbv_typet>(expr.lhs().type())
+      ? bv_utilst::representationt::SIGNED
+      : bv_utilst::representationt::UNSIGNED;
+
   if(
     const auto plus_overflow = expr_try_dynamic_cast<plus_overflow_exprt>(expr))
   {
-    return plus_or_minus_conversion(*plus_overflow, &bv_utilst::overflow_add);
+    if(bv0.size() != bv1.size())
+      return SUB::convert_rest(expr);
+
+    return bv_utils.overflow_add(bv0, bv1, rep);
   }
   if(const auto minus = expr_try_dynamic_cast<minus_overflow_exprt>(expr))
   {
-    return plus_or_minus_conversion(*minus, &bv_utilst::overflow_sub);
+    if(bv0.size() != bv1.size())
+      return SUB::convert_rest(expr);
+
+    return bv_utils.overflow_sub(bv0, bv1, rep);
   }
   else if(
     const auto mult_overflow = expr_try_dynamic_cast<mult_overflow_exprt>(expr))
   {
     if(
-      mult_overflow->lhs().type().id() != ID_unsignedbv &&
-      mult_overflow->lhs().type().id() != ID_signedbv)
+      !can_cast_type<unsignedbv_typet>(expr.lhs().type()) &&
+      !can_cast_type<signedbv_typet>(expr.lhs().type()))
+    {
       return SUB::convert_rest(expr);
-
-    bvt bv0 = convert_bv(mult_overflow->lhs());
-    bvt bv1 = convert_bv(mult_overflow->rhs(), bv0.size());
-
-    bv_utilst::representationt rep =
-      mult_overflow->lhs().type().id() == ID_signedbv
-        ? bv_utilst::representationt::SIGNED
-        : bv_utilst::representationt::UNSIGNED;
+    }
 
     DATA_INVARIANT(
       mult_overflow->lhs().type() == mult_overflow->rhs().type(),
@@ -65,10 +59,10 @@ literalt boolbvt::convert_overflow(const exprt &expr)
     std::size_t new_size=old_size*2;
 
     // sign/zero extension
-    bv0=bv_utils.extension(bv0, new_size, rep);
-    bv1=bv_utils.extension(bv1, new_size, rep);
+    const bvt &bv0_extended = bv_utils.extension(bv0, new_size, rep);
+    const bvt &bv1_extended = bv_utils.extension(bv1, new_size, rep);
 
-    bvt result=bv_utils.multiplier(bv0, bv1, rep);
+    bvt result = bv_utils.multiplier(bv0_extended, bv1_extended, rep);
 
     if(rep==bv_utilst::representationt::UNSIGNED)
     {
@@ -100,23 +94,15 @@ literalt boolbvt::convert_overflow(const exprt &expr)
   else if(
     const auto shl_overflow = expr_try_dynamic_cast<shl_overflow_exprt>(expr))
   {
-    const bvt &bv0 = convert_bv(shl_overflow->lhs());
-    const bvt &bv1 = convert_bv(shl_overflow->rhs());
-
     std::size_t old_size = bv0.size();
     std::size_t new_size = old_size * 2;
 
-    bv_utilst::representationt rep =
-      shl_overflow->lhs().type().id() == ID_signedbv
-        ? bv_utilst::representationt::SIGNED
-        : bv_utilst::representationt::UNSIGNED;
-
     bvt bv_ext=bv_utils.extension(bv0, new_size, rep);
 
     bvt result=bv_utils.shift(bv_ext, bv_utilst::shiftt::SHIFT_LEFT, bv1);
 
     // a negative shift is undefined; yet this isn't an overflow
-    literalt neg_shift = shl_overflow->lhs().type().id() == ID_unsignedbv
+    literalt neg_shift = rep == bv_utilst::representationt::UNSIGNED
                            ? const_literal(false)
                            : bv1.back(); // sign bit
 
@@ -161,7 +147,13 @@ literalt boolbvt::convert_overflow(const exprt &expr)
     return
       prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), overflow));
   }
-  else if(
+
+  return SUB::convert_rest(expr);
+}
+
+literalt boolbvt::convert_unary_overflow(const unary_overflow_exprt &expr)
+{
+  if(
     const auto unary_minus_overflow =
       expr_try_dynamic_cast<unary_minus_overflow_exprt>(expr))
   {