CBMC
Loading...
Searching...
No Matches
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 {
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 {
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 {
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 {
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 {
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 auto &op = expr.op();
142 auto &rounding_mode = expr.rounding_mode();
143
144 // constant folding
145 if(op.is_constant() && rounding_mode.is_constant())
146 {
147 const auto rounding_mode_index =
149
153
154 return op_value.round_to_integral().to_expr();
155 }
156
157 return unchanged(expr);
158}
159
162{
163 // These casts usually reduce precision, and thus, usually round.
164
165 const typet &dest_type = expr.type();
166 const typet &src_type = expr.op().type();
167
168 // eliminate redundant casts
170 return expr.op();
171
172 const exprt &casted_expr = expr.op();
173 const exprt &rounding_mode = expr.rounding_mode();
174
175 // We can soundly re-write (float)((double)x op (double)y)
176 // to x op y. True for any rounding mode!
177
178 #if 0
179 if(casted_expr.id()==ID_floatbv_div ||
183 {
184 if(casted_expr.operands().size()==3 &&
185 casted_expr.op0().id()==ID_typecast &&
186 casted_expr.op1().id()==ID_typecast &&
187 casted_expr.op0().operands().size()==1 &&
188 casted_expr.op1().operands().size()==1 &&
189 casted_expr.op0().type()==dest_type &&
190 casted_expr.op1().type()==dest_type)
191 {
192 exprt result(casted_expr.id(), floatbv_typecast_expr.type());
193 result.operands().resize(3);
194 result.op0()=casted_expr.op0().op0();
195 result.op1()=casted_expr.op1().op0();
196 result.op2()=rounding_mode;
197
198 simplify_node(result);
199 expr.swap(result);
200 return false;
201 }
202 }
203 #endif
204
205 // constant folding
206 if(casted_expr.is_constant() && rounding_mode.is_constant())
207 {
208 const auto rounding_mode_index = numeric_cast<mp_integer>(rounding_mode);
209 if(rounding_mode_index.has_value())
210 {
211 if(src_type.id()==ID_floatbv)
212 {
213 if(dest_type.id()==ID_floatbv) // float to float
214 {
215 auto rounding_mode =
218 ieee_floatt result(to_constant_expr(casted_expr), rounding_mode);
219 result.change_spec(
221 return result.to_expr();
222 }
223 else if(dest_type.id()==ID_signedbv ||
225 {
227 {
228 auto rounding_mode =
231 ieee_floatt result(to_constant_expr(casted_expr), rounding_mode);
232 mp_integer value=result.to_integer();
233 return from_integer(value, dest_type);
234 }
235 }
236 }
237 else if(src_type.id()==ID_signedbv ||
239 {
240 const auto value = numeric_cast<mp_integer>(casted_expr);
241 if(value.has_value())
242 {
243 if(dest_type.id()==ID_floatbv) // int to float
244 {
245 auto rounding_mode =
248 ieee_floatt result(to_floatbv_type(dest_type), rounding_mode);
249 result.from_integer(*value);
250 return result.to_expr();
251 }
252 }
253 }
254 else if(src_type.id() == ID_c_enum_tag)
255 {
256 // go through underlying type
257 const auto &enum_type = ns.follow_tag(to_c_enum_tag_type(src_type));
259 typecast_exprt(casted_expr, enum_type.underlying_type()), ns);
260 if(simplified_typecast.is_constant())
261 {
264
266
267 if(r.has_changed())
268 return r;
269 }
270 }
271 }
272 }
273
274 #if 0
275 // (T)(a?b:c) --> a?(T)b:(T)c
276 if(casted_expr.id()==ID_if)
277 {
279
282
286 expr = simplified_if_expr;
287 return false;
288 }
289 #endif
290
291 return unchanged(expr);
292}
293
296{
297 const typet &type = expr.type();
298
299 PRECONDITION(type.id() == ID_floatbv);
301 expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus ||
302 expr.id() == ID_floatbv_mult || expr.id() == ID_floatbv_div);
303
304 const exprt &op0 = expr.lhs();
305 const exprt &op1 = expr.rhs();
306 const exprt &op2 = expr.rounding_mode();
307
308 INVARIANT(
309 op0.type() == type,
310 "expression type of operand must match type of expression");
311 INVARIANT(
312 op1.type() == type,
313 "expression type of operand must match type of expression");
314
315 // Remember that floating-point addition is _NOT_ associative.
316 // Thus, we don't re-sort the operands.
317 // We only merge constants!
318
319 if(op0.is_constant() && op1.is_constant() && op2.is_constant())
320 {
322
323 if(rounding_mode_opt.has_value())
324 {
325 const auto rounding_mode =
328
329 ieee_floatt v0(to_constant_expr(op0), rounding_mode);
330 ieee_floatt v1(to_constant_expr(op1), rounding_mode);
331
332 ieee_floatt result=v0;
333
334 if(expr.id()==ID_floatbv_plus)
335 result+=v1;
336 else if(expr.id()==ID_floatbv_minus)
337 result-=v1;
338 else if(expr.id()==ID_floatbv_mult)
339 result*=v1;
340 else if(expr.id()==ID_floatbv_div)
341 result/=v1;
342 else
344
345 return result.to_expr();
346 }
347 }
348
349 // division by one? Exact for all rounding modes.
350 if(expr.id()==ID_floatbv_div &&
351 op1.is_constant() && op1.is_one())
352 {
353 return op0;
354 }
355
356 return unchanged(expr);
357}
358
361{
363 expr.id() == ID_ieee_float_equal || expr.id() == ID_ieee_float_notequal);
364
365 // types must match
366 if(expr.lhs().type() != expr.rhs().type())
367 return unchanged(expr);
368
369 if(expr.lhs().type().id() != ID_floatbv)
370 return unchanged(expr);
371
372 // first see if we compare to a constant
373
374 if(expr.lhs().is_constant() && expr.rhs().is_constant())
375 {
378
379 if(expr.id()==ID_ieee_float_notequal)
380 return make_boolean_expr(f_lhs.ieee_not_equal(f_rhs));
381 else if(expr.id()==ID_ieee_float_equal)
382 return make_boolean_expr(f_lhs.ieee_equal(f_rhs));
383 else
385 }
386
387 // addition and multiplication are commutative, but not associative
388 exprt lhs_sorted = expr.lhs();
390 sort_operands(lhs_sorted.operands());
391 exprt rhs_sorted = expr.rhs();
393 sort_operands(rhs_sorted.operands());
394
396 {
397 // x!=x is the same as saying isnan(op)
398 exprt isnan = isnan_exprt(expr.lhs());
399
400 if(expr.id()==ID_ieee_float_notequal)
401 {
402 }
403 else if(expr.id()==ID_ieee_float_equal)
405 else
407
408 return std::move(isnan);
409 }
410
411 return unchanged(expr);
412}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
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:377
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
exprt & lhs()
Definition std_expr.h:668
exprt & rhs()
Definition std_expr.h:678
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
Base class for all expressions.
Definition expr.h:56
bool is_one() const
Return whether the expression is a constant representing 1.
Definition expr.cpp:96
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
exprt & op2()
Definition expr.h:139
Round a floating-point number to an integral value considering the given rounding mode.
Semantic type conversion from/to floating-point formats.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
An IEEE 754 floating-point value, including specificiation.
Definition ieee_float.h:117
bool is_NaN() const
Definition ieee_float.h:259
constant_exprt to_expr() const
bool is_normal() const
bool is_infinity() const
Definition ieee_float.h:260
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
Definition ieee_float.h:338
mp_integer to_integer() const
void from_integer(const mp_integer &i)
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
Definition std_expr.h:2497
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
Evaluates to true if the operand is NaN.
Boolean negation.
Definition std_expr.h:2454
resultt simplify_isnan(const unary_exprt &)
const namespacet & ns
resultt simplify_abs(const abs_exprt &)
resultt simplify_isnormal(const unary_exprt &)
resultt simplify_node(const exprt &)
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
resultt simplify_isinf(const unary_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
resultt simplify_sign(const sign_exprt &)
resultt simplify_floatbv_round_to_integral(const floatbv_round_to_integral_exprt &)
Semantic type conversion.
Definition std_expr.h:2073
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:361
const exprt & op() const
Definition std_expr.h:391
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
static int8_t r
Definition irep_hash.h:60
int isnan(double d)
Definition math.c:163
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:17
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172