float_utilst Class Reference

#include <float_utils.h>

Inheritance diagram for float_utilst:

Collaboration diagram for float_utilst:

Classes
struct	biased_floatt
struct	rounding_mode_bitst
struct	unbiased_floatt
struct	unpacked_floatt

Public Types
enum class	relt {   LT , LE , EQ , GT ,   GE }

Public Member Functions
	float_utilst (propt &_prop)
	float_utilst (propt &_prop, const floatbv_typet &type)
void	set_rounding_mode (const bvt &)
virtual	~float_utilst ()
bvt	build_constant (const ieee_float_valuet &)
bvt	get_exponent (const bvt &)
	Gets the unbiased exponent in a floating-point bit-vector.
bvt	get_fraction (const bvt &)
	Gets the fraction without hidden bit in a floating-point bit-vector src.
literalt	is_normal (const bvt &)
literalt	is_zero (const bvt &)
literalt	is_infinity (const bvt &)
literalt	is_plus_inf (const bvt &)
literalt	is_minus_inf (const bvt &)
literalt	is_NaN (const bvt &)
virtual bvt	add_sub (const bvt &src1, const bvt &src2, bool subtract)
bvt	add (const bvt &src1, const bvt &src2)
bvt	sub (const bvt &src1, const bvt &src2)
virtual bvt	mul (const bvt &src1, const bvt &src2)
virtual bvt	div (const bvt &src1, const bvt &src2)
virtual bvt	rem (const bvt &src1, const bvt &src2)
bvt	abs (const bvt &)
bvt	negate (const bvt &)
bvt	from_unsigned_integer (const bvt &)
bvt	from_signed_integer (const bvt &)
bvt	to_integer (const bvt &src, std::size_t int_width, bool is_signed)
bvt	to_signed_integer (const bvt &src, std::size_t int_width)
bvt	to_unsigned_integer (const bvt &src, std::size_t int_width)
bvt	conversion (const bvt &src, const ieee_float_spect &dest_spec)
bvt	round_to_integral (const bvt &)
literalt	relation (const bvt &src1, relt rel, const bvt &src2)
ieee_float_valuet	get (const bvt &) const
literalt	exponent_all_ones (const bvt &)
literalt	exponent_all_zeros (const bvt &)
literalt	fraction_all_zeros (const bvt &)
bvt	debug1 (const bvt &op0, const bvt &op1)
bvt	debug2 (const bvt &op0, const bvt &op1)

Static Public Member Functions
static literalt	sign_bit (const bvt &src)

Public Attributes
rounding_mode_bitst	rounding_mode_bits
ieee_float_spect	spec

Protected Member Functions
virtual void	normalization_shift (bvt &fraction, bvt &exponent)
	normalize fraction/exponent pair returns 'zero' if fraction is zero
void	denormalization_shift (bvt &fraction, bvt &exponent)
	make sure exponent is not too small; the exponent is unbiased
bvt	add_bias (const bvt &exponent)
bvt	sub_bias (const bvt &exponent)
bvt	limit_distance (const bvt &dist, mp_integer limit)
	Limits the shift distance.
unbiased_floatt	unpack (const bvt &)
biased_floatt	bias (const unbiased_floatt &)
	takes an unbiased float, and applies the bias
unbiased_floatt	rounder (const unbiased_floatt &)
bvt	round_and_pack (const unbiased_floatt &)
bvt	pack (const biased_floatt &)
void	round_fraction (unbiased_floatt &result)
void	round_exponent (unbiased_floatt &result)
literalt	fraction_rounding_decision (const std::size_t dest_bits, const literalt sign, const bvt &fraction)
	rounding decision for fraction using sticky bit
bvt	subtract_exponents (const unbiased_floatt &src1, const unbiased_floatt &src2)
	Subtracts the exponents.
bvt	sticky_right_shift (const bvt &op, const bvt &dist, literalt &sticky)

Protected Attributes
propt &	prop
bv_utilst	bv_utils

Detailed Description

Definition at line 17 of file float_utils.h.

Member Enumeration Documentation

relt

enum class float_utilst::relt

strong

Enumerator
LT
LE
EQ
GT
GE

Definition at line 145 of file float_utils.h.

Constructor & Destructor Documentation

float_utilst() [1/2]

float_utilst::float_utilst ( propt &  _prop )

inlineexplicit

