cprover
bitvector_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes for bitvectors
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "bitvector_expr.h"
10 
11 #include "arith_tools.h"
12 #include "bitvector_types.h"
13 #include "mathematical_types.h"
14 
16  exprt _src,
17  const irep_idt &_id,
18  const std::size_t _distance)
19  : binary_exprt(std::move(_src), _id, from_integer(_distance, integer_typet()))
20 {
21 }
22 
23 extractbit_exprt::extractbit_exprt(exprt _src, const std::size_t _index)
25  std::move(_src),
26  ID_extractbit,
27  from_integer(_index, integer_typet()))
28 {
29 }
30 
32  exprt _src,
33  const std::size_t _upper,
34  const std::size_t _lower,
35  typet _type)
36  : expr_protectedt(ID_extractbits, std::move(_type))
37 {
38  PRECONDITION(_upper >= _lower);
40  std::move(_src),
41  from_integer(_upper, integer_typet()),
42  from_integer(_lower, integer_typet()));
43 }
44 
46 {
47  // Hacker's Delight, variant pop0:
48  // x = (x & 0x55555555) + ((x >> 1) & 0x55555555);
49  // x = (x & 0x33333333) + ((x >> 2) & 0x33333333);
50  // x = (x & 0x0F0F0F0F) + ((x >> 4) & 0x0F0F0F0F);
51  // x = (x & 0x00FF00FF) + ((x >> 8) & 0x00FF00FF);
52  // etc.
53  // return x;
54  // http://www.hackersdelight.org/permissions.htm
55 
56  // make sure the operand width is a power of two
57  exprt x = op();
58  const auto x_width = to_bitvector_type(x.type()).get_width();
59  CHECK_RETURN(x_width >= 1);
60  const std::size_t bits = address_bits(x_width);
61  const std::size_t new_width = numeric_cast_v<std::size_t>(power(2, bits));
62 
63  const bool need_typecast =
64  new_width > x_width || x.type().id() != ID_unsignedbv;
65 
66  if(need_typecast)
67  x = typecast_exprt(x, unsignedbv_typet(new_width));
68 
69  // repeatedly compute x = (x & bitmask) + ((x >> shift) & bitmask)
70  for(std::size_t shift = 1; shift < new_width; shift <<= 1)
71  {
72  // x >> shift
73  lshr_exprt shifted_x(
74  x, from_integer(shift, unsignedbv_typet(address_bits(shift) + 1)));
75  // bitmask is a string of alternating shift-many bits starting from lsb set
76  // to 1
77  std::string bitstring;
78  bitstring.reserve(new_width);
79  for(std::size_t i = 0; i < new_width / (2 * shift); ++i)
80  bitstring += std::string(shift, '0') + std::string(shift, '1');
81  const mp_integer value = binary2integer(bitstring, false);
82  const constant_exprt bitmask(integer2bvrep(value, new_width), x.type());
83  // build the expression
84  x = plus_exprt(bitand_exprt(x, bitmask), bitand_exprt(shifted_x, bitmask));
85  }
86 
87  // the result is restricted to the result type
89 }
90 
92 {
93  // x = x | (x >> 1);
94  // x = x | (x >> 2);
95  // x = x | (x >> 4);
96  // x = x | (x >> 8);
97  // etc.
98  // return popcount(~x);
99 
100  // make sure the operand width is a power of two
101  exprt x = op();
102  const auto x_width = to_bitvector_type(x.type()).get_width();
103  CHECK_RETURN(x_width >= 1);
104  const std::size_t bits = address_bits(x_width);
105  const std::size_t new_width = numeric_cast_v<std::size_t>(power(2, bits));
106 
107  const bool need_typecast =
108  new_width > x_width || x.type().id() != ID_unsignedbv;
109 
110  if(need_typecast)
111  x = typecast_exprt(x, unsignedbv_typet(new_width));
112 
113  // repeatedly compute x = x | (x >> shift)
114  for(std::size_t shift = 1; shift < new_width; shift <<= 1)
115  {
116  // x >> shift
117  lshr_exprt shifted_x(
118  x, from_integer(shift, unsignedbv_typet(address_bits(shift) + 1)));
119  // build the expression
120  x = bitor_exprt{x, shifted_x};
121  }
122 
123  // the result is restricted to the result type
124  return popcount_exprt{
126  .lower();
127 }
128 
130 {
131  exprt x = op();
132  const auto int_width = to_bitvector_type(x.type()).get_width();
133  CHECK_RETURN(int_width >= 1);
134 
135  // popcount(x ^ ((unsigned)x - 1)) - 1
136  const unsignedbv_typet ut{int_width};
138  from_integer(1, ut)};
139  popcount_exprt popcount{
141  minus_exprt result{popcount.lower(), from_integer(1, x.type())};
142 
143  return typecast_exprt::conditional_cast(result, type());
144 }
145 
147 {
148  const std::size_t int_width = to_bitvector_type(type()).get_width();
149 
150  exprt::operandst result_bits;
151  result_bits.reserve(int_width);
152 
153  const symbol_exprt to_reverse("to_reverse", op().type());
154  for(std::size_t i = 0; i < int_width; ++i)
155  result_bits.push_back(extractbit_exprt{to_reverse, i});
156 
157  return let_exprt{to_reverse, op(), concatenation_exprt{result_bits, type()}};
158 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
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...
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
API to expression classes for bitvectors.
Pre-defined bitvector types.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
A base class for binary expressions.
Definition: std_expr.h:550
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
Bit-wise AND.
Bit-wise negation of bit-vectors.
Bit-wise OR.
exprt lower() const
Lower a bitreverse_exprt to arithmetic and logic expressions.
std::size_t get_width() const
Definition: std_types.h:864
Bit-wise XOR.
Concatenation of bit-vector operands.
A constant literal expression.
Definition: std_expr.h:2807
exprt lower() const
Lower a count_leading_zeros_exprt to arithmetic and logic expressions.
exprt lower() const
Lower a count_trailing_zeros_exprt to arithmetic and logic expressions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:343
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
Extracts a single bit of a bit-vector operand.
extractbit_exprt(exprt _src, exprt _index)
Extract the _index-th least significant bit from _src.
extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
Extract the bits [_lower .
Unbounded, signed integers (mathematical integers, not bitvectors)
const irep_idt & id() const
Definition: irep.h:396
A let expression.
Definition: std_expr.h:2973
Logical right shift.
Binary minus.
Definition: std_expr.h:973
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The popcount (counting the number of bits set to 1) expression.
exprt lower() const
Lower a popcount_exprt to arithmetic and logic expressions.
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
Fixed-width bit-vector with unsigned binary interpretation.
Mathematical types.
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:117
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463