CBMC
Loading...
Searching...
No Matches
Classes | Public Types | Public Member Functions | Static Public Member Functions | Public Attributes | Protected Member Functions | Protected Attributes | List of all members
float_utilst Class Reference

#include <float_utils.h>

+ Inheritance diagram for float_utilst:
[フレーム]
[legend]
+ Collaboration diagram for float_utilst:
[フレーム]
[legend]

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:

AltStyle によって変換されたページ (->オリジナル) /