C front-end: Handle all __builtin_*_overflow variants in the type checker

The models in the C library incurred unnecessary overhead in that they
would do the arithmetic operation twice: once for the actual (possibly
overflowing) result, and once for determining the overflow bit.

Author: tautschnig

src/ansi-c/c_typecheck_expr.cpp

@@ -3170,18 +3170,36 @@ exprt c_typecheck_baset::do_special_functions(
   }
   else if(
     identifier == "__builtin_add_overflow" ||
+    identifier == "__builtin_sadd_overflow" ||
+    identifier == "__builtin_saddl_overflow" ||
+    identifier == "__builtin_saddll_overflow" ||
+    identifier == "__builtin_uadd_overflow" ||
+    identifier == "__builtin_uaddl_overflow" ||
+    identifier == "__builtin_uaddll_overflow" ||
     identifier == "__builtin_add_overflow_p")
   {
     return typecheck_builtin_overflow(expr, ID_plus);
   }
   else if(
     identifier == "__builtin_sub_overflow" ||
+    identifier == "__builtin_ssub_overflow" ||
+    identifier == "__builtin_ssubl_overflow" ||
+    identifier == "__builtin_ssubll_overflow" ||
+    identifier == "__builtin_usub_overflow" ||
+    identifier == "__builtin_usubl_overflow" ||
+    identifier == "__builtin_usubll_overflow" ||
     identifier == "__builtin_sub_overflow_p")
   {
     return typecheck_builtin_overflow(expr, ID_minus);
   }
   else if(
     identifier == "__builtin_mul_overflow" ||
+    identifier == "__builtin_smul_overflow" ||
+    identifier == "__builtin_smull_overflow" ||
+    identifier == "__builtin_smulll_overflow" ||
+    identifier == "__builtin_umul_overflow" ||
+    identifier == "__builtin_umull_overflow" ||
+    identifier == "__builtin_umulll_overflow" ||
     identifier == "__builtin_mul_overflow_p")
   {
     return typecheck_builtin_overflow(expr, ID_mult);

src/ansi-c/library/math.c

@@ -2297,165 +2297,3 @@ long double copysignl(long double x, long double y)
   long double abs = fabsl(x);
   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);
-}
-
-/* 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);
-}
-
-/* FUNCTION: __builtin_smul_overflow */
-
-_Bool __builtin_smul_overflow(int a, int b, int *res)
-{
-  *res = a * b;
-  return __CPROVER_overflow_mult(a, b);
-}
-
-/* FUNCTION: __builtin_smull_overflow */
-
-_Bool __builtin_smull_overflow(long a, long b, long *res)
-{
-  *res = a * b;
-  return __CPROVER_overflow_mult(a, b);
-}
-
-/* FUNCTION: __builtin_smulll_overflow */
-
-_Bool __builtin_smulll_overflow(long long a, long long b, long long *res)
-{
-  *res = a * b;
-  return __CPROVER_overflow_mult(a, b);
-}
-
-/* FUNCTION: __builtin_umul_overflow */
-
-_Bool __builtin_umul_overflow(unsigned a, unsigned b, unsigned *res)
-{
-  *res = a * b;
-  return __CPROVER_overflow_mult(a, b);
-}
-
-/* FUNCTION: __builtin_umull_overflow */
-
-_Bool __builtin_umull_overflow(
-  unsigned long a,
-  unsigned long b,
-  unsigned long *res)
-{
-  *res = a * b;
-  return __CPROVER_overflow_mult(a, b);
-}
-
-/* FUNCTION: __builtin_umulll_overflow */
-
-_Bool __builtin_umulll_overflow(
-  unsigned long long a,
-  unsigned long long b,
-  unsigned long long *res)
-{
-  *res = a * b;
-  return __CPROVER_overflow_mult(a, b);
-}