cprover
string_constraint_generator_valueof.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_valueof.cpp:

Go to the source code of this file.

Functions

static unsigned long to_integer_or_default (const exprt &expr, unsigned long def, const namespacet &ns)
 If the expression is a constant expression then we get the value of it as an unsigned long. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_long (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 Add axioms corresponding to the String.valueOf(J) java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_bool (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Add axioms corresponding to the String.valueOf(Z) java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_bool (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &b)
 Add axioms stating that the returned string equals "true" when the Boolean expression is true and "false" when it is false. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_string_of_int (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &input_int, size_t max_size, const namespacet &ns)
 Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String.valueOf(J) Java functions applied on the integer expression. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_string_of_int_with_radix (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size, const namespacet &ns)
 Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String.valueOf(JI) Java functions applied on the integer expression. More...
 
static exprt int_of_hex_char (const exprt &chr)
 Returns the integer value represented by the character. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_int_hex (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &i)
 Add axioms stating that the string res corresponds to the integer argument written in hexadecimal. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_int_hex (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Add axioms corresponding to the Integer.toHexString(I) java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_char (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Conversion from char to string. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_char (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &c)
 Add axiom stating that string res has length 1 and the character it contains equals c. More...
 
string_constraintst add_axioms_for_correct_number_format (const array_string_exprt &str, const exprt &radix_as_char, const unsigned long radix_ul, const std::size_t max_size, const bool strict_formatting)
 Add axioms making the return value true if the given string is a correct number in the given radix. More...
 
string_constraintst add_axioms_for_characters_in_integer_string (const exprt &input_int, const typet &type, const bool strict_formatting, const array_string_exprt &str, const std::size_t max_string_length, const exprt &radix, const unsigned long radix_ul)
 Add axioms connecting the characters in the input string to the value of the output integer. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_parse_int (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 Integer value represented by a string. More...
 
exprt is_digit_with_radix (const exprt &chr, const bool strict_formatting, const exprt &radix_as_char, const unsigned long radix_ul)
 Check if a character is a digit with respect to the given radix, e.g. More...
 
exprt get_numeric_value_from_character (const exprt &chr, const typet &char_type, const typet &type, const bool strict_formatting, const unsigned long radix_ul)
 Get the numeric value of a character, assuming that the radix is large enough. More...
 
size_t max_printed_string_length (const typet &type, unsigned long radix_ul)
 Calculate the string length needed to represent any value of the given type using the given radix. 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_valueof.cpp.

Function Documentation

◆ add_axioms_for_characters_in_integer_string()

string_constraintst add_axioms_for_characters_in_integer_string ( const exprt input_int,
const typet type,
const bool  strict_formatting,
const array_string_exprt str,
const std::size_t  max_string_length,
const exprt radix,
const unsigned long  radix_ul 
)

Add axioms connecting the characters in the input string to the value of the output integer.

It is constructive because it gives a formula for input_int in terms of the characters in str.

Parameters
input_intthe integer represented by str
typethe type for input_int
strict_formattingif true, don't allow a leading plus, redundant zeros or upper case letters
strinput string
max_string_lengththe maximum length str can have
radixthe radix, with the same type as input_int
radix_ulthe radix as an unsigned long, or 0 if that can't be determined

Deal with size==1 case separately. There are axioms from add_axioms_for_correct_number_format which say that the string must contain at least one digit, so we don't have to worry about "+" or "-".

Definition at line 434 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_for_correct_number_format()

string_constraintst add_axioms_for_correct_number_format ( const array_string_exprt str,
const exprt radix_as_char,
const unsigned long  radix_ul,
const std::size_t  max_size,
const bool  strict_formatting 
)

Add axioms making the return value true if the given string is a correct number in the given radix.

Parameters
strstring expression
radix_as_charthe radix as an expression of the same type as the characters in str
radix_ulthe radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix
max_sizemaximum number of characters
strict_formattingif true, don't allow a leading plus, redundant zeros or upper case letters

index < length => is_digit_with_radix(str[index], radix)

Definition at line 348 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_for_parse_int()

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

Integer value represented by a string.

Add axioms ensuring the value of the returned integer corresponds to the value represented by str

Parameters
fresh_symbolgenerator of fresh symbols
fa function application with arguments refined_string str and an optional integer for the radix
array_poolpool of arrays representing strings
nsnamespace
Returns
integer expression equal to the value represented by str
Note
the only thing stopping us from taking longer strings with many leading zeros is the axioms for correct number format

Definition at line 526 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_for_string_of_int()

std::pair<exprt, string_constraintst> add_axioms_for_string_of_int ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const exprt input_int,
size_t  max_size,
const namespacet ns 
)

Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String.valueOf(J) Java functions applied on the integer expression.

Parameters
fresh_symbolgenerator of fresh symbols
resstring expression for the result
input_inta signed integer expression
max_sizea maximal size for the string representation (default 0, which is interpreted to mean "as large as is needed for this type")
nsnamespace
Returns
code 0 on success

Definition at line 140 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_for_string_of_int_with_radix()

std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const exprt input_int,
const exprt radix,
size_t  max_size,
const namespacet ns 
)

Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String.valueOf(JI) Java functions applied on the integer expression.

Parameters
fresh_symbolgenerator of fresh symbols
resstring expression for the result
input_inta signed integer expression
radixthe radix to use
max_sizea maximal size for the string representation (default 0, which is interpreted to mean "as large as is needed for this type")
nsnamespace
Returns
code 0 on success

Most of the time we can evaluate radix as an integer. The value 0 is used to indicate when we can't tell what the radix is.

Definition at line 163 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_bool() [1/2]

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

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

Deprecated:
This is Java specific and should be implemented in Java instead
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with a Boolean argument
array_poolpool of arrays representing strings
Returns
a new string expression

Definition at line 70 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_bool() [2/2]

std::pair<exprt, string_constraintst> add_axioms_from_bool ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const exprt b 
)

Add axioms stating that the returned string equals "true" when the Boolean expression is true and "false" when it is false.

Deprecated:
This is Java specific and should be implemented in Java instead
Parameters
fresh_symbolgenerator of fresh symbols
resstring expression for the result
bBoolean expression
Returns
code 0 on success

Definition at line 89 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_char() [1/2]

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

Conversion from char to string.

Add axiom stating that string res has length 1 and the character it contains equals c. (More...)

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with arguments integer |res|, character pointer &res[0] and character c
array_poolpool of arrays representing strings
Returns
code 0 on success

Definition at line 310 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_char() [2/2]

std::pair<exprt, string_constraintst> add_axioms_from_char ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const exprt c 
)

Add axiom stating that string res has length 1 and the character it contains equals c.

This axiom is: \( |{\tt res}| = 1 \land {\tt res}[0] = {\tt c} \).

Parameters
fresh_symbolgenerator of fresh symbols
resarray of characters expression
ccharacter expression
Returns
code 0 on success

Definition at line 329 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_int_hex() [1/2]

std::pair<exprt, string_constraintst> add_axioms_from_int_hex ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const exprt i 
)

