Merge pull request #6612 from tautschnig/cleanup/c-library-overflow

tautschnig · web-flow · commit 23306ee7ecc0 · 2022-01-28T10:02:13.000+01:00
Cleanup processing and use __builtin_X_overflow
diff --git a/regression/cbmc/gcc_builtin_add_overflow/main.c b/regression/cbmc/gcc_builtin_add_overflow/main.c
@@ -1,6 +1,20 @@
 #include <assert.h>
 #include <limits.h>
 
+#ifndef __GNUC__
+_Bool __builtin_add_overflow();
+_Bool __builtin_add_overflow_p();
+_Bool __builtin_sadd_overflow(int, int, int *);
+_Bool __builtin_saddl_overflow(long, long, long *);
+_Bool __builtin_saddll_overflow(long long, long long, long long *);
+_Bool __builtin_uadd_overflow(unsigned int, unsigned int, unsigned int *);
+_Bool __builtin_uaddl_overflow(unsigned long, unsigned long, unsigned long *);
+_Bool __builtin_uaddll_overflow(
+  unsigned long long,
+  unsigned long long,
+  unsigned long long *);
+#endif
+
 void check_int(void)
 {
   int const one = 1;
diff --git a/regression/cbmc/gcc_builtin_add_overflow/test.desc b/regression/cbmc/gcc_builtin_add_overflow/test.desc
@@ -1,4 +1,4 @@
-CORE gcc-only
+CORE
 main.c
 
 \[check_int.assertion.1\] line \d+ assertion !__builtin_sadd_overflow\(one, one, &result\): SUCCESS
diff --git a/regression/cbmc/gcc_builtin_add_overflow/type-conflict-2.desc b/regression/cbmc/gcc_builtin_add_overflow/type-conflict-2.desc
@@ -0,0 +1,6 @@
+CORE
+type-conflict.c
+
+line 14 function main: __builtin_add_overflow takes exactly 3 arguments, but 2 were provided$
+^EXIT=6$
+^SIGNAL=0$
diff --git a/regression/cbmc/gcc_builtin_add_overflow/type-conflict.c b/regression/cbmc/gcc_builtin_add_overflow/type-conflict.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+
+#ifndef __GNUC__
+_Bool __builtin_add_overflow();
+_Bool __builtin_add_overflow_p();
+#endif
+
+int main(void)
+{
+  int a, b, c, d, r;
+#ifdef CONFLICT1
+  assert(!__builtin_add_overflow(a, b, r));
+#endif
+  assert(__builtin_add_overflow(c, d));
+}
diff --git a/regression/cbmc/gcc_builtin_add_overflow/type-conflict.desc b/regression/cbmc/gcc_builtin_add_overflow/type-conflict.desc
@@ -0,0 +1,6 @@
+CORE
+type-conflict.c
+-DCONFLICT1
+line 12 function main: __builtin_add_overflow has signature __builtin_add_overflow\(integral, integral, integral\*\), but argument 3 \(r\) has type `signed int`$
+^EXIT=6$
+^SIGNAL=0$
diff --git a/regression/cbmc/gcc_builtin_mul_overflow/main.c b/regression/cbmc/gcc_builtin_mul_overflow/main.c
@@ -2,6 +2,20 @@
 #include <limits.h>
 #include <stdint.h>
 
+#ifndef __GNUC__
+_Bool __builtin_mul_overflow();
+_Bool __builtin_mul_overflow_p();
+_Bool __builtin_smul_overflow(int, int, int *);
+_Bool __builtin_smull_overflow(long, long, long *);
+_Bool __builtin_smulll_overflow(long long, long long, long long *);
+_Bool __builtin_umul_overflow(unsigned int, unsigned int, unsigned int *);
+_Bool __builtin_umull_overflow(unsigned long, unsigned long, unsigned long *);
+_Bool __builtin_umulll_overflow(
+  unsigned long long,
+  unsigned long long,
+  unsigned long long *);
+#endif
+
 #define A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(T)                       \
   (((T)(1)) << (sizeof(T) * CHAR_BIT) / 2 - 1)
 
diff --git a/regression/cbmc/gcc_builtin_mul_overflow/test.desc b/regression/cbmc/gcc_builtin_mul_overflow/test.desc
@@ -1,4 +1,4 @@
-CORE gcc-only
+CORE
 main.c
 
 \[check_int.assertion.1\] line \d+ assertion !__builtin_smul_overflow\(1, 1, &result\): SUCCESS
diff --git a/regression/cbmc/gcc_builtin_sub_overflow/main.c b/regression/cbmc/gcc_builtin_sub_overflow/main.c
@@ -1,6 +1,20 @@
 #include <assert.h>
 #include <limits.h>
 
+#ifndef __GNUC__
+_Bool __builtin_sub_overflow();
+_Bool __builtin_sub_overflow_p();
+_Bool __builtin_ssub_overflow(int, int, int *);
+_Bool __builtin_ssubl_overflow(long, long, long *);
+_Bool __builtin_ssubll_overflow(long long, long long, long long *);
+_Bool __builtin_usub_overflow(unsigned int, unsigned int, unsigned int *);
+_Bool __builtin_usubl_overflow(unsigned long, unsigned long, unsigned long *);
+_Bool __builtin_usubll_overflow(
+  unsigned long long,
+  unsigned long long,
+  unsigned long long *);
+#endif
+
 void check_int(void)
 {
   int result;
@@ -30,7 +44,16 @@ void check_long_long(void)
   assert(result == 0ll);
   assert(__builtin_ssubll_overflow(LLONG_MIN, 1ll, &result));
   assert(!__builtin_ssubll_overflow(LLONG_MIN / 2ll, LLONG_MAX / 2ll, &result));
+#if !defined(_WIN32)
+  // Visual Studio x86/32 bit has an 8-byte "long long" type with corresponding
+  // LLONG_MAX and LLONG_MIN constants (9223372036854775807i64 and
+  // -9223372036854775807i64 - 1, respectively), but compiles these to 32-bit
+  // values. The result is that -LLONG_MAX wraps around to the 32-bit value of
+  // -LLONG_MIN (-2147483648), with the consequence that result == LLONG_MIN
+  // after the above subtraction. Therefore, disable this assertion on Visual
+  // Studio x86/32 bit.
   assert(result - 1ll == LLONG_MIN);
+#endif
   assert(0 && "reachability");
 }
 
diff --git a/regression/cbmc/gcc_builtin_sub_overflow/test.desc b/regression/cbmc/gcc_builtin_sub_overflow/test.desc
@@ -1,4 +1,4 @@
-CORE gcc-only
+CORE
 main.c
 
 \[check_int.assertion.1\] line \d+ assertion !__builtin_ssub_overflow\(1, 1, &result\): SUCCESS
@@ -17,8 +17,7 @@ main.c
 \[check_long_long.assertion.2\] line \d+ assertion result == 0ll: SUCCESS
 \[check_long_long.assertion.3\] line \d+ assertion __builtin_ssubll_overflow\(.*, 1ll, &result\): SUCCESS
 \[check_long_long.assertion.4\] line \d+ assertion !__builtin_ssubll_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_long_long.assertion.[56]\] 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
