Merge pull request #5881 from tautschnig/ctz-expression

Implement __builtin_ctz{,l,ll} via count_trailing_zeros_exprt

Author: tautschnig

regression/cbmc/__builtin_clz-01/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --bounds-check
-^\[main.bit_count.\d+\] line 61 count leading zeros argument in __builtin_clz\(0u\): FAILURE$
+^\[main.bit_count.\d+\] line 61 count leading zeros is undefined for value zero in __builtin_clz\(0u\): FAILURE$
 ^\*\* 1 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$

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 is undefined for value zero in __builtin_ctz\(0u\): FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

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 &);
@@ -1336,8 +1336,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(
@@ -1519,13 +1522,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
+    PRECONDITION(false);
+
   add_guarded_property(
     notequal_exprt{expr.op(), from_integer(0, expr.op().type())},
-    "count leading zeros argument",
+    "count " + name + " zeros is undefined for value zero",
     "bit count",
     expr.find_source_location(),
     expr,
@@ -1788,7 +1800,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

@@ -2727,6 +2727,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

@@ -3822,6 +3822,7 @@ optionalt<std::string> expr2ct::convert_function(const exprt &src)
     {ID_complex_real, "__real__"},
     {ID_concatenation, "CONCATENATION"},
     {ID_count_leading_zeros, "__builtin_clz"},
+    {ID_count_trailing_zeros, "__builtin_ctz"},
     {ID_dynamic_object, "DYNAMIC_OBJECT"},
     {ID_floatbv_div, "FLOAT/"},
     {ID_floatbv_minus, "FLOAT-"},

src/solvers/flattening/boolbv.cpp

@@ -218,6 +218,11 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
     return convert_bv(
       simplify_expr(to_count_leading_zeros_expr(expr).lower(), ns));
   }
+  else if(expr.id() == ID_count_trailing_zeros)
+  {
+    return convert_bv(
+      simplify_expr(to_count_trailing_zeros_expr(expr).lower(), ns));
+  }
 
   return conversion_failed(expr);
 }

src/solvers/smt2/smt2_conv.cpp

@@ -2035,6 +2035,10 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     convert_expr(simplify_expr(to_count_leading_zeros_expr(expr).lower(), ns));
   }
+  else if(expr.id() == ID_count_trailing_zeros)
+  {
+    convert_expr(simplify_expr(to_count_trailing_zeros_expr(expr).lower(), ns));
+  }
   else
     INVARIANT_WITH_DIAGNOSTICS(
       false,

src/util/bitvector_expr.cpp

@@ -125,3 +125,20 @@ exprt count_leading_zeros_exprt::lower() const
     bitnot_exprt{typecast_exprt::conditional_cast(x, op().type())}, type()}
     .lower();
 }
+
+exprt count_trailing_zeros_exprt::lower() const
+{
+  exprt x = op();
+  const auto int_width = to_bitvector_type(x.type()).get_width();
+  CHECK_RETURN(int_width >= 1);
+
+  // 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{popcount.lower(), from_integer(1, x.type())};
+
+  return typecast_exprt::conditional_cast(result, type());
+}

src/util/bitvector_expr.h

@@ -825,7 +825,7 @@ inline unary_overflow_exprt &to_unary_overflow_expr(exprt &expr)
 /// \brief The count leading zeros (counting the number of zero bits starting
 /// from the most-significant bit) expression. When \c zero_permitted is set to
 /// false, goto_checkt must generate an assertion that the operand does not
-/// evaluates to zero. The result is always defined, even for zero (where the
+/// evaluate to zero. The result is always defined, even for zero (where the
 /// result is the bit width).
 class count_leading_zeros_exprt : public unary_exprt
 {
@@ -915,4 +915,97 @@ inline count_leading_zeros_exprt &to_count_leading_zeros_expr(exprt &expr)
   return ret;
 }
 
+/// \brief The count trailing zeros (counting the number of zero bits starting
+/// from the least-significant bit) expression. When \c zero_permitted is set to
+/// false, goto_checkt must generate an assertion that the operand does not
+/// evaluate to zero. The result is always defined, even for zero (where the
+/// result is the bit width).
+class count_trailing_zeros_exprt : public unary_exprt
+{
+public:
+  count_trailing_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
+    : unary_exprt(ID_count_trailing_zeros, std::move(_op), std::move(_type))
+  {
+    zero_permitted(_zero_permitted);
+  }
+
+  explicit count_trailing_zeros_exprt(const exprt &_op)
+    : count_trailing_zeros_exprt(_op, true, _op.type())
+  {
+  }
+
+  bool zero_permitted() const
+  {
+    return !get_bool(ID_C_bounds_check);
+  }
+
+  void zero_permitted(bool value)
+  {
+    set(ID_C_bounds_check, !value);
+  }
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      vm,
+      expr.operands().size() == 1,
+      "unary expression must have a single operand");
+    DATA_CHECK(
+      vm,
+      can_cast_type<bitvector_typet>(to_unary_expr(expr).op().type()),
+      "operand must be of bitvector type");
+  }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    check(expr, vm);
+  }
+
+  /// Lower a count_trailing_zeros_exprt to arithmetic and logic expressions.
+  /// \return Semantically equivalent expression
+  exprt lower() const;
+};
+
+template <>
+inline bool can_cast_expr<count_trailing_zeros_exprt>(const exprt &base)
+{
+  return base.id() == ID_count_trailing_zeros;
+}
+
+inline void validate_expr(const count_trailing_zeros_exprt &value)
+{
+  validate_operands(value, 1, "count_trailing_zeros must have one operand");
+}
+
+/// \brief Cast an exprt to a \ref count_trailing_zeros_exprt
+///
+/// \a expr must be known to be \ref count_trailing_zeros_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref count_trailing_zeros_exprt
+inline const count_trailing_zeros_exprt &
+to_count_trailing_zeros_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_count_trailing_zeros);
+  const count_trailing_zeros_exprt &ret =
+    static_cast<const count_trailing_zeros_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_count_trailing_zeros_expr(const exprt &)
+inline count_trailing_zeros_exprt &to_count_trailing_zeros_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_count_trailing_zeros);
+  count_trailing_zeros_exprt &ret =
+    static_cast<count_trailing_zeros_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_UTIL_BITVECTOR_EXPR_H