cprover
string_constraint_generator_transformation.cpp File Reference

Generates string constraints for string transformations, that is, functions taking one string and returning another. More...

+ Include dependency graph for string_constraint_generator_transformation.cpp:

Go to the source code of this file.

Functions

std::pair< exprt, string_constraintstadd_axioms_for_set_length (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Reduce or extend a string to have the given length. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_substring (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Substring of a string between two indices. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_substring (symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
 Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start, 0)and end' = max(min(end, |str|), start')`. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_trim (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Remove leading and trailing whitespaces. More...
 
static optionalt< std::pair< exprt, exprt > > to_char_pair (exprt expr1, exprt expr2, std::function< array_string_exprt(const exprt &)> get_string_expr)
 Convert two expressions to pair of chars If both expressions are characters, return pair of them If both expressions are 1-length strings, return first character of each Otherwise return empty optional. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_replace (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Replace a character by another in a string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_delete_char_at (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 add axioms corresponding to the StringBuilder.deleteCharAt java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_delete (symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end, array_poolt &array_pool)
 Add axioms stating that res corresponds to the input str where we removed characters between the positions start (included) and end (not included). More...
 
std::pair< exprt, string_constraintstadd_axioms_for_delete (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Remove a portion of a string. More...
 

Detailed Description

Generates string constraints for string transformations, that is, functions taking one string and returning another.

Definition in file string_constraint_generator_transformation.cpp.

Function Documentation

◆ add_axioms_for_delete() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_delete ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const array_string_exprt str,
const exprt start,
const exprt end,
array_poolt array_pool 
)

Add axioms stating that res corresponds to the input str where we removed characters between the positions start (included) and end (not included).

These axioms are the same as would be generated for: concat(substring(str, 0, start), substring(end, |str|)) (see add_axioms_for_substring and add_axioms_for_concat_substr).

Parameters
fresh_symbolgenerator of fresh symbols
resarray of characters expression
strarray of characters expression
startinteger expression
endinteger expression
array_poolpool of arrays representing strings
Returns
integer expression different from zero to signal an exception

Definition at line 374 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_delete() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_delete ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

Remove a portion of a string.

Add axioms stating that res corresponds to the input str where we removed characters between the positions start (included) and end (not included). (More...)

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with arguments integer |res|, character pointer &res[0], refined_string str, integer start and integer end
array_poolpool of arrays representing strings
Returns
an integer expression whose value is different from 0 to signal an exception

Definition at line 412 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_delete_char_at()

std::pair<exprt, string_constraintst> add_axioms_for_delete_char_at ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

add axioms corresponding to the StringBuilder.deleteCharAt java function

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with two arguments, the first is a string and the second is an index
array_poolpool of arrays representing strings
Returns
an expression whose value is non null to signal an exception

Definition at line 339 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_replace()

std::pair<exprt, string_constraintst> add_axioms_for_replace ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

Replace a character by another in a string.

Add axioms ensuring that res corresponds to str where occurences of old_char have been replaced by new_char. These axioms are:

  1. \( |{\tt res}| = |{\tt str}| \)
  2. \( \forall i \in 0, |{\tt res}|) .\ {\tt str}[i]={\tt old\_char} \Rightarrow {\tt res}[i]={\tt new\_char} \land {\tt str}[i]\ne {\tt old\_char} \Rightarrow {\tt res}[i]={\tt str}[i] \) Only supports String.replace(char, char) and String.replace(String, String) for single-character strings Returns original string in every other case (that behaviour is to be fixed in the future)
    Parameters
    fresh_symbolgenerator of fresh symbols
    ffunction application with arguments integer |res|, character pointer &res[0], refined_string str, character old_char and character new_char
    array_poolpool of arrays representing strings
    Returns
    an integer expression equal to 0

Definition at line 297 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_set_length()

std::pair<exprt, string_constraintst> add_axioms_for_set_length ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

Reduce or extend a string to have the given length.

Add axioms ensuring the returned string expression res has length k and characters at position i in res are equal to the character at position i in s1 if i is smaller that the length of s1, otherwise it is the null character \u0000.

These axioms are:

  1. \( |{\tt res}|={\tt k} \)
  2. \( \forall i<|{\tt res}|.\ i < |s_1| \Rightarrow {\tt res}[i] = s_1[i] \)
  3. \( \forall i<|{\tt res}|.\ i \ge |s_1| \Rightarrow {\tt res}[i] = 0 \)
    Parameters
    fresh_symbolgenerator of fresh symbols
    ffunction application with arguments integer |res|, character pointer &res[0], refined_string s1, integer k
    array_poolpool of arrays representing strings
    Returns
    integer expression equal to 0

Definition at line 37 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_substring() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_substring ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

Substring of a string between two indices.

Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start, 0)and end' = max(min(end, |str|), start')`. (More...)

Warning
The specification may not be correct for the case where the string is shorter than the end index
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with arguments integer |res|, character pointer &res[0], refined_string str, integer start, optional integer end with default value |str|.
array_poolpool of arrays representing strings
Returns
integer expression which is different from 0 when there is an exception to signal

Definition at line 94 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_substring() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_substring ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const array_string_exprt str,
const exprt start,
const exprt end 
)

Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start, 0)and end' = max(min(end, |str|), start')`.

These axioms are:

  1. \( |{\tt res}| = end' - start' \)
  2. \( \forall i<|{\tt res}|.\ {\tt res}[i]={\tt str}[{\tt start'}+i] \)
    Parameters
    fresh_symbolgenerator of fresh symbols
    resarray of characters expression
    strarray of characters expression
    startinteger expression
    endinteger expression
    Returns
    integer expression equal to zero

Definition at line 124 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_trim()

std::pair<exprt, string_constraintst> add_axioms_for_trim ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

Remove leading and trailing whitespaces.

Add axioms ensuring res corresponds to str from which leading and trailing whitespaces have been removed. Are considered whitespaces, characters whose ascii code are smaller than that of ' ' (space).

These axioms are:

  1. \( idx + |{\tt res}| \le |{\tt str}| \) where idx represents the index of the first non-space character.
  2. \( idx \ge 0 \)
  3. \( |{\tt str}| \ge idx \)
  4. \( |{\tt res}| \ge 0 \)
  5. \( |{\tt res}| \le |{\tt str}| \) (this is necessary to prevent exceeding the biggest integer)
  6. \( \forall n<m.\ {\tt str}[n] \le \lq~\rq \)
  7. \( \forall n<|{\tt str}|-m-|{\tt res}|.\ {\tt str}[m+|{\tt res}|+n] \le \lq~\rq \)
  8. \( \forall n<|{\tt res}|.\ {\tt str}[idx+n]={\tt res}[n] \)
  9. \( (s[m]>{\tt \lq~\rq} \land s[m+|{\tt res}|-1]>{\tt \lq~\rq}) \lor m=|{\tt res}| \)
    Note
    Some of the constraints among 1, 2, 3, 4 and 5 seems to be redundant
    Parameters
    fresh_symbolgenerator of fresh symbols
    ffunction application with arguments integer |res|, character pointer &res[0], refined_string str.
    array_poolpool of arrays representing strings
    Returns
    integer expression which is different from 0 when there is an exception to signal

Definition at line 183 of file string_constraint_generator_transformation.cpp.

◆ to_char_pair()

static optionalt<std::pair<exprt, exprt> > to_char_pair ( exprt  expr1,
exprt  expr2,
std::function< array_string_exprt(const exprt &)>  get_string_expr 
)
static

Convert two expressions to pair of chars If both expressions are characters, return pair of them If both expressions are 1-length strings, return first character of each Otherwise return empty optional.

Parameters
expr1First expression
expr2Second expression
get_string_exprFunction that yields an array_string_exprt corresponding to either expr1 or expr2, for the case where they are not primitive chars.
Returns
Optional pair of two expressions

Definition at line 257 of file string_constraint_generator_transformation.cpp.