cprover
value_set_fivrns.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set (Flow Insensitive, Validity Regions)
4 
5 Author: 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 
25 #include "object_numbering.h"
26 
28 {
29 public:
31  {
32  }
33 
38 
39  void set_from(const irep_idt &function, unsigned inx)
40  {
41  from_function = function_numbering.number(function);
42  from_target_index = inx;
43  }
44 
45  void set_to(const irep_idt &function, unsigned inx)
46  {
47  to_function = function_numbering.number(function);
48  to_target_index = inx;
49  }
50 
51  typedef irep_idt idt;
52 
53  class objectt
54  {
55  public:
56  objectt() :
57  offset_is_set(false)
58  {
59  }
60 
61  explicit objectt(const mp_integer &_offset):
62  offset(_offset),
63  offset_is_set(true)
64  {
65  }
66 
69  bool offset_is_zero() const
70  { return offset_is_set && offset.is_zero(); }
71  };
72 
74  {
75  public:
77  static const object_map_dt blank;
78 
79  typedef std::map<unsigned, objectt> objmapt;
80  objmapt objmap;
81 
82  // NOLINTNEXTLINE(readability/identifiers)
83  typedef objmapt::const_iterator const_iterator;
84  // NOLINTNEXTLINE(readability/identifiers)
85  typedef objmapt::iterator iterator;
86 
87  const_iterator find(unsigned k) { return objmap.find(k); }
88  iterator begin() { return objmap.begin(); }
89  const_iterator begin() const { return objmap.begin(); }
90  iterator end() { return objmap.end(); }
91  const_iterator end() const { return objmap.end(); }
92  size_t size() const { return objmap.size(); }
93  bool empty() const { return objmap.empty(); }
94  void clear() { objmap.clear(); validity_ranges.clear(); }
95 
96  objectt &operator[](unsigned k)
97  {
98  return objmap[k];
99  }
100 
101  // operator[] is the only way to insert something!
102  std::pair<iterator, bool> insert(const std::pair<unsigned, objectt>&)
103  {
104  assert(false);
105  }
106  iterator insert(iterator, const std::pair<unsigned, objectt>&)
107  {
108  assert(false);
109  }
110 
112  {
113  public:
114  unsigned function;
115  unsigned from, to;
116 
118  function(0), from(0), to(0)
119  {
120  }
121 
122  validity_ranget(unsigned fnc, unsigned f, unsigned t):
123  function(fnc), from(f), to(t)
124  {
125  }
126 
127  bool contains(unsigned f, unsigned line) const
128  {
129  return (function==f && from<=line && line<=to);
130  }
131  };
132 
133  typedef std::list<validity_ranget> vrange_listt;
134  typedef std::map<unsigned, vrange_listt> validity_rangest;
135  validity_rangest validity_ranges;
136 
137  bool set_valid_at(unsigned inx, unsigned f, unsigned line);
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  #else
228  typedef std::unordered_map<idt, entryt, string_hash> valuest;
229  #endif
230 
231  void get_value_set(
232  const exprt &expr,
233  std::list<exprt> &expr_set,
234  const namespacet &ns) const;
235 
236  expr_sett &get(
237  const idt &identifier,
238  const std::string &suffix);
239 
240  void make_any()
241  {
242  values.clear();
243  }
244 
245  void clear()
246  {
247  values.clear();
248  }
249 
250  void add_var(const idt &id, const std::string &suffix)
251  {
252  get_entry(id, suffix);
253  }
254 
255  void add_var(const entryt &e)
256  {
258  }
259 
260  entryt &get_entry(const idt &id, const std::string &suffix)
261  {
262  return get_entry(entryt(id, suffix));
263  }
264 
266  {
267  std::string index=id2string(e.identifier)+e.suffix;
268 
269  std::pair<valuest::iterator, bool> r=
270  values.insert(std::pair<idt, entryt>(index, e));
271 
272  return r.first->second;
273  }
274 
275  entryt &get_temporary_entry(const idt &id, const std::string &suffix)
276  {
277  std::string index=id2string(id)+suffix;
278  return temporary_values[index];
279  }
280 
281  void add_vars(const std::list<entryt> &vars)
282  {
283  for(std::list<entryt>::const_iterator
284  it=vars.begin();
285  it!=vars.end();
286  it++)
287  add_var(*it);
288  }
289 
290  void output(
291  const namespacet &ns,
292  std::ostream &out) const;
293 
294  void output_entry(
295  const entryt &e,
296  const namespacet &ns,
297  std::ostream &out) const;
298 
299  valuest values;
301 
302  // true = added something new
303  bool make_union(
304  object_mapt &dest,
305  const object_mapt &src) const;
306 
307  bool make_valid_union(
308  object_mapt &dest,
309  const object_mapt &src) const;
310 
311  void copy_objects(
312  object_mapt &dest,
313  const object_mapt &src) const;
314 
315  void apply_code(
316  const exprt &code,
317  const namespacet &ns);
318 
319  bool handover();
320 
321  void assign(
322  const exprt &lhs,
323  const exprt &rhs,
324  const namespacet &ns,
325  bool add_to_sets=false);
326 
327  void do_function_call(
328  const irep_idt &function,
329  const exprt::operandst &arguments,
330  const namespacet &ns);
331 
332  // edge back to call site
333  void do_end_function(
334  const exprt &lhs,
335  const namespacet &ns);
336 
337  void get_reference_set(
338  const exprt &expr,
339  expr_sett &expr_set,
340  const namespacet &ns) const;
341 
342 protected:
343  void get_value_set_rec(
344  const exprt &expr,
345  object_mapt &dest,
346  const std::string &suffix,
347  const typet &original_type,
348  const namespacet &ns) const;
349 
350  void get_value_set(
351  const exprt &expr,
352  object_mapt &dest,
353  const namespacet &ns) const;
354 
356  const exprt &expr,
357  object_mapt &dest,
358  const namespacet &ns) const
359  {
360  get_reference_set_rec(expr, dest, ns);
361  }
362 
364  const exprt &expr,
365  object_mapt &dest,
366  const namespacet &ns) const;
367 
368  void dereference_rec(
369  const exprt &src,
370  exprt &dest) const;
371 
372  void assign_rec(
373  const exprt &lhs,
374  const object_mapt &values_rhs,
375  const std::string &suffix,
376  const namespacet &ns,
377  bool add_to_sets);
378 
379  void do_free(
380  const exprt &op,
381  const namespacet &ns);
382 };
383 
384 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVRNS_H
bool contains(unsigned f, unsigned line) const
The type of an expression.
Definition: type.h:20
static int8_t r
Definition: irep_hash.h:59
bool insert_to(object_mapt &dest, const exprt &src) const
BigInt mp_integer
Definition: mp_arith.h:19
reference_counting< object_map_dt > object_mapt
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
static object_numberingt object_numbering
void output(const namespacet &ns, std::ostream &out) const
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
std::pair< iterator, bool > insert(const std::pair< unsigned, objectt > &)
std::map< unsigned, objectt > objmapt
objectt(const mp_integer &_offset)
void apply_code(const exprt &code, const namespacet &ns)
void copy_objects(object_mapt &dest, const object_mapt &src) const
static const object_map_dt blank
void dereference_rec(const exprt &src, exprt &dest) const
void set_to(const irep_idt &function, unsigned inx)
bool insert_from(object_mapt &dest, const exprt &expr, const objectt &object) const
entryt & get_entry(const entryt &e)
void do_free(const exprt &op, const namespacet &ns)
bool make_union(object_mapt &dest, const object_mapt &src) const
bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
std::map< unsigned, vrange_listt > validity_rangest
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
bool insert_to(object_mapt &dest, const exprt &src, const mp_integer &offset) const
void output_entry(const entryt &e, const namespacet &ns, std::ostream &out) const
void do_end_function(const exprt &lhs, const namespacet &ns)
entryt & get_entry(const idt &id, const std::string &suffix)
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bool insert_from(object_mapt &dest, const exprt &src) const
void add_var(const entryt &e)
bool insert_to(object_mapt &dest, const exprt &expr, const objectt &object) const
exprt to_expr(object_map_dt::const_iterator it) const
objmapt::const_iterator const_iterator
iterator insert(iterator, const std::pair< unsigned, objectt > &)
void add_var(const idt &id, const std::string &suffix)
std::vector< exprt > operandst
Definition: expr.h:49
std::unordered_map< idt, entryt, string_hash > valuest
void add_vars(const std::list< entryt > &vars)
objectt & operator[](unsigned k)
std::list< validity_ranget > vrange_listt
validity_ranget(unsigned fnc, unsigned f, unsigned t)
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
static hash_numbering< irep_idt, irep_id_hash > function_numbering
void get_reference_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
const_iterator begin() const
std::unordered_set< exprt, irep_hash > expr_sett
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
entryt(const idt &_identifier, const std::string _suffix)
Base class for all expressions.
Definition: expr.h:46
Reference Counting.
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
std::unordered_set< unsigned int > dynamic_object_id_sett
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
const_iterator find(unsigned k)
number_type number(const T &a)
Definition: numbering.h:80
bool insert_from(object_mapt &dest, const exprt &src, const mp_integer &offset) const
unsigned from_target_index
void set_from(const irep_idt &function, unsigned inx)