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