cprover
Loading...
Searching...
No Matches
value_set_fi.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set (Flow Insensitive, Sharing)
4
5Author: Daniel Kroening, kroening@kroening.com
6 CM Wintersteiger
7
8\*******************************************************************/
9
12
13#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H
14#define CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H
15
16#include <list>
17#include <map>
18#include <set>
19#include <unordered_set>
20
21#include <util/mp_arith.h>
23
24#include "object_numbering.h"
25
26class codet;
27class namespacet;
28
30{
31public:
33 changed(false)
34 // to_function, to_target_index are set by set_to()
35 // from_function, from_target_index are set by set_from()
36 {
37 }
38
43
44 void set_from(const irep_idt &function, unsigned inx)
45 {
48 }
49
50 void set_to(const irep_idt &function, unsigned inx)
51 {
53 to_target_index = inx;
54 }
55
56 typedef irep_idt idt;
57
61 bool offset_is_zero(const offsett &offset) const
62 {
63 return offset && offset->is_zero();
64 }
65
67 {
68 typedef std::map<object_numberingt::number_type, offsett> data_typet;
70
71 public:
72 // NOLINTNEXTLINE(readability/identifiers)
73 typedef data_typet::iterator iterator;
74 // NOLINTNEXTLINE(readability/identifiers)
75 typedef data_typet::const_iterator const_iterator;
76 // NOLINTNEXTLINE(readability/identifiers)
77 typedef data_typet::value_type value_type;
78
79 iterator begin() { return data.begin(); }
80 const_iterator begin() const { return data.begin(); }
81 const_iterator cbegin() const { return data.cbegin(); }
82
83 iterator end() { return data.end(); }
84 const_iterator end() const { return data.end(); }
85 const_iterator cend() const { return data.cend(); }
86
87 size_t size() const { return data.size(); }
88
90 {
91 return data[i];
92 }
93
94 template <typename It>
95 void insert(It b, It e) { data.insert(b, e); }
96
97 template <typename T>
98 const_iterator find(T &&t) const { return data.find(std::forward<T>(t)); }
99
100 static const object_map_dt blank;
101
102 protected:
103 ~object_map_dt()=default;
104 };
105
106 exprt to_expr(const object_map_dt::value_type &it) const;
107
109
110 void set(object_mapt &dest, const object_map_dt::value_type &it) const
111 {
112 dest.write()[it.first]=it.second;
113 }
114
115 bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
116 {
117 return insert(dest, it.first, it.second);
118 }
119
120 bool insert(object_mapt &dest, const exprt &src) const
121 {
122 return insert(dest, object_numbering.number(src), offsett());
123 }
124
125 bool insert(
126 object_mapt &dest,
127 const exprt &src,
128 const mp_integer &offset_value) const
129 {
130 return insert(dest, object_numbering.number(src), offsett(offset_value));
131 }
132
133 bool insert(
134 object_mapt &dest,
136 const offsett &offset) const
137 {
138 if(dest.read().find(n)==dest.read().end())
139 {
140 // new
141 dest.write()[n] = offset;
142 return true;
143 }
144 else
145 {
146 offsett &old_offset = dest.write()[n];
147
148 if(old_offset && offset)
149 {
150 if(*old_offset == *offset)
151 return false;
152 else
153 {
154 old_offset.reset();
155 return true;
156 }
157 }
158 else if(!old_offset)
159 return false;
160 else
161 {
162 old_offset.reset();
163 return true;
164 }
165 }
166 }
167
168 bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
169 {
170 return insert(dest, object_numbering.number(expr), offset);
171 }
172
173 struct entryt
174 {
177 std::string suffix;
178
180 {
181 }
182
183 entryt(const idt &_identifier, const std::string _suffix):
184 identifier(_identifier),
185 suffix(_suffix)
186 {
187 }
188 };
189
190 typedef std::unordered_set<exprt, irep_hash> expr_sett;
191
192 typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
193
194 #ifdef USE_DSTRING
195 typedef std::map<idt, entryt> valuest;
196 typedef std::set<idt> flatten_seent;
197 typedef std::unordered_set<idt> gvs_recursion_sett;
198 typedef std::unordered_set<idt> recfind_recursion_sett;
199 typedef std::unordered_set<idt> assign_recursion_sett;
200 #else
201 typedef std::unordered_map<idt, entryt, string_hash> valuest;
202 typedef std::unordered_set<idt, string_hash> flatten_seent;
203 typedef std::unordered_set<idt, string_hash> gvs_recursion_sett;
204 typedef std::unordered_set<idt, string_hash> recfind_recursion_sett;
205 typedef std::unordered_set<idt, string_hash> assign_recursion_sett;
206 #endif
207
208 std::vector<exprt>
209 get_value_set(const exprt &expr, const namespacet &ns) const;
210
212 const idt &identifier,
213 const std::string &suffix);
214
215 void clear()
216 {
217 values.clear();
218 }
219
220 void add_var(const idt &id)
221 {
222 get_entry(id, "");
223 }
224
225 void add_var(const entryt &e)
226 {
228 }
229
230 entryt &get_entry(const idt &id, const std::string &suffix)
231 {
232 return get_entry(entryt(id, suffix));
233 }
234
236 {
237 std::string index=id2string(e.identifier)+e.suffix;
238
239 std::pair<valuest::iterator, bool> r=
240 values.insert(std::pair<idt, entryt>(index, e));
241
242 return r.first->second;
243 }
244
245 void add_vars(const std::list<entryt> &vars)
246 {
247 for(std::list<entryt>::const_iterator
248 it=vars.begin();
249 it!=vars.end();
250 it++)
251 add_var(*it);
252 }
253
254 void output(
255 const namespacet &ns,
256 std::ostream &out) const;
257
259
261
262 // true = added something new
263 bool make_union(object_mapt &dest, const object_mapt &src) const;
264
265 // true = added something new
266 bool make_union(const valuest &new_values);
267
268 // true = added something new
269 bool make_union(const value_set_fit &new_values)
270 {
271 return make_union(new_values.values);
272 }
273
274 void apply_code(const codet &code, const namespacet &ns);
275
276 void assign(
277 const exprt &lhs,
278 const exprt &rhs,
279 const namespacet &ns);
280
281 void do_function_call(
282 const irep_idt &function,
283 const exprt::operandst &arguments,
284 const namespacet &ns);
285
286 // edge back to call site
287 void do_end_function(
288 const exprt &lhs,
289 const namespacet &ns);
290
292 const exprt &expr,
293 expr_sett &expr_set,
294 const namespacet &ns) const;
295
296protected:
298 const exprt &expr,
299 expr_sett &expr_set,
300 const namespacet &ns) const;
301
303 const exprt &expr,
304 object_mapt &dest,
305 const std::string &suffix,
306 const typet &original_type,
307 const namespacet &ns,
308 gvs_recursion_sett &recursion_set) const;
309
310
311 void get_value_set(
312 const exprt &expr,
313 object_mapt &dest,
314 const namespacet &ns) const;
315
317 const exprt &expr,
318 object_mapt &dest,
319 const namespacet &ns) const
320 {
321 get_reference_set_sharing_rec(expr, dest, ns);
322 }
323
325 const exprt &expr,
326 object_mapt &dest,
327 const namespacet &ns) const;
328
329 void dereference_rec(
330 const exprt &src,
331 exprt &dest) const;
332
333 void assign_rec(
334 const exprt &lhs,
335 const object_mapt &values_rhs,
336 const std::string &suffix,
337 const namespacet &ns,
338 assign_recursion_sett &recursion_set);
339
340 void flatten(const entryt &e, object_mapt &dest) const;
341
342 void flatten_rec(
343 const entryt&,
345 flatten_seent&) const;
346};
347
348#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
number_type number(const key_type &a)
Definition numbering.h:37
const T & read() const
The type of an expression, extends irept.
Definition type.h:29
offsett & operator[](object_numberingt::number_type i)
const_iterator find(T &&t) const
data_typet::value_type value_type
std::map< object_numberingt::number_type, offsett > data_typet
const_iterator cbegin() const
const_iterator begin() const
const_iterator end() const
data_typet::const_iterator const_iterator
const_iterator cend() const
static const object_map_dt blank
data_typet::iterator iterator
bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
static object_numberingt object_numbering
std::unordered_set< idt, string_hash > gvs_recursion_sett
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns)
static numberingt< irep_idt > function_numbering
void add_var(const idt &id)
bool make_union(object_mapt &dest, const object_mapt &src) const
void add_vars(const std::list< entryt > &vars)
std::unordered_set< idt, string_hash > recfind_recursion_sett
std::vector< exprt > get_value_set(const exprt &expr, const namespacet &ns) const
void set_from(const irep_idt &function, unsigned inx)
void set_to(const irep_idt &function, unsigned inx)
unsigned from_function
bool make_union(const value_set_fit &new_values)
void apply_code(const codet &code, const namespacet &ns)
reference_counting< object_map_dt > object_mapt
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)
unsigned to_function
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const
void get_reference_set_sharing(const exprt &expr, object_mapt &dest, const namespacet &ns) const
void dereference_rec(const exprt &src, exprt &dest) const
std::unordered_map< idt, entryt, string_hash > valuest
std::unordered_set< idt, string_hash > assign_recursion_sett
void output(const namespacet &ns, std::ostream &out) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &) const
std::unordered_set< exprt, irep_hash > expr_sett
void do_end_function(const exprt &lhs, const namespacet &ns)
std::unordered_set< unsigned int > dynamic_object_id_sett
void flatten(const entryt &e, object_mapt &dest) const
bool offset_is_zero(const offsett &offset) const
entryt & get_entry(const idt &id, const std::string &suffix)
unsigned from_target_index
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
void add_var(const entryt &e)
entryt & get_entry(const entryt &e)
std::unordered_set< idt, string_hash > flatten_seent
bool insert(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
unsigned to_target_index
exprt to_expr(const object_map_dt::value_type &it) const
void set(object_mapt &dest, const object_map_dt::value_type &it) const
bool insert(object_mapt &dest, const exprt &src) const
bool insert(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
expr_sett & get(const idt &identifier, const std::string &suffix)
std::unordered_set< exprt, irep_hash > expr_sett
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
static int8_t r
Definition irep_hash.h:60
Object Numbering.
nonstd::optional< T > optionalt
Definition optional.h:35
Reference Counting.
BigInt mp_integer
Definition smt_terms.h:12
Definition kdev_t.h:24
int size
Definition kdev_t.h:25
entryt(const idt &_identifier, const std::string _suffix)