Merge pull request #5728 from tautschnig/ffs

GCC built-ins: implement __builtin_ffs{,l,ll}

Author: tautschnig

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

@@ -0,0 +1,41 @@
+#include <assert.h>
+#include <limits.h>
+
+#ifndef __GNUC__
+int __builtin_ffs(int);
+int __builtin_ffsl(long);
+int __builtin_ffsll(long long);
+#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] = {
+  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()
+{
+  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);
+
+  int i = __VERIFIER_nondet_int();
+  __CPROVER_assume(i != 0);
+  __CPROVER_assume(sizeof(i) == 4);
+  __CPROVER_assume(i > INT_MIN);
+  assert(
+    multiply_de_bruijn_bit_position
+        [((unsigned)((i & -i) * 0x077CB531U)) >> 27] +
+      1 ==
+    __builtin_ffs(i));
+
+  return 0;
+}

regression/cbmc-library/__builtin_ffs-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/library/gcc.c

@@ -91,6 +91,57 @@ inline int __builtin_clzll(unsigned long long int x)
   return __builtin_popcountll(~x);
 }
 
+/* FUNCTION: __builtin_ffs */
+
+int __builtin_clz(unsigned int x);
+
+inline int __builtin_ffs(int x)
+{
+  if(x == 0)
+    return 0;
+
+#pragma CPROVER check push
+#pragma CPROVER check disable "conversion"
+  unsigned int u = (unsigned int)x;
+#pragma CPROVER check pop
+
+  return sizeof(int) * 8 - __builtin_clz(u & ~(u - 1));
+}
+
+/* FUNCTION: __builtin_ffsl */
+
+int __builtin_clzl(unsigned long x);
+
+inline int __builtin_ffsl(long x)
+{
+  if(x == 0)
+    return 0;
+
+#pragma CPROVER check push
+#pragma CPROVER check disable "conversion"
+  unsigned long u = (unsigned long)x;
+#pragma CPROVER check pop
+
+  return sizeof(long) * 8 - __builtin_clzl(u & ~(u - 1));
+}
+
+/* FUNCTION: __builtin_ffsll */
+
+int __builtin_clzll(unsigned long long x);
+
+inline int __builtin_ffsll(long long x)
+{
+  if(x == 0)
+    return 0;
+
+#pragma CPROVER check push
+#pragma CPROVER check disable "conversion"
+  unsigned long long u = (unsigned long long)x;
+#pragma CPROVER check pop
+
+  return sizeof(long long) * 8 - __builtin_clzll(u & ~(u - 1));
+}
+
 /* FUNCTION: __atomic_test_and_set */
 
 void __atomic_thread_fence(int memorder);