20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H 21 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H 27 #include <util/constexpr.def> 51 const std::unordered_map<exprt, array_string_exprt, irep_hash> &
76 std::unordered_map<array_string_exprt, symbol_exprt, irep_hash>
83 const exprt &char_pointer,
84 const typet &char_array_type);
104 const std::vector<string_not_contains_constraintt> &
121 const exprt &univ_val)
const 161 const exprt &start_index,
162 const exprt &end_index);
167 const exprt &offset);
186 const std::string &char_set);
212 const exprt &offset);
239 const std::string &s,
243 const format_specifiert &fs,
263 const exprt &input_int,
264 size_t max_size = 0);
267 const exprt &input_int,
269 size_t max_size = 0);
280 const exprt &from_index);
284 const exprt &from_index);
289 const exprt &from_index);
293 const exprt &from_index);
340 const exprt &code_point);
347 DEPRECATED(
"This is Java specific and should be implemented in Java")
360 const
exprt &input_int,
362 const
bool strict_formatting,
364 const
std::
size_t max_string_length,
366 const
unsigned long radix_ul);
368 const
exprt &input_int,
370 const
exprt &radix_as_char,
371 const
unsigned long radix_ul,
372 const
std::
size_t max_size,
373 const
bool strict_formatting);
419 const
bool strict_formatting,
420 const
exprt &radix_as_char,
421 const
unsigned long radix_ul);
427 const
bool strict_formatting,
428 unsigned long radix_ul);
455 const
exprt &start_index,
456 const
exprt &end_index);
461 const
exprt &offset);
exprt add_axioms_for_compare_to(const function_application_exprt &f)
Lexicographic comparison of two strings.
The type of an expression.
exprt add_axioms_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
Add axioms ensuring the result res corresponds to s1 where we inserted s2 at position offset...
std::vector< string_not_contains_constraintt > not_contains_constraints
const std::set< array_string_exprt > & get_created_strings() const
Set of strings that have been created by the generator.
exprt add_axioms_for_code_point_at(const function_application_exprt &f)
add axioms corresponding to the String.codePointAt java function
void 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...
std::map< array_string_exprt, symbol_exprt > intern_of_string
application of (mathematical) function
const std::vector< string_constraintt > & get_constraints() const
exprt get_witness_of(const string_not_contains_constraintt &c, const exprt &univ_val) const
exprt add_axioms_from_literal(const function_application_exprt &f)
String corresponding to an internal cprover string.
exprt add_axioms_from_int_with_radix(const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size=0)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String...
const signedbv_typet get_return_code_type()
exprt add_axioms_from_int(const function_application_exprt &f)
Convert an integer to a string.
exprt add_axioms_for_empty_string(const function_application_exprt &f)
Add axioms to say that the returned string expression is empty.
exprt add_axioms_for_equals(const function_application_exprt &f)
Equality of the content of two strings.
exprt add_axioms_for_length(const function_application_exprt &f)
Length of a string.
exprt add_axioms_for_insert_float(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.insert(F) java function.
Type for string expressions used by the string solver.
const std::vector< exprt > & get_lemmas() const
Axioms are of three kinds: universally quantified string constraint, not contains string constraints ...
std::map< array_string_exprt, exprt > hash_code_of_string
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.
Generation of fresh symbols of a given type.
array_poolt(symbol_generatort &symbol_generator)
std::unordered_map< exprt, array_string_exprt, irep_hash > arrays_of_pointers
exprt add_axioms_for_contains(const function_application_exprt &f)
Test whether a string contains another.
exprt add_axioms_for_code_point_count(const function_application_exprt &f)
Add axioms corresponding the String.codePointCount java function.
exprt add_axioms_for_offset_by_code_point(const function_application_exprt &f)
Add axioms corresponding the String.offsetByCodePointCount java function.
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
exprt associate_array_to_pointer(const function_application_exprt &f)
Associate a char array to a char pointer.
exprt get_length(const array_string_exprt &s) const
Associate an actual finite length to infinite arrays.
std::vector< symbol_exprt > boolean_symbols
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.
exprt associate_length_to_array(const function_application_exprt &f)
Associate an integer length to a char array.
exprt add_axioms_from_long(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(J) java function.
const std::vector< string_not_contains_constraintt > & get_not_contains_constraints() const
A constant literal expression.
Correspondance between arrays and pointers string representations.
exprt add_axioms_for_is_empty(const function_application_exprt &f)
Add axioms stating that the returned value is true exactly when the argument string is empty...
exprt add_axioms_for_trim(const function_application_exprt &f)
Remove leading and trailing whitespaces.
exprt add_axioms_for_index_of(const array_string_exprt &str, const exprt &c, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack (str) of the first occurrence...
exprt minimum(const exprt &a, const exprt &b)
void clear_constraints()
Clear all constraints and lemmas.
const std::vector< symbol_exprt > & get_boolean_symbols() const
Boolean symbols for the results of some string functions.
exprt add_axioms_for_function_application(const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms...
exprt 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...
exprt add_axioms_from_double(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(D) java function.
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
exprt add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
The boolean constant true.
exprt add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt())
Add axioms ensuring that the provided string expression and constant are equal.
Constraints to encode non containement of strings.
Defines string constraints.
DEPRECATED("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table
Instruments goto program for a given coverage criterion.
exprt add_axioms_for_hash_code(const function_application_exprt &f)
Value that is identical for strings with the same content.
exprt add_axioms_for_delete_char_at(const function_application_exprt &expr)
add axioms corresponding to the StringBuilder.deleteCharAt java function
exprt add_axioms_for_index_of_string(const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index)
Add axioms stating that the returned value index is the index within haystack of the first occurrence...
std::vector< symbol_exprt > index_symbols
symbol_exprt add_axioms_for_intern(const function_application_exprt &f)
Add axioms corresponding to the String.intern java function.
Fixed-width bit-vector with two's complement interpretation.
exprt add_axioms_for_replace(const function_application_exprt &f)
Replace a character by another in a string.
exprt add_axioms_for_parse_int(const function_application_exprt &f)
Integer value represented by a string.
nonstd::optional< T > optionalt
exprt add_axioms_for_is_suffix(const function_application_exprt &f, bool swap_arguments=false)
Test if the target is a suffix of the string.
exprt add_axioms_for_last_index_of_string(const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack of the last occurrence of nee...
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 ...
exprt add_axioms_for_set_length(const function_application_exprt &f)
Reduce or extend a string to have the given length.
exprt add_axioms_for_equals_ignore_case(const function_application_exprt &f)
Equality of the content ignoring case of characters.
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...
exprt add_axioms_for_char_literal(const function_application_exprt &f)
add axioms stating that the returned value is equal to the argument
symbol_exprt operator()(const irep_idt &prefix, const typet &type=bool_typet())
generate a new symbol expression of the given type with some prefix
bitvector_typet index_type()
array_string_exprt make_char_array_for_char_pointer(const exprt &char_pointer, const typet &char_array_type)
exprt add_axioms_for_char_set(const function_application_exprt &f)
Set a character to a specific value at an index of the string.
static exprt is_low_surrogate(const exprt &chr)
the output is true when the character is a low surrogate for UTF-16 encoding, see https://en...
array_string_exprt of_argument(const exprt &arg)
Converts a struct containing a length and pointer to an array.
exprt add_axioms_for_insert_double(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(D) java function
exprt add_axioms_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 res is the concatenation of s1 with the substring of s2 starting at index â...
exprt add_axioms_for_insert_int(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(I) java function
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 ...
const std::unordered_map< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
std::vector< exprt > operandst
unsigned long to_integer_or_default(const exprt &expr, unsigned long def)
If the expression is a constant expression then we get the value of it as an unsigned long...
exprt maximum(const exprt &a, const exprt &b)
void insert(const exprt &pointer_expr, array_string_exprt &array)
String expressions for the string solver.
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type)
generate an index symbol which is existentially quantified
string_constraint_generatort(const namespacet &ns)
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.
exprt add_axioms_for_copy(const function_application_exprt &f)
add axioms to say that the returned string expression is equal to the argument of the function applic...
exprt add_axioms_for_char_at(const function_application_exprt &f)
Character at a given position.
exprt add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms stating that res corresponds to the input str where we removed characters between the posi...
exprt add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(st...
void add_constraint_on_characters(const array_string_exprt &s, const exprt &start, const exprt &end, const std::string &char_set)
Add constraint on characters of a string.
Base class for all expressions.
optionalt< exprt > make_array_pointer_association(const function_application_exprt &expr)
Associate array to pointer, and array to length.
exprt add_axioms_for_code_point(const array_string_exprt &res, const exprt &code_point)
add axioms for the conversion of an integer representing a java code point to a utf-16 string ...
exprt add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
Add axioms stating that the returned expression is true exactly when the offset is greater or equal t...
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...
exprt add_axioms_from_bool(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(Z) java function.
exprt add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
exprt add_axioms_for_format(const function_application_exprt &f)
Formatted string using a format string and list of arguments.
std::set< array_string_exprt > created_strings
Universally quantified string constraint
exprt add_axioms_for_to_lower_case(const function_application_exprt &f)
Conversion of a string to lower case.
exprt add_axioms_for_code_point_before(const function_application_exprt &f)
add axioms corresponding to the String.codePointBefore java function
static exprt character_equals_ignore_case(exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z)
Returns an expression which is true when the two given characters are equal when ignoring case for AS...
std::vector< exprt > lemmas
exprt sum_overflows(const plus_exprt &sum)
exprt add_axioms_for_constrain_characters(const function_application_exprt &f)
Add axioms to ensure all characters of a string belong to a given set.
exprt add_axioms_for_cprover_string(const array_string_exprt &res, const exprt &arg, const exprt &guard)
Convert an expression of type string_typet to a string_exprt.
Expression to hold a symbol (variable)
void add_axioms_for_correct_number_format(const exprt &input_int, 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...
exprt add_axioms_for_fractional_part(const array_string_exprt &res, const exprt &i, size_t max_size)
Add axioms for representing the fractional part of a floating point starting with a dot...
exprt add_axioms_for_insert_bool(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(Z) java function
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
const array_string_exprt & char_array_of_pointer(const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
std::vector< string_constraintt > constraints
std::map< string_not_contains_constraintt, symbol_exprt > witness
std::unordered_map< array_string_exprt, symbol_exprt, irep_hash > length_of_array
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
exprt add_axioms_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1, const exprt &c)
Add axioms enforcing that res is the concatenation of s1 with character c.
exprt add_axioms_from_char(const function_application_exprt &f)
Conversion from char to string.
const std::vector< symbol_exprt > & get_index_symbols() const
Symbols used in existential quantifications.
struct constructor from list of elements
static exprt int_of_hex_char(const exprt &chr)
Returns the integer value represented by the character.
static exprt is_high_surrogate(const exprt &chr)
the output is true when the character is a high surrogate for UTF-16 encoding, see https://en...
bitvector_typet char_type()
exprt add_axioms_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.
exprt add_axioms_for_concat_code_point(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
array constructor from list of elements
array_string_exprt get_string_expr(const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
void add_lemma(const exprt &)
exprt add_axioms_for_insert_char(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.insert(C) java function.
exprt add_axioms_for_last_index_of(const array_string_exprt &str, const exprt &c, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack (str) of the last occurrence ...
symbol_generatort & fresh_symbol
exprt add_axioms_for_to_upper_case(const function_application_exprt &f)
Conversion of a string to upper case.
symbol_generatort fresh_symbol
exprt axiom_for_is_positive_index(const exprt &x)
expression true exactly when the index is positive
array_string_exprt add_axioms_for_format_specifier(const format_specifiert &fs, const struct_exprt &arg, const typet &index_type, const typet &char_type)
Parse s and add axioms ensuring the output corresponds to the output of String.format.