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
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(is_null_pointer(expr))
29 {
30 int_value=0;
31 return false;
32 }
33 }
34 else if(type_id==ID_integer ||
36 {
38 return false;
39 }
40 else if(type_id==ID_unsignedbv)
41 {
42 const auto width = to_unsignedbv_type(type).get_width();
43 int_value = bvrep2integer(value, width, false);
44 return false;
45 }
46 else if(type_id==ID_signedbv)
47 {
48 const auto width = to_signedbv_type(type).get_width();
49 int_value = bvrep2integer(value, width, true);
50 return false;
51 }
52 else if(type_id==ID_c_bool)
53 {
54 const auto width = to_c_bool_type(type).get_width();
55 int_value = bvrep2integer(value, width, false);
56 return false;
57 }
58 else if(type_id==ID_c_enum)
59 {
60 const typet &underlying_type = to_c_enum_type(type).underlying_type();
61 if(underlying_type.id() == ID_signedbv)
62 {
63 const auto width = to_signedbv_type(underlying_type).get_width();
64 int_value = bvrep2integer(value, width, true);
65 return false;
66 }
67 else if(underlying_type.id() == ID_unsignedbv)
68 {
69 const auto width = to_unsignedbv_type(underlying_type).get_width();
70 int_value = bvrep2integer(value, width, false);
71 return false;
72 }
73 }
74 else if(type_id==ID_c_bit_field)
75 {
76 const auto &c_bit_field_type = to_c_bit_field_type(type);
77 const auto width = c_bit_field_type.get_width();
78 const typet &underlying_type = c_bit_field_type.underlying_type();
79
80 if(underlying_type.id() == ID_signedbv)
81 {
82 int_value = bvrep2integer(value, width, true);
83 return false;
84 }
85 else if(underlying_type.id() == ID_unsignedbv)
86 {
87 int_value = bvrep2integer(value, width, false);
88 return false;
89 }
90 else if(underlying_type.id() == ID_c_bool)
91 {
92 int_value = bvrep2integer(value, width, false);
93 return false;
94 }
95 }
96
97 return true;
98}
99
101 const mp_integer &int_value,
102 const typet &type)
103{
104 const irep_idt &type_id=type.id();
105
107 {
109 }
110 else if(type_id==ID_natural)
111 {
114 }
115 else if(type_id==ID_unsignedbv)
116 {
117 std::size_t width=to_unsignedbv_type(type).get_width();
118 return constant_exprt(integer2bvrep(int_value, width), type);
119 }
120 else if(type_id==ID_bv)
121 {
122 std::size_t width=to_bv_type(type).get_width();
123 return constant_exprt(integer2bvrep(int_value, width), type);
124 }
125 else if(type_id==ID_signedbv)
126 {
127 std::size_t width=to_signedbv_type(type).get_width();
128 return constant_exprt(integer2bvrep(int_value, width), type);
129 }
130 else if(type_id==ID_c_enum)
131 {
132 const std::size_t width =
133 to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width();
134 return constant_exprt(integer2bvrep(int_value, width), type);
135 }
136 else if(type_id==ID_c_bool)
137 {
138 std::size_t width=to_c_bool_type(type).get_width();
139 return constant_exprt(integer2bvrep(int_value, width), type);
140 }
141 else if(type_id==ID_bool)
142 {
143 PRECONDITION(int_value == 0 || int_value == 1);
144 if(int_value == 0)
145 return false_exprt();
146 else
147 return true_exprt();
148 }
149 else if(type_id==ID_pointer)
150 {
153 }
154 else if(type_id==ID_c_bit_field)
155 {
156 std::size_t width=to_c_bit_field_type(type).get_width();
157 return constant_exprt(integer2bvrep(int_value, width), type);
158 }
159 else if(type_id==ID_fixedbv)
160 {
163 fixedbv.from_integer(int_value);
164 return fixedbv.to_expr();
165 }
166 else if(type_id==ID_floatbv)
167 {
169 ieee_float.from_integer(int_value);
170 return ieee_float.to_expr();
171 }
172 else
173 PRECONDITION(false);
174}
175
177std::size_t address_bits(const mp_integer &size)
178{
179 // in theory an arbitrary-precision integer could be as large as
180 // numeric_limits<std::size_t>::max() * CHAR_BIT (but then we would only be
181 // able to store 2^CHAR_BIT many of those; the implementation of mp_integer as
182 // BigInt is much more restricted as its size is stored as an unsigned int
183 std::size_t result = 1;
184
185 for(mp_integer x = 2; x < size; ++result, x *= 2) {}
186
187 INVARIANT(power(2, result) >= size, "address_bits(size) >= log2(size)");
188
189 return result;
190}
191
196 const mp_integer &exponent)
197{
198 PRECONDITION(exponent >= 0);
199
200 /* There are a number of special cases which are:
201 * A. very common
202 * B. handled more efficiently
203 */
204 if(base.is_long() && exponent.is_long())
205 {
206 switch(base.to_long())
207 {
208 case 2:
209 {
210 mp_integer result;
211 result.setPower2(numeric_cast_v<unsigned>(exponent));
212 return result;
213 }
214 case 1: return 1;
215 case 0: return 0;
216 default:
217 {
218 }
219 }
220 }
221
222 if(exponent==0)
223 return 1;
224
225 if(base<0)
226 {
227 mp_integer result = power(-base, exponent);
228 if(exponent.is_odd())
229 return -result;
230 else
231 return result;
232 }
233
234 mp_integer result=base;
235 mp_integer count=exponent-1;
236
237 while(count!=0)
238 {
239 result*=base;
240 --count;
241 }
242
243 return result;
244}
245
247{
248 if(b<a)
249 a=b;
250}
251
253{
254 if(b>a)
255 a=b;
256}
257
263 const irep_idt &src,
264 std::size_t width,
265 std::size_t bit_index)
266{
267 PRECONDITION(bit_index < width);
268
269 // The representation is hex, i.e., four bits per letter,
270 // most significant nibble first, using uppercase letters.
271 // No lowercase, no leading zeros (other than for 'zero'),
272 // to ensure canonicity.
273 const auto nibble_index = bit_index / 4;
274
275 if(nibble_index >= src.size())
276 return false;
277
278 const char nibble = src[src.size() - 1 - nibble_index];
279
281 isdigit(nibble) || (nibble >= 'A' && nibble <= 'F'),
282 "bvrep is hexadecimal, upper-case");
283
284 const unsigned char nibble_value =
285 isdigit(nibble) ? nibble - '0' : nibble - 'A' + 10;
286
287 return ((nibble_value >> (bit_index % 4)) & 1) != 0;
288}
289
291static char nibble2hex(unsigned char nibble)
292{
293 PRECONDITION(nibble <= 0xf);
294
295 if(nibble >= 10)
296 return 'A' + nibble - 10;
297 else
298 return '0' + nibble;
299}
300
306make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)
307{
308 std::string result;
309 result.reserve((width + 3) / 4);
310 unsigned char nibble = 0;
311
312 for(std::size_t i = 0; i < width; i++)
313 {
314 const auto bit_in_nibble = i % 4;
315
316 nibble |= ((unsigned char)f(i)) << bit_in_nibble;
317
318 if(bit_in_nibble == 3)
319 {
320 result += nibble2hex(nibble);
321 nibble = 0;
322 }
323 }
324
325 if(nibble != 0)
326 result += nibble2hex(nibble);
327
328 // drop leading zeros
329 const std::size_t pos = result.find_last_not_of('0');
330
331 if(pos == std::string::npos)
332 return ID_0;
333 else
334 {
335 result.resize(pos + 1);
336
337 std::reverse(result.begin(), result.end());
338
339 return result;
340 }
341}
342
351 const irep_idt &a,
352 const irep_idt &b,
353 const std::size_t width,
354 const std::function<bool(bool, bool)> f)
355{
356 return make_bvrep(width, [&a, &b, &width, f](std::size_t i) {
357 return f(get_bvrep_bit(a, width, i), get_bvrep_bit(b, width, i));
358 });
359}
360
368 const irep_idt &a,
369 const std::size_t width,
370 const std::function<bool(bool)> f)
371{
372 return make_bvrep(width, [&a, &width, f](std::size_t i) {
373 return f(get_bvrep_bit(a, width, i));
374 });
375}
376
380irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
381{
382 const mp_integer p = power(2, width);
383
384 if(src.is_negative())
385 {
386 // do two's complement encoding of negative numbers
387 mp_integer tmp = src;
388 tmp.negate();
389 tmp %= p;
390 if(tmp != 0)
391 tmp = p - tmp;
392 return integer2string(tmp, 16);
393 }
394 else
395 {
396 // we 'wrap around' if 'src' is too large
397 return integer2string(src % p, 16);
398 }
399}
400
402mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
403{
404 if(is_signed)
405 {
406 PRECONDITION(width >= 1);
407 const auto tmp = string2integer(id2string(src), 16);
408 const auto p = power(2, width - 1);
409 if(tmp >= p)
410 {
411 const auto result = tmp - 2 * p;
412 PRECONDITION(result >= -p);
413 return result;
414 }
415 else
416 return tmp;
417 }
418 else
419 {
420 const auto result = string2integer(id2string(src), 16);
421 PRECONDITION(result < power(2, width));
422 return result;
423 }
424}
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:563
A constant literal expression.
Definition std_expr.h:2942
const irep_idt & get_value() const
Definition std_expr.h:2950
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
size_t size() const
Definition dstring.h:122
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3017
const irep_idt & id() const
Definition irep.h:396
The null pointer constant.
The Boolean constant true.
Definition std_expr.h:3008
The type of an expression, extends irept.
Definition type.h:29
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
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.
#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.
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45