cprover
string_constraint_generatort Class Reference

#include <string_constraint_generator.h>

Collaboration diagram for string_constraint_generatort:
[legend]

Public Member Functions

 string_constraint_generatort ()
 
void set_mode (irep_idt _mode)
 
irep_idtget_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< exprtaxioms
 
std::list< symbol_exprtboolean_symbols
 
std::list< symbol_exprtindex_symbols
 
std::map< string_not_contains_constraintt, symbol_exprtwitness
 
std::map< irep_idt, string_exprtsymbol_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::argumentstargs (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_exprtpool
 
std::map< string_exprt, symbol_exprthash
 

Detailed Description

Definition at line 27 of file string_constraint_generator.h.

Constructor & Destructor Documentation

§ string_constraint_generatort()

string_constraint_generatort::string_constraint_generatort ( )
inline

Definition at line 34 of file string_constraint_generator.h.

Member Function Documentation

§ add_axioms_for_char_at()

exprt string_constraint_generatort::add_axioms_for_char_at ( const function_application_exprt f)
private

add axioms stating that the character of the string at the given position is equal to the returned value

parameters: function application with two arguments: a string and an
integer
Returns
a character expression

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().

§ add_axioms_for_char_literal()

exprt string_constraint_generatort::add_axioms_for_char_literal ( const function_application_exprt f)
private

add axioms stating that the returned value is equal to the argument

parameters: function application with one character argument
Returns
a new character expression

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().

§ add_axioms_for_char_set()

string_exprt string_constraint_generatort::add_axioms_for_char_set ( const function_application_exprt f)
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

parameters: function application with three arguments, the first is a
string the second an index and the third a character
Returns
a new string expression

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().

§ add_axioms_for_code_point()

string_exprt string_constraint_generatort::add_axioms_for_code_point ( const exprt code_point,
const refined_string_typet ref_type 
)
private

§ add_axioms_for_code_point_at()

exprt string_constraint_generatort::add_axioms_for_code_point_at ( const function_application_exprt f)
private

add axioms corresponding to the String.codePointAt java function

parameters: function application with two arguments: a string and an
index
Returns
a integer expression corresponding to a code point

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().

§ add_axioms_for_code_point_before()

exprt string_constraint_generatort::add_axioms_for_code_point_before ( const function_application_exprt f)
private

add axioms corresponding to the String.codePointBefore java function

parameters: function application with two arguments: a string and an
index
Returns
a integer expression corresponding to a code point

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().

§ add_axioms_for_code_point_count()

exprt string_constraint_generatort::add_axioms_for_code_point_count ( const function_application_exprt f)
private

add axioms giving approximate bounds on the result of the String.codePointCount java function

parameters: function application with three arguments: a string and two
indexes
Returns
an integer expression

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().

§ add_axioms_for_compare_to()

exprt string_constraint_generatort::add_axioms_for_compare_to ( const function_application_exprt f)
private

§ add_axioms_for_concat() [1/2]

string_exprt string_constraint_generatort::add_axioms_for_concat ( const string_exprt s1,
const string_exprt s2 
)
private

§ add_axioms_for_concat() [2/2]

string_exprt string_constraint_generatort::add_axioms_for_concat ( const function_application_exprt f)
private

add axioms to say that the returned string expression is equal to the concatenation of the two string arguments of the function application

parameters: function application with two arguments which are strings
Returns
a new string expression

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().

§ add_axioms_for_concat_bool()

string_exprt string_constraint_generatort::add_axioms_for_concat_bool ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.append(Z) java function

parameters: function application two arguments: a string and a bool
Returns
a new string expression

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().

§ add_axioms_for_concat_char()

string_exprt string_constraint_generatort::add_axioms_for_concat_char ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.append(C) java function

parameters: function application with two arguments: a string and a
char
Returns
a new string expression

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().

§ add_axioms_for_concat_code_point()

string_exprt string_constraint_generatort::add_axioms_for_concat_code_point ( const function_application_exprt f)
private

Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.

parameters: function application with two arguments: a string and a
code point
Returns
a new string expression

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().

§ add_axioms_for_concat_double()

string_exprt string_constraint_generatort::add_axioms_for_concat_double ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.append(D) java function

parameters: function application with two arguments: a string and a
double
Returns
a new string expression

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().

§ add_axioms_for_concat_float()

string_exprt string_constraint_generatort::add_axioms_for_concat_float ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.append(F) java function

parameters: function application with two arguments: a string and a
float
Returns
a new string expression

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().

§ add_axioms_for_concat_int()

string_exprt string_constraint_generatort::add_axioms_for_concat_int ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.append(I) java function

parameters: function application with two arguments: a string and an
integer
Returns
a new string expression

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().

§ add_axioms_for_concat_long()

string_exprt string_constraint_generatort::add_axioms_for_concat_long ( const function_application_exprt f)
private

Add axioms corresponding to the StringBuilder.append(J) java function.

parameters: function application with two arguments: a string and a
integer of type long
Returns
a new string expression

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().

§ add_axioms_for_constant()

string_exprt string_constraint_generatort::add_axioms_for_constant ( irep_idt  sval,
const refined_string_typet ref_type 
)
private

add axioms saying the returned string expression should be equal to the string constant

parameters: a string constant
Returns
a string expression

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().

§ add_axioms_for_contains()

exprt string_constraint_generatort::add_axioms_for_contains ( const function_application_exprt f)
private

add axioms corresponding to the String.contains java function

parameters: function application with two string arguments
Returns
a Boolean expression

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().

§ add_axioms_for_copy()

string_exprt string_constraint_generatort::add_axioms_for_copy ( const function_application_exprt f)
private

add axioms to say that the returned string expression is equal to the argument of the function application

parameters: function application with one argument, which is a string
Returns
a new string expression

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().

§ add_axioms_for_delete() [1/2]

string_exprt string_constraint_generatort::add_axioms_for_delete ( const string_exprt str,
const exprt start,
const exprt end 
)
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)

