cprover
string_dependencies.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String solver
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H
13 #define CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H
14 
15 #include <memory>
16 
17 #include <util/nodiscard.h>
18 
20 
25 {
26 public:
29  {
30  public:
31  // index in the `builtin_function_nodes` vector
32  std::size_t index;
33  // pointer to the builtin function
34  std::unique_ptr<string_builtin_functiont> data;
35 
37  std::unique_ptr<string_builtin_functiont> d,
38  std::size_t i)
39  : index(i), data(std::move(d))
40  {
41  }
42 
44  : index(other.index), data(std::move(other.data))
45  {
46  }
47 
49  {
50  index = other.index;
51  data = std::move(other.data);
52  return *this;
53  }
54  };
55 
58  {
59  public:
60  // expression the node corresponds to
62  // index in the string_nodes vector
63  std::size_t index;
64  // builtin functions on which it depends, refered by there index in
65  // builtin_function node vector.
66  // \todo should these we shared pointers?
67  std::vector<std::size_t> dependencies;
68  // builtin function of which it is the result
70 
71  explicit string_nodet(array_string_exprt e, const std::size_t index)
72  : expr(std::move(e)), index(index)
73  {
74  }
75  };
76 
77  string_nodet &get_node(const array_string_exprt &e);
78 
79  std::unique_ptr<const string_nodet>
80  node_at(const array_string_exprt &e) const;
81 
82  builtin_function_nodet &
83  make_node(std::unique_ptr<string_builtin_functiont> builtin_function);
85  get_builtin_function(const builtin_function_nodet &node) const;
86 
90  void add_dependency(
91  const array_string_exprt &e,
92  const builtin_function_nodet &builtin_function);
93 
96  const string_nodet &node,
97  const std::function<void(const builtin_function_nodet &)> &f) const;
99  const builtin_function_nodet &node,
100  const std::function<void(const string_nodet &)> &f) const;
101 
107  const array_string_exprt &s,
108  const std::function<exprt(const exprt &)> &get_value) const;
109 
111  void clean_cache();
112 
113  void output_dot(std::ostream &stream) const;
114 
120 
122  void clear();
123 
124 private:
126  std::vector<builtin_function_nodet> builtin_function_nodes;
127 
129  std::vector<string_nodet> string_nodes;
130 
133  std::unordered_map<array_string_exprt, std::size_t, irep_hash>
135 
136  class nodet
137  {
138  public:
139  enum
140  {
142  STRING
143  } kind;
144  std::size_t index;
145 
146  explicit nodet(const builtin_function_nodet &builtin)
147  : kind(BUILTIN), index(builtin.index)
148  {
149  }
150 
151  explicit nodet(const string_nodet &string_node)
152  : kind(STRING), index(string_node.index)
153  {
154  }
155 
156  bool operator==(const nodet &n) const
157  {
158  return n.kind == kind && n.index == index;
159  }
160  };
161 
163  // NOLINTNEXTLINE(readability/identifiers)
164  struct node_hash
165  {
166  size_t
167  operator()(const string_dependenciest::nodet &node) const optional_noexcept
168  {
169  return 2 * node.index +
170  (node.kind == string_dependenciest::nodet::STRING ? 0 : 1);
171  }
172  };
173 
174  mutable std::vector<optionalt<exprt>> eval_string_cache;
175 
177  void for_each_node(const std::function<void(const nodet &)> &f) const;
178 
180  void for_each_successor(
181  const nodet &i,
182  const std::function<void(const nodet &)> &f) const;
183 };
184 
203  string_dependenciest &dependencies,
204  const exprt &expr,
205  array_poolt &array_pool,
206  symbol_generatort &fresh_symbol);
207 
208 #endif // CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:42
Base class for all expressions.
Definition: expr.h:54
Base class for string functions that are built in the solver.
A builtin function node contains a builtin function call.
std::unique_ptr< string_builtin_functiont > data
builtin_function_nodet(builtin_function_nodet &&other)
builtin_function_nodet & operator=(builtin_function_nodet &&other)
builtin_function_nodet(std::unique_ptr< string_builtin_functiont > d, std::size_t i)
nodet(const string_nodet &string_node)
nodet(const builtin_function_nodet &builtin)
bool operator==(const nodet &n) const
enum string_dependenciest::nodet::@6 kind
A string node points to builtin_function on which it depends.
string_nodet(array_string_exprt e, const std::size_t index)
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&#160;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
#define NODISCARD
Definition: nodiscard.h:22
nonstd::optional< T > optionalt
Definition: optional.h:35
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...
Definition: kdev_t.h:24
Collection of constraints of different types: existential formulas, universal formulas,...
size_t operator()(const string_dependenciest::nodet &node) const