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 
12 #include <memory>
13 
15 #include "string_constraint.h"
17 
25 bool is_char_type(const typet &type);
26 
32 bool is_char_array_type(const typet &type, const namespacet &ns);
33 
37 bool is_char_pointer_type(const typet &type);
38 
46 bool has_char_pointer_subtype(const typet &type, const namespacet &ns);
47 
51 bool has_char_array_subexpr(const exprt &expr, const namespacet &ns);
52 
54 {
55  std::map<exprt, std::set<exprt>> cumulative;
56  std::map<exprt, std::set<exprt>> current;
57 };
58 
60 {
61  std::vector<string_constraintt> universal;
62  std::vector<string_not_contains_constraintt> not_contains;
63 };
64 
68 {
69 public:
74  explicit sparse_arrayt(const with_exprt &expr);
75 
78  static exprt to_if_expression(const with_exprt &expr, const exprt &index);
79 
80 protected:
82  std::map<std::size_t, exprt> entries;
84  {
85  }
86 };
87 
93 {
94 public:
99  explicit interval_sparse_arrayt(const with_exprt &expr) : sparse_arrayt(expr)
100  {
101  }
102 
106  interval_sparse_arrayt(const array_exprt &expr, const exprt &extra_value);
107 
112  const array_list_exprt &expr,
113  const exprt &extra_value);
114 
115  exprt to_if_expression(const exprt &index) const;
116 
120  of_expr(const exprt &expr, const exprt &extra_value);
121 
123  array_exprt concretize(std::size_t size, const typet &index_type) const;
124 
127  exprt at(std::size_t index) const;
128 
132  {
133  }
134 };
135 
141 {
142 public:
144  void add(const std::size_t i, const exprt &expr);
145 
149  std::vector<exprt> find_expressions(const std::size_t i);
150 
153  std::vector<std::size_t> find_equations(const exprt &expr);
154 
155 private:
157  std::map<exprt, std::vector<std::size_t>> equations_containing;
159  std::unordered_map<std::size_t, std::vector<exprt>> strings_in_equation;
160 };
161 
162 
167 {
168 public:
171  {
172  public:
173  // index in the `builtin_function_nodes` vector
174  std::size_t index;
175  // pointer to the builtin function
176  std::unique_ptr<string_builtin_functiont> data;
177 
179  std::unique_ptr<string_builtin_functiont> d,
180  std::size_t i)
181  : index(i), data(std::move(d))
182  {
183  }
184 
186  : index(other.index), data(std::move(other.data))
187  {
188  }
189 
191  {
192  index = other.index;
193  data = std::move(other.data);
194  return *this;
195  }
196  };
197 
200  {
201  public:
202  // expression the node corresponds to
204  // index in the string_nodes vector
205  std::size_t index;
206  // builtin functions on which it depends, refered by there index in
207  // builtin_function node vector.
208  // \todo should these we shared pointers?
209  std::vector<std::size_t> dependencies;
210  // builtin function of which it is the result
212 
213  explicit string_nodet(array_string_exprt e, const std::size_t index)
214  : expr(std::move(e)), index(index)
215  {
216  }
217  };
218 
219  string_nodet &get_node(const array_string_exprt &e);
220 
221  std::unique_ptr<const string_nodet>
222  node_at(const array_string_exprt &e) const;
223 
225  builtin_function_nodet &
226  make_node(std::unique_ptr<string_builtin_functiont> &builtin_function);
228  get_builtin_function(const builtin_function_nodet &node) const;
229 
233  void add_dependency(
234  const array_string_exprt &e,
235  const builtin_function_nodet &builtin_function);
236 
238  void for_each_dependency(
239  const string_nodet &node,
240  const std::function<void(const builtin_function_nodet &)> &f) const;
241  void for_each_dependency(
242  const builtin_function_nodet &node,
243  const std::function<void(const string_nodet &)> &f) const;
244 
250  const array_string_exprt &s,
251  const std::function<exprt(const exprt &)> &get_value) const;
252 
254  void clean_cache();
255 
256  void output_dot(std::ostream &stream) const;
257 
262 
264  void clear();
265 
266 private:
268  std::vector<builtin_function_nodet> builtin_function_nodes;
269 
271  std::vector<string_nodet> string_nodes;
272 
275  std::unordered_map<array_string_exprt, std::size_t, irep_hash>
277 
278  class nodet
279  {
280  public:
281  enum
282  {
285  } kind;
286  std::size_t index;
287 
288  explicit nodet(const builtin_function_nodet &builtin)
289  : kind(BUILTIN), index(builtin.index)
290  {
291  }
292 
293  explicit nodet(const string_nodet &string_node)
294  : kind(STRING), index(string_node.index)
295  {
296  }
297 
298  bool operator==(const nodet &n) const
299  {
300  return n.kind == kind && n.index == index;
301  }
302  };
303 
305  // NOLINTNEXTLINE(readability/identifiers)
306  struct node_hash
307  {
308  size_t
309  operator()(const string_dependenciest::nodet &node) const optional_noexcept
310  {
311  return 2 * node.index +
312  (node.kind == string_dependenciest::nodet::STRING ? 0 : 1);
313  }
314  };
315 
316  mutable std::vector<optionalt<exprt>> eval_string_cache;
317 
319  void for_each_node(const std::function<void(const nodet &)> &f) const;
320 
322  void for_each_successor(
323  const nodet &i,
324  const std::function<void(const nodet &)> &f) const;
325 };
326 
340 bool add_node(
341  string_dependenciest &dependencies,
342  const equal_exprt &equation,
343  array_poolt &array_pool);
344 
345 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3514
string_axiomst::universal
std::vector< string_constraintt > universal
Definition: string_refinement_util.h:61
string_builtin_function.h
typet
The type of an expression, extends irept.
Definition: type.h:27
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
data
Definition: kdev_t.h:24
index_set_pairt
Definition: string_refinement_util.h:53
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
sparse_arrayt::sparse_arrayt
sparse_arrayt(exprt default_value)
Definition: string_refinement_util.h:83
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
string_dependenciest::string_nodet::index
std::size_t index
Definition: string_refinement_util.h:205
string_dependenciest::nodet::nodet
nodet(const string_nodet &string_node)
Definition: string_refinement_util.h:293
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_dependenciest::nodet::nodet
nodet(const builtin_function_nodet &builtin)
Definition: string_refinement_util.h:288
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
string_axiomst
Definition: string_refinement_util.h:59
string_dependenciest::node_hash::operator()
size_t operator()(const string_dependenciest::nodet &node) const optional_noexcept
Definition: string_refinement_util.h:309
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1484
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
interval_sparse_arrayt::interval_sparse_arrayt
interval_sparse_arrayt(exprt default_value)
Array containing the same value at each index.
Definition: string_refinement_util.h:130
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&#160;to node for builtin_function if e is a simple array expression.
Definition: string_refinement_util.cpp:293
sparse_arrayt::default_value
exprt default_value
Definition: string_refinement_util.h:81
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
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::node_hash
Hash function for nodes.
Definition: string_refinement_util.h:306
string_dependenciest::string_nodes
std::vector< string_nodet > string_nodes
Set of nodes representing strings.
Definition: string_refinement_util.h:271
has_char_array_subexpr
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
Definition: string_refinement_util.cpp:54
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
string_dependenciest::string_nodet::string_nodet
string_nodet(array_string_exprt e, const std::size_t index)
Definition: string_refinement_util.h:213
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
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
string_dependenciest::output_dot
void output_dot(std::ostream &stream) const
Definition: string_refinement_util.cpp:480
string_dependenciest::nodet::kind
enum string_dependenciest::nodet::@5 kind
string_dependenciest::nodet::STRING
Definition: string_refinement_util.h:284
string_dependenciest::node_at
std::unique_ptr< const string_nodet > node_at(const array_string_exprt &e) const
Definition: string_refinement_util.cpp:259
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
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
equation_symbol_mappingt
Maps equation to expressions contained in them and conversely expressions to equations that contain t...
Definition: string_refinement_util.h:140
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
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
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
string_dependenciest::builtin_function_nodet::builtin_function_nodet
builtin_function_nodet(std::unique_ptr< string_builtin_functiont > d, std::size_t i)
Definition: string_refinement_util.h:178
string_dependenciest::eval_string_cache
std::vector< optionalt< exprt > > eval_string_cache
Definition: string_refinement_util.h:316
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
string_dependenciest::nodet::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
string_constraint.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
string_dependenciest
Keep track of dependencies between strings.
Definition: string_refinement_util.h:166
sparse_arrayt::entries
std::map< std::size_t, exprt > entries
Definition: string_refinement_util.h:82
index_set_pairt::current
std::map< exprt, std::set< exprt > > current
Definition: string_refinement_util.h:56
string_dependenciest::builtin_function_nodet::operator=
builtin_function_nodet & operator=(builtin_function_nodet &&other)
Definition: string_refinement_util.h:190
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
has_char_pointer_subtype
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
Definition: string_refinement_util.cpp:49
string_dependenciest::builtin_function_nodet::builtin_function_nodet
builtin_function_nodet(builtin_function_nodet &&other)
Definition: string_refinement_util.h:185
string_dependenciest::string_nodet::expr
array_string_exprt expr
Definition: string_refinement_util.h:203
index_set_pairt::cumulative
std::map< exprt, std::set< exprt > > cumulative
Definition: string_refinement_util.h:55
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
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
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
string_dependenciest::nodet::operator==
bool operator==(const nodet &n) const
Definition: string_refinement_util.h:298
string_constraint_generator.h
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
string_axiomst::not_contains
std::vector< string_not_contains_constraintt > not_contains
Definition: string_refinement_util.h:62
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