parameters: a string expression, a start index and an end index
Returns
a new string expression

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().

§ add_axioms_for_delete() [2/2]

string_exprt string_constraint_generatort::add_axioms_for_delete ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.delete java function

parameters: function application with three arguments: a string
expression, a start index and an end index
Returns
a new string expression

Definition at line 376 of file string_constraint_generator_transformation.cpp.

References add_axioms_for_delete(), add_axioms_for_string_expr(), and args().

§ add_axioms_for_delete_char_at()

string_exprt string_constraint_generatort::add_axioms_for_delete_char_at ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.deleteCharAt java function

parameters: function application with two arguments, the first is a
string and the second is an index
Returns
a new string expression

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().

§ add_axioms_for_empty_string()

string_exprt string_constraint_generatort::add_axioms_for_empty_string ( const function_application_exprt f)
private

add axioms to say that the returned string expression is empty

parameters: function application without argument
Returns
string expression

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().

§ add_axioms_for_equals()

exprt string_constraint_generatort::add_axioms_for_equals ( const function_application_exprt f)
private

add axioms stating that the result is true exactly when the strings represented by the arguments are equal

parameters: function application with two string arguments
Returns
a expression of Boolean type

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().

§ add_axioms_for_equals_ignore_case()

exprt string_constraint_generatort::add_axioms_for_equals_ignore_case ( const function_application_exprt f)
private

add axioms corresponding to the String.equalsIgnoreCase java function

parameters: function application with two string arguments
Returns
a Boolean expression

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().

§ 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.

parameters: an expression containing a function application
Returns
expression corresponding to the result of 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().

§ add_axioms_for_hash_code()

exprt string_constraint_generatort::add_axioms_for_hash_code ( const function_application_exprt f)
private

add axioms stating that if two strings are equal then their hash codes are equals

parameters: function application with a string argument
Returns
a integer expression corresponding to the hash code of the string

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().

§ add_axioms_for_if()

string_exprt string_constraint_generatort::add_axioms_for_if ( const if_exprt expr)
private

§ add_axioms_for_index_of() [1/2]

exprt string_constraint_generatort::add_axioms_for_index_of ( const string_exprt str,
const exprt c,
const exprt from_index 
)
private

add axioms that the returned value is either -1 or greater than from_index and the character at that position equals to c

parameters: a string expression, a character expression and an integer
expression
Returns
a integer expression

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().

§ add_axioms_for_index_of() [2/2]

exprt string_constraint_generatort::add_axioms_for_index_of ( const function_application_exprt f)
private

add axioms corresponding to the String.indexOf:(C), String.indexOf:(CI), String.indexOf:(String), and String.indexOf:(String,I) java functions

parameters: function application with 2 or 3 arguments
Returns
a integer expression

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().

§ add_axioms_for_index_of_string()

exprt string_constraint_generatort::add_axioms_for_index_of_string ( const string_exprt str,
const string_exprt substring,
const exprt from_index 
)
private

add axioms stating that the returned value is either -1 or greater than from_index and the string beggining there has prefix substring