Add axioms stating that the string res corresponds to the integer argument written in hexadecimal.

Deprecated:
use add_axioms_from_int_with_radix instead
Parameters
fresh_symbolgenerator of fresh symbols
resstring expression for the result
ian integer argument
Returns
code 0 on success

Definition at line 228 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_int_hex() [2/2]

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

Add axioms corresponding to the Integer.toHexString(I) java function.

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with an integer argument
array_poolpool of arrays representing strings
Returns
code 0 on success

Definition at line 287 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_long()

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

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

Deprecated:
should use add_axioms_from_int instead
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with one long argument
array_poolpool of arrays representing strings
nsnamespace
Returns
a new string expression

Definition at line 46 of file string_constraint_generator_valueof.cpp.

◆ get_numeric_value_from_character()

exprt get_numeric_value_from_character ( const exprt chr,
const typet char_type,
const typet type,
const bool  strict_formatting,
const unsigned long  radix_ul 
)

Get the numeric value of a character, assuming that the radix is large enough.

'+' and '-' yield 0.

Parameters
chrthe character to get the numeric value of
char_typethe type to use for characters
typethe type to use for the return value
strict_formattingif true, don't allow upper case characters
radix_ulthe radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix
Returns
an integer expression of the given type with the numeric value of the char

There are four cases, which occur in ASCII in the following order: '+' and '-', digits, upper case letters, lower case letters


