#include <float_bv.h>

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
exprt	operator() (const exprt &src) const

exprt	convert (const exprt &) const

exprt	add_sub (bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const

exprt	mul (const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const

exprt	div (const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const

exprt	fma (const exprt &multiply_lhs, const exprt &multiply_rhs, const exprt &addend, const exprt &rm, const ieee_float_spect &) const
	Fused multiply-add: round(multiply_lhs * multiply_rhs + addend) with a single rounding step.

exprt	from_unsigned_integer (const exprt &, const exprt &rm, const ieee_float_spect &) const

exprt	from_signed_integer (const exprt &, const exprt &rm, const ieee_float_spect &) const

exprt	conversion (const exprt &src, const exprt &rm, const ieee_float_spect &src_spec, const ieee_float_spect &dest_spec) const

Static Public Member Functions
static exprt	negation (const exprt &, const ieee_float_spect &)

static exprt	abs (const exprt &, const ieee_float_spect &)

static exprt	is_equal (const exprt &, const exprt &, const ieee_float_spect &)

static exprt	is_zero (const exprt &)

static exprt	isnan (const exprt &, const ieee_float_spect &)

static exprt	isinf (const exprt &, const ieee_float_spect &)

static exprt	isnormal (const exprt &, const ieee_float_spect &)

static exprt	isfinite (const exprt &, const ieee_float_spect &)

static exprt	to_signed_integer (const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)

static exprt	to_unsigned_integer (const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)

static exprt	to_integer (const exprt &src, std::size_t dest_width, bool is_signed, const exprt &rm, const ieee_float_spect &)

static exprt	relation (const exprt &, relt rel, const exprt &, const ieee_float_spect &)

Private Member Functions
exprt	rounder (const unbiased_floatt &, const exprt &rm, const ieee_float_spect &) const

Static Private Member Functions
static ieee_float_spect	get_spec (const exprt &)

static exprt	get_exponent (const exprt &, const ieee_float_spect &)
	Gets the unbiased exponent in a floating-point bit-vector.

static exprt	get_fraction (const exprt &, const ieee_float_spect &)
	Gets the fraction without hidden bit in a floating-point bit-vector src.

static exprt	sign_bit (const exprt &)

static exprt	exponent_all_ones (const exprt &, const ieee_float_spect &)

static exprt	exponent_all_zeros (const exprt &, const ieee_float_spect &)

static exprt	fraction_all_zeros (const exprt &, const ieee_float_spect &)

static void	normalization_shift (exprt &fraction, exprt &exponent)
	normalize fraction/exponent pair returns 'zero' if fraction is zero

static void	denormalization_shift (exprt &fraction, exprt &exponent, const ieee_float_spect &)
	make sure exponent is not too small; the exponent is unbiased

static exprt	add_bias (const exprt &exponent, const ieee_float_spect &)

static exprt	sub_bias (const exprt &exponent, const ieee_float_spect &)

static exprt	limit_distance (const exprt &dist, mp_integer limit)
	Limits the shift distance.

static biased_floatt	bias (const unbiased_floatt &, const ieee_float_spect &)
	takes an unbiased float, and applies the bias

static exprt	pack (const biased_floatt &, const ieee_float_spect &)

static unbiased_floatt	unpack (const exprt &, const ieee_float_spect &)

static void	round_fraction (unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)

static void	round_exponent (unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)

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

static exprt	subtract_exponents (const unbiased_floatt &src1, const unbiased_floatt &src2)
	Subtracts the exponents.

static exprt	sticky_right_shift (const exprt &op, const exprt &dist, exprt &sticky)

Detailed Description

Definition at line 16 of file float_bv.h.

Member Enumeration Documentation

◆ relt

enum class float_bvt::relt

strong

Enumerator
LT
LE
EQ
GT
GE

Definition at line 97 of file float_bv.h.

Member Function Documentation

◆ abs()

exprt float_bvt::abs	(	const exprt &	op,
		const ieee_float_spect &	spec
	)

static

Definition at line 202 of file float_bv.cpp.

◆ add_bias()

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

staticprivate

Definition at line 1520 of file float_bv.cpp.

◆ add_sub()

exprt float_bvt::add_sub	(	bool	subtract,
		const exprt &	op0,
		const exprt &	op1,
		const exprt &	rm,
		const ieee_float_spect &	spec
	)		const

Definition at line 528 of file float_bv.cpp.

◆ bias()

float_bvt::biased_floatt float_bvt::bias	(	const unbiased_floatt &	src,
		const ieee_float_spect &	spec
	)

staticprivate

takes an unbiased float, and applies the bias

Definition at line 1488 of file float_bv.cpp.

◆ conversion()

exprt float_bvt::conversion	(	const exprt &	src,
		const exprt &	rm,
		const ieee_float_spect &	src_spec,
		const ieee_float_spect &	dest_spec
	)		const

Definition at line 425 of file float_bv.cpp.

◆ convert()

exprt float_bvt::convert ( const exprt & expr ) const

Definition at line 19 of file float_bv.cpp.

◆ denormalization_shift()

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

staticprivate

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

Definition at line 1131 of file float_bv.cpp.

◆ div()

exprt float_bvt::div	(	const exprt &	src1,
		const exprt &	src2,
		const exprt &	rm,
		const ieee_float_spect &	spec
	)		const

Definition at line 748 of file float_bv.cpp.

◆ exponent_all_ones()

exprt float_bvt::exponent_all_ones	(	const exprt &	src,
		const ieee_float_spect &	spec
	)

staticprivate

Definition at line 260 of file float_bv.cpp.

◆ exponent_all_zeros()

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

staticprivate

Definition at line 269 of file float_bv.cpp.

◆ fma()

exprt float_bvt::fma	(	const exprt &	multiply_lhs,
		const exprt &	multiply_rhs,
		const exprt &	addend,
		const exprt &	rm,
		const ieee_float_spect &	spec
	)		const

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
rm	IEEE 754 rounding mode
spec	floating-point format specification

Definition at line 837 of file float_bv.cpp.

◆ fraction_all_zeros()

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

staticprivate

Definition at line 278 of file float_bv.cpp.

◆ 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
	)

staticprivate

rounding decision for fraction using sticky bit

Definition at line 1252 of file float_bv.cpp.

◆ from_signed_integer()

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

Definition at line 313 of file float_bv.cpp.

◆ from_unsigned_integer()

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

Definition at line 337 of file float_bv.cpp.

◆ get_exponent()

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

staticprivate

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

Definition at line 1056 of file float_bv.cpp.

◆ get_fraction()

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

staticprivate

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

Definition at line 1064 of file float_bv.cpp.

◆ get_spec()

ieee_float_spect float_bvt::get_spec ( const exprt & expr )

staticprivate

Definition at line 196 of file float_bv.cpp.

◆ is_equal()

exprt float_bvt::is_equal	(	const exprt &	src0,
		const exprt &	src1,
		const ieee_float_spect &	spec
	)

static

Definition at line 222 of file float_bv.cpp.

◆ is_zero()

exprt float_bvt::is_zero ( const exprt & src )

static

Definition at line 244 of file float_bv.cpp.

◆ isfinite()

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

static

Definition at line 1048 of file float_bv.cpp.

◆ isinf()

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

static

Definition at line 1039 of file float_bv.cpp.

◆ isnan()

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

static

Definition at line 1071 of file float_bv.cpp.

◆ isnormal()

exprt float_bvt::isnormal	(	const exprt &	src,
		const ieee_float_spect &	spec
	)

static

Definition at line 499 of file float_bv.cpp.

◆ limit_distance()

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

staticprivate

Limits the shift distance.

Definition at line 674 of file float_bv.cpp.

◆ mul()

exprt float_bvt::mul	(	const exprt &	src1,
		const exprt &	src2,
		const exprt &	rm,
		const ieee_float_spect &	spec
	)		const

Definition at line 697 of file float_bv.cpp.

◆ negation()

exprt float_bvt::negation	(	const exprt &	op,
		const ieee_float_spect &	spec
	)

static

Definition at line 212 of file float_bv.cpp.

◆ normalization_shift()

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

staticprivate

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

Definition at line 1080 of file float_bv.cpp.

◆ operator()()

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

inline

Definition at line 19 of file float_bv.h.

◆ pack()

exprt float_bvt::pack	(	const biased_floatt &	src,
		const ieee_float_spect &	spec
	)

staticprivate

Definition at line 1573 of file float_bv.cpp.

◆ relation()

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

static

Definition at line 956 of file float_bv.cpp.

◆ round_exponent()

void float_bvt::round_exponent	(	unbiased_floatt &	result,
		const rounding_mode_bitst &	rounding_mode_bits,
		const ieee_float_spect &	spec
	)

staticprivate

Definition at line 1422 of file float_bv.cpp.

◆ round_fraction()

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

staticprivate

Definition at line 1316 of file float_bv.cpp.

◆ rounder()

exprt float_bvt::rounder	(	const unbiased_floatt &	src,
		const exprt &	rm,
		const ieee_float_spect &	spec
	)		const

private

Definition at line 1209 of file float_bv.cpp.

◆ sign_bit()

exprt float_bvt::sign_bit ( const exprt & op )

staticprivate

Definition at line 306 of file float_bv.cpp.

◆ sticky_right_shift()

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

staticprivate

Definition at line 1604 of file float_bv.cpp.

◆ sub_bias()

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

staticprivate

Definition at line 1530 of file float_bv.cpp.

◆ subtract_exponents()

exprt float_bvt::subtract_exponents	(	const unbiased_floatt &	src1,
		const unbiased_floatt &	src2
	)

staticprivate

Subtracts the exponents.

Definition at line 509 of file float_bv.cpp.

◆ 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
	)

static

Definition at line 377 of file float_bv.cpp.

◆ 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
	)

