Implement __builtin_ctz{,l,ll} via count_trailing_zeros_exprt

__builtin_ctz returns the number of trailing zeros. Just like ffs and
clz, introduce a new bitvector expression.

Author: tautschnig

regression/cbmc/__builtin_ctz-01/main.c

@@ -0,0 +1,49 @@
+#include <assert.h>
+#include <limits.h>
+
+#ifndef __GNUC__
+int __builtin_ctz(unsigned int);
+int __builtin_ctzl(unsigned long);
+int __builtin_ctzll(unsigned long long);
+#endif
+
+#ifdef _MSC_VER
+#  define _Static_assert(x, m) static_assert(x, m)
+#endif
+
+unsigned __VERIFIER_nondet_unsigned();
+
+// 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()
+{
+  _Static_assert(__builtin_ctz(1) == 0, "");
+  _Static_assert(__builtin_ctz(UINT_MAX) == 0, "");
+  _Static_assert(
+    __builtin_ctz(1U << (sizeof(unsigned) * 8 - 1)) == sizeof(unsigned) * 8 - 1,
+    "");
+  _Static_assert(
+    __builtin_ctzl(1UL << (sizeof(unsigned) * 8 - 1)) ==
+      sizeof(unsigned) * 8 - 1,
+    "");
+  _Static_assert(
+    __builtin_ctzll(1ULL << (sizeof(unsigned) * 8 - 1)) ==
+      sizeof(unsigned) * 8 - 1,
+    "");
+
+  unsigned u = __VERIFIER_nondet_unsigned();
+  __CPROVER_assume(u != 0);
+  __CPROVER_assume(sizeof(u) == 4);
+  __CPROVER_assume(u > INT_MIN);
+  assert(
+    multiply_de_bruijn_bit_position
+      [((unsigned)((u & -u) * 0x077CB531U)) >> 27] == __builtin_ctz(u));
+
+  // a failing assertion should be generated as __builtin_ctz is undefined for 0
+  __builtin_ctz(0U);
+
+  return 0;
+}

regression/cbmc/__builtin_ctz-01/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--bounds-check
+^\[main.bit_count.\d+\] line 46 count trailing zeros argument in __builtin_ctz\(0u\): FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

scripts/expected_doxygen_warnings.txt

@@ -82,20 +82,20 @@
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'arith_tools.h' not generated, too many nodes (183), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'config.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'invariant.h' not generated, too many nodes (188), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'invariant.h' not generated, too many nodes (189), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'namespace.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (101), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (79), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_expr.h' not generated, too many nodes (245), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_expr.h' not generated, too many nodes (246), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_types.h' not generated, too many nodes (121), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/analyses/goto_check.cpp

@@ -174,7 +174,7 @@ class goto_checkt
 
   void bounds_check(const exprt &, const guardt &);
   void bounds_check_index(const index_exprt &, const guardt &);
-  void bounds_check_clz(const count_leading_zeros_exprt &, const guardt &);
+  void bounds_check_bit_count(const unary_exprt &, const guardt &);
   void div_by_zero_check(const div_exprt &, const guardt &);
   void mod_by_zero_check(const mod_exprt &, const guardt &);
   void mod_overflow_check(const mod_exprt &, const guardt &);
@@ -1326,8 +1326,11 @@ void goto_checkt::bounds_check(const exprt &expr, const guardt &guard)
 
   if(expr.id() == ID_index)
     bounds_check_index(to_index_expr(expr), guard);
-  else if(expr.id() == ID_count_leading_zeros)
-    bounds_check_clz(to_count_leading_zeros_expr(expr), guard);
+  else if(
+    expr.id() == ID_count_leading_zeros || expr.id() == ID_count_trailing_zeros)
+  {
+    bounds_check_bit_count(to_unary_expr(expr), guard);
+  }
 }
 
 void goto_checkt::bounds_check_index(
@@ -1509,13 +1512,22 @@ void goto_checkt::bounds_check_index(
   }
 }
 
