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  binary_exprt tmp_op1(
248  expr.op0().op1(),
249  ID_floatbv_typecast,
250  expr.op1(),
251  dest_type);
252  binary_exprt tmp_op2(
253  expr.op0().op2(),
254  ID_floatbv_typecast,
255  expr.op1(),
256  dest_type);
257  simplify_floatbv_typecast(tmp_op1);
258  simplify_floatbv_typecast(tmp_op2);
259  expr=if_exprt(expr.op0().op0(), tmp_op1, tmp_op2, dest_type);
260  simplify_if(expr);
261  return false;
262  }
263  #endif
264 
265  return true;
266 }
267 
269 {
270  const typet &type=ns.follow(expr.type());
271 
272  if(type.id()!=ID_floatbv)
273  return true;
274 
275  assert(expr.operands().size()==3);
276 
277  exprt op0=expr.op0();
278  exprt op1=expr.op1();
279  exprt op2=expr.op2(); // rounding mode
280 
281  assert(ns.follow(op0.type())==type);
282  assert(ns.follow(op1.type())==type);
283 
284  // Remember that floating-point addition is _NOT_ associative.
285  // Thus, we don't re-sort the operands.
286  // We only merge constants!
287 
288  if(op0.is_constant() && op1.is_constant() && op2.is_constant())
289  {
290  ieee_floatt v0(to_constant_expr(op0));
291  ieee_floatt v1(to_constant_expr(op1));
292 
293  mp_integer rounding_mode;
294  if(!to_integer(op2, rounding_mode))
295  {
296  v0.rounding_mode=
299 
300  ieee_floatt result=v0;
301 
302  if(expr.id()==ID_floatbv_plus)
303  result+=v1;
304  else if(expr.id()==ID_floatbv_minus)
305  result-=v1;
306  else if(expr.id()==ID_floatbv_mult)
307  result*=v1;
308  else if(expr.id()==ID_floatbv_div)
309  result/=v1;
310  else
311  UNREACHABLE;
312 
313  expr=result.to_expr();
314  return false;
315  }
316  }
317 
318  // division by one? Exact for all rounding modes.
319  if(expr.id()==ID_floatbv_div &&
320  op1.is_constant() && op1.is_one())
321  {
322  exprt tmp;
323  tmp.swap(op0);
324  expr.swap(tmp);
325  return false;
326  }
327 
328  return true;
329 }
330 
332 {
333  assert(expr.id()==ID_ieee_float_equal ||
334  expr.id()==ID_ieee_float_notequal);
335 
336  exprt::operandst &operands=expr.operands();
337 
338  if(expr.type().id()!=ID_bool)
339  return true;
340 
341  if(operands.size()!=2)
342  return true;
343 
344  // types must match
345  if(expr.op0().type()!=expr.op1().type())
346  return true;
347 
348  if(expr.op0().type().id()!=ID_floatbv)
349  return true;
350 
351  // first see if we compare to a constant
352 
353  if(expr.op0().is_constant() &&
354  expr.op1().is_constant())
355  {
356  ieee_floatt f0(to_constant_expr(expr.op0()));
357  ieee_floatt f1(to_constant_expr(expr.op1()));
358 
359  if(expr.id()==ID_ieee_float_notequal)
360  expr.make_bool(f0.ieee_not_equal(f1));
361  else if(expr.id()==ID_ieee_float_equal)
362  expr.make_bool(f0.ieee_equal(f1));
363  else
364  UNREACHABLE;
365 
366  return false;
367  }
368 
369  if(expr.op0()==expr.op1())
370  {
371  // x!=x is the same as saying isnan(op)
372  isnan_exprt isnan(expr.op0());
373 
374  if(expr.id()==ID_ieee_float_notequal)
375  {
376  }
377  else if(expr.id()==ID_ieee_float_equal)
378  isnan.make_not();
379  else
380  UNREACHABLE;
381 
382  expr.swap(isnan);
383  return false;
384  }
385 
386  return true;
387 }
The type of an expression.
Definition: type.h:22
bool simplify_abs(exprt &expr)
BigInt mp_integer
Definition: mp_arith.h:22
bool simplify_sign(exprt &expr)
bool simplify_node(exprt &expr)
exprt & op0()
Definition: expr.h:72
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
The trinary if-then-else operator.
Definition: std_expr.h:3359
typet & type()
Definition: expr.h:56
bool is_NaN() const
Definition: ieee_float.h:237
void make_bool(bool value)
Definition: expr.cpp:138
void change_spec(const ieee_float_spect &dest_spec)
bool is_infinity() const
Definition: ieee_float.h:238
bool simplify_if(if_exprt &expr)
const irep_idt & id() const
Definition: irep.h:259
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3986
mp_integer to_integer() const
bool ieee_equal(const ieee_floatt &other) const
A generic base class for binary expressions.
Definition: std_expr.h:649
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:75
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
bool is_constant() const
Definition: expr.cpp:119
std::vector< exprt > operandst
Definition: expr.h:45
bool simplify_floatbv_typecast(exprt &expr)
void make_not()
Definition: expr.cpp:91
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1382
Base class for all expressions.
Definition: expr.h:42
bool simplify_ieee_float_relation(exprt &expr)
const namespacet & ns
#define UNREACHABLE
Definition: invariant.h:271
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:508
void swap(irept &irep)
Definition: irep.h:303
bool ieee_not_equal(const ieee_floatt &other) const
rounding_modet rounding_mode
Definition: ieee_float.h:132
exprt & op2()
Definition: expr.h:78
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
operandst & operands()
Definition: expr.h:66
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:205