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 "expr_util.h"
13#include "fixedbv.h"
14#include "ieee_float.h"
15#include "invariant.h"
16#include "std_expr.h"
17
18#include <algorithm>
19
20bool to_integer(const constant_exprt &expr, mp_integer &int_value)
21{
22 const irep_idt &value=expr.get_value();
23 const typet &type=expr.type();
24 const irep_idt &type_id=type.id();
25
26 if(type_id==ID_pointer)
27 {
28 if(expr.is_null_pointer())
29 {
30 int_value=0;
31 return false;
32 }
33 }
34 else if(type_id == ID_integer || type_id == ID_natural || type_id == ID_range)
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(underlying_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(underlying_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_range)
115 {
116 auto &range_type = to_range_type(type);
117 PRECONDITION(int_value >= range_type.get_from());
118 PRECONDITION(int_value <= range_type.get_to());
119 return constant_exprt{integer2string(int_value), type};
120 }
121 else if(type_id==ID_unsignedbv)
122 {
123 std::size_t width=to_unsignedbv_type(type).get_width();
124 return constant_exprt(integer2bvrep(int_value, width), type);
125 }
126 else if(type_id==ID_bv)
127 {
128 std::size_t width=to_bv_type(type).get_width();
129 return constant_exprt(integer2bvrep(int_value, width), type);
130 }
131 else if(type_id==ID_signedbv)
132 {
133 std::size_t width=to_signedbv_type(type).get_width();
134 return constant_exprt(integer2bvrep(int_value, width), type);
135 }
136 else if(type_id==ID_c_enum)
137 {
138 const std::size_t width =
139 to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width();
140 return constant_exprt(integer2bvrep(int_value, width), type);
141 }
142 else if(type_id==ID_c_bool)
143 {
144 std::size_t width=to_c_bool_type(type).get_width();
145 return constant_exprt(integer2bvrep(int_value, width), type);
146 }
147 else if(type_id==ID_bool)
148 {
149 PRECONDITION(int_value == 0 || int_value == 1);
150 if(int_value == 0)
151 return false_exprt();
152 else
153 return true_exprt();
154 }
155 else if(type_id==ID_pointer)
156 {
157 PRECONDITION(int_value == 0);
159 }
160 else if(type_id==ID_c_bit_field)
161 {
162 std::size_t width=to_c_bit_field_type(type).get_width();
163 return constant_exprt(integer2bvrep(int_value, width), type);
164 }
165 else if(type_id==ID_fixedbv)
166 {
167 fixedbvt fixedbv;
168 fixedbv.spec=fixedbv_spect(to_fixedbv_type(type));
169 fixedbv.from_integer(int_value);
170 return fixedbv.to_expr();
171 }
172 else if(type_id==ID_floatbv)
173 {
174 ieee_floatt ieee_float(to_floatbv_type(type));
175 ieee_float.from_integer(int_value);
176 return ieee_float.to_expr();
177 }
178 else
179 PRECONDITION(false);
180}
181
183std::size_t address_bits(const mp_integer &size)
184{
185 // in theory an arbitrary-precision integer could be as large as
186 // numeric_limits<std::size_t>::max() * CHAR_BIT (but then we would only be
187 // able to store 2^CHAR_BIT many of those; the implementation of mp_integer as
188 // BigInt is much more restricted as its size is stored as an unsigned int
189 std::size_t result = 1;
190
191 for(mp_integer x = 2; x < size; ++result, x *= 2) {}
192
193 INVARIANT(power(2, result) >= size, "address_bits(size) >= log2(size)");
194
195 return result;
196}
197
202 const mp_integer &exponent)
203{
204 PRECONDITION(exponent >= 0);
205
206 /* There are a number of special cases which are:
207 * A. very common
208 * B. handled more efficiently
209 */
210 if(base.is_long() && exponent.is_long())
211 {
212 switch(base.to_long())
213 {
214 case 2:
215 {
216 mp_integer result;
217 result.setPower2(numeric_cast_v<unsigned>(exponent));
218 return result;
219 }
220 case 1: return 1;
221 case 0: return 0;
222 default:
223 {
224 }
225 }
226 }
227
228 if(exponent==0)
229 return 1;
230
231 if(base<0)
232 {
233 mp_integer result = power(-base, exponent);
234 if(exponent.is_odd())
235 return -result;
236 else
237 return result;
238 }
239
240 mp_integer result=base;
241 mp_integer count=exponent-1;
242
243 while(count!=0)
244 {
245 result*=base;
246 --count;
247 }
248
249 return result;
250}
251
252void mp_min(mp_integer &a, const mp_integer &b)
253{
254 if(b<a)
255 a=b;
256}
257
258void mp_max(mp_integer &a, const mp_integer &b)
259{
260 if(b>a)
261 a=b;
262}
263
269 const irep_idt &src,
270 std::size_t width,
271 std::size_t bit_index)
272{
273 PRECONDITION(bit_index < width);
274
275 // The representation is hex, i.e., four bits per letter,
276 // most significant nibble first, using uppercase letters.
277 // No lowercase, no leading zeros (other than for 'zero'),
278 // to ensure canonicity.
279 const auto nibble_index = bit_index / 4;
280
281 if(nibble_index >= src.size())
282 return false;
283
284 const char nibble = src[src.size() - 1 - nibble_index];
285
287 isdigit(nibble) || (nibble >= 'A' && nibble <= 'F'),
288 "bvrep is hexadecimal, upper-case");
289
290 const unsigned char nibble_value =
291 isdigit(nibble) ? nibble - '0' : nibble - 'A' + 10;
292
293 return ((nibble_value >> (bit_index % 4)) & 1) != 0;
294}
295
297static char nibble2hex(unsigned char nibble)
298{
299 PRECONDITION(nibble <= 0xf);
300
301 if(nibble >= 10)
302 return 'A' + nibble - 10;
303 else
304 return '0' + nibble;
305}
306
312make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)
313{
314 std::string result;
315 result.reserve((width + 3) / 4);
316 unsigned char nibble = 0;
317
318 for(std::size_t i = 0; i < width; i++)
319 {
320 const auto bit_in_nibble = i % 4;
321
322 nibble |= ((unsigned char)f(i)) << bit_in_nibble;
323
324 if(bit_in_nibble == 3)
325 {
326 result += nibble2hex(nibble);
327 nibble = 0;
328 }
329 }
330
331 if(nibble != 0)
332 result += nibble2hex(nibble);
333
334 // drop leading zeros
335 const std::size_t pos = result.find_last_not_of('0');
336
337 if(pos == std::string::npos)
338 return ID_0;
339 else
340 {
341 result.resize(pos + 1);
342
343 std::reverse(result.begin(), result.end());
344
345 return result;
346 }
347}
348
357 const irep_idt &a,
358 const irep_idt &b,
359 const std::size_t width,
360 const std::function<bool(bool, bool)> f)
361{
362 return make_bvrep(width, [&a, &b, &width, f](std::size_t i) {
363 return f(get_bvrep_bit(a, width, i), get_bvrep_bit(b, width, i));
364 });
365}
366
374 const irep_idt &a,
375 const std::size_t width,
376 const std::function<bool(bool)> f)
377{
378 return make_bvrep(width, [&a, &width, f](std::size_t i) {
379 return f(get_bvrep_bit(a, width, i));
380 });
381}
382
386irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
387{
388 const mp_integer p = power(2, width);
389
390 if(src.is_negative())
391 {
392 // do two's complement encoding of negative numbers
393 mp_integer tmp = src;
394 tmp.negate();
395 tmp %= p;
396 if(tmp != 0)
397 tmp = p - tmp;
398 return integer2string(tmp, 16);
399 }
400 else
401 {
402 // we 'wrap around' if 'src' is too large
403 return integer2string(src % p, 16);
404 }
405}
406
408mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
409{
410 if(is_signed)
411 {
412 PRECONDITION(width >= 1);
413 const auto tmp = string2integer(id2string(src), 16);
414 const auto p = power(2, width - 1);
415 if(tmp >= p)
416 {
417 const auto result = tmp - 2 * p;
418 PRECONDITION(result >= -p);
419 return result;
420 }
421 else
422 return tmp;
423 }
424 else
425 {
426 const auto result = string2integer(id2string(src), 16);
427 PRECONDITION(result < power(2, width));
428 return result;
429 }
430}
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)
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.
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)
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...
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:80
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition c_types.h:128
std::size_t get_width() const
Definition std_types.h:925
const typet & underlying_type() const
Definition c_types.h:307
A constant literal expression.
Definition std_expr.h:2995
const irep_idt & get_value() const
Definition std_expr.h:3003
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition std_expr.cpp:25
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
size_t size() const
Definition dstring.h:121
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3077
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
void from_integer(const mp_integer &i)
const irep_idt & id() const
Definition irep.h:388
The null pointer constant.
The Boolean constant true.
Definition std_expr.h:3068
The type of an expression, extends irept.
Definition type.h:29
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
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.
BigInt mp_integer
Definition smt_terms.h:17
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#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.
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Definition std_types.h:1037
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45