cprover
value_set_fivrns.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set (Flow Insensitive, Validity Regions)
4
5Author: Daniel Kroening, kroening@kroening.com
6 CM Wintersteiger
7
8\*******************************************************************/
9
12
13#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVRNS_H
14#define CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVRNS_H
15
16#include <list>
17#include <map>
18#include <string>
19#include <unordered_set>
20
21#include <util/mp_arith.h>
22#include <util/namespace.h>
24#include <util/invariant.h>
25
26#include "object_numbering.h"
27
28class codet;
29
31{
32public:
34 {
35 }
36
41
42 void set_from(const irep_idt &function, unsigned inx)
43 {
46 }
47
48 void set_to(const irep_idt &function, unsigned inx)
49 {
51 to_target_index = inx;
52 }
53
54 typedef irep_idt idt;
55
59 bool offset_is_zero(offsett offset) const
60 {
61 return offset && offset->is_zero();
62 }
63
65 {
66 public:
68 static const object_map_dt blank;
69
70 typedef std::map<object_numberingt::number_type, offsett> objmapt;
72
73 // NOLINTNEXTLINE(readability/identifiers)
74 typedef objmapt::const_iterator const_iterator;
75 // NOLINTNEXTLINE(readability/identifiers)
76 typedef objmapt::iterator iterator;
77
79 {
80 return objmap.find(k);
81 }
82 iterator begin() { return objmap.begin(); }
83 const_iterator begin() const { return objmap.begin(); }
84 iterator end() { return objmap.end(); }
85 const_iterator end() const { return objmap.end(); }
86 size_t size() const { return objmap.size(); }
87 bool empty() const { return objmap.empty(); }
88 void clear() { objmap.clear(); validity_ranges.clear(); }
89
91 {
92 return objmap[k];
93 }
94
95 // operator[] is the only way to insert something!
96 std::pair<iterator, bool>
97 insert(const std::pair<object_numberingt::number_type, offsett> &)
98 {
100 }
102 insert(iterator, const std::pair<object_numberingt::number_type, offsett> &)
103 {
105 }
106
108 {
109 public:
110 unsigned function;
111 unsigned from, to;
112
114 function(0), from(0), to(0)
115 {
116 }
117
118 validity_ranget(unsigned fnc, unsigned f, unsigned t):
119 function(fnc), from(f), to(t)
120 {
121 }
122
123 bool contains(unsigned f, unsigned line) const
124 {
125 return (function==f && from<=line && line<=to);
126 }
127 };
128
129 typedef std::list<validity_ranget> vrange_listt;
130 typedef std::map<unsigned, vrange_listt> validity_rangest;
132
133 bool set_valid_at(unsigned inx, unsigned f, unsigned line);
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
157 object_mapt &dest,
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
165 object_mapt &dest,
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
186 object_mapt &dest,
187 const exprt &src,
188 const mp_integer &offset_value) const
189 {
190 return insert_from(
191 dest, object_numbering.number(src), offsett(offset_value));
192 }
193
195 object_mapt &dest,
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),
215 suffix(_suffix)
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 #else
227 typedef std::unordered_map<idt, entryt, string_hash> valuest;
228 #endif
229
231 const exprt &expr,
232 std::list<exprt> &expr_set,
233 const namespacet &ns) const;
234
236 const idt &identifier,
237 const std::string &suffix);
238
239 void clear()
240 {
241 values.clear();
242 }
243
244 void add_var(const idt &id)
245 {
246 get_entry(id, "");
247 }
248
249 void add_var(const entryt &e)
250 {
252 }
253
254 entryt &get_entry(const idt &id, const std::string &suffix)
255 {
256 return get_entry(entryt(id, suffix));
257 }
258
260 {
261 std::string index=id2string(e.identifier)+e.suffix;
262
263 std::pair<valuest::iterator, bool> r=
264 values.insert(std::pair<idt, entryt>(index, e));
265
266 return r.first->second;
267 }
268
269 entryt &get_temporary_entry(const idt &id, const std::string &suffix)
270 {
271 std::string index=id2string(id)+suffix;
272 return temporary_values[index];
273 }
274
275 void add_vars(const std::list<entryt> &vars)
276 {
277 for(std::list<entryt>::const_iterator
278 it=vars.begin();
279 it!=vars.end();
280 it++)
281 add_var(*it);
282 }
283
284 void output(
285 const namespacet &ns,
286 std::ostream &out) const;
287
289 const entryt &e,
290 const namespacet &ns,
291 std::ostream &out) const;
292
295
296 // true = added something new
298 object_mapt &dest,
299 const object_mapt &src) const;
300
302 object_mapt &dest,
303 const object_mapt &src) const;
304
306 object_mapt &dest,
307 const object_mapt &src) const;
308
309 void apply_code(const codet &code, const namespacet &ns);
310
311 bool handover();
312
313 void assign(
314 const exprt &lhs,
315 const exprt &rhs,
316 const namespacet &ns,
317 bool add_to_sets=false);
318
320 const irep_idt &function,
321 const exprt::operandst &arguments,
322 const namespacet &ns);
323
324 // edge back to call site
326 const exprt &lhs,
327 const namespacet &ns);
328
330 const exprt &expr,
331 expr_sett &expr_set,
332 const namespacet &ns) const;
333
334protected:
336 const exprt &expr,
337 object_mapt &dest,
338 const std::string &suffix,
339 const typet &original_type,
340 const namespacet &ns) const;
341
343 const exprt &expr,
344 object_mapt &dest,
345 const namespacet &ns) const;
346
348 const exprt &expr,
349 object_mapt &dest,
350 const namespacet &ns) const
351 {
352 get_reference_set_rec(expr, dest, ns);
353 }
354
356 const exprt &expr,
357 object_mapt &dest,
358 const namespacet &ns) const;
359
361 const exprt &src,
362 exprt &dest) const;
363
365 const exprt &lhs,
366 const object_mapt &values_rhs,
367 const std::string &suffix,
368 const namespacet &ns,
369 bool add_to_sets);
370};
371
372#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVRNS_H
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
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
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)
iterator insert(iterator, const std::pair< object_numberingt::number_type, offsett > &)
const_iterator find(object_numberingt::number_type k)
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
std::list< validity_ranget > vrange_listt
std::pair< iterator, bool > insert(const std::pair< object_numberingt::number_type, offsett > &)
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
static const object_map_dt blank
offsett & operator[](object_numberingt::number_type k)
std::map< unsigned, vrange_listt > validity_rangest
std::map< object_numberingt::number_type, offsett > objmapt
objmapt::const_iterator const_iterator
const_iterator begin() const
static numberingt< irep_idt > function_numbering
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
bool insert_to(object_mapt &dest, const exprt &src) const
bool insert_from(object_mapt &dest, const exprt &expr, const offsett &offset) const
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
std::unordered_set< unsigned int > dynamic_object_id_sett
expr_sett & get(const idt &identifier, const std::string &suffix)
void output(const namespacet &ns, std::ostream &out) const
bool insert_from(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
reference_counting< object_map_dt > object_mapt
exprt to_expr(object_map_dt::const_iterator it) const
std::unordered_map< idt, entryt, string_hash > valuest
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
void set_to(const irep_idt &function, unsigned inx)
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
entryt & get_entry(const idt &id, const std::string &suffix)
bool make_union(object_mapt &dest, const object_mapt &src) const
void apply_code(const codet &code, const namespacet &ns)
void do_end_function(const exprt &lhs, const namespacet &ns)
std::unordered_set< exprt, irep_hash > expr_sett
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
void dereference_rec(const exprt &src, exprt &dest) const
void set_from(const irep_idt &function, unsigned inx)
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
void add_var(const entryt &e)
void add_vars(const std::list< entryt > &vars)
bool insert_to(object_mapt &dest, const exprt &expr, const offsett &offset) const
entryt & get_entry(const entryt &e)
void output_entry(const entryt &e, const namespacet &ns, std::ostream &out) const
void copy_objects(object_mapt &dest, const object_mapt &src) const
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
void add_var(const idt &id)
bool insert_from(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
unsigned from_target_index
void set(object_mapt &dest, object_map_dt::const_iterator it) const
bool insert_to(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
bool insert_to(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
bool insert_from(object_mapt &dest, const exprt &src) const
void get_reference_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
void get_value_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
static object_numberingt object_numbering
bool offset_is_zero(offsett offset) const
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
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
entryt(const idt &_identifier, const std::string _suffix)