CBMC
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 "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 
20 bool 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 ||
35  type_id==ID_natural)
36  {
37  int_value=string2integer(id2string(value));
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 
106  if(type_id==ID_integer)
107  {
108  return constant_exprt(integer2string(int_value), type);
109  }
110  else if(type_id==ID_natural)
111  {
112  PRECONDITION(int_value >= 0);
113  return constant_exprt(integer2string(int_value), type);
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  {
151  PRECONDITION(int_value == 0);
152  return null_pointer_exprt(to_pointer_type(type));
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  {
161  fixedbvt fixedbv;
162  fixedbv.spec=fixedbv_spect(to_fixedbv_type(type));
163  fixedbv.from_integer(int_value);
164  return fixedbv.to_expr();
165  }
166  else if(type_id==ID_floatbv)
167  {
168  ieee_floatt ieee_float(to_floatbv_type(type));
169  ieee_float.from_integer(int_value);
170  return ieee_float.to_expr();
171  }
172  else
173  PRECONDITION(false);
174 }
175 
177 std::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 
246 void mp_min(mp_integer &a, const mp_integer &b)
247 {
248  if(b<a)
249  a=b;
250 }
251 
252 void mp_max(mp_integer &a, const mp_integer &b)
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 
291 static 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 
305 irep_idt
306 make_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 
380 irep_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 
402 mp_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.
Definition: arith_tools.cpp:20
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 floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
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_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_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:2990
const irep_idt & get_value() const
Definition: std_expr.h:2998
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:3072
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
Definition: ieee_float.cpp:703
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:516
const irep_idt & id() const
Definition: irep.h:388
The null pointer constant.
Definition: pointer_expr.h:909
The Boolean constant true.
Definition: std_expr.h:3063
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.
Definition: pointer_expr.h:93
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.
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45