cprover
simplify_expr_floatbv.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 "simplify_expr_class.h"
10 
11 #include <cassert>
12 
13 #include "expr.h"
14 #include "namespace.h"
15 #include "ieee_float.h"
16 #include "std_expr.h"
17 #include "arith_tools.h"
18 
20 {
21  if(expr.operands().size()!=1)
22  return true;
23 
24  if(ns.follow(expr.op0().type()).id()!=ID_floatbv)
25  return true;
26 
27  if(expr.op0().is_constant())
28  {
29  ieee_floatt value(to_constant_expr(expr.op0()));
30  expr.make_bool(value.is_infinity());
31  return false;
32  }
33 
34  return true;
35 }
36 
38 {
39  if(expr.operands().size()!=1)
40  return true;
41 
42  if(expr.op0().is_constant())
43  {
44  ieee_floatt value(to_constant_expr(expr.op0()));
45  expr.make_bool(value.is_NaN());
46  return false;
47  }
48 
49  return true;
50 }
51 
53 {
54  if(expr.operands().size()!=1)
55  return true;
56 
57  if(expr.op0().is_constant())
58  {
59  ieee_floatt value(to_constant_expr(expr.op0()));
60  expr.make_bool(value.is_normal());
61  return false;
62  }
63 
64  return true;
65 }
66 
67 #if 0
69 {
70  if(expr.operands().size()!=1)
71  return true;
72 
73  if(expr.op0().is_constant())
74  {
75  const typet &type=ns.follow(expr.op0().type());
76 
77  if(type.id()==ID_floatbv)
78  {
79  ieee_floatt value(to_constant_expr(expr.op0()));
80  value.set_sign(false);
81  expr=value.to_expr();
82  return false;
83  }
84  else if(type.id()==ID_signedbv ||
85  type.id()==ID_unsignedbv)
86  {
87  mp_integer value;
88  if(!to_integer(expr.op0(), value))
89  {
90  if(value>=0)
91  {
92  expr=expr.op0();
93  return false;
94  }
95  else
96  {
97  value.negate();
98  expr=from_integer(value, type);
99  return false;
100  }
101  }
102  }
103  }
104 
105  return true;
106 }
107 #endif
108 
109 #if 0
111 {
112  if(expr.operands().size()!=1)
113  return true;
114 
115  if(expr.op0().is_constant())
116  {
117  const typet &type=ns.follow(expr.op0().type());
118 
119  if(type.id()==ID_floatbv)
120  {
121  ieee_floatt value(to_constant_expr(expr.op0()));
122  expr.make_bool(value.get_sign());
123  return false;
124  }
125  else if(type.id()==ID_signedbv ||
126  type.id()==ID_unsignedbv)
127  {
128  mp_integer value;
129  if(!to_integer(expr.op0(), value))
130  {
131  expr.make_bool(value>=0);
132  return false;
133  }
134  }
135  }
136 
137  return true;
138 }
139 #endif
140 
142 {
143  // These casts usually reduce precision, and thus, usually round.
144 
145  assert(expr.operands().size()==2);
146 
147  const typet &dest_type=ns.follow(expr.type());
148  const typet &src_type=ns.follow(expr.op0().type());
149 
150  // eliminate redundant casts
151  if(dest_type==src_type)
152  {
153  expr=expr.op0();
154  return false;
155  }
156 
157  exprt op0=expr.op0();
158  exprt op1=expr.op1(); // rounding mode
159 
160  // We can soundly re-write (float)((double)x op (double)y)
161  // to x op y. True for any rounding mode!
162 
163  #if 0
164  if(op0.id()==ID_floatbv_div ||
165  op0.id()==ID_floatbv_mult ||
166  op0.id()==ID_floatbv_plus ||
167  op0.id()==ID_floatbv_minus)
168  {
169  if(op0.operands().size()==3 &&
170  op0.op0().id()==ID_typecast &&
171  op0.op1().id()==ID_typecast &&
172  op0.op0().operands().size()==1 &&
173  op0.op1().operands().size()==1 &&
174  ns.follow(op0.op0().type())==dest_type &&
175  ns.follow(op0.op1().type())==dest_type)
176  {
177  exprt result(op0.id(), expr.type());
178  result.operands().resize(3);
179  result.op0()=op0.op0().op0();
180  result.op1()=op0.op1().op0();
181  result.op2()=op1;
182 
183  simplify_node(result);
184  expr.swap(result);
185  return false;
186  }
187  }
188  #endif
189 
190  // constant folding
191  if(op0.is_constant() && op1.is_constant())
192  {
193  mp_integer rounding_mode;
194  if(!to_integer(op1, rounding_mode))
195  {
196  if(src_type.id()==ID_floatbv)
197  {
198  if(dest_type.id()==ID_floatbv) // float to float
199  {
200  ieee_floatt result(to_constant_expr(op0));
201  result.rounding_mode=
203  result.change_spec(
204  ieee_float_spect(to_floatbv_type(dest_type)));
205  expr=result.to_expr();
206  return false;
207  }
208  else if(dest_type.id()==ID_signedbv ||
209  dest_type.id()==ID_unsignedbv)
210  {
211  if(rounding_mode==ieee_floatt::ROUND_TO_ZERO)
212  {
213  ieee_floatt result(to_constant_expr(op0));
214  result.rounding_mode=
216  mp_integer value=result.to_integer();
217  expr=from_integer(value, dest_type);
218  return false;
219  }
220  }
221  }
222  else if(src_type.id()==ID_signedbv ||
223  src_type.id()==ID_unsignedbv)
224  {
225  mp_integer value;
226  if(!to_integer(op0, value))
227  {
228  if(dest_type.id()==ID_floatbv) // int to float
229  {
230  ieee_floatt result(to_floatbv_type(dest_type));
231  result.rounding_mode=
233  result.from_integer(value);
234  expr=result.to_expr();
235  return false;
236  }
237  }
238  }
239  }
240  }
241 
242  #if 0
243  // (T)(a?b:c) --> a?(T)b:(T)c
244  if(expr.op0().id()==ID_if &&
245  expr.op0().operands().size()==3)
246  {
247  exprt tmp_op1=
248  binary_exprt(
249  expr.op0().op1(),
250  ID_floatbv_typecast,
251  expr.op1(),
252  dest_type);
253  exprt tmp_op2=
254  binary_exprt(
255  expr.op0().op2(),
256  ID_floatbv_typecast,
257  expr.op1(),
258  dest_type);
259  simplify_floatbv_typecast(tmp_op1);
260  simplify_floatbv_typecast(tmp_op2);
261  expr=if_exprt(expr.op0().op0(), tmp_op1, tmp_op2, dest_type);
262  simplify_if(expr);
263  return false;
264  }
265  #endif
266 
267  return true;
268 }
269 
271 {
272  const typet &type=ns.follow(expr.type());
273 
274  if(type.id()!=ID_floatbv)
275  return true;
276 
277  assert(expr.operands().size()==3);
278 
279  exprt op0=expr.op0();
280  exprt op1=expr.op1();
281  exprt op2=expr.op2(); // rounding mode
282 
283  assert(ns.follow(op0.type())==type);
284  assert(ns.follow(op1.type())==type);
285 
286  // Remember that floating-point addition is _NOT_ associative.
287  // Thus, we don't re-sort the operands.
288  // We only merge constants!
289 
290  if(op0.is_constant() && op1.is_constant() && op2.is_constant())
291  {
292  ieee_floatt v0(to_constant_expr(op0));
293  ieee_floatt v1(to_constant_expr(op1));
294 
295  mp_integer rounding_mode;
296  if(!to_integer(op2, rounding_mode))
297  {
298  v0.rounding_mode=
301 
302  ieee_floatt result=v0;
303 
304  if(expr.id()==ID_floatbv_plus)
305  result+=v1;
306  else if(expr.id()==ID_floatbv_minus)
307  result-=v1;
308  else if(expr.id()==ID_floatbv_mult)
309  result*=v1;
310  else if(expr.id()==ID_floatbv_div)
311  result/=v1;
312  else
313  assert(false);
314 
315  expr=result.to_expr();
316  return false;
317  }
318  }
319 
320  // division by one? Exact for all rounding modes.
321  if(expr.id()==ID_floatbv_div &&
322  op1.is_constant() && op1.is_one())
323  {
324  exprt tmp;
325  tmp.swap(op0);
326  expr.swap(tmp);
327  return false;
328  }
329 
330  return true;
331 }
332 
334 {
335  assert(expr.id()==ID_ieee_float_equal ||
336  expr.id()==ID_ieee_float_notequal);
337 
338  exprt::operandst &operands=expr.operands();
339 
340  if(expr.type().id()!=ID_bool)
341  return true;
342 
343  if(operands.size()!=2)
344  return true;
345 
346  // types must match
347  if(expr.op0().type()!=expr.op1().type())
348  return true;
349 
350  if(expr.op0().type().id()!=ID_floatbv)
351  return true;
352 
353  // first see if we compare to a constant
354 
355  if(expr.op0().is_constant() &&
356  expr.op1().is_constant())
357  {
358  ieee_floatt f0(to_constant_expr(expr.op0()));
359  ieee_floatt f1(to_constant_expr(expr.op1()));
360 
361  if(expr.id()==ID_ieee_float_notequal)
362  expr.make_bool(f0.ieee_not_equal(f1));
363  else if(expr.id()==ID_ieee_float_equal)
364  expr.make_bool(f0.ieee_equal(f1));
365  else
366  assert(false);
367 
368  return false;
369  }
370 
371  if(expr.op0()==expr.op1())
372  {
373  // x!=x is the same as saying isnan(op)
374  exprt isnan(ID_isnan, bool_typet());
375  isnan.copy_to_operands(expr.op0());
376 
377  if(expr.id()==ID_ieee_float_notequal)
378  {
379  }
380  else if(expr.id()==ID_ieee_float_equal)
381  isnan.make_not();
382  else
383  assert(false);
384 
385  expr.swap(isnan);
386  return false;
387  }
388 
389  return true;
390 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
bool simplify_abs(exprt &expr)
BigInt mp_integer
Definition: mp_arith.h:19
bool simplify_sign(exprt &expr)
bool simplify_node(exprt &expr)
exprt & op0()
Definition: expr.h:84
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
The trinary if-then-else operator.
Definition: std_expr.h:2771
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
bool is_NaN() const
Definition: ieee_float.h:226
void make_bool(bool value)
Definition: expr.cpp:147
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
void change_spec(const ieee_float_spect &dest_spec)
bool is_infinity() const
Definition: ieee_float.h:227
bool simplify_if(if_exprt &expr)
const irep_idt & id() const
Definition: irep.h:189
mp_integer to_integer() const
bool ieee_equal(const ieee_floatt &other) const
A generic base class for binary expressions.
Definition: std_expr.h:471
bool simplify_floatbv_op(exprt &expr)
bool is_normal() const
Definition: ieee_float.cpp:362
API to expression classes.
bool simplify_isinf(exprt &expr)
exprt & op1()
Definition: expr.h:87
bool is_constant() const
Definition: expr.cpp:128
std::vector< exprt > operandst
Definition: expr.h:49
bool simplify_floatbv_typecast(exprt &expr)
void make_not()
Definition: expr.cpp:100
Base class for all expressions.
Definition: expr.h:46
bool simplify_ieee_float_relation(exprt &expr)
const namespacet & ns
void negate()
Definition: expr.cpp:165
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:508
void swap(irept &irep)
Definition: irep.h:231
bool ieee_not_equal(const ieee_floatt &other) const
rounding_modet rounding_mode
Definition: ieee_float.h:121
exprt & op2()
Definition: expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool simplify_isnormal(exprt &expr)
bool simplify_isnan(exprt &expr)
bool is_one() const
Definition: expr.cpp:280