cprover
Loading...
Searching...
No Matches
value_set_fivr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set (Flow Insensitive, Sharing, Validity Regions)
4
5Author: Daniel Kroening, kroening@kroening.com
6 CM Wintersteiger
7
8\*******************************************************************/
9
12
13#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVR_H
14#define CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVR_H
15
16#include <list>
17#include <map>
18#include <unordered_set>
19
20#include <util/mp_arith.h>
21#include <util/namespace.h>
23#include <util/invariant.h>
24
25#include "object_numbering.h"
26
27class codet;
28
30{
31public:
33 {
34 }
35
40
41 void set_from(const irep_idt &function, unsigned inx)
42 {
43 from_function = function_numbering.number(function);
45 }
46
47 void set_to(const irep_idt &function, unsigned inx)
48 {
49 to_function = function_numbering.number(function);
51 }
52
53 typedef irep_idt idt;
54
58 bool offset_is_zero(const offsett &offset) const
59 {
60 return offset && offset->is_zero();
61 }
62
64 {
65 public:
67 static const object_map_dt blank;
68
69 typedef std::map<object_numberingt::number_type, offsett> objmapt;
71
72 // NOLINTNEXTLINE(readability/identifiers)
73 typedef objmapt::const_iterator const_iterator;
74 // NOLINTNEXTLINE(readability/identifiers)
75 typedef objmapt::iterator iterator;
76
81 iterator begin() { return objmap.begin(); }
82 const_iterator begin() const { return objmap.begin(); }
83 iterator end() { return objmap.end(); }
84 const_iterator end() const { return objmap.end(); }
85 size_t size() const { return objmap.size(); }
86 bool empty() const { return objmap.empty(); }
88
93
94 // operator[] is the only way to insert something!
95 std::pair<iterator, bool>
96 insert(const std::pair<object_numberingt::number_type, offsett> &)
97 {
99 }
101 insert(iterator, const std::pair<object_numberingt::number_type, offsett> &)
102 {
104 }
105
107 {
108 public:
109 unsigned function;
110 unsigned from, to;
111
113 function(0), from(0), to(0)
114 {
115 }
116
117 validity_ranget(unsigned fnc, unsigned f, unsigned t):
118 function(fnc), from(f), to(t)
119 {
120 }
121
122 bool contains(unsigned f, unsigned line) const
123 {
124 return (function==f && from<=line && line<=to);
125 }
126 };
127
128 typedef std::list<validity_ranget> vrange_listt;
129 typedef std::map<unsigned, vrange_listt> validity_rangest;
131
132 bool set_valid_at(unsigned inx, unsigned f, unsigned line);
133 bool set_valid_at(unsigned inx, const validity_ranget &vr);
134 bool is_valid_at(unsigned inx, unsigned f, unsigned line) const;
135 };
136
138
140
142 {
143 dest.write()[it->first]=it->second;
144 }
145
147 {
148 return insert_to(dest, it->first, it->second);
149 }
150
151 bool insert_to(object_mapt &dest, const exprt &src) const
152 {
153 return insert_to(dest, object_numbering.number(src), offsett());
154 }
155
158 const exprt &src,
159 const mp_integer &offset_value) const
160 {
161 return insert_to(dest, object_numbering.number(src), offsett(offset_value));
162 }
163
167 const offsett &offset) const;
168
169 bool
170 insert_to(object_mapt &dest, const exprt &expr, const offsett &offset) const
171 {
172 return insert_to(dest, object_numbering.number(expr), offset);
173 }
174
176 {
177 return insert_from(dest, it->first, it->second);
178 }
179
180 bool insert_from(object_mapt &dest, const exprt &src) const
181 {
182 return insert_from(dest, object_numbering.number(src), offsett());
183 }
184
187 const exprt &src,
188 const mp_integer &offset_value) const
189 {
190 return insert_from(
192 }
193
197 const offsett &offset) const;
198
199 bool
200 insert_from(object_mapt &dest, const exprt &expr, const offsett &offset) const
201 {
202 return insert_from(dest, object_numbering.number(expr), offset);
203 }
204
205 struct entryt
206 {
209 std::string suffix;
210
211 entryt() { }
212
213 entryt(const idt &_identifier, const std::string _suffix):
214 identifier(_identifier),
216 {
217 }
218 };
219
220 typedef std::unordered_set<exprt, irep_hash> expr_sett;
221
222 typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
223
224 #ifdef USE_DSTRING
225 typedef std::map<idt, entryt> valuest;
226 typedef std::unordered_set<idt> flatten_seent;
227 typedef std::unordered_set<idt> gvs_recursion_sett;
228 typedef std::unordered_set<idt> recfind_recursion_sett;
229 typedef std::unordered_set<idt> assign_recursion_sett;
230 #else
231 typedef std::unordered_map<idt, entryt, string_hash> valuest;
232 typedef std::unordered_set<idt, string_hash> flatten_seent;
233 typedef std::unordered_set<idt, string_hash> gvs_recursion_sett;
234 typedef std::unordered_set<idt, string_hash> recfind_recursion_sett;
235 typedef std::unordered_set<idt, string_hash> assign_recursion_sett;
236 #endif
237
239 const exprt &expr,
240 std::list<exprt> &expr_set,
241 const namespacet &ns) const;
242
244 const idt &identifier,
245 const std::string &suffix);
246
247 void clear()
248 {
249 values.clear();
250 }
251
252 void add_var(const idt &id)
253 {
254 get_entry(id, "");
255 }
256
257 void add_var(const entryt &e)
258 {
260 }
261
262 entryt &get_entry(const idt &id, const std::string &suffix)
263 {
264 return get_entry(entryt(id, suffix));
265 }
266
268 {
269 std::string index=id2string(e.identifier)+e.suffix;
270
271 std::pair<valuest::iterator, bool> r=
272 values.insert(std::pair<idt, entryt>(index, e));
273
274 return r.first->second;
275 }
276
277 entryt &get_temporary_entry(const idt &id, const std::string &suffix)
278 {
279 std::string index=id2string(id)+suffix;
280 return temporary_values[index];
281 }
282
283 void add_vars(const std::list<entryt> &vars)
284 {
285 for(std::list<entryt>::const_iterator
286 it=vars.begin();
287 it!=vars.end();
288 it++)
289 add_var(*it);
290 }
291
292 void output(
293 const namespacet &ns,
294 std::ostream &out) const;
295
298
299 // true = added something new
302 const object_mapt &src) const;
303
306 const object_mapt &src) const;
307
310 const object_mapt &src) const;
311
312 void apply_code(const codet &code, const namespacet &ns);
313
314 bool handover();
315
316 void assign(
317 const exprt &lhs,
318 const exprt &rhs,
319 const namespacet &ns,
320 bool add_to_sets=false);
321
323 const irep_idt &function,
324 const exprt::operandst &arguments,
325 const namespacet &ns);
326
327 // edge back to call site
329 const exprt &lhs,
330 const namespacet &ns);
331
333 const exprt &expr,
334 expr_sett &expr_set,
335 const namespacet &ns) const;
336
337protected:
339 const exprt &expr,
340 expr_sett &expr_set,
341 const namespacet &ns) const;
342
344 const exprt &expr,
346 const std::string &suffix,
347 const typet &original_type,
348 const namespacet &ns,
349 gvs_recursion_sett &recursion_set) const;
350
352 const exprt &expr,
354 const namespacet &ns) const;
355
357 const exprt &expr,
359 const namespacet &ns) const
360 {
362 }
363
365 const exprt &expr,
367 const namespacet &ns) const;
368
370 const exprt &src,
371 exprt &dest) const;
372
374 const exprt &lhs,
375 const object_mapt &values_rhs,
376 const std::string &suffix,
377 const namespacet &ns,
378 assign_recursion_sett &recursion_set,
379 bool add_to_sets);
380
382 const entryt &e,
383 object_mapt &dest) const;
384
386 const entryt&,
389 unsigned from_function) const;
390
392 const irep_idt &ident,
393 const object_mapt &rhs,
394 recfind_recursion_sett &recursion_set) const;
395};
396
397#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVR_H
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
The type of an expression, extends irept.
Definition type.h:29
bool contains(unsigned f, unsigned line) const
validity_ranget(unsigned fnc, unsigned f, unsigned t)
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
bool set_valid_at(unsigned inx, const validity_ranget &vr)
const_iterator begin() const
objmapt::const_iterator const_iterator
std::map< unsigned, vrange_listt > validity_rangest
const_iterator find(object_numberingt::number_type k)
iterator insert(iterator, const std::pair< object_numberingt::number_type, offsett > &)
const_iterator end() const
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
offsett & operator[](object_numberingt::number_type k)
std::map< object_numberingt::number_type, offsett > objmapt
std::pair< iterator, bool > insert(const std::pair< object_numberingt::number_type, offsett > &)
static const object_map_dt blank
std::list< validity_ranget > vrange_listt
std::unordered_set< unsigned int > dynamic_object_id_sett
std::unordered_set< idt, string_hash > recfind_recursion_sett
bool recursive_find(const irep_idt &ident, const object_mapt &rhs, recfind_recursion_sett &recursion_set) const
bool insert_from(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
void flatten(const entryt &e, object_mapt &dest) const
bool insert_to(object_mapt &dest, const exprt &expr, const offsett &offset) const
void add_var(const entryt &e)
bool insert_to(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
void dereference_rec(const exprt &src, exprt &dest) const
void get_reference_set_sharing(const exprt &expr, object_mapt &dest, const namespacet &ns) const
bool insert_from(object_mapt &dest, const exprt &expr, const offsett &offset) const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
std::unordered_set< idt, string_hash > gvs_recursion_sett
static object_numberingt object_numbering
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
std::unordered_set< idt, string_hash > flatten_seent
expr_sett & get(const idt &identifier, const std::string &suffix)
void get_value_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
entryt & get_entry(const idt &id, const std::string &suffix)
void do_end_function(const exprt &lhs, const namespacet &ns)
void apply_code(const codet &code, const namespacet &ns)
unsigned to_target_index
unsigned from_target_index
void output(const namespacet &ns, std::ostream &out) const
std::unordered_set< exprt, irep_hash > expr_sett
bool offset_is_zero(const offsett &offset) const
bool insert_from(object_mapt &dest, const exprt &src) const
void add_var(const idt &id)
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
entryt & get_entry(const entryt &e)
bool insert_to(object_mapt &dest, const exprt &src) const
std::unordered_set< idt, string_hash > assign_recursion_sett
bool insert_from(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
static numberingt< irep_idt > function_numbering
bool make_union(object_mapt &dest, const object_mapt &src) const
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set, bool add_to_sets)
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
void add_vars(const std::list< entryt > &vars)
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
bool insert_to(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
void set_from(const irep_idt &function, unsigned inx)
void flatten_rec(const entryt &, object_mapt &, flatten_seent &, unsigned from_function) const
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
unsigned from_function
reference_counting< object_map_dt > object_mapt
std::unordered_map< idt, entryt, string_hash > valuest
void set(object_mapt &dest, object_map_dt::const_iterator it) const
bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
void set_to(const irep_idt &function, unsigned inx)
void copy_objects(object_mapt &dest, const object_mapt &src) const
exprt to_expr(object_map_dt::const_iterator it) const
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
static int8_t r
Definition irep_hash.h:60
Object Numbering.
Reference Counting.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
entryt(const idt &_identifier, const std::string _suffix)