cprover
Loading...
Searching...
No Matches
bitvector_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes for bitvectors
4
5Author: 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
23extractbit_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 _index,
34 typet _type)
35 : expr_protectedt(ID_extractbits, std::move(_type))
36{
37 add_to_operands(std::move(_src), from_integer(_index, integer_typet()));
38}
39
41{
42 const auto width = to_bitvector_type(type()).get_width();
43 auto src_bv_type = bv_typet(width);
44
45 // build a mask 0...0 1
46 auto mask_bv =
47 make_bvrep(width, [](std::size_t index) { return index == 0; });
48 auto mask_expr = constant_exprt(mask_bv, src_bv_type);
49
50 // shift the mask by the index
51 auto mask_shifted = shl_exprt(mask_expr, index());
52
53 auto src_masked = bitand_exprt(
54 typecast_exprt(src(), src_bv_type), bitnot_exprt(mask_shifted));
55
56 // zero-extend the replacement bit to match src
57 auto new_value_casted = typecast_exprt(
58 typecast_exprt(new_value(), unsignedbv_typet(width)), src_bv_type);
59
60 // shift the replacement bits
61 auto new_value_shifted = shl_exprt(new_value_casted, index());
62
63 // or the masked src and the shifted replacement bits
64 return typecast_exprt(
65 bitor_exprt(src_masked, new_value_shifted), src().type());
66}
67
69{
70 const auto width = to_bitvector_type(type()).get_width();
71 const auto new_value_width =
73 auto src_bv_type = bv_typet(width);
74
75 // build a mask 1...1 0...0
76 auto mask_bv = make_bvrep(width, [new_value_width](std::size_t index) {
77 return index >= new_value_width;
78 });
79 auto mask_expr = constant_exprt(mask_bv, src_bv_type);
80
81 // shift the mask by the index
82 auto mask_shifted = shl_exprt(mask_expr, index());
83
84 auto src_masked =
85 bitand_exprt(typecast_exprt(src(), src_bv_type), mask_shifted);
86
87 // zero-extend or shrink the replacement bits to match src
88 auto new_value_casted = typecast_exprt(new_value(), src_bv_type);
89
90 // shift the replacement bits
91 auto new_value_shifted = shl_exprt(new_value_casted, index());
92
93 // or the masked src and the shifted replacement bits
94 return typecast_exprt(
95 bitor_exprt(src_masked, new_value_shifted), src().type());
96}
97
99{
100 // Hacker's Delight, variant pop0:
101 // x = (x & 0x55555555) + ((x >> 1) & 0x55555555);
102 // x = (x & 0x33333333) + ((x >> 2) & 0x33333333);
103 // x = (x & 0x0F0F0F0F) + ((x >> 4) & 0x0F0F0F0F);
104 // x = (x & 0x00FF00FF) + ((x >> 8) & 0x00FF00FF);
105 // etc.
106 // return x;
107 // http://www.hackersdelight.org/permissions.htm
108
109 // make sure the operand width is a power of two
110 exprt x = op();
111 const auto x_width = to_bitvector_type(x.type()).get_width();
112 CHECK_RETURN(x_width >= 1);
113 const std::size_t bits = address_bits(x_width);
114 const std::size_t new_width = numeric_cast_v<std::size_t>(power(2, bits));
115
116 const bool need_typecast =
117 new_width > x_width || x.type().id() != ID_unsignedbv;
118
119 if(need_typecast)
120 x = typecast_exprt(x, unsignedbv_typet(new_width));
121
122 // repeatedly compute x = (x & bitmask) + ((x >> shift) & bitmask)
123 for(std::size_t shift = 1; shift < new_width; shift <<= 1)
124 {
125 // x >> shift
126 lshr_exprt shifted_x(
127 x, from_integer(shift, unsignedbv_typet(address_bits(shift) + 1)));
128 // bitmask is a string of alternating shift-many bits starting from lsb set
129 // to 1
130 std::string bitstring;
131 bitstring.reserve(new_width);
132 for(std::size_t i = 0; i < new_width / (2 * shift); ++i)
133 bitstring += std::string(shift, '0') + std::string(shift, '1');
134 const mp_integer value = binary2integer(bitstring, false);
135 const constant_exprt bitmask(integer2bvrep(value, new_width), x.type());
136 // build the expression
137 x = plus_exprt(bitand_exprt(x, bitmask), bitand_exprt(shifted_x, bitmask));
138 }
139
140 // the result is restricted to the result type
142}
143
145{
146 // x = x | (x >> 1);
147 // x = x | (x >> 2);
148 // x = x | (x >> 4);
149 // x = x | (x >> 8);
150 // etc.
151 // return popcount(~x);
152
153 // make sure the operand width is a power of two
154 exprt x = op();
155 const auto x_width = to_bitvector_type(x.type()).get_width();
156 CHECK_RETURN(x_width >= 1);
157 const std::size_t bits = address_bits(x_width);
158 const std::size_t new_width = numeric_cast_v<std::size_t>(power(2, bits));
159
160 const bool need_typecast =
161 new_width > x_width || x.type().id() != ID_unsignedbv;
162
163 if(need_typecast)
164 x = typecast_exprt(x, unsignedbv_typet(new_width));
165
166 // repeatedly compute x = x | (x >> shift)
167 for(std::size_t shift = 1; shift < new_width; shift <<= 1)
168 {
169 // x >> shift
170 lshr_exprt shifted_x(
171 x, from_integer(shift, unsignedbv_typet(address_bits(shift) + 1)));
172 // build the expression
173 x = bitor_exprt{x, shifted_x};
174 }
175
176 // the result is restricted to the result type
177 return popcount_exprt{
179 .lower();
180}
181
183{
184 exprt x = op();
185
186 // popcount(~(x | (~x + 1)))
187 // compute -x using two's complement
188 plus_exprt minus_x{bitnot_exprt{x}, from_integer(1, x.type())};
189 bitor_exprt x_or_minus_x{x, std::move(minus_x)};
190 popcount_exprt popcount{bitnot_exprt{std::move(x_or_minus_x)}};
191
192 return typecast_exprt::conditional_cast(popcount.lower(), type());
193}
194
196{
197 const std::size_t int_width = to_bitvector_type(type()).get_width();
198
199 exprt::operandst result_bits;
200 result_bits.reserve(int_width);
201
202 const symbol_exprt to_reverse("to_reverse", op().type());
203 for(std::size_t i = 0; i < int_width; ++i)
204 result_bits.push_back(extractbit_exprt{to_reverse, i});
205
206 return let_exprt{to_reverse, op(), concatenation_exprt{result_bits, type()}};
207}
208
210{
211 std::size_t lhs_ssize = to_bitvector_type(lhs().type()).get_width();
212 if(lhs().type().id() == ID_unsignedbv)
213 ++lhs_ssize;
214 std::size_t rhs_ssize = to_bitvector_type(rhs().type()).get_width();
215 if(rhs().type().id() == ID_unsignedbv)
216 ++rhs_ssize;
217
218 std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
219 signedbv_typet ssize_type{ssize};
220 plus_exprt exact_result{
221 typecast_exprt{lhs(), ssize_type}, typecast_exprt{rhs(), ssize_type}};
222
223 return notequal_exprt{
224 typecast_exprt{typecast_exprt{exact_result, lhs().type()}, ssize_type},
225 exact_result};
226}
227
229{
230 std::size_t lhs_ssize = to_bitvector_type(lhs().type()).get_width();
231 if(lhs().type().id() == ID_unsignedbv)
232 ++lhs_ssize;
233 std::size_t rhs_ssize = to_bitvector_type(rhs().type()).get_width();
234 if(rhs().type().id() == ID_unsignedbv)
235 ++rhs_ssize;
236
237 std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
238 signedbv_typet ssize_type{ssize};
239 minus_exprt exact_result{
240 typecast_exprt{lhs(), ssize_type}, typecast_exprt{rhs(), ssize_type}};
241
242 return notequal_exprt{
243 typecast_exprt{typecast_exprt{exact_result, lhs().type()}, ssize_type},
244 exact_result};
245}
246
248{
249 std::size_t lhs_ssize = to_bitvector_type(lhs().type()).get_width();
250 if(lhs().type().id() == ID_unsignedbv)
251 ++lhs_ssize;
252 std::size_t rhs_ssize = to_bitvector_type(rhs().type()).get_width();
253 if(rhs().type().id() == ID_unsignedbv)
254 ++rhs_ssize;
255
256 std::size_t ssize = lhs_ssize + rhs_ssize;
257 signedbv_typet ssize_type{ssize};
258 mult_exprt exact_result{
259 typecast_exprt{lhs(), ssize_type}, typecast_exprt{rhs(), ssize_type}};
260
261 return notequal_exprt{
262 typecast_exprt{typecast_exprt{exact_result, lhs().type()}, ssize_type},
263 exact_result};
264}
265
267{
268 exprt x = op();
269 const auto int_width = to_bitvector_type(x.type()).get_width();
270 CHECK_RETURN(int_width >= 1);
271
272 // bitwidth(x) - clz(x & ~((unsigned)x - 1));
273 const unsignedbv_typet ut{int_width};
274 minus_exprt minus_one{
278 minus_exprt result{from_integer(int_width, x.type()), clz.lower()};
279
280 return typecast_exprt::conditional_cast(result, type());
281}
irep_idt make_bvrep(const std::size_t width, const std::function< bool(std::size_t)> f)
construct a bit-vector representation from a functor
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
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.
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
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:638
exprt & lhs()
Definition std_expr.h:668
exprt & rhs()
Definition std_expr.h:678
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:731
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:920
Fixed-width bit-vector without numerical interpretation.
Concatenation of bit-vector operands.
A constant literal expression.
Definition std_expr.h:2987
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
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:38
Base class for all expressions.
Definition expr.h:344
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
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 _index, typet _type)
Extract the bits [_index .
exprt lower() const
Lower a find_first_set_exprt to arithmetic and logic expressions.
Unbounded, signed integers (mathematical integers, not bitvectors)
const irep_idt & id() const
Definition irep.h:388
A let expression.
Definition std_expr.h:3196
Logical right shift.
Binary minus.
Definition std_expr.h:1061
exprt lower() const
Lower a minus_overflow_exprt to arithmetic and logic expressions.
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
exprt lower() const
Lower a mult_overflow_exprt to arithmetic and logic expressions.
Disequality.
Definition std_expr.h:1420
The plus expression Associativity is not specified.
Definition std_expr.h:1002
exprt lower() const
Lower a plus_overflow_exprt to arithmetic and logic expressions.
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)
Left shift.
Fixed-width bit-vector with two's complement interpretation.
Expression to hold a symbol (variable)
Definition std_expr.h:131
Semantic type conversion.
Definition std_expr.h:2068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2076
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:391
Fixed-width bit-vector with unsigned binary interpretation.
exprt lower() const
A lowering to masking, shifting, or.
exprt lower() const
A lowering to masking, shifting, or.
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
STL namespace.
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495