parameters: two string expressions and an integer expression
Returns
a integer expression

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().

§ add_axioms_for_insert() [1/2]

string_exprt string_constraint_generatort::add_axioms_for_insert ( const string_exprt s1,
const string_exprt s2,
const exprt offset 
)
private

add axioms stating that the result correspond to the first string where we inserted the second one at possition offset

parameters: two string expression and an integer offset
Returns
a new string expression

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().

§ add_axioms_for_insert() [2/2]

string_exprt string_constraint_generatort::add_axioms_for_insert ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.insert(String) java function

parameters: function application with three arguments: two strings and
an index
Returns
a new string expression

Definition at line 33 of file string_constraint_generator_insert.cpp.

References add_axioms_for_insert(), add_axioms_for_string_expr(), and args().

§ add_axioms_for_insert_bool()

string_exprt string_constraint_generatort::add_axioms_for_insert_bool ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.insert(Z) java function

parameters: function application with three arguments: a string, an
integer offset, and a Boolean
Returns
a new string expression

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().

§ add_axioms_for_insert_char()

string_exprt string_constraint_generatort::add_axioms_for_insert_char ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.insert(C) java function

parameters: function application with three arguments: a string, an
integer offset, and a character
Returns
a new string expression

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().

§ add_axioms_for_insert_char_array()

