cprover
|
Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool. More...
#include <solvers/refinement/string_refinement_invariant.h>
#include <solvers/refinement/string_constraint_generator.h>
#include <util/simplify_expr.h>
#include <util/deprecate.h>
#include <cmath>
#include <solvers/floatbv/float_bv.h>
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_constraintst > | add_axioms_from_long (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_constraintst > | add_axioms_from_bool (const function_application_exprt &f, array_poolt &array_pool) |
Add axioms corresponding to the String.valueOf(Z) java function. More... | |
std::pair< exprt, string_constraintst > | add_axioms_from_bool (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_constraintst > | add_axioms_for_string_of_int (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_constraintst > | add_axioms_for_string_of_int_with_radix (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_constraintst > | add_axioms_from_int_hex (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_constraintst > | add_axioms_from_int_hex (const function_application_exprt &f, array_poolt &array_pool) |
Add axioms corresponding to the Integer.toHexString(I) java function. More... | |
std::pair< exprt, string_constraintst > | add_axioms_from_char (const function_application_exprt &f, array_poolt &array_pool) |
Conversion from char to string. More... | |
std::pair< exprt, string_constraintst > | add_axioms_from_char (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_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. 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... | |
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.
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.
input_int | the integer represented by str |
type | the type for input_int |
strict_formatting | if true, don't allow a leading plus, redundant zeros or upper case letters |
str | input string |
max_string_length | the maximum length str can have |
radix | the radix, with the same type as input_int |
radix_ul | the 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 415 of file string_constraint_generator_valueof.cpp.
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.
str | string expression |
radix_as_char | the radix as an expression of the same type as the characters in str |
radix_ul | the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix |
max_size | maximum number of characters |
strict_formatting | if 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 329 of file string_constraint_generator_valueof.cpp.
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
fresh_symbol | generator of fresh symbols |
f | a function application with arguments refined_string str and an optional integer for the radix |
array_pool | pool of arrays representing strings |
ns | namespace |
str
Definition at line 507 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_string_of_int | ( | 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.
res | string expression for the result |
input_int | a signed integer expression |
max_size | a maximal size for the string representation (default 0, which is interpreted to mean "as large as is needed for this type") |
ns | namespace |
Definition at line 132 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix | ( | 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.
res | string expression for the result |
input_int | a signed integer expression |
radix | the radix to use |
max_size | a maximal size for the string representation (default 0, which is interpreted to mean "as large as is needed for this type") |
ns | namespace |
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 153 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_bool | ( | const function_application_exprt & | f, |
array_poolt & | array_pool | ||
) |
Add axioms corresponding to the String.valueOf(Z) java function.
f | function application with a Boolean argument |
array_pool | pool of arrays representing strings |
Definition at line 66 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_bool | ( | 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.
res | string expression for the result |
b | Boolean expression |
Definition at line 83 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_char | ( | 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...)
f | function application with arguments integer |res| , character pointer &res[0] and character c |
array_pool | pool of arrays representing strings |
Definition at line 294 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_char | ( | 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} \).
res | array of characters expression |
c | character expression |
Definition at line 311 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_int_hex | ( | const array_string_exprt & | res, |
const exprt & | i | ||
) |
Add axioms stating that the string res
corresponds to the integer argument written in hexadecimal.
res | string expression for the result |
i | an integer argument |
Definition at line 216 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_int_hex | ( | const function_application_exprt & | f, |
array_poolt & | array_pool | ||
) |
Add axioms corresponding to the Integer.toHexString(I) java function.
f | function application with an integer argument |
array_pool | pool of arrays representing strings |
Definition at line 273 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_long | ( | const function_application_exprt & | f, |
array_poolt & | array_pool, | ||
const namespacet & | ns | ||
) |
Add axioms corresponding to the String.valueOf(J) java function.
f | function application with one long argument |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 45 of file string_constraint_generator_valueof.cpp.
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.
chr | the character to get the numeric value of |
char_type | the type to use for characters |
type | the type to use for the return value |
strict_formatting | if true, don't allow upper case characters |
radix_ul | the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix |
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 630 of file string_constraint_generator_valueof.cpp.
Returns the integer value represented by the character.
chr | a character expression in the following set: 0123456789abcdef |
Definition at line 198 of file string_constraint_generator_valueof.cpp.
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.
chr | the character |
strict_formatting | if true, don't allow upper case characters |
radix_as_char | the radix as an expression of the same type as chr |
radix_ul | the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix |
Definition at line 560 of file string_constraint_generator_valueof.cpp.
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.
type | the type that we are considering values of |
radix_ul | the radix we are using, or 0, in which case the return value will work for any radix |
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 704 of file string_constraint_generator_valueof.cpp.
|
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.
expr | input expression |
def | default value to return if we cannot evaluate expr |
ns | namespace used to simplify the expression |
Definition at line 28 of file string_constraint_generator_valueof.cpp.