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 "arith_tools.h"
12 #include "expr.h"
13 #include "ieee_float.h"
14 #include "invariant.h"
15 #include "namespace.h"
16 #include "simplify_expr.h"
17 #include "std_expr.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  auto const &floatbv_typecast_expr = to_floatbv_typecast_expr(expr);
146 
147  const typet &dest_type = ns.follow(floatbv_typecast_expr.type());
148  const typet &src_type = ns.follow(floatbv_typecast_expr.op().type());
149 
150  // eliminate redundant casts
151  if(dest_type==src_type)
152  {
153  expr = floatbv_typecast_expr.op();
154  return false;
155  }
156 
157  const exprt &casted_expr = floatbv_typecast_expr.op();
158  const exprt &rounding_mode = floatbv_typecast_expr.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(casted_expr.id()==ID_floatbv_div ||
165  casted_expr.id()==ID_floatbv_mult ||
166  casted_expr.id()==ID_floatbv_plus ||
167  casted_expr.id()==ID_floatbv_minus)
168  {
169  if(casted_expr.operands().size()==3 &&
170  casted_expr.op0().id()==ID_typecast &&
171  casted_expr.op1().id()==ID_typecast &&
172  casted_expr.op0().operands().size()==1 &&
173  casted_expr.op1().operands().size()==1 &&
174  ns.follow(casted_expr.op0().type())==dest_type &&
175  ns.follow(casted_expr.op1().type())==dest_type)
176  {
177  exprt result(casted_expr.id(), floatbv_typecast_expr.type());
178  result.operands().resize(3);
179  result.op0()=casted_expr.op0().op0();
180  result.op1()=casted_expr.op1().op0();
181  result.op2()=rounding_mode;
182 
183  simplify_node(result);
184  expr.swap(result);
185  return false;
186  }
187  }
188  #endif
189 
190  // constant folding
191  if(casted_expr.is_constant() && rounding_mode.is_constant())
192  {
193  mp_integer rounding_mode_index;
194  if(!to_integer(rounding_mode, rounding_mode_index))
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(casted_expr));
201  result.rounding_mode =
202  (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
203  rounding_mode_index);
204  result.change_spec(
205  ieee_float_spect(to_floatbv_type(dest_type)));
206  expr=result.to_expr();
207  return false;
208  }
209  else if(dest_type.id()==ID_signedbv ||
210  dest_type.id()==ID_unsignedbv)
211  {
212  if(rounding_mode_index == ieee_floatt::ROUND_TO_ZERO)
213  {
214  ieee_floatt result(to_constant_expr(casted_expr));
215  result.rounding_mode =
216  (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
217  rounding_mode_index);
218  mp_integer value=result.to_integer();
219  expr=from_integer(value, dest_type);
220  return false;
221  }
222  }
223  }
224  else if(src_type.id()==ID_signedbv ||
225  src_type.id()==ID_unsignedbv)
226  {
227  mp_integer value;
228  if(!to_integer(casted_expr, value))
229  {
230  if(dest_type.id()==ID_floatbv) // int to float
231  {
232  ieee_floatt result(to_floatbv_type(dest_type));
233  result.rounding_mode =
234  (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
235  rounding_mode_index);
236  result.from_integer(value);
237  expr=result.to_expr();
238  return false;
239  }
240  }
241  }
242  else if(src_type.id() == ID_c_enum_tag)
243  {
244  // go through underlying type
245  const auto &enum_type = ns.follow_tag(to_c_enum_tag_type(src_type));
246  exprt simplified_typecast = simplify_expr(
247  typecast_exprt(casted_expr, to_c_enum_type(enum_type).subtype()), ns);
248  if(simplified_typecast.is_constant())
249  {
250  floatbv_typecast_exprt new_floatbv_typecast_expr =
251  floatbv_typecast_expr;
252  new_floatbv_typecast_expr.op() = simplified_typecast;
253  if(!simplify_floatbv_typecast(new_floatbv_typecast_expr))
254  {
255  expr = new_floatbv_typecast_expr;
256  return false;
257  }
258  }
259  }
260  }
261  }
262 
263  #if 0
264  // (T)(a?b:c) --> a?(T)b:(T)c
265  if(casted_expr.id()==ID_if)
266  {
267  auto const &casted_if_expr = to_if_expr(casted_expr);
268 
269  floatbv_typecast_exprt casted_true_case(casted_if_expr.true_case(), rounding_mode, dest_type);
270  floatbv_typecast_exprt casted_false_case(casted_if_expr.false_case(), rounding_mode, dest_type);
271 
272  simplify_floatbv_typecast(casted_true_case);
273  simplify_floatbv_typecast(casted_false_case);
274  auto simplified_if_expr = simplify_expr(if_exprt(casted_if_expr.cond(), casted_true_case, casted_false_case, dest_type), ns);
275  expr = simplified_if_expr;
276  return false;
277  }
278  #endif
279 
280  return true;
281 }
282 
284 {
285  const typet &type=ns.follow(expr.type());
286 
287  PRECONDITION(type.id() == ID_floatbv);
288  PRECONDITION(
289  expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus ||
290  expr.id() == ID_floatbv_mult || expr.id() == ID_floatbv_div);
292  expr.operands().size() == 3,
293  "binary operations have two operands, here an addtional parameter "
294  "is for the rounding mode");
295 
296  exprt op0=expr.op0();
297  exprt op1=expr.op1();
298  exprt op2=expr.op2(); // rounding mode
299 
300  INVARIANT(
301  ns.follow(op0.type()) == type,
302  "expression type of operand must match type of expression");
303  INVARIANT(
304  ns.follow(op1.type()) == type,
305  "expression type of operand must match type of expression");
306 
307  // Remember that floating-point addition is _NOT_ associative.
308  // Thus, we don't re-sort the operands.
309  // We only merge constants!
310 
311  if(op0.is_constant() && op1.is_constant() && op2.is_constant())
312  {
313  ieee_floatt v0(to_constant_expr(op0));
314  ieee_floatt v1(to_constant_expr(op1));
315 
316  mp_integer rounding_mode;
317  if(!to_integer(op2, rounding_mode))
318  {
319  v0.rounding_mode =
320  (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(rounding_mode);
322 
323  ieee_floatt result=v0;
324 
325  if(expr.id()==ID_floatbv_plus)
326  result+=v1;
327  else if(expr.id()==ID_floatbv_minus)
328  result-=v1;
329  else if(expr.id()==ID_floatbv_mult)
330  result*=v1;
331  else if(expr.id()==ID_floatbv_div)
332  result/=v1;
333  else
334  UNREACHABLE;
335 
336  expr=result.to_expr();
337  return false;
338  }
339  }
340 
341  // division by one? Exact for all rounding modes.
342  if(expr.id()==ID_floatbv_div &&
343  op1.is_constant() && op1.is_one())
344  {
345  exprt tmp;
346  tmp.swap(op0);
347  expr.swap(tmp);
348  return false;
349  }
350 
351  return true;
352 }
353 
355 {
356  PRECONDITION(
357  expr.id() == ID_ieee_float_equal || expr.id() == ID_ieee_float_notequal);
358 
359  exprt::operandst &operands=expr.operands();
360 
361  if(expr.type().id()!=ID_bool)
362  return true;
363 
364  if(operands.size()!=2)
365  return true;
366 
367  // types must match
368  if(expr.op0().type()!=expr.op1().type())
369  return true;
370 
371  if(expr.op0().type().id()!=ID_floatbv)
372  return true;
373 
374  // first see if we compare to a constant
375 
376  if(expr.op0().is_constant() &&
377  expr.op1().is_constant())
378  {
379  ieee_floatt f0(to_constant_expr(expr.op0()));
380  ieee_floatt f1(to_constant_expr(expr.op1()));
381 
382  if(expr.id()==ID_ieee_float_notequal)
383  expr.make_bool(f0.ieee_not_equal(f1));
384  else if(expr.id()==ID_ieee_float_equal)
385  expr.make_bool(f0.ieee_equal(f1));
386  else
387  UNREACHABLE;
388 
389  return false;
390  }
391 
392  if(expr.op0()==expr.op1())
393  {
394  // x!=x is the same as saying isnan(op)
395  exprt isnan = isnan_exprt(expr.op0());
396 
397  if(expr.id()==ID_ieee_float_notequal)
398  {
399  }
400  else if(expr.id()==ID_ieee_float_equal)
401  isnan = not_exprt(isnan);
402  else
403  UNREACHABLE;
404 
405  expr.swap(isnan);
406  return false;
407  }
408 
409  return true;
410 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
The type of an expression, extends irept.
Definition: type.h:27
bool simplify_abs(exprt &expr)
Boolean negation.
Definition: std_expr.h:3308
Semantic type conversion.
Definition: std_expr.h:2277
BigInt mp_integer
Definition: mp_arith.h:22
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:698
exprt simplify_expr(const exprt &src, const namespacet &ns)
The trinary if-then-else operator.
Definition: std_expr.h:3427
typet & type()
Return the type of the expression.
Definition: expr.h:68
bool is_NaN() const
Definition: ieee_float.h:237
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
Definition: expr.cpp:109
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
void change_spec(const ieee_float_spect &dest_spec)
bool is_infinity() const
Definition: ieee_float.h:238
const irep_idt & id() const
Definition: irep.h:259
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3989
mp_integer to_integer() const
bool ieee_equal(const ieee_floatt &other) const
bool simplify_floatbv_op(exprt &expr)
bool is_normal() const
Definition: ieee_float.cpp:366
API to expression classes.
bool simplify_isinf(exprt &expr)
exprt & op1()
Definition: expr.h:87
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:2378
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:737
std::vector< exprt > operandst
Definition: expr.h:57
bool simplify_floatbv_typecast(exprt &expr)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1442
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2336
Base class for all expressions.
Definition: expr.h:54
bool simplify_ieee_float_relation(exprt &expr)
const namespacet & ns
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:512
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:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:697
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
operandst & operands()
Definition: expr.h:78
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
Return whether the expression is a constant representing 1.
Definition: expr.cpp:180