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