cprover
string_constraint_generator_float.cpp File Reference

Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool. More...

+ Include dependency graph for string_constraint_generator_float.cpp:

Go to the source code of this file.

Functions

exprt get_exponent (const exprt &src, const ieee_float_spect &spec)
 Gets the unbiased exponent in a floating-point bit-vector. More...
 
exprt get_fraction (const exprt &src, const ieee_float_spect &spec)
 Gets the fraction without hidden bit. More...
 
exprt get_significand (const exprt &src, const ieee_float_spect &spec, const typet &type)
 Gets the significand as a java integer, looking for the hidden bit. More...
 
exprt constant_float (const double f, const ieee_float_spect &float_spec)
 Create an expression to represent a float or double value. More...
 
exprt round_expr_to_zero (const exprt &f)
 Round a float expression to an integer closer to 0. More...
 
exprt floatbv_mult (const exprt &f, const exprt &g)
 Multiplication of expressions representing floating points. More...
 
exprt floatbv_of_int_expr (const exprt &i, const ieee_float_spect &spec)
 Convert integers to floating point to be used in operations with other values that are in floating point representation. More...
 
exprt estimate_decimal_exponent (const exprt &f, const ieee_float_spect &spec)
 Estimate the decimal exponent that should be used to represent a given floating point value in decimal. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_string_of_float (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 String representation of a float value. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_double (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 Add axioms corresponding to the String.valueOf(D) java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_string_of_float (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &f, array_poolt &array_pool, const namespacet &ns)
 Add axioms corresponding to the integer part of m, in decimal form with no leading zeroes, followed by '. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_fractional_part (const array_string_exprt &res, const exprt &int_expr, size_t max_size)
 Add axioms for representing the fractional part of a floating point starting with a dot. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_float_scientific_notation (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &f, array_poolt &array_pool, const namespacet &ns)
 Add axioms to write the float in scientific notation. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_float_scientific_notation (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 Representation of a float value in scientific notation. More...
 

Detailed Description

Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool.

Definition in file string_constraint_generator_float.cpp.

Function Documentation

◆ add_axioms_for_fractional_part()

std::pair<exprt, string_constraintst> add_axioms_for_fractional_part ( const array_string_exprt res,
const exprt int_expr,
size_t  max_size 
)

Add axioms for representing the fractional part of a floating point starting with a dot.

Parameters
resstring expression for the result
int_expran integer expression
max_sizea maximal size for the string, this includes the potential minus sign and therefore should be greater than 2
Returns
code 0 on success

Definition at line 255 of file string_constraint_generator_float.cpp.

◆ add_axioms_for_string_of_float() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_string_of_float ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool,
const namespacet ns 
)

String representation of a float value.

Add axioms corresponding to the String.valueOf(F) java function

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with one float argument
array_poolpool of arrays representing strings
nsnamespace
Returns
an integer expression

Definition at line 158 of file string_constraint_generator_float.cpp.

◆ add_axioms_for_string_of_float() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_string_of_float ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const exprt f,
array_poolt array_pool,
const namespacet ns 
)

Add axioms corresponding to the integer part of m, in decimal form with no leading zeroes, followed by '.

', followed by one or more decimal digits representing the fractional part of m. This specification is correct for inputs that do not exceed 100000 and the function is unspecified for other values.

Parameters
fresh_symbolgenerator of fresh symbols
resstring expression corresponding to the result
fa float expression, which is positive
array_poolpool of arrays representing strings
nsnamespace
Returns
an integer expression, different from zero if an error should be raised

Definition at line 201 of file string_constraint_generator_float.cpp.

◆ add_axioms_from_double()

std::pair<exprt, string_constraintst> add_axioms_from_double ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool,
const namespacet ns 
)

Add axioms corresponding to the String.valueOf(D) java function.

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with one double argument
array_poolpool of arrays representing strings
nsnamespace
Returns
an integer expression

Definition at line 177 of file string_constraint_generator_float.cpp.

◆ add_axioms_from_float_scientific_notation() [1/2]

std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const exprt f,
array_poolt array_pool,
const namespacet ns 
)

Add axioms to write the float in scientific notation.

