cprover
string_refinement_util.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: String solver
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
10 #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
11 
13 #include "string_constraint.h"
15 
23 bool is_char_type(const typet &type);
24 
30 bool is_char_array_type(const typet &type, const namespacet &ns);
31 
35 bool is_char_pointer_type(const typet &type);
36 
44 bool has_char_pointer_subtype(const typet &type, const namespacet &ns);
45 
49 bool has_char_array_subexpr(const exprt &expr, const namespacet &ns);
50 
52 {
53  std::map<exprt, std::set<exprt>> cumulative;
54  std::map<exprt, std::set<exprt>> current;
55 };
56 
58 {
59  std::vector<string_constraintt> universal;
60  std::vector<string_not_contains_constraintt> not_contains;
61 };
62 
66 {
67 public:
72  explicit sparse_arrayt(const with_exprt &expr);
73 
76  virtual exprt to_if_expression(const exprt &index) const;
77 
80  virtual exprt at(std::size_t index) const;
81 
82 protected:
84  std::map<std::size_t, exprt> entries;
86  {
87  }
88 };
89 
95 {
96 public:
101  explicit interval_sparse_arrayt(const with_exprt &expr) : sparse_arrayt(expr)
102  {
103  }
104 
108  interval_sparse_arrayt(const array_exprt &expr, const exprt &extra_value);
109 
114  const array_list_exprt &expr,
115  const exprt &extra_value);
116 
117  exprt to_if_expression(const exprt &index) const override;
118 
122  of_expr(const exprt &expr, const exprt &extra_value);
123 
125  array_exprt concretize(std::size_t size, const typet &index_type) const;
126 
129  exprt at(std::size_t index) const override;
130 
134  {
135  }
136 };
137 
143 {
144 public:
146  void add(const std::size_t i, const exprt &expr);
147 
151  std::vector<exprt> find_expressions(const std::size_t i);
152 
155  std::vector<std::size_t> find_equations(const exprt &expr);
156 
157 private:
159  std::map<exprt, std::vector<std::size_t>> equations_containing;
161  std::unordered_map<std::size_t, std::vector<exprt>> strings_in_equation;
162 };
163 
164 
169 {
170 public:
173  {
174  public:
175  // index in the `builtin_function_nodes` vector
176  std::size_t index;
177  // pointer to the builtin function
178  std::unique_ptr<string_builtin_functiont> data;
179 
181  std::unique_ptr<string_builtin_functiont> d,
182  std::size_t i)
183  : index(i), data(std::move(d))
184  {
185  }
186 
188  : index(other.index), data(std::move(other.data))
189  {
190  }
191 
193  {
194  index = other.index;
195  data = std::move(other.data);
196  return *this;
197  }
198  };
199 
202  {
203  public:
204  // expression the node corresponds to
206  // index in the string_nodes vector
207  std::size_t index;
208  // builtin functions on which it depends, refered by there index in
209  // builtin_function node vector.
210  // \todo should these we shared pointers?
211  std::vector<std::size_t> dependencies;
212  // builtin function of which it is the result
214 
215  explicit string_nodet(array_string_exprt e, const std::size_t index)
216  : expr(std::move(e)), index(index)
217  {
218  }
219  };
220 
221  string_nodet &get_node(const array_string_exprt &e);
222 
223  std::unique_ptr<const string_nodet>
224  node_at(const array_string_exprt &e) const;
225 
227  builtin_function_nodet &
228  make_node(std::unique_ptr<string_builtin_functiont> &builtin_function);
230  get_builtin_function(const builtin_function_nodet &node) const;
231 
235  void add_dependency(
236  const array_string_exprt &e,
237  const builtin_function_nodet &builtin_function);
238 
240  void for_each_dependency(
241  const string_nodet &node,
242  const std::function<void(const builtin_function_nodet &)> &f) const;
243  void for_each_dependency(
244  const builtin_function_nodet &node,
245  const std::function<void(const string_nodet &)> &f) const;
246 
252  const array_string_exprt &s,
253  const std::function<exprt(const exprt &)> &get_value) const;
254 
256  void clean_cache();
257 
258  void output_dot(std::ostream &stream) const;
259 
264 
266  void clear();
267 
268 private:
270  std::vector<builtin_function_nodet> builtin_function_nodes;
271 
273  std::vector<string_nodet> string_nodes;
274 
277  std::unordered_map<array_string_exprt, std::size_t, irep_hash>
279 
280  class nodet
281  {
282  public:
283  enum
284  {
287  } kind;
288  std::size_t index;
289 
290  explicit nodet(const builtin_function_nodet &builtin)
291  : kind(BUILTIN), index(builtin.index)
292  {
293  }
294 
295  explicit nodet(const string_nodet &string_node)
296  : kind(STRING), index(string_node.index)
297  {
298  }
299 
300  bool operator==(const nodet &n) const
301  {
302  return n.kind == kind && n.index == index;
303  }
304  };
305 
307  // NOLINTNEXTLINE(readability/identifiers)
308  struct node_hash
309  {
310  size_t
311  operator()(const string_dependenciest::nodet &node) const optional_noexcept
312  {
313  return 2 * node.index +
314  (node.kind == string_dependenciest::nodet::STRING ? 0 : 1);
315  }
316  };
317 
318  mutable std::vector<optionalt<exprt>> eval_string_cache;
319 
321  void for_each_node(const std::function<void(const nodet &)> &f) const;
322 
324  void for_each_successor(
325  const nodet &i,
326  const std::function<void(const nodet &)> &f) const;
327 };
328 
342 bool add_node(
343  string_dependenciest &dependencies,
344  const equal_exprt &equation,
345  array_poolt &array_pool);
346 
347 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
The type of an expression.
Definition: type.h:22
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
string_nodet(array_string_exprt e, const std::size_t index)
const string_builtin_functiont & get_builtin_function(const builtin_function_nodet &node) const
Generates string constraints to link results from string functions with their arguments.
void add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
virtual exprt to_if_expression(const exprt &index) const
Creates an if_expr corresponding to the result of accessing the array at the given index...
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
void clean_cache()
Clean the cache used by eval
std::unique_ptr< string_builtin_functiont > data
string_nodet & get_node(const array_string_exprt &e)
enum string_dependenciest::nodet::@4 kind
std::map< exprt, std::set< exprt > > current
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 ...
std::unique_ptr< const string_nodet > node_at(const array_string_exprt &e) const
exprt to_if_expression(const exprt &index) const override
Creates an if_expr corresponding to the result of accessing the array at the given index...
STL namespace.
std::vector< builtin_function_nodet > builtin_function_nodes
Set of nodes representing builtin_functions.
Correspondance between arrays and pointers string representations.
Base class for string functions that are built in the solver.
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...
nodet(const string_nodet &string_node)
equality
Definition: std_expr.h:1354
void for_each_successor(const nodet &i, const std::function< void(const nodet &)> &f) const
Applies f on all successors of the node n.
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...
Defines string constraints.
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...
std::map< exprt, std::vector< std::size_t > > equations_containing
Record index of the equations that contain a given expression.
std::map< exprt, std::set< exprt > > cumulative
Represents arrays by the indexes up to which the value remains the same.
nonstd::optional< T > optionalt
Definition: optional.h:35
std::vector< string_nodet > string_nodes
Set of nodes representing strings.
void clear()
Clear the content of the dependency graph.
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list...
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::map< std::size_t, exprt > entries
bool operator==(const nodet &n) const
bitvector_typet index_type()
Definition: c_types.cpp:16
builtin_function_nodet(std::unique_ptr< string_builtin_functiont > d, std::size_t i)
exprt at(std::size_t index) const override
Get the value at the specified index.
std::vector< optionalt< exprt > > eval_string_cache
std::unordered_map< std::size_t, std::vector< exprt > > strings_in_equation
Record expressions that are contained in the equation with the given index.
Keep track of dependencies between strings.
interval_sparse_arrayt(exprt default_value)
Array containing the same value at each index.
A builtin function node contains a builtin function call.
A string node points to builtin_function on which it depends.
std::vector< string_constraintt > universal
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
std::vector< exprt > find_expressions(const std::size_t i)
Maps equation to expressions contained in them and conversely expressions to equations that contain t...
size_t operator()(const string_dependenciest::nodet &node) const optional_noexcept
Base class for all expressions.
Definition: expr.h:42
builtin_function_nodet & operator=(builtin_function_nodet &&other)
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
nodet(const builtin_function_nodet &builtin)
Operator to update elements in structs and arrays.
Definition: std_expr.h:3461
std::vector< std::size_t > dependencies
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
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} ...
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character...
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.
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, otherwise returns empty optional.
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
virtual exprt at(std::size_t index) const
Get the value at the specified index.
builtin_function_nodet(builtin_function_nodet &&other)
std::vector< std::size_t > find_equations(const exprt &expr)
sparse_arrayt(exprt default_value)
void for_each_node(const std::function< void(const nodet &)> &f) const
Applies f on all nodes.
array constructor from list of elements
Definition: std_expr.h:1617
Definition: kdev_t.h:24
std::vector< string_not_contains_constraintt > not_contains
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.
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating.
Definition: std_expr.h:1662
void output_dot(std::ostream &stream) const