Add generic gcc overflow builtins

regression/cbmc/gcc_builtin_add_overflow/main.c

@@ -82,13 +82,31 @@ void check_unsigned_long_long(void)
   unsigned long long const one = 1ull;
   unsigned long long result;
 
-  assert(!__builtin_uaddl_overflow(one, one, &result));
+  assert(!__builtin_uaddll_overflow(one, one, &result));
   assert(result == 2ull);
   assert(!__builtin_uaddll_overflow(ULLONG_MAX / 2, ULLONG_MAX / 2, &result));
   assert(result + 1ull == ULLONG_MAX);
   assert(
     __builtin_uaddll_overflow(ULLONG_MAX / 2 + 2, ULLONG_MAX / 2 + 2, &result));
-  assert(__builtin_uaddl_overflow(one, ULLONG_MAX, &result));
+  assert(__builtin_uaddll_overflow(one, ULLONG_MAX, &result));
+  assert(0 && "reachability");
+}
+
+void check_generic(void)
+{
+  unsigned char small_result;
+  signed long long big_result;
+  assert(!__builtin_add_overflow(17, 25, &small_result));
+  assert(small_result == 42);
+  assert(!__builtin_add_overflow(17, 25, &big_result));
+  assert(big_result == 42ll);
+  assert(__builtin_add_overflow(216, 129, &small_result));
+  assert(!__builtin_add_overflow(216, 129, &big_result));
+  assert(big_result == 345);
+  assert(!__builtin_add_overflow(INT_MAX, INT_MAX, &big_result));
+  assert(big_result == 2ll * INT_MAX);
+  assert(
+    __builtin_add_overflow(LLONG_MAX / 2 + 1, LLONG_MAX / 2 + 1, &big_result));
   assert(0 && "reachability");
 }
 
@@ -100,4 +118,5 @@ int main(void)
   check_unsigned();
   check_unsigned_long();
   check_unsigned_long_long();
+  check_generic();
 }

regression/cbmc/gcc_builtin_add_overflow/test.desc

