Merge pull request #5897 from tautschnig/overflow-exprt

Add {binary,unary_overflow_exprt}

Author: tautschnig

scripts/expected_doxygen_warnings.txt

@@ -93,7 +93,7 @@ warning: Included by graph for 'irep.h' not generated, too many nodes (62), thre
 warning: Included by graph for 'message.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'namespace.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'prefix.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_expr.h' not generated, too many nodes (243), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/analyses/goto_check.cpp

@@ -872,29 +872,40 @@ void goto_checkt::integer_overflow_check(
         tmp.operands().resize(i);
       }
 
-      overflow.operands().resize(2);
-      overflow.op0()=tmp;
-      overflow.op1()=expr.operands()[i];
-
       std::string kind=
         type.id()==ID_unsignedbv?"unsigned":"signed";
 
       add_guarded_property(
-        not_exprt(overflow),
+        not_exprt{binary_overflow_exprt{tmp, expr.id(), expr.operands()[i]}},
         "arithmetic overflow on " + kind + " " + expr.id_string(),
         "overflow",
         expr.find_source_location(),
         expr,
         guard);
     }
   }
+  else if(expr.operands().size() == 2)
+  {
+    std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
+
+    const binary_exprt &bexpr = to_binary_expr(expr);
+    add_guarded_property(
+      not_exprt{binary_overflow_exprt{bexpr.lhs(), expr.id(), bexpr.rhs()}},
+      "arithmetic overflow on " + kind + " " + expr.id_string(),
+      "overflow",
+      expr.find_source_location(),
+      expr,
+      guard);
+  }
   else
   {
+    PRECONDITION(expr.id() == ID_unary_minus);
+
     std::string kind=
       type.id()==ID_unsignedbv?"unsigned":"signed";
 
     add_guarded_property(
-      not_exprt(overflow),
+      not_exprt{unary_overflow_exprt{expr.id(), to_unary_expr(expr).op()}},
       "arithmetic overflow on " + kind + " " + expr.id_string(),
       "overflow",
       expr.find_source_location(),

src/ansi-c/c_typecheck_expr.cpp

@@ -2925,8 +2925,7 @@ exprt c_typecheck_baset::do_special_functions(
     identifier == CPROVER_PREFIX "overflow_minus" ||
     identifier == CPROVER_PREFIX "overflow_mult" ||
     identifier == CPROVER_PREFIX "overflow_plus" ||
-    identifier == CPROVER_PREFIX "overflow_shl" ||
-    identifier == CPROVER_PREFIX "overflow_unary_minus")
+    identifier == CPROVER_PREFIX "overflow_shl")
   {
     exprt overflow{identifier, typet{}, exprt::operandst{expr.arguments()}};
     overflow.add_source_location() = f_op.source_location();
@@ -2951,15 +2950,22 @@ exprt c_typecheck_baset::do_special_functions(
       overflow.id(ID_shl);
       typecheck_expr_shifts(to_shift_expr(overflow));
     }
-    else if(identifier == CPROVER_PREFIX "overflow_unary_minus")
-    {
-      overflow.id(ID_unary_minus);
-      typecheck_expr_unary_arithmetic(overflow);
-    }
 
-    overflow.id("overflow-" + overflow.id_string());
-    overflow.type() = bool_typet{};
-    return overflow;
+    binary_overflow_exprt of{
+      overflow.operands()[0], overflow.id(), overflow.operands()[1]};
+    of.add_source_location() = overflow.source_location();
+    return std::move(of);
+  }
+  else if(identifier == CPROVER_PREFIX "overflow_unary_minus")
+  {
+    exprt tmp{ID_unary_minus, typet{}, exprt::operandst{expr.arguments()}};
+    tmp.add_source_location() = f_op.source_location();
+
+    typecheck_expr_unary_arithmetic(tmp);
+
+    unary_overflow_exprt overflow{ID_unary_minus, tmp.operands().front()};
+    overflow.add_source_location() = tmp.source_location();
+    return std::move(overflow);
   }
   else if(identifier == CPROVER_PREFIX "enum_is_in_range")
   {

src/goto-instrument/accelerate/overflow_instrumenter.cpp

@@ -13,10 +13,11 @@ Author: Matt Lewis
 
 #include <iostream>
 
-#include <util/std_expr.h>
-#include <util/std_code.h>
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/simplify_expr.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
 
 #include <goto-programs/goto_program.h>
 
@@ -211,38 +212,25 @@ void overflow_instrumentert::overflow_expr(
           expr.id()==ID_mult)
   {
     // A generic arithmetic operation.
-    multi_ary_exprt overflow(
-      "overflow-" + expr.id_string(), expr.operands(), bool_typet());
-
-    if(expr.operands().size()>=3)
+    // The overflow checks are binary.
+    for(std::size_t i = 1; i < expr.operands().size(); i++)
     {
-      // The overflow checks are binary.
-      for(std::size_t i=1; i<expr.operands().size(); i++)
-      {
-        exprt tmp;
+      exprt tmp;
 
-        if(i==1)
-        {
-          tmp = to_multi_ary_expr(expr).op0();
-        }
-        else
-        {
-          tmp=expr;
-          tmp.operands().resize(i);
-        }
+      if(i == 1)
+      {
+        tmp = to_multi_ary_expr(expr).op0();
+      }
+      else
+      {
+        tmp = expr;
+        tmp.operands().resize(i);
+      }
 
-        overflow.operands().resize(2);
-        overflow.op0()=tmp;
-        overflow.op1()=expr.operands()[i];
+      binary_overflow_exprt overflow{tmp, expr.id(), expr.operands()[i]};
 
-        fix_types(to_binary_expr(overflow));
+      fix_types(overflow);
 
-        cases.insert(overflow);
-      }
-    }
-    else
-    {
-      fix_types(to_binary_expr(overflow));
       cases.insert(overflow);
     }
   }

src/solvers/flattening/boolbv.cpp

@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/floatbv_expr.h>
 #include <util/magic.h>
 #include <util/mp_arith.h>
-#include <util/prefix.h>
 #include <util/replace_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
@@ -413,8 +412,13 @@ literalt boolbvt::convert_rest(const exprt &expr)
     return convert_reduction(to_unary_expr(expr));
   else if(expr.id()==ID_onehot || expr.id()==ID_onehot0)
     return convert_onehot(to_unary_expr(expr));
-  else if(has_prefix(expr.id_string(), "overflow-"))
+  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)
+  {
     return convert_overflow(expr);
+  }
   else if(expr.id()==ID_isnan)
   {
     const auto &op = to_unary_expr(expr).op();

src/util/bitvector_expr.h

@@ -677,4 +677,145 @@ inline popcount_exprt &to_popcount_expr(exprt &expr)
   return ret;
 }
 
+/// \brief A Boolean expression returning true, iff operation \c kind would
+/// result in an overflow when applied to operands \c lhs and \c rhs.
+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))
+  {
+  }
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    binary_exprt::check(expr, vm);
+
+    if(expr.id() != ID_overflow_shl)
+    {
+      const binary_exprt &binary_expr = to_binary_expr(expr);
+      DATA_CHECK(
+        vm,
+        binary_expr.lhs().type() == binary_expr.rhs().type(),
+        "operand types must match");
+    }
+  }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    check(expr, vm);
+  }
+};
+
+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;
+}
+
+inline void validate_expr(const binary_overflow_exprt &value)
+{
+  validate_operands(
+    value, 2, "binary overflow expression must have two operands");
+}
+
+/// \brief Cast an exprt to a \ref binary_overflow_exprt
+///
+/// \a expr must be known to be \ref binary_overflow_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref binary_overflow_exprt
+inline const binary_overflow_exprt &to_binary_overflow_expr(const exprt &expr)
+{
+  PRECONDITION(
+    expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
+    expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
+  const binary_overflow_exprt &ret =
+    static_cast<const binary_overflow_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_binary_overflow_expr(const exprt &)
+inline binary_overflow_exprt &to_binary_overflow_expr(exprt &expr)
+{
+  PRECONDITION(
+    expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
+    expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
+  binary_overflow_exprt &ret = static_cast<binary_overflow_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \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
+{
+public:
+  unary_overflow_exprt(const irep_idt &kind, exprt _op)
+    : unary_predicate_exprt("overflow-" + id2string(kind), 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_overflow_exprt>(const exprt &base)
+{
+  return base.id() == ID_overflow_unary_minus;
+}
+
+inline void validate_expr(const unary_overflow_exprt &value)
+{
+  validate_operands(
+    value, 1, "unary 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.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref unary_overflow_exprt
+inline const unary_overflow_exprt &to_unary_overflow_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_overflow_unary_minus);
+  const unary_overflow_exprt &ret =
+    static_cast<const unary_overflow_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_unary_overflow_expr(const exprt &)
+inline unary_overflow_exprt &to_unary_overflow_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_overflow_unary_minus);
+  unary_overflow_exprt &ret = static_cast<unary_overflow_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_UTIL_BITVECTOR_EXPR_H

src/util/simplify_expr.cpp

@@ -2048,7 +2048,7 @@ simplify_exprt::simplify_complex(const unary_exprt &expr)
 }
 
 simplify_exprt::resultt<>
-simplify_exprt::simplify_overflow_binary(const binary_exprt &expr)
+simplify_exprt::simplify_overflow_binary(const binary_overflow_exprt &expr)
 {
   // zero is a neutral element for all operations supported here
   if(
@@ -2111,7 +2111,7 @@ simplify_exprt::simplify_overflow_binary(const binary_exprt &expr)
 }
 
 simplify_exprt::resultt<>
-simplify_exprt::simplify_overflow_unary(const unary_exprt &expr)
+simplify_exprt::simplify_overflow_unary(const unary_overflow_exprt &expr)
 {
   // zero is a neutral element for all operations supported here
   if(expr.op().is_zero())
@@ -2405,11 +2405,11 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
     expr.id() == ID_overflow_plus || expr.id() == ID_overflow_minus ||
     expr.id() == ID_overflow_mult || expr.id() == ID_overflow_shl)
   {
-    r = simplify_overflow_binary(to_binary_expr(expr));
+    r = simplify_overflow_binary(to_binary_overflow_expr(expr));
   }
   else if(expr.id() == ID_overflow_unary_minus)
   {
-    r = simplify_overflow_unary(to_unary_expr(expr));
+    r = simplify_overflow_unary(to_unary_overflow_expr(expr));
   }
 
   if(!no_change_join_operands)

src/util/simplify_expr_class.h

@@ -30,6 +30,7 @@ class abs_exprt;
 class address_of_exprt;
 class array_exprt;
 class binary_exprt;
+class binary_overflow_exprt;
 class binary_relation_exprt;
 class bitnot_exprt;
 class bswap_exprt;
@@ -62,6 +63,7 @@ class sign_exprt;
 class typecast_exprt;
 class unary_exprt;
 class unary_minus_exprt;
+class unary_overflow_exprt;
 class unary_plus_exprt;
 class update_exprt;
 class with_exprt;
@@ -188,12 +190,12 @@ class simplify_exprt
   /// Try to simplify overflow-+, overflow-*, overflow--, overflow-shl.
   /// Simplification will be possible when the operands are constants or the
   /// types of the operands have infinite domains.
-  NODISCARD resultt<> simplify_overflow_binary(const binary_exprt &);
+  NODISCARD resultt<> simplify_overflow_binary(const binary_overflow_exprt &);
 
   /// Try to simplify overflow-unary-.
   /// Simplification will be possible when the operand is constants or the
   /// type of the operand has an infinite domain.
-  NODISCARD resultt<> simplify_overflow_unary(const unary_exprt &);
+  NODISCARD resultt<> simplify_overflow_unary(const unary_overflow_exprt &);
 
   /// Attempt to simplify mathematical function applications if we have
   /// enough information to do so. Currently focused on constant comparisons.