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 #include <util/invariant.h>
25 
26 #include "object_numbering.h"
27 
29 {
30 public:
32  {
33  }
34 
39 
40  void set_from(const irep_idt &function, unsigned inx)
41  {
42  from_function = function_numbering.number(function);
43  from_target_index = inx;
44  }
45 
46  void set_to(const irep_idt &function, unsigned inx)
47  {
48  to_function = function_numbering.number(function);
49  to_target_index = inx;
50  }
51 
52  typedef irep_idt idt;
53 
57  bool offset_is_zero(offsett offset) const
58  {
59  return offset && offset->is_zero();
60  }
61 
63  {
64  public:
66  static const object_map_dt blank;
67 
68  typedef std::map<object_numberingt::number_type, offsett> objmapt;
70 
71  // NOLINTNEXTLINE(readability/identifiers)
72  typedef objmapt::const_iterator const_iterator;
73  // NOLINTNEXTLINE(readability/identifiers)
74  typedef objmapt::iterator iterator;
75 
77  {
78  return objmap.find(k);
79  }
80  iterator begin() { return objmap.begin(); }
81  const_iterator begin() const { return objmap.begin(); }
82  iterator end() { return objmap.end(); }
83  const_iterator end() const { return objmap.end(); }
84  size_t size() const { return objmap.size(); }
85  bool empty() const { return objmap.empty(); }
86  void clear() { objmap.clear(); validity_ranges.clear(); }
87 
89  {
90  return objmap[k];
91  }
92 
93  // operator[] is the only way to insert something!
94  std::pair<iterator, bool>
95  insert(const std::pair<object_numberingt::number_type, offsett> &)
96  {
98  }
99  iterator
100  insert(iterator, const std::pair<object_numberingt::number_type, offsett> &)
101  {
102  UNREACHABLE;
103  }
104 
106  {
107  public:
108  unsigned function;
109  unsigned from, to;
110 
112  function(0), from(0), to(0)
113  {
114  }
115 
116  validity_ranget(unsigned fnc, unsigned f, unsigned t):
117  function(fnc), from(f), to(t)
118  {
119  }
120 
121  bool contains(unsigned f, unsigned line) const
122  {
123  return (function==f && from<=line && line<=to);
124  }
125  };
126 
127  typedef std::list<validity_ranget> vrange_listt;
128  typedef std::map<unsigned, vrange_listt> validity_rangest;
130 
131  bool set_valid_at(unsigned inx, unsigned f, unsigned line);
132  bool is_valid_at(unsigned inx, unsigned f, unsigned line) const;
133  };
134 
136 
138 
139  void set(object_mapt &dest, object_map_dt::const_iterator it) const
140  {
141  dest.write()[it->first]=it->second;
142  }
143 
145  {
146  return insert_to(dest, it->first, it->second);
147  }
148 
149  bool insert_to(object_mapt &dest, const exprt &src) const
150  {
151  return insert_to(dest, object_numbering.number(src), offsett());
152  }
153 
154  bool insert_to(
155  object_mapt &dest,
156  const exprt &src,
157  const mp_integer &offset_value) const
158  {
159  return insert_to(dest, object_numbering.number(src), offsett(offset_value));
160  }
161 
162  bool insert_to(
163  object_mapt &dest,
165  const offsett &offset) const;
166 
167  bool
168  insert_to(object_mapt &dest, const exprt &expr, const offsett &offset) const
169  {
170  return insert_to(dest, object_numbering.number(expr), offset);
171  }
172 
174  {
175  return insert_from(dest, it->first, it->second);
176  }
177 
178  bool insert_from(object_mapt &dest, const exprt &src) const
179  {
180  return insert_from(dest, object_numbering.number(src), offsett());
181  }
182 
184  object_mapt &dest,
185  const exprt &src,
186  const mp_integer &offset_value) const
187  {
188  return insert_from(
189  dest, object_numbering.number(src), offsett(offset_value));
190  }
191 
192  bool insert_from(
193  object_mapt &dest,
195  const offsett &offset) const;
196 
197  bool
198  insert_from(object_mapt &dest, const exprt &expr, const offsett &offset) const
199  {
200  return insert_from(dest, object_numbering.number(expr), offset);
201  }
202 
203  struct entryt
204  {
207  std::string suffix;
208 
209  entryt() { }
210 
211  entryt(const idt &_identifier, const std::string _suffix):
212  identifier(_identifier),
213  suffix(_suffix)
214  {
215  }
216  };
217 
218  typedef std::unordered_set<exprt, irep_hash> expr_sett;
219 
220  typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
221 
222  #ifdef USE_DSTRING
223  typedef std::map<idt, entryt> valuest;
224  #else
225  typedef std::unordered_map<idt, entryt, string_hash> valuest;
226  #endif
227 
228  void get_value_set(
229  const exprt &expr,
230  std::list<exprt> &expr_set,
231  const namespacet &ns) const;
232 
233  expr_sett &get(
234  const idt &identifier,
235  const std::string &suffix);
236 
237  void make_any()
238  {
239  values.clear();
240  }
241 
242  void clear()
243  {
244  values.clear();
245  }
246 
247  void add_var(const idt &id, const std::string &suffix)
248  {
249  get_entry(id, suffix);
250  }
251 
252  void add_var(const entryt &e)
253  {
255  }
256 
257  entryt &get_entry(const idt &id, const std::string &suffix)
258  {
259  return get_entry(entryt(id, suffix));
260  }
261 
263  {
264  std::string index=id2string(e.identifier)+e.suffix;
265 
266  std::pair<valuest::iterator, bool> r=
267  values.insert(std::pair<idt, entryt>(index, e));
268 
269  return r.first->second;
270  }
271 
272  entryt &get_temporary_entry(const idt &id, const std::string &suffix)
273  {
274  std::string index=id2string(id)+suffix;
275  return temporary_values[index];
276  }
277 
278  void add_vars(const std::list<entryt> &vars)
279  {
280  for(std::list<entryt>::const_iterator
281  it=vars.begin();
282  it!=vars.end();
283  it++)
284  add_var(*it);
285  }
286 
287  void output(
288  const namespacet &ns,
289  std::ostream &out) const;
290 
291  void output_entry(
292  const entryt &e,
293  const namespacet &ns,
294  std::ostream &out) const;
295 
298 
299  // true = added something new
300  bool make_union(
301  object_mapt &dest,
302  const object_mapt &src) const;
303 
304  bool make_valid_union(
305  object_mapt &dest,
306  const object_mapt &src) const;
307 
308  void copy_objects(
309  object_mapt &dest,
310  const object_mapt &src) const;
311 
312  void apply_code(
313  const exprt &code,
314  const namespacet &ns);
315 
316  bool handover();
317 
318  void assign(
319  const exprt &lhs,
320  const exprt &rhs,
321  const namespacet &ns,
322  bool add_to_sets=false);
323 
324  void do_function_call(
325  const irep_idt &function,
326  const exprt::operandst &arguments,
327  const namespacet &ns);
328 
329  // edge back to call site
330  void do_end_function(
331  const exprt &lhs,
332  const namespacet &ns);
333 
334  void get_reference_set(
335  const exprt &expr,
336  expr_sett &expr_set,
337  const namespacet &ns) const;
338 
339 protected:
340  void get_value_set_rec(
341  const exprt &expr,
342  object_mapt &dest,
343  const std::string &suffix,
344  const typet &original_type,
345  const namespacet &ns) const;
346 
347  void get_value_set(
348  const exprt &expr,
349  object_mapt &dest,
350  const namespacet &ns) const;
351 
353  const exprt &expr,
354  object_mapt &dest,
355  const namespacet &ns) const
356  {
357  get_reference_set_rec(expr, dest, ns);
358  }
359 
361  const exprt &expr,
362  object_mapt &dest,
363  const namespacet &ns) const;
364 
365  void dereference_rec(
366  const exprt &src,
367  exprt &dest) const;
368 
369  void assign_rec(
370  const exprt &lhs,
371  const object_mapt &values_rhs,
372  const std::string &suffix,
373  const namespacet &ns,
374  bool add_to_sets);
375 
376  void do_free(
377  const exprt &op,
378  const namespacet &ns);
379 };
380 
381 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVRNS_H
bool contains(unsigned f, unsigned line) const
The type of an expression.
Definition: type.h:22
static int8_t r
Definition: irep_hash.h:59
bool insert_to(object_mapt &dest, const exprt &src) const
bool insert_from(object_mapt &dest, const exprt &expr, const offsett &offset) const
BigInt mp_integer
Definition: mp_arith.h:22
reference_counting< object_map_dt > object_mapt
number_type number(const key_type &a)
Definition: numbering.h:37
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
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
void apply_code(const exprt &code, const namespacet &ns)
const_iterator find(object_numberingt::number_type k)
void copy_objects(object_mapt &dest, const object_mapt &src) const
static const object_map_dt blank
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value...
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 &src, const mp_integer &offset_value) 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 offset_is_zero(offsett offset) 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
void output_entry(const entryt &e, const namespacet &ns, std::ostream &out) const
void do_end_function(const exprt &lhs, const namespacet &ns)
nonstd::optional< T > optionalt
Definition: optional.h:35
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:74
bool insert_from(object_mapt &dest, const exprt &src) const
void add_var(const entryt &e)
offsett & operator[](object_numberingt::number_type k)
exprt to_expr(object_map_dt::const_iterator it) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
typename Map::mapped_type number_type
Definition: numbering.h:24
objmapt::const_iterator const_iterator
std::map< object_numberingt::number_type, offsett > objmapt
void add_var(const idt &id, const std::string &suffix)
std::vector< exprt > operandst
Definition: expr.h:45
std::unordered_map< idt, entryt, string_hash > valuest
void add_vars(const std::list< entryt > &vars)
std::list< validity_ranget > vrange_listt
validity_ranget(unsigned fnc, unsigned f, unsigned t)
iterator insert(iterator, const std::pair< object_numberingt::number_type, offsett > &)
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
bool insert_to(object_mapt &dest, const exprt &expr, const offsett &offset) 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:42
Reference Counting.
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
#define UNREACHABLE
Definition: invariant.h:271
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
bool insert_to(object_mapt &dest, const exprt &src, const mp_integer &offset_value) 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)
std::pair< iterator, bool > insert(const std::pair< object_numberingt::number_type, offsett > &)
unsigned from_target_index
void set_from(const irep_idt &function, unsigned inx)