Merge pull request #5900 from tautschnig/side-effect-overflow-expression

Add side_effect_expr_overflowt

Author: tautschnig

src/ansi-c/c_expr.h

@@ -107,4 +107,97 @@ inline shuffle_vector_exprt &to_shuffle_vector_expr(exprt &expr)
   return ret;
 }
 
+/// \brief A Boolean expression returning true, iff the result of performing
+/// operation \c kind on operands \c lhs and \c rhs in infinite-precision
+/// arithmetic cannot be represented in the type of the object that \c result
+/// points to.
+/// If \c result is a pointer, the result of the operation is stored in the
+/// object pointed to by \c result.
+class side_effect_expr_overflowt : public side_effect_exprt
+{
+public:
+  side_effect_expr_overflowt(
+    const irep_idt &kind,
+    exprt _lhs,
+    exprt _rhs,
+    exprt _result,
+    const source_locationt &loc)
+    : side_effect_exprt(
+        "overflow-" + id2string(kind),
+        {std::move(_lhs), std::move(_rhs), std::move(_result)},
+        bool_typet{},
+        loc)
+  {
+  }
+
+  exprt &lhs()
+  {
+    return op0();
+  }
+
+  const exprt &lhs() const
+  {
+    return op0();
+  }
+
+  exprt &rhs()
+  {
+    return op1();
+  }
+
+  const exprt &rhs() const
+  {
+    return op1();
+  }
+
+  exprt &result()
+  {
+    return op2();
+  }
+
+  const exprt &result() const
+  {
+    return op2();
+  }
+};
+
+template <>
+inline bool can_cast_expr<side_effect_expr_overflowt>(const exprt &base)
+{
+  if(base.id() != ID_side_effect)
+    return false;
+
+  const irep_idt &statement = to_side_effect_expr(base).get_statement();
+  return statement == ID_overflow_plus || statement == ID_overflow_mult ||
+         statement == ID_overflow_minus;
+}
+
+/// \brief Cast an exprt to a \ref side_effect_expr_overflowt
+///
+/// \a expr must be known to be \ref side_effect_expr_overflowt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref side_effect_expr_overflowt
+inline const side_effect_expr_overflowt &
+to_side_effect_expr_overflow(const exprt &expr)
+{
+  const auto &side_effect_expr = to_side_effect_expr(expr);
+  PRECONDITION(
+    side_effect_expr.get_statement() == ID_overflow_plus ||
+    side_effect_expr.get_statement() == ID_overflow_mult ||
+    side_effect_expr.get_statement() == ID_overflow_minus);
+  return static_cast<const side_effect_expr_overflowt &>(side_effect_expr);
+}
+
+/// \copydoc to_side_effect_expr_overflow(const exprt &)
+inline side_effect_expr_overflowt &to_side_effect_expr_overflow(exprt &expr)
+{
+  auto &side_effect_expr = to_side_effect_expr(expr);
+  PRECONDITION(
+    side_effect_expr.get_statement() == ID_overflow_plus ||
+    side_effect_expr.get_statement() == ID_overflow_mult ||
+    side_effect_expr.get_statement() == ID_overflow_minus);
+  return static_cast<side_effect_expr_overflowt &>(side_effect_expr);
+}
+
 #endif // CPROVER_ANSI_C_C_EXPR_H

src/ansi-c/c_typecheck_expr.cpp

@@ -34,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "anonymous_member.h"
 #include "builtin_factory.h"
+#include "c_expr.h"
 #include "c_qualifiers.h"
 #include "c_typecast.h"
 #include "expr2c.h"
@@ -3023,14 +3024,12 @@ exprt c_typecheck_baset::do_special_functions(
       throw invalid_source_file_exceptiont{error_message.str()};
     }
 
+    typecheck_function_call_arguments(expr);
+
     auto lhs = expr.arguments()[0];
     auto rhs = expr.arguments()[1];
     auto result_ptr = expr.arguments()[2];
 
