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  exprt both_zero=and_exprt(is_zero0, is_zero1);
135 
136  // NaN compares to nothing
137  exprt isnan0=isnan(src0, spec);
138  exprt isnan1=isnan(src1, spec);
139  exprt nan=or_exprt(isnan0, isnan1);
140 
141  exprt bitwise_equal=equal_exprt(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).to_long()+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).to_long()+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  exprt distance=minus_exprt(offset, unpacked.exponent);
298  exprt shift_result=lshr_exprt(unpacked.fraction, distance);
299 
300  // if the exponent is negative, we have zero anyways
301  exprt result=shift_result;
302  exprt exponent_sign=sign_exprt(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  exprt extended_exponent1=
414  typecast_exprt(src1.exponent, signedbv_typet(old_width1+1));
415  exprt extended_exponent2=
416  typecast_exprt(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  exprt src2_bigger=sign_exprt(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  exprt fraction2_stickied=
475  bitor_exprt(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  exprt subtract_lit=
491  notequal_exprt(unpacked1.sign, unpacked2.sign);
492 
493  result.fraction=
494  if_exprt(subtract_lit,
495  minus_exprt(fraction1_ext, fraction2_ext),
496  plus_exprt(fraction1_ext, fraction2_ext));
497 
498  // sign of result
499  std::size_t width=to_bitvector_type(result.fraction.type()).get_width();
500  exprt fraction_sign=
502  result.fraction=
505  unsignedbv_typet(width));
506 
507  result.exponent=bigger_exponent;
508 
509  // adjust the exponent for the fact that we added two bits to the fraction
510  result.exponent=
512  from_integer(2, signedbv_typet(spec.e+1)));
513 
514  // NaN?
515  result.NaN=or_exprt(
516  and_exprt(and_exprt(unpacked1.infinity, unpacked2.infinity),
517  notequal_exprt(unpacked1.sign, unpacked2.sign)),
518  or_exprt(unpacked1.NaN, unpacked2.NaN));
519 
520  // infinity?
521  result.infinity=and_exprt(
522  not_exprt(result.NaN),
523  or_exprt(unpacked1.infinity, unpacked2.infinity));
524 
525  // zero?
526  // Note that:
527  // 1. The zero flag isn't used apart from in divide and
528  // is only set on unpack
529  // 2. Subnormals mean that addition or subtraction can't round to 0,
530  // thus we can perform this test now
531  // 3. The rules for sign are different for zero
532  result.zero=
533  and_exprt(
534  not_exprt(or_exprt(result.infinity, result.NaN)),
535  equal_exprt(
536  result.fraction,
537  from_integer(0, result.fraction.type())));
538 
539  // sign
540  exprt add_sub_sign=
541  notequal_exprt(if_exprt(src2_bigger, unpacked2.sign, unpacked1.sign),
542  fraction_sign);
543 
544  exprt infinity_sign=
545  if_exprt(unpacked1.infinity, unpacked1.sign, unpacked2.sign);
546 
547  #if 1
548  rounding_mode_bitst rounding_mode_bits(rm);
549 
550  exprt zero_sign=
551  if_exprt(rounding_mode_bits.round_to_minus_inf,
552  or_exprt(unpacked1.sign, unpacked2.sign),
553  and_exprt(unpacked1.sign, unpacked2.sign));
554 
555  result.sign=if_exprt(
556  result.infinity,
557  infinity_sign,
558  if_exprt(result.zero,
559  zero_sign,
560  add_sub_sign));
561  #else
562  result.sign=if_exprt(
563  result.infinity,
564  infinity_sign,
565  add_sub_sign);
566  #endif
567 
568  return rounder(result, rm, spec);
569 }
570 
573  const exprt &dist,
574  mp_integer limit)
575 {
576  std::size_t nb_bits=integer2unsigned(address_bits(limit));
577  std::size_t dist_width=to_unsignedbv_type(dist.type()).get_width();
578 
579  if(dist_width<=nb_bits)
580  return dist;
581 
582  exprt upper_bits=
583  extractbits_exprt(dist, dist_width-1, nb_bits,
584  unsignedbv_typet(dist_width-nb_bits));
585  exprt upper_bits_zero=
586  equal_exprt(upper_bits, from_integer(0, upper_bits.type()));
587 
588  exprt lower_bits=
589  extractbits_exprt(dist, nb_bits-1, 0,
590  unsignedbv_typet(nb_bits));
591 
592  return if_exprt(
593  upper_bits_zero,
594  lower_bits,
595  unsignedbv_typet(nb_bits).largest_expr());
596 }
597 
599  const exprt &src1,
600  const exprt &src2,
601  const exprt &rm,
602  const ieee_float_spect &spec)
603 {
604  // unpack
605  const unbiased_floatt unpacked1=unpack(src1, spec);
606  const unbiased_floatt unpacked2=unpack(src2, spec);
607 
608  // zero-extend the fractions (unpacked fraction has the hidden bit)
609  typet new_fraction_type=unsignedbv_typet((spec.f+1)*2);
610  const exprt fraction1=typecast_exprt(unpacked1.fraction, new_fraction_type);
611  const exprt fraction2=typecast_exprt(unpacked2.fraction, new_fraction_type);
612 
613  // multiply the fractions
614  unbiased_floatt result;
615  result.fraction=mult_exprt(fraction1, fraction2);
616 
617  // extend exponents to account for overflow
618  // add two bits, as we do extra arithmetic on it later
619  typet new_exponent_type=signedbv_typet(spec.e+2);
620  const exprt exponent1=typecast_exprt(unpacked1.exponent, new_exponent_type);
621  const exprt exponent2=typecast_exprt(unpacked2.exponent, new_exponent_type);
622 
623  exprt added_exponent=plus_exprt(exponent1, exponent2);
624 
625  // Adjust exponent; we are thowing in an extra fraction bit,
626  // it has been extended above.
627  result.exponent=
628  plus_exprt(added_exponent, from_integer(1, new_exponent_type));
629 
630  // new sign
631  result.sign=notequal_exprt(unpacked1.sign, unpacked2.sign);
632 
633  // infinity?
634  result.infinity=or_exprt(unpacked1.infinity, unpacked2.infinity);
635 
636  // NaN?
637  {
638  exprt NaN_cond(ID_or, bool_typet());
639 
640  NaN_cond.copy_to_operands(isnan(src1, spec));
641  NaN_cond.copy_to_operands(isnan(src2, spec));
642 
643  // infinity * 0 is NaN!
644  NaN_cond.copy_to_operands(and_exprt(unpacked1.zero, unpacked2.infinity));
645  NaN_cond.copy_to_operands(and_exprt(unpacked2.zero, unpacked1.infinity));
646 
647  result.NaN=NaN_cond;
648  }
649 
650  return rounder(result, rm, spec);
651 }
652 
654  const exprt &src1,
655  const exprt &src2,
656  const exprt &rm,
657  const ieee_float_spect &spec)
658 {
659  // unpack
660  const unbiased_floatt unpacked1=unpack(src1, spec);
661  const unbiased_floatt unpacked2=unpack(src2, spec);
662 
663  std::size_t fraction_width=
664  to_unsignedbv_type(unpacked1.fraction.type()).get_width();
665  std::size_t div_width=fraction_width*2+1;
666 
667  // pad fraction1 with zeros
668  exprt fraction1=
670  unpacked1.fraction,
671  from_integer(0, unsignedbv_typet(div_width-fraction_width)),
672  unsignedbv_typet(div_width));
673 
674  // zero-extend fraction2 to match faction1
675  const exprt fraction2=
676  typecast_exprt(unpacked2.fraction, fraction1.type());
677 
678  // divide fractions
679  unbiased_floatt result;
680  exprt rem;
681 
682  // the below should be merged somehow
683  result.fraction=div_exprt(fraction1, fraction2);
684  rem=mod_exprt(fraction1, fraction2);
685 
686  // is there a remainder?
687  exprt have_remainder=notequal_exprt(rem, from_integer(0, rem.type()));
688 
689  // we throw this into the result, as least-significant bit,
690  // to get the right rounding decision
691  result.fraction=
693  result.fraction, have_remainder, unsignedbv_typet(div_width+1));
694 
695  // We will subtract the exponents;
696  // to account for overflow, we add a bit.
697  const exprt exponent1=
698  typecast_exprt(unpacked1.exponent, signedbv_typet(spec.e+1));
699  const exprt exponent2=
700  typecast_exprt(unpacked2.exponent, signedbv_typet(spec.e+1));
701 
702  // subtract exponents
703  exprt added_exponent=minus_exprt(exponent1, exponent2);
704 
705  // adjust, as we have thown in extra fraction bits
706  result.exponent=plus_exprt(
707  added_exponent,
708  from_integer(spec.f, added_exponent.type()));
709 
710  // new sign
711  result.sign=notequal_exprt(unpacked1.sign, unpacked2.sign);
712 
713  // Infinity? This happens when
714  // 1) dividing a non-nan/non-zero by zero, or
715  // 2) first operand is inf and second is non-nan and non-zero
716  // In particular, inf/0=inf.
717  result.infinity=
718  or_exprt(
719  and_exprt(not_exprt(unpacked1.zero),
720  and_exprt(not_exprt(unpacked1.NaN),
721  unpacked2.zero)),
722  and_exprt(unpacked1.infinity,
723  and_exprt(not_exprt(unpacked2.NaN),
724  not_exprt(unpacked2.zero))));
725 
726  // NaN?
727  result.NaN=or_exprt(unpacked1.NaN,
728  or_exprt(unpacked2.NaN,
729  or_exprt(and_exprt(unpacked1.zero, unpacked2.zero),
730  and_exprt(unpacked1.infinity, unpacked2.infinity))));
731 
732  // Division by infinity produces zero, unless we have NaN
733  exprt force_zero=
734  and_exprt(not_exprt(unpacked1.NaN), unpacked2.infinity);
735 
736  result.fraction=
737  if_exprt(
738  force_zero,
739  from_integer(0, result.fraction.type()),
740  result.fraction);
741 
742  return rounder(result, rm, spec);
743 }
744 
746  const exprt &src1,
747  relt rel,
748  const exprt &src2,
749  const ieee_float_spect &spec)
750 {
751  if(rel==relt::GT)
752  return relation(src2, relt::LT, src1, spec); // swapped
753  else if(rel==relt::GE)
754  return relation(src2, relt::LE, src1, spec); // swapped
755 
756  assert(rel==relt::EQ || rel==relt::LT || rel==relt::LE);
757 
758  // special cases: -0 and 0 are equal
759  exprt is_zero1=is_zero(src1, spec);
760  exprt is_zero2=is_zero(src2, spec);
761  exprt both_zero=and_exprt(is_zero1, is_zero2);
762 
763  // NaN compares to nothing
764  exprt isnan1=isnan(src1, spec);
765  exprt isnan2=isnan(src2, spec);
766  exprt nan=or_exprt(isnan1, isnan2);
767 
768  if(rel==relt::LT || rel==relt::LE)
769  {
770  exprt bitwise_equal=equal_exprt(src1, src2);
771 
772  // signs different? trivial! Unless Zero.
773 
774  exprt signs_different=
775  notequal_exprt(sign_bit(src1), sign_bit(src2));
776 
777  // as long as the signs match: compare like unsigned numbers
778 
779  // this works due to the BIAS
780  exprt less_than1=
783  unsignedbv_typet(spec.width())),
784  ID_lt,
786  unsignedbv_typet(spec.width())));
787 
788  // if both are negative (and not the same), need to turn around!
789  exprt less_than2=
790  notequal_exprt(less_than1,
791  and_exprt(sign_bit(src1), sign_bit(src2)));
792 
793  exprt less_than3=
794  if_exprt(signs_different,
795  sign_bit(src1),
796  less_than2);
797 
798  if(rel==relt::LT)
799  {
800  exprt and_bv(ID_and, bool_typet());
801  and_bv.copy_to_operands(less_than3);
802  // for the case of two negative numbers
803  and_bv.copy_to_operands(not_exprt(bitwise_equal));
804  and_bv.copy_to_operands(not_exprt(both_zero));
805  and_bv.copy_to_operands(not_exprt(nan));
806 
807  return and_bv;
808  }
809  else if(rel==relt::LE)
810  {
811  exprt or_bv(ID_or, bool_typet());
812  or_bv.copy_to_operands(less_than3);
813  or_bv.copy_to_operands(both_zero);
814  or_bv.copy_to_operands(bitwise_equal);
815 
816  return and_exprt(or_bv, not_exprt(nan));
817  }
818  else
819  assert(false);
820  }
821  else if(rel==relt::EQ)
822  {
823  exprt bitwise_equal=equal_exprt(src1, src2);
824 
825  return and_exprt(
826  or_exprt(bitwise_equal, both_zero),
827  not_exprt(nan));
828  }
829  else
830  assert(0);
831 
832  // not reached
833  return false_exprt();
834 }
835 
837  const exprt &src,
838  const ieee_float_spect &spec)
839 {
840  return and_exprt(
841  exponent_all_ones(src, spec),
842  fraction_all_zeros(src, spec));
843 }
844 
846  const exprt &src,
847  const ieee_float_spect &spec)
848 {
849  return not_exprt(or_exprt(isinf(src, spec), isnan(src, spec)));
850 }
851 
854  const exprt &src,
855  const ieee_float_spect &spec)
856 {
857  return extractbits_exprt(
858  src, spec.f+spec.e-1, spec.f,
859  unsignedbv_typet(spec.e));
860 }
861 
864  const exprt &src,
865  const ieee_float_spect &spec)
866 {
867  return extractbits_exprt(
868  src, spec.f-1, 0,
869  unsignedbv_typet(spec.f));
870 }
871 
873  const exprt &src,
874  const ieee_float_spect &spec)
875 {
876  return and_exprt(exponent_all_ones(src, spec),
877  not_exprt(fraction_all_zeros(src, spec)));
878 }
879 
882  exprt &fraction,
883  exprt &exponent)
884 {
885  // n-log-n alignment shifter.
886  // The worst-case shift is the number of fraction
887  // bits minus one, in case the faction is one exactly.
888  std::size_t fraction_bits=to_unsignedbv_type(fraction.type()).get_width();
889  std::size_t exponent_bits=to_signedbv_type(exponent.type()).get_width();
890  assert(fraction_bits!=0);
891 
892  unsigned depth=integer2unsigned(address_bits(fraction_bits-1));
893 
894  if(exponent_bits<depth)
895  exponent=typecast_exprt(exponent, signedbv_typet(depth));
896 
897  exprt exponent_delta=from_integer(0, exponent.type());
898 
899  for(int d=depth-1; d>=0; d--)
900  {
901  unsigned distance=(1<<d);
902  assert(fraction_bits>distance);
903 
904  // check if first 'distance'-many bits are zeros
905  const exprt prefix=
906  extractbits_exprt(fraction, fraction_bits-1, fraction_bits-distance,
907  unsignedbv_typet(distance));
908  exprt prefix_is_zero=equal_exprt(prefix, from_integer(0, prefix.type()));
909 
910  // If so, shift the zeros out left by 'distance'.
911  // Otherwise, leave as is.
912  const exprt shifted=
913  shl_exprt(fraction, distance);
914 
915  fraction=
916  if_exprt(prefix_is_zero, shifted, fraction);
917 
918  // add corresponding weight to exponent
919  assert(d<(signed int)exponent_bits);
920 
921  exponent_delta=
922  bitor_exprt(exponent_delta,
923  shl_exprt(typecast_exprt(prefix_is_zero, exponent_delta.type()), d));
924  }
925 
926  exponent=minus_exprt(exponent, exponent_delta);
927 }
928 
931  exprt &fraction,
932  exprt &exponent,
933  const ieee_float_spect &spec)
934 {
935  mp_integer bias=spec.bias();
936 
937  // Is the exponent strictly less than -bias+1, i.e., exponent<-bias+1?
938  // This is transformed to distance=(-bias+1)-exponent
939  // i.e., distance>0
940  // Note that 1-bias is the exponent represented by 0...01,
941  // i.e. the exponent of the smallest normal number and thus the 'base'
942  // exponent for subnormal numbers.
943 
944  std::size_t exponent_bits=to_signedbv_type(exponent.type()).get_width();
945  assert(exponent_bits>=spec.e);
946 
947 #if 1
948  // Need to sign extend to avoid overflow. Note that this is a
949  // relatively rare problem as the value needs to be close to the top
950  // of the exponent range and then range must not have been
951  // previously extended as add, multiply, etc. do. This is primarily
952  // to handle casting down from larger ranges.
953  exponent=typecast_exprt(exponent, signedbv_typet(exponent_bits+1));
954 #endif
955 
956  exprt distance=minus_exprt(
957  from_integer(-bias+1, exponent.type()), exponent);
958 
959  // use sign bit
960  exprt denormal=
961  and_exprt(
962  not_exprt(sign_exprt(distance)),
963  notequal_exprt(distance, from_integer(0, distance.type())));
964 
965 #if 1
966  // Care must be taken to not loose information required for the
967  // guard and sticky bits. +3 is for the hidden, guard and sticky bits.
968  std::size_t fraction_bits=to_unsignedbv_type(fraction.type()).get_width();
969 
970  if(fraction_bits < spec.f+3)
971  {
972  // Add zeros at the LSB end for the guard bit to shift into
973  fraction=
975  fraction, unsignedbv_typet(spec.f + 3 - fraction_bits).zero_expr(),
976  unsignedbv_typet(spec.f+3));
977  }
978 
979  exprt denormalisedFraction = fraction;
980 
981  exprt sticky_bit = false_exprt();
982  denormalisedFraction =
983  sticky_right_shift(fraction, distance, sticky_bit);
984 
985  denormalisedFraction=
986  bitor_exprt(denormalisedFraction,
987  typecast_exprt(sticky_bit, denormalisedFraction.type()));
988 
989  fraction=
990  if_exprt(
991  denormal,
992  denormalisedFraction,
993  fraction);
994 
995 #else
996  fraction=
997  if_exprt(
998  denormal,
999  lshr_exprt(fraction, distance),
1000  fraction);
1001 #endif
1002 
1003  exponent=
1004  if_exprt(denormal,
1005  from_integer(-bias, exponent.type()),
1006  exponent);
1007 }
1008 
1010  const unbiased_floatt &src,
1011  const exprt &rm,
1012  const ieee_float_spect &spec)
1013 {
1014  // incoming: some fraction (with explicit 1),
1015  // some exponent without bias
1016  // outgoing: rounded, with right size, with hidden bit, bias
1017 
1018  exprt aligned_fraction=src.fraction,
1019  aligned_exponent=src.exponent;
1020 
1021  {
1022  std::size_t exponent_bits=
1023  std::max((std::size_t)integer2size_t(address_bits(spec.f)),
1024  (std::size_t)spec.e)+1;
1025 
1026  // before normalization, make sure exponent is large enough
1027  if(to_signedbv_type(aligned_exponent.type()).get_width()<exponent_bits)
1028  {
1029  // sign extend
1030  aligned_exponent=
1031  typecast_exprt(aligned_exponent, signedbv_typet(exponent_bits));
1032  }
1033  }
1034 
1035  // align it!
1036  normalization_shift(aligned_fraction, aligned_exponent);
1037  denormalization_shift(aligned_fraction, aligned_exponent, spec);
1038 
1039  unbiased_floatt result;
1040  result.fraction=aligned_fraction;
1041  result.exponent=aligned_exponent;
1042  result.sign=src.sign;
1043  result.NaN=src.NaN;
1044  result.infinity=src.infinity;
1045 
1046  rounding_mode_bitst rounding_mode_bits(rm);
1047  round_fraction(result, rounding_mode_bits, spec);
1048  round_exponent(result, rounding_mode_bits, spec);
1049 
1050  return pack(bias(result, spec), spec);
1051 }
1052 
1055  const std::size_t dest_bits,
1056  const exprt sign,
1057  const exprt &fraction,
1058  const rounding_mode_bitst &rounding_mode_bits)
1059 {
1060  std::size_t fraction_bits=
1061  to_unsignedbv_type(fraction.type()).get_width();
1062 
1063  assert(dest_bits<fraction_bits);
1064 
1065  // we have too many fraction bits
1066  std::size_t extra_bits=fraction_bits-dest_bits;
1067 
1068  // more than two extra bits are superflus, and are
1069  // turned into a sticky bit
1070 
1071  exprt sticky_bit=false_exprt();
1072 
1073  if(extra_bits>=2)
1074  {
1075  // We keep most-significant bits, and thus the tail is made
1076  // of least-significant bits.
1077  exprt tail=
1078  extractbits_exprt(fraction, extra_bits-2, 0,
1079  unsignedbv_typet(extra_bits-2+1));
1080  sticky_bit=notequal_exprt(tail, from_integer(0, tail.type()));
1081  }
1082 
1083  // the rounding bit is the last extra bit
1084  assert(extra_bits>=1);
1085  exprt rounding_bit=extractbit_exprt(fraction, extra_bits-1);
1086 
1087  // we get one bit of the fraction for some rounding decisions
1088  exprt rounding_least=extractbit_exprt(fraction, extra_bits);
1089 
1090  // round-to-nearest (ties to even)
1091  exprt round_to_even=
1092  and_exprt(rounding_bit,
1093  or_exprt(rounding_least, sticky_bit));
1094 
1095  // round up
1096  exprt round_to_plus_inf=
1097  and_exprt(not_exprt(sign),
1098  or_exprt(rounding_bit, sticky_bit));
1099 
1100  // round down
1101  exprt round_to_minus_inf=
1102  and_exprt(sign,
1103  or_exprt(rounding_bit, sticky_bit));
1104 
1105  // round to zero
1106  exprt round_to_zero=
1107  false_exprt();
1108 
1109  // now select appropriate one
1110  return if_exprt(rounding_mode_bits.round_to_even, round_to_even,
1111  if_exprt(rounding_mode_bits.round_to_plus_inf, round_to_plus_inf,
1112  if_exprt(rounding_mode_bits.round_to_minus_inf, round_to_minus_inf,
1113  if_exprt(rounding_mode_bits.round_to_zero, round_to_zero,
1114  false_exprt())))); // otherwise zero
1115 }
1116 
1118  unbiased_floatt &result,
1119  const rounding_mode_bitst &rounding_mode_bits,
1120  const ieee_float_spect &spec)
1121 {
1122  std::size_t fraction_size=spec.f+1;
1123  std::size_t result_fraction_size=
1124  to_unsignedbv_type(result.fraction.type()).get_width();
1125 
1126  // do we need to enlarge the fraction?
1127  if(result_fraction_size<fraction_size)
1128  {
1129  // pad with zeros at bottom
1130  std::size_t padding=fraction_size-result_fraction_size;
1131 
1133  result.fraction,
1134  unsignedbv_typet(padding).zero_expr(),
1135  unsignedbv_typet(fraction_size));
1136  }
1137  else if(result_fraction_size==fraction_size) // it stays
1138  {
1139  // do nothing
1140  }
1141  else // fraction gets smaller -- rounding
1142  {
1143  std::size_t extra_bits=result_fraction_size-fraction_size;
1144  assert(extra_bits>=1);
1145 
1146  // this computes the rounding decision
1148  fraction_size, result.sign, result.fraction, rounding_mode_bits);
1149 
1150  // chop off all the extra bits
1151  result.fraction=extractbits_exprt(
1152  result.fraction, result_fraction_size-1, extra_bits,
1153  unsignedbv_typet(fraction_size));
1154 
1155 #if 0
1156  // *** does not catch when the overflow goes subnormal -> normal ***
1157  // incrementing the fraction might result in an overflow
1158  result.fraction=
1159  bv_utils.zero_extension(result.fraction, result.fraction.size()+1);
1160 
1161  result.fraction=bv_utils.incrementer(result.fraction, increment);
1162 
1163  exprt overflow=result.fraction.back();
1164 
1165  // In case of an overflow, the exponent has to be incremented.
1166  // "Post normalization" is then required.
1167  result.exponent=
1168  bv_utils.incrementer(result.exponent, overflow);
1169 
1170  // post normalization of the fraction
1171  exprt integer_part1=result.fraction.back();
1172  exprt integer_part0=result.fraction[result.fraction.size()-2];
1173  exprt new_integer_part=or_exprt(integer_part1, integer_part0);
1174 
1175  result.fraction.resize(result.fraction.size()-1);
1176  result.fraction.back()=new_integer_part;
1177 
1178 #else
1179  // When incrementing due to rounding there are two edge
1180  // cases we need to be aware of:
1181  // 1. If the number is normal, the increment can overflow.
1182  // In this case we need to increment the exponent and
1183  // set the MSB of the fraction to 1.
1184  // 2. If the number is the largest subnormal, the increment
1185  // can change the MSB making it normal. Thus the exponent
1186  // must be incremented but the fraction will be OK.
1187  exprt oldMSB=
1188  extractbit_exprt(result.fraction, fraction_size-1);
1189 
1190  // increment if 'increment' is true
1191  result.fraction=
1192  plus_exprt(result.fraction,
1193  typecast_exprt(increment, result.fraction.type()));
1194 
1195  // Normal overflow when old MSB == 1 and new MSB == 0
1196  exprt newMSB=
1197  extractbit_exprt(result.fraction, fraction_size-1);
1198 
1199  exprt overflow=and_exprt(oldMSB, not_exprt(newMSB));
1200 
1201  // Subnormal to normal transition when old MSB == 0 and new MSB == 1
1202  exprt subnormal_to_normal=
1203  and_exprt(not_exprt(oldMSB), newMSB);
1204 
1205  // In case of an overflow or subnormal to normal conversion,
1206  // the exponent has to be incremented.
1207  result.exponent=
1208  plus_exprt(
1209  result.exponent,
1210  if_exprt(
1211  or_exprt(overflow, subnormal_to_normal),
1212  from_integer(1, result.exponent.type()),
1213  from_integer(0, result.exponent.type())));
1214 
1215  // post normalization of the fraction
1216  // In the case of overflow, set the MSB to 1
1217  // The subnormal case will have (only) the MSB set to 1
1218  result.fraction=bitor_exprt(
1219  result.fraction,
1220  if_exprt(overflow,
1221  from_integer(1<<(fraction_size-1), result.fraction.type()),
1222  from_integer(0, result.fraction.type())));
1223 #endif
1224  }
1225 }
1226 
1228  unbiased_floatt &result,
1229  const rounding_mode_bitst &rounding_mode_bits,
1230  const ieee_float_spect &spec)
1231 {
1232  std::size_t result_exponent_size=
1233  to_signedbv_type(result.exponent.type()).get_width();
1234 
1235  // do we need to enlarge the exponent?
1236  if(result_exponent_size<spec.e)
1237  {
1238  // should have been done before
1239  assert(false);
1240  }
1241  else if(result_exponent_size==spec.e) // it stays
1242  {
1243  // do nothing
1244  }
1245  else // exponent gets smaller -- chop off top bits
1246  {
1247  exprt old_exponent=result.exponent;
1248  result.exponent=
1249  extractbits_exprt(result.exponent, spec.e-1, 0, signedbv_typet(spec.e));
1250 
1251  // max_exponent is the maximum representable
1252  // i.e. 1 higher than the maximum possible for a normal number
1253  exprt max_exponent=
1254  from_integer(
1255  spec.max_exponent()-spec.bias(), old_exponent.type());
1256 
1257  // the exponent is garbage if the fractional is zero
1258 
1259  exprt exponent_too_large=
1260  and_exprt(
1261  binary_relation_exprt(old_exponent, ID_ge, max_exponent),
1263  result.fraction,
1264  from_integer(0, result.fraction.type())));
1265 
1266 #if 1
1267  // Directed rounding modes round overflow to the maximum normal
1268  // depending on the particular mode and the sign
1269  exprt overflow_to_inf=
1270  or_exprt(rounding_mode_bits.round_to_even,
1271  or_exprt(and_exprt(rounding_mode_bits.round_to_plus_inf,
1272  not_exprt(result.sign)),
1273  and_exprt(rounding_mode_bits.round_to_minus_inf,
1274  result.sign)));
1275 
1276  exprt set_to_max=
1277  and_exprt(exponent_too_large, not_exprt(overflow_to_inf));
1278 
1279 
1280  exprt largest_normal_exponent=
1281  from_integer(
1282  spec.max_exponent()-(spec.bias() + 1), result.exponent.type());
1283 
1284  result.exponent=
1285  if_exprt(set_to_max, largest_normal_exponent, result.exponent);
1286 
1287  result.fraction=
1288  if_exprt(set_to_max,
1289  to_unsignedbv_type(result.fraction.type()).largest_expr(),
1290  result.fraction);
1291 
1292  result.infinity=or_exprt(result.infinity,
1293  and_exprt(exponent_too_large,
1294  overflow_to_inf));
1295 #else
1296  result.infinity=or_exprt(result.infinity, exponent_too_large);
1297 #endif
1298  }
1299 }
1300 
1303  const unbiased_floatt &src,
1304  const ieee_float_spect &spec)
1305 {
1306  biased_floatt result;
1307 
1308  result.sign=src.sign;
1309  result.NaN=src.NaN;
1310  result.infinity=src.infinity;
1311 
1312  // we need to bias the new exponent
1313  result.exponent=add_bias(src.exponent, spec);
1314 
1315  // strip off the hidden bit
1316  assert(to_unsignedbv_type(src.fraction.type()).get_width()==spec.f+1);
1317 
1318  exprt hidden_bit=extractbit_exprt(src.fraction, spec.f);
1319  exprt denormal=not_exprt(hidden_bit);
1320 
1321  result.fraction=
1323  src.fraction, spec.f-1, 0,
1324  unsignedbv_typet(spec.f));
1325 
1326  // make exponent zero if its denormal
1327  // (includes zero)
1328  result.exponent=
1329  if_exprt(denormal, from_integer(0, result.exponent.type()),
1330  result.exponent);
1331 
1332  return result;
1333 }
1334 
1336  const exprt &src,
1337  const ieee_float_spect &spec)
1338 {
1339  typet t=unsignedbv_typet(spec.e);
1340  return plus_exprt(
1341  typecast_exprt(src, t),
1342  from_integer(spec.bias(), t));
1343 }
1344 
1346  const exprt &src,
1347  const ieee_float_spect &spec)
1348 {
1349  typet t=signedbv_typet(spec.e);
1350  return minus_exprt(
1351  typecast_exprt(src, t),
1352  from_integer(spec.bias(), t));
1353 }
1354 
1356  const exprt &src,
1357  const ieee_float_spect &spec)
1358 {
1359  unbiased_floatt result;
1360 
1361  result.sign=sign_bit(src);
1362 
1363  result.fraction=get_fraction(src, spec);
1364 
1365  // add hidden bit
1366  exprt hidden_bit=isnormal(src, spec);
1367  result.fraction=
1368  concatenation_exprt(hidden_bit, result.fraction,
1369  unsignedbv_typet(spec.f+1));
1370 
1371  result.exponent=get_exponent(src, spec);
1372 
1373  // unbias the exponent
1374  exprt denormal=exponent_all_zeros(src, spec);
1375 
1376  result.exponent=
1377  if_exprt(denormal,
1378  from_integer(-spec.bias()+1, signedbv_typet(spec.e)),
1379  sub_bias(result.exponent, spec));
1380 
1381  result.infinity=isinf(src, spec);
1382  result.zero=is_zero(src, spec);
1383  result.NaN=isnan(src, spec);
1384 
1385  return result;
1386 }
1387 
1389  const biased_floatt &src,
1390  const ieee_float_spect &spec)
1391 {
1392  assert(to_unsignedbv_type(src.fraction.type()).get_width()==spec.f);
1393  assert(to_unsignedbv_type(src.exponent.type()).get_width()==spec.e);
1394 
1395  // do sign -- we make this 'false' for NaN
1396  exprt sign_bit=
1397  if_exprt(src.NaN, false_exprt(), src.sign);
1398 
1399  // the fraction is zero in case of infinity,
1400  // and one in case of NaN
1401  exprt fraction=
1402  if_exprt(src.NaN, from_integer(1, src.fraction.type()),
1403  if_exprt(src.infinity, from_integer(0, src.fraction.type()),
1404  src.fraction));
1405 
1406  exprt infinity_or_NaN=
1407  or_exprt(src.NaN, src.infinity);
1408 
1409  // do exponent
1410  exprt exponent=
1411  if_exprt(infinity_or_NaN, from_integer(-1, src.exponent.type()),
1412  src.exponent);
1413 
1414  // stitch all three together
1415  return concatenation_exprt(
1416  sign_bit,
1418  exponent, fraction,
1419  unsignedbv_typet(spec.e+spec.f)),
1420  spec.to_type());
1421 }
1422 
1424  const exprt &op,
1425  const exprt &dist,
1426  exprt &sticky)
1427 {
1428  std::size_t d=1, width=to_unsignedbv_type(op.type()).get_width();
1429  exprt result=op;
1430  sticky=false_exprt();
1431 
1432  std::size_t dist_width=to_bitvector_type(dist.type()).get_width();
1433 
1434  for(std::size_t stage=0; stage<dist_width; stage++)
1435  {
1436  exprt tmp=lshr_exprt(result, d);
1437 
1438  exprt lost_bits;
1439 
1440  if(d<=width)
1441  lost_bits=extractbits_exprt(result, d-1, 0, unsignedbv_typet(d));
1442  else
1443  lost_bits=result;
1444 
1445  exprt dist_bit=
1446  extractbit_exprt(dist, stage);
1447 
1448  sticky=
1449  or_exprt(
1450  and_exprt(
1451  dist_bit,
1452  notequal_exprt(lost_bits, from_integer(0, lost_bits.type()))),
1453  sticky);
1454 
1455  result=if_exprt(dist_bit, tmp, result);
1456 
1457  d=d<<1;
1458  }
1459 
1460  return result;
1461 }
const abs_exprt & to_abs_expr(const exprt &expr)
Cast a generic exprt to a abs_exprt.
Definition: std_expr.h:323
void round_exponent(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
Definition: float_bv.cpp:1227
exprt isinf(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:836
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:598
The type of an expression.
Definition: type.h:20
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:745
ieee_float_spect get_spec(const exprt &)
Definition: float_bv.cpp:98
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1125
Boolean negation.
Definition: std_expr.h:2648
constant_exprt zero_expr() const
Definition: std_types.cpp:172
semantic type conversion
Definition: std_expr.h:1725
BigInt mp_integer
Definition: mp_arith.h:19
exprt add_bias(const exprt &exponent, const ieee_float_spect &)
Definition: float_bv.cpp:1335
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:568
boolean OR
Definition: std_expr.h:1968
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:84
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1255
exprt pack(const biased_floatt &, const ieee_float_spect &)
Definition: float_bv.cpp:1388
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:258
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:61
void round_fraction(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
Definition: float_bv.cpp:1117
biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &)
takes an unbiased float, and applies the bias
Definition: float_bv.cpp:1302
The trinary if-then-else operator.
Definition: std_expr.h:2771
mp_integer address_bits(const mp_integer &size)
ceil(log2(size))
typet & type()
Definition: expr.h:60
mp_integer max_exponent() const
Definition: ieee_float.cpp:36
The proper Booleans.
Definition: std_types.h:33
A constant literal expression.
Definition: std_expr.h:3685
exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:272
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
Concatenation of bit-vector operands.
Definition: std_expr.h:3855
equality
Definition: std_expr.h:1082
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:2087
division (integer and real)
Definition: std_expr.h:854
virtual exprt rounder(const unbiased_floatt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:1009
The NIL expression.
Definition: std_expr.h:3764
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1171
boolean AND
Definition: std_expr.h:1852
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2505
exprt isnormal(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:394
API to expression classes.
exprt & op1()
Definition: expr.h:87
exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:126
inequality
Definition: std_expr.h:1124
Left shift.
Definition: std_expr.h:2301
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:702
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:2341
exprt abs(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:104
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1154
mp_integer bias() const
Definition: ieee_float.cpp:21
The unary minus expression.
Definition: std_expr.h:346
Base class of bitvector types.
Definition: std_types.h:1003
The boolean constant false.
Definition: std_expr.h:3753
std::size_t get_width() const
Definition: std_types.h:1030
binary multiplication
Definition: std_expr.h:806
exprt get_exponent(const exprt &, const ieee_float_spect &)
Gets the unbiased exponent in a floating-point bit-vector.
Definition: float_bv.cpp:853
void get(const exprt &rm)
Definition: float_bv.cpp:195
exprt sub_bias(const exprt &exponent, const ieee_float_spect &)
Definition: float_bv.cpp:1345
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
Bit-wise XOR.
Definition: std_expr.h:2134
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:1054
exprt sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky)
Definition: float_bv.cpp:1423
exprt is_zero(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:148
Base class for all expressions.
Definition: expr.h:46
absolute value
Definition: std_expr.h:300
sign of an expression
Definition: std_expr.h:456
exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
Definition: float_bv.cpp:572
unbiased_floatt unpack(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:1355
void normalization_shift(exprt &fraction, exprt &exponent)
normalize fraction/exponent pair returns &#39;zero&#39; if fraction is zero
Definition: float_bv.cpp:881
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:424
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1200
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:653
exprt isfinite(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:845
binary minus
Definition: std_expr.h:758
Bit-wise AND.
Definition: std_expr.h:2180
exprt & op2()
Definition: expr.h:90
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:863
exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:185
std::size_t width() const
Definition: ieee_float.h:50
std::size_t f
Definition: ieee_float.h:26
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
fixed-width bit-vector without numerical interpretation
Definition: std_types.h:1085
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast a generic exprt to a unary_minus_exprt.
Definition: std_expr.h:376
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:26
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:930
binary modulo
Definition: std_expr.h:902
exprt isnan(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:872
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2434
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1051