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