New expression: find_first_set_exprt

Rather than ad-hoc handling __builtin_ffs (and its variants) in the C
front-end, make find-first-set available across the code base.

Author: tautschnig

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

@@ -7,9 +7,11 @@ int __builtin_ffsl(long);
 int __builtin_ffsll(long long);
 #endif
 
+#ifdef _MSC_VER
+#  define _Static_assert(x, m) static_assert(x, m)
+#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] = {
@@ -18,14 +20,14 @@ static const int multiply_de_bruijn_bit_position[32] = {
 
 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);
+  _Static_assert(__builtin_ffs(0) == 0, "");
+  _Static_assert(__builtin_ffs(-1) == 1, "");
+  _Static_assert(__builtin_ffs(INT_MIN) == sizeof(int) * 8, "");
+  _Static_assert(__builtin_ffsl(INT_MIN) == sizeof(int) * 8, "");
+  _Static_assert(__builtin_ffsl(LONG_MIN) == sizeof(long) * 8, "");
+  _Static_assert(__builtin_ffsll(INT_MIN) == sizeof(int) * 8, "");
+  _Static_assert(__builtin_ffsll(LLONG_MIN) == sizeof(long long) * 8, "");
+  _Static_assert(__builtin_ffs(INT_MAX) == 1, "");
 
   int i = __VERIFIER_nondet_int();
   __CPROVER_assume(i != 0);

regression/cbmc-library/__builtin_ffs-01/test.desc renamed to regression/cbmc/__builtin_ffs-01/test.desc

@@ -82,7 +82,7 @@
 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 (183), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'arith_tools.h' not generated, too many nodes (184), 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.

scripts/expected_doxygen_warnings.txt

@@ -2698,6 +2698,24 @@ exprt c_typecheck_baset::do_special_functions(
 
     return clz;
   }
+  else if(
+    identifier == "__builtin_ffs" || identifier == "__builtin_ffsl" ||
+    identifier == "__builtin_ffsll")
+  {
+    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);
+
+    find_first_set_exprt ffs{expr.arguments().front(), expr.type()};
+    ffs.add_source_location() = source_location;
+
+    return ffs;
+  }
   else if(identifier==CPROVER_PREFIX "equal")
   {
     if(expr.arguments().size()!=2)

src/ansi-c/c_typecheck_expr.cpp

@@ -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/ansi-c/library/gcc.c

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

src/solvers/Makefile

@@ -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_find_first_set)
+    return convert_bv(lower_ffs(to_find_first_set_expr(expr), ns));
 
   return conversion_failed(expr);
 }

src/solvers/flattening/boolbv.cpp

@@ -14,6 +14,7 @@ Author: Michael Tautschnig
 class byte_extract_exprt;
 class byte_update_exprt;
 class count_leading_zeros_exprt;
+class find_first_set_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 find_first_set_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_ffs(const find_first_set_exprt &expr, const namespacet &ns);
+
 #endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */

src/solvers/lowering/expr_lowering.h

@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+Module: Lowering of find_first_set
+
+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_ffs(const find_first_set_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);
+
+  // bitwidth(x) - clz(x & ~((unsigned)x - 1));
+  const unsignedbv_typet ut{int_width};
+  minus_exprt minus_one{typecast_exprt::conditional_cast(x, ut),
+                        from_integer(1, ut)};
+  count_leading_zeros_exprt clz{bitand_exprt{
+    x, bitnot_exprt{typecast_exprt::conditional_cast(minus_one, x.type())}}};
+  minus_exprt result{from_integer(*x_width, x.type()), lower_clz(clz, ns)};
+  return simplify_expr(result, ns);
+}

src/solvers/lowering/find_first_set.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_find_first_set)
+  {
+    exprt lowered = lower_ffs(to_find_first_set_expr(expr), ns);
+    convert_expr(lowered);
+  }
   else
     INVARIANT_WITH_DIAGNOSTICS(
       false,

src/solvers/smt2/smt2_conv.cpp

@@ -766,4 +766,77 @@ inline count_leading_zeros_exprt &to_count_leading_zeros_expr(exprt &expr)
   return ret;
 }
 