@@ -39,13 +39,24 @@ main.c
 \[check_unsigned_long.assertion.5\] line \d+ assertion __builtin_uaddl_overflow\(.* / 2 \+ 2, .* / 2 \+ 2, &result\): SUCCESS
 \[check_unsigned_long.assertion.6\] line \d+ assertion __builtin_uaddl_overflow\(one, .*, &result\): SUCCESS
 \[check_unsigned_long.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE
-\[check_unsigned_long_long.assertion.1\] line \d+ assertion !__builtin_uaddl_overflow\(one, one, &result\): SUCCESS
+\[check_unsigned_long_long.assertion.1\] line \d+ assertion !__builtin_uaddll_overflow\(one, one, &result\): SUCCESS
 \[check_unsigned_long_long.assertion.2\] line \d+ assertion result == 2ull: SUCCESS
 \[check_unsigned_long_long.assertion.3\] line \d+ assertion !__builtin_uaddll_overflow\(.* / 2, .* / 2, &result\): SUCCESS
 \[check_unsigned_long_long.assertion.4\] line \d+ assertion result \+ 1ull == .*: SUCCESS
 \[check_unsigned_long_long.assertion.5\] line \d+ assertion __builtin_uaddll_overflow\(.* / 2 \+ 2, .* / 2 \+ 2, &result\): SUCCESS
-\[check_unsigned_long_long.assertion.6\] line \d+ assertion __builtin_uaddl_overflow\(one, .*, &result\): SUCCESS
+\[check_unsigned_long_long.assertion.6\] line \d+ assertion __builtin_uaddll_overflow\(one, .*, &result\): SUCCESS
 \[check_unsigned_long_long.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_generic.assertion.1\] line \d+ assertion !__builtin_add_overflow\(17, 25, &small_result\): SUCCESS
+\[check_generic.assertion.2\] line \d+ assertion small_result == 42: SUCCESS
+\[check_generic.assertion.3\] line \d+ assertion !__builtin_add_overflow\(17, 25, &big_result\): SUCCESS
+\[check_generic.assertion.4\] line \d+ assertion big_result == 42ll: SUCCESS
+\[check_generic.assertion.5\] line \d+ assertion __builtin_add_overflow\(216, 129, &small_result\): SUCCESS
+\[check_generic.assertion.6\] line \d+ assertion !__builtin_add_overflow\(216, 129, &big_result\): SUCCESS
+\[check_generic.assertion.7\] line \d+ assertion big_result == 345: SUCCESS
+\[check_generic.assertion.8\] line \d+ assertion !__builtin_add_overflow\(.*, .*, &big_result\): SUCCESS
+\[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
 VERIFICATION FAILED
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/gcc_builtin_mul_overflow/main.c

@@ -104,6 +104,22 @@ void check_unsigned_long_long(void)
   assert(0 && "reachability");
 }
 
+void check_generic(void)
+{
+  unsigned char small_result;
+  long long big_result;
+
+  assert(__builtin_mul_overflow(100, 100, &small_result));
+  assert(!__builtin_mul_overflow(100, 100, &big_result));
+  assert(big_result == 10000);
+  assert(!__builtin_mul_overflow(10, 10, &small_result));
+  assert(small_result == 100);
+  assert(!__builtin_mul_overflow(INT_MAX, INT_MAX, &big_result));
+  assert(big_result == 4611686014132420609ll);
+  assert(__builtin_mul_overflow(INT_MAX * 2ll, INT_MAX * 2ll, &big_result));
+  assert(0 && "reachability");
+}
+
 int main(void)
 {
   check_int();
@@ -112,5 +128,6 @@ int main(void)
   check_unsigned();
   check_unsigned_long();
   check_unsigned_long_long();
+  check_generic();
   return 0;
 }

regression/cbmc/gcc_builtin_mul_overflow/test.desc

@@ -37,5 +37,14 @@ main.c
 \[check_unsigned_long_long.assertion.4\] line \d+ assertion result == lt_isqrt_of_unsigned_long_long_max \* lt_isqrt_of_unsigned_long_long_max: SUCCESS
 \[check_unsigned_long_long.assertion.5\] line \d+ assertion __builtin_umulll_overflow\( lt_isqrt_of_unsigned_long_long_max << 1, lt_isqrt_of_unsigned_long_long_max << 1, &result\): SUCCESS
 \[check_unsigned_long_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_generic.assertion.1\] line \d+ assertion __builtin_mul_overflow\(100, 100, &small_result\): SUCCESS
+\[check_generic.assertion.2\] line \d+ assertion !__builtin_mul_overflow\(100, 100, &big_result\): SUCCESS
+\[check_generic.assertion.3\] line \d+ assertion big_result == 10000: SUCCESS
+\[check_generic.assertion.4\] line \d+ assertion !__builtin_mul_overflow\(10, 10, &small_result\): SUCCESS
+\[check_generic.assertion.5\] line \d+ assertion small_result == 100: SUCCESS
+\[check_generic.assertion.6\] line \d+ assertion !__builtin_mul_overflow\(.*, .*, &big_result\): SUCCESS
+\[check_generic.assertion.7\] line \d+ assertion big_result == 4611686014132420609ll: SUCCESS
+\[check_generic.assertion.8\] line \d+ assertion __builtin_mul_overflow\(.* \* 2ll, .* \* 2ll, &big_result\): SUCCESS
+\[check_generic.assertion.9\] line \d+ assertion 0 && "reachability": FAILURE
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/gcc_builtin_sub_overflow/main.c

@@ -71,6 +71,23 @@ void check_unsigned_long_long(void)
   assert(0 && "reachability");
 }
 
+void check_generic(void)
+{
+  unsigned char small_result;
+  long long big_result;
+
+  assert(__builtin_sub_overflow(5, 10, &small_result));
+  assert(!__builtin_sub_overflow(5, 10, &big_result));
+  assert(big_result == -5ll);
+  assert(!__builtin_sub_overflow(10, 5, &small_result));
+  assert(small_result == 5);
+  assert(!__builtin_sub_overflow(10, 5, &big_result));
+  assert(big_result == 5ll);
+  assert(!__builtin_sub_overflow(INT_MIN, INT_MAX, &big_result));
+  assert(big_result == 2ll * INT_MIN + 1);
+  assert(0 && "reachability");
+}
+
 int main(void)
 {
   check_int();
@@ -79,4 +96,5 @@ int main(void)
   check_unsigned();
   check_unsigned_long();
   check_unsigned_long_long();
+  check_generic();
 }

