cprover
array_pool.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String solver
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
13 
14 #ifndef CPROVER_SOLVERS_STRINGS_ARRAY_POOL_H
15 #define CPROVER_SOLVERS_STRINGS_ARRAY_POOL_H
16 
17 #include <set>
18 #include <util/std_expr.h>
19 #include <util/string_expr.h>
20 
22 class symbol_generatort final
23 {
24 public:
29  operator()(const irep_idt &prefix, const typet &type = bool_typet());
30 
31 private:
32  unsigned symbol_count = 0;
33 
34 #ifdef DEBUG
35 public:
37  std::vector<symbol_exprt> created_symbols;
38 #endif
39 };
40 
42 class array_poolt final
43 {
44 public:
45  explicit array_poolt(symbol_generatort &symbol_generator)
46  : fresh_symbol(symbol_generator)
47  {
48  }
49 
50  const std::unordered_map<exprt, array_string_exprt, irep_hash> &
52  {
53  return arrays_of_pointers;
54  }
55 
66 
73 
74  void insert(const exprt &pointer_expr, const array_string_exprt &array);
75 
77  array_string_exprt find(const exprt &pointer, const exprt &length);
78 
79  const std::unordered_map<array_string_exprt, exprt, irep_hash> &
80  created_strings() const;
81 
88 
89 private:
96  std::unordered_map<exprt, array_string_exprt, irep_hash> arrays_of_pointers;
97 
99  std::unordered_map<array_string_exprt, exprt, irep_hash> length_of_array;
100 
103 
105  const exprt &char_pointer,
106  const typet &char_array_type);
107 };
108 
113 array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg);
114 
119 array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr);
120 
121 #endif // CPROVER_SOLVERS_STRINGS_ARRAY_POOL_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
array_poolt::created_strings
const std::unordered_map< array_string_exprt, exprt, irep_hash > & created_strings() const
Return a map mapping all array_string_exprt of the array_pool to their length.
Definition: array_pool.cpp:177
symbol_generatort::operator()
symbol_exprt operator()(const irep_idt &prefix, const typet &type=bool_typet())
Generate a new symbol expression of the given type with some prefix.
Definition: array_pool.cpp:12
array_poolt::get_arrays_of_pointers
const std::unordered_map< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
Definition: array_pool.h:51
array_poolt::array_poolt
array_poolt(symbol_generatort &symbol_generator)
Definition: array_pool.h:45
array_poolt::find
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:182
typet
The type of an expression, extends irept.
Definition: type.h:29
array_poolt
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:43
array_poolt::get_or_create_length
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
Definition: array_pool.cpp:24
exprt
Base class for all expressions.
Definition: expr.h:53
bool_typet
The Boolean type.
Definition: std_types.h:37
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
symbol_generatort
Generation of fresh symbols of a given type.
Definition: array_pool.h:23
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
get_string_expr
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
Definition: array_pool.cpp:196
symbol_generatort::symbol_count
unsigned symbol_count
Definition: array_pool.h:32
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
array_poolt::get_length_if_exists
optionalt< exprt > get_length_if_exists(const array_string_exprt &s) const
As opposed to get_length(), do not create a new symbol if the length of the array_string_exprt does n...
Definition: array_pool.cpp:46
array_poolt::fresh_symbol
symbol_generatort & fresh_symbol
Generate fresh symbols.
Definition: array_pool.h:102
array_poolt::length_of_array
std::unordered_map< array_string_exprt, exprt, irep_hash > length_of_array
Associate length to arrays of infinite size.
Definition: array_pool.h:99
of_argument
array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg)
Converts a struct containing a length and pointer to an array.
Definition: array_pool.cpp:190
array_poolt::make_char_array_for_char_pointer
array_string_exprt make_char_array_for_char_pointer(const exprt &char_pointer, const typet &char_array_type)
Helper function for find.
Definition: array_pool.cpp:72
array_poolt::insert
void insert(const exprt &pointer_expr, const array_string_exprt &array)
Definition: array_pool.cpp:158
std_expr.h
API to expression classes.
string_expr.h
String expressions for the string solver.
array_string_exprt
Definition: string_expr.h:67
array_poolt::arrays_of_pointers
std::unordered_map< exprt, array_string_exprt, irep_hash > arrays_of_pointers
Associate arrays to char pointers Invariant: Each array_string_exprt in this map has a corresponding ...
Definition: array_pool.h:96
array_poolt::fresh_string
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
Construct a string expression whose length and content are new variables.
Definition: array_pool.cpp:55