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 <cassert>
12 
13 #include "fixedbv.h"
14 #include "ieee_float.h"
15 #include "std_types.h"
16 #include "std_expr.h"
17 
18 bool to_integer(const exprt &expr, mp_integer &int_value)
19 {
20  if(!expr.is_constant())
21  return true;
22  return to_integer(to_constant_expr(expr), int_value);
23 }
24 
25 bool to_integer(const constant_exprt &expr, mp_integer &int_value)
26 {
27  const irep_idt &value=expr.get_value();
28  const typet &type=expr.type();
29  const irep_idt &type_id=type.id();
30 
31  if(type_id==ID_pointer)
32  {
33  if(value==ID_NULL)
34  {
35  int_value=0;
36  return false;
37  }
38  }
39  else if(type_id==ID_integer ||
40  type_id==ID_natural)
41  {
42  int_value=string2integer(id2string(value));
43  return false;
44  }
45  else if(type_id==ID_unsignedbv)
46  {
47  int_value=binary2integer(id2string(value), false);
48  return false;
49  }
50  else if(type_id==ID_signedbv)
51  {
52  int_value=binary2integer(id2string(value), true);
53  return false;
54  }
55  else if(type_id==ID_c_bool)
56  {
57  int_value=binary2integer(id2string(value), false);
58  return false;
59  }
60  else if(type_id==ID_c_enum)
61  {
62  const typet &subtype=to_c_enum_type(type).subtype();
63  if(subtype.id()==ID_signedbv)
64  {
65  int_value=binary2integer(id2string(value), true);
66  return false;
67  }
68  else if(subtype.id()==ID_unsignedbv)
69  {
70  int_value=binary2integer(id2string(value), false);
71  return false;
72  }
73  }
74  else if(type_id==ID_c_bit_field)
75  {
76  const typet &subtype=type.subtype();
77  if(subtype.id()==ID_signedbv)
78  {
79  int_value=binary2integer(id2string(value), true);
80  return false;
81  }
82  else if(subtype.id()==ID_unsignedbv)
83  {
84  int_value=binary2integer(id2string(value), false);
85  return false;
86  }
87  }
88 
89  return true;
90 }
91 
95 bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
96 {
97  mp_integer i;
98  if(to_integer(expr, i))
99  return true;
100  if(i<0)
101  return true;
102  else
103  {
104  uint_value=integer2unsigned(i);
105  return false;
106  }
107 }
108 
110  const mp_integer &int_value,
111  const typet &type)
112 {
113  const irep_idt &type_id=type.id();
114 
115  if(type_id==ID_integer)
116  {
117  constant_exprt result(type);
118  result.set_value(integer2string(int_value));
119  return result;
120  }
121  else if(type_id==ID_natural)
122  {
123  if(int_value<0)
124  {
126  r.make_nil();
127  return r;
128  }
129  constant_exprt result(type);
130  result.set_value(integer2string(int_value));
131  return result;
132  }
133  else if(type_id==ID_unsignedbv)
134  {
135  std::size_t width=to_unsignedbv_type(type).get_width();
136  constant_exprt result(type);
137  result.set_value(integer2binary(int_value, width));
138  return result;
139  }
140  else if(type_id==ID_bv)
141  {
142  std::size_t width=to_bv_type(type).get_width();
143  constant_exprt result(type);
144  result.set_value(integer2binary(int_value, width));
145  return result;
146  }
147  else if(type_id==ID_signedbv)
148  {
149  std::size_t width=to_signedbv_type(type).get_width();
150  constant_exprt result(type);
151  result.set_value(integer2binary(int_value, width));
152  return result;
153  }
154  else if(type_id==ID_c_enum)
155  {
156  std::size_t width=to_c_enum_type(type).subtype().get_unsigned_int(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  assert(false);
204  r.make_nil();
205  return r;
206  }
207 }
208 
211 {
212  mp_integer result, x=2;
213 
214  for(result=1; x<size; result+=1, x*=2) {}
215 
216  return result;
217 }
218 
223  const mp_integer &exponent)
224 {
225  assert(exponent>=0);
226 
227  /* There are a number of special cases which are:
228  * A. very common
229  * B. handled more efficiently
230  */
231  if(base.is_long() && exponent.is_long())
232  {
233  switch(base.to_long())
234  {
235  case 2:
236  {
237  mp_integer result;
238  result.setPower2(exponent.to_ulong());
239  return result;
240  }
241  case 1: return 1;
242  case 0: return 0;
243  default:
244  {
245  }
246  }
247  }
248 
249  if(exponent==0)
250  return 1;
251 
252  if(base<0)
253  {
254  mp_integer result = power(-base, exponent);
255  if(exponent.is_odd())
256  return -result;
257  else
258  return result;
259  }
260 
261  mp_integer result=base;
262  mp_integer count=exponent-1;
263 
264  while(count!=0)
265  {
266  result*=base;
267  --count;
268  }
269 
270  return result;
271 }
272 
273 void mp_min(mp_integer &a, const mp_integer &b)
274 {
275  if(b<a)
276  a=b;
277 }
278 
279 void mp_max(mp_integer &a, const mp_integer &b)
280 {
281  if(b>a)
282  a=b;
283 }
The type of an expression.
Definition: type.h:20
static int8_t r
Definition: irep_hash.h:59
BigInt mp_integer
Definition: mp_arith.h:19
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:53
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
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:3702
The null pointer constant.
Definition: std_expr.h:3774
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
mp_integer address_bits(const mp_integer &size)
ceil(log2(size))
typet & type()
Definition: expr.h:60
A constant literal expression.
Definition: std_expr.h:3685
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
convert a positive integer expression to an unsigned int
Definition: arith_tools.cpp:95
const irep_idt & id() const
Definition: irep.h:189
void set_value(const irep_idt &value)
Definition: std_expr.h:3707
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a generic typet to a c_bool_typet.
Definition: std_types.h:1473
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
Definition: std_types.h:680
The boolean constant true.
Definition: std_expr.h:3742
fixedbv_spect spec
Definition: fixedbv.h:44
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
API to expression classes.
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:1319
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1154
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
The boolean constant false.
Definition: std_expr.h:3753
bool is_constant() const
Definition: expr.cpp:128
std::size_t get_width() const
Definition: std_types.h:1030
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
Definition: std_types.h:1108
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1377
API to type classes.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1247
Base class for all expressions.
Definition: expr.h:46
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1200
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:63
void make_nil()
Definition: irep.h:243
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
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
const typet & subtype() const
Definition: type.h:31
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.