Add support for gccs __builtin_sub_overflow primitives

regression/cbmc/gcc_builtin_sub_overflow/main.c

@@ -0,0 +1,82 @@
+#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)
+{
+  check_int();
+  check_long();
+  check_long_long();
+  check_unsigned();
+  check_unsigned_long();
+  check_unsigned_long_long();
+}

regression/cbmc/gcc_builtin_sub_overflow/test.desc

@@ -0,0 +1,44 @@
+CORE gcc-only
+main.c
+
+\[check_int.assertion.1\] line \d+ assertion !__builtin_ssub_overflow\(1, 1, &result\): SUCCESS
+\[check_int.assertion.2\] line \d+ assertion result == 0: SUCCESS
+\[check_int.assertion.3\] line \d+ assertion __builtin_ssub_overflow\(.*, 1, &result\): SUCCESS
+\[check_int.assertion.4\] line \d+ assertion !__builtin_ssub_overflow\(.* / 2, .* / 2, &result\): SUCCESS
+\[check_int.assertion.5\] line \d+ assertion result - 1 == .*: SUCCESS
+\[check_int.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_long.assertion.1\] line \d+ assertion !__builtin_ssubl_overflow\(1l, 1l, &result\): SUCCESS
+\[check_long.assertion.2\] line \d+ assertion result == 0l: SUCCESS
+\[check_long.assertion.3\] line \d+ assertion __builtin_ssubl_overflow\(.*, 1l, &result\): SUCCESS
+\[check_long.assertion.4\] line \d+ assertion !__builtin_ssubl_overflow\(.* / 2l, .* / 2l, &result\): SUCCESS
+\[check_long.assertion.5\] line \d+ assertion result - 1l == .*: SUCCESS
+\[check_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_long_long.assertion.1\] line \d+ assertion !__builtin_ssubl_overflow\(1ll, 1ll, &result\): SUCCESS
+\[check_long_long.assertion.2\] line \d+ assertion result == 0ll: SUCCESS
+\[check_long_long.assertion.3\] line \d+ assertion __builtin_ssubl_overflow\(.*, 1ll, &result\): SUCCESS
+\[check_long_long.assertion.4\] line \d+ assertion !__builtin_ssubl_overflow\(.* / 2ll, .* / 2ll, &result\): SUCCESS
+\[check_long_long.assertion.5\] line \d+ assertion result - 1ll == .*: SUCCESS
+\[check_long_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_unsigned.assertion.1\] line \d+ assertion !__builtin_usub_overflow\(1u, 1u, &result\): SUCCESS
+\[check_unsigned.assertion.2\] line \d+ assertion result == 0u: SUCCESS
+\[check_unsigned.assertion.3\] line \d+ assertion __builtin_usub_overflow\(0u, 1u, &result\): SUCCESS
+\[check_unsigned.assertion.4\] line \d+ assertion !__builtin_usub_overflow\(.* / 2u, .* / 2u, &result\): SUCCESS
+\[check_unsigned.assertion.5\] line \d+ assertion result == 0u: SUCCESS
+\[check_unsigned.assertion.6\] line \d+ assertion __builtin_usub_overflow\(.* / 2u, .*, &result\): SUCCESS
+\[check_unsigned.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_unsigned_long.assertion.1\] line \d+ assertion !__builtin_usubl_overflow\(1ul, 1ul, &result\): SUCCESS
+\[check_unsigned_long.assertion.2\] line \d+ assertion result == 0ul: SUCCESS
+\[check_unsigned_long.assertion.3\] line \d+ assertion __builtin_usubl_overflow\(0ul, 1ul, &result\): SUCCESS
+\[check_unsigned_long.assertion.4\] line \d+ assertion !__builtin_usubl_overflow\(.* / 2ul, .* / 2ul, &result\): SUCCESS
+\[check_unsigned_long.assertion.5\] line \d+ assertion result == 0ul: SUCCESS
+\[check_unsigned_long.assertion.6\] line \d+ assertion __builtin_usubl_overflow\(.* / 2ul, .*, &result\): SUCCESS
+\[check_unsigned_long.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_unsigned_long_long.assertion.1\] line \d+ assertion !__builtin_usubll_overflow\(1ull, 1ull, &result\): SUCCESS
+\[check_unsigned_long_long.assertion.2\] line \d+ assertion result == 0ull: SUCCESS
+\[check_unsigned_long_long.assertion.3\] line \d+ assertion __builtin_usubll_overflow\(0ull, 1ull, &result\): SUCCESS
+\[check_unsigned_long_long.assertion.4\] line \d+ assertion !__builtin_usubll_overflow\(.* / 2ull, .* / 2ull, &result\): SUCCESS
+\[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
+^EXIT=10$
+^SIGNAL=0$

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);
+}