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 "expr_util.h"
14 #include "ieee_float.h"
15 #include "invariant.h"
16 #include "namespace.h"
17 #include "simplify_expr.h"
18 #include "std_expr.h"
19 
22 {
23  if(expr.op().type().id() != ID_floatbv)
24  return unchanged(expr);
25 
26  if(expr.op().is_constant())
27  {
28  ieee_floatt value(to_constant_expr(expr.op()));
29  return make_boolean_expr(value.is_infinity());
30  }
31 
32  return unchanged(expr);
33 }
34 
37 {
38  if(expr.op().is_constant())
39  {
40  ieee_floatt value(to_constant_expr(expr.op()));
41  return make_boolean_expr(value.is_NaN());
42  }
43 
44  return unchanged(expr);
45 }
46 
49 {
50  if(expr.op().is_constant())
51  {
52  ieee_floatt value(to_constant_expr(expr.op()));
53  return make_boolean_expr(value.is_normal());
54  }
55 
56  return unchanged(expr);
57 }
58 
59 #if 0
61 {
62  if(expr.operands().size()!=1)
63  return true;
64 
65  if(expr.op0().is_constant())
66  {
67  const typet &type = expr.op0().type();
68 
69  if(type.id()==ID_floatbv)
70  {
71  ieee_floatt value(to_constant_expr(expr.op0()));
72  value.set_sign(false);
73  expr=value.to_expr();
74  return false;
75  }
76  else if(type.id()==ID_signedbv ||
77  type.id()==ID_unsignedbv)
78  {
79  mp_integer value;
80  if(!to_integer(expr.op0(), value))
81  {
82  if(value>=0)
83  {
84  expr=expr.op0();
85  return false;
86  }
87  else
88  {
89  value.negate();
90  expr=from_integer(value, type);
91  return false;
92  }
93  }
94  }
95  }
96 
97  return true;
98 }
99 #endif
100 
101 #if 0
103 {
104  if(expr.operands().size()!=1)
105  return true;
106 
107  if(expr.op0().is_constant())
108  {
109  const typet &type = expr.op0().type();
110 
111  if(type.id()==ID_floatbv)
112  {
113  ieee_floatt value(to_constant_expr(expr.op0()));
114  expr = make_boolean_expr(value.get_sign());
115  return false;
116  }
117  else if(type.id()==ID_signedbv ||
118  type.id()==ID_unsignedbv)
119  {
120  mp_integer value;
121  if(!to_integer(expr.op0(), value))
122  {
123  expr = make_boolean_expr(value>=0);
124  return false;
125  }
126  }
127  }
128 
129  return true;
130 }
131 #endif
132 
135 {
136  // These casts usually reduce precision, and thus, usually round.
137 
138  const typet &dest_type = expr.type();
139  const typet &src_type = expr.op().type();
140 
141  // eliminate redundant casts
142  if(dest_type==src_type)
143  return expr.op();
144 
145  const exprt &casted_expr = expr.op();
146  const exprt &rounding_mode = expr.rounding_mode();
147 
148  // We can soundly re-write (float)((double)x op (double)y)
149  // to x op y. True for any rounding mode!
150 
151  #if 0
152  if(casted_expr.id()==ID_floatbv_div ||
153  casted_expr.id()==ID_floatbv_mult ||
154  casted_expr.id()==ID_floatbv_plus ||
155  casted_expr.id()==ID_floatbv_minus)
156  {
157  if(casted_expr.operands().size()==3 &&
158  casted_expr.op0().id()==ID_typecast &&
159  casted_expr.op1().id()==ID_typecast &&
160  casted_expr.op0().operands().size()==1 &&
161  casted_expr.op1().operands().size()==1 &&
162  casted_expr.op0().type()==dest_type &&
163  casted_expr.op1().type()==dest_type)
164  {
165  exprt result(casted_expr.id(), floatbv_typecast_expr.type());
166  result.operands().resize(3);
167  result.op0()=casted_expr.op0().op0();
168  result.op1()=casted_expr.op1().op0();
169  result.op2()=rounding_mode;
170 
171  simplify_node(result);
172  expr.swap(result);
173  return false;
174  }
175  }
176  #endif
177 
178  // constant folding
179  if(casted_expr.is_constant() && rounding_mode.is_constant())
180  {
181  const auto rounding_mode_index = numeric_cast<mp_integer>(rounding_mode);
182  if(rounding_mode_index.has_value())
183  {
184  if(src_type.id()==ID_floatbv)
185  {
186  if(dest_type.id()==ID_floatbv) // float to float
187  {
188  ieee_floatt result(to_constant_expr(casted_expr));
189  result.rounding_mode =
190  (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
191  *rounding_mode_index);
192  result.change_spec(
193  ieee_float_spect(to_floatbv_type(dest_type)));
194  return result.to_expr();
195  }
196  else if(dest_type.id()==ID_signedbv ||
197  dest_type.id()==ID_unsignedbv)
198  {
199  if(*rounding_mode_index == ieee_floatt::ROUND_TO_ZERO)
200  {
201  ieee_floatt result(to_constant_expr(casted_expr));
202  result.rounding_mode =
203  (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
204  *rounding_mode_index);
205  mp_integer value=result.to_integer();
206  return from_integer(value, dest_type);
207  }
208  }
209  }
210  else if(src_type.id()==ID_signedbv ||
211  src_type.id()==ID_unsignedbv)
212  {
213  const auto value = numeric_cast<mp_integer>(casted_expr);
214  if(value.has_value())
215  {
216  if(dest_type.id()==ID_floatbv) // int to float
217  {
218  ieee_floatt result(to_floatbv_type(dest_type));
219  result.rounding_mode =
220  (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
221  *rounding_mode_index);
222  result.from_integer(*value);
223  return result.to_expr();
224  }
225  }
226  }
227  else if(src_type.id() == ID_c_enum_tag)
228  {
229  // go through underlying type
230  const auto &enum_type = ns.follow_tag(to_c_enum_tag_type(src_type));
231  exprt simplified_typecast =
232  simplify_expr(typecast_exprt(casted_expr, enum_type.subtype()), ns);
233  if(simplified_typecast.is_constant())
234  {
235  floatbv_typecast_exprt new_floatbv_typecast_expr = expr;
236  new_floatbv_typecast_expr.op() = simplified_typecast;
237 
238  auto r = simplify_floatbv_typecast(new_floatbv_typecast_expr);
239 
240  if(r.has_changed())
241  return r;
242  }
243  }
244  }
245  }
246 
247  #if 0
248  // (T)(a?b:c) --> a?(T)b:(T)c
249  if(casted_expr.id()==ID_if)
250  {
251  auto const &casted_if_expr = to_if_expr(casted_expr);
252 
253  floatbv_typecast_exprt casted_true_case(casted_if_expr.true_case(), rounding_mode, dest_type);
254  floatbv_typecast_exprt casted_false_case(casted_if_expr.false_case(), rounding_mode, dest_type);
255 
256  simplify_floatbv_typecast(casted_true_case);
257  simplify_floatbv_typecast(casted_false_case);
258  auto simplified_if_expr = simplify_expr(if_exprt(casted_if_expr.cond(), casted_true_case, casted_false_case, dest_type), ns);
259  expr = simplified_if_expr;
260  return false;
261  }
262  #endif
263 
264  return unchanged(expr);
265 }
266 
269 {
270  const typet &type = expr.type();
271 
272  PRECONDITION(type.id() == ID_floatbv);
273  PRECONDITION(
274  expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus ||
275  expr.id() == ID_floatbv_mult || expr.id() == ID_floatbv_div);
276 
277  const exprt &op0 = expr.lhs();
278  const exprt &op1 = expr.rhs();
279  const exprt &op2 = expr.rounding_mode();
280 
281  INVARIANT(
282  op0.type() == type,
283  "expression type of operand must match type of expression");
284  INVARIANT(
285  op1.type() == type,
286  "expression type of operand must match type of expression");
287 
288  // Remember that floating-point addition is _NOT_ associative.
289  // Thus, we don't re-sort the operands.
290  // We only merge constants!
291 
292  if(op0.is_constant() && op1.is_constant() && op2.is_constant())
293  {
294  ieee_floatt v0(to_constant_expr(op0));
295  ieee_floatt v1(to_constant_expr(op1));
296 
297  const auto rounding_mode = numeric_cast<mp_integer>(op2);
298  if(rounding_mode.has_value())
299  {
300  v0.rounding_mode =
301  (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
302  *rounding_mode);
304 
305  ieee_floatt result=v0;
306 
307  if(expr.id()==ID_floatbv_plus)
308  result+=v1;
309  else if(expr.id()==ID_floatbv_minus)
310  result-=v1;
311  else if(expr.id()==ID_floatbv_mult)
312  result*=v1;
313  else if(expr.id()==ID_floatbv_div)
314  result/=v1;
315  else
316  UNREACHABLE;
317 
318  return result.to_expr();
319  }
320  }
321 
322  // division by one? Exact for all rounding modes.
323  if(expr.id()==ID_floatbv_div &&
324  op1.is_constant() && op1.is_one())
325  {
326  return op0;
327  }
328 
329  return unchanged(expr);
330 }
331 
334 {
335  PRECONDITION(
336  expr.id() == ID_ieee_float_equal || expr.id() == ID_ieee_float_notequal);
337 
338  // types must match
339  if(expr.lhs().type() != expr.rhs().type())
340  return unchanged(expr);
341 
342  if(expr.lhs().type().id() != ID_floatbv)
343  return unchanged(expr);
344 
345  // first see if we compare to a constant
346 
347  if(expr.lhs().is_constant() && expr.rhs().is_constant())
348  {
349  ieee_floatt f_lhs(to_constant_expr(expr.lhs()));
350  ieee_floatt f_rhs(to_constant_expr(expr.rhs()));
351 
352  if(expr.id()==ID_ieee_float_notequal)
353  return make_boolean_expr(f_lhs.ieee_not_equal(f_rhs));
354  else if(expr.id()==ID_ieee_float_equal)
355  return make_boolean_expr(f_lhs.ieee_equal(f_rhs));
356  else
357  UNREACHABLE;
358  }
359 
360  if(expr.lhs() == expr.rhs())
361  {
362  // x!=x is the same as saying isnan(op)
363  exprt isnan = isnan_exprt(expr.lhs());
364 
365  if(expr.id()==ID_ieee_float_notequal)
366  {
367  }
368  else if(expr.id()==ID_ieee_float_equal)
369  isnan = not_exprt(isnan);
370  else
371  UNREACHABLE;
372 
373  return std::move(isnan);
374  }
375 
376  return unchanged(expr);
377 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
exprt::op2
exprt & op2()
Definition: expr.h:108
to_c_enum_tag_type
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:721
simplify_exprt::simplify_isnormal
resultt simplify_isnormal(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:48
ieee_floatt
Definition: ieee_float.h:120
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:641
simplify_expr_class.h
arith_tools.h
floatbv_typecast_exprt::op
exprt & op()
Definition: std_expr.h:2078
typet
The type of an expression, extends irept.
Definition: type.h:29
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
ieee_floatt::is_normal
bool is_normal() const
Definition: ieee_float.cpp:365
ieee_floatt::change_spec
void change_spec(const ieee_float_spect &dest_spec)
Definition: ieee_float.cpp:1044
exprt
Base class for all expressions.
Definition: expr.h:53
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:631
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:269
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
exprt::op0
exprt & op0()
Definition: expr.h:102
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
ieee_floatt::to_integer
mp_integer to_integer() const
Definition: ieee_float.cpp:1069
namespace.h
simplify_exprt::unchanged
static resultt unchanged(exprt expr)
Definition: simplify_expr_class.h:130
simplify_exprt::simplify_node
resultt simplify_node(exprt)
Definition: simplify_expr.cpp:2371
ieee_float_spect
Definition: ieee_float.h:26
expr.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
floatbv_typecast_exprt
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2067
simplify_exprt::simplify_isnan
resultt simplify_isnan(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:36
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
ieee_floatt::ieee_equal
bool ieee_equal(const ieee_floatt &other) const
Definition: ieee_float.cpp:1012
exprt::op1
exprt & op1()
Definition: expr.h:105
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
irept::swap
void swap(irept &irep)
Definition: irep.h:463
irept::id
const irep_idt & id() const
Definition: irep.h:418
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
ieee_floatt::rounding_modet
rounding_modet
Definition: ieee_float.h:126
simplify_exprt::resultt
Definition: simplify_expr_class.h:97
ieee_floatt::is_infinity
bool is_infinity() const
Definition: ieee_float.h:238
ieee_floatt::from_integer
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:511
ieee_floatt::rounding_mode
rounding_modet rounding_mode
Definition: ieee_float.h:132
simplify_expr.h
expr_util.h
Deprecated expression utility functions.
ieee_float_op_exprt::rounding_mode
exprt & rounding_mode()
Definition: std_expr.h:3821
ieee_floatt::ieee_not_equal
bool ieee_not_equal(const ieee_floatt &other) const
Definition: ieee_float.cpp:1034
floatbv_typecast_exprt::rounding_mode
exprt & rounding_mode()
Definition: std_expr.h:2088
simplify_exprt::simplify_sign
resultt simplify_sign(const sign_exprt &)
Definition: simplify_expr.cpp:101
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
ieee_float.h
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:85
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
invariant.h
ieee_float_op_exprt::lhs
exprt & lhs()
Definition: std_expr.h:3801
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
ieee_float_op_exprt
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: std_expr.h:3790
exprt::is_one
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:182
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:246
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
make_boolean_expr
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:283
exprt::operands
operandst & operands()
Definition: expr.h:95
r
static int8_t r
Definition: irep_hash.h:59
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
simplify_exprt::simplify_abs
resultt simplify_abs(const abs_exprt &)
Definition: simplify_expr.cpp:67
std_expr.h
API to expression classes.
simplify_exprt::simplify_ieee_float_relation
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
Definition: simplify_expr_floatbv.cpp:333
ieee_float_op_exprt::rhs
exprt & rhs()
Definition: std_expr.h:3811
ieee_floatt::ROUND_TO_ZERO
@ ROUND_TO_ZERO
Definition: ieee_float.h:128
validation_modet::INVARIANT
@ INVARIANT
simplify_exprt::simplify_floatbv_typecast
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
Definition: simplify_expr_floatbv.cpp:134
simplify_exprt::simplify_floatbv_op
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
Definition: simplify_expr_floatbv.cpp:268
isnan_exprt
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3509
not_exprt
Boolean negation.
Definition: std_expr.h:2843
ieee_floatt::is_NaN
bool is_NaN() const
Definition: ieee_float.h:237
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
simplify_exprt::simplify_isinf
resultt simplify_isinf(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:21