C library: add __lzcnt (Visual Studio) and test it

regression/cbmc/gcc_clz1/main.c → regression/cbmc-library/__builtin_clz-01/main.c

@@ -1,9 +1,8 @@
 #include <assert.h>
 
-#ifndef __GNUC__
-int __builtin_clz(unsigned int);
-int __builtin_clzl(unsigned long);
-int __builtin_clzll(unsigned long long);
+#ifdef _MSC_VER
+#  define __builtin_clz(x) __lzcnt(x)
+#  define __builtin_clzll(x) __lzcnt64(x)
 #endif
 
 unsigned int __VERIFIER_nondet_unsigned();
@@ -39,10 +38,16 @@ int nlz2a(unsigned x)
 
 int main()
 {
+#ifdef _MSC_VER
+  unsigned short f = 42;
+  assert(__lzcnt16(f) == 10);
+#endif
   assert(nlz2a(42) == 26);
   assert(__builtin_clz(42) == 26);
+#ifndef _MSC_VER
   assert(
     __builtin_clzl(42) == 26 + (sizeof(unsigned long) - sizeof(unsigned)) * 8);
+#endif
   assert(
     __builtin_clzll(42) ==
     26 + (sizeof(unsigned long long) - sizeof(unsigned)) * 8);

src/ansi-c/library/windows.c

@@ -51,3 +51,46 @@ inline HANDLE CreateThread(
   return handle;
 }
 #endif
+
+/* FUNCTION: __lzcnt16 */
+
+#ifdef _MSC_VER
+int __builtin_clz(unsigned int x);
+
+unsigned short __lzcnt16(unsigned short value)
+{
+  if(value == 0)
+    return 16;
+
+  return __builtin_clz(value) -
+         (sizeof(unsigned int) - sizeof(unsigned short)) * 8;
+}
+#endif
+
+/* FUNCTION: __lzcnt */
+
+#ifdef _MSC_VER
+int __builtin_clz(unsigned int x);
+
+unsigned int __lzcnt(unsigned int value)
+{
+  if(value == 0)
+    return 32;
+
+  return __builtin_clz(value);
+}
+#endif
+
+/* FUNCTION: __lzcnt64 */
+
+#ifdef _MSC_VER
+int __builtin_clzll(unsigned long long x);
+
+unsigned __int64 __lzcnt64(unsigned __int64 value)
+{
+  if(value == 0)
+    return 64;
+
+  return __builtin_clzll(value);
+}
+#endif