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