Definition at line 75 of file float_utils.h.

float_utilst() [2/2]

float_utilst::float_utilst ( propt &  _prop, const floatbv_typet &  type  )

inline

Definition at line 81 of file float_utils.h.

~float_utilst()

virtual float_utilst::~float_utilst ( )

inlinevirtual

Definition at line 90 of file float_utils.h.

Member Function Documentation

abs()

bvt float_utilst::abs

(

const bvt &

src

)

Definition at line 603 of file float_utils.cpp.

add()

bvt float_utilst::add ( const bvt &  src1, const bvt &  src2  )

inline

Definition at line 117 of file float_utils.h.

add_bias()

bvt float_utilst::add_bias ( const bvt &  exponent )

protected

Definition at line 1237 of file float_utils.cpp.

add_sub()

bvt float_utilst::add_sub ( const bvt &  src1, const bvt &  src2, bool  subtract  )

virtual

Definition at line 280 of file float_utils.cpp.

bias()

float_utilst::biased_floatt float_utilst::bias ( const unbiased_floatt &  src )

protected

takes an unbiased float, and applies the bias

Definition at line 1207 of file float_utils.cpp.

build_constant()

bvt float_utilst::build_constant

(

const ieee_float_valuet &

src

)

Definition at line 142 of file float_utils.cpp.

conversion()

bvt float_utilst::conversion	(	const bvt &	src,
		const ieee_float_spect &	dest_spec
	)

Definition at line 185 of file float_utils.cpp.

debug1()

bvt float_utilst::debug1	(	const bvt &	op0,
		const bvt &	op1
	)

Definition at line 1364 of file float_utils.cpp.

debug2()

bvt float_utilst::debug2	(	const bvt &	op0,
		const bvt &	op1
	)

Definition at line 1371 of file float_utils.cpp.

denormalization_shift()

void float_utilst::denormalization_shift ( bvt &  fraction, bvt &  exponent  )

protected

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

Definition at line 869 of file float_utils.cpp.

div()

bvt float_utilst::div ( const bvt &  src1, const bvt &  src2  )

virtual

Definition at line 497 of file float_utils.cpp.

exponent_all_ones()

literalt float_utilst::exponent_all_ones

(

const bvt &

src

)

Definition at line 744 of file float_utils.cpp.

exponent_all_zeros()

literalt float_utilst::exponent_all_zeros

(

const bvt &

src

)

Definition at line 757 of file float_utils.cpp.

fraction_all_zeros()

literalt float_utilst::fraction_all_zeros

(

const bvt &

src

)

Definition at line 770 of file float_utils.cpp.

fraction_rounding_decision()

literalt float_utilst::fraction_rounding_decision ( const std::size_t  dest_bits, const literalt  sign, const bvt &  fraction  )

protected

rounding decision for fraction using sticky bit

Definition at line 981 of file float_utils.cpp.

from_signed_integer()

bvt float_utilst::from_signed_integer

(

const bvt &

src

)

Definition at line 35 of file float_utils.cpp.

from_unsigned_integer()

bvt float_utilst::from_unsigned_integer

(

const bvt &

src

)

Definition at line 53 of file float_utils.cpp.

get()

ieee_float_valuet float_utilst::get

(

const bvt &

src

)

const

Definition at line 1315 of file float_utils.cpp.

get_exponent()

bvt float_utilst::get_exponent

(

const bvt &

src

)

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

Definition at line 718 of file float_utils.cpp.

get_fraction()

bvt float_utilst::get_fraction

(

const bvt &

src

)

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

Definition at line 724 of file float_utils.cpp.

is_infinity()

literalt float_utilst::is_infinity

(

const bvt &

src

)

Definition at line 710 of file float_utils.cpp.

is_minus_inf()

literalt float_utilst::is_minus_inf

(

const bvt &

src

)

Definition at line 729 of file float_utils.cpp.

is_NaN()

literalt float_utilst::is_NaN

(

const bvt &

src

)

Definition at line 738 of file float_utils.cpp.

is_normal()

literalt float_utilst::is_normal

(

const bvt &

src

)

Definition at line 256 of file float_utils.cpp.

is_plus_inf()

literalt float_utilst::is_plus_inf

(

const bvt &

src

)

Definition at line 701 of file float_utils.cpp.

is_zero()

literalt float_utilst::is_zero

(

const bvt &

src

)

