cprover
|
Keep track of dependencies between strings. More...
#include <string_refinement_util.h>
Classes | |
class | builtin_function_nodet |
A builtin function node contains a builtin function call. More... | |
struct | node_hash |
Hash function for nodes. More... | |
class | nodet |
class | string_nodet |
A string node points to builtin_function on which it depends. More... | |
Public Member Functions | |
string_nodet & | get_node (const array_string_exprt &e) |
std::unique_ptr< const string_nodet > | node_at (const array_string_exprt &e) const |
builtin_function_nodet & | make_node (std::unique_ptr< string_builtin_functiont > &builtin_function) |
builtin_function is reset to an empty pointer after the node is created More... | |
const string_builtin_functiont & | get_builtin_function (const builtin_function_nodet &node) const |
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. More... | |
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. More... | |
void | for_each_dependency (const builtin_function_nodet &node, const std::function< void(const string_nodet &)> &f) const |
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 depends Warning: eval uses a cache which must be cleaned everytime the valuations given by get_value can change. More... | |
void | clean_cache () |
Clean the cache used by eval More... | |
void | output_dot (std::ostream &stream) const |
void | add_constraints (string_constraint_generatort &generatort) |
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding constraints. More... | |
void | clear () |
Clear the content of the dependency graph. More... | |
Private Member Functions | |
void | for_each_node (const std::function< void(const nodet &)> &f) const |
Applies f on all nodes. More... | |
void | for_each_successor (const nodet &i, const std::function< void(const nodet &)> &f) const |
Applies f on all successors of the node n. More... | |
Private Attributes | |
std::vector< builtin_function_nodet > | builtin_function_nodes |
Set of nodes representing builtin_functions. More... | |
std::vector< string_nodet > | string_nodes |
Set of nodes representing strings. More... | |
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 string_nodes . More... | |
std::vector< optionalt< exprt > > | eval_string_cache |
Keep track of dependencies between strings.
Each string points to the builtin_function calls on which it depends. Each builtin_function points to the strings on which the result depends.
Definition at line 168 of file string_refinement_util.h.
void string_dependenciest::add_constraints | ( | string_constraint_generatort & | generatort | ) |
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding constraints.
For the other builtin only add constraints on the length.
Definition at line 490 of file string_refinement_util.cpp.
References string_constraint_generatort::add_lemma(), builtin_function_nodes, irept::data, for_each_successor(), get_reachable(), and string_dependenciest::nodet::index.
Referenced by string_refinementt::dec_solve().
void string_dependenciest::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.
If it is an if_exprt
we add the sub-expressions that are not if_exprt
s instead.
Definition at line 279 of file string_refinement_util.cpp.
References string_dependenciest::string_nodet::dependencies, for_each_atomic_string(), get_node(), and string_dependenciest::builtin_function_nodet::index.
Referenced by add_dependency_to_string_subexprs(), and add_node().
void string_dependenciest::clean_cache | ( | ) |
Clean the cache used by eval
Definition at line 352 of file string_refinement_util.cpp.
References eval_string_cache, and string_nodes.
Referenced by clear(), and string_refinementt::dec_solve().
void string_dependenciest::clear | ( | void | ) |
Clear the content of the dependency graph.
Definition at line 289 of file string_refinement_util.cpp.
References builtin_function_nodes, clean_cache(), node_index_pool, and string_nodes.
optionalt< exprt > string_dependenciest::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 depends Warning: eval uses a cache which must be cleaned everytime the valuations given by get_value can change.
Definition at line 330 of file string_refinement_util.cpp.
References builtin_function_nodes, eval_string_cache, node_index_pool, and string_nodes.
Referenced by string_refinementt::get().
void string_dependenciest::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.
Definition at line 429 of file string_refinement_util.cpp.
References builtin_function_nodes, and string_dependenciest::string_nodet::dependencies.
Referenced by for_each_successor().
void string_dependenciest::for_each_dependency | ( | const builtin_function_nodet & | node, |
const std::function< void(const string_nodet &)> & | f | ||
) | const |
Definition at line 400 of file string_refinement_util.cpp.
References string_dependenciest::builtin_function_nodet::data, INVARIANT, node_at(), stack, and to_array_string_expr().
|
private |
Applies f
on all nodes.
Definition at line 457 of file string_refinement_util.cpp.
References builtin_function_nodes, and string_nodes.
Referenced by output_dot().
|
private |
Applies f
on all successors of the node n.
Definition at line 437 of file string_refinement_util.cpp.
References string_dependenciest::nodet::BUILTIN, builtin_function_nodes, for_each_dependency(), string_dependenciest::nodet::index, string_dependenciest::nodet::kind, string_dependenciest::nodet::STRING, and string_nodes.
Referenced by add_constraints(), and output_dot().
const string_builtin_functiont & string_dependenciest::get_builtin_function | ( | const builtin_function_nodet & | node | ) | const |
Definition at line 261 of file string_refinement_util.cpp.
References string_dependenciest::builtin_function_nodet::data.
Referenced by add_node().
string_dependenciest::string_nodet & string_dependenciest::get_node | ( | const array_string_exprt & | e | ) |
Definition at line 234 of file string_refinement_util.cpp.
References node_index_pool, and string_nodes.
Referenced by add_dependency(), and add_node().
string_dependenciest::builtin_function_nodet & string_dependenciest::make_node | ( | std::unique_ptr< string_builtin_functiont > & | builtin_function | ) |
builtin_function
is reset to an empty pointer after the node is created
Definition at line 253 of file string_refinement_util.cpp.
References builtin_function_nodes.
Referenced by add_node().
std::unique_ptr< const string_dependenciest::string_nodet > string_dependenciest::node_at | ( | const array_string_exprt & | e | ) | const |
Definition at line 245 of file string_refinement_util.cpp.
References node_index_pool, and string_nodes.
Referenced by for_each_dependency().
void string_dependenciest::output_dot | ( | std::ostream & | stream | ) | const |
Definition at line 466 of file string_refinement_util.cpp.
References string_dependenciest::nodet::BUILTIN, builtin_function_nodes, for_each_node(), for_each_successor(), format(), string_dependenciest::nodet::index, string_dependenciest::nodet::kind, and string_nodes.
Referenced by string_refinementt::dec_solve().
|
private |
Set of nodes representing builtin_functions.
Definition at line 270 of file string_refinement_util.h.
Referenced by add_constraints(), clear(), eval(), for_each_dependency(), for_each_node(), for_each_successor(), make_node(), and output_dot().
Definition at line 318 of file string_refinement_util.h.
Referenced by clean_cache(), and eval().
|
private |
Nodes describing dependencies of a string: values of the map correspond to indexes in the vector string_nodes
.
Definition at line 278 of file string_refinement_util.h.
Referenced by clear(), eval(), get_node(), and node_at().
|
private |
Set of nodes representing strings.
Definition at line 273 of file string_refinement_util.h.
Referenced by clean_cache(), clear(), eval(), for_each_node(), for_each_successor(), get_node(), node_at(), and output_dot().