regression/cbmc/gcc_builtin_sub_overflow/test.desc

@@ -40,5 +40,15 @@ main.c
 \[check_unsigned_long_long.assertion.5\] line \d+ assertion result == 0ull: SUCCESS
 \[check_unsigned_long_long.assertion.6\] line \d+ assertion __builtin_usubll_overflow\(.* / 2ull, .*, &result\): SUCCESS
 \[check_unsigned_long_long.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_generic.assertion.1\] line 79 assertion __builtin_sub_overflow\(5, 10, &small_result\): SUCCESS
+\[check_generic.assertion.2\] line 80 assertion !__builtin_sub_overflow\(5, 10, &big_result\): SUCCESS
+\[check_generic.assertion.3\] line 81 assertion big_result == -5ll: SUCCESS
+\[check_generic.assertion.4\] line 82 assertion !__builtin_sub_overflow\(10, 5, &small_result\): SUCCESS
+\[check_generic.assertion.5\] line 83 assertion small_result == 5: SUCCESS
+\[check_generic.assertion.6\] line 84 assertion !__builtin_sub_overflow\(10, 5, &big_result\): SUCCESS
+\[check_generic.assertion.7\] line 85 assertion big_result == 5ll: SUCCESS
+\[check_generic.assertion.8\] line 86 assertion !__builtin_sub_overflow\(.*, .*, &big_result\): SUCCESS
+\[check_generic.assertion.9\] line 87 assertion big_result == 2ll \* .* \+ 1: SUCCESS
+\[check_generic.assertion.10\] line 88 assertion 0 && "reachability": FAILURE
 ^EXIT=10$
 ^SIGNAL=0$

src/ansi-c/c_typecheck_expr.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "c_typecheck_base.h"
 
 #include <cassert>
+#include <sstream>
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
@@ -33,6 +34,7 @@ Author: Daniel Kroening, [email protected]
 #include "builtin_factory.h"
 #include "c_qualifiers.h"
 #include "c_typecast.h"
+#include "expr2c.h"
 #include "padding.h"
 #include "type2name.h"
 
@@ -2801,6 +2803,102 @@ exprt c_typecheck_baset::do_special_functions(
     overflow.type() = bool_typet{};
     return overflow;
   }
+  else if(
+    identifier == "__builtin_add_overflow" ||
+    identifier == "__builtin_sub_overflow" ||
+    identifier == "__builtin_mul_overflow")
+  {
+    // check function signature
+    if(expr.arguments().size() != 3)
+    {
+      std::ostringstream error_message;
+      error_message << expr.source_location().as_string() << ": " << identifier
+                    << " takes exactly 3 arguments, but "
+                    << expr.arguments().size() << " were provided";
+      throw invalid_source_file_exceptiont{error_message.str()};
+    }
+
+    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,
+         identifier](const exprt &wrong_argument, std::size_t argument_number) {
+          std::ostringstream error_message;
+          error_message << wrong_argument.source_location().as_string() << ": "
+                        << identifier << " has signature " << identifier
+                        << "(integral, integral, integral*), "
+                        << "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})
+      {
+        auto const &argument = expr.arguments()[arg_index];
+
+        if(!is_signed_or_unsigned_bitvector(argument.type()))
+        {
+          raise_wrong_argument_error(argument, arg_index + 1);
+        }
+      }
+      if(
+        result_ptr.type().id() != ID_pointer ||
+        !is_signed_or_unsigned_bitvector(result_ptr.type().subtype()))
+      {
+        raise_wrong_argument_error(result_ptr, 3);
+      }
+    }
+
+    // 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}};
+  }
   else
     return nil_exprt();
 }