Make lower_popcount a method of popcount_exprt

Expression lowering may be useful well outside the solvers/ context.
Making it a method of the class being lowered also serves as a way of
describing the semantics of the expression.

This is mainly a refactoring, no changes in behaviour are intended.

Author: tautschnig

src/solvers/Makefile

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

src/solvers/flattening/boolbv.cpp

@@ -227,7 +227,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_power)
      return convert_power(to_binary_expr(expr));
   else if(expr.id() == ID_popcount)
-    return convert_bv(lower_popcount(to_popcount_expr(expr), ns));
+    return convert_bv(to_popcount_expr(expr).lower());
 
   return conversion_failed(expr);
 }

src/solvers/lowering/expr_lowering.h

@@ -14,7 +14,6 @@ Author: Michael Tautschnig
 class byte_extract_exprt;
 class byte_update_exprt;
 class namespacet;
-class popcount_exprt;
 
 /// Rewrite a byte extract expression to more fundamental operations.
 /// \param src: Byte extract expression
@@ -44,10 +43,4 @@ exprt lower_byte_operators(const exprt &src, const namespacet &ns);
 
 bool has_byte_operator(const exprt &src);
 
-/// Lower a popcount_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_popcount(const popcount_exprt &expr, const namespacet &ns);
-
 #endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */

src/solvers/lowering/popcount.cpp

@@ -1984,8 +1984,7 @@ void smt2_convt::convert_expr(const exprt &expr)
   }
   else if(expr.id() == ID_popcount)
   {
-    exprt lowered = lower_popcount(to_popcount_expr(expr), ns);
-    convert_expr(lowered);
+    convert_expr(to_popcount_expr(expr).lower());
   }
   else
     INVARIANT_WITH_DIAGNOSTICS(

src/solvers/smt2/smt2_conv.cpp

@@ -9,7 +9,11 @@ Author: Daniel Kroening, [email protected]
 #include "bitvector_expr.h"
 
 #include "arith_tools.h"
+#include "bitvector_types.h"
 #include "mathematical_types.h"
+#include "namespace.h"
+#include "simplify_expr.h"
+#include "symbol_table.h"
 
 shift_exprt::shift_exprt(
   exprt _src,
@@ -40,3 +44,52 @@ extractbits_exprt::extractbits_exprt(
     from_integer(_upper, integer_typet()),
     from_integer(_lower, integer_typet()));
 }
+
+exprt popcount_exprt::lower() const
+{
+  // Hacker's Delight, variant pop0:
+  // x = (x & 0x55555555) + ((x >> 1) & 0x55555555);
+  // x = (x & 0x33333333) + ((x >> 2) & 0x33333333);
+  // x = (x & 0x0F0F0F0F) + ((x >> 4) & 0x0F0F0F0F);
+  // x = (x & 0x00FF00FF) + ((x >> 8) & 0x00FF00FF);
+  // etc.
+  // return x;
+  // http://www.hackersdelight.org/permissions.htm
+
+  // make sure the operand width is a power of two
+  exprt x = op();
+  const auto x_width = to_bitvector_type(x.type()).get_width();
+  CHECK_RETURN(x_width >= 1);
+  const std::size_t bits = address_bits(x_width);
+  const std::size_t new_width = numeric_cast_v<std::size_t>(power(2, bits));
+
+  const bool need_typecast =
+    new_width > x_width || x.type().id() != ID_unsignedbv;
+
+  if(need_typecast)
+    x = typecast_exprt(x, unsignedbv_typet(new_width));
+
+  // repeatedly compute x = (x & bitmask) + ((x >> shift) & bitmask)
+  for(std::size_t shift = 1; shift < new_width; shift <<= 1)
+  {
+    // x >> shift
+    lshr_exprt shifted_x(
+      x, from_integer(shift, unsignedbv_typet(address_bits(shift) + 1)));
+    // bitmask is a string of alternating shift-many bits starting from lsb set
+    // to 1
+    std::string bitstring;
+    bitstring.reserve(new_width);
+    for(std::size_t i = 0; i < new_width / (2 * shift); ++i)
+      bitstring += std::string(shift, '0') + std::string(shift, '1');
+    const mp_integer value = binary2integer(bitstring, false);
+    const constant_exprt bitmask(integer2bvrep(value, new_width), x.type());
+    // build the expression
+    x = plus_exprt(bitand_exprt(x, bitmask), bitand_exprt(shifted_x, bitmask));
+  }
+
+  // the result is restricted to the result type and simplified; use a dummy
+  // symbol table here as there is no need for type lookups
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+  return simplify_expr(typecast_exprt{x, type()}, ns);
+}

src/util/bitvector_expr.cpp

@@ -641,6 +641,10 @@ class popcount_exprt : public unary_exprt
     : unary_exprt(ID_popcount, _op, _op.type())
   {
   }
+
+  /// Lower a popcount_exprt to arithmetic and logic expressions.
+  /// \return Semantically equivalent expression
+  exprt lower() const;
 };
 
 template <>