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\(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\(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

@@ -28,6 +28,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
 #include <util/string_constant.h>
+#include <util/suffix.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 
@@ -2813,7 +2814,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)
@@ -2833,33 +2837,37 @@ exprt c_typecheck_baset::do_special_functions(
     typecheck_expr(rhs);
     typecheck_expr(result_ptr);
 
+    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_ptr.type().id() != ID_pointer ||
+         !is_signed_or_unsigned_bitvector(result_ptr.type().subtype())))
       {
-        raise_wrong_argument_error(result_ptr, 3);
+        raise_wrong_argument_error(result_ptr, 3, is__p_variant);
       }
     }
 
@@ -2873,14 +2881,14 @@ exprt c_typecheck_baset::do_special_functions(
       if(rhs.type().id() == ID_unsignedbv)
         ++rhs_ssize;
 
-      if(identifier == "__builtin_add_overflow")
+      if(has_prefix(id2string(identifier), "__builtin_add_overflow"))
       {
         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(identifier == "__builtin_sub_overflow")
+      else if(has_prefix(id2string(identifier), "__builtin_sub_overflow"))
       {
         std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
         integer_bitvector_typet ssize_type{ID_signedbv, ssize};
@@ -2890,7 +2898,7 @@ exprt c_typecheck_baset::do_special_functions(
       else
       {
         INVARIANT(
-          identifier == "__builtin_mul_overflow",
+          has_prefix(id2string(identifier), "__builtin_mul_overflow"),
           "the three overflow operations are add, sub and mul");
         std::size_t ssize = lhs_ssize + rhs_ssize;
         integer_bitvector_typet ssize_type{ID_signedbv, ssize};
@@ -2902,7 +2910,10 @@ exprt c_typecheck_baset::do_special_functions(
     // Generating the following statement expression:
     // ({ large_signedbv tmp = (large_signedbv)lhs OP (large_signedbv)rhs;
     //    *result = (result_type)large_signedbv;
-    //    (large_signedbv)*result != tmp; })
+    //    (large_signedbv)(result_type)tmp != tmp; })
+    // The _p variant just uses result; in place of the assignment to *result.
+    code_blockt statements;
+
     // 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 casted result is not equivalent to the full-length
@@ -2923,23 +2934,43 @@ exprt c_typecheck_baset::do_special_functions(
 
     code_declt decl{new_symbol.symbol_expr()};
     decl.add_source_location() = expr.source_location();
+    statements.add(decl);
 
     code_assignt tmp_assignment{decl.symbol(), operation};
     tmp_assignment.add_source_location() = expr.source_location();
+    statements.add(tmp_assignment);
 
-    const auto &result_type = to_pointer_type(result_ptr.type()).subtype();
-    code_assignt result_assignment{dereference_exprt{result_ptr},
-                                   typecast_exprt{decl.symbol(), result_type}};
-    result_assignment.add_source_location() = expr.source_location();
+    typet result_type;
+    if(!is__p_variant)
+    {
+      result_type = to_pointer_type(result_ptr.type()).subtype();
+      code_assignt result_assignment{
+        dereference_exprt{result_ptr},
+        typecast_exprt{decl.symbol(), result_type}};
+      result_assignment.add_source_location() = expr.source_location();
+      statements.add(result_assignment);
+    }
+    else
+    {
+      result_type = result_ptr.type();
+      code_expressiont eval_side_effects{result_ptr};
+      eval_side_effects.add_source_location() = expr.source_location();
+      statements.add(eval_side_effects);
+    }
 
-    notequal_exprt overflow_check{
-      typecast_exprt{dereference_exprt{result_ptr}, operation.type()},
-      decl.symbol()};
+    typecast_exprt inner_tc{decl.symbol(), 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, decl.symbol()};
     overflow_check.add_source_location() = expr.source_location();
+
     code_expressiont return_expr{overflow_check};
+    return_expr.add_source_location() = expr.source_location();
+    statements.add(return_expr);
 
-    code_blockt statements{
-      {decl, tmp_assignment, result_assignment, return_expr}};
     return side_effect_expr_statement_expressiont{
       statements, overflow_check.type(), expr.source_location()};
   }