string_exprt string_constraint_generatort::add_axioms_for_insert_char_array ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.insert:(I[CII) and StringBuilder.insert:(I[C) java functions

parameters: function application with 4 arguments plus two optional
arguments: a string, an offset index, a length, data array, an offset and a count
Returns
a new string expression

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().

§ add_axioms_for_insert_double()

string_exprt string_constraint_generatort::add_axioms_for_insert_double ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.insert(D) java function

parameters: function application with three arguments: a string, an
integer offset, and a double
Returns
a new string expression

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().

§ add_axioms_for_insert_float()

string_exprt string_constraint_generatort::add_axioms_for_insert_float ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.insert(F) java function

parameters: function application with three arguments: a string, an
integer offset, and a float
Returns
a new string expression

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().

§ add_axioms_for_insert_int()

string_exprt string_constraint_generatort::add_axioms_for_insert_int ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.insert(I) java function

parameters: function application with three arguments: a string, an
integer offset, and an integer
Returns
a new string expression

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().

§ add_axioms_for_insert_long()

string_exprt string_constraint_generatort::add_axioms_for_insert_long ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.insert(J) java function

parameters: function application with three arguments: a string, an
integer offset and a long
Returns
a new string expression

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().

§ add_axioms_for_intern()

symbol_exprt string_constraint_generatort::add_axioms_for_intern ( const function_application_exprt f)
private

add axioms stating that the return value for two equal string should be the same

parameters: function application with one string argument
Returns
a string expression

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().

§ add_axioms_for_is_empty()

exprt string_constraint_generatort::add_axioms_for_is_empty ( const function_application_exprt f)
private

add axioms stating that the returned value is true exactly when the argument string is empty

parameters: function application with a string argument
Returns
a Boolean expression

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().

§ add_axioms_for_is_prefix() [1/2]

exprt string_constraint_generatort::add_axioms_for_is_prefix ( const string_exprt prefix,
const string_exprt str,
const exprt offset 
)
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

parameters: a prefix string, a string and an integer offset
Returns
a Boolean expression

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().

§ add_axioms_for_is_prefix() [2/2]

exprt string_constraint_generatort::add_axioms_for_is_prefix ( const function_application_exprt f,
bool  swap_arguments = false 
)
private

add axioms corresponding to the String.isPrefix java function

parameters: a function application with 2 or 3 arguments and a Boolean
telling whether the prefix is the second argument (when swap_arguments is true) or the first argument
Returns
a Boolean expression

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().

§ add_axioms_for_is_suffix()

exprt string_constraint_generatort::add_axioms_for_is_suffix ( const function_application_exprt f,
bool  swap_arguments = false 
)
private

add axioms corresponding to the String.isSuffix java function

parameters: a function application with 2 or 3 arguments and a Boolean
telling whether the suffix is the second argument (when swap_arguments is true) or the first argument
Returns
a Boolean expression

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().

§ add_axioms_for_java_char_array()

string_exprt string_constraint_generatort::add_axioms_for_java_char_array ( const exprt char_array)
private

add axioms corresponding to the String.valueOf([C) java function

parameters: an expression corresponding to a java object of type char
array
Returns
a new string expression

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().

§ add_axioms_for_last_index_of() [1/2]

exprt string_constraint_generatort::add_axioms_for_last_index_of ( const string_exprt str,
const exprt c,
const exprt from_index 
)
private

§ add_axioms_for_last_index_of() [2/2]

exprt string_constraint_generatort::add_axioms_for_last_index_of ( const function_application_exprt f)
private

add axioms corresponding to the String.lastIndexOf:(C), String.lastIndexOf:(CI), String.lastIndexOf:(String), and String.lastIndexOf:(String,I) java functions

parameters: function application with 2 or 3 arguments
Returns
a integer expression

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().

§ add_axioms_for_last_index_of_string()

exprt string_constraint_generatort::add_axioms_for_last_index_of_string ( const string_exprt str,
const string_exprt substring,
const exprt from_index 
)
private

§ add_axioms_for_length()

exprt string_constraint_generatort::add_axioms_for_length ( const function_application_exprt f)
private

add axioms corresponding to the String.length java function

parameters: function application with one string argument
Returns
a string expression of index type

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().

§ add_axioms_for_offset_by_code_point()

exprt string_constraint_generatort::add_axioms_for_offset_by_code_point ( const function_application_exprt f)
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

parameters: function application with three arguments: a string and two
indexes
Returns
a new string expression

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().

§ add_axioms_for_parse_int()

exprt string_constraint_generatort::add_axioms_for_parse_int ( const function_application_exprt f)
private

add axioms corresponding to the Integer.parseInt java function

parameters: function application with one string expression
Returns
an integer expression

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().

§ add_axioms_for_replace()

string_exprt string_constraint_generatort::add_axioms_for_replace ( const function_application_exprt f)
private

add axioms corresponding to the String.replace java function

parameters: function application with three arguments, the first is a
string, the second and the third are characters
Returns
a new string expression

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().

§ add_axioms_for_set_length()

string_exprt string_constraint_generatort::add_axioms_for_set_length ( const function_application_exprt f)
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

parameters: function application with two arguments, the first of which
is a string and the second an integer which should have same type has return by get_index_type()
Returns
a new string expression

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().

§ add_axioms_for_string_expr()

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

parameters: an expression of type string
Returns
a string expression that is linked to the argument through axioms that are added to the list

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().

§ add_axioms_for_substring() [1/2]

string_exprt string_constraint_generatort::add_axioms_for_substring ( const string_exprt str,
const exprt start,
const exprt end 
)
private

add axioms stating that the returned string expression is equal to the input one starting at start and ending before end

parameters: a string expression, an expression for the start index, and
an expression for the end index
Returns
a new string expression

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().

§ add_axioms_for_substring() [2/2]

string_exprt string_constraint_generatort::add_axioms_for_substring ( const function_application_exprt f)
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

parameters: function application with one string argument, one start
index argument and an optional end index argument
Returns
a new string expression

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().

§ add_axioms_for_to_char_array()

exprt string_constraint_generatort::add_axioms_for_to_char_array ( const function_application_exprt f)
private

add axioms corresponding to the String.toCharArray java function

parameters: function application with one string argument
Returns
a char array expression

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().

§ add_axioms_for_to_lower_case()

string_exprt string_constraint_generatort::add_axioms_for_to_lower_case ( const function_application_exprt expr)
private

§ add_axioms_for_to_upper_case()

string_exprt string_constraint_generatort::add_axioms_for_to_upper_case ( const function_application_exprt expr)
private

§ add_axioms_for_trim()

string_exprt string_constraint_generatort::add_axioms_for_trim ( const function_application_exprt expr)
private

§ add_axioms_for_value_of()

string_exprt string_constraint_generatort::add_axioms_for_value_of ( const function_application_exprt f)
private

add axioms corresponding to the String.valueOf([C) and String.valueOf([CII) functions

parameters: function application with one or three arguments
Returns
a new string expression

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().

§ add_axioms_from_bool() [1/2]

string_exprt string_constraint_generatort::add_axioms_from_bool ( const function_application_exprt f)
private

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

parameters: function application with on Boolean argument
Returns
a new string expression

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().

§ add_axioms_from_bool() [2/2]

string_exprt string_constraint_generatort::add_axioms_from_bool ( const exprt b,
const refined_string_typet ref_type 
)
private

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

parameters: Boolean expression
Returns
a new string expression

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().

§ add_axioms_from_char() [1/2]

string_exprt string_constraint_generatort::add_axioms_from_char ( const function_application_exprt f)
private

add axioms corresponding to the String.valueOf(C) java function

parameters: function application one char argument
Returns
a new string expression

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().

§ add_axioms_from_char() [2/2]

string_exprt string_constraint_generatort::add_axioms_from_char ( const exprt c,
const refined_string_typet ref_type 
)
private

add axioms stating that the returned string has length 1 and the character it contains correspond to the input expression

parameters: one expression of type char
Returns
a new string expression

Definition at line 424 of file string_constraint_generator_valueof.cpp.

References string_exprt::axiom_for_has_length(), axioms, and fresh_string().

§ add_axioms_from_char_array() [1/2]

string_exprt string_constraint_generatort::add_axioms_from_char_array ( const function_application_exprt f)
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

Parameters
argumentslength, char array, offset and count
Returns
a new string expression

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().

§ add_axioms_from_char_array() [2/2]

string_exprt string_constraint_generatort::add_axioms_from_char_array ( const exprt length,
const exprt data,
const exprt offset,
const exprt count 
)
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

parameters: a length expression, an array expression, a offset index,
and a count index
Returns
a new string expression

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().

§ add_axioms_from_double()

string_exprt string_constraint_generatort::add_axioms_from_double ( const function_application_exprt f)
private

add axioms corresponding to the String.valueOf(D) java function

parameters: function application with one double argument
Returns
a new string expression

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().

§ add_axioms_from_float() [1/2]

string_exprt string_constraint_generatort::add_axioms_from_float ( const function_application_exprt f)
private

add axioms corresponding to the String.valueOf(F) java function

parameters: function application with one float argument
Returns
a new string expression

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().

§ add_axioms_from_float() [2/2]

string_exprt string_constraint_generatort::add_axioms_from_float ( const exprt f,
bool  double_precision = false 
)
private

§ add_axioms_from_int() [1/2]

string_exprt string_constraint_generatort::add_axioms_from_int ( const function_application_exprt expr)
private

add axioms corresponding to the String.valueOf(I) java function

parameters: function application with one integer argument
Returns
a new string expression

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().

§ add_axioms_from_int() [2/2]

string_exprt string_constraint_generatort::add_axioms_from_int ( const exprt i,
size_t  max_size,
const refined_string_typet ref_type 
)
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

parameters: a signed integer expression, and a maximal size for the
string representation
Returns
a string 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().

§ add_axioms_from_int_hex() [1/2]

string_exprt string_constraint_generatort::add_axioms_from_int_hex ( const exprt i,
const refined_string_typet ref_type 
)
private

§ add_axioms_from_int_hex() [2/2]

string_exprt string_constraint_generatort::add_axioms_from_int_hex ( const function_application_exprt f)
private

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

parameters: function application with integer argument
Returns
a new string expression

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().

§ add_axioms_from_literal()

string_exprt string_constraint_generatort::add_axioms_from_literal ( const function_application_exprt f)
private

add axioms to say that the returned string expression is equal to the string literal

parameters: function application with an argument which is a string
literal
Returns
string expression

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().

§ add_axioms_from_long() [1/2]

string_exprt string_constraint_generatort::add_axioms_from_long ( const function_application_exprt expr)
private

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

parameters: function application with one long argument
Returns
a new string expression

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().

§ add_axioms_from_long() [2/2]

string_exprt string_constraint_generatort::add_axioms_from_long ( const exprt i,
size_t  max_size 
)
private

§ args()

static const function_application_exprt::argumentst& string_constraint_generatort::args ( const function_application_exprt expr,
size_t  nb 
)
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().

§ assign_to_symbol()

void string_constraint_generatort::assign_to_symbol ( const symbol_exprt sym,
const string_exprt expr 
)
inline

§ axiom_for_is_positive_index()

exprt string_constraint_generatort::axiom_for_is_positive_index ( const exprt x)
private

expression true exactly when the index is positive

parameters: an index expression
Returns
a Boolean expression

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().

§ character_equals_ignore_case()

exprt string_constraint_generatort::character_equals_ignore_case ( exprt  char1,
exprt  char2,
exprt  char_a,
exprt  char_A,
exprt  char_Z 
)
staticprivate

returns an expression which is true when the two given characters are equal when ignoring case for ASCII

parameters: two character expressions and constant character
expressions representing 'a', 'A' and 'Z'
Returns
a expression of Boolean type

Definition at line 66 of file string_constraint_generator_comparison.cpp.

Referenced by add_axioms_for_equals_ignore_case(), and args().

§ constant_char()

constant_exprt string_constraint_generatort::constant_char ( int  i,
const typet char_type 
)
static

generate constant character expression with character type.

parameters: integer representing a character, and a type for
characters; we do not use char type here because in some languages (for instance java) characters use more than 8 bits.
Returns
constant expression corresponding to the character.

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().

§ extract_java_string()

irep_idt string_constraint_generatort::extract_java_string ( const symbol_exprt s)
staticprivate

extract java string from symbol expression when they are encoded inside the symbol name

parameters: a symbol expression representing a java literal
Returns
a string constant

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().

§ find_or_add_string_of_symbol()

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.

parameters: a symbol expression
Returns
a string expression

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().

§ fresh_boolean()

symbol_exprt string_constraint_generatort::fresh_boolean ( const irep_idt prefix)

§ fresh_exist_index()

symbol_exprt string_constraint_generatort::fresh_exist_index ( const irep_idt prefix,
const typet type 
)

§ fresh_string()

§ fresh_symbol()

symbol_exprt string_constraint_generatort::fresh_symbol ( const irep_idt prefix,
const typet type = bool_typet() 
)
static

generate a new symbol expression of the given type with some prefix

parameters: a prefix and a type
Returns
a symbol of type tp whose name starts with "string_refinement#" followed by 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().

§ fresh_univ_index()

§ get_mode()

irep_idt& string_constraint_generatort::get_mode ( )
inline

Definition at line 45 of file string_constraint_generator.h.

References mode.

Referenced by string_refinementt::boolbv_set_equality_to_true().

§ get_witness_of()

exprt string_constraint_generatort::get_witness_of ( const string_not_contains_constraintt c,
const exprt univ_val 
) const
inline

§ int_of_hex_char()

exprt string_constraint_generatort::int_of_hex_char ( const exprt chr) const
private

returns the value represented by the character

parameters: a character expression in the following set:
0123456789abcdef
Returns
an integer expression

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().

§ is_high_surrogate()

exprt string_constraint_generatort::is_high_surrogate ( const exprt chr) const
private

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

parameters: a character expression
Returns
a Boolean expression

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().

§ is_low_surrogate()

exprt string_constraint_generatort::is_low_surrogate ( const exprt chr) const
private

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

parameters: a character expression
Returns
a Boolean expression

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().

§ set_mode()

void string_constraint_generatort::set_mode ( irep_idt  _mode)
inline

Definition at line 38 of file string_constraint_generator.h.

References mode.

Referenced by string_refinementt::set_mode().

§ set_string_symbol_equal_to_expr()

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

parameters: a symbol and a string

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().

Member Data Documentation

§ axioms

§ boolean_symbols

std::list<symbol_exprt> string_constraint_generatort::boolean_symbols

§ hash

std::map<string_exprt, symbol_exprt> string_constraint_generatort::hash
private

Definition at line 310 of file string_constraint_generator.h.

Referenced by add_axioms_for_hash_code().

§ index_symbols

std::list<symbol_exprt> string_constraint_generatort::index_symbols

§ MAX_DOUBLE_LENGTH

const std::size_t string_constraint_generatort::MAX_DOUBLE_LENGTH =30
private

Definition at line 104 of file string_constraint_generator.h.

Referenced by add_axioms_for_concat_double().

§ MAX_FLOAT_LENGTH

const std::size_t string_constraint_generatort::MAX_FLOAT_LENGTH =15
private

Definition at line 103 of file string_constraint_generator.h.

Referenced by add_axioms_for_concat_float().

§ MAX_INTEGER_LENGTH

const std::size_t string_constraint_generatort::MAX_INTEGER_LENGTH =11
private

§ MAX_LONG_LENGTH

const std::size_t string_constraint_generatort::MAX_LONG_LENGTH =20
private

§ mode

irep_idt string_constraint_generatort::mode
private

Definition at line 289 of file string_constraint_generator.h.

Referenced by add_axioms_for_constant(), get_mode(), and set_mode().

§ next_symbol_id

unsigned string_constraint_generatort::next_symbol_id =1
static

Definition at line 67 of file string_constraint_generator.h.

Referenced by fresh_symbol().

§ pool

std::map<string_exprt, symbol_exprt> string_constraint_generatort::pool
private

Definition at line 307 of file string_constraint_generator.h.

Referenced by add_axioms_for_intern().

§ symbol_to_string

std::map<irep_idt, string_exprt> string_constraint_generatort::symbol_to_string

§ witness


The documentation for this class was generated from the following files: