cprover
popcount.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Lowering of popcount
4 
5 Author: Michael Tautschnig
6 
7 \*******************************************************************/
8 
9 #include "expr_lowering.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/bitvector_expr.h>
13 #include <util/invariant.h>
15 #include <util/std_expr.h>
16 
18 {
19  // Hacker's Delight, variant pop0:
20  // x = (x & 0x55555555) + ((x >> 1) & 0x55555555);
21  // x = (x & 0x33333333) + ((x >> 2) & 0x33333333);
22  // x = (x & 0x0F0F0F0F) + ((x >> 4) & 0x0F0F0F0F);
23  // x = (x & 0x00FF00FF) + ((x >> 8) & 0x00FF00FF);
24  // etc.
25  // return x;
26  // http://www.hackersdelight.org/permissions.htm
27 
28  // make sure the operand width is a power of two
29  exprt x = expr.op();
30  const auto x_width = pointer_offset_bits(x.type(), ns);
31  CHECK_RETURN(x_width.has_value() && *x_width >= 1);
32  const std::size_t bits = address_bits(*x_width);
33  const std::size_t new_width = numeric_cast_v<std::size_t>(power(2, bits));
34 
35  const bool need_typecast =
36  new_width > *x_width || x.type().id() != ID_unsignedbv;
37 
38  if(need_typecast)
39  x = typecast_exprt(x, unsignedbv_typet(new_width));
40 
41  // repeatedly compute x = (x & bitmask) + ((x >> shift) & bitmask)
42  for(std::size_t shift = 1; shift < new_width; shift <<= 1)
43  {
44  // x >> shift
45  lshr_exprt shifted_x(
46  x, from_integer(shift, unsignedbv_typet(address_bits(shift) + 1)));
47  // bitmask is a string of alternating shift-many bits starting from lsb set
48  // to 1
49  std::string bitstring;
50  bitstring.reserve(new_width);
51  for(std::size_t i = 0; i < new_width / (2 * shift); ++i)
52  bitstring += std::string(shift, '0') + std::string(shift, '1');
53  const mp_integer value = binary2integer(bitstring, false);
54  const constant_exprt bitmask(integer2bvrep(value, new_width), x.type());
55  // build the expression
56  x = plus_exprt(bitand_exprt(x, bitmask), bitand_exprt(shifted_x, bitmask));
57  }
58 
59  // the result is restricted to the result type
60  return typecast_exprt(x, expr.type());
61 }
pointer_offset_size.h
Pointer Logic.
arith_tools.h
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
invariant.h
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:831
exprt
Base class for all expressions.
Definition: expr.h:54
lshr_exprt
Logical right shift.
Definition: bitvector_expr.h:348
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
expr_lowering.h
address_bits
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
Definition: arith_tools.cpp:176
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
integer2bvrep
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
Definition: arith_tools.cpp:379
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
irept::id
const irep_idt & id() const
Definition: irep.h:407
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:294
bitand_exprt
Bit-wise AND.
Definition: bitvector_expr.h:195
lower_popcount
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
Definition: popcount.cpp:17
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
binary2integer
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: bitvector_expr.h:633
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1781
constant_exprt
A constant literal expression.
Definition: std_expr.h:2668
std_expr.h
API to expression classes.
bitvector_expr.h
API to expression classes for bitvectors.