cprover
string_constraint_generator_main.cpp File Reference

Generates string constraints to link results from string functions with their arguments. More...

+ Include dependency graph for string_constraint_generator_main.cpp:

Go to the source code of this file.

Functions

exprt sum_overflows (const plus_exprt &sum)
 
array_string_exprt get_string_expr (array_poolt &pool, const exprt &expr)
 casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbol. More...
 
void merge (string_constraintst &result, string_constraintst other)
 Merge two sets of constraints by appending to the first one. More...
 
string_constraintst add_constraint_on_characters (symbol_generatort &fresh_symbol, const array_string_exprt &s, const exprt &start, const exprt &end, const std::string &char_set)
 Add constraint on characters of a string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_constrain_characters (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Add axioms to ensure all characters of a string belong to a given set. More...
 
const array_string_exprtchar_array_of_pointer (array_poolt &pool, const exprt &pointer, const exprt &length)
 Adds creates a new array if it does not already exists. More...
 
array_string_exprt of_argument (array_poolt &array_pool, const exprt &arg)
 Converts a struct containing a length and pointer to an array. More...
 
signedbv_typet get_return_code_type ()
 
static irep_idt get_function_name (const function_application_exprt &expr)
 
std::pair< exprt, string_constraintstadd_axioms_for_copy (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 add axioms to say that the returned string expression is equal to the argument of the function application More...
 
std::pair< exprt, string_constraintstadd_axioms_for_length (const function_application_exprt &f, array_poolt &array_pool)
 Length of a string. More...
 
exprt is_positive (const exprt &x)
 
std::pair< exprt, string_constraintstadd_axioms_for_char_literal (const function_application_exprt &f)
 add axioms stating that the returned value is equal to the argument More...
 
std::pair< exprt, string_constraintstadd_axioms_for_char_at (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Character at a given position. More...
 
exprt minimum (const exprt &a, const exprt &b)
 
exprt maximum (const exprt &a, const exprt &b)
 
exprt zero_if_negative (const exprt &expr)
 Returns a non-negative version of the argument. More...
 
std::pair< exprt, string_constraintstcombine_results (std::pair< exprt, string_constraintst > result1, std::pair< exprt, string_constraintst > result2)
 Combine the results of two add_axioms function by taking the maximum of the return codes and merging the constraints. More...
 

Detailed Description

Generates string constraints to link results from string functions with their arguments.

This is inspired by the PASS paper at HVC'13: "PASS: String Solving with Parameterized Array and Interval Automaton" by Guodong Li and Indradeep Ghosh, which gives examples of constraints for several functions.

Definition in file string_constraint_generator_main.cpp.

Function Documentation

◆ add_axioms_for_char_at()

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

Character at a given position.

Add axioms stating that the character of the string at position given by second argument is equal to the returned value. This axiom is \( char = str[i] \).

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with arguments string str and integer i
array_poolpool of arrays representing strings
Returns
character expression char

Definition at line 566 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_char_literal()

std::pair<exprt, string_constraintst> add_axioms_for_char_literal ( const function_application_exprt f)

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

Parameters
ffunction application with one character argument
Returns
a new character expression

Definition at line 532 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_constrain_characters()

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

Add axioms to ensure all characters of a string belong to a given set.

The axiom is: \(\forall i \in [start, end).\ s[i] \in char_set \), where char_set is given by the string char_set_string composed of three characters low_char, - and high_char. Character c belongs to char_set if \(low_char \le c \le high_char\).

Parameters
fresh_symbolgenerator of fresh symbols
fa function application with arguments: integer |s|, character pointer &s[0], string char_set_string, optional integers start and end
array_poolpool of arrays representing strings
Returns
integer expression whose value is zero

Definition at line 290 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_copy()

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

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

Deprecated:
should use substring instead
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with one argument, which is a string, or three arguments: string, integer offset and count
array_poolpool of arrays representing strings
Returns
a new string expression

Definition at line 490 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_length()

std::pair<exprt, string_constraintst> add_axioms_for_length ( const function_application_exprt f,
array_poolt array_pool 
)

Length of a string.

Returns the length of the string argument of the given function application

Parameters
ffunction application with argument string str
array_poolpool of arrays representing strings
Returns
expression |str|

Definition at line 513 of file string_constraint_generator_main.cpp.

◆ add_constraint_on_characters()

string_constraintst add_constraint_on_characters ( symbol_generatort fresh_symbol,
const array_string_exprt s,
const exprt start,
const exprt end,
const std::string &  char_set 
)

Add constraint on characters of a string.

This constraint is \( \forall i \in [start, end), low\_char \le s[i] \le high\_char \)

Parameters
fresh_symbolgenerator of fresh symbols
sa string expression
startindex of the first character to constrain
endindex at which we stop adding constraints
char_seta string of the form "<low_char>-<high_char>" where <low_char> and <high_char> are two characters, which represents the set of characters that are between low_char and high_char.
Returns
a string expression that is linked to the argument through axioms that are added to the list

Definition at line 254 of file string_constraint_generator_main.cpp.

◆ char_array_of_pointer()

const array_string_exprt& char_array_of_pointer ( array_poolt pool,
const exprt pointer,
const exprt length 
)

Adds creates a new array if it does not already exists.

Definition at line 325 of file string_constraint_generator_main.cpp.

◆ combine_results()

std::pair<exprt, string_constraintst> combine_results ( std::pair< exprt, string_constraintst result1,
std::pair< exprt, string_constraintst result2 
)

Combine the results of two add_axioms function by taking the maximum of the return codes and merging the constraints.

Definition at line 598 of file string_constraint_generator_main.cpp.

◆ get_function_name()

static irep_idt get_function_name ( const function_application_exprt expr)
static

Definition at line 344 of file string_constraint_generator_main.cpp.

◆ get_return_code_type()

signedbv_typet get_return_code_type ( )

Definition at line 339 of file string_constraint_generator_main.cpp.

◆ get_string_expr()

array_string_exprt get_string_expr ( array_poolt pool,
const exprt expr 
)

casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbol.

Parameters
poolpool of arrays representing strings
expran expression of refined string type
Returns
a string expression

Definition at line 210 of file string_constraint_generator_main.cpp.

◆ is_positive()

exprt is_positive ( const exprt x)
Parameters
xan expression
Returns
a Boolean expression true exactly when x is positive

Definition at line 524 of file string_constraint_generator_main.cpp.

◆ maximum()

exprt maximum ( const exprt a,
const exprt b 
)
Returns
expression representing the maximum of two expressions

Definition at line 583 of file string_constraint_generator_main.cpp.

◆ merge()

void merge ( string_constraintst result,
string_constraintst  other 
)

Merge two sets of constraints by appending to the first one.

Definition at line 225 of file string_constraint_generator_main.cpp.

◆ minimum()

exprt minimum ( const exprt a,
const exprt b 
)
Returns
expression representing the minimum of two expressions

Definition at line 578 of file string_constraint_generator_main.cpp.

◆ of_argument()

array_string_exprt of_argument ( array_poolt array_pool,
const exprt arg 
)

Converts a struct containing a length and pointer to an array.

This allows to get a string expression from arguments of a string builtion function, because string arguments in these function calls are given as a struct containing a length and pointer to an array.

Definition at line 333 of file string_constraint_generator_main.cpp.

◆ sum_overflows()

exprt sum_overflows ( const plus_exprt sum)
Returns
Boolean true when the sum of the two expressions overflows

Definition at line 54 of file string_constraint_generator_main.cpp.

◆ zero_if_negative()

exprt zero_if_negative ( const exprt expr)

Returns a non-negative version of the argument.

Parameters
exprexpression of which we want a non-negative version
Returns
max(0, expr)

Definition at line 591 of file string_constraint_generator_main.cpp.