static

Definition at line 359 of file float_bv.cpp.

◆ 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
	)

static

Definition at line 368 of file float_bv.cpp.

◆ unpack()

float_bvt::unbiased_floatt float_bvt::unpack	(	const exprt &	src,
		const ieee_float_spect &	spec
	)

staticprivate

Definition at line 1540 of file float_bv.cpp.

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

/home/runner/work/cbmc/cbmc/src/solvers/floatbv/float_bv.h
/home/runner/work/cbmc/cbmc/src/solvers/floatbv/float_bv.cpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Private Member Functions

Static Private Member Functions

Detailed Description

Member Enumeration Documentation

◆ relt

Member Function Documentation

◆ abs()

◆ add_bias()

◆ add_sub()

◆ bias()

◆ conversion()

◆ convert()

◆ denormalization_shift()

◆ div()

◆ exponent_all_ones()

◆ exponent_all_zeros()

◆ fma()

◆ fraction_all_zeros()

◆ fraction_rounding_decision()

◆ from_signed_integer()

◆ from_unsigned_integer()

◆ get_exponent()

◆ get_fraction()

◆ get_spec()

◆ is_equal()

◆ is_zero()

◆ isfinite()

◆ isinf()

◆ isnan()

◆ isnormal()

◆ limit_distance()

◆ mul()

◆ negation()

◆ normalization_shift()

◆ operator()()

◆ pack()

◆ relation()

◆ round_exponent()

◆ round_fraction()

◆ rounder()

◆ sign_bit()

◆ sticky_right_shift()

◆ sub_bias()

◆ subtract_exponents()

◆ to_integer()

◆ to_signed_integer()

◆ to_unsigned_integer()

◆ unpack()