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