-    typecheck_expr(lhs);
-    typecheck_expr(rhs);
-    typecheck_expr(result_ptr);
-
     {
       auto const raise_wrong_argument_error =
         [this,
@@ -3061,48 +3060,16 @@ exprt c_typecheck_baset::do_special_functions(
       }
     }
 
-    // actual logic implementing the operators
-    auto const make_operation = [&identifier](exprt lhs, exprt rhs) -> exprt {
-      if(identifier == "__builtin_add_overflow")
-      {
-        return plus_exprt{lhs, rhs};
-      }
-      else if(identifier == "__builtin_sub_overflow")
-      {
-        return minus_exprt{lhs, rhs};
-      }
-      else
-      {
-        INVARIANT(
-          identifier == "__builtin_mul_overflow",
-          "the three overflow operations are add, sub and mul");
-        return mult_exprt{lhs, rhs};
-      }
-    };
-
-    // we’re basically generating this expression
-    // (*result = (result_type)((integer)lhs OP (integer)rhs)),
-    //   ((integer)result == (integer)lhs OP (integer)rhs)
-    // i.e. perform the operation (+, -, *) on arbitrary length integer,
-    // cast to result type, check if the casted result is still equivalent
-    // to the arbitrary length result.
-    auto operation = make_operation(
-      typecast_exprt{lhs, integer_typet{}},
-      typecast_exprt{rhs, integer_typet{}});
-
-    auto operation_result =
-      typecast_exprt{operation, result_ptr.type().subtype()};
-    typecheck_expr_typecast(operation_result);
-    auto overflow_check = notequal_exprt{
-      typecast_exprt{dereference_exprt{result_ptr}, integer_typet{}},
-      operation};
-    typecheck_expr(overflow_check);
-    return exprt{ID_comma,
-                 bool_typet{},
-                 {side_effect_expr_assignt{dereference_exprt{result_ptr},
-                                           operation_result,
-                                           expr.source_location()},
-                  overflow_check}};
+    irep_idt kind =
+      (identifier == "__builtin_add_overflow")
+        ? ID_plus
+        : (identifier == "__builtin_sub_overflow") ? ID_minus : ID_mult;
+
+    return side_effect_expr_overflowt{kind,
+                                      std::move(lhs),
+                                      std::move(rhs),
+                                      std::move(result_ptr),
+                                      expr.source_location()};
   }
   else
     return nil_exprt();

src/goto-programs/goto_convert_class.h

@@ -25,6 +25,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_program.h"
 #include "destructor_tree.h"
 
+class side_effect_expr_overflowt;
+
 class goto_convertt:public messaget
 {
 public:
@@ -150,6 +152,11 @@ class goto_convertt:public messaget
     exprt &expr,
     goto_programt &dest,
     const irep_idt &mode);
+  void remove_overflow(
+    side_effect_expr_overflowt &expr,
+    goto_programt &dest,
+    bool result_is_used,
+    const irep_idt &mode);
 
   virtual void do_cpp_new(
     const exprt &lhs,

src/goto-programs/goto_convert_side_effect.cpp

@@ -21,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/c_types.h>
 
+#include <ansi-c/c_expr.h>
+
 bool goto_convertt::has_function_call(const exprt &expr)
 {
   forall_operands(it, expr)
@@ -588,6 +590,63 @@ void goto_convertt::remove_statement_expression(
   static_cast<exprt &>(expr)=tmp_symbol_expr;
 }
 
+void goto_convertt::remove_overflow(
+  side_effect_expr_overflowt &expr,
+  goto_programt &dest,
+  bool result_is_used,
+  const irep_idt &mode)
+{
+  const irep_idt &statement = expr.get_statement();
+  const exprt &lhs = expr.lhs();
+  const exprt &rhs = expr.rhs();
+  const exprt &result_ptr = expr.result();
+
+  // actual logic implementing the operators
+  auto const make_operation = [&statement](exprt lhs, exprt rhs) -> exprt {
+    if(statement == ID_overflow_plus)
+    {
+      return plus_exprt{lhs, rhs};
+    }
+    else if(statement == ID_overflow_minus)
+    {
+      return minus_exprt{lhs, rhs};
+    }
+    else
+    {
+      INVARIANT(
+        statement == ID_overflow_mult,
+        "the three overflow operations are add, sub and mul");
+      return mult_exprt{lhs, rhs};
+    }
+  };
+
+  // we’re basically generating this expression
+  // (*result = (result_type)((integer)lhs OP (integer)rhs)),
+  //   ((integer)result == (integer)lhs OP (integer)rhs)
+  // i.e. perform the operation (+, -, *) on arbitrary length integer,
+  // cast to result type, check if the casted result is still equivalent
+  // to the arbitrary length result.
+  auto operation = make_operation(
+    typecast_exprt{lhs, integer_typet{}}, typecast_exprt{rhs, integer_typet{}});
+
+  typecast_exprt operation_result{operation, result_ptr.type().subtype()};
+
+  code_assignt assign{dereference_exprt{result_ptr},
+                      std::move(operation_result),
+                      expr.source_location()};
+  convert_assign(assign, dest, mode);
+
+  if(result_is_used)
+  {
+    notequal_exprt overflow_check{
+      typecast_exprt{dereference_exprt{result_ptr}, integer_typet{}},
+      operation};
+    expr.swap(overflow_check);
+  }
+  else
+    expr.make_nil();
+}
+
 void goto_convertt::remove_side_effect(
   side_effect_exprt &expr,
   goto_programt &dest,
@@ -651,6 +710,13 @@ void goto_convertt::remove_side_effect(
     // the result can't be used, these are void
     expr.make_nil();
   }
+  else if(
+    statement == ID_overflow_plus || statement == ID_overflow_minus ||
+    statement == ID_overflow_mult)
+  {
+    remove_overflow(
+      to_side_effect_expr_overflow(expr), dest, result_is_used, mode);
+  }
   else
   {
     UNREACHABLE;