-void goto_checkt::bounds_check_clz(
-  const count_leading_zeros_exprt &expr,
+void goto_checkt::bounds_check_bit_count(
+  const unary_exprt &expr,
   const guardt &guard)
 {
+  std::string name;
+
+  if(expr.id() == ID_count_leading_zeros)
+    name = "leading";
+  else if(expr.id() == ID_count_trailing_zeros)
+    name = "trailing";
+  else
+    UNREACHABLE;
+
   add_guarded_property(
     notequal_exprt{expr.op(), from_integer(0, expr.op().type())},
-    "count leading zeros argument",
+    "count " + name + " zeros argument",
     "bit count",
     expr.find_source_location(),
     expr,
@@ -1778,7 +1790,8 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
   {
     pointer_primitive_check(expr, guard);
   }
-  else if(expr.id() == ID_count_leading_zeros)
+  else if(
+    expr.id() == ID_count_leading_zeros || expr.id() == ID_count_trailing_zeros)
   {
     bounds_check(expr, guard);
   }

src/ansi-c/c_typecheck_expr.cpp

@@ -2698,6 +2698,25 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(clz);
   }
+  else if(
+    identifier == "__builtin_ctz" || identifier == "__builtin_ctzl" ||
+    identifier == "__builtin_ctzll")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << identifier << " expects one operand" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    count_trailing_zeros_exprt ctz{
+      expr.arguments().front(), false, expr.type()};
+    ctz.add_source_location() = source_location;
+
+    return std::move(ctz);
+  }
   else if(identifier==CPROVER_PREFIX "equal")
   {
     if(expr.arguments().size()!=2)

src/ansi-c/expr2c.cpp

@@ -3899,6 +3899,9 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id() == ID_count_leading_zeros)
     return convert_function(src, "__builtin_clz");
 
+  else if(src.id() == ID_count_trailing_zeros)
+    return convert_function(src, "__builtin_ctz");
+
   // no C language expression for internal representation
   return convert_norep(src, precedence);
 }

src/ansi-c/library/gcc.c

@@ -33,57 +33,6 @@ inline void __sync_synchronize(void)
   #endif
 }
 
-/* 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);

src/solvers/Makefile

@@ -141,6 +141,7 @@ SRC = $(BOOLEFORCE_SRC) \
       floatbv/float_approximation.cpp \
       lowering/byte_operators.cpp \
       lowering/count_leading_zeros.cpp \
+      lowering/count_trailing_zeros.cpp \
       lowering/functions.cpp \
       lowering/popcount.cpp \
       bdd/miniBDD/miniBDD.cpp \

src/solvers/flattening/boolbv.cpp

@@ -230,6 +230,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
     return convert_bv(lower_popcount(to_popcount_expr(expr), ns));
   else if(expr.id() == ID_count_leading_zeros)
     return convert_bv(lower_clz(to_count_leading_zeros_expr(expr), ns));
+  else if(expr.id() == ID_count_trailing_zeros)
+    return convert_bv(lower_ctz(to_count_trailing_zeros_expr(expr), ns));
 
   return conversion_failed(expr);
 }

src/solvers/lowering/count_trailing_zeros.cpp

@@ -0,0 +1,35 @@
+/*******************************************************************\
+
+Module: Lowering of count_trailing_zeros
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include "expr_lowering.h"
+
+#include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
+#include <util/invariant.h>
+#include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
+#include <util/std_expr.h>
+
+exprt lower_ctz(const count_trailing_zeros_exprt &expr, const namespacet &ns)
+{
+  exprt x = expr.op();
+  const auto x_width = pointer_offset_bits(x.type(), ns);
+  CHECK_RETURN(x_width.has_value() && *x_width >= 1);
+  const std::size_t int_width = numeric_cast_v<std::size_t>(*x_width);
+
+  // popcount(x ^ ((unsigned)x - 1)) - 1
+  const unsignedbv_typet ut{int_width};
+  minus_exprt minus_one{typecast_exprt::conditional_cast(x, ut),
+                        from_integer(1, ut)};
+  popcount_exprt popcount{
+    bitxor_exprt{x, typecast_exprt::conditional_cast(minus_one, x.type())}};
+  minus_exprt result{lower_popcount(popcount, ns), from_integer(1, x.type())};
+
+  return simplify_expr(
+    typecast_exprt::conditional_cast(result, expr.type()), ns);
+}

src/solvers/lowering/expr_lowering.h

@@ -14,6 +14,7 @@ Author: Michael Tautschnig
 class byte_extract_exprt;
 class byte_update_exprt;
 class count_leading_zeros_exprt;
+class count_trailing_zeros_exprt;
 class namespacet;
 class popcount_exprt;
 
@@ -57,4 +58,10 @@ exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns);
 /// \return Semantically equivalent expression
 exprt lower_clz(const count_leading_zeros_exprt &expr, const namespacet &ns);
 
+/// Lower a count_trailing_zeros_exprt to arithmetic and logic expressions.
+/// \param expr: Input expression to be translated
+/// \param ns: Namespace for type lookups
+/// \return Semantically equivalent expression
+exprt lower_ctz(const count_trailing_zeros_exprt &expr, const namespacet &ns);
+
 #endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */

src/solvers/smt2/smt2_conv.cpp

@@ -1992,6 +1992,11 @@ void smt2_convt::convert_expr(const exprt &expr)
     exprt lowered = lower_clz(to_count_leading_zeros_expr(expr), ns);
     convert_expr(lowered);
   }
+  else if(expr.id() == ID_count_trailing_zeros)
+  {
+    exprt lowered = lower_ctz(to_count_trailing_zeros_expr(expr), ns);
+    convert_expr(lowered);
+  }
   else
     INVARIANT_WITH_DIAGNOSTICS(
       false,