Go to the documentation of this file.
12 #include <unordered_set>
28 const exprt &return_code,
31 const auto name = expr_checked_cast<symbol_exprt>(fun_app.
function());
34 const irep_idt &
id = name.get_identifier();
36 if(
id == ID_cprover_string_insert_func)
37 return util_make_unique<string_insertion_builtin_functiont>(
38 return_code, fun_app.
arguments(), array_pool);
40 if(
id == ID_cprover_string_concat_func)
41 return util_make_unique<string_concatenation_builtin_functiont>(
42 return_code, fun_app.
arguments(), array_pool);
44 if(
id == ID_cprover_string_concat_char_func)
45 return util_make_unique<string_concat_char_builtin_functiont>(
46 return_code, fun_app.
arguments(), array_pool);
48 if(
id == ID_cprover_string_format_func)
49 return util_make_unique<string_format_builtin_functiont>(
50 return_code, fun_app.
arguments(), array_pool);
52 if(
id == ID_cprover_string_of_int_func)
53 return util_make_unique<string_of_int_builtin_functiont>(
54 return_code, fun_app.
arguments(), array_pool);
56 if(
id == ID_cprover_string_char_set_func)
57 return util_make_unique<string_set_char_builtin_functiont>(
58 return_code, fun_app.
arguments(), array_pool);
60 if(
id == ID_cprover_string_to_lower_case_func)
61 return util_make_unique<string_to_lower_case_builtin_functiont>(
62 return_code, fun_app.
arguments(), array_pool);
64 if(
id == ID_cprover_string_to_upper_case_func)
65 return util_make_unique<string_to_upper_case_builtin_functiont>(
66 return_code, fun_app.
arguments(), array_pool);
68 return util_make_unique<string_builtin_function_with_no_evalt>(
69 return_code, fun_app, array_pool);
76 if(!entry_inserted.second)
79 string_nodes.emplace_back(e, entry_inserted.first->second);
83 std::unique_ptr<const string_dependenciest::string_nodet>
88 return util_make_unique<const string_nodet>(
string_nodes.at(it->second));
93 std::unique_ptr<string_builtin_functiont> builtin_function)
145 fun_app.
arguments()[1].type().id() == ID_pointer)
153 for(
const auto &expr : fun_app.
arguments())
158 [&](
const exprt &e) {
159 if(is_refined_string_type(e.type()))
161 const auto string_struct = expr_checked_cast<struct_exprt>(e);
162 const auto string = of_argument(array_pool, string_struct);
163 dependencies.add_dependency(string, builtin_function_node);
171 const std::function<
exprt(
const exprt &)> &get_value)
const
181 const auto &f = node.result_from;
182 if(f && node.dependencies.size() == 1)
204 const auto fun_app = expr_try_dynamic_cast<function_application_exprt>(expr);
208 bool copy_differs_from_expr =
false;
209 for(std::size_t i = 0; i < expr.
operands().size(); ++i)
216 copy_differs_from_expr =
true;
219 if(copy_differs_from_expr)
224 const exprt return_code = fresh_symbol(
"string_builtin_return", expr.
type());
225 auto builtin_function =
229 const auto &builtin_function_node =
230 dependencies.
make_node(std::move(builtin_function));
233 const auto &string_result =
236 dependencies.
add_dependency(*string_result, builtin_function_node);
237 auto &node = dependencies.
get_node(*string_result);
241 for(
const auto &arg : builtin_function_node.data->string_arguments())
245 (void)dependencies.
get_node(atomic);
251 dependencies, *fun_app, builtin_function_node, array_pool);
258 const std::function<
void(
const string_nodet &)> &f)
const
260 for(
const auto &s : node.
data->string_arguments())
262 std::vector<std::reference_wrapper<const exprt>> stack({s});
263 while(!stack.empty())
265 const auto current = stack.back();
267 if(
const auto if_expr = expr_try_dynamic_cast<if_exprt>(current.get()))
269 stack.emplace_back(if_expr->true_case());
270 stack.emplace_back(if_expr->false_case());
277 "dependencies of the node should have been added to the graph at "
279 current.get().pretty());
296 const std::function<
void(
const nodet &)> &f)
const
315 const std::function<
void(
const nodet &)> &f)
const
318 f(
nodet(string_node));
325 const auto for_each =
326 [&](
const std::function<void(
const nodet &)> &f) {
329 const auto for_each_succ =
330 [&](
const nodet &n,
const std::function<void(
const nodet &)> &f) {
333 const auto node_to_string = [&](
const nodet &n) {
334 std::stringstream ostream;
340 return ostream.str();
342 stream <<
"digraph dependencies {\n";
343 output_dot_generic<nodet>(
344 stream, for_each, for_each_succ, node_to_string, node_to_string);
345 stream <<
'}' << std::endl;
351 std::unordered_set<nodet, node_hash> test_dependencies;
354 if(builtin.data->maybe_testing_function())
355 test_dependencies.insert(
nodet(builtin));
362 const std::function<
void(
const nodet &)> &f) {
369 if(test_dependencies.count(
nodet(node)))
372 merge(constraints, builtin.data->constraints(generator));
375 constraints.existential.push_back(node.data->length_constraint());
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Builtin functions for string concatenations.
builtin_function_nodet & make_node(std::unique_ptr< string_builtin_functiont > builtin_function)
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
#define CHECK_RETURN(CONDITION)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Correspondance between arrays and pointers string representations.
const string_builtin_functiont & get_builtin_function(const builtin_function_nodet &node) const
A string node points to builtin_function on which it depends.
Base class for all expressions.
Collection of constraints of different types: existential formulas, universal formulas,...
void for_each_successor(const nodet &i, const std::function< void(const nodet &)> &f) const
Applies f on all successors of the node n.
virtual optionalt< array_string_exprt > string_result() const
string_nodet & get_node(const array_string_exprt &e)
A builtin function node contains a builtin function call.
Keeps track of dependencies between strings.
optionalt< std::size_t > result_from
void add_dependency(const array_string_exprt &e, const builtin_function_nodet &builtin_function)
Add edge from node for e to node for builtin_function if e is a simple array expression.
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
enum string_dependenciest::nodet::@5 kind
std::vector< builtin_function_nodet > builtin_function_nodes
Set of nodes representing builtin_functions.
typet & type()
Return the type of the expression.
std::vector< string_nodet > string_nodes
Set of nodes representing strings.
Generation of fresh symbols of a given type.
bool is_ssa_expr(const exprt &expr)
optionalt< exprt > add_node(string_dependenciest &dependencies, const exprt &expr, array_poolt &array_pool, symbol_generatort &fresh_symbol)
When a sub-expression of expr is a builtin_function, add a "string_builtin_function" node to the grap...
void for_each_node(const std::function< void(const nodet &)> &f) const
Applies f on all nodes.
void clean_cache()
Clean the cache used by eval
optionalt< exprt > eval(const array_string_exprt &s, const std::function< exprt(const exprt &)> &get_value) const
Attempt to evaluate the given string from the dependencies and valuation of strings on which it depen...
#define PRECONDITION(CONDITION)
void output_dot(std::ostream &stream) const
void get_reachable(Container &set, const std::function< void(const typename Container::value_type &, const std::function< void(const typename Container::value_type &)> &)> &for_each_successor)
Add to set, nodes that are reachable from set.
Application of (mathematical) function.
std::unique_ptr< const string_nodet > node_at(const array_string_exprt &e) const
const irep_idt & id() const
NODISCARD string_constraintst add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
std::unordered_map< array_string_exprt, std::size_t, irep_hash > node_index_pool
Nodes describing dependencies of a string: values of the map correspond to indexes in the vector stri...
array_string_exprt & to_array_string_expr(exprt &expr)
nonstd::optional< T > optionalt
Base class for string functions that are built in the solver.
static void for_each_atomic_string(const array_string_exprt &e, const std::function< void(const array_string_exprt &)> f)
Applies f on all strings contained in e that are not if-expressions.
static std::unique_ptr< string_builtin_functiont > to_string_builtin_function(const function_application_exprt &fun_app, const exprt &return_code, array_poolt &array_pool)
Construct a string_builtin_functiont object from a function application.
std::vector< optionalt< exprt > > eval_string_cache
std::unique_ptr< string_builtin_functiont > data
std::vector< std::size_t > dependencies
A Template Class for Graphs.
Forward depth-first search iterators These iterators' copy operations are expensive,...
Keep track of dependencies between strings.
void for_each_dependency(const string_nodet &node, const std::function< void(const builtin_function_nodet &)> &f) const
Applies f to each node on which node depends.
void clear()
Clear the content of the dependency graph.
static void add_dependency_to_string_subexprs(string_dependenciest &dependencies, const function_application_exprt &fun_app, const string_dependenciest::builtin_function_nodet &builtin_function_node, array_poolt &array_pool)