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 
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 
56  bool offset_is_zero(const offsett &offset) const
57  {
58  return offset && offset->is_zero();
59  }
60 
62  {
63  public:
65  static const object_map_dt blank;
66 
67  typedef std::map<object_numberingt::number_type, offsett> objmapt;
69 
70  // NOLINTNEXTLINE(readability/identifiers)
71  typedef objmapt::const_iterator const_iterator;
72  // NOLINTNEXTLINE(readability/identifiers)
73  typedef objmapt::iterator iterator;
74 
76  {
77  return objmap.find(k);
78  }
79  iterator begin() { return objmap.begin(); }
80  const_iterator begin() const { return objmap.begin(); }
81  iterator end() { return objmap.end(); }
82  const_iterator end() const { return objmap.end(); }
83  size_t size() const { return objmap.size(); }
84  bool empty() const { return objmap.empty(); }
85  void clear() { objmap.clear(); validity_ranges.clear(); }
86 
88  {
89  return objmap[k];
90  }
91 
92  // operator[] is the only way to insert something!
93  std::pair<iterator, bool>
94  insert(const std::pair<object_numberingt::number_type, offsett> &)
95  {
97  }
98  iterator
99  insert(iterator, const std::pair<object_numberingt::number_type, offsett> &)
100  {
101  UNREACHABLE;
102  }
103 
105  {
106  public:
107  unsigned function;
108  unsigned from, to;
109 
111  function(0), from(0), to(0)
112  {
113  }
114 
115  validity_ranget(unsigned fnc, unsigned f, unsigned t):
116  function(fnc), from(f), to(t)
117  {
118  }
119 
120  bool contains(unsigned f, unsigned line) const
121  {
122  return (function==f && from<=line && line<=to);
123  }
124  };
125 
126  typedef std::list<validity_ranget> vrange_listt;
127  typedef std::map<unsigned, vrange_listt> validity_rangest;
129 
130  bool set_valid_at(unsigned inx, unsigned f, unsigned line);
131  bool set_valid_at(unsigned inx, const validity_ranget &vr);
132  bool is_valid_at(unsigned inx, unsigned f, unsigned line) const;
133  };
134 
136 
138 
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  typedef std::unordered_set<idt> flatten_seent;
225  typedef std::unordered_set<idt> gvs_recursion_sett;
226  typedef std::unordered_set<idt> recfind_recursion_sett;
227  typedef std::unordered_set<idt> assign_recursion_sett;
228  #else
229  typedef std::unordered_map<idt, entryt, string_hash> valuest;
230  typedef std::unordered_set<idt, string_hash> flatten_seent;
231  typedef std::unordered_set<idt, string_hash> gvs_recursion_sett;
232  typedef std::unordered_set<idt, string_hash> recfind_recursion_sett;
233  typedef std::unordered_set<idt, string_hash> assign_recursion_sett;
234  #endif
235 
236  void get_value_set(
237  const exprt &expr,
238  std::list<exprt> &expr_set,
239  const namespacet &ns) const;
240 
241  expr_sett &get(
242  const idt &identifier,
243  const std::string &suffix);
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 
296 
297  // true = added something new
298  bool make_union(
299  object_mapt &dest,
300  const object_mapt &src) const;
301 
302  bool make_valid_union(
303  object_mapt &dest,
304  const object_mapt &src) const;
305 
306  void copy_objects(
307  object_mapt &dest,
308  const object_mapt &src) const;
309 
310  void apply_code(
311  const exprt &code,
312  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 
322  void do_function_call(
323  const irep_idt &function,
324  const exprt::operandst &arguments,
325  const namespacet &ns);
326 
327  // edge back to call site
328  void do_end_function(
329  const exprt &lhs,
330  const namespacet &ns);
331 
332  void get_reference_set(
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 
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,
349  gvs_recursion_sett &recursion_set) const;
350 
351  void get_value_set(
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 
369  void dereference_rec(
370  const exprt &src,
371  exprt &dest) const;
372 
373  void assign_rec(
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 
385  void flatten_rec(
386  const entryt&,
387  object_mapt&,
388  flatten_seent&,
389  unsigned from_function) const;
390 
391  bool recursive_find(
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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
value_set_fivrt::object_map_dt::validity_rangest
std::map< unsigned, vrange_listt > validity_rangest
Definition: value_set_fivr.h:127
value_set_fivrt::values
valuest values
Definition: value_set_fivr.h:294
value_set_fivrt::get_reference_set_sharing
void get_reference_set_sharing(const exprt &expr, object_mapt &dest, const namespacet &ns) const
Definition: value_set_fivr.h:356
value_set_fivrt::to_target_index
unsigned to_target_index
Definition: value_set_fivr.h:35
value_set_fivrt::object_map_dt::begin
const_iterator begin() const
Definition: value_set_fivr.h:80
mp_arith.h
value_set_fivrt::object_map_dt::set_valid_at
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
Definition: value_set_fivr.cpp:1658
value_set_fivrt::get
expr_sett & get(const idt &identifier, const std::string &suffix)
typet
The type of an expression, extends irept.
Definition: type.h:27
value_set_fivrt::recursive_find
bool recursive_find(const irep_idt &ident, const object_mapt &rhs, recfind_recursion_sett &recursion_set) const
Definition: value_set_fivr.cpp:1759
value_set_fivrt::object_map_dt::clear
void clear()
Definition: value_set_fivr.h:85
value_set_fivrt::do_end_function
void do_end_function(const exprt &lhs, const namespacet &ns)
Definition: value_set_fivr.cpp:1469
value_set_fivrt::entryt::entryt
entryt()
Definition: value_set_fivr.h:209
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
value_set_fivrt::make_union
bool make_union(object_mapt &dest, const object_mapt &src) const
Definition: value_set_fivr.cpp:363
template_numberingt
Definition: numbering.h:21
value_set_fivrt::set
void set(object_mapt &dest, object_map_dt::const_iterator it) const
Definition: value_set_fivr.h:139
value_set_fivrt::output
void output(const namespacet &ns, std::ostream &out) const
Definition: value_set_fivr.cpp:57
value_set_fivrt::get_reference_set_sharing_rec
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
Definition: value_set_fivr.cpp:877
value_set_fivrt::entryt::suffix
std::string suffix
Definition: value_set_fivr.h:207
value_set_fivrt::set_from
void set_from(const irep_idt &function, unsigned inx)
Definition: value_set_fivr.h:39
exprt
Base class for all expressions.
Definition: expr.h:54
object_numbering.h
invariant.h
value_set_fivrt::object_map_dt::end
const_iterator end() const
Definition: value_set_fivr.h:82
value_set_fivrt
Definition: value_set_fivr.h:27
value_set_fivrt::insert_from
bool insert_from(object_mapt &dest, const exprt &expr, const offsett &offset) const
Definition: value_set_fivr.h:198
value_set_fivrt::expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: value_set_fivr.h:218
namespace.h
value_set_fivrt::from_function
unsigned from_function
Definition: value_set_fivr.h:34
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
value_set_fivrt::object_map_dt::objmap
objmapt objmap
Definition: value_set_fivr.h:68
value_set_fivrt::object_map_dt::blank
static const object_map_dt blank
Definition: value_set_fivr.h:65
value_set_fivrt::clear
void clear()
Definition: value_set_fivr.h:245
value_set_fivrt::object_map_dt::validity_ranget::to
unsigned to
Definition: value_set_fivr.h:108
value_set_fivrt::idt
irep_idt idt
Definition: value_set_fivr.h:51
value_set_fivrt::object_map_dt::find
const_iterator find(object_numberingt::number_type k)
Definition: value_set_fivr.h:75
value_set_fivrt::get_entry
entryt & get_entry(const entryt &e)
Definition: value_set_fivr.h:265
template_numberingt::number
number_type number(const key_type &a)
Definition: numbering.h:37
value_set_fivrt::do_function_call
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Definition: value_set_fivr.cpp:1403
value_set_fivrt::temporary_values
valuest temporary_values
Definition: value_set_fivr.h:295
value_set_fivrt::object_map_dt::size
size_t size() const
Definition: value_set_fivr.h:83
value_set_fivrt::offset_is_zero
bool offset_is_zero(const offsett &offset) const
Definition: value_set_fivr.h:56
value_set_fivrt::get_reference_set_sharing
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
Definition: value_set_fivr.cpp:865
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
value_set_fivrt::assign
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
Definition: value_set_fivr.cpp:1070
value_set_fivrt::copy_objects
void copy_objects(object_mapt &dest, const object_mapt &src) const
Definition: value_set_fivr.cpp:393
value_set_fivrt::get_value_set
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
Definition: value_set_fivr.cpp:407
value_set_fivrt::object_map_dt::validity_ranget::function
unsigned function
Definition: value_set_fivr.h:107
value_set_fivrt::object_numbering
static object_numberingt object_numbering
Definition: value_set_fivr.h:36
value_set_fivrt::object_map_dt::validity_ranget::from
unsigned from
Definition: value_set_fivr.h:108
value_set_fivrt::object_map_dt::operator[]
offsett & operator[](object_numberingt::number_type k)
Definition: value_set_fivr.h:87
value_set_fivrt::to_function
unsigned to_function
Definition: value_set_fivr.h:34
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
value_set_fivrt::entryt::object_map
object_mapt object_map
Definition: value_set_fivr.h:205
value_set_fivrt::get_value_set_rec
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
Definition: value_set_fivr.cpp:482
value_set_fivrt::from_target_index
unsigned from_target_index
Definition: value_set_fivr.h:35
value_set_fivrt::valuest
std::unordered_map< idt, entryt, string_hash > valuest
Definition: value_set_fivr.h:229
value_set_fivrt::object_map_dt::validity_ranget::validity_ranget
validity_ranget(unsigned fnc, unsigned f, unsigned t)
Definition: value_set_fivr.h:115
value_set_fivrt::insert_from
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
Definition: value_set_fivr.h:173
value_set_fivrt::object_map_dt::empty
bool empty() const
Definition: value_set_fivr.h:84
value_set_fivrt::make_valid_union
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
Definition: value_set_fivr.cpp:378
value_set_fivrt::object_map_dt::validity_ranget::contains
bool contains(unsigned f, unsigned line) const
Definition: value_set_fivr.h:120
value_set_fivrt::insert_to
bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
Definition: value_set_fivr.h:144
value_set_fivrt::set_to
void set_to(const irep_idt &function, unsigned inx)
Definition: value_set_fivr.h:45
value_set_fivrt::apply_code
void apply_code(const exprt &code, const namespacet &ns)
Definition: value_set_fivr.cpp:1482
value_set_fivrt::assign_rec
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)
Definition: value_set_fivr.cpp:1227
value_set_fivrt::flatten
void flatten(const entryt &e, object_mapt &dest) const
Definition: value_set_fivr.cpp:215
value_set_fivrt::insert_from
bool insert_from(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
Definition: value_set_fivr.h:183
value_set_fivrt::insert_to
bool insert_to(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
Definition: value_set_fivr.h:154
reference_counting::write
T & write()
Definition: reference_counting.h:74
value_set_fivrt::entryt::entryt
entryt(const idt &_identifier, const std::string _suffix)
Definition: value_set_fivr.h:211
value_set_fivrt::object_map_dt::insert
iterator insert(iterator, const std::pair< object_numberingt::number_type, offsett > &)
Definition: value_set_fivr.h:99
value_set_fivrt::flatten_rec
void flatten_rec(const entryt &, object_mapt &, flatten_seent &, unsigned from_function) const
Definition: value_set_fivr.cpp:231
value_set_fivrt::object_mapt
reference_counting< object_map_dt > object_mapt
Definition: value_set_fivr.h:137
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
value_set_fivrt::insert_to
bool insert_to(object_mapt &dest, const exprt &expr, const offsett &offset) const
Definition: value_set_fivr.h:168
value_set_fivrt::object_map_dt::const_iterator
objmapt::const_iterator const_iterator
Definition: value_set_fivr.h:71
value_set_fivrt::add_vars
void add_vars(const std::list< entryt > &vars)
Definition: value_set_fivr.h:281
value_set_fivrt::entryt
Definition: value_set_fivr.h:203
value_set_fivrt::insert_from
bool insert_from(object_mapt &dest, const exprt &src) const
Definition: value_set_fivr.h:178
reference_counting< object_map_dt >
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
value_set_fivrt::get_entry
entryt & get_entry(const idt &id, const std::string &suffix)
Definition: value_set_fivr.h:260
value_set_fivrt::entryt::identifier
idt identifier
Definition: value_set_fivr.h:206
value_set_fivrt::to_expr
exprt to_expr(object_map_dt::const_iterator it) const
Definition: value_set_fivr.cpp:343
value_set_fivrt::value_set_fivrt
value_set_fivrt()
Definition: value_set_fivr.h:30
value_set_fivrt::object_map_dt::objmapt
std::map< object_numberingt::number_type, offsett > objmapt
Definition: value_set_fivr.h:67
value_set_fivrt::get_temporary_entry
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
Definition: value_set_fivr.h:275
template_numberingt::number_type
typename Map::mapped_type number_type
Definition: numbering.h:24
value_set_fivrt::gvs_recursion_sett
std::unordered_set< idt, string_hash > gvs_recursion_sett
Definition: value_set_fivr.h:231
value_set_fivrt::object_map_dt::validity_ranget::validity_ranget
validity_ranget()
Definition: value_set_fivr.h:110
value_set_fivrt::object_map_dt::insert
std::pair< iterator, bool > insert(const std::pair< object_numberingt::number_type, offsett > &)
Definition: value_set_fivr.h:94
value_set_fivrt::flatten_seent
std::unordered_set< idt, string_hash > flatten_seent
Definition: value_set_fivr.h:230
value_set_fivrt::dynamic_object_id_sett
std::unordered_set< unsigned int > dynamic_object_id_sett
Definition: value_set_fivr.h:220
reference_counting.h
value_set_fivrt::object_map_dt::vrange_listt
std::list< validity_ranget > vrange_listt
Definition: value_set_fivr.h:126
value_set_fivrt::object_map_dt::validity_ranget
Definition: value_set_fivr.h:104
value_set_fivrt::recfind_recursion_sett
std::unordered_set< idt, string_hash > recfind_recursion_sett
Definition: value_set_fivr.h:232
value_set_fivrt::offsett
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
Definition: value_set_fivr.h:55
value_set_fivrt::object_map_dt
Definition: value_set_fivr.h:61
r
static int8_t r
Definition: irep_hash.h:59
value_set_fivrt::object_map_dt::begin
iterator begin()
Definition: value_set_fivr.h:79
value_set_fivrt::add_var
void add_var(const idt &id, const std::string &suffix)
Definition: value_set_fivr.h:250
value_set_fivrt::insert_to
bool insert_to(object_mapt &dest, const exprt &src) const
Definition: value_set_fivr.h:149
value_set_fivrt::object_map_dt::is_valid_at
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
Definition: value_set_fivr.cpp:1729
value_set_fivrt::object_map_dt::validity_ranges
validity_rangest validity_ranges
Definition: value_set_fivr.h:128
value_set_fivrt::function_numbering
static hash_numbering< irep_idt, irep_id_hash > function_numbering
Definition: value_set_fivr.h:37
value_set_fivrt::assign_recursion_sett
std::unordered_set< idt, string_hash > assign_recursion_sett
Definition: value_set_fivr.h:233
value_set_fivrt::dereference_rec
void dereference_rec(const exprt &src, exprt &dest) const
Definition: value_set_fivr.cpp:799
value_set_fivrt::handover
bool handover()
Definition: value_set_fivr.cpp:1798
value_set_fivrt::object_map_dt::iterator
objmapt::iterator iterator
Definition: value_set_fivr.h:73
value_set_fivrt::object_map_dt::end
iterator end()
Definition: value_set_fivr.h:81
value_set_fivrt::object_map_dt::object_map_dt
object_map_dt()
Definition: value_set_fivr.h:64
value_set_fivrt::get_reference_set
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
Definition: value_set_fivr.cpp:817
value_set_fivrt::add_var
void add_var(const entryt &e)
Definition: value_set_fivr.h:255