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