CBMC: /home/runner/work/cbmc/cbmc/src/util/bitvector_expr.cpp Source File

CBMC
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)
20{
21}
22
30
32 exprt _src,
33 const std::size_t _index,
34 typet _type)
35 : expr_protectedt(ID_extractbits, std::move(_type))
36{
38}
39
41 exprt _src,
42 const std::size_t _index,
45 std::move(_src),
47 std::move(_new_value))
48{
49}
50
52{
53 const auto width = to_bitvector_type(type()).get_width();
54 auto src_bv_type = bv_typet(width);
55
56 // build a mask 0...0 1
57 auto mask_bv =
58 make_bvrep(width, [](std::size_t index) { return index == 0; });
60
61 // shift the mask by the index
63
66
67 // zero-extend the replacement bit to match src
70
71 // shift the replacement bits
73
74 // or the masked src and the shifted replacement bits
75 return typecast_exprt(
77}
78
80{
81 const auto width = to_bitvector_type(type()).get_width();
82 const auto new_value_width =
83 to_bitvector_type(new_value().type()).get_width();
84 auto src_bv_type = bv_typet(width);
85
86 // build a mask 1...1 0...0
87 auto mask_bv = make_bvrep(width, [new_value_width](std::size_t index) {
88 return index >= new_value_width;
89 });
91
92 // shift the mask by the index
94
95 auto src_masked =
97
98 // zero-extend or shrink the replacement bits to match src
100
101 // shift the replacement bits
103
104 // or the masked src and the shifted replacement bits
105 return typecast_exprt(
107}
108
110{
111 // Hacker's Delight, variant pop0:
112 // x = (x & 0x55555555) + ((x >> 1) & 0x55555555);
113 // x = (x & 0x33333333) + ((x >> 2) & 0x33333333);
114 // x = (x & 0x0F0F0F0F) + ((x >> 4) & 0x0F0F0F0F);
115 // x = (x & 0x00FF00FF) + ((x >> 8) & 0x00FF00FF);
116 // etc.
117 // return x;
118 // http://www.hackersdelight.org/permissions.htm
119
120 // make sure the operand width is a power of two
121 exprt x = op();
122 const auto x_width = to_bitvector_type(x.type()).get_width();
123 CHECK_RETURN(x_width >= 1);
124 const std::size_t bits = address_bits(x_width);
125 const std::size_t new_width = numeric_cast_v<std::size_t>(power(2, bits));
126
127 const bool need_typecast =
128 new_width > x_width || x.type().id() != ID_unsignedbv;
129
130 if(need_typecast)
132
133 // repeatedly compute x = (x & bitmask) + ((x >> shift) & bitmask)
134 for(std::size_t shift = 1; shift < new_width; shift <<= 1)
135 {
136 // x >> shift
138 x, from_integer(shift, unsignedbv_typet(address_bits(shift) + 1)));
139 // bitmask is a string of alternating shift-many bits starting from lsb set
140 // to 1
141 std::string bitstring;
142 bitstring.reserve(new_width);
143 for(std::size_t i = 0; i < new_width / (2 * shift); ++i)
144 bitstring += std::string(shift, '0') + std::string(shift, '1');
145 const mp_integer value = binary2integer(bitstring, false);
146 const constant_exprt bitmask(integer2bvrep(value, new_width), x.type());
147 // build the expression
149 }
150
151 // the result is restricted to the result type
153}
154
156{
157 // x = x | (x >> 1);
158 // x = x | (x >> 2);
159 // x = x | (x >> 4);
160 // x = x | (x >> 8);
161 // etc.
162 // return popcount(~x);
163
164 // make sure the operand width is a power of two
165 exprt x = op();
166 const auto x_width = to_bitvector_type(x.type()).get_width();
167 CHECK_RETURN(x_width >= 1);
168 const std::size_t bits = address_bits(x_width);
169 const std::size_t new_width = numeric_cast_v<std::size_t>(power(2, bits));
170
171 const bool need_typecast =
172 new_width > x_width || x.type().id() != ID_unsignedbv;
173
174 if(need_typecast)
176
177 // repeatedly compute x = x | (x >> shift)
178 for(std::size_t shift = 1; shift < new_width; shift <<= 1)
179 {
180 // x >> shift
182 x, from_integer(shift, unsignedbv_typet(address_bits(shift) + 1)));
183 // build the expression
185 }
186
187 // the result is restricted to the result type
188 return popcount_exprt{
190 .lower();
191}
192
194{
195 exprt x = op();
196
197 // popcount(~(x | (~x + 1)))
198 // compute -x using two's complement
200 bitor_exprt x_or_minus_x{x, std::move(minus_x)};
201 popcount_exprt popcount{bitnot_exprt{std::move(x_or_minus_x)}};
202
203 return typecast_exprt::conditional_cast(popcount.lower(), type());
204}
205
207{
208 const std::size_t int_width = to_bitvector_type(type()).get_width();
209
211 result_bits.reserve(int_width);
212
213 const symbol_exprt to_reverse("to_reverse", op().type());
214 for(std::size_t i = 0; i < int_width; ++i)
215 result_bits.push_back(extractbit_exprt{to_reverse, i});
216
218}
219
221{
222 std::size_t lhs_ssize = to_bitvector_type(lhs().type()).get_width();
223 if(lhs().type().id() == ID_unsignedbv)
224 ++lhs_ssize;
225 std::size_t rhs_ssize = to_bitvector_type(rhs().type()).get_width();
226 if(rhs().type().id() == ID_unsignedbv)
227 ++rhs_ssize;
228
229 std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
233
234 return notequal_exprt{
237}
238
240{
241 std::size_t lhs_ssize = to_bitvector_type(lhs().type()).get_width();
242 if(lhs().type().id() == ID_unsignedbv)
243 ++lhs_ssize;
244 std::size_t rhs_ssize = to_bitvector_type(rhs().type()).get_width();
245 if(rhs().type().id() == ID_unsignedbv)
246 ++rhs_ssize;
247
248 std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
252
253 return notequal_exprt{
256}
257
259{
260 std::size_t lhs_ssize = to_bitvector_type(lhs().type()).get_width();
261 if(lhs().type().id() == ID_unsignedbv)
262 ++lhs_ssize;
263 std::size_t rhs_ssize = to_bitvector_type(rhs().type()).get_width();
264 if(rhs().type().id() == ID_unsignedbv)
265 ++rhs_ssize;
266
267 std::size_t ssize = lhs_ssize + rhs_ssize;
271
272 return notequal_exprt{
275}
276
278{
279 exprt x = op();
280 const auto int_width = to_bitvector_type(x.type()).get_width();
281 CHECK_RETURN(int_width >= 1);
282
283 // bitwidth(x) - clz(x & ~((unsigned)x - 1));
284 const unsignedbv_typet ut{int_width};
289 minus_exprt result{from_integer(int_width, x.type()), clz.lower()};
290
291 return typecast_exprt::conditional_cast(result, type());
292}
293
295{
296 const auto old_width = to_bitvector_type(op().type()).get_width();
297 const auto new_width = to_bitvector_type(type()).get_width();
298
299 if(new_width > old_width)
300 {
301 return concatenation_exprt{
302 bv_typet{new_width - old_width}.all_zeros_expr(), op(), type()};
303 }
304 else // new_width <= old_width
305 {
306 return extractbits_exprt{op(), 0, type()};
307 }
308}
309
310 static exprt onehot_lowering(const exprt &expr)
311{
313 const auto width = to_bitvector_type(expr.type()).get_width();
315 more_than_one_seen_disjuncts.reserve(width);
316
317 for(std::size_t i = 0; i < width; i++)
318 {
319 auto bit = extractbit_exprt{expr, i};
322 }
323
325
327}
328
330{
331 auto symbol = symbol_exprt{"onehot-op", op().type()};
332
333 return let_exprt{symbol, op(), onehot_lowering(symbol)};
334}
335
337{
338 auto symbol = symbol_exprt{"onehot-op", op().type()};
339
340 // same as onehot, but on flipped operand bits
341 return let_exprt{symbol, bitnot_exprt{op()}, onehot_lowering(symbol)};
342}
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.
static exprt onehot_lowering(const exprt &expr)
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Boolean AND All operands must be boolean, and the result is always boolean.
Definition std_expr.h:2043
A base class for binary expressions.
Definition std_expr.h:649
exprt & lhs()
Definition std_expr.h:679
exprt & rhs()
Definition std_expr.h:689
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:737
Bit-wise AND Any number of operands that is greater or equal one.
Bit-wise negation of bit-vectors.
Bit-wise OR Any number of operands that is greater or equal one.
exprt lower() const
Lower a bitreverse_exprt to arithmetic and logic expressions.
Fixed-width bit-vector without numerical interpretation.
Concatenation of bit-vector operands.
A constant literal expression.
Definition std_expr.h:3007
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:350
Base class for all expressions.
Definition expr.h:57
std::vector< exprt > operandst
Definition expr.h:59
typet & type()
Return the type of the expression.
Definition expr.h:85
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:171
Extracts a single bit of a bit-vector operand.
extractbit_exprt(exprt _src, exprt _index)
Extract the _index-th least significant bit from _src.
Extracts a sub-range of a bit-vector operand.
extractbits_exprt(exprt _src, exprt _index, typet _type)
Extract the bits [_index .
The Boolean constant false.
Definition std_expr.h:3135
exprt lower() const
Lower a find_first_set_exprt to arithmetic and logic expressions.
Unbounded, signed integers (mathematical integers, not bitvectors)
A let expression.
Definition std_expr.h:3259
Logical right shift.
Binary minus.
Definition std_expr.h:1065
exprt lower() const
Lower a minus_overflow_exprt to arithmetic and logic expressions.
Binary multiplication Associativity is not specified.
Definition std_expr.h:1104
exprt lower() const
Lower a mult_overflow_exprt to arithmetic and logic expressions.
Boolean negation.
Definition std_expr.h:2388
Disequality.
Definition std_expr.h:1393
exprt lower() const
lowering to extractbit
exprt lower() const
lowering to extractbit
Boolean OR All operands must be boolean, and the result is always boolean.
Definition std_expr.h:2193
The plus expression Associativity is not specified.
Definition std_expr.h:1006
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:132
Semantic type conversion.
Definition std_expr.h:1995
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2003
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:394
Fixed-width bit-vector with unsigned binary interpretation.
Replaces a sub-range of a bit-vector operand.
exprt & src()
update_bit_exprt(exprt _src, exprt _index, exprt _new_value)
Replaces the bit [_index] from _src to produce a result of the same type as _src.
exprt & new_value()
exprt lower() const
A lowering to masking, shifting, or.
exprt & index()
exprt & new_value()
exprt & src()
exprt lower() const
A lowering to masking, shifting, or.
exprt & index()
zero extension The operand is converted to the given type by either a) truncating if the new type is ...
exprt lower() const
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.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:240

AltStyle によって変換されたページ (->オリジナル) /