cprover
float_bvt Class Reference

#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
}
 

Public Member Functions

 float_bvt ()
 
 ~float_bvt ()
 
exprt operator() (const exprt &src)
 
exprt convert (const exprt &)
 
exprt negation (const exprt &, const ieee_float_spect &)
 
exprt abs (const exprt &, const ieee_float_spect &)
 
exprt is_equal (const exprt &, const exprt &, const ieee_float_spect &)
 
exprt is_zero (const exprt &, const ieee_float_spect &)
 
exprt isnan (const exprt &, const ieee_float_spect &)
 
exprt isinf (const exprt &, const ieee_float_spect &)
 
exprt isnormal (const exprt &, const ieee_float_spect &)
 
exprt isfinite (const exprt &, const ieee_float_spect &)
 
exprt add_sub (bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
 
exprt mul (const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
 
exprt div (const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
 
exprt from_unsigned_integer (const exprt &, const exprt &rm, const ieee_float_spect &)
 
exprt from_signed_integer (const exprt &, const exprt &rm, const ieee_float_spect &)
 
exprt to_signed_integer (const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
 
exprt to_unsigned_integer (const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
 
exprt to_integer (const exprt &src, std::size_t dest_width, bool is_signed, const exprt &rm, const ieee_float_spect &)
 
exprt conversion (const exprt &src, const exprt &rm, const ieee_float_spect &src_spec, const ieee_float_spect &dest_spec)
 
exprt relation (const exprt &, relt rel, const exprt &, const ieee_float_spect &)
 

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)
 

Detailed Description

Definition at line 18 of file float_bv.h.

Member Enumeration Documentation

◆ relt

enum float_bvt::relt
strong
Enumerator
LT 
LE 
EQ 
GT 
GE 

Definition at line 97 of file float_bv.h.

Constructor & Destructor Documentation

◆ float_bvt()

float_bvt::float_bvt ( )
inline

Definition at line 21 of file float_bv.h.

◆ ~float_bvt()

float_bvt::~float_bvt ( )
inline

Definition at line 25 of file float_bv.h.

Member Function Documentation

◆ abs()

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().

◆ add_bias()

exprt float_bvt::add_bias ( const exprt exponent,
const ieee_float_spect spec 
)
protected

Definition at line 1302 of file float_bv.cpp.

References ieee_float_spect::bias(), ieee_float_spect::e, and from_integer().

Referenced by bias().

◆ add_sub()

◆ bias()

◆ conversion()

◆ convert()

◆ denormalization_shift()

void float_bvt::denormalization_shift ( exprt fraction,
exprt exponent,
const ieee_float_spect spec 
)
protected

make sure exponent is not too small; the exponent is unbiased

Definition at line 916 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().

◆ div()

◆ exponent_all_ones()

exprt float_bvt::exponent_all_ones ( const exprt src,
const ieee_float_spect spec 
)
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().

◆ exponent_all_zeros()

exprt float_bvt::exponent_all_zeros ( const exprt src,
const ieee_float_spect spec 
)
protected

Definition at line 176 of file float_bv.cpp.

References get_exponent(), to_unsignedbv_type(), and exprt::type().

Referenced by isnormal(), and unpack().

◆ fraction_all_zeros()

exprt float_bvt::fraction_all_zeros ( const exprt src,
const ieee_float_spect spec 
)
protected

Definition at line 185 of file float_bv.cpp.

References get_fraction(), to_unsignedbv_type(), and exprt::type().

Referenced by isinf(), and isnan().

◆ fraction_rounding_decision()

exprt float_bvt::fraction_rounding_decision ( const std::size_t  dest_bits,
const exprt  sign,
const exprt fraction,
const rounding_mode_bitst rounding_mode_bits 
)
protected

◆ from_signed_integer()

exprt float_bvt::from_signed_integer ( const exprt src,
const exprt rm,
const ieee_float_spect spec 
)

◆ from_unsigned_integer()

exprt float_bvt::from_unsigned_integer ( const exprt src,
const exprt rm,
const ieee_float_spect spec 
)

◆ get_exponent()

exprt float_bvt::get_exponent ( const exprt src,
const ieee_float_spect spec 
)
protected

Gets the unbiased exponent in a floating-point bit-vector.

Definition at line 838 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().

◆ get_fraction()

exprt float_bvt::get_fraction ( const exprt src,
const ieee_float_spect spec 
)
protected

Gets the fraction without hidden bit in a floating-point bit-vector src.

Definition at line 848 of file float_bv.cpp.

References ieee_float_spect::f.

Referenced by fraction_all_zeros(), and unpack().

◆ get_spec()

ieee_float_spect float_bvt::get_spec ( const exprt expr)
protected

Definition at line 98 of file float_bv.cpp.

References to_floatbv_type(), and exprt::type().

Referenced by convert().

◆ is_equal()

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().

◆ is_zero()

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 convert(), is_equal(), relation(), and unpack().

◆ isfinite()

exprt float_bvt::isfinite ( const exprt src,
const ieee_float_spect spec 
)

Definition at line 830 of file float_bv.cpp.

References isinf(), and isnan().

Referenced by convert().

◆ isinf()

exprt float_bvt::isinf ( const exprt src,
const ieee_float_spect spec 
)

Definition at line 821 of file float_bv.cpp.

References exponent_all_ones(), and fraction_all_zeros().

Referenced by convert(), isfinite(), and unpack().

◆ isnan()

exprt float_bvt::isnan ( const exprt src,
const ieee_float_spect spec 
)

Definition at line 857 of file float_bv.cpp.

References exponent_all_ones(), and fraction_all_zeros().

Referenced by convert(), is_equal(), isfinite(), mul(), relation(), and unpack().

◆ isnormal()

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().

Referenced by convert(), and unpack().

◆ limit_distance()

exprt float_bvt::limit_distance ( const exprt dist,
mp_integer  limit 
)
protected

Limits the shift distance.

Definition at line 570 of file float_bv.cpp.

References address_bits(), from_integer(), to_unsignedbv_type(), and exprt::type().

Referenced by add_sub().

◆ mul()

◆ negation()

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().

◆ normalization_shift()

void float_bvt::normalization_shift ( exprt fraction,
exprt exponent 
)
protected

normalize fraction/exponent pair returns 'zero' if fraction is zero

Definition at line 866 of file float_bv.cpp.

References address_bits(), from_integer(), to_signedbv_type(), to_unsignedbv_type(), and exprt::type().

Referenced by conversion(), and rounder().

◆ operator()()

exprt float_bvt::operator() ( const exprt src)
inline

Definition at line 29 of file float_bv.h.

References convert().

◆ pack()

◆ relation()

exprt float_bvt::relation ( const exprt src1,
relt  rel,
const exprt src2,
const ieee_float_spect spec 
)

◆ round_exponent()

◆ round_fraction()

void float_bvt::round_fraction ( unbiased_floatt result,
const rounding_mode_bitst rounding_mode_bits,
const ieee_float_spect spec 
)
protected

◆ rounder()

◆ sign_bit()

exprt float_bvt::sign_bit ( const exprt op)
protected

◆ sticky_right_shift()

exprt float_bvt::sticky_right_shift ( const exprt op,
const exprt dist,
exprt sticky 
)
protected

Definition at line 1387 of file float_bv.cpp.

References from_integer(), to_bitvector_type(), to_unsignedbv_type(), and exprt::type().

Referenced by add_sub(), and denormalization_shift().

◆ sub_bias()

exprt float_bvt::sub_bias ( const exprt exponent,
const ieee_float_spect spec 
)
protected

Definition at line 1312 of file float_bv.cpp.

References ieee_float_spect::bias(), ieee_float_spect::e, and from_integer().

Referenced by unpack().

◆ subtract_exponents()

exprt float_bvt::subtract_exponents ( const unbiased_floatt src1,
const unbiased_floatt src2 
)
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().

◆ to_integer()

exprt float_bvt::to_integer ( const exprt src,
std::size_t  dest_width,
bool  is_signed,
const exprt rm,
const ieee_float_spect spec 
)

◆ to_signed_integer()

exprt float_bvt::to_signed_integer ( const exprt src,
std::size_t  dest_width,
const exprt rm,
const ieee_float_spect spec 
)

Definition at line 263 of file float_bv.cpp.

References to_integer().

Referenced by convert().

◆ to_unsigned_integer()

exprt float_bvt::to_unsigned_integer ( const exprt src,
std::size_t  dest_width,
const exprt rm,
const ieee_float_spect spec 
)

Definition at line 272 of file float_bv.cpp.

References to_integer().

Referenced by convert().

◆ unpack()


The documentation for this class was generated from the following files: