CBMC
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
21{
22 const irep_idt &value=expr.get_value();
23 const typet &type=expr.type();
24 const irep_idt &type_id=type.id();
25
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 {
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
106 {
108 }
109 else if(type_id==ID_natural)
110 {
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());
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 {
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 {
169 fixedbv.from_integer(int_value);
170 return fixedbv.to_expr();
171 }
172 else if(type_id==ID_floatbv)
173 {
176 // always rounds to zero
177 ieee_float.from_integer(int_value);
178 return ieee_float.to_expr();
179 }
180 else
181 PRECONDITION(false);
182}
183
185std::size_t address_bits(const mp_integer &size)
186{
187 // in theory an arbitrary-precision integer could be as large as
188 // numeric_limits<std::size_t>::max() * CHAR_BIT (but then we would only be
189 // able to store 2^CHAR_BIT many of those; the implementation of mp_integer as
190 // BigInt is much more restricted as its size is stored as an unsigned int
191 std::size_t result = 1;
192
193 for(mp_integer x = 2; x < size; ++result, x *= 2) {}
194
195 INVARIANT(power(2, result) >= size, "address_bits(size) >= log2(size)");
196
197 return result;
198}
199
204 const mp_integer &exponent)
205{
206 PRECONDITION(exponent >= 0);
207
208 /* There are a number of special cases which are:
209 * A. very common
210 * B. handled more efficiently
211 */
212 if(base.is_long() && exponent.is_long())
213 {
214 switch(base.to_long())
215 {
216 case 2:
217 {
218 mp_integer result;
219 result.setPower2(numeric_cast_v<unsigned>(exponent));
220 return result;
221 }
222 case 1: return 1;
223 case 0: return 0;
224 default:
225 {
226 }
227 }
228 }
229
230 if(exponent==0)
231 return 1;
232
233 if(base<0)
234 {
235 mp_integer result = power(-base, exponent);
236 if(exponent.is_odd())
237 return -result;
238 else
239 return result;
240 }
241
242 mp_integer result=base;
243 mp_integer count=exponent-1;
244
245 while(count!=0)
246 {
247 result*=base;
248 --count;
249 }
250
251 return result;
252}
253
255{
256 if(b<a)
257 a=b;
258}
259
261{
262 if(b>a)
263 a=b;
264}
265
271 const irep_idt &src,
272 std::size_t width,
273 std::size_t bit_index)
274{
275 PRECONDITION(bit_index < width);
276
277 // The representation is hex, i.e., four bits per letter,
278 // most significant nibble first, using uppercase letters.
279 // No lowercase, no leading zeros (other than for 'zero'),
280 // to ensure canonicity.
281 const auto nibble_index = bit_index / 4;
282
283 if(nibble_index >= src.size())
284 return false;
285
286 const char nibble = src[src.size() - 1 - nibble_index];
287
289 isdigit(nibble) || (nibble >= 'A' && nibble <= 'F'),
290 "bvrep is hexadecimal, upper-case");
291
292 const unsigned char nibble_value =
293 isdigit(nibble) ? nibble - '0' : nibble - 'A' + 10;
294
295 return ((nibble_value >> (bit_index % 4)) & 1) != 0;
296}
297
299static char nibble2hex(unsigned char nibble)
300{
301 PRECONDITION(nibble <= 0xf);
302
303 if(nibble >= 10)
304 return 'A' + nibble - 10;
305 else
306 return '0' + nibble;
307}
308
314make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)
315{
316 std::string result;
317 result.reserve((width + 3) / 4);
318 unsigned char nibble = 0;
319
320 for(std::size_t i = 0; i < width; i++)
321 {
322 const auto bit_in_nibble = i % 4;
323
324 nibble |= ((unsigned char)f(i)) << bit_in_nibble;
325
326 if(bit_in_nibble == 3)
327 {
328 result += nibble2hex(nibble);
329 nibble = 0;
330 }
331 }
332
333 if(nibble != 0)
334 result += nibble2hex(nibble);
335
336 // drop leading zeros
337 const std::size_t pos = result.find_last_not_of('0');
338
339 if(pos == std::string::npos)
340 return ID_0;
341 else
342 {
343 result.resize(pos + 1);
344
345 std::reverse(result.begin(), result.end());
346
347 return result;
348 }
349}
350
359 const irep_idt &a,
360 const irep_idt &b,
361 const std::size_t width,
362 const std::function<bool(bool, bool)> f)
363{
364 return make_bvrep(width, [&a, &b, &width, f](std::size_t i) {
365 return f(get_bvrep_bit(a, width, i), get_bvrep_bit(b, width, i));
366 });
367}
368
376 const irep_idt &a,
377 const std::size_t width,
378 const std::function<bool(bool)> f)
379{
380 return make_bvrep(width, [&a, &width, f](std::size_t i) {
381 return f(get_bvrep_bit(a, width, i));
382 });
383}
384
388irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
389{
390 const mp_integer p = power(2, width);
391
392 if(src.is_negative())
393 {
394 // do two's complement encoding of negative numbers
395 mp_integer tmp = src;
396 tmp.negate();
397 tmp %= p;
398 if(tmp != 0)
399 tmp = p - tmp;
400 return integer2string(tmp, 16);
401 }
402 else
403 {
404 // we 'wrap around' if 'src' is too large
405 return integer2string(src % p, 16);
406 }
407}
408
410mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
411{
412 if(is_signed)
413 {
414 PRECONDITION(width >= 1);
415 const auto tmp = string2integer(id2string(src), 16);
416 const auto p = power(2, width - 1);
417 if(tmp >= p)
418 {
419 const auto result = tmp - 2 * p;
420 PRECONDITION(result >= -p);
421 return result;
422 }
423 else
424 return tmp;
425 }
426 else
427 {
428 const auto result = string2integer(id2string(src), 16);
429 PRECONDITION(result < power(2, width));
430 return result;
431 }
432}
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)
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A constant literal expression.
Definition std_expr.h:3117
const irep_idt & get_value() const
Definition std_expr.h:3125
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:3199
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
Definition ieee_float.h:338
const irep_idt & id() const
Definition irep.h:388
The null pointer constant.
The Boolean constant true.
Definition std_expr.h:3190
The type of an expression, extends irept.
Definition type.h:29
int isdigit(int c)
Definition ctype.c:24
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:1040
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45