Add support for gccs __builtin_sub_overflow primitives

Note: Not the generic version

Author: hannes-steffenhagen-diffblue

regression/cbmc/gcc_builtin_sub_overflow/main.c

@@ -0,0 +1,83 @@
+#include <assert.h>
+#include <limits.h>
+
+void check_int(void)
+{
+  int result;
+  assert(!__builtin_ssub_overflow(1, 1, &result));
+  assert(result == 0);
+  assert(__builtin_ssub_overflow(INT_MIN, 1, &result));
+  assert(!__builtin_ssub_overflow(INT_MIN / 2, INT_MAX / 2, &result));
+  assert(result - 1 == INT_MIN);
+  assert(0 && "reachability");
+}
+
+void check_long(void)
+{
+  long result;
+  assert(!__builtin_ssubl_overflow(1l, 1l, &result));
+  assert(result == 0l);
+  assert(__builtin_ssubl_overflow(LONG_MIN, 1l, &result));
+  assert(!__builtin_ssubl_overflow(LONG_MIN / 2l, LONG_MAX / 2l, &result));
+  assert(result - 1l == LONG_MIN);
+  assert(0 && "reachability");
+}
+
+void check_long_long(void)
+{
+  long result;
+  assert(!__builtin_ssubl_overflow(1ll, 1ll, &result));
+  assert(result == 0ll);
+  assert(__builtin_ssubl_overflow(LLONG_MIN, 1ll, &result));
+  assert(!__builtin_ssubl_overflow(LLONG_MIN / 2ll, LLONG_MAX / 2ll, &result));
+  assert(result - 1ll == LLONG_MIN);
+  assert(0 && "reachability");
+}
+
+void check_unsigned(void)
+{
+  unsigned result;
+  assert(!__builtin_usub_overflow(1u, 1u, &result));
+  assert(result == 0u);
+  assert(__builtin_usub_overflow(0u, 1u, &result));
+  assert(!__builtin_usub_overflow(UINT_MAX / 2u, UINT_MAX / 2u, &result));
+  assert(result == 0u);
+  assert(__builtin_usub_overflow(UINT_MAX / 2u, UINT_MAX, &result));
+  assert(0 && "reachability");
+}
+
+void check_unsigned_long(void)
+{
+  unsigned long result;
+  assert(!__builtin_usubl_overflow(1ul, 1ul, &result));
+  assert(result == 0ul);
+  assert(__builtin_usubl_overflow(0ul, 1ul, &result));
+  assert(!__builtin_usubl_overflow(ULONG_MAX / 2ul, ULONG_MAX / 2ul, &result));
+  assert(result == 0ul);
+  assert(__builtin_usubl_overflow(ULONG_MAX / 2ul, ULONG_MAX, &result));
+  assert(0 && "reachability");
+}
+
+void check_unsigned_long_long(void)
+{
+  unsigned long long result;
+  assert(!__builtin_usubll_overflow(1ull, 1ull, &result));
+  assert(result == 0ull);
+  assert(__builtin_usubll_overflow(0ull, 1ull, &result));
+  assert(
+    !__builtin_usubll_overflow(ULLONG_MAX / 2ull, ULLONG_MAX / 2ull, &result));
+  assert(result == 0ull);
+  assert(__builtin_usubll_overflow(ULLONG_MAX / 2ull, ULLONG_MAX, &result));
+  assert(0 && "reachability");
+}
+
+int main(void)
+{
+  __builtin_ssad_overflow(5, 3, (void *)0);
+  check_int();
+  check_long();
+  check_long_long();
+  check_unsigned();
+  check_unsigned_long();
+  check_unsigned_long_long();
+}

src/ansi-c/library/math.c

@@ -2352,3 +2352,57 @@ _Bool __builtin_uaddll_overflow(
   *res = a + b;
   return __CPROVER_overflow_plus(a, b);
 }
+
+/* FUNCTION: __builtin_ssub_overflow */
+
+_Bool __builtin_ssub_overflow(int a, int b, int *res)
+{
+  *res = a - b;
+  return __CPROVER_overflow_minus(a, b);
+}
+
+/* FUNCTION: __builtin_ssubl_overflow */
+
+_Bool __builtin_ssubl_overflow(long a, long b, long *res)
+{
+  *res = a - b;
+  return __CPROVER_overflow_minus(a, b);
+}
+
+/* FUNCTION: __builtin_ssubll_overflow */
+
+_Bool __builtin_ssubll_overflow(long long a, long long b, long long *res)
+{
+  *res = a - b;
+  return __CPROVER_overflow_minus(a, b);
+}
+
+/* FUNCTION: __builtin_usub_overflow */
+
+_Bool __builtin_usub_overflow(unsigned a, unsigned b, unsigned *res)
+{
+  *res = a - b;
+  return __CPROVER_overflow_minus(a, b);
+}
+
+/* FUNCTION: __builtin_usubl_overflow */
+
+_Bool __builtin_usubl_overflow(
+  unsigned long a,
+  unsigned long b,
+  unsigned long *res)
+{
+  *res = a - b;
+  return __CPROVER_overflow_minus(a, b);
+}
+
+/* FUNCTION: __builtin_usubll_overflow */
+
+_Bool __builtin_usubll_overflow(
+  unsigned long long a,
+  unsigned long long b,
+  unsigned long long *res)
+{
+  *res = a - b;
+  return __CPROVER_overflow_minus(a, b);
+}