cprover
|
#include <solvers/refinement/string_constraint_generator.h>
#include <iterator>
#include <limits>
#include <solvers/refinement/string_refinement_invariant.h>
#include <util/arith_tools.h>
#include <util/pointer_predicates.h>
#include <util/ssa_expr.h>
#include <util/string_constant.h>
#include <util/deprecate.h>
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_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. More... | |
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. 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_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 More... | |
std::pair< exprt, string_constraintst > | add_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_constraintst > | add_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_constraintst > | add_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_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. More... | |
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.
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] \).
fresh_symbol | generator of fresh symbols |
f | function application with arguments string str and integer i |
array_pool | pool of arrays representing strings |
char
Definition at line 566 of file string_constraint_generator_main.cpp.
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
f | function application with one character argument |
Definition at line 532 of file string_constraint_generator_main.cpp.
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\).
fresh_symbol | generator of fresh symbols |
f | a function application with arguments: integer |s| , character pointer &s[0] , string char_set_string , optional integers start and end |
array_pool | pool of arrays representing strings |
Definition at line 290 of file string_constraint_generator_main.cpp.
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
fresh_symbol | generator of fresh symbols |
f | function application with one argument, which is a string, or three arguments: string, integer offset and count |
array_pool | pool of arrays representing strings |
Definition at line 490 of file string_constraint_generator_main.cpp.
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
f | function application with argument string str |
array_pool | pool of arrays representing strings |
|str|
Definition at line 513 of file string_constraint_generator_main.cpp.
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 \)
fresh_symbol | generator of fresh symbols |
s | a string expression |
start | index of the first character to constrain |
end | index at which we stop adding constraints |
char_set | a 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 . |
Definition at line 254 of file string_constraint_generator_main.cpp.
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.
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.
|
static |
Definition at line 344 of file string_constraint_generator_main.cpp.
signedbv_typet get_return_code_type | ( | ) |
Definition at line 339 of file string_constraint_generator_main.cpp.
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.
pool | pool of arrays representing strings |
expr | an expression of refined string type |
Definition at line 210 of file string_constraint_generator_main.cpp.
x | an expression |
x
is positive Definition at line 524 of file string_constraint_generator_main.cpp.
Definition at line 583 of file string_constraint_generator_main.cpp.
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.
Definition at line 578 of file string_constraint_generator_main.cpp.
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.
exprt sum_overflows | ( | const plus_exprt & | sum | ) |
Definition at line 54 of file string_constraint_generator_main.cpp.
Returns a non-negative version of the argument.
expr | expression of which we want a non-negative version |
max(0, expr)
Definition at line 591 of file string_constraint_generator_main.cpp.