Add __builtin_add_overflow primitives

regression/cbmc/gcc_builtin_add_overflow/main.c

@@ -0,0 +1,103 @@
+#include <assert.h>
+#include <limits.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(INT_MAX / 2, INT_MAX / 2, &result));
+  assert(result + 1 == INT_MAX);
+  assert(__builtin_sadd_overflow(INT_MAX / 2 + 2, INT_MAX / 2 + 2, &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(LONG_MAX / 2l, LONG_MAX / 2l, &result));
+  assert(result + 1l == LONG_MAX);
+  assert(
+    __builtin_saddl_overflow(LONG_MAX / 2l + 2l, LONG_MAX / 2l + 2l, &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(LLONG_MAX / 2ll, LLONG_MAX / 2ll, &result));
+  assert(result + 1ll == LLONG_MAX);
+  assert(__builtin_saddll_overflow(
+    LLONG_MAX / 2ll + 2ll, LLONG_MAX / 2ll + 2ll, &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(UINT_MAX / 2, UINT_MAX / 2, &result));
+  assert(result + 1u == UINT_MAX);
+  assert(__builtin_uadd_overflow(UINT_MAX / 2 + 2, UINT_MAX / 2 + 2, &result));
+  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(ULONG_MAX / 2, ULONG_MAX / 2, &result));
+  assert(result + 1ul == ULONG_MAX);
+  assert(
+    __builtin_uaddl_overflow(ULONG_MAX / 2 + 2, ULONG_MAX / 2 + 2, &result));
+  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_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(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,51 @@
+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, .*, &result\): SUCCESS
+\[check_int.assertion.4\] line \d+ assertion !__builtin_sadd_overflow\(.* / 2, .* / 2, &result\): SUCCESS
+\[check_int.assertion.5\] line \d+ assertion result \+ 1 == .*: SUCCESS
+\[check_int.assertion.6\] line \d+ assertion __builtin_sadd_overflow\(.* / 2 \+ 2, .* / 2 \+ 2, &result\): SUCCESS
+\[check_int.assertion.7\] line \d+ assertion __builtin_sadd_overflow\(-one, .*, &result\): SUCCESS
+\[check_int.assertion.8\] 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, .*, &result\): SUCCESS
+\[check_long.assertion.4\] line \d+ assertion !__builtin_saddl_overflow\(.* / 2l, .* / 2l, &result\): SUCCESS
+\[check_long.assertion.5\] line \d+ assertion result \+ 1l == .*: SUCCESS
+\[check_long.assertion.6\] line \d+ assertion __builtin_saddl_overflow\(.* / 2l \+ 2l, .* / 2l \+ 2l, &result\): SUCCESS
+\[check_long.assertion.7\] line \d+ assertion __builtin_saddl_overflow\(-one, .*, &result\): SUCCESS
+\[check_long.assertion.8\] 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, .*, &result\): SUCCESS
+\[check_long_long.assertion.4\] line \d+ assertion !__builtin_saddll_overflow\(.* / 2ll, .* / 2ll, &result\): SUCCESS
+\[check_long_long.assertion.5\] line \d+ assertion result \+ 1ll == .*: SUCCESS
+\[check_long_long.assertion.6\] line \d+ assertion __builtin_saddll_overflow\(.* / 2ll \+ 2ll, .* / 2ll \+ 2ll, &result\): SUCCESS
+\[check_long_long.assertion.7\] line \d+ assertion __builtin_saddll_overflow\(-one, .*, &result\): SUCCESS
+\[check_long_long.assertion.8\] 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\(.* / 2, .* / 2, &result\): SUCCESS
+\[check_unsigned.assertion.4\] line \d+ assertion result \+ 1u == .*: SUCCESS
+\[check_unsigned.assertion.5\] line \d+ assertion __builtin_uadd_overflow\(.* / 2 \+ 2, .* / 2 \+ 2, &result\): SUCCESS
+\[check_unsigned.assertion.6\] line \d+ assertion __builtin_uadd_overflow\(one, .*, &result\): SUCCESS
+\[check_unsigned.assertion.7\] 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\(.* / 2, .* / 2, &result\): SUCCESS
+\[check_unsigned_long.assertion.4\] line \d+ assertion result \+ 1ul == .*: SUCCESS
+\[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.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.7\] line \d+ assertion 0 && "reachability": FAILURE
+VERIFICATION FAILED
+^EXIT=10$
+^SIGNAL=0$

src/ansi-c/CMakeLists.txt

@@ -13,7 +13,7 @@ endforeach()
 
 add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
     COMMAND converter < ${converter_input_path} > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
-    DEPENDS converter
+    DEPENDS converter ${converter_input_path}
 )
 
 add_executable(file_converter file_converter.cpp)

src/ansi-c/library/math.c

@@ -2299,5 +2299,56 @@ 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);
+}