Implement GCC's __builtin_{add,sub,mul}_overflow_p

Refactor and expand the implementation of
__builtin_{add,sub,mul}_overflow (i.e., without the _p suffix) to also
support the variant that does not store the computed result.

Author: tautschnig

regression/cbmc/gcc_builtin_add_overflow/main.c

@@ -110,6 +110,17 @@ 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;
@@ -128,5 +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,11 @@ 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

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>
 
@@ -2997,7 +2998,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)
@@ -3013,47 +3017,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

@@ -597,7 +597,7 @@ void goto_convertt::remove_overflow(
   const irep_idt &statement = expr.get_statement();
   const exprt &lhs = expr.a();
   const exprt &rhs = expr.b();
-  const exprt &result_ptr = expr.result();
+  const exprt &result = expr.result();
 
   // actual logic implementing the operators: perform operations on signed
   // bitvector types of sufficiently large size to hold the result
@@ -637,8 +637,8 @@ void goto_convertt::remove_overflow(
 
   // Generating the following sequence of statements:
   // large_signedbv tmp = (large_signedbv)lhs OP (large_signedbv)rhs;
-  // *result = (result_type)tmp;
-  // (large_signedbv)*result != tmp;
+  // *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
@@ -651,17 +651,33 @@ void goto_convertt::remove_overflow(
 
   make_temp_symbol(operation, "large_bv", dest, mode);
 
-  const auto &result_type = to_pointer_type(result_ptr.type()).subtype();
-  code_assignt result_assignment{dereference_exprt{result_ptr},
-                                 typecast_exprt{operation, result_type},
-                                 expr.source_location()};
-  convert_assign(result_assignment, 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}, operation.type()},
-      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);

src/util/std_code.h

@@ -2563,7 +2563,8 @@ inline code_function_bodyt &to_code_function_body(codet &code)
 
 /// \brief A Boolean expression returning true, iff the result of performing
 /// 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.
+/// 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