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  const std::size_t width =
156  to_c_enum_type(type).subtype().get_size_t(ID_width);
157  constant_exprt result(type);
158  result.set_value(integer2binary(int_value, width));
159  return result;
160  }
161  else if(type_id==ID_c_bool)
162  {
163  std::size_t width=to_c_bool_type(type).get_width();
164  constant_exprt result(type);
165  result.set_value(integer2binary(int_value, width));
166  return result;
167  }
168  else if(type_id==ID_bool)
169  {
170  if(int_value==0)
171  return false_exprt();
172  else if(int_value==1)
173  return true_exprt();
174  }
175  else if(type_id==ID_pointer)
176  {
177  if(int_value==0)
178  return null_pointer_exprt(to_pointer_type(type));
179  }
180  else if(type_id==ID_c_bit_field)
181  {
182  std::size_t width=to_c_bit_field_type(type).get_width();
183  constant_exprt result(type);
184  result.set_value(integer2binary(int_value, width));
185  return result;
186  }
187  else if(type_id==ID_fixedbv)
188  {
189  fixedbvt fixedbv;
190  fixedbv.spec=fixedbv_spect(to_fixedbv_type(type));
191  fixedbv.from_integer(int_value);
192  return fixedbv.to_expr();
193  }
194  else if(type_id==ID_floatbv)
195  {
196  ieee_floatt ieee_float(to_floatbv_type(type));
197  ieee_float.from_integer(int_value);
198  return ieee_float.to_expr();
199  }
200 
201  {
202  PRECONDITION(false);
204  r.make_nil();
205  return r;
206  }
207 }
208 
210 std::size_t address_bits(const mp_integer &size)
211 {
212  // in theory an arbitrary-precision integer could be as large as
213  // numeric_limits<std::size_t>::max() * CHAR_BIT (but then we would only be
214  // able to store 2^CHAR_BIT many of those; the implementation of mp_integer as
215  // BigInt is much more restricted as its size is stored as an unsigned int
216  std::size_t result = 1;
217 
218  for(mp_integer x = 2; x < size; ++result, x *= 2) {}
219 
220  INVARIANT(power(2, result) >= size, "address_bits(size) >= log2(size)");
221 
222  return result;
223 }
224 
229  const mp_integer &exponent)
230 {
231  PRECONDITION(exponent >= 0);
232 
233  /* There are a number of special cases which are:
234  * A. very common
235  * B. handled more efficiently
236  */
237  if(base.is_long() && exponent.is_long())
238  {
239  switch(base.to_long())
240  {
241  case 2:
242  {
243  mp_integer result;
244  result.setPower2(exponent.to_ulong());
245  return result;
246  }
247  case 1: return 1;
248  case 0: return 0;
249  default:
250  {
251  }
252  }
253  }
254 
255  if(exponent==0)
256  return 1;
257 
258  if(base<0)
259  {
260  mp_integer result = power(-base, exponent);
261  if(exponent.is_odd())
262  return -result;
263  else
264  return result;
265  }
266 
267  mp_integer result=base;
268  mp_integer count=exponent-1;
269 
270  while(count!=0)
271  {
272  result*=base;
273  --count;
274  }
275 
276  return result;
277 }
278 
279 void mp_min(mp_integer &a, const mp_integer &b)
280 {
281  if(b<a)
282  a=b;
283 }
284 
285 void mp_max(mp_integer &a, const mp_integer &b)
286 {
287  if(b>a)
288  a=b;
289 }
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: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 generic typet to a signedbv_typet.
Definition: std_types.h:1296
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:4439
The null pointer constant.
Definition: std_expr.h:4518
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:4422
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a generic typet to a c_bool_typet.
Definition: std_types.h:1561
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:259
void set_value(const irep_idt &value)
Definition: std_expr.h:4444
The boolean constant true.
Definition: std_expr.h:4486
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:242
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:4463
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
Definition: std_types.h:1212
The boolean constant false.
Definition: std_expr.h:4497
bool is_constant() const
Definition: expr.cpp:119
std::size_t get_width() const
Definition: std_types.h:1138
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1254
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:1382
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1343
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
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:1411
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:1459
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)
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:255
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.