Add separate overflow expr classes

src/ansi-c/c_typecheck_expr.cpp

@@ -3161,7 +3161,7 @@ exprt c_typecheck_baset::do_special_functions(
 
     typecheck_expr_unary_arithmetic(tmp);
 
-    unary_overflow_exprt overflow{ID_unary_minus, tmp.operands().front()};
+    unary_minus_overflow_exprt overflow{tmp.operands().front()};
     overflow.add_source_location() = tmp.source_location();
     return std::move(overflow);
   }

src/ansi-c/expr2c.cpp

@@ -3921,9 +3921,8 @@ std::string expr2ct::convert_with_precedence(
     return convert_cond(src, precedence);
 
   else if(
-    src.id() == ID_overflow_unary_minus || src.id() == ID_overflow_minus ||
-    src.id() == ID_overflow_mult || src.id() == ID_overflow_plus ||
-    src.id() == ID_overflow_shl)
+    can_cast_expr<unary_minus_overflow_exprt>(src) ||
+    can_cast_expr<binary_overflow_exprt>(src))
   {
     return convert_overflow(src, precedence);
   }

src/ansi-c/goto_check_c.cpp

@@ -1052,7 +1052,7 @@ void goto_check_ct::integer_overflow_check(
     std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
 
     add_guarded_property(
-      not_exprt{unary_overflow_exprt{expr.id(), to_unary_expr(expr).op()}},
+      not_exprt{unary_minus_overflow_exprt{to_unary_expr(expr).op()}},
       "arithmetic overflow on " + kind + " " + expr.id_string(),
       "overflow",
       expr.find_source_location(),

src/solvers/flattening/boolbv.cpp

@@ -417,9 +417,8 @@ 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(
-    expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
-    expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl ||
-    expr.id() == ID_overflow_unary_minus)
+    can_cast_expr<binary_overflow_exprt>(expr) ||
+    can_cast_expr<unary_minus_overflow_exprt>(expr))
   {
     return convert_overflow(expr);
   }

src/solvers/flattening/boolbv_overflow.cpp

@@ -6,51 +6,59 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include "boolbv.h"
-
+#include <util/bitvector_expr.h>
 #include <util/invariant.h>
 
+#include "boolbv.h"
+
 literalt boolbvt::convert_overflow(const exprt &expr)
 {
-  if(expr.id()==ID_overflow_plus ||
-     expr.id()==ID_overflow_minus)
+  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);
+    };
+  if(
+    const auto plus_overflow = expr_try_dynamic_cast<plus_overflow_exprt>(expr))
   {
-    const auto &overflow_expr = to_binary_expr(expr);
-
-    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 expr.id()==ID_overflow_minus?
-      bv_utils.overflow_sub(bv0, bv1, rep):
-      bv_utils.overflow_add(bv0, bv1, rep);
+    return plus_or_minus_conversion(*plus_overflow, &bv_utilst::overflow_add);
   }
-  else if(expr.id()==ID_overflow_mult)
+  if(const auto minus = expr_try_dynamic_cast<minus_overflow_exprt>(expr))
+  {
+    return plus_or_minus_conversion(*minus, &bv_utilst::overflow_sub);
+  }
+  else if(
+    const auto mult_overflow = expr_try_dynamic_cast<mult_overflow_exprt>(expr))
   {
-    const auto &overflow_expr = to_binary_expr(expr);
-
     if(
-      overflow_expr.lhs().type().id() != ID_unsignedbv &&
-      overflow_expr.lhs().type().id() != ID_signedbv)
+      mult_overflow->lhs().type().id() != ID_unsignedbv &&
+      mult_overflow->lhs().type().id() != ID_signedbv)
       return SUB::convert_rest(expr);
 
-    bvt bv0 = convert_bv(overflow_expr.lhs());
-    bvt bv1 = convert_bv(overflow_expr.rhs(), bv0.size());
+    bvt bv0 = convert_bv(mult_overflow->lhs());
+    bvt bv1 = convert_bv(mult_overflow->rhs(), bv0.size());
 
     bv_utilst::representationt rep =
