Use bitvector types to implement __builtin_{add,sub,mul}_overflow

regression/cbmc/gcc_builtin_add_overflow/main.c

@@ -110,6 +110,26 @@ void check_generic(void)
   assert(0 && "reachability");
 }
 
+void check_generic_p(void)
+{
+  unsigned char small_result = 0;
+  signed long long big_result = 0;
+  assert(!__builtin_add_overflow_p(17, 25, small_result));
+  assert(small_result == 0);
+  assert(!__builtin_add_overflow_p(17, 25, big_result));
+  assert(big_result == 0);
+  assert(0 && "reachability");
+}
+
+void check_non_const()
+{
+  int a, b, c, d, r;
+  // this may overflow (negated assertion fails)
+  assert(!__builtin_add_overflow(a, b, &r));
+  // but need not overflow (assertion fails)
+  assert(__builtin_add_overflow(c, d, &c));
+}
+
 int main(void)
 {
   check_int();
@@ -119,4 +139,6 @@ int main(void)
   check_unsigned_long();
   check_unsigned_long_long();
   check_generic();
+  check_generic_p();
+  check_non_const();
 }

regression/cbmc/gcc_builtin_add_overflow/test.desc

@@ -57,6 +57,13 @@ main.c
 \[check_generic.assertion.9\] line \d+ assertion big_result == 2ll \* .*: SUCCESS
 \[check_generic.assertion.10\] line \d+ assertion __builtin_add_overflow\(.* / 2 \+ 1, .*/ 2 \+ 1, &big_result\): SUCCESS
 \[check_generic.assertion.11\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_generic_p.assertion.1\] line \d+ assertion !__builtin_add_overflow_p\(17, 25, small_result\): SUCCESS
+\[check_generic_p.assertion.2\] line \d+ assertion small_result == 0: SUCCESS
+\[check_generic_p.assertion.3\] line \d+ assertion !__builtin_add_overflow_p\(17, 25, big_result\): SUCCESS
+\[check_generic_p.assertion.4\] line \d+ assertion big_result == 0: SUCCESS
+\[check_generic_p.assertion.5\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_non_const\.assertion\.1\] line \d+ assertion !__builtin_add_overflow\(a, b, &r\): FAILURE
+\[check_non_const\.assertion\.2\] line \d+ assertion __builtin_add_overflow\(c, d, &c\): FAILURE
 VERIFICATION FAILED
 ^EXIT=10$
 ^SIGNAL=0$

src/ansi-c/c_expr.h

@@ -108,9 +108,9 @@ inline shuffle_vector_exprt &to_shuffle_vector_expr(exprt &expr)
 }
 
 /// \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.
+/// operation \c kind on operands \c a and \c b in infinite-precision arithmetic
+/// cannot be represented in the type of the object that \c result points to (or
+/// the type of \c result, if it is not a pointer).
 /// 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

src/ansi-c/c_typecheck_expr.cpp

@@ -29,6 +29,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/range.h>
 #include <util/simplify_expr.h>
 #include <util/string_constant.h>
