cprover
Loading...
Searching...
No Matches
arith_tools.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "arith_tools.h"
10
11#include "c_types.h"
12#include "fixedbv.h"
13#include "ieee_float.h"
14#include "invariant.h"
15#include "std_expr.h"
16
17#include <algorithm>
18
19bool to_integer(const constant_exprt &expr, mp_integer &int_value)
20{
21 const irep_idt &value=expr.get_value();
22 const typet &type=expr.type();
23 const irep_idt &type_id=type.id();
24
25 if(type_id==ID_pointer)
26 {
27 if(value==ID_NULL)
28 {
29 int_value=0;
30 return false;
31 }
32 }
33 else if(type_id==ID_integer ||
34 type_id==ID_natural)
35 {
36 int_value=string2integer(id2string(value));
37 return false;
38 }
39 else if(type_id==ID_unsignedbv)
40 {
41 const auto width = to_unsignedbv_type(type).get_width();
42 int_value = bvrep2integer(value, width, false);
43 return false;
44 }
45 else if(type_id==ID_signedbv)
46 {
47 const auto width = to_signedbv_type(type).get_width();
48 int_value = bvrep2integer(value, width, true);
49 return false;
50 }
51 else if(type_id==ID_c_bool)
52 {
53 const auto width = to_c_bool_type(type).get_width();
54 int_value = bvrep2integer(value, width, false);
55 return false;
56 }
57 else if(type_id==ID_c_enum)
58 {
59 const typet &underlying_type = to_c_enum_type(type).underlying_type();
60 if(underlying_type.id() == ID_signedbv)
61 {
62 const auto width = to_signedbv_type(type).get_width();
63 int_value = bvrep2integer(value, width, true);
64 return false;
65 }
66 else if(underlying_type.id() == ID_unsignedbv)
67 {
68 const auto width = to_unsignedbv_type(type).get_width();
69 int_value = bvrep2integer(value, width, false);
70 return false;
71 }
72 }
73 else if(type_id==ID_c_bit_field)
74 {
75 const auto &c_bit_field_type = to_c_bit_field_type(type);
76 const auto width = c_bit_field_type.get_width();
77 const typet &underlying_type = c_bit_field_type.underlying_type();
78
79 if(underlying_type.id() == ID_signedbv)
80 {
81 int_value = bvrep2integer(value, width, true);
82 return false;
83 }
84 else if(underlying_type.id() == ID_unsignedbv)
85 {
86 int_value = bvrep2integer(value, width, false);
87 return false;
88 }
89 else if(underlying_type.id() == ID_c_bool)
90 {
91 int_value = bvrep2integer(value, width, false);
92 return false;
93 }
94 }
95
96 return true;
97}
98
100 const mp_integer &int_value,
101 const typet &type)
102{
103 const irep_idt &type_id=type.id();
104
105 if(type_id==ID_integer)
106 {
107 return constant_exprt(integer2string(int_value), type);
108 }
109 else if(type_id==ID_natural)
110 {
111 PRECONDITION(int_value >= 0);
112 return constant_exprt(integer2string(int_value), type);
113 }
114 else if(type_id==ID_unsignedbv)
115 {
116 std::size_t width=to_unsignedbv_type(type).get_width();
117 return constant_exprt(integer2bvrep(int_value, width), type);
118 }
119 else if(type_id==ID_bv)
120 {
121 std::size_t width=to_bv_type(type).get_width();
122 return constant_exprt(integer2bvrep(int_value, width), type);
123 }
124 else if(type_id==ID_signedbv)
125 {
126 std::size_t width=to_signedbv_type(type).get_width();
127 return constant_exprt(integer2bvrep(int_value, width), type);
128 }
129 else if(type_id==ID_c_enum)
130 {
131 const std::size_t width =
132 to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width();
133 return constant_exprt(integer2bvrep(int_value, width), type);
134 }
135 else if(type_id==ID_c_bool)
136 {
137 std::size_t width=to_c_bool_type(type).get_width();
138 return constant_exprt(integer2bvrep(int_value, width), type);
139 }
140 else if(type_id==ID_bool)
141 {
142 PRECONDITION(int_value == 0 || int_value == 1);
143 if(int_value == 0)
144 return false_exprt();
145 else
146 return true_exprt();
147 }
148 else if(type_id==ID_pointer)
149 {
150 PRECONDITION(int_value == 0);
152 }
153 else if(type_id==ID_c_bit_field)
154 {
155 std::size_t width=to_c_bit_field_type(type).get_width();
156 return constant_exprt(integer2bvrep(int_value, width), type);
157 }
158 else if(type_id==ID_fixedbv)
159 {
160 fixedbvt fixedbv;
161 fixedbv.spec=fixedbv_spect(to_fixedbv_type(type));
162 fixedbv.from_integer(int_value);
163 return fixedbv.to_expr();
164 }
165 else if(type_id==ID_floatbv)
166 {
167 ieee_floatt ieee_float(to_floatbv_type(type));
168 ieee_float.from_integer(int_value);
169 return ieee_float.to_expr();
170 }
171 else
172 PRECONDITION(false);
173}
174
176std::size_t address_bits(const mp_integer &size)
177{
178 // in theory an arbitrary-precision integer could be as large as
179 // numeric_limits<std::size_t>::max() * CHAR_BIT (but then we would only be
180 // able to store 2^CHAR_BIT many of those; the implementation of mp_integer as
181 // BigInt is much more restricted as its size is stored as an unsigned int
182 std::size_t result = 1;
183
184 for(mp_integer x = 2; x < size; ++result, x *= 2) {}
185
186 INVARIANT(power(2, result) >= size, "address_bits(size) >= log2(size)");
187
188 return result;
189}
190
195 const mp_integer &exponent)
196{
197 PRECONDITION(exponent >= 0);
198
199 /* There are a number of special cases which are:
200 * A. very common
201 * B. handled more efficiently
202 */
203 if(base.is_long() && exponent.is_long())
204 {
205 switch(base.to_long())
206 {
207 case 2:
208 {
209 mp_integer result;
210 result.setPower2(numeric_cast_v<unsigned>(exponent));
211 return result;
212 }
213 case 1: return 1;
214 case 0: return 0;
215 default:
216 {
217 }
218 }
219 }
220
221 if(exponent==0)
222 return 1;
223
224 if(base<0)
225 {
226 mp_integer result = power(-base, exponent);
227 if(exponent.is_odd())
228 return -result;
229 else
230 return result;
231 }
232
233 mp_integer result=base;
234 mp_integer count=exponent-1;
235
236 while(count!=0)
237 {
238 result*=base;
239 --count;
240 }
241
242 return result;
243}
244
245void mp_min(mp_integer &a, const mp_integer &b)
246{
247 if(b<a)
248 a=b;
249}
250
251void mp_max(mp_integer &a, const mp_integer &b)
252{
253 if(b>a)
254 a=b;
255}
256
262 const irep_idt &src,
263 std::size_t width,
264 std::size_t bit_index)
265{
266 PRECONDITION(bit_index < width);
267
268 // The representation is hex, i.e., four bits per letter,
269 // most significant nibble first, using uppercase letters.
270 // No lowercase, no leading zeros (other than for 'zero'),
271 // to ensure canonicity.
272 const auto nibble_index = bit_index / 4;
273
274 if(nibble_index >= src.size())
275 return false;
276
277 const char nibble = src[src.size() - 1 - nibble_index];
278
280 isdigit(nibble) || (nibble >= 'A' && nibble <= 'F'),
281 "bvrep is hexadecimal, upper-case");
282
283 const unsigned char nibble_value =
284 isdigit(nibble) ? nibble - '0' : nibble - 'A' + 10;
285
286 return ((nibble_value >> (bit_index % 4)) & 1) != 0;
287}
288
290static char nibble2hex(unsigned char nibble)
291{
292 PRECONDITION(nibble <= 0xf);
293
294 if(nibble >= 10)
295 return 'A' + nibble - 10;
296 else
297 return '0' + nibble;
298}
299
305make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)
306{
307 std::string result;
308 result.reserve((width + 3) / 4);
309 unsigned char nibble = 0;
310
311 for(std::size_t i = 0; i < width; i++)
312 {
313 const auto bit_in_nibble = i % 4;
314
315 nibble |= ((unsigned char)f(i)) << bit_in_nibble;
316
317 if(bit_in_nibble == 3)
318 {
319 result += nibble2hex(nibble);
320 nibble = 0;
321 }
322 }
323
324 if(nibble != 0)
325 result += nibble2hex(nibble);
326
327 // drop leading zeros
328 const std::size_t pos = result.find_last_not_of('0');
329
330 if(pos == std::string::npos)
331 return ID_0;
332 else
333 {
334 result.resize(pos + 1);
335
336 std::reverse(result.begin(), result.end());
337
338 return result;
339 }
340}
341
350 const irep_idt &a,
351 const irep_idt &b,
352 const std::size_t width,
353 const std::function<bool(bool, bool)> f)
354{
355 return make_bvrep(width, [&a, &b, &width, f](std::size_t i) {
356 return f(get_bvrep_bit(a, width, i), get_bvrep_bit(b, width, i));
357 });
358}
359
367 const irep_idt &a,
368 const std::size_t width,
369 const std::function<bool(bool)> f)
370{
371 return make_bvrep(width, [&a, &width, f](std::size_t i) {
372 return f(get_bvrep_bit(a, width, i));
373 });
374}
375
379irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
380{
381 const mp_integer p = power(2, width);
382
383 if(src.is_negative())
384 {
385 // do two's complement encoding of negative numbers
386 mp_integer tmp = src;
387 tmp.negate();
388 tmp %= p;
389 if(tmp != 0)
390 tmp = p - tmp;
391 return integer2string(tmp, 16);
392 }
393 else
394 {
395 // we 'wrap around' if 'src' is too large
396 return integer2string(src % p, 16);
397 }
398}
399
401mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
402{
403 if(is_signed)
404 {
405 PRECONDITION(width >= 1);
406 const auto tmp = string2integer(id2string(src), 16);
407 const auto p = power(2, width - 1);
408 if(tmp >= p)
409 {
410 const auto result = tmp - 2 * p;
411 PRECONDITION(result >= -p);
412 return result;
413 }
414 else
415 return tmp;
416 }
417 else
418 {
419 const auto result = string2integer(id2string(src), 16);
420 PRECONDITION(result < power(2, width));
421 return result;
422 }
423}
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
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)
Definition: arith_tools.cpp:99
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
void mp_max(mp_integer &a, const mp_integer &b)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
static char nibble2hex(unsigned char nibble)
turn a value 0...15 into '0'-'9', 'A'-'Z'
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
irep_idt bvrep_bitwise_op(const irep_idt &a, const irep_idt &b, const std::size_t width, const std::function< bool(bool, bool)> f)
perform a binary bit-wise operation, given as a functor, on a bit-vector representation
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.
void mp_min(mp_integer &a, const mp_integer &b)
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:58
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: c_types.h:106
std::size_t get_width() const
Definition: std_types.h:864
const typet & underlying_type() const
Definition: c_types.h:274
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
size_t size() const
Definition: dstring.h:104
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2865
fixedbv_spect spec
Definition: fixedbv.h:44
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
constant_exprt to_expr() const
Definition: ieee_float.cpp:703
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:516
const irep_idt & id() const
Definition: irep.h:396
The null pointer constant.
Definition: pointer_expr.h:723
The Boolean constant true.
Definition: std_expr.h:2856
The type of an expression, extends irept.
Definition: type.h:29
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
literalt pos(literalt a)
Definition: literal.h:194
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
BigInt mp_integer
Definition: smt_terms.h:12
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
API to expression classes.
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45