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