12#include <unordered_set>
28 const exprt &return_code,
34 const irep_idt &
id = name.get_identifier();
38 return_code,
fun_app.arguments(), array_pool);
42 return_code,
fun_app.arguments(), array_pool);
46 return_code,
fun_app.arguments(), array_pool);
50 return_code,
fun_app.arguments(), array_pool);
54 return_code,
fun_app.arguments(), array_pool);
58 return_code,
fun_app.arguments(), array_pool);
62 return_code,
fun_app.arguments(), array_pool);
66 return_code,
fun_app.arguments(), array_pool);
69 return_code,
fun_app, array_pool);
83std::unique_ptr<const string_dependenciest::string_nodet>
144 fun_app.arguments().size() > 1 &&
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)
209 for(std::size_t
i = 0;
i < expr.
operands().size(); ++
i)
224 const exprt return_code = fresh_symbol(
"string_builtin_return", expr.
type());
233 const auto &string_result =
237 auto &node = dependencies.
get_node(*string_result);
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();
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
326 [&](
const std::function<
void(
const nodet &)> &f) {
334 std::stringstream ostream;
340 return ostream.str();
342 stream <<
"digraph dependencies {\n";
345 stream <<
'}' << std::endl;
354 if(
builtin.data->maybe_testing_function())
362 const std::function<
void(
const nodet &)> &f) {
372 merge(constraints,
builtin.data->constraints(generator));
375 constraints.existential.push_back(node.data->length_constraint());
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Correspondance between arrays and pointers string representations.
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
Application of (mathematical) function.
const irep_idt & id() const
Base class for string functions that are built in the solver.
virtual optionalt< array_string_exprt > string_result() const
A builtin function node contains a builtin function call.
std::unique_ptr< string_builtin_functiont > data
enum string_dependenciest::nodet::@6 kind
A string node points to builtin_function on which it depends.
optionalt< std::size_t > result_from
std::vector< std::size_t > dependencies
Keep track of dependencies between strings.
std::unique_ptr< const string_nodet > node_at(const array_string_exprt &e) const
void for_each_node(const std::function< void(const nodet &)> &f) const
Applies f on all nodes.
builtin_function_nodet & make_node(std::unique_ptr< string_builtin_functiont > builtin_function)
void output_dot(std::ostream &stream) const
void clean_cache()
Clean the cache used by eval
std::vector< builtin_function_nodet > builtin_function_nodes
Set of nodes representing builtin_functions.
void clear()
Clear the content of the dependency graph.
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...
const string_builtin_functiont & get_builtin_function(const builtin_function_nodet &node) const
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...
std::vector< string_nodet > string_nodes
Set of nodes representing 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.
std::vector< optionalt< exprt > > eval_string_cache
void for_each_successor(const nodet &i, const std::function< void(const nodet &)> &f) const
Applies f on all successors of the node n.
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.
string_nodet & get_node(const array_string_exprt &e)
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...
Generation of fresh symbols of a given type.
Forward depth-first search iterators These iterators' copy operations are expensive,...
A Template Class for Graphs.
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.
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
bool is_ssa_expr(const exprt &expr)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Builtin functions for string concatenations.
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
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...
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.
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)
Keeps track of dependencies between strings.
array_string_exprt & to_array_string_expr(exprt &expr)
Collection of constraints of different types: existential formulas, universal formulas,...