cprover
value_set_fivr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set (Flow Insensitive, Sharing, Validity Regions)
4 
5 Author: 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 
24 #include "object_numbering.h"
25 
27 {
28 public:
30  {
31  }
32 
37 
38  void set_from(const irep_idt &function, unsigned inx)
39  {
40  from_function = function_numbering.number(function);
41  from_target_index = inx;
42  }
43 
44  void set_to(const irep_idt &function, unsigned inx)
45  {
46  to_function = function_numbering.number(function);
47  to_target_index = inx;
48  }
49 
50  typedef irep_idt idt;
51 
52  class objectt
53  {
54  public:
55  objectt() :
56  offset_is_set(false)
57  {
58  }
59 
60  explicit objectt(const mp_integer &_offset):
61  offset(_offset),
62  offset_is_set(true)
63  {
64  }
65 
68  bool offset_is_zero() const
69  { return offset_is_set && offset.is_zero(); }
70  };
71 
73  {
74  public:
76  static const object_map_dt blank;
77 
78  typedef std::map<unsigned, objectt> objmapt;
79  objmapt objmap;
80 
81  // NOLINTNEXTLINE(readability/identifiers)
82  typedef objmapt::const_iterator const_iterator;
83  // NOLINTNEXTLINE(readability/identifiers)
84  typedef objmapt::iterator iterator;
85 
86  const_iterator find(unsigned k) { return objmap.find(k); }
87  iterator begin() { return objmap.begin(); }
88  const_iterator begin() const { return objmap.begin(); }
89  iterator end() { return objmap.end(); }
90  const_iterator end() const { return objmap.end(); }
91  size_t size() const { return objmap.size(); }
92  bool empty() const { return objmap.empty(); }
93  void clear() { objmap.clear(); validity_ranges.clear(); }
94 
95  objectt &operator[](unsigned k)
96  {
97  return objmap[k];
98  }
99 
100  // operator[] is the only way to insert something!
101  std::pair<iterator, bool> insert(const std::pair<unsigned, objectt>&)
102  {
103  assert(false);
104  }
105  iterator insert(iterator, const std::pair<unsigned, objectt>&)
106  {
107  assert(false);
108  }
109 
111  {
112  public:
113  unsigned function;
114  unsigned from, to;
115 
117  function(0), from(0), to(0)
118  {
119  }
120 
121  validity_ranget(unsigned fnc, unsigned f, unsigned t):
122  function(fnc), from(f), to(t)
123  {
124  }
125 
126  bool contains(unsigned f, unsigned line) const
127  {
128  return (function==f && from<=line && line<=to);
129  }
130  };
131 
132  typedef std::list<validity_ranget> vrange_listt;
133  typedef std::map<unsigned, vrange_listt> validity_rangest;
134  validity_rangest validity_ranges;
135 
136  bool set_valid_at(unsigned inx, unsigned f, unsigned line);
137  bool set_valid_at(unsigned inx, const validity_ranget &vr);
138  bool is_valid_at(unsigned inx, unsigned f, unsigned line) const;
139  };
140 
142 
144 
145  void set(object_mapt &dest, object_map_dt::const_iterator it) const
146  {
147  dest.write()[it->first]=it->second;
148  }
149 
150  bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
151  {
152  return insert_to(dest, it->first, it->second);
153  }
154 
155  bool insert_to(object_mapt &dest, const exprt &src) const
156  {
157  return insert_to(dest, object_numbering.number(src), objectt());
158  }
159 
160  bool insert_to(
161  object_mapt &dest,
162  const exprt &src,
163  const mp_integer &offset) const
164  {
165  return insert_to(dest, object_numbering.number(src), objectt(offset));
166  }
167 
168  bool insert_to(object_mapt &dest, unsigned n, const objectt &object) const;
169 
170  bool insert_to(
171  object_mapt &dest,
172  const exprt &expr,
173  const objectt &object) const
174  {
175  return insert_to(dest, object_numbering.number(expr), object);
176  }
177 
178  bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
179  {
180  return insert_from(dest, it->first, it->second);
181  }
182 
183  bool insert_from(object_mapt &dest, const exprt &src) const
184  {
185  return insert_from(dest, object_numbering.number(src), objectt());
186  }
187 
189  object_mapt &dest,
190  const exprt &src,
191  const mp_integer &offset) const
192  {
193  return insert_from(dest, object_numbering.number(src), objectt(offset));
194  }
195 
196  bool insert_from(object_mapt &dest, unsigned n, const objectt &object) const;
197 
199  object_mapt &dest,
200  const exprt &expr,
201  const objectt &object) const
202  {
203  return insert_from(dest, object_numbering.number(expr), object);
204  }
205 
206  struct entryt
207  {
208  object_mapt object_map;
210  std::string suffix;
211 
212  entryt() { }
213 
214  entryt(const idt &_identifier, const std::string _suffix):
215  identifier(_identifier),
216  suffix(_suffix)
217  {
218  }
219  };
220 
221  typedef std::unordered_set<exprt, irep_hash> expr_sett;
222 
223  typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
224 
225  #ifdef USE_DSTRING
226  typedef std::map<idt, entryt> valuest;
227  typedef std::unordered_set<idt, irep_id_hash> flatten_seent;
228  typedef std::unordered_set<idt, irep_id_hash> gvs_recursion_sett;
229  typedef std::unordered_set<idt, irep_id_hash> recfind_recursion_sett;
230  typedef std::unordered_set<idt, irep_id_hash> assign_recursion_sett;
231  #else
232  typedef std::unordered_map<idt, entryt, string_hash> valuest;
233  typedef std::unordered_set<idt, string_hash> flatten_seent;
234  typedef std::unordered_set<idt, string_hash> gvs_recursion_sett;
235  typedef std::unordered_set<idt, string_hash> recfind_recursion_sett;
236  typedef std::unordered_set<idt, string_hash> assign_recursion_sett;
237  #endif
238 
239  void get_value_set(
240  const exprt &expr,
241  std::list<exprt> &expr_set,
242  const namespacet &ns) const;
243 
244  expr_sett &get(
245  const idt &identifier,
246  const std::string &suffix);
247 
248  void make_any()
249  {
250  values.clear();
251  }
252 
253  void clear()
254  {
255  values.clear();
256  }
257 
258  void add_var(const idt &id, const std::string &suffix)
259  {
260  get_entry(id, suffix);
261  }
262 
263  void add_var(const entryt &e)
264  {
266  }
267 
268  entryt &get_entry(const idt &id, const std::string &suffix)
269  {
270  return get_entry(entryt(id, suffix));
271  }
272 
274  {
275  std::string index=id2string(e.identifier)+e.suffix;
276 
277  std::pair<valuest::iterator, bool> r=
278  values.insert(std::pair<idt, entryt>(index, e));
279 
280  return r.first->second;
281  }
282 
283  entryt &get_temporary_entry(const idt &id, const std::string &suffix)
284  {
285  std::string index=id2string(id)+suffix;
286  return temporary_values[index];
287  }
288 
289  void add_vars(const std::list<entryt> &vars)
290  {
291  for(std::list<entryt>::const_iterator
292  it=vars.begin();
293  it!=vars.end();
294  it++)
295  add_var(*it);
296  }
297 
298  void output(
299  const namespacet &ns,
300  std::ostream &out) const;
301 
302  valuest values;
304 
305  // true = added something new
306  bool make_union(
307  object_mapt &dest,
308  const object_mapt &src) const;
309 
310  bool make_valid_union(
311  object_mapt &dest,
312  const object_mapt &src) const;
313 
314  void copy_objects(
315  object_mapt &dest,
316  const object_mapt &src) const;
317 
318  void apply_code(
319  const exprt &code,
320  const namespacet &ns);
321 
322  bool handover();
323 
324  void assign(
325  const exprt &lhs,
326  const exprt &rhs,
327  const namespacet &ns,
328  bool add_to_sets=false);
329 
330  void do_function_call(
331  const irep_idt &function,
332  const exprt::operandst &arguments,
333  const namespacet &ns);
334 
335  // edge back to call site
336  void do_end_function(
337  const exprt &lhs,
338  const namespacet &ns);
339 
340  void get_reference_set(
341  const exprt &expr,
342  expr_sett &expr_set,
343  const namespacet &ns) const;
344 
345 protected:
347  const exprt &expr,
348  expr_sett &expr_set,
349  const namespacet &ns) const;
350 
351  void get_value_set_rec(
352  const exprt &expr,
353  object_mapt &dest,
354  const std::string &suffix,
355  const typet &original_type,
356  const namespacet &ns,
357  gvs_recursion_sett &recursion_set) const;
358 
359  void get_value_set(
360  const exprt &expr,
361  object_mapt &dest,
362  const namespacet &ns) const;
363 
365  const exprt &expr,
366  object_mapt &dest,
367  const namespacet &ns) const
368  {
369  get_reference_set_sharing_rec(expr, dest, ns);
370  }
371 
373  const exprt &expr,
374  object_mapt &dest,
375  const namespacet &ns) const;
376 
377  void dereference_rec(
378  const exprt &src,
379  exprt &dest) const;
380 
381  void assign_rec(
382  const exprt &lhs,
383  const object_mapt &values_rhs,
384  const std::string &suffix,
385  const namespacet &ns,
386  assign_recursion_sett &recursion_set,
387  bool add_to_sets);
388 
389  void do_free(
390  const exprt &op,
391  const namespacet &ns);
392 
393  void flatten(
394  const entryt &e,
395  object_mapt &dest) const;
396 
397  void flatten_rec(
398  const entryt&,
399  object_mapt&,
400  flatten_seent&,
401  unsigned from_function,
402  unsigned from_index) const;
403 
404  bool recursive_find(
405  const irep_idt &ident,
406  const object_mapt &rhs,
407  recfind_recursion_sett &recursion_set) const;
408 };
409 
410 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVR_H
The type of an expression.
Definition: type.h:20
std::pair< iterator, bool > insert(const std::pair< unsigned, objectt > &)
void get_reference_set_sharing(const exprt &expr, object_mapt &dest, const namespacet &ns) const
bool insert_to(object_mapt &dest, const exprt &src, const mp_integer &offset) const
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
static int8_t r
Definition: irep_hash.h:59
BigInt mp_integer
Definition: mp_arith.h:19
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void dereference_rec(const exprt &src, exprt &dest) const
void do_end_function(const exprt &lhs, const namespacet &ns)
const_iterator end() const
void add_var(const entryt &e)
unsigned from_function
void set_from(const irep_idt &function, unsigned inx)
bool recursive_find(const irep_idt &ident, const object_mapt &rhs, recfind_recursion_sett &recursion_set) const
objectt(const mp_integer &_offset)
unsigned to_target_index
bool make_union(object_mapt &dest, const object_mapt &src) const
void copy_objects(object_mapt &dest, const object_mapt &src) const
void output(const namespacet &ns, std::ostream &out) const
std::map< unsigned, objectt > objmapt
objectt & operator[](unsigned k)
std::unordered_set< exprt, irep_hash > expr_sett
unsigned to_function
unsigned from_target_index
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
bool insert_from(object_mapt &dest, const exprt &expr, const objectt &object) const
void set_to(const irep_idt &function, unsigned inx)
validity_ranget(unsigned fnc, unsigned f, unsigned t)
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
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &, unsigned from_function, unsigned from_index) const
bool insert_from(object_mapt &dest, const exprt &src) const
void apply_code(const exprt &code, const namespacet &ns)
entryt & get_entry(const entryt &e)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::list< validity_ranget > vrange_listt
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
valuest temporary_values
std::unordered_map< idt, entryt, string_hash > valuest
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
std::unordered_set< idt, string_hash > gvs_recursion_sett
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
void add_vars(const std::list< entryt > &vars)
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
entryt & get_entry(const idt &id, const std::string &suffix)
static object_numberingt object_numbering
void flatten(const entryt &e, object_mapt &dest) const
static const object_map_dt blank
std::unordered_set< unsigned int > dynamic_object_id_sett
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
std::vector< exprt > operandst
Definition: expr.h:49
bool insert_from(object_mapt &dest, const exprt &src, const mp_integer &offset) const
exprt to_expr(object_map_dt::const_iterator it) const
objmapt::const_iterator const_iterator
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)
bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
reference_counting< object_map_dt > object_mapt
Base class for all expressions.
Definition: expr.h:46
Reference Counting.
static hash_numbering< irep_idt, irep_id_hash > function_numbering
std::unordered_set< idt, string_hash > flatten_seent
std::map< unsigned, vrange_listt > validity_rangest
entryt(const idt &_identifier, const std::string _suffix)
const_iterator begin() const
void add_var(const idt &id, const std::string &suffix)
std::unordered_set< idt, string_hash > assign_recursion_sett
bool contains(unsigned f, unsigned line) const
void do_free(const exprt &op, const namespacet &ns)
number_type number(const T &a)
Definition: numbering.h:80
iterator insert(iterator, const std::pair< unsigned, objectt > &)
std::unordered_set< idt, string_hash > recfind_recursion_sett
bool insert_to(object_mapt &dest, const exprt &src) const
bool insert_to(object_mapt &dest, const exprt &expr, const objectt &object) const
const_iterator find(unsigned k)