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 bool to_integer(const exprt &expr, mp_integer &int_value)
18 {
19  if(!expr.is_constant())
20  return true;
21  return to_integer(to_constant_expr(expr), int_value);
22 }
23 
24 bool to_integer(const constant_exprt &expr, mp_integer &int_value)
25 {
26  const irep_idt &value=expr.get_value();
27  const typet &type=expr.type();
28  const irep_idt &type_id=type.id();
29 
30  if(type_id==ID_pointer)
31  {
32  if(value==ID_NULL)
33  {
34  int_value=0;
35  return false;
36  }
37  }
38  else if(type_id==ID_integer ||
39  type_id==ID_natural)
40  {
41  int_value=string2integer(id2string(value));
42  return false;
43  }
44  else if(type_id==ID_unsignedbv)
45  {
46  int_value=binary2integer(id2string(value), false);
47  return false;
48  }
49  else if(type_id==ID_signedbv)
50  {
51  int_value=binary2integer(id2string(value), true);
52  return false;
53  }
54  else if(type_id==ID_c_bool)
55  {
56  int_value=binary2integer(id2string(value), false);
57  return false;
58  }
59  else if(type_id==ID_c_enum)
60  {
61  const typet &subtype=to_c_enum_type(type).subtype();
62  if(subtype.id()==ID_signedbv)
63  {
64  int_value=binary2integer(id2string(value), true);
65  return false;
66  }
67  else if(subtype.id()==ID_unsignedbv)
68  {
69  int_value=binary2integer(id2string(value), false);
70  return false;
71  }
72  }
73  else if(type_id==ID_c_bit_field)
74  {
75  const typet &subtype=type.subtype();
76  if(subtype.id()==ID_signedbv)
77  {
78  int_value=binary2integer(id2string(value), true);
79  return false;
80  }
81  else if(subtype.id()==ID_unsignedbv)
82  {
83  int_value=binary2integer(id2string(value), false);
84  return false;
85  }
86  }
87 
88  return true;
89 }
90 
94 bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
95 {
96  mp_integer i;
97  if(to_integer(expr, i))
98  return true;
99  if(i<0)
100  return true;
101  else
102  {
103  uint_value=integer2unsigned(i);
104  return false;
105  }
106 }
107 
109  const mp_integer &int_value,
110  const typet &type)
111 {
112  const irep_idt &type_id=type.id();
113 
114  if(type_id==ID_integer)
115  {
116  constant_exprt result(type);
117  result.set_value(integer2string(int_value));
118  return result;
119  }
120  else if(type_id==ID_natural)
121  {
122  if(int_value<0)
123  {
125  r.make_nil();
126  return r;
127  }
128  constant_exprt result(type);
129  result.set_value(integer2string(int_value));
130  return result;
131  }
132  else if(type_id==ID_unsignedbv)
133  {
134  std::size_t width=to_unsignedbv_type(type).get_width();
135  constant_exprt result(type);
136  result.set_value(integer2binary(int_value, width));
137  return result;
138  }
139  else if(type_id==ID_bv)
140  {
141  std::size_t width=to_bv_type(type).get_width();
142  constant_exprt result(type);
143  result.set_value(integer2binary(int_value, width));
144  return result;
145  }
146  else if(type_id==ID_signedbv)
147  {
148  std::size_t width=to_signedbv_type(type).get_width();
149  constant_exprt result(type);
150  result.set_value(integer2binary(int_value, width));
151  return result;
152  }
153  else if(type_id==ID_c_enum)
154  {
155  std::size_t width=to_c_enum_type(type).subtype().get_unsigned_int(ID_width);
156  constant_exprt result(type);
157  result.set_value(integer2binary(int_value, width));
158  return result;
159  }
160  else if(type_id==ID_c_bool)
161  {
162  std::size_t width=to_c_bool_type(type).get_width();
163  constant_exprt result(type);
164  result.set_value(integer2binary(int_value, width));
165  return result;
166  }
167  else if(type_id==ID_bool)
168  {
169  if(int_value==0)
170  return false_exprt();
171  else if(int_value==1)
172  return true_exprt();
173  }
174  else if(type_id==ID_pointer)
175  {
176  if(int_value==0)
177  return null_pointer_exprt(to_pointer_type(type));
178  }
179  else if(type_id==ID_c_bit_field)
180  {
181  std::size_t width=to_c_bit_field_type(type).get_width();
182  constant_exprt result(type);
183  result.set_value(integer2binary(int_value, width));
184  return result;
185  }
186  else if(type_id==ID_fixedbv)
187  {
188  fixedbvt fixedbv;
189  fixedbv.spec=fixedbv_spect(to_fixedbv_type(type));
190  fixedbv.from_integer(int_value);
191  return fixedbv.to_expr();
192  }
193  else if(type_id==ID_floatbv)
194  {
195  ieee_floatt ieee_float(to_floatbv_type(type));
196  ieee_float.from_integer(int_value);
197  return ieee_float.to_expr();
198  }
199 
200  {
201  PRECONDITION(false);
203  r.make_nil();
204  return r;
205  }
206 }
207 
209 std::size_t address_bits(const mp_integer &size)
210 {
211  // in theory an arbitrary-precision integer could be as large as
212  // numeric_limits<std::size_t>::max() * CHAR_BIT (but then we would only be
213  // able to store 2^CHAR_BIT many of those; the implementation of mp_integer as
214  // BigInt is much more restricted as its size is stored as an unsigned int
215  std::size_t result = 1;
216 
217  for(mp_integer x = 2; x < size; ++result, x *= 2) {}
218 
219  INVARIANT(power(2, result) >= size, "address_bits(size) >= log2(size)");
220 
221  return result;
222 }
223 
228  const mp_integer &exponent)
229 {
230  PRECONDITION(exponent >= 0);
231 
232  /* There are a number of special cases which are:
233  * A. very common
234  * B. handled more efficiently
235  */
236  if(base.is_long() && exponent.is_long())
237  {
238  switch(base.to_long())
239  {
240  case 2:
241  {
242  mp_integer result;
243  result.setPower2(exponent.to_ulong());
244  return result;
245  }
246  case 1: return 1;
247  case 0: return 0;
248  default:
249  {
250  }
251  }
252  }
253 
254  if(exponent==0)
255  return 1;
256 
257  if(base<0)
258  {
259  mp_integer result = power(-base, exponent);
260  if(exponent.is_odd())
261  return -result;
262  else
263  return result;
264  }
265 
266  mp_integer result=base;
267  mp_integer count=exponent-1;
268 
269  while(count!=0)
270  {
271  result*=base;
272  --count;
273  }
274 
275  return result;
276 }
277 
278 void mp_min(mp_integer &a, const mp_integer &b)
279 {
280  if(b<a)
281  a=b;
282 }
283 
284 void mp_max(mp_integer &a, const mp_integer &b)
285 {
286  if(b>a)
287  a=b;
288 }
The type of an expression.
Definition: type.h:22
static int8_t r
Definition: irep_hash.h:59
BigInt mp_integer
Definition: mp_arith.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
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 generic typet to a signedbv_typet.
Definition: std_types.h:1287
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
void mp_max(mp_integer &a, const mp_integer &b)
const irep_idt & get_value() const
Definition: std_expr.h:4441
The null pointer constant.
Definition: std_expr.h:4520
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
typet & type()
Definition: expr.h:56
A constant literal expression.
Definition: std_expr.h:4424
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a generic typet to a c_bool_typet.
Definition: std_types.h:1552
bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
convert a positive integer expression to an unsigned int
Definition: arith_tools.cpp:94
const irep_idt & id() const
Definition: irep.h:189
void set_value(const irep_idt &value)
Definition: std_expr.h:4446
The boolean constant true.
Definition: std_expr.h:4488
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:230
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4465
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
Definition: std_types.h:1203
The boolean constant false.
Definition: std_expr.h:4499
bool is_constant() const
Definition: expr.cpp:119
std::size_t get_width() const
Definition: std_types.h:1129
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:202
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1245
API to type classes.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1373
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1334
Base class for all expressions.
Definition: expr.h:42
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:508
unsigned int get_unsigned_int(const irep_namet &name) const
Definition: irep.cpp:250
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Definition: std_types.h:1402
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
Definition: std_types.h:710
const typet & subtype() const
Definition: type.h:33
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.