cprover
|
Generates string constraints to link results from string functions with their arguments. More...
#include <limits>
#include <util/string_expr.h>
#include <util/replace_expr.h>
#include <util/refined_string_type.h>
#include <util/constexpr.def>
#include <util/deprecate.h>
#include <solvers/refinement/string_constraint.h>
Go to the source code of this file.
Classes | |
class | symbol_generatort |
Generation of fresh symbols of a given type. More... | |
class | array_poolt |
Correspondance between arrays and pointers string representations. More... | |
class | string_constraint_generatort |
Functions | |
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, 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 ul_radix) |
Calculate the string length needed to represent any value of the given type using the given radix. More... | |
std::string | utf16_constant_array_to_java (const array_exprt &arr, std::size_t length) |
Construct a string from a constant array. More... | |
exprt | minimum (const exprt &a, const exprt &b) |
exprt | maximum (const exprt &a, const exprt &b) |
exprt | sum_overflows (const plus_exprt &sum) |
exprt | length_constraint_for_concat_char (const array_string_exprt &res, const array_string_exprt &s1) |
Add axioms enforcing that the length of res is that of the concatenation of s1 with. More... | |
exprt | length_constraint_for_concat (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2) |
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2 More... | |
exprt | length_constraint_for_concat_substr (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index) |
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of s2 starting at index ‘start’ and ending at index end'`. More... | |
exprt | length_constraint_for_insert (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset) |
Add axioms ensuring the length of res corresponds that of s1 where we inserted s2 at position offset . More... | |
Generates string constraints to link results from string functions with their arguments.
This is inspired by the PASS paper at HVC'13: "PASS: String Solving with Parameterized Array and Interval Automaton" by Guodong Li and Indradeep Ghosh, which gives examples of constraints for several functions.
Definition in file string_constraint_generator.h.
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 628 of file string_constraint_generator_valueof.cpp.
References char_type(), and from_integer().
Referenced by string_constraint_generatort::add_axioms_for_characters_in_integer_string().
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 558 of file string_constraint_generator_valueof.cpp.
References char_type(), exprt::copy_to_operands(), from_integer(), PRECONDITION, and exprt::type().
Referenced by string_constraint_generatort::add_axioms_for_correct_number_format().
exprt length_constraint_for_concat | ( | const array_string_exprt & | res, |
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2 | ||
) |
Add axioms enforcing that the length of res
is that of the concatenation of s1
with s2
Definition at line 95 of file string_constraint_generator_concat.cpp.
References array_string_exprt::length().
Referenced by string_concatenation_builtin_functiont::length_constraint().
exprt length_constraint_for_concat_char | ( | const array_string_exprt & | res, |
const array_string_exprt & | s1 | ||
) |
Add axioms enforcing that the length of res
is that of the concatenation of s1
with.
Definition at line 135 of file string_constraint_generator_concat.cpp.
References from_integer(), and array_string_exprt::length().
Referenced by string_constraint_generatort::add_axioms_for_concat_char(), and string_concat_char_builtin_functiont::length_constraint().
exprt length_constraint_for_concat_substr | ( | const array_string_exprt & | res, |
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2, | ||
const exprt & | start, | ||
const exprt & | end | ||
) |
Add axioms enforcing that the length of res
is that of the concatenation of s1
with the substring of s2
starting at index ‘start’ and ending at index
end'`.
Where start_index' is max(0, start) and end' is max(min(end, s2.length), start')
Definition at line 77 of file string_constraint_generator_concat.cpp.
References from_integer(), irept::id(), array_string_exprt::length(), maximum(), minimum(), PRECONDITION, sum_overflows(), to_signedbv_type(), and exprt::type().
Referenced by string_constraint_generatort::add_axioms_for_concat_substr(), and string_concatenation_builtin_functiont::length_constraint().
exprt length_constraint_for_insert | ( | const array_string_exprt & | res, |
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2, | ||
const exprt & | offset | ||
) |
Add axioms ensuring the length of res
corresponds that of s1
where we inserted s2
at position offset
.
Definition at line 74 of file string_constraint_generator_insert.cpp.
References array_string_exprt::length().
Referenced by string_constraint_generatort::add_axioms_for_insert(), and string_insertion_builtin_functiont::length_constraint().
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 702 of file string_constraint_generator_valueof.cpp.
References bitvector_typet::get_width(), irept::id(), and to_bitvector_type().
Referenced by string_constraint_generatort::add_axioms_for_parse_int(), and string_constraint_generatort::add_axioms_from_int_with_radix().
Definition at line 626 of file string_constraint_generator_main.cpp.
Referenced by string_constraint_generatort::add_axioms_for_concat_substr(), string_constraint_generatort::add_axioms_for_insert(), string_constraint_generatort::add_axioms_for_offset_by_code_point(), string_constraint_generatort::add_axioms_for_substring(), and length_constraint_for_concat_substr().
Definition at line 621 of file string_constraint_generator_main.cpp.
Referenced by string_constraint_generatort::add_axioms_for_char_set(), string_constraint_generatort::add_axioms_for_code_point_count(), string_constraint_generatort::add_axioms_for_concat_substr(), string_constraint_generatort::add_axioms_for_insert(), string_constraint_generatort::add_axioms_for_offset_by_code_point(), string_constraint_generatort::add_axioms_for_set_length(), string_constraint_generatort::add_axioms_for_substring(), and length_constraint_for_concat_substr().
exprt sum_overflows | ( | const plus_exprt & | sum | ) |
Definition at line 132 of file string_constraint_generator_main.cpp.
References from_integer(), exprt::op0(), exprt::op1(), exprt::operands(), PRECONDITION, and exprt::type().
Referenced by length_constraint_for_concat_substr().
std::string utf16_constant_array_to_java | ( | const array_exprt & | arr, |
std::size_t | length | ||
) |
Construct a string from a constant array.
arr | an array expression containing only constants |
length | an unsigned value representing the length of the array |
length
represented by the array assuming each field in arr
represents a character. Definition at line 435 of file string_constraint_generator_format.cpp.
References INVARIANT, exprt::operands(), PRECONDITION, to_constant_expr(), to_unsigned_integer(), and utf16_little_endian_to_java().
Referenced by string_constraint_generatort::add_axioms_for_format(), and string_of_array().