+/// \brief Returns one plus the index of the least-significant one bit, or zero
+/// if the operand is zero.
+class find_first_set_exprt : public unary_exprt
+{
+public:
+  find_first_set_exprt(exprt _op, typet _type)
+    : unary_exprt(ID_find_first_set, std::move(_op), std::move(_type))
+  {
+  }
+
+  explicit find_first_set_exprt(const exprt &_op)
+    : find_first_set_exprt(_op, _op.type())
+  {
+  }
+
+  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<find_first_set_exprt>(const exprt &base)
+{
+  return base.id() == ID_find_first_set;
+}
+
+inline void validate_expr(const find_first_set_exprt &value)
+{
+  validate_operands(value, 1, "find_first_set must have one operand");
+}
+
+/// \brief Cast an exprt to a \ref find_first_set_exprt
+///
+/// \a expr must be known to be \ref find_first_set_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref find_first_set_exprt
+inline const find_first_set_exprt &to_find_first_set_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_find_first_set);
+  const find_first_set_exprt &ret =
+    static_cast<const find_first_set_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_find_first_set_expr(const exprt &)
+inline find_first_set_exprt &to_find_first_set_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_find_first_set);
+  find_first_set_exprt &ret = static_cast<find_first_set_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_UTIL_BITVECTOR_EXPR_H

src/util/bitvector_expr.h

@@ -843,6 +843,7 @@ IREP_ID_ONE(min)
 IREP_ID_ONE(constant_interval)
 IREP_ID_TWO(C_bounds_check, #bounds_check)
 IREP_ID_ONE(count_leading_zeros)
+IREP_ID_ONE(find_first_set)
 
 // 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

src/util/irep_ids.def

@@ -172,6 +172,25 @@ simplify_exprt::simplify_clz(const count_leading_zeros_exprt &expr)
   return from_integer(n_leading_zeros, expr.type());
 }
 
+simplify_exprt::resultt<>
+simplify_exprt::simplify_ffs(const find_first_set_exprt &expr)
+{
+  const auto const_bits_opt = expr2bits(
+    expr.op(), byte_extract_id() == ID_byte_extract_little_endian, ns);
+
+  if(!const_bits_opt.has_value())
+    return unchanged(expr);
+
+  // expr2bits generates a bit string starting with the least-significant bit
+  std::size_t first_one_bit = const_bits_opt->find('1');
+  if(first_one_bit == std::string::npos)
+    first_one_bit = 0;
+  else
+    ++first_one_bit;
+
+  return from_integer(first_one_bit, expr.type());
+}
+
 /// Simplify String.endsWith function when arguments are constant
 /// \param expr: the expression to simplify
 /// \param ns: namespace
@@ -2421,6 +2440,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
   {
     r = simplify_clz(to_count_leading_zeros_expr(expr));
   }
+  else if(expr.id() == ID_find_first_set)
+  {
+    r = simplify_ffs(to_find_first_set_expr(expr));
+  }
   else if(expr.id() == ID_function_application)
   {
     r = simplify_function_application(to_function_application_expr(expr));

src/util/simplify_expr.cpp

@@ -42,6 +42,7 @@ class div_exprt;
 class exprt;
 class extractbit_exprt;
 class extractbits_exprt;
+class find_first_set_exprt;
 class floatbv_typecast_exprt;
 class function_application_exprt;
 class ieee_float_op_exprt;
@@ -204,6 +205,9 @@ class simplify_exprt
   /// Try to simplify count-leading-zeros to a constant expression.
   NODISCARD resultt<> simplify_clz(const count_leading_zeros_exprt &);
 
+  /// Try to simplify find-first-set to a constant expression.
+  NODISCARD resultt<> simplify_ffs(const find_first_set_exprt &);
+
   // auxiliary
   bool simplify_if_implies(
     exprt &expr, const exprt &cond, bool truth, bool &new_truth);