#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	fma (const bvt &multiply_lhs, const bvt &multiply_rhs, const bvt &addend)
	Fused multiply-add: round(multiply_lhs * multiply_rhs + addend) with a single rounding step.

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 152 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 729 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 1370 of file float_utils.cpp.

◆ add_sub()

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

virtual

Definition at line 291 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 1340 of file float_utils.cpp.

◆ build_constant()

bvt float_utilst::build_constant ( const ieee_float_valuet & src )

Definition at line 153 of file float_utils.cpp.

◆ conversion()

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

Definition at line 196 of file float_utils.cpp.

◆ debug1()

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

Definition at line 1497 of file float_utils.cpp.

◆ debug2()

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

Definition at line 1504 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 1002 of file float_utils.cpp.

◆ div()

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

virtual

Definition at line 623 of file float_utils.cpp.

◆ exponent_all_ones()

literalt float_utilst::exponent_all_ones ( const bvt & src )

Definition at line 870 of file float_utils.cpp.

◆ exponent_all_zeros()

literalt float_utilst::exponent_all_zeros ( const bvt & src )

Definition at line 883 of file float_utils.cpp.

◆ fma()

bvt float_utilst::fma	(	const bvt &	multiply_lhs,
		const bvt &	multiply_rhs,
		const bvt &	addend
	)

Fused multiply-add: round(multiply_lhs * multiply_rhs + addend) with a single rounding step.

Parameters

multiply_lhs	left-hand side of the multiplication
multiply_rhs	right-hand side of the multiplication
addend	value added to the product

Definition at line 508 of file float_utils.cpp.

◆ fraction_all_zeros()

literalt float_utilst::fraction_all_zeros ( const bvt & src )

Definition at line 896 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 1114 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 1448 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 844 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 850 of file float_utils.cpp.

◆ is_infinity()

literalt float_utilst::is_infinity ( const bvt & src )

Definition at line 836 of file float_utils.cpp.

◆ is_minus_inf()

literalt float_utilst::is_minus_inf ( const bvt & src )

Definition at line 855 of file float_utils.cpp.

◆ is_NaN()

literalt float_utilst::is_NaN ( const bvt & src )

Definition at line 864 of file float_utils.cpp.

◆ is_normal()

literalt float_utilst::is_normal ( const bvt & src )

Definition at line 267 of file float_utils.cpp.

◆ is_plus_inf()

literalt float_utilst::is_plus_inf ( const bvt & src )

Definition at line 827 of file float_utils.cpp.

◆ is_zero()

literalt float_utilst::is_zero ( const bvt & src )

Definition at line 818 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 433 of file float_utils.cpp.

◆ mul()

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

virtual

Definition at line 456 of file float_utils.cpp.

◆ negate()

bvt float_utilst::negate ( const bvt & src )

Definition at line 720 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 906 of file float_utils.cpp.

◆ pack()

bvt float_utilst::pack ( const biased_floatt & src )

protected

Definition at line 1417 of file float_utils.cpp.

◆ relation()

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

Definition at line 737 of file float_utils.cpp.

◆ rem()

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

virtual

Definition at line 702 of file float_utils.cpp.

◆ round_and_pack()

bvt float_utilst::round_and_pack ( const unbiased_floatt & src )

protected

Definition at line 1108 of file float_utils.cpp.

◆ round_exponent()

void float_utilst::round_exponent ( unbiased_floatt & result )

protected

Definition at line 1277 of file float_utils.cpp.

◆ round_fraction()

void float_utilst::round_fraction ( unbiased_floatt & result )

protected

Definition at line 1178 of file float_utils.cpp.

◆ round_to_integral()

bvt float_utilst::round_to_integral ( const bvt & src )

Definition at line 166 of file float_utils.cpp.

◆ rounder()

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

protected

Definition at line 1070 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 1462 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 1379 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 275 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 1388 of file float_utils.cpp.

Member Data Documentation

◆ bv_utils

bv_utilst float_utilst::bv_utils

protected

Definition at line 169 of file float_utils.h.

◆ prop

propt& float_utilst::prop

protected

Definition at line 168 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

Classes

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Detailed Description

Member Enumeration Documentation

◆ relt

Constructor & Destructor Documentation

◆ float_utilst() [1/2]

◆ float_utilst() [2/2]

◆ ~float_utilst()

Member Function Documentation

◆ abs()

◆ add()

◆ add_bias()

◆ add_sub()

◆ bias()

◆ build_constant()

◆ conversion()

◆ debug1()

◆ debug2()

◆ denormalization_shift()

◆ div()

◆ exponent_all_ones()

◆ exponent_all_zeros()

◆ fma()

◆ fraction_all_zeros()

◆ fraction_rounding_decision()

◆ from_signed_integer()

◆ from_unsigned_integer()

◆ get()

◆ get_exponent()

◆ get_fraction()

◆ is_infinity()

◆ is_minus_inf()

◆ is_NaN()

◆ is_normal()

◆ is_plus_inf()

◆ is_zero()

◆ limit_distance()

◆ mul()

◆ negate()

◆ normalization_shift()

◆ pack()

◆ relation()

◆ rem()

◆ round_and_pack()

◆ round_exponent()

◆ round_fraction()

◆ round_to_integral()

◆ rounder()

◆ set_rounding_mode()

◆ sign_bit()

◆ sticky_right_shift()

◆ sub()

◆ sub_bias()

◆ subtract_exponents()

◆ to_integer()

◆ to_signed_integer()

◆ to_unsigned_integer()

◆ unpack()

Member Data Documentation

◆ bv_utils

◆ prop

◆ rounding_mode_bits

◆ spec