+#include <util/suffix.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 
@@ -3012,7 +3013,10 @@ exprt c_typecheck_baset::do_special_functions(
   else if(
     identifier == "__builtin_add_overflow" ||
     identifier == "__builtin_sub_overflow" ||
-    identifier == "__builtin_mul_overflow")
+    identifier == "__builtin_mul_overflow" ||
+    identifier == "__builtin_add_overflow_p" ||
+    identifier == "__builtin_sub_overflow_p" ||
+    identifier == "__builtin_mul_overflow_p")
   {
     // check function signature
     if(expr.arguments().size() != 3)
@@ -3028,47 +3032,52 @@ exprt c_typecheck_baset::do_special_functions(
 
     auto lhs = expr.arguments()[0];
     auto rhs = expr.arguments()[1];
-    auto result_ptr = expr.arguments()[2];
+    auto result = expr.arguments()[2];
+
+    const bool is__p_variant = has_suffix(id2string(identifier), "_p");
 
     {
       auto const raise_wrong_argument_error =
-        [this,
-         identifier](const exprt &wrong_argument, std::size_t argument_number) {
+        [this, identifier](
+          const exprt &wrong_argument, std::size_t argument_number, bool _p) {
           std::ostringstream error_message;
           error_message << wrong_argument.source_location().as_string() << ": "
                         << identifier << " has signature " << identifier
-                        << "(integral, integral, integral*), "
+                        << "(integral, integral, integral" << (_p ? "" : "*")
+                        << "), "
                         << "but argument " << argument_number << " ("
                         << expr2c(wrong_argument, *this) << ") has type `"
                         << type2c(wrong_argument.type(), *this) << '`';
           throw invalid_source_file_exceptiont{error_message.str()};
         };
-      for(auto const arg_index : {0, 1})
+      for(int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
       {
         auto const &argument = expr.arguments()[arg_index];
 
         if(!is_signed_or_unsigned_bitvector(argument.type()))
         {
-          raise_wrong_argument_error(argument, arg_index + 1);
+          raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
         }
       }
       if(
-        result_ptr.type().id() != ID_pointer ||
-        !is_signed_or_unsigned_bitvector(result_ptr.type().subtype()))
+        !is__p_variant &&
+        (result.type().id() != ID_pointer ||
+         !is_signed_or_unsigned_bitvector(result.type().subtype())))
       {
-        raise_wrong_argument_error(result_ptr, 3);
+        raise_wrong_argument_error(result, 3, is__p_variant);
       }
     }
 
     irep_idt kind =
-      (identifier == "__builtin_add_overflow")
+      has_prefix(id2string(identifier), "__builtin_add_overflow")
         ? ID_plus
-        : (identifier == "__builtin_sub_overflow") ? ID_minus : ID_mult;
+        : has_prefix(id2string(identifier), "__builtin_sub_overflow") ? ID_minus
+                                                                      : ID_mult;
 
     return side_effect_expr_overflowt{kind,
                                       std::move(lhs),
                                       std::move(rhs),
-                                      std::move(result_ptr),
+                                      std::move(result),
                                       expr.source_location()};
   }
   else

src/goto-programs/goto_convert_side_effect.cpp

@@ -599,48 +599,89 @@ void goto_convertt::remove_overflow(
   const irep_idt &statement = expr.get_statement();
   const exprt &lhs = expr.lhs();
   const exprt &rhs = expr.rhs();
-  const exprt &result_ptr = expr.result();
+  const exprt &result = expr.result();
 
-  // actual logic implementing the operators
+  // actual logic implementing the operators: perform operations on signed
+  // bitvector types of sufficiently large size to hold the result
   auto const make_operation = [&statement](exprt lhs, exprt rhs) -> exprt {
+    std::size_t lhs_ssize = to_bitvector_type(lhs.type()).get_width();
+    if(lhs.type().id() == ID_unsignedbv)
+      ++lhs_ssize;
+    std::size_t rhs_ssize = to_bitvector_type(rhs.type()).get_width();
+    if(rhs.type().id() == ID_unsignedbv)
+      ++rhs_ssize;
+
     if(statement == ID_overflow_plus)
     {
-      return plus_exprt{lhs, rhs};
+      std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
+      integer_bitvector_typet ssize_type{ID_signedbv, ssize};
+      return plus_exprt{typecast_exprt{lhs, ssize_type},
+                        typecast_exprt{rhs, ssize_type}};
     }
     else if(statement == ID_overflow_minus)
     {
-      return minus_exprt{lhs, rhs};
+      std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
+      integer_bitvector_typet ssize_type{ID_signedbv, ssize};
+      return minus_exprt{typecast_exprt{lhs, ssize_type},
+                         typecast_exprt{rhs, ssize_type}};
     }
     else
     {
       INVARIANT(
         statement == ID_overflow_mult,
         "the three overflow operations are add, sub and mul");
-      return mult_exprt{lhs, rhs};
+      std::size_t ssize = lhs_ssize + rhs_ssize;
+      integer_bitvector_typet ssize_type{ID_signedbv, ssize};
+      return mult_exprt{typecast_exprt{lhs, ssize_type},
+                        typecast_exprt{rhs, ssize_type}};
     }
   };
 
-  // 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);
+  // Generating the following sequence of statements:
+  // large_signedbv tmp = (large_signedbv)lhs OP (large_signedbv)rhs;
+  // *result = (result_type)tmp; // only if result is a pointer
+  // (large_signedbv)(result_type)tmp != tmp;
+  // This performs the operation (+, -, *) on a signed bitvector type of
+  // sufficiently large width to store the precise result, cast to result
+  // type, check if the cast result is not equivalent to the full-length
+  // result.
+  auto operation = make_operation(lhs, rhs);
+  // Disable overflow checks as the operation cannot overflow on the larger
+  // type
+  operation.add_source_location() = expr.source_location();
+  operation.add_source_location().add_pragma("disable:signed-overflow-check");
+
+  make_temp_symbol(operation, "large_bv", dest, mode);
+
+  optionalt<typet> result_type;
+  if(result.type().id() == ID_pointer)
+  {
+    result_type = to_pointer_type(result.type()).subtype();
+    code_assignt result_assignment{dereference_exprt{result},
+                                   typecast_exprt{operation, *result_type},
+                                   expr.source_location()};
+    convert_assign(result_assignment, dest, mode);
+  }
+  else
+  {
+    result_type = result.type();
+    // evaluate side effects
+    exprt tmp = result;
+    clean_expr(tmp, dest, mode, false); // result _not_ used
+  }
 
   if(result_is_used)
   {
-    notequal_exprt overflow_check{
-      typecast_exprt{dereference_exprt{result_ptr}, integer_typet{}},
-      operation};
+    typecast_exprt inner_tc{operation, *result_type};
+    inner_tc.add_source_location() = expr.source_location();
+    inner_tc.add_source_location().add_pragma("disable:conversion-check");
+    typecast_exprt outer_tc{inner_tc, operation.type()};
+    outer_tc.add_source_location() = expr.source_location();
+    outer_tc.add_source_location().add_pragma("disable:conversion-check");
+
+    notequal_exprt overflow_check{outer_tc, operation};
+    overflow_check.add_source_location() = expr.source_location();
+
     expr.swap(overflow_check);
   }
   else