C front-end: evaluate __builtin_clz over constants

regression/cbmc-library/__builtin_clz-02/main.c

@@ -0,0 +1,12 @@
+#ifdef _MSC_VER
+#  define __builtin_clz(x) __lzcnt(x)
+#  define _Static_assert static_assert
+#endif
+
+int main()
+{
+  _Static_assert(
+    __builtin_clz(0xffU) == 8 * sizeof(unsigned) - 8, "compile-time constant");
+
+  return 0;
+}

regression/cbmc-library/__builtin_clz-02/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+For this example, __builtin_clz is fully evaluated in the front-end. The
+_Static_assert ensures this is the case, as type checking fails when
+_Static_assert does not have a compile-time constant value.

src/ansi-c/c_typecheck_expr.cpp

@@ -2591,6 +2591,40 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(popcount_expr);
   }
+  else if(
+    identifier == "__builtin_clz" || identifier == "__builtin_clzl" ||
+    identifier == "__builtin_clzll" || identifier == "__lzcnt16" ||
+    identifier == "__lzcnt" || identifier == "__lzcnt64")
+  {
+    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::string binary_value = integer2binary(
+      *int_constant, to_unsignedbv_type(argument.type()).get_width());
+    std::size_t n_leading_zeros = binary_value.find('1');
+    CHECK_RETURN(n_leading_zeros != std::string::npos);
+
+    return from_integer(
+      n_leading_zeros,
+      to_code_type(try_constant.function().type()).return_type());
+  }
   else if(identifier==CPROVER_PREFIX "equal")
   {
     if(expr.arguments().size()!=2)

src/ansi-c/windows_builtin_headers.h

@@ -1 +1,4 @@
 int __assume(int);
+unsigned short __lzcnt16(unsigned short value);
+unsigned int __lzcnt(unsigned int value);
+unsigned __int64 __lzcnt64(unsigned __int64 value);