cprover
|
#include <float_bv.h>
Classes | |
struct | biased_floatt |
struct | rounding_mode_bitst |
struct | unbiased_floatt |
struct | unpacked_floatt |
Public Types | |
enum | relt { relt::LT, relt::LE, relt::EQ, relt::GT, relt::GE } |
Protected Member Functions | |
ieee_float_spect | get_spec (const exprt &) |
exprt | get_exponent (const exprt &, const ieee_float_spect &) |
Gets the unbiased exponent in a floating-point bit-vector. More... | |
exprt | get_fraction (const exprt &, const ieee_float_spect &) |
Gets the fraction without hidden bit in a floating-point bit-vector src. More... | |
exprt | sign_bit (const exprt &) |
exprt | exponent_all_ones (const exprt &, const ieee_float_spect &) |
exprt | exponent_all_zeros (const exprt &, const ieee_float_spect &) |
exprt | fraction_all_zeros (const exprt &, const ieee_float_spect &) |
void | normalization_shift (exprt &fraction, exprt &exponent) |
normalize fraction/exponent pair returns 'zero' if fraction is zero More... | |
void | denormalization_shift (exprt &fraction, exprt &exponent, const ieee_float_spect &) |
make sure exponent is not too small; the exponent is unbiased More... | |
exprt | add_bias (const exprt &exponent, const ieee_float_spect &) |
exprt | sub_bias (const exprt &exponent, const ieee_float_spect &) |
exprt | limit_distance (const exprt &dist, mp_integer limit) |
Limits the shift distance. More... | |
biased_floatt | bias (const unbiased_floatt &, const ieee_float_spect &) |
takes an unbiased float, and applies the bias More... | |
virtual exprt | rounder (const unbiased_floatt &, const exprt &rm, const ieee_float_spect &) |
exprt | pack (const biased_floatt &, const ieee_float_spect &) |
unbiased_floatt | unpack (const exprt &, const ieee_float_spect &) |
void | round_fraction (unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &) |
void | round_exponent (unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &) |
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 More... | |
exprt | subtract_exponents (const unbiased_floatt &src1, const unbiased_floatt &src2) |
Subtracts the exponents. More... | |
exprt | sticky_right_shift (const exprt &op, const exprt &dist, exprt &sticky) |
Definition at line 18 of file float_bv.h.
|
strong |
Enumerator | |
---|---|
LT | |
LE | |
EQ | |
GT | |
GE |
Definition at line 97 of file float_bv.h.
|
inline |
Definition at line 21 of file float_bv.h.
|
inline |
Definition at line 25 of file float_bv.h.
exprt float_bvt::abs | ( | const exprt & | op, |
const ieee_float_spect & | spec | ||
) |
Definition at line 104 of file float_bv.cpp.
References exprt::type(), and ieee_float_spect::width().
Referenced by convert().
|
protected |
Definition at line 1335 of file float_bv.cpp.
References ieee_float_spect::bias(), ieee_float_spect::e, and from_integer().
Referenced by bias().
exprt float_bvt::add_sub | ( | bool | subtract, |
const exprt & | op0, | ||
const exprt & | op1, | ||
const exprt & | rm, | ||
const ieee_float_spect & | spec | ||
) |
Definition at line 424 of file float_bv.cpp.
References ieee_float_spect::e, float_bvt::unpacked_floatt::exponent, ieee_float_spect::f, float_bvt::unpacked_floatt::fraction, from_integer(), float_bvt::unpacked_floatt::infinity, limit_distance(), float_bvt::unpacked_floatt::NaN, float_bvt::rounding_mode_bitst::round_to_minus_inf, rounder(), float_bvt::unpacked_floatt::sign, sticky_right_shift(), subtract_exponents(), to_bitvector_type(), exprt::type(), unpack(), and float_bvt::unpacked_floatt::zero.
Referenced by convert().
|
protected |
takes an unbiased float, and applies the bias
Definition at line 1302 of file float_bv.cpp.
References add_bias(), float_bvt::unpacked_floatt::exponent, ieee_float_spect::f, float_bvt::unpacked_floatt::fraction, from_integer(), float_bvt::unpacked_floatt::infinity, float_bvt::unpacked_floatt::NaN, float_bvt::unpacked_floatt::sign, to_unsignedbv_type(), and exprt::type().
Referenced by conversion(), denormalization_shift(), and rounder().
exprt float_bvt::conversion | ( | const exprt & | src, |
const exprt & | rm, | ||
const ieee_float_spect & | src_spec, | ||
const ieee_float_spect & | dest_spec | ||
) |
Definition at line 329 of file float_bv.cpp.
References bias(), ieee_float_spect::e, float_bvt::unpacked_floatt::exponent, ieee_float_spect::f, float_bvt::unpacked_floatt::fraction, from_integer(), irept::id(), float_bvt::unpacked_floatt::infinity, float_bvt::unpacked_floatt::NaN, normalization_shift(), pack(), rounder(), float_bvt::unpacked_floatt::sign, exprt::type(), and unpack().
Referenced by convert().
Definition at line 17 of file float_bv.cpp.
References abs(), add_sub(), conversion(), div(), from_signed_integer(), from_unsigned_integer(), GE, get_spec(), bitvector_typet::get_width(), GT, irept::id(), is_equal(), is_zero(), isfinite(), isinf(), isnan(), isnormal(), LE, LT, mul(), negation(), unary_exprt::op(), exprt::op0(), exprt::op1(), exprt::op2(), relation(), sign_bit(), to_abs_expr(), to_signed_integer(), to_signedbv_type(), to_unary_minus_expr(), to_unsigned_integer(), to_unsignedbv_type(), and exprt::type().
Referenced by operator()().
|
protected |
make sure exponent is not too small; the exponent is unbiased
Definition at line 930 of file float_bv.cpp.
References ieee_float_spect::bias(), bias(), ieee_float_spect::e, ieee_float_spect::f, from_integer(), sticky_right_shift(), to_signedbv_type(), to_unsignedbv_type(), exprt::type(), and unsignedbv_typet::zero_expr().
Referenced by rounder().
exprt float_bvt::div | ( | const exprt & | src1, |
const exprt & | src2, | ||
const exprt & | rm, | ||
const ieee_float_spect & | spec | ||
) |
Definition at line 653 of file float_bv.cpp.
References ieee_float_spect::e, float_bvt::unpacked_floatt::exponent, ieee_float_spect::f, float_bvt::unpacked_floatt::fraction, from_integer(), float_bvt::unpacked_floatt::infinity, float_bvt::unpacked_floatt::NaN, rounder(), float_bvt::unpacked_floatt::sign, to_unsignedbv_type(), exprt::type(), unpack(), and float_bvt::unpacked_floatt::zero.
Referenced by convert().
|
protected |
Definition at line 167 of file float_bv.cpp.
References get_exponent(), to_unsignedbv_type(), and exprt::type().
Referenced by isinf(), isnan(), and isnormal().
|
protected |
Definition at line 176 of file float_bv.cpp.
References get_exponent(), to_unsignedbv_type(), and exprt::type().
Referenced by isnormal(), and unpack().
|
protected |
Definition at line 185 of file float_bv.cpp.
References get_fraction(), to_unsignedbv_type(), and exprt::type().
|
protected |
rounding decision for fraction using sticky bit
Definition at line 1054 of file float_bv.cpp.
References from_integer(), float_bvt::rounding_mode_bitst::round_to_even, float_bvt::rounding_mode_bitst::round_to_minus_inf, float_bvt::rounding_mode_bitst::round_to_plus_inf, float_bvt::rounding_mode_bitst::round_to_zero, to_unsignedbv_type(), and exprt::type().
Referenced by round_fraction().
exprt float_bvt::from_signed_integer | ( | const exprt & | src, |
const exprt & | rm, | ||
const ieee_float_spect & | spec | ||
) |
Definition at line 217 of file float_bv.cpp.
References address_bits(), float_bvt::unpacked_floatt::exponent, float_bvt::unpacked_floatt::fraction, from_integer(), rounder(), float_bvt::unpacked_floatt::sign, sign_bit(), to_signedbv_type(), and exprt::type().
Referenced by convert().
exprt float_bvt::from_unsigned_integer | ( | const exprt & | src, |
const exprt & | rm, | ||
const ieee_float_spect & | spec | ||
) |
Definition at line 241 of file float_bv.cpp.
References address_bits(), float_bvt::unpacked_floatt::exponent, float_bvt::unpacked_floatt::fraction, from_integer(), rounder(), float_bvt::unpacked_floatt::sign, to_unsignedbv_type(), and exprt::type().
Referenced by convert().
|
protected |
Gets the unbiased exponent in a floating-point bit-vector.
Definition at line 853 of file float_bv.cpp.
References ieee_float_spect::e, and ieee_float_spect::f.
Referenced by exponent_all_ones(), exponent_all_zeros(), and unpack().
|
protected |
Gets the fraction without hidden bit in a floating-point bit-vector src.
Definition at line 863 of file float_bv.cpp.
References ieee_float_spect::f.
Referenced by fraction_all_zeros(), and unpack().
|
protected |
Definition at line 98 of file float_bv.cpp.
References to_floatbv_type(), and exprt::type().
Referenced by convert().
exprt float_bvt::is_equal | ( | const exprt & | src0, |
const exprt & | src1, | ||
const ieee_float_spect & | spec | ||
) |
Definition at line 126 of file float_bv.cpp.
References is_zero(), and isnan().
Referenced by convert().
exprt float_bvt::is_zero | ( | const exprt & | src, |
const ieee_float_spect & | spec | ||
) |
Definition at line 148 of file float_bv.cpp.
References bitvector_typet::get_width(), to_floatbv_type(), and exprt::type().
Referenced by string_constraint_generatort::add_axioms_from_float(), convert(), is_equal(), relation(), and unpack().
exprt float_bvt::isfinite | ( | const exprt & | src, |
const ieee_float_spect & | spec | ||
) |
Definition at line 845 of file float_bv.cpp.
References isinf(), and isnan().
Referenced by convert().
exprt float_bvt::isinf | ( | const exprt & | src, |
const ieee_float_spect & | spec | ||
) |
Definition at line 836 of file float_bv.cpp.
References exponent_all_ones(), and fraction_all_zeros().
Referenced by string_constraint_generatort::add_axioms_from_float(), convert(), isfinite(), and unpack().
exprt float_bvt::isnan | ( | const exprt & | src, |
const ieee_float_spect & | spec | ||
) |
Definition at line 872 of file float_bv.cpp.
References exponent_all_ones(), and fraction_all_zeros().
Referenced by string_constraint_generatort::add_axioms_from_float(), convert(), is_equal(), isfinite(), mul(), relation(), and unpack().
exprt float_bvt::isnormal | ( | const exprt & | src, |
const ieee_float_spect & | spec | ||
) |
Definition at line 394 of file float_bv.cpp.
References exponent_all_ones(), and exponent_all_zeros().
|
protected |
Limits the shift distance.
Definition at line 572 of file float_bv.cpp.
References address_bits(), from_integer(), integer2unsigned(), to_unsignedbv_type(), and exprt::type().
Referenced by add_sub().
exprt float_bvt::mul | ( | const exprt & | src1, |
const exprt & | src2, | ||
const exprt & | rm, | ||
const ieee_float_spect & | spec | ||
) |
Definition at line 598 of file float_bv.cpp.
References exprt::copy_to_operands(), ieee_float_spect::e, float_bvt::unpacked_floatt::exponent, ieee_float_spect::f, float_bvt::unpacked_floatt::fraction, from_integer(), float_bvt::unpacked_floatt::infinity, isnan(), float_bvt::unpacked_floatt::NaN, rounder(), float_bvt::unpacked_floatt::sign, unpack(), and float_bvt::unpacked_floatt::zero.
Referenced by convert().
exprt float_bvt::negation | ( | const exprt & | op, |
const ieee_float_spect & | spec | ||
) |
Definition at line 115 of file float_bv.cpp.
References exprt::type(), and ieee_float_spect::width().
Referenced by convert().
normalize fraction/exponent pair returns 'zero' if fraction is zero
Definition at line 881 of file float_bv.cpp.
References address_bits(), from_integer(), integer2unsigned(), to_signedbv_type(), to_unsignedbv_type(), and exprt::type().
Referenced by conversion(), and rounder().
Definition at line 29 of file float_bv.h.
References convert().
|
protected |
Definition at line 1388 of file float_bv.cpp.
References ieee_float_spect::e, float_bvt::unpacked_floatt::exponent, ieee_float_spect::f, float_bvt::unpacked_floatt::fraction, from_integer(), float_bvt::unpacked_floatt::infinity, float_bvt::unpacked_floatt::NaN, float_bvt::unpacked_floatt::sign, sign_bit(), ieee_float_spect::to_type(), to_unsignedbv_type(), and exprt::type().
Referenced by conversion(), and rounder().
exprt float_bvt::relation | ( | const exprt & | src1, |
relt | rel, | ||
const exprt & | src2, | ||
const ieee_float_spect & | spec | ||
) |
Definition at line 745 of file float_bv.cpp.
References exprt::copy_to_operands(), EQ, GE, GT, is_zero(), isnan(), LE, LT, sign_bit(), and ieee_float_spect::width().
Referenced by convert().
|
protected |
Definition at line 1227 of file float_bv.cpp.
References ieee_float_spect::bias(), ieee_float_spect::e, float_bvt::unpacked_floatt::exponent, float_bvt::unpacked_floatt::fraction, from_integer(), float_bvt::unpacked_floatt::infinity, ieee_float_spect::max_exponent(), float_bvt::rounding_mode_bitst::round_to_even, float_bvt::rounding_mode_bitst::round_to_minus_inf, float_bvt::rounding_mode_bitst::round_to_plus_inf, float_bvt::unpacked_floatt::sign, to_signedbv_type(), to_unsignedbv_type(), and exprt::type().
Referenced by rounder().
|
protected |
Definition at line 1117 of file float_bv.cpp.
References float_bvt::unpacked_floatt::exponent, ieee_float_spect::f, float_bvt::unpacked_floatt::fraction, fraction_rounding_decision(), from_integer(), float_bvt::unpacked_floatt::sign, to_unsignedbv_type(), and exprt::type().
Referenced by rounder().
|
protectedvirtual |
Definition at line 1009 of file float_bv.cpp.
References address_bits(), bias(), denormalization_shift(), ieee_float_spect::e, float_bvt::unpacked_floatt::exponent, ieee_float_spect::f, float_bvt::unpacked_floatt::fraction, float_bvt::unpacked_floatt::infinity, integer2size_t(), float_bvt::unpacked_floatt::NaN, normalization_shift(), pack(), round_exponent(), round_fraction(), float_bvt::unpacked_floatt::sign, and to_signedbv_type().
Referenced by add_sub(), conversion(), div(), from_signed_integer(), from_unsigned_integer(), and mul().
Definition at line 210 of file float_bv.cpp.
References bitvector_typet::get_width(), to_bitvector_type(), and exprt::type().
Referenced by convert(), from_signed_integer(), pack(), relation(), and unpack().
|
protected |
Definition at line 1423 of file float_bv.cpp.
References from_integer(), to_bitvector_type(), to_unsignedbv_type(), and exprt::type().
Referenced by add_sub(), and denormalization_shift().
|
protected |
Definition at line 1345 of file float_bv.cpp.
References ieee_float_spect::bias(), ieee_float_spect::e, and from_integer().
Referenced by unpack().
|
protected |
Subtracts the exponents.
Definition at line 404 of file float_bv.cpp.
References float_bvt::unpacked_floatt::exponent, to_signedbv_type(), and exprt::type().
Referenced by add_sub().
exprt float_bvt::to_integer | ( | const exprt & | src, |
std::size_t | dest_width, | ||
bool | is_signed, | ||
const exprt & | rm, | ||
const ieee_float_spect & | spec | ||
) |
Definition at line 281 of file float_bv.cpp.
References ieee_float_spect::e, float_bvt::unpacked_floatt::exponent, ieee_float_spect::f, float_bvt::unpacked_floatt::fraction, from_integer(), is_signed(), float_bvt::unpacked_floatt::sign, exprt::type(), and unpack().
Referenced by to_signed_integer(), and to_unsigned_integer().
exprt float_bvt::to_signed_integer | ( | const exprt & | src, |
std::size_t | dest_width, | ||
const exprt & | rm, | ||
const ieee_float_spect & | spec | ||
) |
exprt float_bvt::to_unsigned_integer | ( | const exprt & | src, |
std::size_t | dest_width, | ||
const exprt & | rm, | ||
const ieee_float_spect & | spec | ||
) |
|
protected |
Definition at line 1355 of file float_bv.cpp.
References ieee_float_spect::bias(), ieee_float_spect::e, float_bvt::unpacked_floatt::exponent, exponent_all_zeros(), ieee_float_spect::f, float_bvt::unpacked_floatt::fraction, from_integer(), get_exponent(), get_fraction(), float_bvt::unpacked_floatt::infinity, is_zero(), isinf(), isnan(), isnormal(), float_bvt::unpacked_floatt::NaN, float_bvt::unpacked_floatt::sign, sign_bit(), sub_bias(), and float_bvt::unpacked_floatt::zero.
Referenced by add_sub(), conversion(), div(), mul(), and to_integer().