A float is represented as \(f = m * 2^e\) where \(0 <= m < 2\) is the significand and \(-126 <= e <= 127\) is the exponent. We want an alternate representation by finding \(n\) and \(d\) such that \(f=n*10^d\). We can estimate \(d\) the following way: \(d ~= log_10(f/n) ~= log_10(m) + log_10(2) * e - log_10(n)\) \(d = floor(log_10(2) * e)\) Then \(n\) can be expressed by the equation: \(log_10(n) = log_10(m) + log_10(2) * e - d\) \(n = f / 10^d = m * 2^e / 10^d = m * 2^e / 10^(floor(log_10(2) * e))\)

Parameters
fresh_symbolgenerator of fresh symbols
resstring expression representing the float in scientific notation
fa float expression, which is positive
array_poolpool of arrays representing strings
nsnamespace
Returns
a integer expression different from 0 to signal an exception

Definition at line 344 of file string_constraint_generator_float.cpp.

◆ add_axioms_from_float_scientific_notation() [2/2]

std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool,
const namespacet ns 
)

Representation of a float value in scientific notation.

Add axioms corresponding to the scientific representation of floating point values

Parameters
fresh_symbolgenerator of fresh symbols
fa function application expression
array_poolpool of arrays representing strings
nsnamespace
Returns
code 0 on success

Definition at line 540 of file string_constraint_generator_float.cpp.

◆ constant_float()

exprt constant_float ( const double  f,
const ieee_float_spect float_spec 
)

Create an expression to represent a float or double value.

Parameters
fa floating point value in double precision
float_speca specification for floats
Returns
an expression representing this floating point

Definition at line 76 of file string_constraint_generator_float.cpp.

◆ estimate_decimal_exponent()

exprt estimate_decimal_exponent ( const exprt f,
const ieee_float_spect spec 
)

Estimate the decimal exponent that should be used to represent a given floating point value in decimal.

We are looking for \(d\) such that \(n * 10^d = m * 2^e\), so: \(d = log_10(m) + log_10(2) * e - log_10(n)\) m – the fraction – should be between 1 and 2 so log_10(m) in [0,log_10(2)]. n – the fraction in base 10 – should be between 1 and 10 so log_10(n) in [0, 1]. So the estimate is given by: d ~=~ floor(log_10(2) * e)

Parameters
fa floating point expression
specspecification for floating point

Definition at line 137 of file string_constraint_generator_float.cpp.

◆ floatbv_mult()

exprt floatbv_mult ( const exprt f,
const exprt g 
)

Multiplication of expressions representing floating points.

Note that the rounding mode is set to ROUND_TO_EVEN.

Parameters
fa floating point expression
ga floating point expression
Returns
An expression representing floating point multiplication.

Definition at line 102 of file string_constraint_generator_float.cpp.

◆ floatbv_of_int_expr()

exprt floatbv_of_int_expr ( const exprt i,
const ieee_float_spect spec 
)

Convert integers to floating point to be used in operations with other values that are in floating point representation.

Parameters
ian expression representing an integer
specspecification for floating point numbers
Returns
An expression representing the value of the input integer as a float.

Definition at line 119 of file string_constraint_generator_float.cpp.

◆ get_exponent()

exprt get_exponent ( const exprt src,
const ieee_float_spect spec 
)

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

Parameters
srca floating point expression
specspecification for floating points
Returns
A new 32 bit integer expression representing the exponent. Note that 32 bits are sufficient for the exponent even in octuple precision.

Definition at line 27 of file string_constraint_generator_float.cpp.

◆ get_fraction()

exprt get_fraction ( const exprt src,
const ieee_float_spect spec 
)

Gets the fraction without hidden bit.

Parameters
srca floating point expression
specspecification for floating points
Returns
An unsigned value representing the fractional part.

Definition at line 44 of file string_constraint_generator_float.cpp.

◆ get_significand()

exprt get_significand ( const exprt src,
const ieee_float_spect spec,
const typet type 
)

Gets the significand as a java integer, looking for the hidden bit.

Since the most significant bit is 1 for normalized number, it is not part of the encoding of the significand and is 0 only if all the bits of the exponent are 0, that is why it is called the hidden bit.

Parameters
srca floating point expression
specspecification for floating points
typetype of the output, should be unsigned with width greater than the width of the significand in the given spec
Returns
An integer expression of the given type representing the significand.

Definition at line 59 of file string_constraint_generator_float.cpp.

◆ round_expr_to_zero()

exprt round_expr_to_zero ( const exprt f)

Round a float expression to an integer closer to 0.

Parameters
fexpression representing a float
Returns
expression representing a 32 bit integer

Definition at line 91 of file string_constraint_generator_float.cpp.