return char >= '0' ? (char - '0') : 0

return char >= 'a' ? (char - 'a' + 10) : char >= '0' ? (char - '0') : 0
return char >= 'a' ? (char - 'a' + 10) : char >= 'A' ? (char - 'A' + 10) : char >= '0' ? (char - '0') : 0

Definition at line 649 of file string_constraint_generator_valueof.cpp.

◆ int_of_hex_char()

static exprt int_of_hex_char ( const exprt chr)
static

Returns the integer value represented by the character.

Parameters
chra character expression in the following set: 0123456789abcdef
Returns
an integer expression

Definition at line 209 of file string_constraint_generator_valueof.cpp.

◆ is_digit_with_radix()

exprt is_digit_with_radix ( const exprt chr,
const bool  strict_formatting,
const exprt radix_as_char,
const unsigned long  radix_ul 
)

Check if a character is a digit with respect to the given radix, e.g.

if the radix is 10 then check if the character is in the range 0-9.

Parameters
chrthe character
strict_formattingif true, don't allow upper case characters
radix_as_charthe radix as an expression of the same type as chr
radix_ulthe radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix
Returns
an expression for the condition

Definition at line 579 of file string_constraint_generator_valueof.cpp.

◆ max_printed_string_length()

size_t max_printed_string_length ( const typet type,
unsigned long  radix_ul 
)

Calculate the string length needed to represent any value of the given type using the given radix.

Due to floating point rounding errors we sometimes return a value 1 larger than needed, which is fine for our purposes.

Parameters
typethe type that we are considering values of
radix_ulthe radix we are using, or 0, in which case the return value will work for any radix
Returns
the maximum string length

We want to calculate max, the maximum number of characters needed to represent any value of the given type.

For signed types, the longest string will be for -2^(n_bits-1), so max = 1 + min{k: 2^(n_bits-1) < radix^k} (the 1 is for the minus sign) = 1 + min{k: n_bits-1 < k log_2(radix)} = 1 + min{k: k > (n_bits-1) / log_2(radix)} = 1 + min{k: k > floor((n_bits-1) / log_2(radix))} = 1 + (1 + floor((n_bits-1) / log_2(radix))) = 2 + floor((n_bits-1) / log_2(radix))

For unsigned types, the longest string will be for (2^n_bits)-1, so max = min{k: (2^n_bits)-1 < radix^k} = min{k: 2^n_bits <= radix^k} = min{k: n_bits <= k log_2(radix)} = min{k: k >= n_bits / log_2(radix)} = min{k: k >= ceil(n_bits / log_2(radix))} = ceil(n_bits / log_2(radix))

Definition at line 723 of file string_constraint_generator_valueof.cpp.

◆ to_integer_or_default()

static unsigned long to_integer_or_default ( const exprt expr,
unsigned long  def,
const namespacet ns 
)
static

If the expression is a constant expression then we get the value of it as an unsigned long.

If not we return a default value.

Parameters
exprinput expression
defdefault value to return if we cannot evaluate expr
nsnamespace used to simplify the expression
Returns
the output as an unsigned long

Definition at line 28 of file string_constraint_generator_valueof.cpp.