@@ -40,15 +39,17 @@ main.c
 \[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
-\[check_generic.assertion.1\] line 79 assertion __builtin_sub_overflow\(5, 10, &small_result\): SUCCESS
-\[check_generic.assertion.2\] line 80 assertion !__builtin_sub_overflow\(5, 10, &big_result\): SUCCESS
-\[check_generic.assertion.3\] line 81 assertion big_result == -5ll: SUCCESS
-\[check_generic.assertion.4\] line 82 assertion !__builtin_sub_overflow\(10, 5, &small_result\): SUCCESS
-\[check_generic.assertion.5\] line 83 assertion small_result == 5: SUCCESS
-\[check_generic.assertion.6\] line 84 assertion !__builtin_sub_overflow\(10, 5, &big_result\): SUCCESS
-\[check_generic.assertion.7\] line 85 assertion big_result == 5ll: SUCCESS
-\[check_generic.assertion.8\] line 86 assertion !__builtin_sub_overflow\(.*, .*, &big_result\): SUCCESS
-\[check_generic.assertion.9\] line 87 assertion big_result == 2ll \* .* \+ 1: SUCCESS
-\[check_generic.assertion.10\] line 88 assertion 0 && "reachability": FAILURE
+\[check_generic.assertion.1\] line 102 assertion __builtin_sub_overflow\(5, 10, &small_result\): SUCCESS
+\[check_generic.assertion.2\] line 103 assertion !__builtin_sub_overflow\(5, 10, &big_result\): SUCCESS
+\[check_generic.assertion.3\] line 104 assertion big_result == -5ll: SUCCESS
+\[check_generic.assertion.4\] line 105 assertion !__builtin_sub_overflow\(10, 5, &small_result\): SUCCESS
+\[check_generic.assertion.5\] line 106 assertion small_result == 5: SUCCESS
+\[check_generic.assertion.6\] line 107 assertion !__builtin_sub_overflow\(10, 5, &big_result\): SUCCESS
+\[check_generic.assertion.7\] line 108 assertion big_result == 5ll: SUCCESS
+\[check_generic.assertion.8\] line 109 assertion !__builtin_sub_overflow\(.*, .*, &big_result\): SUCCESS
+\[check_generic.assertion.9\] line 110 assertion big_result == 2ll \* .* \+ 1: SUCCESS
+\[check_generic.assertion.10\] line 111 assertion 0 && "reachability": FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
+--
+\[check_long_long.assertion.5\] line \d+ assertion result - 1ll == .*: FAILURE
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
@@ -202,6 +202,9 @@ class c_typecheck_baset:
   virtual void typecheck_function_call_arguments(
     side_effect_expr_function_callt &expr);
   virtual exprt do_special_functions(side_effect_expr_function_callt &expr);
+  exprt typecheck_builtin_overflow(
+    side_effect_expr_function_callt &expr,
+    const irep_idt &arith_op);
   virtual optionalt<symbol_exprt> typecheck_gcc_polymorphic_builtin(
     const irep_idt &identifier,
     const exprt::operandst &arguments,
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -3170,76 +3170,106 @@ 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_add_overflow_p" ||
-    identifier == "__builtin_sub_overflow_p" ||
+    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")
   {
-    // check function signature
-    if(expr.arguments().size() != 3)
-    {
-      std::ostringstream error_message;
-      error_message << expr.source_location().as_string() << ": " << identifier
-                    << " takes exactly 3 arguments, but "
-                    << expr.arguments().size() << " were provided";
-      throw invalid_source_file_exceptiont{error_message.str()};
-    }
+    return typecheck_builtin_overflow(expr, ID_mult);
+  }
+  else
+    return nil_exprt();
+  // NOLINTNEXTLINE(readability/fn_size)
+}
 
-    typecheck_function_call_arguments(expr);
+exprt c_typecheck_baset::typecheck_builtin_overflow(
+  side_effect_expr_function_callt &expr,
+  const irep_idt &arith_op)
+{
+  const irep_idt &identifier = to_symbol_expr(expr.function()).get_identifier();
 
-    auto lhs = expr.arguments()[0];
-    auto rhs = expr.arguments()[1];
-    auto result = expr.arguments()[2];
-
-    const bool is__p_variant = has_suffix(id2string(identifier), "_p");
-
-    {
-      auto const raise_wrong_argument_error =
-        [this, identifier](
-          const exprt &wrong_argument, std::size_t argument_number, bool _p) {
-          std::ostringstream error_message;
-          error_message << wrong_argument.source_location().as_string() << ": "
-                        << identifier << " has signature " << identifier
-                        << "(integral, integral, integral" << (_p ? "" : "*")
-                        << "), "
-                        << "but argument " << argument_number << " ("
-                        << expr2c(wrong_argument, *this) << ") has type `"
-                        << type2c(wrong_argument.type(), *this) << '`';
-          throw invalid_source_file_exceptiont{error_message.str()};
-        };
-      for(int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
-      {
-        auto const &argument = expr.arguments()[arg_index];
+  // check function signature
+  if(expr.arguments().size() != 3)
+  {
+    std::ostringstream error_message;
+    error_message << expr.source_location().as_string() << ": " << identifier
+                  << " takes exactly 3 arguments, but "
+                  << expr.arguments().size() << " were provided";
+    throw invalid_source_file_exceptiont{error_message.str()};
+  }
 
-        if(!is_signed_or_unsigned_bitvector(argument.type()))
-        {
-          raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
-        }
-      }
-      if(
-        !is__p_variant &&
-        (result.type().id() != ID_pointer ||
-         !is_signed_or_unsigned_bitvector(result.type().subtype())))
+  typecheck_function_call_arguments(expr);
+
+  auto lhs = expr.arguments()[0];
+  auto rhs = expr.arguments()[1];
+  auto result = expr.arguments()[2];
+
+  const bool is__p_variant = has_suffix(id2string(identifier), "_p");
+
+  {
+    auto const raise_wrong_argument_error =
+      [this, identifier](
+        const exprt &wrong_argument, std::size_t argument_number, bool _p) {
+        std::ostringstream error_message;
+        error_message << wrong_argument.source_location().as_string() << ": "
+                      << identifier << " has signature " << identifier
+                      << "(integral, integral, integral" << (_p ? "" : "*")
+                      << "), "
+                      << "but argument " << argument_number << " ("
+                      << expr2c(wrong_argument, *this) << ") has type `"
+                      << type2c(wrong_argument.type(), *this) << '`';
+        throw invalid_source_file_exceptiont{error_message.str()};
+      };
+    for(int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
+    {
+      auto const &argument = expr.arguments()[arg_index];
+
+      if(!is_signed_or_unsigned_bitvector(argument.type()))
       {
-        raise_wrong_argument_error(result, 3, is__p_variant);
+        raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
       }
     }
-
-    irep_idt kind =
-      has_prefix(id2string(identifier), "__builtin_add_overflow")
-        ? ID_plus
-        : has_prefix(id2string(identifier), "__builtin_sub_overflow") ? ID_minus
-                                                                      : ID_mult;
-
-    return side_effect_expr_overflowt{kind,
-                                      std::move(lhs),
-                                      std::move(rhs),
-                                      std::move(result),
-                                      expr.source_location()};
+    if(
+      !is__p_variant &&
+      (result.type().id() != ID_pointer ||
+       !is_signed_or_unsigned_bitvector(result.type().subtype())))
+    {
+      raise_wrong_argument_error(result, 3, is__p_variant);
+    }
   }
-  else
-    return nil_exprt();
+
+  return side_effect_expr_overflowt{arith_op,
+                                    std::move(lhs),
+                                    std::move(rhs),
+                                    std::move(result),
+                                    expr.source_location()};
 }
 
 /// Typecheck the parameters in a function call expression, and where
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE gcc-only`
	`1`	`+CORE`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`\[check_int.assertion.1\] line \d+ assertion !__builtin_sadd_overflow\(one, one, &result\): SUCCESS`