cprover
string_refinement_util.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: String solver
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #include <algorithm>
10 #include <numeric>
11 #include <functional>
12 #include <iostream>
13 #include <util/arith_tools.h>
14 #include <util/expr_util.h>
15 #include <util/ssa_expr.h>
16 #include <util/std_expr.h>
17 #include <util/expr_iterator.h>
18 #include <util/graph.h>
19 #include <util/magic.h>
20 #include <util/make_unique.h>
21 #include <unordered_set>
22 #include "string_refinement_util.h"
23 
26 static void for_each_atomic_string(
27  const array_string_exprt &e,
28  const std::function<void(const array_string_exprt &)> f);
29 
30 bool is_char_type(const typet &type)
31 {
32  return type.id() == ID_unsignedbv &&
33  to_unsignedbv_type(type).get_width() <=
35 }
36 
37 bool is_char_array_type(const typet &type, const namespacet &ns)
38 {
39  if(type.id() == ID_struct_tag)
40  return is_char_array_type(ns.follow_tag(to_struct_tag_type(type)), ns);
41  return type.id() == ID_array && is_char_type(type.subtype());
42 }
43 
44 bool is_char_pointer_type(const typet &type)
45 {
46  return type.id() == ID_pointer && is_char_type(type.subtype());
47 }
48 
49 bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
50 {
51  return has_subtype(type, is_char_pointer_type, ns);
52 }
53 
54 bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
55 {
56  return has_subexpr(
57  expr, [&](const exprt &e) { return is_char_array_type(e.type(), ns); });
58 }
59 
61 {
62  auto ref = std::ref(static_cast<const exprt &>(expr));
63  while(can_cast_expr<with_exprt>(ref.get()))
64  {
65  const auto &with_expr = expr_dynamic_cast<with_exprt>(ref.get());
66  const auto current_index = numeric_cast_v<std::size_t>(with_expr.where());
67  entries[current_index] = with_expr.new_value();
68  ref = with_expr.old();
69  }
70 
71  // This function only handles 'with' and 'array_of' expressions
72  PRECONDITION(ref.get().id() == ID_array_of);
73  default_value = expr_dynamic_cast<array_of_exprt>(ref.get()).what();
74 }
75 
77  const with_exprt &expr,
78  const exprt &index)
79 {
80  sparse_arrayt sparse_array(expr);
81 
82  return std::accumulate(
83  sparse_array.entries.begin(),
84  sparse_array.entries.end(),
85  sparse_array.default_value,
86  [&](
87  const exprt if_expr,
88  const std::pair<std::size_t, exprt> &entry) { // NOLINT
89  const exprt entry_index = from_integer(entry.first, index.type());
90  const exprt &then_expr = entry.second;
91  CHECK_RETURN(then_expr.type() == if_expr.type());
92  const equal_exprt index_equal(index, entry_index);
93  return if_exprt(index_equal, then_expr, if_expr, if_expr.type());
94  });
95 }
96 
98 {
99  return std::accumulate(
100  entries.rbegin(),
101  entries.rend(),
103  [&](
104  const exprt if_expr,
105  const std::pair<std::size_t, exprt> &entry) { // NOLINT
106  const exprt entry_index = from_integer(entry.first, index.type());
107  const exprt &then_expr = entry.second;
108  CHECK_RETURN(then_expr.type() == if_expr.type());
109  const binary_relation_exprt index_small_eq(index, ID_le, entry_index);
110  return if_exprt(index_small_eq, then_expr, if_expr, if_expr.type());
111  });
112 }
113 
115  const array_exprt &expr,
116  const exprt &extra_value)
117  : sparse_arrayt(extra_value)
118 {
119  const auto &operands = expr.operands();
120  exprt last_added = extra_value;
121  for(std::size_t i = 0; i < operands.size(); ++i)
122  {
123  const std::size_t index = operands.size() - 1 - i;
124  if(operands[index].id() != ID_unknown && operands[index] != last_added)
125  {
126  entries[index] = operands[index];
127  last_added = operands[index];
128  }
129  }
130 }
131 
133  const array_list_exprt &expr,
134  const exprt &extra_value)
135  : interval_sparse_arrayt(extra_value)
136 {
137  PRECONDITION(expr.operands().size() % 2 == 0);
138  for(std::size_t i = 0; i < expr.operands().size(); i += 2)
139  {
140  const auto index = numeric_cast<std::size_t>(expr.operands()[i]);
141  INVARIANT(
142  expr.operands()[i + 1].type() == extra_value.type(),
143  "all values in array should have the same type");
144  if(index.has_value() && expr.operands()[i + 1].id() != ID_unknown)
145  entries[*index] = expr.operands()[i + 1];
146  }
147 }
148 
150 interval_sparse_arrayt::of_expr(const exprt &expr, const exprt &extra_value)
151 {
152  if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(expr))
153  return interval_sparse_arrayt(*array_expr, extra_value);
154  if(const auto &with_expr = expr_try_dynamic_cast<with_exprt>(expr))
155  return interval_sparse_arrayt(*with_expr);
156  if(const auto &array_list = expr_try_dynamic_cast<array_list_exprt>(expr))
157  return interval_sparse_arrayt(*array_list, extra_value);
158  return {};
159 }
160 
161 exprt interval_sparse_arrayt::at(const std::size_t index) const
162 {
163  // First element at or after index
164  const auto it = entries.lower_bound(index);
165  return it != entries.end() ? it->second : default_value;
166 }
167 
169  std::size_t size,
170  const typet &index_type) const
171 {
172  const array_typet array_type(
174  array_exprt array(array_type);
175  array.operands().reserve(size);
176 
177  auto it = entries.begin();
178  for(; it != entries.end() && it->first < size; ++it)
179  array.operands().resize(it->first + 1, it->second);
180 
181  array.operands().resize(
182  size, it == entries.end() ? default_value : it->second);
183  return array;
184 }
185 
186 void equation_symbol_mappingt::add(const std::size_t i, const exprt &expr)
187 {
188  equations_containing[expr].push_back(i);
189  strings_in_equation[i].push_back(expr);
190 }
191 
192 std::vector<exprt>
194 {
195  return strings_in_equation[i];
196 }
197 
198 std::vector<std::size_t>
200 {
201  return equations_containing[expr];
202 }
203 
206 static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
207  const function_application_exprt &fun_app,
208  const exprt &return_code,
209  array_poolt &array_pool)
210 {
211  const auto name = expr_checked_cast<symbol_exprt>(fun_app.function());
212  const irep_idt &id = is_ssa_expr(name) ? to_ssa_expr(name).get_object_name()
213  : name.get_identifier();
214 
215  if(id == ID_cprover_string_insert_func)
216  return util_make_unique<string_insertion_builtin_functiont>(
217  return_code, fun_app.arguments(), array_pool);
218 
219  if(id == ID_cprover_string_concat_func)
220  return util_make_unique<string_concatenation_builtin_functiont>(
221  return_code, fun_app.arguments(), array_pool);
222 
223  if(id == ID_cprover_string_concat_char_func)
224  return util_make_unique<string_concat_char_builtin_functiont>(
225  return_code, fun_app.arguments(), array_pool);
226 
227  if(id == ID_cprover_string_of_int_func)
228  return util_make_unique<string_of_int_builtin_functiont>(
229  return_code, fun_app.arguments(), array_pool);
230 
231  if(id == ID_cprover_string_char_set_func)
232  return util_make_unique<string_set_char_builtin_functiont>(
233  return_code, fun_app.arguments(), array_pool);
234 
235  if(id == ID_cprover_string_to_lower_case_func)
236  return util_make_unique<string_to_lower_case_builtin_functiont>(
237  return_code, fun_app.arguments(), array_pool);
238 
239  if(id == ID_cprover_string_to_upper_case_func)
240  return util_make_unique<string_to_upper_case_builtin_functiont>(
241  return_code, fun_app.arguments(), array_pool);
242 
243  return util_make_unique<string_builtin_function_with_no_evalt>(
244  return_code, fun_app, array_pool);
245 }
246 
249 {
250  auto entry_inserted = node_index_pool.emplace(e, string_nodes.size());
251  if(!entry_inserted.second)
252  return string_nodes[entry_inserted.first->second];
253 
254  string_nodes.emplace_back(e, entry_inserted.first->second);
255  return string_nodes.back();
256 }
257 
258 std::unique_ptr<const string_dependenciest::string_nodet>
260 {
261  const auto &it = node_index_pool.find(e);
262  if(it != node_index_pool.end())
263  return util_make_unique<const string_nodet>(string_nodes.at(it->second));
264  return {};
265 }
266 
268  std::unique_ptr<string_builtin_functiont> &builtin_function)
269 {
270  builtin_function_nodes.emplace_back(
271  std::move(builtin_function), builtin_function_nodes.size());
272  return builtin_function_nodes.back();
273 }
274 
276  const builtin_function_nodet &node) const
277 {
278  return *node.data;
279 }
280 
282  const array_string_exprt &e,
283  const std::function<void(const array_string_exprt &)> f)
284 {
285  if(e.id() != ID_if)
286  return f(e);
287 
288  const auto if_expr = to_if_expr(e);
289  for_each_atomic_string(to_array_string_expr(if_expr.true_case()), f);
290  for_each_atomic_string(to_array_string_expr(if_expr.false_case()), f);
291 }
292 
294  const array_string_exprt &e,
295  const builtin_function_nodet &builtin_function_node)
296 {
297  for_each_atomic_string(e, [&](const array_string_exprt &s) { //NOLINT
298  string_nodet &string_node = get_node(s);
299  string_node.dependencies.push_back(builtin_function_node.index);
300  });
301 }
302 
304 {
305  builtin_function_nodes.clear();
306  string_nodes.clear();
307  node_index_pool.clear();
308  clean_cache();
309 }
310 
312  string_dependenciest &dependencies,
313  const function_application_exprt &fun_app,
314  const string_dependenciest::builtin_function_nodet &builtin_function_node,
315  array_poolt &array_pool)
316 {
317  PRECONDITION(fun_app.arguments()[0].type().id() != ID_pointer);
318  if(
319  fun_app.arguments().size() > 1 &&
320  fun_app.arguments()[1].type().id() == ID_pointer)
321  {
322  // Case where the result is given as a pointer argument
323  const array_string_exprt string =
324  array_pool.find(fun_app.arguments()[1], fun_app.arguments()[0]);
325  dependencies.add_dependency(string, builtin_function_node);
326  }
327 
328  for(const auto &expr : fun_app.arguments())
329  {
330  std::for_each(
331  expr.depth_begin(),
332  expr.depth_end(),
333  [&](const exprt &e) { // NOLINT
334  if(is_refined_string_type(e.type()))
335  {
336  const auto string_struct = expr_checked_cast<struct_exprt>(e);
337  const auto string = of_argument(array_pool, string_struct);
338  dependencies.add_dependency(string, builtin_function_node);
339  }
340  });
341  }
342 }
343 
345  const array_string_exprt &s,
346  const std::function<exprt(const exprt &)> &get_value) const
347 {
348  const auto &it = node_index_pool.find(s);
349  if(it == node_index_pool.end())
350  return {};
351 
352  if(eval_string_cache[it->second])
353  return eval_string_cache[it->second];
354 
355  const auto node = string_nodes[it->second];
356  const auto &f = node.result_from;
357  if(f && node.dependencies.size() == 1)
358  {
359  const auto value_opt = builtin_function_nodes[*f].data->eval(get_value);
360  eval_string_cache[it->second] = value_opt;
361  return value_opt;
362  }
363  return {};
364 }
365 
367 {
368  eval_string_cache.resize(string_nodes.size());
369  for(auto &e : eval_string_cache)
370  e.reset();
371 }
372 
373 bool add_node(
374  string_dependenciest &dependencies,
375  const equal_exprt &equation,
376  array_poolt &array_pool)
377 {
378  const auto fun_app =
379  expr_try_dynamic_cast<function_application_exprt>(equation.rhs());
380  if(!fun_app)
381  return false;
382 
383  auto builtin_function =
384  to_string_builtin_function(*fun_app, equation.lhs(), array_pool);
385 
386  CHECK_RETURN(builtin_function != nullptr);
387  const auto &builtin_function_node = dependencies.make_node(builtin_function);
388  // Warning: `builtin_function` has been emptied and should not be used anymore
389 
390  if(
391  const auto &string_result =
392  dependencies.get_builtin_function(builtin_function_node).string_result())
393  {
394  dependencies.add_dependency(*string_result, builtin_function_node);
395  auto &node = dependencies.get_node(*string_result);
396  node.result_from = builtin_function_node.index;
397 
398  // Ensure all atomic strings in the argument have an associated node
399  for(const auto arg : builtin_function_node.data->string_arguments())
400  {
402  arg, [&](const array_string_exprt &atomic) { // NOLINT
403  (void)dependencies.get_node(atomic);
404  });
405  }
406  }
407  else
409  dependencies, *fun_app, builtin_function_node, array_pool);
410 
411  return true;
412 }
413 
415  const builtin_function_nodet &node,
416  const std::function<void(const string_nodet &)> &f) const
417 {
418  for(const auto &s : node.data->string_arguments())
419  {
420  std::vector<std::reference_wrapper<const exprt>> stack({s});
421  while(!stack.empty())
422  {
423  const auto current = stack.back();
424  stack.pop_back();
425  if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(current.get()))
426  {
427  stack.emplace_back(if_expr->true_case());
428  stack.emplace_back(if_expr->false_case());
429  }
430  else
431  {
432  const auto string_node = node_at(to_array_string_expr(current));
433  INVARIANT(
434  string_node,
435  "dependencies of the node should have been added to the graph at node creation "
436  + current.get().pretty());
437  f(*string_node);
438  }
439  }
440  }
441 }
442 
444  const string_nodet &node,
445  const std::function<void(const builtin_function_nodet &)> &f) const
446 {
447  for(const std::size_t &index : node.dependencies)
448  f(builtin_function_nodes[index]);
449 }
450 
452  const nodet &node,
453  const std::function<void(const nodet &)> &f) const
454 {
455  switch(node.kind)
456  {
457  case nodet::BUILTIN:
460  [&](const string_nodet &n) { return f(nodet(n)); });
461  break;
462 
463  case nodet::STRING:
465  string_nodes[node.index],
466  [&](const builtin_function_nodet &n) { return f(nodet(n)); });
467  break;
468  }
469 }
470 
472  const std::function<void(const nodet &)> &f) const
473 {
474  for(const auto string_node : string_nodes)
475  f(nodet(string_node));
476  for(std::size_t i = 0; i < builtin_function_nodes.size(); ++i)
478 }
479 
480 void string_dependenciest::output_dot(std::ostream &stream) const
481 {
482  const auto for_each =
483  [&](const std::function<void(const nodet &)> &f) { // NOLINT
484  for_each_node(f);
485  };
486  const auto for_each_succ =
487  [&](const nodet &n, const std::function<void(const nodet &)> &f) { // NOLINT
488  for_each_successor(n, f);
489  };
490  const auto node_to_string = [&](const nodet &n) { // NOLINT
491  std::stringstream ostream;
492  if(n.kind == nodet::BUILTIN)
493  ostream << '"' << builtin_function_nodes[n.index].data->name() << '_'
494  << n.index << '"';
495  else
496  ostream << '"' << format(string_nodes[n.index].expr) << '"';
497  return ostream.str();
498  };
499  stream << "digraph dependencies {\n";
500  output_dot_generic<nodet>(
501  stream, for_each, for_each_succ, node_to_string, node_to_string);
502  stream << '}' << std::endl;
503 }
504 
506  string_constraint_generatort &generator)
507 {
508  std::unordered_set<nodet, node_hash> test_dependencies;
509  for(const auto &builtin : builtin_function_nodes)
510  {
511  if(builtin.data->maybe_testing_function())
512  test_dependencies.insert(nodet(builtin));
513  }
514 
516  test_dependencies,
517  [&](
518  const nodet &n,
519  const std::function<void(const nodet &)> &f) { // NOLINT
520  for_each_successor(n, f);
521  });
522 
523  for(const auto &node : builtin_function_nodes)
524  {
525  if(test_dependencies.count(nodet(node)))
526  {
527  const auto &builtin = builtin_function_nodes[node.index];
528  string_constraintst constraints = builtin.data->constraints(generator);
529  merge(generator.constraints, std::move(constraints));
530  }
531  else
532  generator.constraints.existential.push_back(
533  node.data->length_constraint());
534  }
535 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3514
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
function_application_exprt::arguments
argumentst & arguments()
Definition: std_expr.h:4506
format
static format_containert< T > format(const T &o)
Definition: format.h:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
typet::subtype
const typet & subtype() const
Definition: type.h:38
for_each_atomic_string
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.
Definition: string_refinement_util.cpp:281
has_subexpr
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:139
arith_tools.h
add_dependency_to_string_subexprs
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)
Definition: string_refinement_util.cpp:311
typet
The type of an expression, extends irept.
Definition: type.h:27
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
array_poolt
Correspondance between arrays and pointers string representations.
Definition: string_constraint_generator.h:49
sparse_arrayt
Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list...
Definition: string_refinement_util.h:67
string_dependenciest::get_builtin_function
const string_builtin_functiont & get_builtin_function(const builtin_function_nodet &node) const
Definition: string_refinement_util.cpp:275
add_node
bool add_node(string_dependenciest &dependencies, const equal_exprt &equation, array_poolt &array_pool)
When right hand side of equation is a builtin_function add a "string_builtin_function" node to the gr...
Definition: string_refinement_util.cpp:373
is_char_type
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.
Definition: string_refinement_util.cpp:30
interval_sparse_arrayt
Represents arrays by the indexes up to which the value remains the same.
Definition: string_refinement_util.h:92
string_dependenciest::string_nodet
A string node points to builtin_function on which it depends.
Definition: string_refinement_util.h:199
interval_sparse_arrayt::to_if_expression
exprt to_if_expression(const exprt &index) const
Definition: string_refinement_util.cpp:97
binary_relation_exprt::rhs
exprt & rhs()
Definition: std_expr.h:931
string_dependenciest::make_node
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
Definition: string_refinement_util.cpp:267
exprt
Base class for all expressions.
Definition: expr.h:54
ssa_exprt::get_object_name
irep_idt get_object_name() const
Definition: ssa_expr.h:46
binary_relation_exprt::lhs
exprt & lhs()
Definition: std_expr.h:921
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:108
interval_sparse_arrayt::of_expr
static optionalt< interval_sparse_arrayt > of_expr(const exprt &expr, const exprt &extra_value)
If the expression is an array_exprt or a with_exprt uses the appropriate constructor,...
Definition: string_refinement_util.cpp:150
string_dependenciest::for_each_successor
void for_each_successor(const nodet &i, const std::function< void(const nodet &)> &f) const
Applies f on all successors of the node n.
Definition: string_refinement_util.cpp:451
string_builtin_functiont::string_result
virtual optionalt< array_string_exprt > string_result() const
Definition: string_builtin_function.h:25
string_dependenciest::get_node
string_nodet & get_node(const array_string_exprt &e)
Definition: string_refinement_util.cpp:248
string_dependenciest::builtin_function_nodet
A builtin function node contains a builtin function call.
Definition: string_refinement_util.h:170
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1484
magic.h
Magic numbers used throughout the codebase.
sparse_arrayt::sparse_arrayt
sparse_arrayt(const with_exprt &expr)
Initialize a sparse array from an expression of the form array_of(x) with {i:=a} with {j:=b} ....
Definition: string_refinement_util.cpp:60
sparse_arrayt::to_if_expression
static exprt to_if_expression(const with_exprt &expr, const exprt &index)
Creates an if_expr corresponding to the result of accessing the array at the given index.
Definition: string_refinement_util.cpp:76
string_constraint_generatort
Definition: string_constraint_generator.h:120
string_dependenciest::string_nodet::result_from
optionalt< std::size_t > result_from
Definition: string_refinement_util.h:211
string_dependenciest::add_dependency
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.
Definition: string_refinement_util.cpp:293
merge
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
Definition: string_constraint_generator_main.cpp:225
sparse_arrayt::default_value
exprt default_value
Definition: string_refinement_util.h:81
string_dependenciest::nodet::kind
enum string_dependenciest::nodet::@5 kind
interval_sparse_arrayt::interval_sparse_arrayt
interval_sparse_arrayt(const with_exprt &expr)
An expression of the form array_of(x) with {i:=a} with {j:=b} is converted to an array arr where for ...
Definition: string_refinement_util.h:99
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
string_dependenciest::builtin_function_nodes
std::vector< builtin_function_nodet > builtin_function_nodes
Set of nodes representing builtin_functions.
Definition: string_refinement_util.h:268
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
interval_sparse_arrayt::at
exprt at(std::size_t index) const
Get the value at the specified index.
Definition: string_refinement_util.cpp:161
string_dependenciest::nodet
Definition: string_refinement_util.h:278
string_dependenciest::string_nodes
std::vector< string_nodet > string_nodes
Set of nodes representing strings.
Definition: string_refinement_util.h:271
to_string_builtin_function
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.
Definition: string_refinement_util.cpp:206
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:179
is_char_pointer_type
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
Definition: string_refinement_util.cpp:44
make_unique.h
string_dependenciest::for_each_node
void for_each_node(const std::function< void(const nodet &)> &f) const
Applies f on all nodes.
Definition: string_refinement_util.cpp:471
string_dependenciest::clean_cache
void clean_cache()
Clean the cache used by eval
Definition: string_refinement_util.cpp:366
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1262
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
STRING_REFINEMENT_MAX_CHAR_WIDTH
const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH
Definition: magic.h:12
namespace_baset::follow_tag
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
string_refinement_util.h
string_dependenciest::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...
Definition: string_refinement_util.cpp:344
has_subtype
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Definition: expr_util.cpp:153
string_constraint_generatort::constraints
string_constraintst constraints
Definition: string_constraint_generator.h:137
string_dependenciest::output_dot
void output_dot(std::ostream &stream) const
Definition: string_refinement_util.cpp:480
get_reachable
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:569
string_dependenciest::nodet::STRING
@ STRING
Definition: string_refinement_util.h:284
function_application_exprt
Application of (mathematical) function.
Definition: std_expr.h:4481
string_dependenciest::node_at
std::unique_ptr< const string_nodet > node_at(const array_string_exprt &e) const
Definition: string_refinement_util.cpp:259
is_char_array_type
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
Definition: string_refinement_util.cpp:37
string_dependenciest::add_constraints
void add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
Definition: string_refinement_util.cpp:505
irept::id
const irep_idt & id() const
Definition: irep.h:259
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
equation_symbol_mappingt::add
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
Definition: string_refinement_util.cpp:186
string_dependenciest::node_index_pool
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...
Definition: string_refinement_util.h:276
to_array_string_expr
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:101
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
string_builtin_functiont
Base class for string functions that are built in the solver.
Definition: string_builtin_function.h:19
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1117
string_dependenciest::eval_string_cache
std::vector< optionalt< exprt > > eval_string_cache
Definition: string_refinement_util.h:316
expr_util.h
Deprecated expression utility functions.
equation_symbol_mappingt::equations_containing
std::map< exprt, std::vector< std::size_t > > equations_containing
Record index of the equations that contain a given expression.
Definition: string_refinement_util.h:157
ssa_expr.h
string_dependenciest::nodet::BUILTIN
@ BUILTIN
Definition: string_refinement_util.h:283
string_dependenciest::builtin_function_nodet::index
std::size_t index
Definition: string_refinement_util.h:174
string_dependenciest::builtin_function_nodet::data
std::unique_ptr< string_builtin_functiont > data
Definition: string_refinement_util.h:176
interval_sparse_arrayt::concretize
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
Definition: string_refinement_util.cpp:168
string_dependenciest::string_nodet::dependencies
std::vector< std::size_t > dependencies
Definition: string_refinement_util.h:209
graph.h
array_typet
Arrays with given size.
Definition: std_types.h:1000
expr_iterator.h
equation_symbol_mappingt::strings_in_equation
std::unordered_map< std::size_t, std::vector< exprt > > strings_in_equation
Record expressions that are contained in the equation with the given index.
Definition: string_refinement_util.h:159
array_poolt::find
const array_string_exprt & find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
Definition: string_constraint_generator_main.cpp:314
stack
#define stack(x)
Definition: parser.h:144
string_dependenciest
Keep track of dependencies between strings.
Definition: string_refinement_util.h:166
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
has_char_pointer_subtype
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
Definition: string_refinement_util.cpp:49
sparse_arrayt::entries
std::map< std::size_t, exprt > entries
Definition: string_refinement_util.h:82
function_application_exprt::function
symbol_exprt & function()
Definition: std_expr.h:4496
string_dependenciest::nodet::index
std::size_t index
Definition: string_refinement_util.h:286
equation_symbol_mappingt::find_expressions
std::vector< exprt > find_expressions(const std::size_t i)
Definition: string_refinement_util.cpp:193
string_dependenciest::for_each_dependency
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.
Definition: string_refinement_util.cpp:443
array_list_exprt
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1779
exprt::operands
operandst & operands()
Definition: expr.h:78
std_expr.h
has_char_array_subexpr
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
Definition: string_refinement_util.cpp:54
equation_symbol_mappingt::find_equations
std::vector< std::size_t > find_equations(const exprt &expr)
Definition: string_refinement_util.cpp:199
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1739
can_cast_expr< with_exprt >
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:3588
array_string_exprt
Definition: string_expr.h:67
string_dependenciest::clear
void clear()
Clear the content of the dependency graph.
Definition: string_refinement_util.cpp:303
validation_modet::INVARIANT
@ INVARIANT
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:110
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470