Model GCC's __builtin_clz{,l,ll}

Implement counting leading zeros based on algorithms described in
Hacker's Delight.

Author: tautschnig

regression/cbmc/gcc_clz1/main.c

@@ -0,0 +1,55 @@
+#include <assert.h>
+
+#ifndef __GNUC__
+int __builtin_clz(unsigned int);
+int __builtin_clzl(unsigned long);
+int __builtin_clzll(unsigned long long);
+#endif
+
+unsigned int __VERIFIER_nondet_unsigned();
+unsigned long __VERIFIER_nondet_unsigned_long();
+unsigned long long __VERIFIER_nondet_unsigned_long_long();
+
+// Hacker's Delight
+// http://www.hackersdelight.org/permissions.htm
+int nlz2a(unsigned x)
+{
+  unsigned y;
+  int n, c;
+
+  n = sizeof(x) * 8;
+  c = n / 2;
+  // variant with additional bounding to make sure symbolic execution always
+  // terminates without having to specify an unwinding bound
+  int i = 0;
+  do
+  {
+    y = x >> c;
+    if(y != 0)
+    {
+      n = n - c;
+      x = y;
+    }
+    c = c >> 1;
+    ++i;
+  } while(c != 0 && i < sizeof(x) * 8);
+
+  return n - x;
+}
+
+int main()
+{
+  assert(nlz2a(42) == 26);
+  assert(__builtin_clz(42) == 26);
+  assert(
+    __builtin_clzl(42) == 26 + (sizeof(unsigned long) - sizeof(unsigned)) * 8);
+  assert(
+    __builtin_clzll(42) ==
+    26 + (sizeof(unsigned long long) - sizeof(unsigned)) * 8);
+
+  unsigned int u = __VERIFIER_nondet_unsigned();
+  __CPROVER_assume(u != 0);
+  assert(nlz2a(u) == __builtin_clz(u));
+
+  return 0;
+}

regression/cbmc/gcc_clz1/test.desc

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

src/ansi-c/library/gcc.c

@@ -32,3 +32,61 @@ inline void __sync_synchronize(void)
                   "WWcumul", "RRcumul", "RWcumul", "WRcumul");
   #endif
 }
+
+/* FUNCTION: __builtin_clz */
+
+int __builtin_popcount(unsigned int);
+
+inline int __builtin_clz(unsigned int x)
+{
+  __CPROVER_precondition(x != 0, "__builtin_clz(0) is undefined");
+
+  x = x | (x >> 1);
+  x = x | (x >> 2);
+  x = x | (x >> 4);
+  x = x | (x >> 8);
+  if(sizeof(x) >= 4)
+    x = x | (x >> 16);
+
+  return __builtin_popcount(~x);
+}
+
+/* FUNCTION: __builtin_clzl */
+
+int __builtin_popcountl(unsigned long int);
+
+inline int __builtin_clzl(unsigned long int x)
+{
+  __CPROVER_precondition(x != 0, "__builtin_clzl(0) is undefined");
+
+  x = x | (x >> 1);
+  x = x | (x >> 2);
+  x = x | (x >> 4);
+  x = x | (x >> 8);
+  if(sizeof(x) >= 4)
+    x = x | (x >> 16);
+  if(sizeof(x) >= 8)
+    x = x | (x >> 32);
+
+  return __builtin_popcountl(~x);
+}
+
+/* FUNCTION: __builtin_clzll */
+
+int __builtin_popcountll(unsigned long long int);
+
+inline int __builtin_clzll(unsigned long long int x)
+{
+  __CPROVER_precondition(x != 0, "__builtin_clzll(0) is undefined");
+
+  x = x | (x >> 1);
+  x = x | (x >> 2);
+  x = x | (x >> 4);
+  x = x | (x >> 8);
+  if(sizeof(x) >= 4)
+    x = x | (x >> 16);
+  if(sizeof(x) >= 8)
+    x = x | (x >> 32);
+
+  return __builtin_popcountll(~x);
+}