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 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 &subtype=to_c_enum_type(type).subtype();
60  if(subtype.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(subtype.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 &subtype = c_bit_field_type.subtype();
78 
79  if(subtype.id()==ID_signedbv)
80  {
81  int_value = bvrep2integer(value, width, true);
82  return false;
83  }
84  else if(subtype.id()==ID_unsignedbv)
85  {
86  int_value = bvrep2integer(value, width, false);
87  return false;
88  }
89  else if(subtype.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).subtype()).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);
151  return null_pointer_exprt(to_pointer_type(type));
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 
176 std::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 
245 void mp_min(mp_integer &a, const mp_integer &b)
246 {
247  if(b<a)
248  a=b;
249 }
250 
251 void 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 
290 static 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 
304 irep_idt
305 make_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 
379 irep_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 
401 mp_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 }
to_c_bool_type
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: std_types.h:1636
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
ieee_floatt
Definition: ieee_float.h:119
typet::subtype
const typet & subtype() const
Definition: type.h:47
fixedbvt::from_integer
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
arith_tools.h
make_bvrep
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
Definition: arith_tools.cpp:305
pos
literalt pos(literalt a)
Definition: literal.h:194
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:681
typet
The type of an expression, extends irept.
Definition: type.h:28
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
is_signed
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
fixedbv.h
invariant.h
to_integer
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
mp_max
void mp_max(mp_integer &a, const mp_integer &b)
Definition: arith_tools.cpp:251
fixedbvt::to_expr
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
to_bv_type
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: std_types.h:1139
address_bits
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
Definition: arith_tools.cpp:176
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1362
integer2bvrep
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...
Definition: arith_tools.cpp:379
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1248
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3988
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
bvrep_bitwise_op
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
Definition: arith_tools.cpp:349
std_types.h
to_c_bit_field_type
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:1471
nibble2hex
static char nibble2hex(unsigned char nibble)
turn a value 0...15 into '0'-'9', 'A'-'Z'
Definition: arith_tools.cpp:290
irept::id
const irep_idt & id() const
Definition: irep.h:418
false_exprt
The Boolean constant false.
Definition: std_expr.h:3963
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
ieee_floatt::from_integer
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:511
fixedbv_spect
Definition: fixedbv.h:19
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:401
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
ieee_float.h
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1298
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
fixedbvt::spec
fixedbv_spect spec
Definition: fixedbv.h:44
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
fixedbvt
Definition: fixedbv.h:41
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
mp_min
void mp_min(mp_integer &a, const mp_integer &b)
Definition: arith_tools.cpp:245
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
true_exprt
The Boolean constant true.
Definition: std_expr.h:3954
constant_exprt
A constant literal expression.
Definition: std_expr.h:3905
std_expr.h
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
dstringt::size
size_t size() const
Definition: dstring.h:104
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
get_bvrep_bit
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.
Definition: arith_tools.cpp:261
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106