cprover
|
#include <string_constraint_generator.h>
Public Member Functions | |
string_constraint_generatort () | |
void | set_mode (irep_idt _mode) |
irep_idt & | get_mode () |
exprt | get_witness_of (const string_not_contains_constraintt &c, const exprt &univ_val) const |
symbol_exprt | fresh_exist_index (const irep_idt &prefix, const typet &type) |
generate an index symbol which is existentially quantified More... | |
symbol_exprt | fresh_univ_index (const irep_idt &prefix, const typet &type) |
generate an index symbol to be used as an universaly quantified variable More... | |
symbol_exprt | fresh_boolean (const irep_idt &prefix) |
generate a Boolean symbol which is existentially quantified More... | |
string_exprt | fresh_string (const refined_string_typet &type) |
construct a string expression whose length and content are new variables More... | |
string_exprt | find_or_add_string_of_symbol (const symbol_exprt &sym) |
if a symbol represent a string is present in the symbol_to_string table, returns the corresponding string, if the symbol is not yet present, creates a new string with the correct type depending on whether the mode is java or c, adds it to the table and returns it. More... | |
void | assign_to_symbol (const symbol_exprt &sym, const string_exprt &expr) |
string_exprt | add_axioms_for_string_expr (const exprt &expr) |
obtain a refined string expression corresponding to string variable of string function call More... | |
void | set_string_symbol_equal_to_expr (const symbol_exprt &sym, const exprt &str) |
add a correspondence to make sure the symbol points to the same string as the second argument More... | |
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. More... | |
Static Public Member Functions | |
static symbol_exprt | fresh_symbol (const irep_idt &prefix, const typet &type=bool_typet()) |
generate a new symbol expression of the given type with some prefix More... | |
static constant_exprt | constant_char (int i, const typet &char_type) |
generate constant character expression with character type. More... | |
Public Attributes | |
std::list< exprt > | axioms |
std::list< symbol_exprt > | boolean_symbols |
std::list< symbol_exprt > | index_symbols |
std::map< string_not_contains_constraintt, symbol_exprt > | witness |
std::map< irep_idt, string_exprt > | symbol_to_string |
Static Public Attributes | |
static unsigned | next_symbol_id =1 |
Private Member Functions | |
exprt | axiom_for_is_positive_index (const exprt &x) |
expression true exactly when the index is positive More... | |
exprt | add_axioms_for_char_at (const function_application_exprt &f) |
add axioms stating that the character of the string at the given position is equal to the returned value More... | |
exprt | add_axioms_for_code_point_at (const function_application_exprt &f) |
add axioms corresponding to the String.codePointAt java function More... | |
exprt | add_axioms_for_code_point_before (const function_application_exprt &f) |
add axioms corresponding to the String.codePointBefore java function More... | |
exprt | add_axioms_for_contains (const function_application_exprt &f) |
add axioms corresponding to the String.contains java function More... | |
exprt | add_axioms_for_equals (const function_application_exprt &f) |
add axioms stating that the result is true exactly when the strings represented by the arguments are equal More... | |
exprt | add_axioms_for_equals_ignore_case (const function_application_exprt &f) |
add axioms corresponding to the String.equalsIgnoreCase java function More... | |
exprt | add_axioms_for_hash_code (const function_application_exprt &f) |
add axioms stating that if two strings are equal then their hash codes are equals More... | |
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 More... | |
exprt | add_axioms_for_is_prefix (const string_exprt &prefix, const string_exprt &str, const exprt &offset) |
add axioms stating that the returned expression is true exactly when the first string is a prefix of the second one, starting at position offset More... | |
exprt | add_axioms_for_is_prefix (const function_application_exprt &f, bool swap_arguments=false) |
add axioms corresponding to the String.isPrefix java function More... | |
exprt | add_axioms_for_is_suffix (const function_application_exprt &f, bool swap_arguments=false) |
add axioms corresponding to the String.isSuffix java function More... | |
exprt | add_axioms_for_length (const function_application_exprt &f) |
add axioms corresponding to the String.length java function More... | |
string_exprt | add_axioms_for_empty_string (const function_application_exprt &f) |
add axioms to say that the returned string expression is empty More... | |
string_exprt | add_axioms_for_char_set (const function_application_exprt &expr) |
add axioms corresponding stating that the result is similar to that of the StringBuilder.setCharAt java function Warning: this may be underspecified in the case wher the index exceed the length of the string More... | |
string_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 application More... | |
string_exprt | add_axioms_for_concat (const string_exprt &s1, const string_exprt &s2) |
add axioms to say that the returned string expression is equal to the concatenation of the two string expressions given as input More... | |
string_exprt | add_axioms_for_concat (const function_application_exprt &f) |
add axioms to say that the returned string expression is equal to the concatenation of the two string arguments of the function application More... | |
string_exprt | add_axioms_for_concat_int (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.append(I) java function More... | |
string_exprt | add_axioms_for_concat_long (const function_application_exprt &f) |
Add axioms corresponding to the StringBuilder.append(J) java function. More... | |
string_exprt | add_axioms_for_concat_bool (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.append(Z) java function More... | |
string_exprt | add_axioms_for_concat_char (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.append(C) java function More... | |
string_exprt | add_axioms_for_concat_double (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.append(D) java function More... | |
string_exprt | add_axioms_for_concat_float (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.append(F) java function More... | |
string_exprt | add_axioms_for_concat_code_point (const function_application_exprt &f) |
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function. More... | |
string_exprt | add_axioms_for_constant (irep_idt sval, const refined_string_typet &ref_type) |
add axioms saying the returned string expression should be equal to the string constant More... | |
string_exprt | add_axioms_for_delete (const string_exprt &str, const exprt &start, const exprt &end) |
add axioms stating that the returned string corresponds to the input one where we removed characters between the positions start (included) and end (not included) More... | |
string_exprt | add_axioms_for_delete (const function_application_exprt &expr) |
add axioms corresponding to the StringBuilder.delete java function More... | |
string_exprt | add_axioms_for_delete_char_at (const function_application_exprt &expr) |
add axioms corresponding to the StringBuilder.deleteCharAt java function More... | |
string_exprt | add_axioms_for_insert (const string_exprt &s1, const string_exprt &s2, const exprt &offset) |
add axioms stating that the result correspond to the first string where we inserted the second one at possition offset More... | |
string_exprt | add_axioms_for_insert (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.insert(String) java function More... | |
string_exprt | add_axioms_for_insert_int (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.insert(I) java function More... | |
string_exprt | add_axioms_for_insert_long (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.insert(J) java function More... | |
string_exprt | add_axioms_for_insert_bool (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.insert(Z) java function More... | |
string_exprt | add_axioms_for_insert_char (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.insert(C) java function More... | |
string_exprt | add_axioms_for_insert_double (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.insert(D) java function More... | |
string_exprt | add_axioms_for_insert_float (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.insert(F) java function More... | |
string_exprt | add_axioms_for_insert_char_array (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.insert:(I[CII) and StringBuilder.insert:(I[C) java functions More... | |
string_exprt | add_axioms_from_literal (const function_application_exprt &f) |
add axioms to say that the returned string expression is equal to the string literal More... | |
string_exprt | add_axioms_from_int (const function_application_exprt &f) |
add axioms corresponding to the String.valueOf(I) java function More... | |
string_exprt | add_axioms_from_int (const exprt &i, size_t max_size, const refined_string_typet &ref_type) |
add axioms to say the string corresponds to the result of String.valueOf(I) or String.valueOf(J) java functions applied on the integer expression More... | |
string_exprt | add_axioms_from_int_hex (const exprt &i, const refined_string_typet &ref_type) |
add axioms stating that the returned string corresponds to the integer argument written in hexadecimal More... | |
string_exprt | add_axioms_from_int_hex (const function_application_exprt &f) |
add axioms corresponding to the Integer.toHexString(I) java function More... | |
string_exprt | add_axioms_from_long (const function_application_exprt &f) |
add axioms corresponding to the String.valueOf(J) java function More... | |
string_exprt | add_axioms_from_long (const exprt &i, size_t max_size) |
string_exprt | add_axioms_from_bool (const function_application_exprt &f) |
add axioms corresponding to the String.valueOf(Z) java function More... | |
string_exprt | add_axioms_from_bool (const exprt &i, const refined_string_typet &ref_type) |
add axioms stating that the returned string equals "true" when the Boolean expression is true and "false" when it is false More... | |
string_exprt | add_axioms_from_char (const function_application_exprt &f) |
add axioms corresponding to the String.valueOf(C) java function More... | |
string_exprt | add_axioms_from_char (const exprt &i, const refined_string_typet &ref_type) |
add axioms stating that the returned string has length 1 and the character it contains correspond to the input expression More... | |
string_exprt | add_axioms_from_char_array (const function_application_exprt &f) |
add axioms corresponding to the String. More... | |
string_exprt | add_axioms_from_char_array (const exprt &length, const exprt &data, const exprt &offset, const exprt &count) |
add axioms stating that the content of the returned string equals to the content of the array argument, starting at offset and with count characters More... | |
exprt | add_axioms_for_index_of (const string_exprt &str, const exprt &c, const exprt &from_index) |
add axioms that the returned value is either -1 or greater than from_index and the character at that position equals to c More... | |
exprt | add_axioms_for_index_of_string (const string_exprt &str, const string_exprt &substring, const exprt &from_index) |
add axioms stating that the returned value is either -1 or greater than from_index and the string beggining there has prefix substring More... | |
exprt | add_axioms_for_index_of (const function_application_exprt &f) |
add axioms corresponding to the String.indexOf:(C), String.indexOf:(CI), String.indexOf:(String), and String.indexOf:(String,I) java functions More... | |
exprt | add_axioms_for_last_index_of_string (const string_exprt &str, const string_exprt &substring, const exprt &from_index) |
exprt | add_axioms_for_last_index_of (const string_exprt &str, const exprt &c, const exprt &from_index) |
exprt | add_axioms_for_last_index_of (const function_application_exprt &f) |
add axioms corresponding to the String.lastIndexOf:(C), String.lastIndexOf:(CI), String.lastIndexOf:(String), and String.lastIndexOf:(String,I) java functions More... | |
string_exprt | add_axioms_from_float (const function_application_exprt &f) |
add axioms corresponding to the String.valueOf(F) java function More... | |
string_exprt | add_axioms_from_float (const exprt &f, bool double_precision=false) |
add axioms corresponding to the String.valueOf(F) java function Warning: we currently only have partial specification More... | |
string_exprt | add_axioms_from_double (const function_application_exprt &f) |
add axioms corresponding to the String.valueOf(D) java function More... | |
string_exprt | add_axioms_for_replace (const function_application_exprt &f) |
add axioms corresponding to the String.replace java function More... | |
string_exprt | add_axioms_for_set_length (const function_application_exprt &f) |
add axioms to say that the returned string expression has length given by the second argument and whose characters are equal to those of the first argument for the positions which are defined in both strings More... | |
string_exprt | add_axioms_for_substring (const string_exprt &str, const exprt &start, const exprt &end) |
add axioms stating that the returned string expression is equal to the input one starting at start and ending before end More... | |
string_exprt | add_axioms_for_substring (const function_application_exprt &expr) |
add axioms corresponding to the String.substring java function Warning: the specification may not be correct for the case where the string is shorter than the end index More... | |
string_exprt | add_axioms_for_to_lower_case (const function_application_exprt &expr) |
add axioms corresponding to the String.toLowerCase java function More... | |
string_exprt | add_axioms_for_to_upper_case (const function_application_exprt &expr) |
add axioms corresponding to the String.toUpperCase java function More... | |
string_exprt | add_axioms_for_trim (const function_application_exprt &expr) |
add axioms corresponding to the String.trim java function More... | |
string_exprt | add_axioms_for_value_of (const function_application_exprt &f) |
add axioms corresponding to the String.valueOf([C) and String.valueOf([CII) functions More... | |
string_exprt | add_axioms_for_code_point (const exprt &code_point, const refined_string_typet &ref_type) |
string_exprt | add_axioms_for_java_char_array (const exprt &char_array) |
add axioms corresponding to the String.valueOf([C) java function More... | |
string_exprt | add_axioms_for_if (const if_exprt &expr) |
add axioms for an if expression which should return a string More... | |
exprt | add_axioms_for_char_literal (const function_application_exprt &f) |
add axioms stating that the returned value is equal to the argument More... | |
exprt | add_axioms_for_code_point_count (const function_application_exprt &f) |
add axioms giving approximate bounds on the result of the String.codePointCount java function More... | |
exprt | add_axioms_for_offset_by_code_point (const function_application_exprt &f) |
add axioms giving approximate bounds on the result of the String.offsetByCodePointCount java function. More... | |
exprt | add_axioms_for_parse_int (const function_application_exprt &f) |
add axioms corresponding to the Integer.parseInt java function More... | |
exprt | add_axioms_for_to_char_array (const function_application_exprt &f) |
add axioms corresponding to the String.toCharArray java function More... | |
exprt | add_axioms_for_compare_to (const function_application_exprt &f) |
add axioms corresponding to the String.compareTo java function More... | |
symbol_exprt | add_axioms_for_intern (const function_application_exprt &f) |
add axioms stating that the return value for two equal string should be the same More... | |
exprt | int_of_hex_char (const exprt &chr) const |
returns the value represented by the character More... | |
exprt | is_high_surrogate (const exprt &chr) const |
the output is true when the character is a high surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xD800..0xDBFF More... | |
exprt | is_low_surrogate (const exprt &chr) const |
the output is true when the character is a low surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xDC00..0xDFFF More... | |
Static Private Member Functions | |
static irep_idt | extract_java_string (const symbol_exprt &s) |
extract java string from symbol expression when they are encoded inside the symbol name More... | |
static const function_application_exprt::argumentst & | args (const function_application_exprt &expr, size_t nb) |
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 ASCII More... | |
Private Attributes | |
const std::size_t | MAX_INTEGER_LENGTH =11 |
const std::size_t | MAX_LONG_LENGTH =20 |
const std::size_t | MAX_FLOAT_LENGTH =15 |
const std::size_t | MAX_DOUBLE_LENGTH =30 |
irep_idt | mode |
std::map< string_exprt, symbol_exprt > | pool |
std::map< string_exprt, symbol_exprt > | hash |
Definition at line 27 of file string_constraint_generator.h.
|
inline |
Definition at line 34 of file string_constraint_generator.h.
|
private |
add axioms stating that the character of the string at the given position is equal to the returned value
Definition at line 486 of file string_constraint_generator_main.cpp.
References add_axioms_for_string_expr(), args(), axioms, fresh_symbol(), refined_string_typet::get_char_type(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms stating that the returned value is equal to the argument
Definition at line 456 of file string_constraint_generator_main.cpp.
References args(), function_application_exprt::arguments(), from_integer(), string_constantt::get_value(), and to_string_constant().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding stating that the result is similar to that of the StringBuilder.setCharAt java function Warning: this may be underspecified in the case wher the index exceed the length of the string
Definition at line 288 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_string_expr(), args(), axioms, string_exprt::content(), fresh_string(), string_exprt::length(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
Definition at line 28 of file string_constraint_generator_code_points.cpp.
References string_exprt::axiom_for_has_length(), axioms, fresh_string(), from_integer(), refined_string_typet::get_char_type(), irept::id(), and exprt::type().
Referenced by add_axioms_for_concat_code_point().
|
private |
add axioms corresponding to the String.codePointAt java function
Definition at line 125 of file string_constraint_generator_code_points.cpp.
References add_axioms_for_string_expr(), args(), axioms, fresh_symbol(), from_integer(), irept::id(), is_high_surrogate(), is_low_surrogate(), pair_value(), pos(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the String.codePointBefore java function
Definition at line 153 of file string_constraint_generator_code_points.cpp.
References add_axioms_for_string_expr(), args(), function_application_exprt::arguments(), axioms, fresh_symbol(), from_integer(), is_high_surrogate(), is_low_surrogate(), string_exprt::length(), pair_value(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms giving approximate bounds on the result of the String.codePointCount java function
Definition at line 185 of file string_constraint_generator_code_points.cpp.
References add_axioms_for_string_expr(), args(), axioms, fresh_symbol(), from_integer(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the String.compareTo java function
Definition at line 182 of file string_constraint_generator_comparison.cpp.
References add_axioms_for_string_expr(), args(), string_exprt::axiom_for_has_length(), string_exprt::axiom_for_has_same_length_as(), string_exprt::axiom_for_is_longer_than(), string_exprt::axiom_for_is_shorter_than(), string_exprt::axiom_for_is_strictly_longer_than(), axioms, fresh_exist_index(), fresh_symbol(), fresh_univ_index(), from_integer(), irept::id(), index_type(), string_exprt::length(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms to say that the returned string expression is equal to the concatenation of the two string expressions given as input
Definition at line 20 of file string_constraint_generator_concat.cpp.
References string_exprt::axiom_for_is_shorter_than(), axioms, fresh_string(), fresh_univ_index(), string_exprt::length(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_concat(), add_axioms_for_concat_bool(), add_axioms_for_concat_char(), add_axioms_for_concat_code_point(), add_axioms_for_concat_double(), add_axioms_for_concat_float(), add_axioms_for_concat_int(), add_axioms_for_concat_long(), add_axioms_for_delete(), add_axioms_for_function_application(), add_axioms_for_insert(), and add_axioms_from_float().
|
private |
add axioms to say that the returned string expression is equal to the concatenation of the two string arguments of the function application
Definition at line 55 of file string_constraint_generator_concat.cpp.
References add_axioms_for_concat(), add_axioms_for_string_expr(), args(), and function_application_exprt::arguments().
|
private |
add axioms corresponding to the StringBuilder.append(Z) java function
Definition at line 97 of file string_constraint_generator_concat.cpp.
References add_axioms_for_concat(), add_axioms_for_string_expr(), add_axioms_from_bool(), args(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the StringBuilder.append(C) java function
Definition at line 110 of file string_constraint_generator_concat.cpp.
References add_axioms_for_concat(), add_axioms_for_string_expr(), add_axioms_from_char(), args(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
Definition at line 148 of file string_constraint_generator_concat.cpp.
References add_axioms_for_code_point(), add_axioms_for_concat(), add_axioms_for_string_expr(), args(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the StringBuilder.append(D) java function
Definition at line 123 of file string_constraint_generator_concat.cpp.
References add_axioms_for_concat(), add_axioms_for_string_expr(), add_axioms_from_float(), args(), and MAX_DOUBLE_LENGTH.
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the StringBuilder.append(F) java function
Definition at line 136 of file string_constraint_generator_concat.cpp.
References add_axioms_for_concat(), add_axioms_for_string_expr(), add_axioms_from_float(), args(), and MAX_FLOAT_LENGTH.
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the StringBuilder.append(I) java function
Definition at line 71 of file string_constraint_generator_concat.cpp.
References add_axioms_for_concat(), add_axioms_for_string_expr(), add_axioms_from_int(), args(), MAX_INTEGER_LENGTH, to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
Add axioms corresponding to the StringBuilder.append(J) java function.
Definition at line 85 of file string_constraint_generator_concat.cpp.
References add_axioms_for_concat(), add_axioms_for_string_expr(), add_axioms_from_int(), args(), MAX_LONG_LENGTH, to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms saying the returned string expression should be equal to the string constant
Definition at line 36 of file string_constraint_generator_constants.cpp.
References string_exprt::axiom_for_has_length(), axioms, fresh_string(), from_integer(), refined_string_typet::get_char_type(), refined_string_typet::get_index_type(), id2string(), mode, utf8_to_utf16_little_endian(), and widen().
Referenced by add_axioms_from_bool(), add_axioms_from_float(), and add_axioms_from_literal().
|
private |
add axioms corresponding to the String.contains java function
Definition at line 163 of file string_constraint_generator_testing.cpp.
References add_axioms_for_string_expr(), args(), axiom_for_is_positive_index(), axioms, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), irept::id(), index_type(), string_exprt::length(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms to say that the returned string expression is equal to the argument of the function application
Definition at line 338 of file string_constraint_generator_main.cpp.
References add_axioms_for_string_expr(), args(), axioms, fresh_string(), fresh_univ_index(), refined_string_typet::get_index_type(), string_exprt::length(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms stating that the returned string corresponds to the input one where we removed characters between the positions start (included) and end (not included)
Definition at line 361 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_concat(), add_axioms_for_substring(), from_integer(), string_exprt::length(), and exprt::type().
Referenced by add_axioms_for_delete(), add_axioms_for_delete_char_at(), and add_axioms_for_function_application().
|
private |
add axioms corresponding to the StringBuilder.delete java function
Definition at line 376 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_delete(), add_axioms_for_string_expr(), and args().
|
private |
add axioms corresponding to the StringBuilder.deleteCharAt java function
Definition at line 347 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_delete(), add_axioms_for_string_expr(), args(), from_integer(), string_exprt::length(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms to say that the returned string expression is empty
Definition at line 69 of file string_constraint_generator_constants.cpp.
References function_application_exprt::arguments(), axioms, fresh_string(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms stating that the result is true exactly when the strings represented by the arguments are equal
Definition at line 20 of file string_constraint_generator_comparison.cpp.
References add_axioms_for_string_expr(), args(), axioms, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), irept::id(), index_type(), string_exprt::length(), exprt::type(), and witness.
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the String.equalsIgnoreCase java function
Definition at line 90 of file string_constraint_generator_comparison.cpp.
References add_axioms_for_string_expr(), args(), axioms, char_type(), character_equals_ignore_case(), constant_char(), fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), irept::id(), index_type(), string_exprt::length(), to_refined_string_type(), exprt::type(), and witness.
Referenced by add_axioms_for_function_application().
exprt string_constraint_generatort::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.
Axioms are then added to enforce that the result corresponds to the function application.
Definition at line 197 of file string_constraint_generator_main.cpp.
References add_axioms_for_char_at(), add_axioms_for_char_literal(), add_axioms_for_char_set(), add_axioms_for_code_point_at(), add_axioms_for_code_point_before(), add_axioms_for_code_point_count(), add_axioms_for_compare_to(), add_axioms_for_concat(), add_axioms_for_concat_bool(), add_axioms_for_concat_char(), add_axioms_for_concat_code_point(), add_axioms_for_concat_double(), add_axioms_for_concat_float(), add_axioms_for_concat_int(), add_axioms_for_concat_long(), add_axioms_for_contains(), add_axioms_for_copy(), add_axioms_for_delete(), add_axioms_for_delete_char_at(), add_axioms_for_empty_string(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_hash_code(), add_axioms_for_index_of(), add_axioms_for_insert(), add_axioms_for_insert_bool(), add_axioms_for_insert_char(), add_axioms_for_insert_char_array(), add_axioms_for_insert_double(), add_axioms_for_insert_float(), add_axioms_for_insert_int(), add_axioms_for_insert_long(), add_axioms_for_is_empty(), add_axioms_for_is_prefix(), add_axioms_for_is_suffix(), add_axioms_for_last_index_of(), add_axioms_for_length(), add_axioms_for_offset_by_code_point(), add_axioms_for_parse_int(), add_axioms_for_replace(), add_axioms_for_set_length(), add_axioms_for_substring(), add_axioms_for_to_char_array(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), add_axioms_for_trim(), add_axioms_for_value_of(), add_axioms_from_bool(), add_axioms_from_char(), add_axioms_from_char_array(), add_axioms_from_double(), add_axioms_from_float(), add_axioms_from_int(), add_axioms_from_int_hex(), add_axioms_from_literal(), add_axioms_from_long(), function_application_exprt::function(), symbol_exprt::get_identifier(), ssa_exprt::get_object_name(), irept::id(), id2string(), is_ssa_expr(), to_ssa_expr(), and to_symbol_expr().
Referenced by add_axioms_for_string_expr(), assign_to_symbol(), and string_refinementt::convert_function_application().
|
private |
add axioms stating that if two strings are equal then their hash codes are equals
Definition at line 143 of file string_constraint_generator_comparison.cpp.
References add_axioms_for_string_expr(), args(), axiom_for_is_positive_index(), axioms, fresh_exist_index(), fresh_symbol(), hash, index_type(), string_exprt::length(), symbol_to_string, and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms for an if expression which should return a string
Definition at line 149 of file string_constraint_generator_main.cpp.
References add_axioms_for_string_expr(), string_exprt::axiom_for_has_same_length_as(), axioms, if_exprt::cond(), if_exprt::false_case(), fresh_string(), fresh_univ_index(), index_type(), refined_string_typet::is_unrefined_string_type(), string_exprt::length(), to_refined_string_type(), if_exprt::true_case(), and exprt::type().
Referenced by add_axioms_for_string_expr().
|
private |
add axioms that the returned value is either -1 or greater than from_index and the character at that position equals to c
Definition at line 21 of file string_constraint_generator_indexof.cpp.
References axioms, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), index_type(), string_exprt::length(), and exprt::type().
Referenced by add_axioms_for_function_application(), and add_axioms_for_index_of().
|
private |
add axioms corresponding to the String.indexOf:(C), String.indexOf:(CI), String.indexOf:(String), and String.indexOf:(String,I) java functions
Definition at line 149 of file string_constraint_generator_indexof.cpp.
References add_axioms_for_index_of(), add_axioms_for_index_of_string(), add_axioms_for_string_expr(), args(), function_application_exprt::arguments(), from_integer(), refined_string_typet::get_char_type(), refined_string_typet::get_index_type(), refined_string_typet::is_java_string_pointer_type(), to_refined_string_type(), and exprt::type().
|
private |
add axioms stating that the returned value is either -1 or greater than from_index and the string beggining there has prefix substring
Definition at line 72 of file string_constraint_generator_indexof.cpp.
References string_exprt::axiom_for_is_longer_than(), axioms, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), index_type(), string_exprt::length(), and exprt::type().
Referenced by add_axioms_for_index_of().
|
private |
add axioms stating that the result correspond to the first string where we inserted the second one at possition offset
Definition at line 18 of file string_constraint_generator_insert.cpp.
References add_axioms_for_concat(), add_axioms_for_substring(), from_integer(), string_exprt::length(), and exprt::type().
Referenced by add_axioms_for_function_application(), add_axioms_for_insert(), add_axioms_for_insert_bool(), add_axioms_for_insert_char(), add_axioms_for_insert_char_array(), add_axioms_for_insert_double(), add_axioms_for_insert_float(), add_axioms_for_insert_int(), and add_axioms_for_insert_long().
|
private |
add axioms corresponding to the StringBuilder.insert(String) java function
Definition at line 33 of file string_constraint_generator_insert.cpp.
References add_axioms_for_insert(), add_axioms_for_string_expr(), and args().
|
private |
add axioms corresponding to the StringBuilder.insert(Z) java function
Definition at line 75 of file string_constraint_generator_insert.cpp.
References add_axioms_for_insert(), add_axioms_for_string_expr(), add_axioms_from_bool(), args(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the StringBuilder.insert(C) java function
Definition at line 89 of file string_constraint_generator_insert.cpp.
References add_axioms_for_insert(), add_axioms_for_string_expr(), add_axioms_from_char(), args(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the StringBuilder.insert:(I[CII) and StringBuilder.insert:(I[C) java functions
Definition at line 131 of file string_constraint_generator_insert.cpp.
References add_axioms_for_insert(), add_axioms_for_string_expr(), add_axioms_from_char_array(), function_application_exprt::arguments(), and from_integer().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the StringBuilder.insert(D) java function
Definition at line 103 of file string_constraint_generator_insert.cpp.
References add_axioms_for_insert(), add_axioms_for_string_expr(), add_axioms_from_float(), and args().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the StringBuilder.insert(F) java function
Definition at line 116 of file string_constraint_generator_insert.cpp.
References add_axioms_for_insert(), add_axioms_for_string_expr(), add_axioms_from_float(), and args().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the StringBuilder.insert(I) java function
Definition at line 46 of file string_constraint_generator_insert.cpp.
References add_axioms_for_insert(), add_axioms_for_string_expr(), add_axioms_from_int(), args(), MAX_INTEGER_LENGTH, to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the StringBuilder.insert(J) java function
Definition at line 61 of file string_constraint_generator_insert.cpp.
References add_axioms_for_insert(), add_axioms_for_string_expr(), add_axioms_from_int(), args(), MAX_LONG_LENGTH, to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms stating that the return value for two equal string should be the same
Definition at line 255 of file string_constraint_generator_comparison.cpp.
References add_axioms_for_string_expr(), args(), axiom_for_is_positive_index(), axioms, fresh_exist_index(), fresh_symbol(), index_type(), string_exprt::length(), pool, symbol_to_string, and exprt::type().
|
private |
add axioms stating that the returned value is true exactly when the argument string is empty
Definition at line 90 of file string_constraint_generator_testing.cpp.
References add_axioms_for_string_expr(), args(), string_exprt::axiom_for_has_length(), axioms, fresh_boolean(), irept::id(), is_empty(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms stating that the returned expression is true exactly when the first string is a prefix of the second one, starting at position offset
Definition at line 19 of file string_constraint_generator_testing.cpp.
References string_exprt::axiom_for_is_longer_than(), axiom_for_is_positive_index(), string_exprt::axiom_for_is_strictly_longer_than(), axioms, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), index_type(), string_exprt::length(), exprt::type(), and witness.
Referenced by add_axioms_for_function_application(), and add_axioms_for_is_prefix().
|
private |
add axioms corresponding to the String.isPrefix java function
Definition at line 71 of file string_constraint_generator_testing.cpp.
References add_axioms_for_is_prefix(), add_axioms_for_string_expr(), args(), function_application_exprt::arguments(), from_integer(), irept::id(), and exprt::type().
|
private |
add axioms corresponding to the String.isSuffix java function
Definition at line 112 of file string_constraint_generator_testing.cpp.
References add_axioms_for_string_expr(), args(), function_application_exprt::arguments(), string_exprt::axiom_for_is_longer_than(), axiom_for_is_positive_index(), axioms, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), irept::id(), index_type(), string_exprt::length(), exprt::type(), and witness.
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the String.valueOf([C) java function
Definition at line 361 of file string_constraint_generator_main.cpp.
References string_exprt::content(), fresh_string(), java_char_type(), java_int_type(), string_exprt::length(), address_of_exprt::object(), to_address_of_expr(), and exprt::type().
Referenced by add_axioms_for_value_of().
|
private |
Definition at line 176 of file string_constraint_generator_indexof.cpp.
References axioms, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), refined_string_typet::get_index_type(), index_type(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application(), and add_axioms_for_last_index_of().
|
private |
add axioms corresponding to the String.lastIndexOf:(C), String.lastIndexOf:(CI), String.lastIndexOf:(String), and String.lastIndexOf:(String,I) java functions
Definition at line 234 of file string_constraint_generator_indexof.cpp.
References add_axioms_for_last_index_of(), add_axioms_for_last_index_of_string(), add_axioms_for_string_expr(), args(), function_application_exprt::arguments(), from_integer(), refined_string_typet::get_char_type(), refined_string_typet::get_index_type(), refined_string_typet::is_java_string_pointer_type(), string_exprt::length(), to_refined_string_type(), and exprt::type().
|
private |
Definition at line 110 of file string_constraint_generator_indexof.cpp.
References string_exprt::axiom_for_is_longer_than(), axioms, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), index_type(), string_exprt::length(), and exprt::type().
Referenced by add_axioms_for_last_index_of().
|
private |
add axioms corresponding to the String.length java function
Definition at line 377 of file string_constraint_generator_main.cpp.
References add_axioms_for_string_expr(), args(), and string_exprt::length().
Referenced by add_axioms_for_function_application().
|
private |
add axioms giving approximate bounds on the result of the String.offsetByCodePointCount java function.
We approximate the result by saying the result is between index + offset and index + 2 * offset
Definition at line 207 of file string_constraint_generator_code_points.cpp.
References add_axioms_for_string_expr(), args(), axioms, fresh_symbol(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the Integer.parseInt java function
Definition at line 473 of file string_constraint_generator_valueof.cpp.
References add_axioms_for_string_expr(), args(), string_exprt::axiom_for_has_length(), axioms, char_type(), constant_char(), fresh_symbol(), from_integer(), refined_string_typet::get_char_type(), irept::id(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the String.replace java function
Definition at line 313 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_string_expr(), args(), string_exprt::axiom_for_has_same_length_as(), axioms, fresh_string(), fresh_univ_index(), refined_string_typet::get_index_type(), string_exprt::length(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms to say that the returned string expression has length given by the second argument and whose characters are equal to those of the first argument for the positions which are defined in both strings
Definition at line 24 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_string_expr(), args(), string_exprt::axiom_for_is_shorter_than(), string_exprt::axiom_for_is_strictly_longer_than(), axioms, constant_char(), fresh_string(), fresh_univ_index(), refined_string_typet::get_char_type(), refined_string_typet::get_index_type(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
string_exprt string_constraint_generatort::add_axioms_for_string_expr | ( | const exprt & | unrefined_string | ) |
obtain a refined string expression corresponding to string variable of string function call
Definition at line 103 of file string_constraint_generator_main.cpp.
References add_axioms_for_function_application(), add_axioms_for_if(), string_exprt::axiom_for_is_longer_than(), axioms, find_or_add_string_of_symbol(), from_integer(), irept::id(), string_exprt::length(), typecast_exprt::op(), exprt::op0(), irept::pretty(), to_function_application_expr(), to_if_expr(), to_string_expr(), to_symbol_expr(), to_typecast_expr(), and exprt::type().
Referenced by add_axioms_for_char_at(), add_axioms_for_char_set(), add_axioms_for_code_point_at(), add_axioms_for_code_point_before(), add_axioms_for_code_point_count(), add_axioms_for_compare_to(), add_axioms_for_concat(), add_axioms_for_concat_bool(), add_axioms_for_concat_char(), add_axioms_for_concat_code_point(), add_axioms_for_concat_double(), add_axioms_for_concat_float(), add_axioms_for_concat_int(), add_axioms_for_concat_long(), add_axioms_for_contains(), add_axioms_for_copy(), add_axioms_for_delete(), add_axioms_for_delete_char_at(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_hash_code(), add_axioms_for_if(), add_axioms_for_index_of(), add_axioms_for_insert(), add_axioms_for_insert_bool(), add_axioms_for_insert_char(), add_axioms_for_insert_char_array(), add_axioms_for_insert_double(), add_axioms_for_insert_float(), add_axioms_for_insert_int(), add_axioms_for_insert_long(), add_axioms_for_intern(), add_axioms_for_is_empty(), add_axioms_for_is_prefix(), add_axioms_for_is_suffix(), add_axioms_for_last_index_of(), add_axioms_for_length(), add_axioms_for_offset_by_code_point(), add_axioms_for_parse_int(), add_axioms_for_replace(), add_axioms_for_set_length(), add_axioms_for_substring(), add_axioms_for_to_char_array(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), add_axioms_for_trim(), assign_to_symbol(), and set_string_symbol_equal_to_expr().
|
private |
add axioms stating that the returned string expression is equal to the input one starting at start
and ending before end
Definition at line 87 of file string_constraint_generator_transformation.cpp.
References string_exprt::axiom_for_is_longer_than(), axioms, fresh_exist_index(), fresh_string(), from_integer(), refined_string_typet::get_index_type(), index_type(), is_empty(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_delete(), add_axioms_for_function_application(), add_axioms_for_insert(), and add_axioms_for_substring().
|
private |
add axioms corresponding to the String.substring java function Warning: the specification may not be correct for the case where the string is shorter than the end index
Definition at line 61 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_string_expr(), add_axioms_for_substring(), args(), and function_application_exprt::arguments().
|
private |
add axioms corresponding to the String.toCharArray java function
Definition at line 499 of file string_constraint_generator_main.cpp.
References add_axioms_for_string_expr(), args(), and string_exprt::content().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the String.toLowerCase java function
Definition at line 197 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_string_expr(), args(), string_exprt::axiom_for_has_same_length_as(), axioms, char_type(), constant_char(), convert(), fresh_string(), fresh_univ_index(), refined_string_typet::get_char_type(), refined_string_typet::get_index_type(), index_type(), string_exprt::length(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the String.toUpperCase java function
Definition at line 241 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_string_expr(), args(), string_exprt::axiom_for_has_same_length_as(), axioms, char_type(), constant_char(), convert(), fresh_string(), fresh_univ_index(), refined_string_typet::get_char_type(), refined_string_typet::get_index_type(), index_type(), string_exprt::length(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the String.trim java function
Definition at line 124 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_string_expr(), args(), string_exprt::axiom_for_is_longer_than(), string_exprt::axiom_for_is_shorter_than(), axioms, constant_char(), fresh_exist_index(), fresh_string(), fresh_univ_index(), from_integer(), refined_string_typet::get_char_type(), refined_string_typet::get_index_type(), index_type(), string_exprt::length(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the String.valueOf([C) and String.valueOf([CII) functions
Definition at line 437 of file string_constraint_generator_valueof.cpp.
References add_axioms_for_java_char_array(), args(), function_application_exprt::arguments(), axioms, fresh_string(), fresh_univ_index(), refined_string_typet::get_index_type(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the String.valueOf(Z) java function
Definition at line 157 of file string_constraint_generator_valueof.cpp.
References args(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_concat_bool(), add_axioms_for_function_application(), and add_axioms_for_insert_bool().
|
private |
add axioms stating that the returned string equals "true" when the Boolean expression is true and "false" when it is false
Definition at line 169 of file string_constraint_generator_valueof.cpp.
References add_axioms_for_constant(), string_exprt::axiom_for_has_same_length_as(), axioms, fresh_string(), fresh_univ_index(), refined_string_typet::get_index_type(), irept::id(), index_type(), string_exprt::length(), and exprt::type().
|
private |
add axioms corresponding to the String.valueOf(C) java function
Definition at line 413 of file string_constraint_generator_valueof.cpp.
References args(), to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_concat_char(), add_axioms_for_function_application(), and add_axioms_for_insert_char().
|
private |
add axioms stating that the returned string has length 1 and the character it contains correspond to the input expression
Definition at line 424 of file string_constraint_generator_valueof.cpp.
References string_exprt::axiom_for_has_length(), axioms, and fresh_string().
|
private |
add axioms corresponding to the String.
<init>:(I[CII) and String.<init>:(I[C) java functions function application with 2 arguments and 2 additional optional
arguments | length, char array, offset and count |
Definition at line 423 of file string_constraint_generator_main.cpp.
References function_application_exprt::arguments(), and from_integer().
Referenced by add_axioms_for_function_application(), and add_axioms_for_insert_char_array().
|
private |
add axioms stating that the content of the returned string equals to the content of the array argument, starting at offset and with count
characters
Definition at line 391 of file string_constraint_generator_main.cpp.
References axioms, char_type(), fresh_string(), fresh_univ_index(), irept::id(), index_type(), string_exprt::length(), exprt::op1(), to_array_type(), and exprt::type().
|
private |
add axioms corresponding to the String.valueOf(D) java function
Definition at line 50 of file string_constraint_generator_valueof.cpp.
References add_axioms_from_float(), and args().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the String.valueOf(F) java function
Definition at line 41 of file string_constraint_generator_valueof.cpp.
References args().
Referenced by add_axioms_for_concat_double(), add_axioms_for_concat_float(), add_axioms_for_function_application(), add_axioms_for_insert_double(), add_axioms_for_insert_float(), and add_axioms_from_double().
|
private |
add axioms corresponding to the String.valueOf(F) java function Warning: we currently only have partial specification
Definition at line 62 of file string_constraint_generator_valueof.cpp.
References add_axioms_for_concat(), add_axioms_for_constant(), string_exprt::axiom_for_has_length(), string_exprt::axiom_for_has_same_length_as(), string_exprt::axiom_for_is_shorter_than(), axioms, char_type(), constant_char(), ieee_float_spect::double_precision(), fresh_string(), fresh_univ_index(), from_integer(), refined_string_typet::get_char_type(), refined_string_typet::get_index_type(), bitvector_typet::get_width(), index_type(), float_bvt::is_zero(), float_bvt::isinf(), float_bvt::isnan(), string_exprt::length(), ieee_float_spect::single_precision(), to_bitvector_type(), to_refined_string_type(), and exprt::type().
|
private |
add axioms corresponding to the String.valueOf(I) java function
Definition at line 21 of file string_constraint_generator_valueof.cpp.
References args(), MAX_INTEGER_LENGTH, to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_concat_int(), add_axioms_for_concat_long(), add_axioms_for_function_application(), add_axioms_for_insert_int(), add_axioms_for_insert_long(), and add_axioms_from_long().
|
private |
add axioms to say the string corresponds to the result of String.valueOf(I) or String.valueOf(J) java functions applied on the integer expression
Definition at line 227 of file string_constraint_generator_valueof.cpp.
References string_exprt::axiom_for_has_length(), string_exprt::axiom_for_is_shorter_than(), string_exprt::axiom_for_is_strictly_longer_than(), axioms, char_type(), constant_char(), fresh_string(), from_integer(), refined_string_typet::get_char_type(), refined_string_typet::get_index_type(), irept::id(), index_type(), is_number(), smallest_by_digit(), and exprt::type().
|
private |
add axioms stating that the returned string corresponds to the integer argument written in hexadecimal
Definition at line 347 of file string_constraint_generator_valueof.cpp.
References string_exprt::axiom_for_has_length(), string_exprt::axiom_for_is_shorter_than(), string_exprt::axiom_for_is_strictly_longer_than(), axioms, char_type(), constant_char(), fresh_string(), from_integer(), refined_string_typet::get_char_type(), refined_string_typet::get_index_type(), irept::id(), index_type(), int_of_hex_char(), is_number(), and exprt::type().
Referenced by add_axioms_for_function_application(), and add_axioms_from_int_hex().
|
private |
add axioms corresponding to the Integer.toHexString(I) java function
Definition at line 403 of file string_constraint_generator_valueof.cpp.
References add_axioms_from_int_hex(), args(), to_refined_string_type(), and exprt::type().
|
private |
add axioms to say that the returned string expression is equal to the string literal
Definition at line 84 of file string_constraint_generator_constants.cpp.
References add_axioms_for_constant(), args(), function_application_exprt::arguments(), extract_java_string(), string_constantt::get_value(), refined_string_typet::is_unrefined_string_type(), exprt::op0(), to_refined_string_type(), to_string_constant(), to_symbol_expr(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the String.valueOf(J) java function
Definition at line 31 of file string_constraint_generator_valueof.cpp.
References add_axioms_from_int(), args(), MAX_LONG_LENGTH, to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
|
inlinestaticprivate |
Definition at line 292 of file string_constraint_generator.h.
References function_application_exprt::arguments(), character_equals_ignore_case(), int_of_hex_char(), is_high_surrogate(), and is_low_surrogate().
Referenced by add_axioms_for_char_at(), add_axioms_for_char_literal(), add_axioms_for_char_set(), add_axioms_for_code_point_at(), add_axioms_for_code_point_before(), add_axioms_for_code_point_count(), add_axioms_for_compare_to(), add_axioms_for_concat(), add_axioms_for_concat_bool(), add_axioms_for_concat_char(), add_axioms_for_concat_code_point(), add_axioms_for_concat_double(), add_axioms_for_concat_float(), add_axioms_for_concat_int(), add_axioms_for_concat_long(), add_axioms_for_contains(), add_axioms_for_copy(), add_axioms_for_delete(), add_axioms_for_delete_char_at(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_hash_code(), add_axioms_for_index_of(), add_axioms_for_insert(), add_axioms_for_insert_bool(), add_axioms_for_insert_char(), add_axioms_for_insert_double(), add_axioms_for_insert_float(), add_axioms_for_insert_int(), add_axioms_for_insert_long(), add_axioms_for_intern(), add_axioms_for_is_empty(), add_axioms_for_is_prefix(), add_axioms_for_is_suffix(), add_axioms_for_last_index_of(), add_axioms_for_length(), add_axioms_for_offset_by_code_point(), add_axioms_for_parse_int(), add_axioms_for_replace(), add_axioms_for_set_length(), add_axioms_for_substring(), add_axioms_for_to_char_array(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), add_axioms_for_trim(), add_axioms_for_value_of(), add_axioms_from_bool(), add_axioms_from_char(), add_axioms_from_double(), add_axioms_from_float(), add_axioms_from_int(), add_axioms_from_int_hex(), add_axioms_from_literal(), and add_axioms_from_long().
|
inline |
Definition at line 81 of file string_constraint_generator.h.
References add_axioms_for_function_application(), add_axioms_for_string_expr(), char_type(), constant_char(), symbol_exprt::get_identifier(), and set_string_symbol_equal_to_expr().
Referenced by set_string_symbol_equal_to_expr().
expression true exactly when the index is positive
Definition at line 447 of file string_constraint_generator_main.cpp.
References from_integer(), and exprt::type().
Referenced by add_axioms_for_contains(), add_axioms_for_hash_code(), add_axioms_for_intern(), add_axioms_for_is_prefix(), and add_axioms_for_is_suffix().
|
staticprivate |
returns an expression which is true when the two given characters are equal when ignoring case for ASCII
Definition at line 66 of file string_constraint_generator_comparison.cpp.
Referenced by add_axioms_for_equals_ignore_case(), and args().
|
static |
generate constant character expression with character type.
Definition at line 36 of file string_constraint_generator_main.cpp.
References from_integer().
Referenced by add_axioms_for_equals_ignore_case(), add_axioms_for_parse_int(), add_axioms_for_set_length(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), add_axioms_for_trim(), add_axioms_from_float(), add_axioms_from_int(), add_axioms_from_int_hex(), assign_to_symbol(), int_of_hex_char(), is_high_surrogate(), and is_low_surrogate().
|
staticprivate |
extract java string from symbol expression when they are encoded inside the symbol name
Definition at line 22 of file string_constraint_generator_constants.cpp.
References symbol_exprt::get_identifier(), has_prefix(), and id2string().
Referenced by add_axioms_from_literal().
string_exprt string_constraint_generatort::find_or_add_string_of_symbol | ( | const symbol_exprt & | sym | ) |
if a symbol represent a string is present in the symbol_to_string table, returns the corresponding string, if the symbol is not yet present, creates a new string with the correct type depending on whether the mode is java or c, adds it to the table and returns it.
Definition at line 182 of file string_constraint_generator_main.cpp.
References fresh_string(), symbol_exprt::get_identifier(), symbol_to_string, to_refined_string_type(), and exprt::type().
Referenced by add_axioms_for_string_expr(), string_refinementt::convert_symbol(), and set_string_symbol_equal_to_expr().
symbol_exprt string_constraint_generatort::fresh_boolean | ( | const irep_idt & | prefix | ) |
generate a Boolean symbol which is existentially quantified
Definition at line 78 of file string_constraint_generator_main.cpp.
References boolean_symbols, and fresh_symbol().
Referenced by add_axioms_for_contains(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_index_of(), add_axioms_for_index_of_string(), add_axioms_for_is_empty(), add_axioms_for_is_prefix(), add_axioms_for_is_suffix(), add_axioms_for_last_index_of(), and add_axioms_for_last_index_of_string().
symbol_exprt string_constraint_generatort::fresh_exist_index | ( | const irep_idt & | prefix, |
const typet & | type | ||
) |
generate an index symbol which is existentially quantified
Definition at line 67 of file string_constraint_generator_main.cpp.
References fresh_symbol(), and index_symbols.
Referenced by add_axioms_for_compare_to(), add_axioms_for_contains(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_hash_code(), add_axioms_for_index_of(), add_axioms_for_index_of_string(), add_axioms_for_intern(), add_axioms_for_is_prefix(), add_axioms_for_is_suffix(), add_axioms_for_last_index_of(), add_axioms_for_last_index_of_string(), add_axioms_for_substring(), and add_axioms_for_trim().
string_exprt string_constraint_generatort::fresh_string | ( | const refined_string_typet & | type | ) |
construct a string expression whose length and content are new variables
Definition at line 89 of file string_constraint_generator_main.cpp.
References fresh_symbol(), refined_string_typet::get_content_type(), and refined_string_typet::get_index_type().
Referenced by add_axioms_for_char_set(), add_axioms_for_code_point(), add_axioms_for_concat(), add_axioms_for_constant(), add_axioms_for_copy(), add_axioms_for_empty_string(), add_axioms_for_if(), add_axioms_for_java_char_array(), add_axioms_for_replace(), add_axioms_for_set_length(), add_axioms_for_substring(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), add_axioms_for_trim(), add_axioms_for_value_of(), add_axioms_from_bool(), add_axioms_from_char(), add_axioms_from_char_array(), add_axioms_from_float(), add_axioms_from_int(), add_axioms_from_int_hex(), and find_or_add_string_of_symbol().
|
static |
generate a new symbol expression of the given type with some prefix
Definition at line 46 of file string_constraint_generator_main.cpp.
References next_symbol_id.
Referenced by add_axioms_for_char_at(), add_axioms_for_code_point_at(), add_axioms_for_code_point_before(), add_axioms_for_code_point_count(), add_axioms_for_compare_to(), add_axioms_for_hash_code(), add_axioms_for_intern(), add_axioms_for_offset_by_code_point(), add_axioms_for_parse_int(), string_refinementt::dec_solve(), fresh_boolean(), fresh_exist_index(), fresh_string(), and fresh_univ_index().
symbol_exprt string_constraint_generatort::fresh_univ_index | ( | const irep_idt & | prefix, |
const typet & | type | ||
) |
generate an index symbol to be used as an universaly quantified variable
Definition at line 58 of file string_constraint_generator_main.cpp.
References fresh_symbol().
Referenced by add_axioms_for_compare_to(), add_axioms_for_concat(), add_axioms_for_contains(), add_axioms_for_copy(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_if(), add_axioms_for_index_of(), add_axioms_for_index_of_string(), add_axioms_for_is_prefix(), add_axioms_for_is_suffix(), add_axioms_for_last_index_of(), add_axioms_for_last_index_of_string(), add_axioms_for_replace(), add_axioms_for_set_length(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), add_axioms_for_trim(), add_axioms_for_value_of(), add_axioms_from_bool(), add_axioms_from_char_array(), and add_axioms_from_float().
|
inline |
Definition at line 45 of file string_constraint_generator.h.
References mode.
Referenced by string_refinementt::boolbv_set_equality_to_true().
|
inline |
Definition at line 60 of file string_constraint_generator.h.
Referenced by string_refinementt::check_axioms(), and string_refinementt::instantiate_not_contains().
returns the value represented by the character
Definition at line 332 of file string_constraint_generator_valueof.cpp.
References constant_char(), and exprt::type().
Referenced by add_axioms_from_int_hex(), and args().
the output is true when the character is a high surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xD800..0xDBFF
Definition at line 82 of file string_constraint_generator_code_points.cpp.
References constant_char(), and exprt::type().
Referenced by add_axioms_for_code_point_at(), add_axioms_for_code_point_before(), and args().
the output is true when the character is a low surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xDC00..0xDFFF
Definition at line 95 of file string_constraint_generator_code_points.cpp.
References constant_char(), and exprt::type().
Referenced by add_axioms_for_code_point_at(), add_axioms_for_code_point_before(), and args().
|
inline |
Definition at line 38 of file string_constraint_generator.h.
References mode.
Referenced by string_refinementt::set_mode().
void string_constraint_generatort::set_string_symbol_equal_to_expr | ( | const symbol_exprt & | sym, |
const exprt & | str | ||
) |
add a correspondence to make sure the symbol points to the same string as the second argument
Definition at line 509 of file string_constraint_generator_main.cpp.
References add_axioms_for_string_expr(), assign_to_symbol(), find_or_add_string_of_symbol(), irept::id(), and to_symbol_expr().
Referenced by assign_to_symbol(), and string_refinementt::boolbv_set_equality_to_true().
std::list<exprt> string_constraint_generatort::axioms |
Definition at line 49 of file string_constraint_generator.h.
Referenced by add_axioms_for_char_at(), add_axioms_for_char_set(), add_axioms_for_code_point(), add_axioms_for_code_point_at(), add_axioms_for_code_point_before(), add_axioms_for_code_point_count(), add_axioms_for_compare_to(), add_axioms_for_concat(), add_axioms_for_constant(), add_axioms_for_contains(), add_axioms_for_copy(), add_axioms_for_empty_string(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_hash_code(), add_axioms_for_if(), add_axioms_for_index_of(), add_axioms_for_index_of_string(), add_axioms_for_intern(), add_axioms_for_is_empty(), add_axioms_for_is_prefix(), add_axioms_for_is_suffix(), add_axioms_for_last_index_of(), add_axioms_for_last_index_of_string(), add_axioms_for_offset_by_code_point(), add_axioms_for_parse_int(), add_axioms_for_replace(), add_axioms_for_set_length(), add_axioms_for_string_expr(), add_axioms_for_substring(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), add_axioms_for_trim(), add_axioms_for_value_of(), add_axioms_from_bool(), add_axioms_from_char(), add_axioms_from_char_array(), add_axioms_from_float(), add_axioms_from_int(), add_axioms_from_int_hex(), and string_refinementt::dec_solve().
std::list<symbol_exprt> string_constraint_generatort::boolean_symbols |
Definition at line 52 of file string_constraint_generator.h.
Referenced by string_refinementt::check_axioms(), and fresh_boolean().
|
private |
Definition at line 310 of file string_constraint_generator.h.
Referenced by add_axioms_for_hash_code().
std::list<symbol_exprt> string_constraint_generatort::index_symbols |
Definition at line 55 of file string_constraint_generator.h.
Referenced by string_refinementt::check_axioms(), and fresh_exist_index().
|
private |
Definition at line 104 of file string_constraint_generator.h.
Referenced by add_axioms_for_concat_double().
|
private |
Definition at line 103 of file string_constraint_generator.h.
Referenced by add_axioms_for_concat_float().
|
private |
Definition at line 101 of file string_constraint_generator.h.
Referenced by add_axioms_for_concat_int(), add_axioms_for_insert_int(), and add_axioms_from_int().
|
private |
Definition at line 102 of file string_constraint_generator.h.
Referenced by add_axioms_for_concat_long(), add_axioms_for_insert_long(), and add_axioms_from_long().
|
private |
Definition at line 289 of file string_constraint_generator.h.
Referenced by add_axioms_for_constant(), get_mode(), and set_mode().
|
static |
Definition at line 67 of file string_constraint_generator.h.
Referenced by fresh_symbol().
|
private |
Definition at line 307 of file string_constraint_generator.h.
Referenced by add_axioms_for_intern().
std::map<irep_idt, string_exprt> string_constraint_generatort::symbol_to_string |
Definition at line 77 of file string_constraint_generator.h.
Referenced by add_axioms_for_hash_code(), add_axioms_for_intern(), string_refinementt::check_axioms(), and find_or_add_string_of_symbol().
std::map<string_not_contains_constraintt, symbol_exprt> string_constraint_generatort::witness |
Definition at line 58 of file string_constraint_generator.h.
Referenced by add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_is_prefix(), add_axioms_for_is_suffix(), and string_refinementt::dec_solve().