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 #include <util/invariant.h>
24 
25 #include "object_numbering.h"
26 
27 class codet;
28 
30 {
31 public:
33  {
34  }
35 
40 
41  void set_from(const irep_idt &function, unsigned inx)
42  {
44  from_target_index = inx;
45  }
46 
47  void set_to(const irep_idt &function, unsigned inx)
48  {
50  to_target_index = inx;
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 
78  {
79  return objmap.find(k);
80  }
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(); }
87  void clear() { objmap.clear(); validity_ranges.clear(); }
88 
90  {
91  return objmap[k];
92  }
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  }
100  iterator
101  insert(iterator, const std::pair<object_numberingt::number_type, offsett> &)
102  {
103  UNREACHABLE;
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 
156  bool insert_to(
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 
164  bool insert_to(
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  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
301  object_mapt &dest,
302  const object_mapt &src) const;
303 
305  object_mapt &dest,
306  const object_mapt &src) const;
307 
309  object_mapt &dest,
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 
337 protected:
339  const exprt &expr,
340  expr_sett &expr_set,
341  const namespacet &ns) const;
342 
344  const exprt &expr,
345  object_mapt &dest,
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,
353  object_mapt &dest,
354  const namespacet &ns) const;
355 
357  const exprt &expr,
358  object_mapt &dest,
359  const namespacet &ns) const
360  {
361  get_reference_set_sharing_rec(expr, dest, ns);
362  }
363 
365  const exprt &expr,
366  object_mapt &dest,
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 
381  void flatten(
382  const entryt &e,
383  object_mapt &dest) const;
384 
386  const entryt&,
387  object_mapt&,
388  flatten_seent&,
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
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
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:28
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
offsett & operator[](object_numberingt::number_type k)
std::map< unsigned, vrange_listt > validity_rangest
const_iterator find(object_numberingt::number_type k)
std::pair< iterator, bool > insert(const std::pair< object_numberingt::number_type, offsett > &)
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
std::map< object_numberingt::number_type, offsett > objmapt
static const object_map_dt blank
std::list< validity_ranget > vrange_listt
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
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)
unsigned to_function
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
valuest temporary_values
void get_value_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
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
bool insert_to(object_mapt &dest, const exprt &src) const
std::unordered_set< idt, string_hash > assign_recursion_sett
entryt & get_entry(const idt &id, const std::string &suffix)
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
entryt & get_entry(const entryt &e)
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)
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
expr_sett & get(const idt &identifier, const std::string &suffix)
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:49
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)