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/invariant.h>
14 #include <util/std_expr.h>
15 
17 {
18  // Hacker's Delight, variant pop0:
19  // x = (x & 0x55555555) + ((x >> 1) & 0x55555555);
20  // x = (x & 0x33333333) + ((x >> 2) & 0x33333333);
21  // x = (x & 0x0F0F0F0F) + ((x >> 4) & 0x0F0F0F0F);
22  // x = (x & 0x00FF00FF) + ((x >> 8) & 0x00FF00FF);
23  // etc.
24  // return x;
25  // http://www.hackersdelight.org/permissions.htm
26 
27  // make sure the operand width is a power of two
28  exprt x = expr.op();
29  const mp_integer x_width = pointer_offset_bits(x.type(), ns);
30  CHECK_RETURN(x_width > 0);
31  const std::size_t bits = address_bits(x_width);
32  const std::size_t new_width = integer2size_t(power(2, bits));
33  const bool need_typecast =
34  new_width > x_width || x.type().id() != ID_unsignedbv;
35  if(need_typecast)
36  x.make_typecast(unsignedbv_typet(new_width));
37 
38  // repeatedly compute x = (x & bitmask) + ((x >> shift) & bitmask)
39  for(std::size_t shift = 1; shift < new_width; shift <<= 1)
40  {
41  // x >> shift
42  lshr_exprt shifted_x(
43  x, from_integer(shift, unsignedbv_typet(address_bits(shift) + 1)));
44  // bitmask is a string of alternating shift-many bits starting from lsb set
45  // to 1
46  std::string bitstring;
47  bitstring.reserve(new_width);
48  for(std::size_t i = 0; i < new_width / (2 * shift); ++i)
49  bitstring += std::string(shift, '0') + std::string(shift, '1');
50  constant_exprt bitmask(bitstring, x.type());
51  // build the expression
52  x = plus_exprt(bitand_exprt(x, bitmask), bitand_exprt(shifted_x, bitmask));
53  }
54 
55  // the result is restricted to the result type
56  x.make_typecast(expr.type());
57 
58  return x;
59 }
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1220
BigInt mp_integer
Definition: mp_arith.h:22
const exprt & op() const
Definition: std_expr.h:340
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
typet & type()
Definition: expr.h:56
A constant literal expression.
Definition: std_expr.h:4424
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
Definition: popcount.cpp:16
const irep_idt & id() const
Definition: irep.h:189
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
The plus expression.
Definition: std_expr.h:893
Logical right shift.
Definition: std_expr.h:2888
Pointer Logic.
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4890
Base class for all expressions.
Definition: expr.h:42
Bit-wise AND.
Definition: std_expr.h:2704
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void make_typecast(const typet &_type)
Definition: expr.cpp:84
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.