-      overflow_expr.lhs().type().id() == ID_signedbv
+      mult_overflow->lhs().type().id() == ID_signedbv
         ? bv_utilst::representationt::SIGNED
         : bv_utilst::representationt::UNSIGNED;
 
     DATA_INVARIANT(
-      overflow_expr.lhs().type() == overflow_expr.rhs().type(),
+      mult_overflow->lhs().type() == mult_overflow->rhs().type(),
       "operands of overflow_mult expression shall have same type");
 
     std::size_t old_size=bv0.size();
@@ -89,18 +97,17 @@ literalt boolbvt::convert_overflow(const exprt &expr)
       return !prop.lor(all_one, all_zero);
     }
   }
-  else if(expr.id() == ID_overflow_shl)
+  else if(
+    const auto shl_overflow = expr_try_dynamic_cast<shl_overflow_exprt>(expr))
   {
-    const auto &overflow_expr = to_binary_expr(expr);
-
-    const bvt &bv0 = convert_bv(overflow_expr.lhs());
-    const bvt &bv1 = convert_bv(overflow_expr.rhs());
+    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 =
-      overflow_expr.lhs().type().id() == ID_signedbv
+      shl_overflow->lhs().type().id() == ID_signedbv
         ? bv_utilst::representationt::SIGNED
         : bv_utilst::representationt::UNSIGNED;
 
@@ -109,7 +116,7 @@ literalt boolbvt::convert_overflow(const exprt &expr)
     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 = overflow_expr.lhs().type().id() == ID_unsignedbv
+    literalt neg_shift = shl_overflow->lhs().type().id() == ID_unsignedbv
                            ? const_literal(false)
                            : bv1.back(); // sign bit
 
@@ -154,11 +161,11 @@ literalt boolbvt::convert_overflow(const exprt &expr)
     return
       prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), overflow));
   }
-  else if(expr.id()==ID_overflow_unary_minus)
+  else if(
+    const auto unary_minus_overflow =
+      expr_try_dynamic_cast<unary_minus_overflow_exprt>(expr))
   {
-    const auto &overflow_expr = to_unary_expr(expr);
-
-    const bvt &bv = convert_bv(overflow_expr.op());
+    const bvt &bv = convert_bv(unary_minus_overflow->op());
 
     return bv_utils.overflow_negate(bv);
   }

src/solvers/smt2/smt2_conv.cpp

@@ -1856,8 +1856,9 @@ void smt2_convt::convert_expr(const exprt &expr)
     else
       UNREACHABLE;
   }
-  else if(expr.id()==ID_overflow_plus ||
-          expr.id()==ID_overflow_minus)
+  else if(
+    can_cast_expr<plus_overflow_exprt>(expr) ||
+    can_cast_expr<minus_overflow_exprt>(expr))
   {
     const auto &op0 = to_binary_expr(expr).op0();
     const auto &op1 = to_binary_expr(expr).op1();
@@ -1866,7 +1867,7 @@ void smt2_convt::convert_expr(const exprt &expr)
       expr.type().id() == ID_bool,
       "overflow plus and overflow minus expressions shall be of Boolean type");
 
-    bool subtract=expr.id()==ID_overflow_minus;
+    bool subtract = can_cast_expr<minus_overflow_exprt>(expr);
     const typet &op_type = op0.type();
     std::size_t width=boolbv_width(op_type);
 
@@ -1907,13 +1908,14 @@ void smt2_convt::convert_expr(const exprt &expr)
         "overflow check should not be performed on unsupported type",
         op_type.id_string());
   }
