Evaluate __builtin_ffs{,l,ll} over constants at compile time

GCC evaluates this built-in at compile time, and the Linux kernel
assumes this is the case.

Author: tautschnig

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

@@ -7,9 +7,11 @@ int __builtin_ffsl(long);
 int __builtin_ffsll(long long);
 #endif
 
+#ifdef _MSC_VER
+#  define _Static_assert(x, m) static_assert(x, m)
+#endif
+
 int __VERIFIER_nondet_int();
-long __VERIFIER_nondet_long();
-long long __VERIFIER_nondet_long_long();
 
 // http://graphics.stanford.edu/~seander/bithacks.html#ZerosOnRightMultLookup
 static const int multiply_de_bruijn_bit_position[32] = {
@@ -18,14 +20,14 @@ static const int multiply_de_bruijn_bit_position[32] = {
 
 int main()
 {
-  assert(__builtin_ffs(0) == 0);
-  assert(__builtin_ffs(-1) == 1);
-  assert(__builtin_ffs(INT_MIN) == sizeof(int) * 8);
-  assert(__builtin_ffsl(INT_MIN) == sizeof(int) * 8);
-  assert(__builtin_ffsl(LONG_MIN) == sizeof(long) * 8);
-  assert(__builtin_ffsll(INT_MIN) == sizeof(int) * 8);
-  assert(__builtin_ffsll(LLONG_MIN) == sizeof(long long) * 8);
-  assert(__builtin_ffs(INT_MAX) == 1);
+  _Static_assert(__builtin_ffs(0) == 0, "");
+  _Static_assert(__builtin_ffs(-1) == 1, "");
+  _Static_assert(__builtin_ffs(INT_MIN) == sizeof(int) * 8, "");
+  _Static_assert(__builtin_ffsl(INT_MIN) == sizeof(int) * 8, "");
+  _Static_assert(__builtin_ffsl(LONG_MIN) == sizeof(long) * 8, "");
+  _Static_assert(__builtin_ffsll(INT_MIN) == sizeof(int) * 8, "");
+  _Static_assert(__builtin_ffsll(LLONG_MIN) == sizeof(long long) * 8, "");
+  _Static_assert(__builtin_ffs(INT_MAX) == 1, "");
 
   int i = __VERIFIER_nondet_int();
   __CPROVER_assume(i != 0);

src/ansi-c/c_typecheck_expr.cpp

@@ -2759,6 +2759,42 @@ exprt c_typecheck_baset::do_special_functions(
       n_leading_zeros,
       to_code_type(try_constant.function().type()).return_type());
   }
+  else if(
+    identifier == "__builtin_ffs" || identifier == "__builtin_ffsl" ||
+    identifier == "__builtin_ffsll")
+  {
+    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() || argument.type().id() != ID_signedbv)
+    {
+      return nil_exprt{};
+    }
+    else if(*int_constant == 0)
+    {
+      return from_integer(
+        0, to_code_type(try_constant.function().type()).return_type());
+    }
+
+    const std::size_t bit_width = to_signedbv_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,
+      to_code_type(try_constant.function().type()).return_type());
+  }
   else if(identifier==CPROVER_PREFIX "equal")
   {
     if(expr.arguments().size()!=2)