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