-  else if(expr.id()==ID_overflow_mult)
+  else if(
+    const auto mult_overflow = expr_try_dynamic_cast<mult_overflow_exprt>(expr))
   {
-    const auto &op0 = to_binary_expr(expr).op0();
-    const auto &op1 = to_binary_expr(expr).op1();
+    const auto &op0 = mult_overflow->op0();
+    const auto &op1 = mult_overflow->op1();
 
     DATA_INVARIANT(
-      expr.type().id() == ID_bool,
+      mult_overflow->type().id() == ID_bool,
       "overflow mult expression shall be of Boolean type");
 
     // No better idea than to multiply with double the bits and then compare

src/util/bitvector_expr.h

@@ -705,11 +705,12 @@ class binary_overflow_exprt : public binary_predicate_exprt
 {
 public:
   binary_overflow_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
-    : binary_predicate_exprt(
-        std::move(_lhs),
-        "overflow-" + id2string(kind),
-        std::move(_rhs))
+    : binary_predicate_exprt(std::move(_lhs), make_id(kind), std::move(_rhs))
   {
+    INVARIANT(
+      valid_id(id()),
+      "The kind used to construct binary_overflow_exprt should be in the set "
+      "of expected valid kinds.");
   }
 
   static void check(
@@ -735,13 +736,28 @@ class binary_overflow_exprt : public binary_predicate_exprt
   {
     check(expr, vm);
   }
+
+  /// Returns true iff \p id is a valid identifier of a `binary_overflow_exprt`.
+  static bool valid_id(const irep_idt &id)
+  {
+    return id == ID_overflow_plus || id == ID_overflow_mult ||
+           id == ID_overflow_minus || id == ID_overflow_shl;
+  }
+
+private:
+  static irep_idt make_id(const irep_idt &kind)
+  {
+    if(valid_id(kind))
+      return kind;
+    else
+      return "overflow-" + id2string(kind);
+  }
 };
 
 template <>
 inline bool can_cast_expr<binary_overflow_exprt>(const exprt &base)
 {
-  return base.id() == ID_overflow_plus || base.id() == ID_overflow_mult ||
-         base.id() == ID_overflow_minus || base.id() == ID_overflow_shl;
+  return binary_overflow_exprt::valid_id(base.id());
 }
 
 inline void validate_expr(const binary_overflow_exprt &value)
@@ -778,6 +794,66 @@ inline binary_overflow_exprt &to_binary_overflow_expr(exprt &expr)
   return ret;
 }
 
+class plus_overflow_exprt : public binary_overflow_exprt
+{
+public:
+  plus_overflow_exprt(exprt _lhs, exprt _rhs)
+    : binary_overflow_exprt(std::move(_lhs), ID_overflow_plus, std::move(_rhs))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<plus_overflow_exprt>(const exprt &base)
+{
+  return base.id() == ID_overflow_plus;
+}
+
+class minus_overflow_exprt : public binary_overflow_exprt
+{
+public:
+  minus_overflow_exprt(exprt _lhs, exprt _rhs)
+    : binary_overflow_exprt(std::move(_lhs), ID_overflow_minus, std::move(_rhs))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<minus_overflow_exprt>(const exprt &base)
+{
+  return base.id() == ID_overflow_minus;
+}
+
+class mult_overflow_exprt : public binary_overflow_exprt
+{
+public:
+  mult_overflow_exprt(exprt _lhs, exprt _rhs)
+    : binary_overflow_exprt(std::move(_lhs), ID_overflow_mult, std::move(_rhs))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<mult_overflow_exprt>(const exprt &base)
+{
+  return base.id() == ID_overflow_mult;
+}
+
+class shl_overflow_exprt : public binary_overflow_exprt
+{
+public:
+  shl_overflow_exprt(exprt _lhs, exprt _rhs)
+    : binary_overflow_exprt(std::move(_lhs), ID_overflow_shl, std::move(_rhs))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<shl_overflow_exprt>(const exprt &base)
+{
+  return base.id() == ID_overflow_shl;
+}
+
 /// \brief A Boolean expression returning true, iff operation \c kind would
 /// result in an overflow when applied to the (single) operand.
 class unary_overflow_exprt : public unary_predicate_exprt
@@ -816,6 +892,44 @@ inline void validate_expr(const unary_overflow_exprt &value)
     value, 1, "unary overflow expression must have one operand");
 }
 
+/// \brief A Boolean expression returning true, iff negation would result in an
+/// overflow when applied to the (single) operand.
+class unary_minus_overflow_exprt : public unary_overflow_exprt
+{
+public:
+  explicit unary_minus_overflow_exprt(exprt _op)
+    : unary_overflow_exprt(ID_unary_minus, std::move(_op))
+  {
+  }
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    unary_exprt::check(expr, vm);
+  }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    check(expr, vm);
+  }
+};
+
+template <>
+inline bool can_cast_expr<unary_minus_overflow_exprt>(const exprt &base)
+{
+  return base.id() == ID_overflow_unary_minus;
+}
+
+inline void validate_expr(const unary_minus_overflow_exprt &value)
+{
+  validate_operands(
+    value, 1, "unary minus overflow expression must have one operand");
+}
+
 /// \brief Cast an exprt to a \ref unary_overflow_exprt
 ///
 /// \a expr must be known to be \ref unary_overflow_exprt.