cprover
string_dependencies.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: String solver
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
12#include <unordered_set>
13#include <util/expr_iterator.h>
14#include <util/graph.h>
15#include <util/make_unique.h>
16#include <util/ssa_expr.h>
17
20static void for_each_atomic_string(
21 const array_string_exprt &e,
22 const std::function<void(const array_string_exprt &)> f);
23
26static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
27 const function_application_exprt &fun_app,
28 const exprt &return_code,
29 array_poolt &array_pool)
30{
31 const auto name = expr_checked_cast<symbol_exprt>(fun_app.function());
33
34 const irep_idt &id = name.get_identifier();
35
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);
39
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);
43
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);
47
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);
51
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);
55
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);
59
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);
63
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);
67
68 return util_make_unique<string_builtin_function_with_no_evalt>(
69 return_code, fun_app, array_pool);
70}
71
74{
75 auto entry_inserted = node_index_pool.emplace(e, string_nodes.size());
76 if(!entry_inserted.second)
77 return string_nodes[entry_inserted.first->second];
78
79 string_nodes.emplace_back(e, entry_inserted.first->second);
80 return string_nodes.back();
81}
82
83std::unique_ptr<const string_dependenciest::string_nodet>
85{
86 const auto &it = node_index_pool.find(e);
87 if(it != node_index_pool.end())
88 return util_make_unique<const string_nodet>(string_nodes.at(it->second));
89 return {};
90}
91
93 std::unique_ptr<string_builtin_functiont> builtin_function)
94{
95 builtin_function_nodes.emplace_back(
96 std::move(builtin_function), builtin_function_nodes.size());
97 return builtin_function_nodes.back();
98}
99
101 const builtin_function_nodet &node) const
102{
103 return *node.data;
104}
105
107 const array_string_exprt &e,
108 const std::function<void(const array_string_exprt &)> f)
109{
110 if(e.id() != ID_if)
111 return f(e);
112
113 const auto if_expr = to_if_expr(e);
114 for_each_atomic_string(to_array_string_expr(if_expr.true_case()), f);
115 for_each_atomic_string(to_array_string_expr(if_expr.false_case()), f);
116}
117
119 const array_string_exprt &e,
120 const builtin_function_nodet &builtin_function_node)
121{
122 for_each_atomic_string(e, [&](const array_string_exprt &s) { //NOLINT
123 string_nodet &string_node = get_node(s);
124 string_node.dependencies.push_back(builtin_function_node.index);
125 });
126}
127
129{
131 string_nodes.clear();
132 node_index_pool.clear();
133 clean_cache();
134}
135
137 string_dependenciest &dependencies,
138 const function_application_exprt &fun_app,
139 const string_dependenciest::builtin_function_nodet &builtin_function_node,
140 array_poolt &array_pool)
141{
142 PRECONDITION(fun_app.arguments()[0].type().id() != ID_pointer);
143 if(
144 fun_app.arguments().size() > 1 &&
145 fun_app.arguments()[1].type().id() == ID_pointer)
146 {
147 // Case where the result is given as a pointer argument
148 const array_string_exprt string =
149 array_pool.find(fun_app.arguments()[1], fun_app.arguments()[0]);
150 dependencies.add_dependency(string, builtin_function_node);
151 }
152
153 for(const auto &expr : fun_app.arguments())
154 {
155 std::for_each(
156 expr.depth_begin(),
157 expr.depth_end(),
158 [&](const exprt &e) { // NOLINT
159 if(is_refined_string_type(e.type()))
160 {
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);
164 }
165 });
166 }
167}
168
170 const array_string_exprt &s,
171 const std::function<exprt(const exprt &)> &get_value) const
172{
173 const auto &it = node_index_pool.find(s);
174 if(it == node_index_pool.end())
175 return {};
176
177 if(eval_string_cache[it->second])
178 return eval_string_cache[it->second];
179
180 const auto node = string_nodes[it->second];
181 const auto &f = node.result_from;
182 if(f && node.dependencies.size() == 1)
183 {
184 const auto value_opt = builtin_function_nodes[*f].data->eval(get_value);
185 eval_string_cache[it->second] = value_opt;
186 return value_opt;
187 }
188 return {};
189}
190
192{
193 eval_string_cache.resize(string_nodes.size());
194 for(auto &e : eval_string_cache)
195 e.reset();
196}
197
199 string_dependenciest &dependencies,
200 const exprt &expr,
201 array_poolt &array_pool,
202 symbol_generatort &fresh_symbol)
203{
204 const auto fun_app = expr_try_dynamic_cast<function_application_exprt>(expr);
205 if(!fun_app)
206 {
207 exprt copy = expr;
208 bool copy_differs_from_expr = false;
209 for(std::size_t i = 0; i < expr.operands().size(); ++i)
210 {
211 auto new_op =
212 add_node(dependencies, expr.operands()[i], array_pool, fresh_symbol);
213 if(new_op)
214 {
215 copy.operands()[i] = *new_op;
216 copy_differs_from_expr = true;
217 }
218 }
219 if(copy_differs_from_expr)
220 return copy;
221 return {};
222 }
223
224 const exprt return_code = fresh_symbol("string_builtin_return", expr.type());
225 auto builtin_function =
226 to_string_builtin_function(*fun_app, return_code, array_pool);
227
228 CHECK_RETURN(builtin_function != nullptr);
229 const auto &builtin_function_node =
230 dependencies.make_node(std::move(builtin_function));
231
232 if(
233 const auto &string_result =
234 dependencies.get_builtin_function(builtin_function_node).string_result())
235 {
236 dependencies.add_dependency(*string_result, builtin_function_node);
237 auto &node = dependencies.get_node(*string_result);
238 node.result_from = builtin_function_node.index;
239
240 // Ensure all atomic strings in the argument have an associated node
241 for(const auto &arg : builtin_function_node.data->string_arguments())
242 {
244 arg, [&](const array_string_exprt &atomic) { // NOLINT
245 (void)dependencies.get_node(atomic);
246 });
247 }
248 }
249 else
251 dependencies, *fun_app, builtin_function_node, array_pool);
252
253 return return_code;
254}
255
257 const builtin_function_nodet &node,
258 const std::function<void(const string_nodet &)> &f) const
259{
260 for(const auto &s : node.data->string_arguments())
261 {
262 std::vector<std::reference_wrapper<const exprt>> stack({s});
263 while(!stack.empty())
264 {
265 const auto current = stack.back();
266 stack.pop_back();
267 if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(current.get()))
268 {
269 stack.emplace_back(if_expr->true_case());
270 stack.emplace_back(if_expr->false_case());
271 }
272 else
273 {
274 const auto string_node = node_at(to_array_string_expr(current));
275 INVARIANT(
276 string_node,
277 "dependencies of the node should have been added to the graph at "
278 "node creation " +
279 current.get().pretty());
280 f(*string_node);
281 }
282 }
283 }
284}
285
287 const string_nodet &node,
288 const std::function<void(const builtin_function_nodet &)> &f) const
289{
290 for(const std::size_t &index : node.dependencies)
291 f(builtin_function_nodes[index]);
292}
293
295 const nodet &node,
296 const std::function<void(const nodet &)> &f) const
297{
298 switch(node.kind)
299 {
300 case nodet::BUILTIN:
303 [&](const string_nodet &n) { return f(nodet(n)); });
304 break;
305
306 case nodet::STRING:
308 string_nodes[node.index],
309 [&](const builtin_function_nodet &n) { return f(nodet(n)); });
310 break;
311 }
312}
313
315 const std::function<void(const nodet &)> &f) const
316{
317 for(const auto &string_node : string_nodes)
318 f(nodet(string_node));
319 for(std::size_t i = 0; i < builtin_function_nodes.size(); ++i)
321}
322
323void string_dependenciest::output_dot(std::ostream &stream) const
324{
325 const auto for_each =
326 [&](const std::function<void(const nodet &)> &f) { // NOLINT
327 for_each_node(f);
328 };
329 const auto for_each_succ =
330 [&](const nodet &n, const std::function<void(const nodet &)> &f) { // NOLINT
331 for_each_successor(n, f);
332 };
333 const auto node_to_string = [&](const nodet &n) { // NOLINT
334 std::stringstream ostream;
335 if(n.kind == nodet::BUILTIN)
336 ostream << '"' << builtin_function_nodes[n.index].data->name() << '_'
337 << n.index << '"';
338 else
339 ostream << '"' << format(string_nodes[n.index].expr) << '"';
340 return ostream.str();
341 };
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;
346}
347
350{
351 std::unordered_set<nodet, node_hash> test_dependencies;
352 for(const auto &builtin : builtin_function_nodes)
353 {
354 if(builtin.data->maybe_testing_function())
355 test_dependencies.insert(nodet(builtin));
356 }
357
359 test_dependencies,
360 [&](
361 const nodet &n,
362 const std::function<void(const nodet &)> &f) { // NOLINT
363 for_each_successor(n, f);
364 });
365
366 string_constraintst constraints;
367 for(const auto &node : builtin_function_nodes)
368 {
369 if(test_dependencies.count(nodet(node)))
370 {
371 const auto &builtin = builtin_function_nodes[node.index];
372 merge(constraints, builtin.data->constraints(generator));
373 }
374 else
375 constraints.existential.push_back(node.data->length_constraint());
376 }
377 return constraints;
378}
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:42
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
Definition: array_pool.cpp:184
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Application of (mathematical) function.
const irep_idt & id() const
Definition: irep.h:396
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.
Definition: array_pool.h:22
Forward depth-first search iterators These iterators' copy operations are expensive,...
static format_containert< T > format(const T &o)
Definition: format.h:37
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.
Definition: graph.h:573
nonstd::optional< T > optionalt
Definition: optional.h:35
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
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)
Definition: string_expr.h:95
Built-in function for String.format.
Collection of constraints of different types: existential formulas, universal formulas,...