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 
28 class codet;
29 
31 {
32 public:
34  {
35  }
36 
41 
42  void set_from(const irep_idt &function, unsigned inx)
43  {
44  from_function = function_numbering.number(function);
45  from_target_index = inx;
46  }
47 
48  void set_to(const irep_idt &function, unsigned inx)
49  {
50  to_function = function_numbering.number(function);
51  to_target_index = inx;
52  }
53 
54  typedef irep_idt idt;
55 
59  bool offset_is_zero(offsett offset) const
60  {
61  return offset && offset->is_zero();
62  }
63 
65  {
66  public:
68  static const object_map_dt blank;
69 
70  typedef std::map<object_numberingt::number_type, offsett> objmapt;
72 
73  // NOLINTNEXTLINE(readability/identifiers)
74  typedef objmapt::const_iterator const_iterator;
75  // NOLINTNEXTLINE(readability/identifiers)
76  typedef objmapt::iterator iterator;
77 
79  {
80  return objmap.find(k);
81  }
82  iterator begin() { return objmap.begin(); }
83  const_iterator begin() const { return objmap.begin(); }
84  iterator end() { return objmap.end(); }
85  const_iterator end() const { return objmap.end(); }
86  size_t size() const { return objmap.size(); }
87  bool empty() const { return objmap.empty(); }
88  void clear() { objmap.clear(); validity_ranges.clear(); }
89 
91  {
92  return objmap[k];
93  }
94 
95  // operator[] is the only way to insert something!
96  std::pair<iterator, bool>
97  insert(const std::pair<object_numberingt::number_type, offsett> &)
98  {
100  }
101  iterator
102  insert(iterator, const std::pair<object_numberingt::number_type, offsett> &)
103  {
104  UNREACHABLE;
105  }
106 
108  {
109  public:
110  unsigned function;
111  unsigned from, to;
112 
114  function(0), from(0), to(0)
115  {
116  }
117 
118  validity_ranget(unsigned fnc, unsigned f, unsigned t):
119  function(fnc), from(f), to(t)
120  {
121  }
122 
123  bool contains(unsigned f, unsigned line) const
124  {
125  return (function==f && from<=line && line<=to);
126  }
127  };
128 
129  typedef std::list<validity_ranget> vrange_listt;
130  typedef std::map<unsigned, vrange_listt> validity_rangest;
132 
133  bool set_valid_at(unsigned inx, unsigned f, unsigned line);
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  #else
227  typedef std::unordered_map<idt, entryt, string_hash> valuest;
228  #endif
229 
231  const exprt &expr,
232  std::list<exprt> &expr_set,
233  const namespacet &ns) const;
234 
236  const idt &identifier,
237  const std::string &suffix);
238 
239  void clear()
240  {
241  values.clear();
242  }
243 
244  void add_var(const idt &id)
245  {
246  get_entry(id, "");
247  }
248 
249  void add_var(const entryt &e)
250  {
252  }
253 
254  entryt &get_entry(const idt &id, const std::string &suffix)
255  {
256  return get_entry(entryt(id, suffix));
257  }
258 
260  {
261  std::string index=id2string(e.identifier)+e.suffix;
262 
263  std::pair<valuest::iterator, bool> r=
264  values.insert(std::pair<idt, entryt>(index, e));
265 
266  return r.first->second;
267  }
268 
269  entryt &get_temporary_entry(const idt &id, const std::string &suffix)
270  {
271  std::string index=id2string(id)+suffix;
272  return temporary_values[index];
273  }
274 
275  void add_vars(const std::list<entryt> &vars)
276  {
277  for(std::list<entryt>::const_iterator
278  it=vars.begin();
279  it!=vars.end();
280  it++)
281  add_var(*it);
282  }
283 
284  void output(
285  const namespacet &ns,
286  std::ostream &out) const;
287 
289  const entryt &e,
290  const namespacet &ns,
291  std::ostream &out) const;
292 
295 
296  // true = added something new
298  object_mapt &dest,
299  const object_mapt &src) const;
300 
302  object_mapt &dest,
303  const object_mapt &src) const;
304 
306  object_mapt &dest,
307  const object_mapt &src) const;
308 
309  void apply_code(const codet &code, const namespacet &ns);
310 
311  bool handover();
312 
313  void assign(
314  const exprt &lhs,
315  const exprt &rhs,
316  const namespacet &ns,
317  bool add_to_sets=false);
318 
320  const irep_idt &function,
321  const exprt::operandst &arguments,
322  const namespacet &ns);
323 
324  // edge back to call site
326  const exprt &lhs,
327  const namespacet &ns);
328 
330  const exprt &expr,
331  expr_sett &expr_set,
332  const namespacet &ns) const;
333 
334 protected:
336  const exprt &expr,
337  object_mapt &dest,
338  const std::string &suffix,
339  const typet &original_type,
340  const namespacet &ns) const;
341 
343  const exprt &expr,
344  object_mapt &dest,
345  const namespacet &ns) const;
346 
348  const exprt &expr,
349  object_mapt &dest,
350  const namespacet &ns) const
351  {
352  get_reference_set_rec(expr, dest, ns);
353  }
354 
356  const exprt &expr,
357  object_mapt &dest,
358  const namespacet &ns) const;
359 
361  const exprt &src,
362  exprt &dest) const;
363 
365  const exprt &lhs,
366  const object_mapt &values_rhs,
367  const std::string &suffix,
368  const namespacet &ns,
369  bool add_to_sets);
370 };
371 
372 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVRNS_H
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
value_set_fivrnst::get_value_set
void get_value_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
value_set_fivrnst::object_map_dt::validity_ranget::contains
bool contains(unsigned f, unsigned line) const
Definition: value_set_fivrns.h:123
value_set_fivrnst::set
void set(object_mapt &dest, object_map_dt::const_iterator it) const
Definition: value_set_fivrns.h:141
value_set_fivrnst::assign
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
value_set_fivrnst::output
void output(const namespacet &ns, std::ostream &out) const
value_set_fivrnst::to_expr
exprt to_expr(object_map_dt::const_iterator it) const
value_set_fivrnst::object_map_dt::begin
const_iterator begin() const
Definition: value_set_fivrns.h:83
mp_arith.h
value_set_fivrnst::object_map_dt::set_valid_at
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
value_set_fivrnst::object_map_dt::begin
iterator begin()
Definition: value_set_fivrns.h:82
value_set_fivrnst::values
valuest values
Definition: value_set_fivrns.h:293
value_set_fivrnst::object_map_dt::validity_ranget::validity_ranget
validity_ranget()
Definition: value_set_fivrns.h:113
typet
The type of an expression, extends irept.
Definition: type.h:29
value_set_fivrnst::do_function_call
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
value_set_fivrnst::object_map_dt::validity_rangest
std::map< unsigned, vrange_listt > validity_rangest
Definition: value_set_fivrns.h:130
value_set_fivrnst::get_reference_set_rec
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
value_set_fivrnst::set_to
void set_to(const irep_idt &function, unsigned inx)
Definition: value_set_fivrns.h:48
value_set_fivrnst::insert_from
bool insert_from(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
value_set_fivrnst::add_vars
void add_vars(const std::list< entryt > &vars)
Definition: value_set_fivrns.h:275
value_set_fivrnst::entryt::entryt
entryt()
Definition: value_set_fivrns.h:211
template_numberingt
Definition: numbering.h:22
value_set_fivrnst::to_target_index
unsigned to_target_index
Definition: value_set_fivrns.h:38
value_set_fivrnst::object_map_dt::insert
std::pair< iterator, bool > insert(const std::pair< object_numberingt::number_type, offsett > &)
Definition: value_set_fivrns.h:97
value_set_fivrnst::object_map_dt::object_map_dt
object_map_dt()
Definition: value_set_fivrns.h:67
invariant.h
value_set_fivrnst::expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: value_set_fivrns.h:220
value_set_fivrnst::from_target_index
unsigned from_target_index
Definition: value_set_fivrns.h:38
value_set_fivrnst::add_var
void add_var(const idt &id)
Definition: value_set_fivrns.h:244
exprt
Base class for all expressions.
Definition: expr.h:53
object_numbering.h
Object Numbering.
value_set_fivrnst::handover
bool handover()
value_set_fivrnst::object_map_dt::clear
void clear()
Definition: value_set_fivrns.h:88
value_set_fivrnst::entryt::suffix
std::string suffix
Definition: value_set_fivrns.h:209
value_set_fivrnst::assign_rec
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
value_set_fivrnst::offsett
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
Definition: value_set_fivrns.h:58
namespace.h
value_set_fivrnst
Definition: value_set_fivrns.h:31
template_numberingt::number
number_type number(const key_type &a)
Definition: numbering.h:37
value_set_fivrnst::get_value_set
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
value_set_fivrnst::object_map_dt::objmap
objmapt objmap
Definition: value_set_fivrns.h:71
value_set_fivrnst::object_map_dt::size
size_t size() const
Definition: value_set_fivrns.h:86
value_set_fivrnst::insert_from
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
Definition: value_set_fivrns.h:175
value_set_fivrnst::function_numbering
static hash_numbering< irep_idt, irep_id_hash > function_numbering
Definition: value_set_fivrns.h:40
value_set_fivrnst::idt
irep_idt idt
Definition: value_set_fivrns.h:54
value_set_fivrnst::insert_to
bool insert_to(object_mapt &dest, const exprt &expr, const offsett &offset) const
Definition: value_set_fivrns.h:170
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
value_set_fivrnst::get_reference_set
void get_reference_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
Definition: value_set_fivrns.h:347
value_set_fivrnst::get_reference_set
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
value_set_fivrnst::object_map_dt::empty
bool empty() const
Definition: value_set_fivrns.h:87
value_set_fivrnst::object_map_dt::operator[]
offsett & operator[](object_numberingt::number_type k)
Definition: value_set_fivrns.h:90
value_set_fivrnst::insert_from
bool insert_from(object_mapt &dest, const exprt &expr, const offsett &offset) const
Definition: value_set_fivrns.h:200
value_set_fivrnst::object_map_dt::end
const_iterator end() const
Definition: value_set_fivrns.h:85
value_set_fivrnst::entryt::object_map
object_mapt object_map
Definition: value_set_fivrns.h:207
value_set_fivrnst::object_map_dt::vrange_listt
std::list< validity_ranget > vrange_listt
Definition: value_set_fivrns.h:129
value_set_fivrnst::object_map_dt::find
const_iterator find(object_numberingt::number_type k)
Definition: value_set_fivrns.h:78
value_set_fivrnst::make_valid_union
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
value_set_fivrnst::object_map_dt::validity_ranges
validity_rangest validity_ranges
Definition: value_set_fivrns.h:131
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
value_set_fivrnst::object_map_dt::is_valid_at
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
value_set_fivrnst::object_map_dt::validity_ranget::to
unsigned to
Definition: value_set_fivrns.h:111
value_set_fivrnst::to_function
unsigned to_function
Definition: value_set_fivrns.h:37
value_set_fivrnst::object_mapt
reference_counting< object_map_dt > object_mapt
Definition: value_set_fivrns.h:139
reference_counting< object_map_dt >
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
value_set_fivrnst::get
expr_sett & get(const idt &identifier, const std::string &suffix)
value_set_fivrnst::value_set_fivrnst
value_set_fivrnst()
Definition: value_set_fivrns.h:33
value_set_fivrnst::set_from
void set_from(const irep_idt &function, unsigned inx)
Definition: value_set_fivrns.h:42
value_set_fivrnst::object_map_dt::const_iterator
objmapt::const_iterator const_iterator
Definition: value_set_fivrns.h:74
value_set_fivrnst::object_map_dt::validity_ranget::function
unsigned function
Definition: value_set_fivrns.h:110
value_set_fivrnst::make_union
bool make_union(object_mapt &dest, const object_mapt &src) const
value_set_fivrnst::insert_to
bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
Definition: value_set_fivrns.h:146
value_set_fivrnst::object_map_dt
Definition: value_set_fivrns.h:65
value_set_fivrnst::copy_objects
void copy_objects(object_mapt &dest, const object_mapt &src) const
template_numberingt::number_type
typename Map::mapped_type number_type
Definition: numbering.h:24
value_set_fivrnst::dereference_rec
void dereference_rec(const exprt &src, exprt &dest) const
value_set_fivrnst::do_end_function
void do_end_function(const exprt &lhs, const namespacet &ns)
value_set_fivrnst::object_map_dt::validity_ranget::from
unsigned from
Definition: value_set_fivrns.h:111
value_set_fivrnst::from_function
unsigned from_function
Definition: value_set_fivrns.h:37
value_set_fivrnst::insert_to
bool insert_to(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
Definition: value_set_fivrns.h:156
value_set_fivrnst::insert_to
bool insert_to(object_mapt &dest, const exprt &src) const
Definition: value_set_fivrns.h:151
value_set_fivrnst::clear
void clear()
Definition: value_set_fivrns.h:239
reference_counting.h
Reference Counting.
value_set_fivrnst::insert_to
bool insert_to(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
value_set_fivrnst::add_var
void add_var(const entryt &e)
Definition: value_set_fivrns.h:249
value_set_fivrnst::get_entry
entryt & get_entry(const entryt &e)
Definition: value_set_fivrns.h:259
value_set_fivrnst::object_map_dt::validity_ranget
Definition: value_set_fivrns.h:108
reference_counting::write
T & write()
Definition: reference_counting.h:76
value_set_fivrnst::entryt::identifier
idt identifier
Definition: value_set_fivrns.h:208
value_set_fivrnst::insert_from
bool insert_from(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
Definition: value_set_fivrns.h:185
value_set_fivrnst::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) const
value_set_fivrnst::get_temporary_entry
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
Definition: value_set_fivrns.h:269
value_set_fivrnst::temporary_values
valuest temporary_values
Definition: value_set_fivrns.h:294
value_set_fivrnst::object_map_dt::end
iterator end()
Definition: value_set_fivrns.h:84
value_set_fivrnst::object_map_dt::insert
iterator insert(iterator, const std::pair< object_numberingt::number_type, offsett > &)
Definition: value_set_fivrns.h:102
value_set_fivrnst::entryt
Definition: value_set_fivrns.h:206
r
static int8_t r
Definition: irep_hash.h:59
value_set_fivrnst::offset_is_zero
bool offset_is_zero(offsett offset) const
Definition: value_set_fivrns.h:59
value_set_fivrnst::object_numbering
static object_numberingt object_numbering
Definition: value_set_fivrns.h:39
value_set_fivrnst::object_map_dt::objmapt
std::map< object_numberingt::number_type, offsett > objmapt
Definition: value_set_fivrns.h:70
value_set_fivrnst::object_map_dt::iterator
objmapt::iterator iterator
Definition: value_set_fivrns.h:76
value_set_fivrnst::dynamic_object_id_sett
std::unordered_set< unsigned int > dynamic_object_id_sett
Definition: value_set_fivrns.h:222
value_set_fivrnst::object_map_dt::blank
static const object_map_dt blank
Definition: value_set_fivrns.h:68
value_set_fivrnst::output_entry
void output_entry(const entryt &e, const namespacet &ns, std::ostream &out) const
value_set_fivrnst::object_map_dt::validity_ranget::validity_ranget
validity_ranget(unsigned fnc, unsigned f, unsigned t)
Definition: value_set_fivrns.h:118
value_set_fivrnst::get_entry
entryt & get_entry(const idt &id, const std::string &suffix)
Definition: value_set_fivrns.h:254
value_set_fivrnst::insert_from
bool insert_from(object_mapt &dest, const exprt &src) const
Definition: value_set_fivrns.h:180
value_set_fivrnst::entryt::entryt
entryt(const idt &_identifier, const std::string _suffix)
Definition: value_set_fivrns.h:213
value_set_fivrnst::apply_code
void apply_code(const codet &code, const namespacet &ns)
value_set_fivrnst::valuest
std::unordered_map< idt, entryt, string_hash > valuest
Definition: value_set_fivrns.h:227
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35