cprover
Loading...
Searching...
No Matches
float_bv.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "float_bv.h"
10
11#include <algorithm>
12
13#include <util/arith_tools.h>
14#include <util/bitvector_expr.h>
16#include <util/floatbv_expr.h>
17#include <util/std_expr.h>
18
19exprt float_bvt::convert(const exprt &expr) const
20{
21 if(expr.id()==ID_abs)
22 return abs(to_abs_expr(expr).op(), get_spec(expr));
23 else if(expr.id()==ID_unary_minus)
24 return negation(to_unary_minus_expr(expr).op(), get_spec(expr));
25 else if(expr.id()==ID_ieee_float_equal)
26 {
27 const auto &equal_expr = to_ieee_float_equal_expr(expr);
28 return is_equal(
29 equal_expr.lhs(), equal_expr.rhs(), get_spec(equal_expr.lhs()));
30 }
31 else if(expr.id()==ID_ieee_float_notequal)
32 {
33 const auto &notequal_expr = to_ieee_float_notequal_expr(expr);
34 return not_exprt(is_equal(
35 notequal_expr.lhs(), notequal_expr.rhs(), get_spec(notequal_expr.lhs())));
36 }
37 else if(expr.id()==ID_floatbv_typecast)
38 {
39 const auto &floatbv_typecast_expr = to_floatbv_typecast_expr(expr);
40 const auto &op = floatbv_typecast_expr.op();
41 const typet &src_type = floatbv_typecast_expr.op().type();
42 const typet &dest_type = floatbv_typecast_expr.type();
43 const auto &rounding_mode = floatbv_typecast_expr.rounding_mode();
44
45 if(dest_type.id()==ID_signedbv &&
46 src_type.id()==ID_floatbv) // float -> signed
47 return to_signed_integer(
48 op,
49 to_signedbv_type(dest_type).get_width(),
50 rounding_mode,
51 get_spec(op));
52 else if(dest_type.id()==ID_unsignedbv &&
53 src_type.id()==ID_floatbv) // float -> unsigned
55 op,
56 to_unsignedbv_type(dest_type).get_width(),
57 rounding_mode,
58 get_spec(op));
59 else if(src_type.id()==ID_signedbv &&
60 dest_type.id()==ID_floatbv) // signed -> float
61 return from_signed_integer(op, rounding_mode, get_spec(expr));
62 else if(src_type.id()==ID_unsignedbv &&
63 dest_type.id()==ID_floatbv) // unsigned -> float
64 {
65 return from_unsigned_integer(op, rounding_mode, get_spec(expr));
66 }
67 else if(dest_type.id()==ID_floatbv &&
68 src_type.id()==ID_floatbv) // float -> float
69 {
70 return conversion(op, rounding_mode, get_spec(op), get_spec(expr));
71 }
72 else
73 return nil_exprt();
74 }
75 else if(
76 expr.id() == ID_typecast && expr.type().id() == ID_bool &&
77 to_typecast_expr(expr).op().type().id() == ID_floatbv) // float -> bool
78 {
79 return not_exprt(is_zero(to_typecast_expr(expr).op()));
80 }
81 else if(expr.id()==ID_floatbv_plus)
82 {
83 const auto &float_expr = to_ieee_float_op_expr(expr);
84 return add_sub(
85 false,
86 float_expr.lhs(),
87 float_expr.rhs(),
88 float_expr.rounding_mode(),
89 get_spec(expr));
90 }
91 else if(expr.id()==ID_floatbv_minus)
92 {
93 const auto &float_expr = to_ieee_float_op_expr(expr);
94 return add_sub(
95 true,
96 float_expr.lhs(),
97 float_expr.rhs(),
98 float_expr.rounding_mode(),
99 get_spec(expr));
100 }
101 else if(expr.id()==ID_floatbv_mult)
102 {
103 const auto &float_expr = to_ieee_float_op_expr(expr);
104 return mul(
105 float_expr.lhs(),
106 float_expr.rhs(),
107 float_expr.rounding_mode(),
108 get_spec(expr));
109 }
110 else if(expr.id()==ID_floatbv_div)
111 {
112 const auto &float_expr = to_ieee_float_op_expr(expr);
113 return div(
114 float_expr.lhs(),
115 float_expr.rhs(),
116 float_expr.rounding_mode(),
117 get_spec(expr));
118 }
119 else if(expr.id()==ID_isnan)
120 {
121 const auto &op = to_unary_expr(expr).op();
122 return isnan(op, get_spec(op));
123 }
124 else if(expr.id()==ID_isfinite)
125 {
126 const auto &op = to_unary_expr(expr).op();
127 return isfinite(op, get_spec(op));
128 }
129 else if(expr.id()==ID_isinf)
130 {
131 const auto &op = to_unary_expr(expr).op();
132 return isinf(op, get_spec(op));
133 }
134 else if(expr.id()==ID_isnormal)
135 {
136 const auto &op = to_unary_expr(expr).op();
137 return isnormal(op, get_spec(op));
138 }
139 else if(expr.id()==ID_lt)
140 {
141 const auto &rel_expr = to_binary_relation_expr(expr);
142 return relation(
143 rel_expr.lhs(), relt::LT, rel_expr.rhs(), get_spec(rel_expr.lhs()));
144 }
145 else if(expr.id()==ID_gt)
146 {
147 const auto &rel_expr = to_binary_relation_expr(expr);
148 return relation(
149 rel_expr.lhs(), relt::GT, rel_expr.rhs(), get_spec(rel_expr.lhs()));
150 }
151 else if(expr.id()==ID_le)
152 {
153 const auto &rel_expr = to_binary_relation_expr(expr);
154 return relation(
155 rel_expr.lhs(), relt::LE, rel_expr.rhs(), get_spec(rel_expr.lhs()));
156 }
157 else if(expr.id()==ID_ge)
158 {
159 const auto &rel_expr = to_binary_relation_expr(expr);
160 return relation(
161 rel_expr.lhs(), relt::GE, rel_expr.rhs(), get_spec(rel_expr.lhs()));
162 }
163 else if(expr.id()==ID_sign)
164 return sign_bit(to_unary_expr(expr).op());
165
166 return nil_exprt();
167}
168
170{
171 const floatbv_typet &type=to_floatbv_type(expr.type());
172 return ieee_float_spect(type);
173}
174
176{
177 // we mask away the sign bit, which is the most significant bit
178 const mp_integer v = power(2, spec.width() - 1) - 1;
179
180 const constant_exprt mask(integer2bvrep(v, spec.width()), op.type());
181
182 return bitand_exprt(op, mask);
183}
184
186{
187 // we flip the sign bit with an xor
188 const mp_integer v = power(2, spec.width() - 1);
189
190 constant_exprt mask(integer2bvrep(v, spec.width()), op.type());
191
192 return bitxor_exprt(op, mask);
193}
194
196 const exprt &src0,
197 const exprt &src1,
198 const ieee_float_spect &spec)
199{
200 // special cases: -0 and 0 are equal
201 const exprt is_zero0 = is_zero(src0);
202 const exprt is_zero1 = is_zero(src1);
203 const and_exprt both_zero(is_zero0, is_zero1);
204
205 // NaN compares to nothing
206 exprt isnan0=isnan(src0, spec);
207 exprt isnan1=isnan(src1, spec);
208 const or_exprt nan(isnan0, isnan1);
209
210 const equal_exprt bitwise_equal(src0, src1);
211
212 return and_exprt(
213 or_exprt(bitwise_equal, both_zero),
214 not_exprt(nan));
215}
216
218{
219 // we mask away the sign bit, which is the most significant bit
220 const floatbv_typet &type=to_floatbv_type(src.type());
221 std::size_t width=type.get_width();
222
223 const mp_integer v = power(2, width - 1) - 1;
224
225 constant_exprt mask(integer2bvrep(v, width), src.type());
226
227 ieee_floatt z(type);
228 z.make_zero();
229
230 return equal_exprt(bitand_exprt(src, mask), z.to_expr());
231}
232
234 const exprt &src,
235 const ieee_float_spect &spec)
236{
237 exprt exponent=get_exponent(src, spec);
238 exprt all_ones=to_unsignedbv_type(exponent.type()).largest_expr();
239 return equal_exprt(exponent, all_ones);
240}
241
243 const exprt &src,
244 const ieee_float_spect &spec)
245{
246 exprt exponent=get_exponent(src, spec);
247 exprt all_zeros=to_unsignedbv_type(exponent.type()).zero_expr();
248 return equal_exprt(exponent, all_zeros);
249}
250
252 const exprt &src,
253 const ieee_float_spect &spec)
254{
255 // does not include hidden bit
256 exprt fraction=get_fraction(src, spec);
257 exprt all_zeros=to_unsignedbv_type(fraction.type()).zero_expr();
258 return equal_exprt(fraction, all_zeros);
259}
260
262{
263 exprt round_to_even_const=from_integer(ieee_floatt::ROUND_TO_EVEN, rm.type());
264 exprt round_to_plus_inf_const=
266 exprt round_to_minus_inf_const=
268 exprt round_to_zero_const=from_integer(ieee_floatt::ROUND_TO_ZERO, rm.type());
269
270 round_to_even=equal_exprt(rm, round_to_even_const);
271 round_to_plus_inf=equal_exprt(rm, round_to_plus_inf_const);
272 round_to_minus_inf=equal_exprt(rm, round_to_minus_inf_const);
273 round_to_zero=equal_exprt(rm, round_to_zero_const);
274}
275
277{
278 const bitvector_typet &bv_type=to_bitvector_type(op.type());
279 std::size_t width=bv_type.get_width();
280 return extractbit_exprt(op, width-1);
281}
282
284 const exprt &src,
285 const exprt &rm,
286 const ieee_float_spect &spec) const
287{
288 std::size_t src_width=to_signedbv_type(src.type()).get_width();
289
290 unbiased_floatt result;
291
292 // we need to adjust for negative integers
293 result.sign=sign_bit(src);
294
295 result.fraction=
296 typecast_exprt(abs_exprt(src), unsignedbv_typet(src_width));
297
298 // build an exponent (unbiased) -- this is signed!
299 result.exponent=
301 src_width-1,
302 signedbv_typet(address_bits(src_width - 1) + 1));
303
304 return rounder(result, rm, spec);
305}
306
308 const exprt &src,
309 const exprt &rm,
310 const ieee_float_spect &spec) const
311{
312 unbiased_floatt result;
313
314 result.fraction=src;
315
316 std::size_t src_width=to_unsignedbv_type(src.type()).get_width();
317
318 // build an exponent (unbiased) -- this is signed!
319 result.exponent=
321 src_width-1,
322 signedbv_typet(address_bits(src_width - 1) + 1));
323
324 result.sign=false_exprt();
325
326 return rounder(result, rm, spec);
327}
328
330 const exprt &src,
331 std::size_t dest_width,
332 const exprt &rm,
333 const ieee_float_spect &spec)
334{
335 return to_integer(src, dest_width, true, rm, spec);
336}
337
339 const exprt &src,
340 std::size_t dest_width,
341 const exprt &rm,
342 const ieee_float_spect &spec)
343{
344 return to_integer(src, dest_width, false, rm, spec);
345}
346
348 const exprt &src,
349 std::size_t dest_width,
350 bool is_signed,
351 const exprt &rm,
352 const ieee_float_spect &spec)
353{
354 const unbiased_floatt unpacked=unpack(src, spec);
355
356 rounding_mode_bitst rounding_mode_bits(rm);
357
358 // Right now hard-wired to round-to-zero, which is
359 // the usual case in ANSI-C.
360
361 // if the exponent is positive, shift right
362 exprt offset=from_integer(spec.f, signedbv_typet(spec.e));
363 const minus_exprt distance(offset, unpacked.exponent);
364 const lshr_exprt shift_result(unpacked.fraction, distance);
365
366 // if the exponent is negative, we have zero anyways
367 exprt result=shift_result;
368 const sign_exprt exponent_sign(unpacked.exponent);
369
370 result=
371 if_exprt(exponent_sign, from_integer(0, result.type()), result);
372
373 // chop out the right number of bits from the result
374 typet result_type=
375 is_signed?static_cast<typet>(signedbv_typet(dest_width)):
376 static_cast<typet>(unsignedbv_typet(dest_width));
377
378 result=typecast_exprt(result, result_type);
379
380 // if signed, apply sign.
381 if(is_signed)
382 {
383 result=if_exprt(
384 unpacked.sign, unary_minus_exprt(result), result);
385 }
386 else
387 {
388 // It's unclear what the behaviour for negative floats
389 // to integer shall be.
390 }
391
392 return result;
393}
394
396 const exprt &src,
397 const exprt &rm,
398 const ieee_float_spect &src_spec,
399 const ieee_float_spect &dest_spec) const
400{
401 // Catch the special case in which we extend,
402 // e.g. single to double.
403 // In this case, rounding can be avoided,
404 // but a denormal number may be come normal.
405 // Be careful to exclude the difficult case
406 // when denormalised numbers in the old format
407 // can be converted to denormalised numbers in the
408 // new format. Note that this is rare and will only
409 // happen with very non-standard formats.
410
411 int sourceSmallestNormalExponent = -((1 << (src_spec.e - 1)) - 1);
412 int sourceSmallestDenormalExponent =
413 sourceSmallestNormalExponent - src_spec.f;
414
415 // Using the fact that f doesn't include the hidden bit
416
417 int destSmallestNormalExponent = -((1 << (dest_spec.e - 1)) - 1);
418
419 if(dest_spec.e>=src_spec.e &&
420 dest_spec.f>=src_spec.f &&
421 !(sourceSmallestDenormalExponent < destSmallestNormalExponent))
422 {
423 unbiased_floatt unpacked_src=unpack(src, src_spec);
424 unbiased_floatt result;
425
426 // the fraction gets zero-padded
427 std::size_t padding=dest_spec.f-src_spec.f;
428 result.fraction=
430 unpacked_src.fraction,
431 from_integer(0, unsignedbv_typet(padding)),
432 unsignedbv_typet(dest_spec.f+1));
433
434 // the exponent gets sign-extended
435 INVARIANT(
436 unpacked_src.exponent.type().id() == ID_signedbv,
437 "the exponent needs to have a signed type");
438 result.exponent=
439 typecast_exprt(unpacked_src.exponent, signedbv_typet(dest_spec.e));
440
441 // if the number was denormal and is normal in the new format,
442 // normalise it!
443 if(dest_spec.e > src_spec.e)
444 normalization_shift(result.fraction, result.exponent);
445
446 // the flags get copied
447 result.sign=unpacked_src.sign;
448 result.NaN=unpacked_src.NaN;
449 result.infinity=unpacked_src.infinity;
450
451 // no rounding needed!
452 return pack(bias(result, dest_spec), dest_spec);
453 }
454 else
455 {
456 // we actually need to round
457 unbiased_floatt result=unpack(src, src_spec);
458 return rounder(result, rm, dest_spec);
459 }
460}
461
463 const exprt &src,
464 const ieee_float_spect &spec)
465{
466 return and_exprt(
467 not_exprt(exponent_all_zeros(src, spec)),
468 not_exprt(exponent_all_ones(src, spec)));
469}
470
473 const unbiased_floatt &src1,
474 const unbiased_floatt &src2)
475{
476 // extend both by one bit
477 std::size_t old_width1=to_signedbv_type(src1.exponent.type()).get_width();
478 std::size_t old_width2=to_signedbv_type(src2.exponent.type()).get_width();
479 PRECONDITION(old_width1 == old_width2);
480
481 const typecast_exprt extended_exponent1(
482 src1.exponent, signedbv_typet(old_width1 + 1));
483
484 const typecast_exprt extended_exponent2(
485 src2.exponent, signedbv_typet(old_width2 + 1));
486
487 // compute shift distance (here is the subtraction)
488 return minus_exprt(extended_exponent1, extended_exponent2);
489}
490
492 bool subtract,
493 const exprt &op0,
494 const exprt &op1,
495 const exprt &rm,
496 const ieee_float_spect &spec) const
497{
498 unbiased_floatt unpacked1=unpack(op0, spec);
499 unbiased_floatt unpacked2=unpack(op1, spec);
500
501 // subtract?
502 if(subtract)
503 unpacked2.sign=not_exprt(unpacked2.sign);
504
505 // figure out which operand has the bigger exponent
506 const exprt exponent_difference=subtract_exponents(unpacked1, unpacked2);
507 const sign_exprt src2_bigger(exponent_difference);
508
509 const exprt bigger_exponent=
510 if_exprt(src2_bigger, unpacked2.exponent, unpacked1.exponent);
511
512 // swap fractions as needed
513 const exprt new_fraction1=
514 if_exprt(src2_bigger, unpacked2.fraction, unpacked1.fraction);
515
516 const exprt new_fraction2=
517 if_exprt(src2_bigger, unpacked1.fraction, unpacked2.fraction);
518
519 // compute distance
520 const exprt distance=
521 typecast_exprt(abs_exprt(exponent_difference), unsignedbv_typet(spec.e));
522
523 // limit the distance: shifting more than f+3 bits is unnecessary
524 const exprt limited_dist=limit_distance(distance, spec.f+3);
525
526 // pad fractions with 3 zeros from below
527 exprt three_zeros=from_integer(0, unsignedbv_typet(3));
528 // add 4 to spec.f because unpacked new_fraction has the hidden bit
529 const exprt fraction1_padded=
530 concatenation_exprt(new_fraction1, three_zeros, unsignedbv_typet(spec.f+4));
531 const exprt fraction2_padded=
532 concatenation_exprt(new_fraction2, three_zeros, unsignedbv_typet(spec.f+4));
533
534 // shift new_fraction2
535 exprt sticky_bit;
536 const exprt fraction1_shifted=fraction1_padded;
537 const exprt fraction2_shifted=sticky_right_shift(
538 fraction2_padded, limited_dist, sticky_bit);
539
540 // sticky bit: 'or' of the bits lost by the right-shift
541 const bitor_exprt fraction2_stickied(
542 fraction2_shifted,
544 from_integer(0, unsignedbv_typet(spec.f + 3)),
545 sticky_bit,
546 fraction2_shifted.type()));
547
548 // need to have two extra fraction bits for addition and rounding
549 const exprt fraction1_ext=
550 typecast_exprt(fraction1_shifted, unsignedbv_typet(spec.f+4+2));
551 const exprt fraction2_ext=
552 typecast_exprt(fraction2_stickied, unsignedbv_typet(spec.f+4+2));
553
554 unbiased_floatt result;
555
556 // now add/sub them
557 const notequal_exprt subtract_lit(unpacked1.sign, unpacked2.sign);
558
559 result.fraction=
560 if_exprt(subtract_lit,
561 minus_exprt(fraction1_ext, fraction2_ext),
562 plus_exprt(fraction1_ext, fraction2_ext));
563
564 // sign of result
565 std::size_t width=to_bitvector_type(result.fraction.type()).get_width();
566 const sign_exprt fraction_sign(
567 typecast_exprt(result.fraction, signedbv_typet(width)));
568 result.fraction=
571 unsignedbv_typet(width));
572
573 result.exponent=bigger_exponent;
574
575 // adjust the exponent for the fact that we added two bits to the fraction
576 result.exponent=
578 from_integer(2, signedbv_typet(spec.e+1)));
579
580 // NaN?
581 result.NaN=or_exprt(
582 and_exprt(and_exprt(unpacked1.infinity, unpacked2.infinity),
583 notequal_exprt(unpacked1.sign, unpacked2.sign)),
584 or_exprt(unpacked1.NaN, unpacked2.NaN));
585
586 // infinity?
587 result.infinity=and_exprt(
588 not_exprt(result.NaN),
589 or_exprt(unpacked1.infinity, unpacked2.infinity));
590
591 // zero?
592 // Note that:
593 // 1. The zero flag isn't used apart from in divide and
594 // is only set on unpack
595 // 2. Subnormals mean that addition or subtraction can't round to 0,
596 // thus we can perform this test now
597 // 3. The rules for sign are different for zero
598 result.zero=
599 and_exprt(
600 not_exprt(or_exprt(result.infinity, result.NaN)),
602 result.fraction,
603 from_integer(0, result.fraction.type())));
604
605 // sign
606 const notequal_exprt add_sub_sign(
607 if_exprt(src2_bigger, unpacked2.sign, unpacked1.sign), fraction_sign);
608
609 const if_exprt infinity_sign(
610 unpacked1.infinity, unpacked1.sign, unpacked2.sign);
611
612 #if 1
613 rounding_mode_bitst rounding_mode_bits(rm);
614
615 const if_exprt zero_sign(
616 rounding_mode_bits.round_to_minus_inf,
617 or_exprt(unpacked1.sign, unpacked2.sign),
618 and_exprt(unpacked1.sign, unpacked2.sign));
619
620 result.sign=if_exprt(
621 result.infinity,
622 infinity_sign,
623 if_exprt(result.zero,
624 zero_sign,
625 add_sub_sign));
626 #else
627 result.sign=if_exprt(
628 result.infinity,
629 infinity_sign,
630 add_sub_sign);
631 #endif
632
633 return rounder(result, rm, spec);
634}
635
638 const exprt &dist,
639 mp_integer limit)
640{
641 std::size_t nb_bits = address_bits(limit);
642 std::size_t dist_width=to_unsignedbv_type(dist.type()).get_width();
643
644 if(dist_width<=nb_bits)
645 return dist;
646
647 const extractbits_exprt upper_bits(
648 dist, dist_width - 1, nb_bits, unsignedbv_typet(dist_width - nb_bits));
649 const equal_exprt upper_bits_zero(
650 upper_bits, from_integer(0, upper_bits.type()));
651
652 const extractbits_exprt lower_bits(
653 dist, nb_bits - 1, 0, unsignedbv_typet(nb_bits));
654
655 return if_exprt(
656 upper_bits_zero,
657 lower_bits,
658 unsignedbv_typet(nb_bits).largest_expr());
659}
660
662 const exprt &src1,
663 const exprt &src2,
664 const exprt &rm,
665 const ieee_float_spect &spec) const
666{
667 // unpack
668 const unbiased_floatt unpacked1=unpack(src1, spec);
669 const unbiased_floatt unpacked2=unpack(src2, spec);
670
671 // zero-extend the fractions (unpacked fraction has the hidden bit)
672 typet new_fraction_type=unsignedbv_typet((spec.f+1)*2);
673 const exprt fraction1=typecast_exprt(unpacked1.fraction, new_fraction_type);
674 const exprt fraction2=typecast_exprt(unpacked2.fraction, new_fraction_type);
675
676 // multiply the fractions
677 unbiased_floatt result;
678 result.fraction=mult_exprt(fraction1, fraction2);
679
680 // extend exponents to account for overflow
681 // add two bits, as we do extra arithmetic on it later
682 typet new_exponent_type=signedbv_typet(spec.e+2);
683 const exprt exponent1=typecast_exprt(unpacked1.exponent, new_exponent_type);
684 const exprt exponent2=typecast_exprt(unpacked2.exponent, new_exponent_type);
685
686 const plus_exprt added_exponent(exponent1, exponent2);
687
688 // Adjust exponent; we are thowing in an extra fraction bit,
689 // it has been extended above.
690 result.exponent=
691 plus_exprt(added_exponent, from_integer(1, new_exponent_type));
692
693 // new sign
694 result.sign=notequal_exprt(unpacked1.sign, unpacked2.sign);
695
696 // infinity?
697 result.infinity=or_exprt(unpacked1.infinity, unpacked2.infinity);
698
699 // NaN?
700 result.NaN = disjunction(
701 {isnan(src1, spec),
702 isnan(src2, spec),
703 // infinity * 0 is NaN!
704 and_exprt(unpacked1.zero, unpacked2.infinity),
705 and_exprt(unpacked2.zero, unpacked1.infinity)});
706
707 return rounder(result, rm, spec);
708}
709
711 const exprt &src1,
712 const exprt &src2,
713 const exprt &rm,
714 const ieee_float_spect &spec) const
715{
716 // unpack
717 const unbiased_floatt unpacked1=unpack(src1, spec);
718 const unbiased_floatt unpacked2=unpack(src2, spec);
719
720 std::size_t fraction_width=
722 std::size_t div_width=fraction_width*2+1;
723
724 // pad fraction1 with zeros
725 const concatenation_exprt fraction1(
726 unpacked1.fraction,
727 from_integer(0, unsignedbv_typet(div_width - fraction_width)),
728 unsignedbv_typet(div_width));
729
730 // zero-extend fraction2 to match fraction1
731 const typecast_exprt fraction2(unpacked2.fraction, fraction1.type());
732
733 // divide fractions
734 unbiased_floatt result;
735 exprt rem;
736
737 // the below should be merged somehow
738 result.fraction=div_exprt(fraction1, fraction2);
739 rem=mod_exprt(fraction1, fraction2);
740
741 // is there a remainder?
742 const notequal_exprt have_remainder(rem, from_integer(0, rem.type()));
743
744 // we throw this into the result, as least-significant bit,
745 // to get the right rounding decision
746 result.fraction=
748 result.fraction, have_remainder, unsignedbv_typet(div_width+1));
749
750 // We will subtract the exponents;
751 // to account for overflow, we add a bit.
752 const typecast_exprt exponent1(
753 unpacked1.exponent, signedbv_typet(spec.e + 1));
754 const typecast_exprt exponent2(
755 unpacked2.exponent, signedbv_typet(spec.e + 1));
756
757 // subtract exponents
758 const minus_exprt added_exponent(exponent1, exponent2);
759
760 // adjust, as we have thown in extra fraction bits
761 result.exponent=plus_exprt(
762 added_exponent,
763 from_integer(spec.f, added_exponent.type()));
764
765 // new sign
766 result.sign=notequal_exprt(unpacked1.sign, unpacked2.sign);
767
768 // Infinity? This happens when
769 // 1) dividing a non-nan/non-zero by zero, or
770 // 2) first operand is inf and second is non-nan and non-zero
771 // In particular, inf/0=inf.
772 result.infinity=
773 or_exprt(
774 and_exprt(not_exprt(unpacked1.zero),
775 and_exprt(not_exprt(unpacked1.NaN),
776 unpacked2.zero)),
777 and_exprt(unpacked1.infinity,
778 and_exprt(not_exprt(unpacked2.NaN),
779 not_exprt(unpacked2.zero))));
780
781 // NaN?
782 result.NaN=or_exprt(unpacked1.NaN,
783 or_exprt(unpacked2.NaN,
784 or_exprt(and_exprt(unpacked1.zero, unpacked2.zero),
785 and_exprt(unpacked1.infinity, unpacked2.infinity))));
786
787 // Division by infinity produces zero, unless we have NaN
788 const and_exprt force_zero(not_exprt(unpacked1.NaN), unpacked2.infinity);
789
790 result.fraction=
791 if_exprt(
792 force_zero,
793 from_integer(0, result.fraction.type()),
794 result.fraction);
795
796 return rounder(result, rm, spec);
797}
798
800 const exprt &src1,
801 relt rel,
802 const exprt &src2,
803 const ieee_float_spect &spec)
804{
805 if(rel==relt::GT)
806 return relation(src2, relt::LT, src1, spec); // swapped
807 else if(rel==relt::GE)
808 return relation(src2, relt::LE, src1, spec); // swapped
809
810 INVARIANT(
811 rel == relt::EQ || rel == relt::LT || rel == relt::LE,
812 "relation should be equality, less-than, or less-or-equal");
813
814 // special cases: -0 and 0 are equal
815 const exprt is_zero1 = is_zero(src1);
816 const exprt is_zero2 = is_zero(src2);
817 const and_exprt both_zero(is_zero1, is_zero2);
818
819 // NaN compares to nothing
820 exprt isnan1=isnan(src1, spec);
821 exprt isnan2=isnan(src2, spec);
822 const or_exprt nan(isnan1, isnan2);
823
824 if(rel==relt::LT || rel==relt::LE)
825 {
826 const equal_exprt bitwise_equal(src1, src2);
827
828 // signs different? trivial! Unless Zero.
829
830 const notequal_exprt signs_different(sign_bit(src1), sign_bit(src2));
831
832 // as long as the signs match: compare like unsigned numbers
833
834 // this works due to the BIAS
835 const binary_relation_exprt less_than1(
837 typecast_exprt(src1, bv_typet(spec.width())),
838 unsignedbv_typet(spec.width())),
839 ID_lt,
841 typecast_exprt(src2, bv_typet(spec.width())),
842 unsignedbv_typet(spec.width())));
843
844 // if both are negative (and not the same), need to turn around!
845 const notequal_exprt less_than2(
846 less_than1, and_exprt(sign_bit(src1), sign_bit(src2)));
847
848 const if_exprt less_than3(signs_different, sign_bit(src1), less_than2);
849
850 if(rel==relt::LT)
851 {
852 and_exprt and_bv{{less_than3,
853 // for the case of two negative numbers
854 not_exprt(bitwise_equal),
855 not_exprt(both_zero),
856 not_exprt(nan)}};
857
858 return std::move(and_bv);
859 }
860 else if(rel==relt::LE)
861 {
862 or_exprt or_bv{{less_than3, both_zero, bitwise_equal}};
863
864 return and_exprt(or_bv, not_exprt(nan));
865 }
866 else
868 }
869 else if(rel==relt::EQ)
870 {
871 const equal_exprt bitwise_equal(src1, src2);
872
873 return and_exprt(
874 or_exprt(bitwise_equal, both_zero),
875 not_exprt(nan));
876 }
877
879 return false_exprt();
880}
881
883 const exprt &src,
884 const ieee_float_spect &spec)
885{
886 return and_exprt(
887 exponent_all_ones(src, spec),
888 fraction_all_zeros(src, spec));
889}
890
892 const exprt &src,
893 const ieee_float_spect &spec)
894{
895 return not_exprt(or_exprt(isinf(src, spec), isnan(src, spec)));
896}
897
900 const exprt &src,
901 const ieee_float_spect &spec)
902{
903 return extractbits_exprt(
904 src, spec.f+spec.e-1, spec.f,
905 unsignedbv_typet(spec.e));
906}
907
910 const exprt &src,
911 const ieee_float_spect &spec)
912{
913 return extractbits_exprt(
914 src, spec.f-1, 0,
915 unsignedbv_typet(spec.f));
916}
917
919 const exprt &src,
920 const ieee_float_spect &spec)
921{
922 return and_exprt(exponent_all_ones(src, spec),
923 not_exprt(fraction_all_zeros(src, spec)));
924}
925
928 exprt &fraction,
929 exprt &exponent)
930{
931 // n-log-n alignment shifter.
932 // The worst-case shift is the number of fraction
933 // bits minus one, in case the fraction is one exactly.
934 std::size_t fraction_bits=to_unsignedbv_type(fraction.type()).get_width();
935 std::size_t exponent_bits=to_signedbv_type(exponent.type()).get_width();
936 PRECONDITION(fraction_bits != 0);
937
938 std::size_t depth = address_bits(fraction_bits - 1);
939
940 if(exponent_bits<depth)
941 exponent=typecast_exprt(exponent, signedbv_typet(depth));
942
943 exprt exponent_delta=from_integer(0, exponent.type());
944
945 for(int d=depth-1; d>=0; d--)
946 {
947 unsigned distance=(1<<d);
948 INVARIANT(
949 fraction_bits > distance,
950 "distance must be within the range of fraction bits");
951
952 // check if first 'distance'-many bits are zeros
953 const extractbits_exprt prefix(
954 fraction,
955 fraction_bits - 1,
956 fraction_bits - distance,
957 unsignedbv_typet(distance));
958 const equal_exprt prefix_is_zero(prefix, from_integer(0, prefix.type()));
959
960 // If so, shift the zeros out left by 'distance'.
961 // Otherwise, leave as is.
962 const shl_exprt shifted(fraction, distance);
963
964 fraction=
965 if_exprt(prefix_is_zero, shifted, fraction);
966
967 // add corresponding weight to exponent
968 INVARIANT(
969 d < (signed int)exponent_bits,
970 "depth must be smaller than exponent bits");
971
972 exponent_delta=
973 bitor_exprt(exponent_delta,
974 shl_exprt(typecast_exprt(prefix_is_zero, exponent_delta.type()), d));
975 }
976
977 exponent=minus_exprt(exponent, exponent_delta);
978}
979
982 exprt &fraction,
983 exprt &exponent,
984 const ieee_float_spect &spec)
985{
986 mp_integer bias=spec.bias();
987
988 // Is the exponent strictly less than -bias+1, i.e., exponent<-bias+1?
989 // This is transformed to distance=(-bias+1)-exponent
990 // i.e., distance>0
991 // Note that 1-bias is the exponent represented by 0...01,
992 // i.e. the exponent of the smallest normal number and thus the 'base'
993 // exponent for subnormal numbers.
994
995 std::size_t exponent_bits=to_signedbv_type(exponent.type()).get_width();
996 PRECONDITION(exponent_bits >= spec.e);
997
998#if 1
999 // Need to sign extend to avoid overflow. Note that this is a
1000 // relatively rare problem as the value needs to be close to the top
1001 // of the exponent range and then range must not have been
1002 // previously extended as add, multiply, etc. do. This is primarily
1003 // to handle casting down from larger ranges.
1004 exponent=typecast_exprt(exponent, signedbv_typet(exponent_bits+1));
1005#endif
1006
1007 const minus_exprt distance(
1008 from_integer(-bias + 1, exponent.type()), exponent);
1009
1010 // use sign bit
1011 const and_exprt denormal(
1012 not_exprt(sign_exprt(distance)),
1013 notequal_exprt(distance, from_integer(0, distance.type())));
1014
1015#if 1
1016 // Care must be taken to not loose information required for the
1017 // guard and sticky bits. +3 is for the hidden, guard and sticky bits.
1018 std::size_t fraction_bits=to_unsignedbv_type(fraction.type()).get_width();
1019
1020 if(fraction_bits < spec.f+3)
1021 {
1022 // Add zeros at the LSB end for the guard bit to shift into
1023 fraction=
1025 fraction, unsignedbv_typet(spec.f + 3 - fraction_bits).zero_expr(),
1026 unsignedbv_typet(spec.f+3));
1027 }
1028
1029 exprt denormalisedFraction = fraction;
1030
1031 exprt sticky_bit = false_exprt();
1032 denormalisedFraction =
1033 sticky_right_shift(fraction, distance, sticky_bit);
1034
1035 denormalisedFraction=
1036 bitor_exprt(denormalisedFraction,
1037 typecast_exprt(sticky_bit, denormalisedFraction.type()));
1038
1039 fraction=
1040 if_exprt(
1041 denormal,
1042 denormalisedFraction,
1043 fraction);
1044
1045#else
1046 fraction=
1047 if_exprt(
1048 denormal,
1049 lshr_exprt(fraction, distance),
1050 fraction);
1051#endif
1052
1053 exponent=
1054 if_exprt(denormal,
1055 from_integer(-bias, exponent.type()),
1056 exponent);
1057}
1058
1060 const unbiased_floatt &src,
1061 const exprt &rm,
1062 const ieee_float_spect &spec) const
1063{
1064 // incoming: some fraction (with explicit 1),
1065 // some exponent without bias
1066 // outgoing: rounded, with right size, with hidden bit, bias
1067
1068 exprt aligned_fraction=src.fraction,
1069 aligned_exponent=src.exponent;
1070
1071 {
1072 std::size_t exponent_bits = std::max(address_bits(spec.f), spec.e) + 1;
1073
1074 // before normalization, make sure exponent is large enough
1075 if(to_signedbv_type(aligned_exponent.type()).get_width()<exponent_bits)
1076 {
1077 // sign extend
1078 aligned_exponent=
1079 typecast_exprt(aligned_exponent, signedbv_typet(exponent_bits));
1080 }
1081 }
1082
1083 // align it!
1084 normalization_shift(aligned_fraction, aligned_exponent);
1085 denormalization_shift(aligned_fraction, aligned_exponent, spec);
1086
1087 unbiased_floatt result;
1088 result.fraction=aligned_fraction;
1089 result.exponent=aligned_exponent;
1090 result.sign=src.sign;
1091 result.NaN=src.NaN;
1092 result.infinity=src.infinity;
1093
1094 rounding_mode_bitst rounding_mode_bits(rm);
1095 round_fraction(result, rounding_mode_bits, spec);
1096 round_exponent(result, rounding_mode_bits, spec);
1097
1098 return pack(bias(result, spec), spec);
1099}
1100
1103 const std::size_t dest_bits,
1104 const exprt sign,
1105 const exprt &fraction,
1106 const rounding_mode_bitst &rounding_mode_bits)
1107{
1108 std::size_t fraction_bits=
1109 to_unsignedbv_type(fraction.type()).get_width();
1110
1111 PRECONDITION(dest_bits < fraction_bits);
1112
1113 // we have too many fraction bits
1114 std::size_t extra_bits=fraction_bits-dest_bits;
1115
1116 // more than two extra bits are superflus, and are
1117 // turned into a sticky bit
1118
1119 exprt sticky_bit=false_exprt();
1120
1121 if(extra_bits>=2)
1122 {
1123 // We keep most-significant bits, and thus the tail is made
1124 // of least-significant bits.
1125 const extractbits_exprt tail(
1126 fraction, extra_bits - 2, 0, unsignedbv_typet(extra_bits - 2 + 1));
1127 sticky_bit=notequal_exprt(tail, from_integer(0, tail.type()));
1128 }
1129
1130 // the rounding bit is the last extra bit
1131 INVARIANT(
1132 extra_bits >= 1, "the extra bits contain at least the rounding bit");
1133 const extractbit_exprt rounding_bit(fraction, extra_bits - 1);
1134
1135 // we get one bit of the fraction for some rounding decisions
1136 const extractbit_exprt rounding_least(fraction, extra_bits);
1137
1138 // round-to-nearest (ties to even)
1139 const and_exprt round_to_even(
1140 rounding_bit, or_exprt(rounding_least, sticky_bit));
1141
1142 // round up
1143 const and_exprt round_to_plus_inf(
1144 not_exprt(sign), or_exprt(rounding_bit, sticky_bit));
1145
1146 // round down
1147 const and_exprt round_to_minus_inf(sign, or_exprt(rounding_bit, sticky_bit));
1148
1149 // round to zero
1150 false_exprt round_to_zero;
1151
1152 // now select appropriate one
1153 return if_exprt(rounding_mode_bits.round_to_even, round_to_even,
1154 if_exprt(rounding_mode_bits.round_to_plus_inf, round_to_plus_inf,
1155 if_exprt(rounding_mode_bits.round_to_minus_inf, round_to_minus_inf,
1156 if_exprt(rounding_mode_bits.round_to_zero, round_to_zero,
1157 false_exprt())))); // otherwise zero
1158}
1159
1161 unbiased_floatt &result,
1162 const rounding_mode_bitst &rounding_mode_bits,
1163 const ieee_float_spect &spec)
1164{
1165 std::size_t fraction_size=spec.f+1;
1166 std::size_t result_fraction_size=
1168
1169 // do we need to enlarge the fraction?
1170 if(result_fraction_size<fraction_size)
1171 {
1172 // pad with zeros at bottom
1173 std::size_t padding=fraction_size-result_fraction_size;
1174
1176 result.fraction,
1177 unsignedbv_typet(padding).zero_expr(),
1178 unsignedbv_typet(fraction_size));
1179 }
1180 else if(result_fraction_size==fraction_size) // it stays
1181 {
1182 // do nothing
1183 }
1184 else // fraction gets smaller -- rounding
1185 {
1186 std::size_t extra_bits=result_fraction_size-fraction_size;
1187 INVARIANT(
1188 extra_bits >= 1, "the extra bits include at least the rounding bit");
1189
1190 // this computes the rounding decision
1192 fraction_size, result.sign, result.fraction, rounding_mode_bits);
1193
1194 // chop off all the extra bits
1196 result.fraction, result_fraction_size-1, extra_bits,
1197 unsignedbv_typet(fraction_size));
1198
1199#if 0
1200 // *** does not catch when the overflow goes subnormal -> normal ***
1201 // incrementing the fraction might result in an overflow
1202 result.fraction=
1203 bv_utils.zero_extension(result.fraction, result.fraction.size()+1);
1204
1205 result.fraction=bv_utils.incrementer(result.fraction, increment);
1206
1207 exprt overflow=result.fraction.back();
1208
1209 // In case of an overflow, the exponent has to be incremented.
1210 // "Post normalization" is then required.
1211 result.exponent=
1212 bv_utils.incrementer(result.exponent, overflow);
1213
1214 // post normalization of the fraction
1215 exprt integer_part1=result.fraction.back();
1216 exprt integer_part0=result.fraction[result.fraction.size()-2];
1217 const or_exprt new_integer_part(integer_part1, integer_part0);
1218
1219 result.fraction.resize(result.fraction.size()-1);
1220 result.fraction.back()=new_integer_part;
1221
1222#else
1223 // When incrementing due to rounding there are two edge
1224 // cases we need to be aware of:
1225 // 1. If the number is normal, the increment can overflow.
1226 // In this case we need to increment the exponent and
1227 // set the MSB of the fraction to 1.
1228 // 2. If the number is the largest subnormal, the increment
1229 // can change the MSB making it normal. Thus the exponent
1230 // must be incremented but the fraction will be OK.
1231 const extractbit_exprt old_msb(result.fraction, fraction_size - 1);
1232
1233 // increment if 'increment' is true
1234 result.fraction=
1235 plus_exprt(result.fraction,
1236 typecast_exprt(increment, result.fraction.type()));
1237
1238 // Normal overflow when old MSB == 1 and new MSB == 0
1239 const extractbit_exprt new_msb(result.fraction, fraction_size - 1);
1240 const and_exprt overflow(old_msb, not_exprt(new_msb));
1241
1242 // Subnormal to normal transition when old MSB == 0 and new MSB == 1
1243 const and_exprt subnormal_to_normal(not_exprt(old_msb), new_msb);
1244
1245 // In case of an overflow or subnormal to normal conversion,
1246 // the exponent has to be incremented.
1247 result.exponent=
1248 plus_exprt(
1249 result.exponent,
1250 if_exprt(
1251 or_exprt(overflow, subnormal_to_normal),
1252 from_integer(1, result.exponent.type()),
1253 from_integer(0, result.exponent.type())));
1254
1255 // post normalization of the fraction
1256 // In the case of overflow, set the MSB to 1
1257 // The subnormal case will have (only) the MSB set to 1
1258 result.fraction=bitor_exprt(
1259 result.fraction,
1260 if_exprt(overflow,
1261 from_integer(1<<(fraction_size-1), result.fraction.type()),
1262 from_integer(0, result.fraction.type())));
1263#endif
1264 }
1265}
1266
1268 unbiased_floatt &result,
1269 const rounding_mode_bitst &rounding_mode_bits,
1270 const ieee_float_spect &spec)
1271{
1272 std::size_t result_exponent_size=
1274
1275 PRECONDITION(result_exponent_size >= spec.e);
1276
1277 // do we need to enlarge the exponent?
1278 if(result_exponent_size == spec.e) // it stays
1279 {
1280 // do nothing
1281 }
1282 else // exponent gets smaller -- chop off top bits
1283 {
1284 exprt old_exponent=result.exponent;
1285 result.exponent=
1286 extractbits_exprt(result.exponent, spec.e-1, 0, signedbv_typet(spec.e));
1287
1288 // max_exponent is the maximum representable
1289 // i.e. 1 higher than the maximum possible for a normal number
1290 exprt max_exponent=
1292 spec.max_exponent()-spec.bias(), old_exponent.type());
1293
1294 // the exponent is garbage if the fractional is zero
1295
1296 const and_exprt exponent_too_large(
1297 binary_relation_exprt(old_exponent, ID_ge, max_exponent),
1298 notequal_exprt(result.fraction, from_integer(0, result.fraction.type())));
1299
1300#if 1
1301 // Directed rounding modes round overflow to the maximum normal
1302 // depending on the particular mode and the sign
1303 const or_exprt overflow_to_inf(
1304 rounding_mode_bits.round_to_even,
1305 or_exprt(
1306 and_exprt(rounding_mode_bits.round_to_plus_inf, not_exprt(result.sign)),
1307 and_exprt(rounding_mode_bits.round_to_minus_inf, result.sign)));
1308
1309 const and_exprt set_to_max(exponent_too_large, not_exprt(overflow_to_inf));
1310
1311 exprt largest_normal_exponent=
1313 spec.max_exponent()-(spec.bias() + 1), result.exponent.type());
1314
1315 result.exponent=
1316 if_exprt(set_to_max, largest_normal_exponent, result.exponent);
1317
1318 result.fraction=
1319 if_exprt(set_to_max,
1321 result.fraction);
1322
1323 result.infinity=or_exprt(result.infinity,
1324 and_exprt(exponent_too_large,
1325 overflow_to_inf));
1326#else
1327 result.infinity=or_exprt(result.infinity, exponent_too_large);
1328#endif
1329 }
1330}
1331
1334 const unbiased_floatt &src,
1335 const ieee_float_spect &spec)
1336{
1337 biased_floatt result;
1338
1339 result.sign=src.sign;
1340 result.NaN=src.NaN;
1341 result.infinity=src.infinity;
1342
1343 // we need to bias the new exponent
1344 result.exponent=add_bias(src.exponent, spec);
1345
1346 // strip off the hidden bit
1348 to_unsignedbv_type(src.fraction.type()).get_width() == spec.f + 1);
1349
1350 const extractbit_exprt hidden_bit(src.fraction, spec.f);
1351 const not_exprt denormal(hidden_bit);
1352
1353 result.fraction=
1355 src.fraction, spec.f-1, 0,
1356 unsignedbv_typet(spec.f));
1357
1358 // make exponent zero if its denormal
1359 // (includes zero)
1360 result.exponent=
1361 if_exprt(denormal, from_integer(0, result.exponent.type()),
1362 result.exponent);
1363
1364 return result;
1365}
1366
1368 const exprt &src,
1369 const ieee_float_spect &spec)
1370{
1371 typet t=unsignedbv_typet(spec.e);
1372 return plus_exprt(
1373 typecast_exprt(src, t),
1374 from_integer(spec.bias(), t));
1375}
1376
1378 const exprt &src,
1379 const ieee_float_spect &spec)
1380{
1381 typet t=signedbv_typet(spec.e);
1382 return minus_exprt(
1383 typecast_exprt(src, t),
1384 from_integer(spec.bias(), t));
1385}
1386
1388 const exprt &src,
1389 const ieee_float_spect &spec)
1390{
1391 unbiased_floatt result;
1392
1393 result.sign=sign_bit(src);
1394
1395 result.fraction=get_fraction(src, spec);
1396
1397 // add hidden bit
1398 exprt hidden_bit=isnormal(src, spec);
1399 result.fraction=
1400 concatenation_exprt(hidden_bit, result.fraction,
1401 unsignedbv_typet(spec.f+1));
1402
1403 result.exponent=get_exponent(src, spec);
1404
1405 // unbias the exponent
1406 exprt denormal=exponent_all_zeros(src, spec);
1407
1408 result.exponent=
1409 if_exprt(denormal,
1410 from_integer(-spec.bias()+1, signedbv_typet(spec.e)),
1411 sub_bias(result.exponent, spec));
1412
1413 result.infinity=isinf(src, spec);
1414 result.zero = is_zero(src);
1415 result.NaN=isnan(src, spec);
1416
1417 return result;
1418}
1419
1421 const biased_floatt &src,
1422 const ieee_float_spect &spec)
1423{
1426
1427 // do sign -- we make this 'false' for NaN
1428 const if_exprt sign_bit(src.NaN, false_exprt(), src.sign);
1429
1430 // the fraction is zero in case of infinity,
1431 // and one in case of NaN
1432 const if_exprt fraction(
1433 src.NaN,
1434 from_integer(1, src.fraction.type()),
1435 if_exprt(src.infinity, from_integer(0, src.fraction.type()), src.fraction));
1436
1437 const or_exprt infinity_or_NaN(src.NaN, src.infinity);
1438
1439 // do exponent
1440 const if_exprt exponent(
1441 infinity_or_NaN, from_integer(-1, src.exponent.type()), src.exponent);
1442
1443 // stitch all three together
1444 return typecast_exprt(
1446 {std::move(sign_bit), std::move(exponent), std::move(fraction)},
1447 bv_typet(spec.f + spec.e + 1)),
1448 spec.to_type());
1449}
1450
1452 const exprt &op,
1453 const exprt &dist,
1454 exprt &sticky)
1455{
1456 std::size_t d=1, width=to_unsignedbv_type(op.type()).get_width();
1457 exprt result=op;
1458 sticky=false_exprt();
1459
1460 std::size_t dist_width=to_bitvector_type(dist.type()).get_width();
1461
1462 for(std::size_t stage=0; stage<dist_width; stage++)
1463 {
1464 const lshr_exprt tmp(result, d);
1465
1466 exprt lost_bits;
1467
1468 if(d<=width)
1469 lost_bits=extractbits_exprt(result, d-1, 0, unsignedbv_typet(d));
1470 else
1471 lost_bits=result;
1472
1473 const extractbit_exprt dist_bit(dist, stage);
1474
1475 sticky=
1476 or_exprt(
1477 and_exprt(
1478 dist_bit,
1479 notequal_exprt(lost_bits, from_integer(0, lost_bits.type()))),
1480 sticky);
1481
1482 result=if_exprt(dist_bit, tmp, result);
1483
1484 d=d<<1;
1485 }
1486
1487 return result;
1488}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
API to expression classes for bitvectors.
Pre-defined bitvector types.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Absolute value.
Definition std_expr.h:346
Boolean AND.
Definition std_expr.h:1974
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
Bit-wise AND.
Bit-wise OR.
Base class of fixed-width bit-vector types.
Definition std_types.h:853
std::size_t get_width() const
Definition std_types.h:864
Bit-wise XOR.
Fixed-width bit-vector without numerical interpretation.
Concatenation of bit-vector operands.
A constant literal expression.
Definition std_expr.h:2807
Division.
Definition std_expr.h:1064
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
Extracts a single bit of a bit-vector operand.
Extracts a sub-range of a bit-vector operand.
The Boolean constant false.
Definition std_expr.h:2865
static unbiased_floatt unpack(const exprt &, const ieee_float_spect &)
static void normalization_shift(exprt &fraction, exprt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
Definition float_bv.cpp:927
static exprt get_fraction(const exprt &, const ieee_float_spect &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
Definition float_bv.cpp:909
static exprt sub_bias(const exprt &exponent, const ieee_float_spect &)
static exprt exponent_all_ones(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:233
static exprt to_integer(const exprt &src, std::size_t dest_width, bool is_signed, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:347
exprt from_unsigned_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:307
static exprt isfinite(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:891
static exprt isnormal(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:462
exprt from_signed_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:283
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:491
static exprt is_zero(const exprt &)
Definition float_bv.cpp:217
static exprt abs(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:175
static void round_fraction(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
static exprt fraction_rounding_decision(const std::size_t dest_bits, const exprt sign, const exprt &fraction, const rounding_mode_bitst &)
rounding decision for fraction using sticky bit
exprt conversion(const exprt &src, const exprt &rm, const ieee_float_spect &src_spec, const ieee_float_spect &dest_spec) const
Definition float_bv.cpp:395
static exprt isnan(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:918
static biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &)
takes an unbiased float, and applies the bias
static exprt get_exponent(const exprt &, const ieee_float_spect &)
Gets the unbiased exponent in a floating-point bit-vector.
Definition float_bv.cpp:899
static void denormalization_shift(exprt &fraction, exprt &exponent, const ieee_float_spect &)
make sure exponent is not too small; the exponent is unbiased
Definition float_bv.cpp:981
static exprt add_bias(const exprt &exponent, const ieee_float_spect &)
static exprt sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky)
exprt rounder(const unbiased_floatt &, const exprt &rm, const ieee_float_spect &) const
static exprt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
Definition float_bv.cpp:472
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:710
exprt convert(const exprt &) const
Definition float_bv.cpp:19
static ieee_float_spect get_spec(const exprt &)
Definition float_bv.cpp:169
static exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:338
static exprt negation(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:185
static exprt relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:799
static exprt isinf(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:882
static exprt sign_bit(const exprt &)
Definition float_bv.cpp:276
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:661
static exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:251
static exprt exponent_all_zeros(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:242
static exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:195
static exprt to_signed_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:329
static exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
Definition float_bv.cpp:637
static exprt pack(const biased_floatt &, const ieee_float_spect &)
static void round_exponent(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
Fixed-width bit-vector with IEEE floating-point interpretation.
class floatbv_typet to_type() const
mp_integer bias() const
mp_integer max_exponent() const
std::size_t f
Definition ieee_float.h:27
std::size_t width() const
Definition ieee_float.h:51
std::size_t e
Definition ieee_float.h:27
constant_exprt to_expr() const
void make_zero()
Definition ieee_float.h:187
The trinary if-then-else operator.
Definition std_expr.h:2226
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
constant_exprt zero_expr() const
Return an expression representing the zero value of this type.
const irep_idt & id() const
Definition irep.h:396
Logical right shift.
Binary minus.
Definition std_expr.h:973
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1135
Binary multiplication Associativity is not specified.
Definition std_expr.h:1019
The NIL expression.
Definition std_expr.h:2874
Boolean negation.
Definition std_expr.h:2181
Disequality.
Definition std_expr.h:1283
Boolean OR.
Definition std_expr.h:2082
The plus expression Associativity is not specified.
Definition std_expr.h:914
Left shift.
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:506
Fixed-width bit-vector with two's complement interpretation.
Semantic type conversion.
Definition std_expr.h:1920
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:293
The unary minus expression.
Definition std_expr.h:390
Fixed-width bit-vector with unsigned binary interpretation.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const ieee_float_notequal_exprt & to_ieee_float_notequal_expr(const exprt &expr)
Cast an exprt to an ieee_float_notequal_exprt.
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast an exprt to an ieee_float_equal_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:22
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:807
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:328
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition std_expr.h:370
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:420
void get(const exprt &rm)
Definition float_bv.cpp:261
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45