Implement __builtin_ctz{,l,ll} including constant evaluation

__builtin_ctz returns the number of trailing zeros. Just like ffs and
clz, evaluate application of the built-in to constants in the front-end.

Author: tautschnig

regression/cbmc-library/__builtin_ctz-01/main.c

@@ -0,0 +1,46 @@
+#include <assert.h>
+#include <limits.h>
+
+#ifndef __GNUC__
+int __builtin_ctz(int);
+int __builtin_ctzl(long);
+int __builtin_ctzll(long long);
+#endif
+
+#ifdef _MSC_VER
+#  define _Static_assert(x, m) static_assert(x, m)
+#endif
+
+unsigned __VERIFIER_nondet_unsigned();
+
+// http://graphics.stanford.edu/~seander/bithacks.html#ZerosOnRightMultLookup
+static const int multiply_de_bruijn_bit_position[32] = {
+  0,  1,  28, 2,  29, 14, 24, 3, 30, 22, 20, 15, 25, 17, 4,  8,
+  31, 27, 13, 23, 21, 19, 16, 7, 26, 12, 18, 6,  11, 5,  10, 9};
+
+int main()
+{
+  _Static_assert(__builtin_ctz(1) == 0, "");
+  _Static_assert(__builtin_ctz(UINT_MAX) == 0, "");
+  _Static_assert(
+    __builtin_ctz(1U << (sizeof(unsigned) * 8 - 1)) == sizeof(unsigned) * 8 - 1,
+    "");
+  _Static_assert(
+    __builtin_ctzl(1UL << (sizeof(unsigned) * 8 - 1)) ==
+      sizeof(unsigned) * 8 - 1,
+    "");
+  _Static_assert(
+    __builtin_ctzll(1ULL << (sizeof(unsigned) * 8 - 1)) ==
+      sizeof(unsigned) * 8 - 1,
+    "");
+
+  unsigned u = __VERIFIER_nondet_unsigned();
+  __CPROVER_assume(u != 0);
+  __CPROVER_assume(sizeof(u) == 4);
+  __CPROVER_assume(u > INT_MIN);
+  assert(
+    multiply_de_bruijn_bit_position
+      [((unsigned)((u & -u) * 0x077CB531U)) >> 27] == __builtin_ctz(u));
+
+  return 0;
+}

regression/cbmc-library/__builtin_ctz-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_expr.cpp

@@ -2768,6 +2768,40 @@ exprt c_typecheck_baset::do_special_functions(
       n_leading_zeros,
       to_code_type(try_constant.function().type()).return_type());
   }
+  else if(
+    identifier == "__builtin_ctz" || identifier == "__builtin_ctzl" ||
+    identifier == "__builtin_ctzll")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << identifier << " expects one operand" << eom;
+      throw 0;
+    }
+
+    side_effect_expr_function_callt try_constant{expr};
+    typecheck_function_call_arguments(try_constant);
+    exprt argument = try_constant.arguments().front();
+    simplify(argument, *this);
+    const auto int_constant = numeric_cast<mp_integer>(argument);
+
+    if(
+      !int_constant.has_value() || *int_constant == 0 ||
+      argument.type().id() != ID_unsignedbv)
+    {
+      return nil_exprt{};
+    }
+
+    const std::size_t bit_width =
+      to_unsignedbv_type(argument.type()).get_width();
+    const std::string binary_value = integer2binary(*int_constant, bit_width);
+    std::size_t last_one_bit = binary_value.rfind('1');
+    CHECK_RETURN(last_one_bit != std::string::npos);
+
+    return from_integer(
+      bit_width - last_one_bit - 1,
+      to_code_type(try_constant.function().type()).return_type());
+  }
   else if(
     identifier == "__builtin_ffs" || identifier == "__builtin_ffsl" ||
     identifier == "__builtin_ffsll")

src/ansi-c/library/gcc.c

@@ -91,6 +91,39 @@ inline int __builtin_clzll(unsigned long long int x)
   return __builtin_popcountll(~x);
 }
 
+/* FUNCTION: __builtin_ctz */
+
+int __builtin_popcount(unsigned int);
+
+inline int __builtin_ctz(unsigned int x)
+{
+  __CPROVER_precondition(x != 0, "__builtin_ctz(0) is undefined");
+
+  return __builtin_popcount(x ^ (x - 1)) - 1;
+}
+
+/* FUNCTION: __builtin_ctzl */
+
+int __builtin_popcountl(unsigned long int);
+
+inline int __builtin_ctzl(unsigned long int x)
+{
+  __CPROVER_precondition(x != 0, "__builtin_ctzl(0) is undefined");
+
+  return __builtin_popcountl(x ^ (x - 1)) - 1;
+}
+
+/* FUNCTION: __builtin_ctzll */
+
+int __builtin_popcountll(unsigned long long int);
+
+inline int __builtin_ctzll(unsigned long long int x)
+{
+  __CPROVER_precondition(x != 0, "__builtin_ctzll(0) is undefined");
+
+  return __builtin_popcountll(x ^ (x - 1)) - 1;
+}
+
 /* FUNCTION: __builtin_ffs */
 
 int __builtin_clz(unsigned int x);