Definition at line 692 of file float_utils.cpp.

limit_distance()

bvt float_utilst::limit_distance ( const bvt &  dist, mp_integer  limit  )

protected

Limits the shift distance.

Definition at line 422 of file float_utils.cpp.

mul()

bvt float_utilst::mul ( const bvt &  src1, const bvt &  src2  )

virtual

Definition at line 445 of file float_utils.cpp.

negate()

bvt float_utilst::negate

(

const bvt &

src

)

Definition at line 594 of file float_utils.cpp.

normalization_shift()

void float_utilst::normalization_shift ( bvt &  fraction, bvt &  exponent  )

protectedvirtual

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

Reimplemented in float_approximationt.

Definition at line 780 of file float_utils.cpp.

pack()

bvt float_utilst::pack ( const biased_floatt &  src )

protected

Definition at line 1284 of file float_utils.cpp.

relation()

literalt float_utilst::relation	(	const bvt &	src1,
		relt	rel,
		const bvt &	src2
	)

Definition at line 611 of file float_utils.cpp.

rem()

bvt float_utilst::rem ( const bvt &  src1, const bvt &  src2  )

virtual

Definition at line 576 of file float_utils.cpp.

round_and_pack()

bvt float_utilst::round_and_pack ( const unbiased_floatt &  src )

protected

Definition at line 975 of file float_utils.cpp.

round_exponent()

void float_utilst::round_exponent ( unbiased_floatt &  result )

protected

Definition at line 1144 of file float_utils.cpp.

round_fraction()

void float_utilst::round_fraction ( unbiased_floatt &  result )

protected

Definition at line 1045 of file float_utils.cpp.

round_to_integral()

bvt float_utilst::round_to_integral

(

const bvt &

src

)

Definition at line 155 of file float_utils.cpp.

rounder()

float_utilst::unbiased_floatt float_utilst::rounder ( const unbiased_floatt &  src )

protected

Definition at line 937 of file float_utils.cpp.

set_rounding_mode()

void float_utilst::set_rounding_mode

(

const bvt &

src

)

Definition at line 15 of file float_utils.cpp.

sign_bit()

static literalt float_utilst::sign_bit ( const bvt &  src )

inlinestatic

Definition at line 98 of file float_utils.h.

sticky_right_shift()

bvt float_utilst::sticky_right_shift ( const bvt &  op, const bvt &  dist, literalt &  sticky  )

protected

Definition at line 1329 of file float_utils.cpp.

sub()

bvt float_utilst::sub ( const bvt &  src1, const bvt &  src2  )

inline

Definition at line 122 of file float_utils.h.

sub_bias()

bvt float_utilst::sub_bias ( const bvt &  exponent )

protected

Definition at line 1246 of file float_utils.cpp.

subtract_exponents()

bvt float_utilst::subtract_exponents ( const unbiased_floatt &  src1, const unbiased_floatt &  src2  )

protected

Subtracts the exponents.

Definition at line 264 of file float_utils.cpp.

to_integer()

bvt float_utilst::to_integer	(	const bvt &	src,
		std::size_t	int_width,
		bool	is_signed
	)

Definition at line 84 of file float_utils.cpp.

to_signed_integer()

bvt float_utilst::to_signed_integer	(	const bvt &	src,
		std::size_t	int_width
	)

Definition at line 70 of file float_utils.cpp.

to_unsigned_integer()

bvt float_utilst::to_unsigned_integer	(	const bvt &	src,
		std::size_t	int_width
	)

Definition at line 77 of file float_utils.cpp.

unpack()

float_utilst::unbiased_floatt float_utilst::unpack ( const bvt &  src )

protected

Definition at line 1255 of file float_utils.cpp.

Member Data Documentation

bv_utils

bv_utilst float_utilst::bv_utils

protected

Definition at line 162 of file float_utils.h.

prop

propt& float_utilst::prop

protected

Definition at line 161 of file float_utils.h.

rounding_mode_bits

rounding_mode_bitst float_utilst::rounding_mode_bits

Definition at line 73 of file float_utils.h.

spec

ieee_float_spect float_utilst::spec

Definition at line 94 of file float_utils.h.

---

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

• /home/runner/work/cbmc/cbmc/src/solvers/floatbv/float_utils.h
• /home/runner/work/cbmc/cbmc/src/solvers/floatbv/float_utils.cpp