New expression: count_leading_zeros_exprt

Rather than ad-hoc handling __builtin_clz and __lzcnt (and their
variants) in the C front-end, make counting-leading-zeros available
across the code base.

Author: tautschnig

regression/ansi-c/__builtin_clz-02/main.c

@@ -0,0 +1,10 @@
+int main()
+{
+#ifdef __GNUC__
+  _Static_assert(
+    __builtin_clz(0xffU) == 8 * sizeof(unsigned) - 8,
+    "GCC/Clang compile-time constant");
+#endif
+
+  return 0;
+}

regression/cbmc-library/__builtin_clz-02/test.desc renamed to regression/ansi-c/__builtin_clz-02/test.desc

@@ -2689,27 +2689,22 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    side_effect_expr_function_callt try_constant{expr};
-    typecheck_function_call_arguments(try_constant);
-    exprt argument = try_constant.arguments().front();
-    simplify(argument, *this);
-    const auto int_constant = numeric_cast<mp_integer>(argument);
+    typecheck_function_call_arguments(expr);
+
+    exprt clz =
+      count_leading_zeros_exprt{expr.arguments().front(),
+                                has_prefix(id2string(identifier), "__lzcnt"),
+                                expr.type()};
+    clz.add_source_location() = source_location;
 
     if(
-      !int_constant.has_value() || *int_constant == 0 ||
-      argument.type().id() != ID_unsignedbv)
+      config.ansi_c.mode == configt::ansi_ct::flavourt::GCC ||
+      config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG)
     {
-      return nil_exprt{};
+      simplify(clz, *this);
     }
 
-    const std::string binary_value = integer2binary(
-      *int_constant, to_unsignedbv_type(argument.type()).get_width());
-    std::size_t n_leading_zeros = binary_value.find('1');
-    CHECK_RETURN(n_leading_zeros != std::string::npos);
-
-    return from_integer(
-      n_leading_zeros,
-      to_code_type(try_constant.function().type()).return_type());
+    return clz;
   }
   else if(identifier==CPROVER_PREFIX "equal")
   {

regression/cbmc-library/__builtin_clz-02/main.c

@@ -33,64 +33,6 @@ inline void __sync_synchronize(void)
   #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);
-}
-
 /* FUNCTION: __builtin_ffs */
 
 int __builtin_clz(unsigned int x);

regression/cbmc-library/__builtin_clz-01/main.c renamed to regression/cbmc/__builtin_clz-01/main.c

@@ -51,46 +51,3 @@ 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

src/ansi-c/c_typecheck_expr.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_convert_class.h"
 
+#include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/cprover_prefix.h>
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
@@ -100,6 +102,13 @@ bool goto_convertt::needs_cleaning(const exprt &expr)
   if(expr.id()==ID_forall || expr.id()==ID_exists)
     return false;
 
+  if(
+    expr.id() == ID_count_leading_zeros &&
+    !to_count_leading_zeros_expr(expr).zero_permitted())
+  {
+    return true;
+  }
+
   forall_operands(it, expr)
     if(needs_cleaning(*it))
       return true;
@@ -429,6 +438,22 @@ void goto_convertt::clean_expr(
       expr.operands().size() == 1, "ID_compound_literal has a single operand");
     expr = to_unary_expr(expr).op();
   }
+  else if(expr.id() == ID_count_leading_zeros)
+  {
+    count_leading_zeros_exprt &clz = to_count_leading_zeros_expr(expr);
+    if(!clz.zero_permitted())
+    {
+      clz.zero_permitted(true);
+      const source_locationt source_location = clz.source_location();
+
+      exprt nondet = side_effect_expr_nondett{expr.type(), source_location};
+      remove_side_effect(to_side_effect_expr(nondet), dest, mode, true, false);
+
+      expr = if_exprt{
+        equal_exprt{clz.op(), from_integer(0, clz.op().type())}, nondet, clz};
+      expr.add_source_location() = source_location;
+    }
+  }
 }
 
 void goto_convertt::clean_expr_address_of(

src/ansi-c/library/gcc.c

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

src/ansi-c/library/windows.c

@@ -228,6 +228,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
      return convert_power(to_binary_expr(expr));
   else if(expr.id() == ID_popcount)
     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));
 
   return conversion_failed(expr);
 }

src/goto-programs/goto_clean_expr.cpp

@@ -13,6 +13,7 @@ Author: Michael Tautschnig
 
 class byte_extract_exprt;
 class byte_update_exprt;
+class count_leading_zeros_exprt;
 class namespacet;
 class popcount_exprt;
 
@@ -50,4 +51,10 @@ bool has_byte_operator(const exprt &src);
 /// \return Semantically equivalent expression
 exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns);
 
+/// Lower a count_leading_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_clz(const count_leading_zeros_exprt &expr, const namespacet &ns);
+
 #endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */

src/solvers/Makefile

@@ -1987,6 +1987,11 @@ void smt2_convt::convert_expr(const exprt &expr)
     exprt lowered = lower_popcount(to_popcount_expr(expr), ns);
     convert_expr(lowered);
   }
+  else if(expr.id() == ID_count_leading_zeros)
+  {
+    exprt lowered = lower_clz(to_count_leading_zeros_expr(expr), ns);
+    convert_expr(lowered);
+  }
   else
     INVARIANT_WITH_DIAGNOSTICS(
       false,

src/solvers/flattening/boolbv.cpp

@@ -677,4 +677,92 @@ inline popcount_exprt &to_popcount_expr(exprt &expr)
   return ret;
 }
 
+/// \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, the result is non-deterministic when the operand is evaluates to
+/// zero.
+class count_leading_zeros_exprt : public unary_exprt
+{
+public:
+  count_leading_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
+    : unary_exprt(ID_count_leading_zeros, std::move(_op), std::move(_type))
+  {
+    zero_permitted(_zero_permitted);
+  }
+
+  explicit count_leading_zeros_exprt(const exprt &_op)
+    : count_leading_zeros_exprt(_op, true, _op.type())
+  {
+  }
+
+  bool zero_permitted() const
+  {
+    return get_bool(ID_zero_permitted);
+  }
+
+  void zero_permitted(bool value)
+  {
+    set(ID_zero_permitted, 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);
+  }
+};
+
+template <>
+inline bool can_cast_expr<count_leading_zeros_exprt>(const exprt &base)
+{
+  return base.id() == ID_count_leading_zeros;
+}
+
+inline void validate_expr(const count_leading_zeros_exprt &value)
+{
+  validate_operands(value, 1, "count_leading_zeros must have one operand");
+}
+
+/// \brief Cast an exprt to a \ref count_leading_zeros_exprt
+///
+/// \a expr must be known to be \ref count_leading_zeros_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref count_leading_zeros_exprt
+inline const count_leading_zeros_exprt &
+to_count_leading_zeros_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_count_leading_zeros);
+  const count_leading_zeros_exprt &ret =
+    static_cast<const count_leading_zeros_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_count_leading_zeros_expr(const exprt &)
+inline count_leading_zeros_exprt &to_count_leading_zeros_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_count_leading_zeros);
+  count_leading_zeros_exprt &ret =
+    static_cast<count_leading_zeros_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_UTIL_BITVECTOR_EXPR_H

src/solvers/lowering/expr_lowering.h

@@ -841,6 +841,8 @@ IREP_ID_ONE(statement_list_instructions)
 IREP_ID_ONE(max)
 IREP_ID_ONE(min)
 IREP_ID_ONE(constant_interval)
+IREP_ID_ONE(count_leading_zeros)
+IREP_ID_ONE(zero_permitted)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree