Add support for GCCs __builtin_add_overflow primitives

Note: Not the generic version.

Author: hannes-steffenhagen-diffblue

regression/cbmc/gcc_builtin_add_overflow/main.c

@@ -0,0 +1,80 @@
+#include <limits.h>
+#include <assert.h>
+
+void check_int(void)
+{
+  int const one = 1;
+  int result;
+
+  assert(!__builtin_sadd_overflow(one, one, &result));
+  assert(result == 2);
+  assert(__builtin_sadd_overflow(one, INT_MAX, &result));
+  assert(__builtin_sadd_overflow(-one, INT_MIN, &result));
+  assert(0 && "reachability");
+}
+
+void check_long(void)
+{
+  long const one = 1l;
+  long result;
+
+  assert(!__builtin_saddl_overflow(one, one, &result));
+  assert(result == 2l);
+  assert(__builtin_saddl_overflow(one, LONG_MAX, &result));
+  assert(__builtin_saddl_overflow(-one, LONG_MIN, &result));
+  assert(0 && "reachability");
+}
+
+void check_long_long(void)
+{
+  long long const one = 1ll;
+  long long result;
+
+  assert(!__builtin_saddll_overflow(one, one, &result));
+  assert(result == 2ll);
+  assert(__builtin_saddll_overflow(one, LLONG_MAX, &result));
+  assert(__builtin_saddll_overflow(-one, LLONG_MIN, &result));
+  assert(0 && "reachability");
+}
+
+void check_unsigned(void)
+{
+  unsigned const one = 1u;
+  unsigned result;
+
+  assert(!__builtin_uadd_overflow(one, one, &result));
+  assert(result == 2u);
+  assert(__builtin_uadd_overflow(one, UINT_MAX, &result));
+  assert(0 && "reachability");
+}
+
+void check_unsigned_long(void)
+{
+  unsigned long const one = 1ul;
+  unsigned long result;
+
+  assert(!__builtin_uaddl_overflow(one, one, &result));
+  assert(result == 2ul);
+  assert(__builtin_uaddl_overflow(one, ULONG_MAX, &result));
+  assert(0 && "reachability");
+}
+
+void check_unsigned_long_long(void)
+{
+  unsigned long long const one = 1ull;
+  unsigned long long result;
+
+  assert(!__builtin_uaddl_overflow(one, one, &result));
+  assert(result == 2ull);
+  assert(__builtin_uaddl_overflow(one, ULLONG_MAX, &result));
+  assert(0 && "reachability");
+}
+
+int main(void) {
+  check_int();
+  check_long();
+  check_long_long();
+  check_unsigned();
+  check_unsigned_long();
+  check_unsigned_long_long();
+}

regression/cbmc/gcc_builtin_add_overflow/test.desc

@@ -0,0 +1,34 @@
+CORE gcc-only
+main.c
+
+\[check_int.assertion.1\] line \d+ assertion !__builtin_sadd_overflow\(one, one, &result\): SUCCESS
+\[check_int.assertion.2\] line \d+ assertion result == 2: SUCCESS
+\[check_int.assertion.3\] line \d+ assertion __builtin_sadd_overflow\(one, INT_MAX, &result\): SUCCESS
+\[check_int.assertion.4\] line \d+ assertion __builtin_sadd_overflow\(-one, INT_MIN, &result\): SUCCESS
+\[check_int.assertion.5\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_long.assertion.1\] line \d+ assertion !__builtin_saddl_overflow\(one, one, &result\): SUCCESS
+\[check_long.assertion.2\] line \d+ assertion result == 2l: SUCCESS
+\[check_long.assertion.3\] line \d+ assertion __builtin_saddl_overflow\(one, LONG_MAX, &result\): SUCCESS
+\[check_long.assertion.4\] line \d+ assertion __builtin_saddl_overflow\(-one, LONG_MIN, &result\): SUCCESS
+\[check_long.assertion.5\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_long_long.assertion.1\] line \d+ assertion !__builtin_saddll_overflow\(one, one, &result\): SUCCESS
+\[check_long_long.assertion.2\] line \d+ assertion result == 2ll: SUCCESS
+\[check_long_long.assertion.3\] line \d+ assertion __builtin_saddll_overflow\(one, LLONG_MAX, &result\): SUCCESS
+\[check_long_long.assertion.4\] line \d+ assertion __builtin_saddll_overflow\(-one, LLONG_MIN, &result\): SUCCESS
+\[check_long_long.assertion.5\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_unsigned.assertion.1\] line \d+ assertion !__builtin_uadd_overflow\(one, one, &result\): SUCCESS
+\[check_unsigned.assertion.2\] line \d+ assertion result == 2u: SUCCESS
+\[check_unsigned.assertion.3\] line \d+ assertion __builtin_uadd_overflow\(one, UINT_MAX, &result\): SUCCESS
+\[check_unsigned.assertion.4\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_unsigned_long.assertion.1\] line \d+ assertion !__builtin_uaddl_overflow\(one, one, &result\): SUCCESS
+\[check_unsigned_long.assertion.2\] line \d+ assertion result == 2ul: SUCCESS
+\[check_unsigned_long.assertion.3\] line \d+ assertion __builtin_uaddl_overflow\(one, ULONG_MAX, &result\): SUCCESS
+\[check_unsigned_long.assertion.4\] 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.2\] line \d+ assertion result == 2ull: SUCCESS
+\[check_unsigned_long_long.assertion.3\] line \d+ assertion __builtin_uaddl_overflow\(one, ULLONG_MAX, &result\): SUCCESS
+\[check_unsigned_long_long.assertion.4\] line \d+ assertion 0 && "reachability": FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--

src/ansi-c/library/math.c

@@ -2299,5 +2299,44 @@ long double copysignl(long double x, long double y)
   return (signbit(y)) ? -abs : abs;
 }
 
+/* FUNCTION: __builtin_sadd_overflow */
 
+_Bool __builtin_sadd_overflow(int a, int b, int *res) {
+  *res = a + b;
+  return __CPROVER_overflow_plus(a, b);
+}
+
+/* FUNCTION: __builtin_saddl_overflow */
+
+_Bool __builtin_saddl_overflow(long a, long b, long *res) {
+  *res = a + b;
+  return __CPROVER_overflow_plus(a, b);
+}
+
+/* FUNCTION: __builtin_saddll_overflow */
+
+_Bool __builtin_saddll_overflow(long long a, long long b, long long *res) {
+  *res = a + b;
+  return __CPROVER_overflow_plus(a, b);
+}
+
+/* FUNCTION: __builtin_uadd_overflow */
 
+_Bool __builtin_uadd_overflow(unsigned a, unsigned b, unsigned *res) {
+  *res = a + b;
+  return __CPROVER_overflow_plus(a, b);
+}
+
+/* FUNCTION: __builtin_uaddl_overflow */
+
+_Bool __builtin_uaddl_overflow(unsigned long a, unsigned long b, unsigned long *res) {
+  *res = a + b;
+  return __CPROVER_overflow_plus(a, b);
+}
+
+/* FUNCTION: __builtin_uaddll_overflow */
+
+_Bool __builtin_uaddll_overflow(unsigned long long a, unsigned long long b, unsigned long long *res) {
+  *res = a + b;
+  return __CPROVER_overflow_plus(a, b);
+}