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 <solvers/floatbv/float_bv.h>
#include "string_constraint_generator.h"
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 &float_expr, 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

 std::pair 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
 res string expression for the result int_expr an integer expression max_size a 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 257 of file string_constraint_generator_float.cpp.

 std::pair 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_symbol generator of fresh symbols f function application with one float argument array_pool pool of arrays representing strings ns namespace
Returns
an integer expression

Definition at line 161 of file string_constraint_generator_float.cpp.

 std::pair 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_symbol generator of fresh symbols res string expression corresponding to the result f a float expression, which is positive array_pool pool of arrays representing strings ns namespace
Returns
an integer expression, different from zero if an error should be raised

Definition at line 203 of file string_constraint_generator_float.cpp.

 std::pair 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_symbol generator of fresh symbols f function application with one double argument array_pool pool of arrays representing strings ns namespace
Returns
an integer expression

Definition at line 179 of file string_constraint_generator_float.cpp.

 std::pair add_axioms_from_float_scientific_notation ( symbol_generatort & fresh_symbol, const array_string_exprt & res, const exprt & float_expr, 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_symbol generator of fresh symbols res string expression representing the float in scientific notation float_expr a float expression, which is positive array_pool pool of arrays representing strings ns namespace
Returns
a integer expression different from 0 to signal an exception

Definition at line 347 of file string_constraint_generator_float.cpp.

 std::pair 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_symbol generator of fresh symbols f a function application expression array_pool pool of arrays representing strings ns namespace
Returns
code 0 on success

Definition at line 546 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
 f a floating point value in double precision float_spec a 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
 f a floating point expression spec specification for floating point

Definition at line 139 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
 f a floating point expression g a floating point expression
Returns
An expression representing floating point multiplication.

Definition at line 103 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
 i an expression representing an integer spec specification for floating point numbers
Returns
An expression representing the value of the input integer as a float.

Definition at line 120 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
 src a floating point expression spec specification 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 26 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
 src a floating point expression spec specification for floating points
Returns
An unsigned value representing the fractional part.

Definition at line 42 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
 src a floating point expression spec specification for floating points type type 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 57 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
 f expression representing a float
Returns
expression representing a 32 bit integer

Definition at line 91 of file string_constraint_generator_float.cpp.