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