cprover
value_set_fi.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set (Flow Insensitive, Sharing)
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  CM Wintersteiger
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H
14 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H
15 
16 #include <list>
17 #include <map>
18 #include <set>
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  changed(false)
32  // to_function, to_target_index are set by set_to()
33  // from_function, from_target_index are set by set_from()
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(const offsett &offset) const
60  {
61  return offset && offset->is_zero();
62  }
63 
65  {
66  typedef std::map<object_numberingt::number_type, offsett> data_typet;
68 
69  public:
70  // NOLINTNEXTLINE(readability/identifiers)
71  typedef data_typet::iterator iterator;
72  // NOLINTNEXTLINE(readability/identifiers)
73  typedef data_typet::const_iterator const_iterator;
74  // NOLINTNEXTLINE(readability/identifiers)
75  typedef data_typet::value_type value_type;
76 
77  iterator begin() { return data.begin(); }
78  const_iterator begin() const { return data.begin(); }
79  const_iterator cbegin() const { return data.cbegin(); }
80 
81  iterator end() { return data.end(); }
82  const_iterator end() const { return data.end(); }
83  const_iterator cend() const { return data.cend(); }
84 
85  size_t size() const { return data.size(); }
86 
88  {
89  return data[i];
90  }
91 
92  template <typename It>
93  void insert(It b, It e) { data.insert(b, e); }
94 
95  template <typename T>
96  const_iterator find(T &&t) const { return data.find(std::forward<T>(t)); }
97 
98  static const object_map_dt blank;
99 
100  protected:
101  ~object_map_dt()=default;
102  };
103 
104  exprt to_expr(const object_map_dt::value_type &it) const;
105 
107 
108  void set(object_mapt &dest, const object_map_dt::value_type &it) const
109  {
110  dest.write()[it.first]=it.second;
111  }
112 
113  bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
114  {
115  return insert(dest, it.first, it.second);
116  }
117 
118  bool insert(object_mapt &dest, const exprt &src) const
119  {
120  return insert(dest, object_numbering.number(src), offsett());
121  }
122 
123  bool insert(
124  object_mapt &dest,
125  const exprt &src,
126  const mp_integer &offset_value) const
127  {
128  return insert(dest, object_numbering.number(src), offsett(offset_value));
129  }
130 
131  bool insert(
132  object_mapt &dest,
134  const offsett &offset) const
135  {
136  if(dest.read().find(n)==dest.read().end())
137  {
138  // new
139  dest.write()[n] = offset;
140  return true;
141  }
142  else
143  {
144  offsett &old_offset = dest.write()[n];
145 
146  if(old_offset && offset)
147  {
148  if(*old_offset == *offset)
149  return false;
150  else
151  {
152  old_offset.reset();
153  return true;
154  }
155  }
156  else if(!old_offset)
157  return false;
158  else
159  {
160  old_offset.reset();
161  return true;
162  }
163  }
164  }
165 
166  bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
167  {
168  return insert(dest, object_numbering.number(expr), offset);
169  }
170 
171  struct entryt
172  {
175  std::string suffix;
176 
178  {
179  }
180 
181  entryt(const idt &_identifier, const std::string _suffix):
182  identifier(_identifier),
183  suffix(_suffix)
184  {
185  }
186  };
187 
188  typedef std::unordered_set<exprt, irep_hash> expr_sett;
189 
190  typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
191 
192  #ifdef USE_DSTRING
193  typedef std::map<idt, entryt> valuest;
194  typedef std::set<idt> flatten_seent;
195  typedef std::unordered_set<idt> gvs_recursion_sett;
196  typedef std::unordered_set<idt> recfind_recursion_sett;
197  typedef std::unordered_set<idt> assign_recursion_sett;
198  #else
199  typedef std::unordered_map<idt, entryt, string_hash> valuest;
200  typedef std::unordered_set<idt, string_hash> flatten_seent;
201  typedef std::unordered_set<idt, string_hash> gvs_recursion_sett;
202  typedef std::unordered_set<idt, string_hash> recfind_recursion_sett;
203  typedef std::unordered_set<idt, string_hash> assign_recursion_sett;
204  #endif
205 
206  void get_value_set(
207  const exprt &expr,
208  std::list<exprt> &dest,
209  const namespacet &ns) const;
210 
211  expr_sett &get(
212  const idt &identifier,
213  const std::string &suffix);
214 
215  void make_any()
216  {
217  values.clear();
218  }
219 
220  void clear()
221  {
222  values.clear();
223  }
224 
225  void add_var(const idt &id, const std::string &suffix)
226  {
227  get_entry(id, suffix);
228  }
229 
230  void add_var(const entryt &e)
231  {
233  }
234 
235  entryt &get_entry(const idt &id, const std::string &suffix)
236  {
237  return get_entry(entryt(id, suffix));
238  }
239 
241  {
242  std::string index=id2string(e.identifier)+e.suffix;
243 
244  std::pair<valuest::iterator, bool> r=
245  values.insert(std::pair<idt, entryt>(index, e));
246 
247  return r.first->second;
248  }
249 
250  void add_vars(const std::list<entryt> &vars)
251  {
252  for(std::list<entryt>::const_iterator
253  it=vars.begin();
254  it!=vars.end();
255  it++)
256  add_var(*it);
257  }
258 
259  void output(
260  const namespacet &ns,
261  std::ostream &out) const;
262 
264 
265  bool changed;
266 
267  // true = added something new
268  bool make_union(object_mapt &dest, const object_mapt &src) const;
269 
270  // true = added something new
271  bool make_union(const valuest &new_values);
272 
273  // true = added something new
274  bool make_union(const value_set_fit &new_values)
275  {
276  return make_union(new_values.values);
277  }
278 
279  void apply_code(
280  const exprt &code,
281  const namespacet &ns);
282 
283  void assign(
284  const exprt &lhs,
285  const exprt &rhs,
286  const namespacet &ns);
287 
288  void do_function_call(
289  const irep_idt &function,
290  const exprt::operandst &arguments,
291  const namespacet &ns);
292 
293  // edge back to call site
294  void do_end_function(
295  const exprt &lhs,
296  const namespacet &ns);
297 
298  void get_reference_set(
299  const exprt &expr,
300  expr_sett &expr_set,
301  const namespacet &ns) const;
302 
303 protected:
305  const exprt &expr,
306  expr_sett &expr_set,
307  const namespacet &ns) const;
308 
309  void get_value_set_rec(
310  const exprt &expr,
311  object_mapt &dest,
312  const std::string &suffix,
313  const typet &original_type,
314  const namespacet &ns,
315  gvs_recursion_sett &recursion_set) const;
316 
317 
318  void get_value_set(
319  const exprt &expr,
320  object_mapt &dest,
321  const namespacet &ns) const;
322 
324  const exprt &expr,
325  object_mapt &dest,
326  const namespacet &ns) const
327  {
328  get_reference_set_sharing_rec(expr, dest, ns);
329  }
330 
332  const exprt &expr,
333  object_mapt &dest,
334  const namespacet &ns) const;
335 
336  void dereference_rec(
337  const exprt &src,
338  exprt &dest) const;
339 
340  void assign_rec(
341  const exprt &lhs,
342  const object_mapt &values_rhs,
343  const std::string &suffix,
344  const namespacet &ns,
345  assign_recursion_sett &recursion_set);
346 
347  void do_free(
348  const exprt &op,
349  const namespacet &ns);
350 
351  void flatten(const entryt &e, object_mapt &dest) const;
352 
353  void flatten_rec(
354  const entryt&,
355  object_mapt&,
356  flatten_seent&) const;
357 };
358 
359 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H
The type of an expression.
Definition: type.h:22
void output(const namespacet &ns, std::ostream &out) const
bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
Definition: value_set_fi.h:166
void set_from(const irep_idt &function, unsigned inx)
Definition: value_set_fi.h:42
data_typet::value_type value_type
Definition: value_set_fi.h:75
static int8_t r
Definition: irep_hash.h:59
std::unordered_set< unsigned int > dynamic_object_id_sett
Definition: value_set_fi.h:190
BigInt mp_integer
Definition: mp_arith.h:22
number_type number(const key_type &a)
Definition: numbering.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
std::unordered_set< idt, string_hash > recfind_recursion_sett
Definition: value_set_fi.h:202
std::unordered_set< idt, string_hash > flatten_seent
Definition: value_set_fi.h:200
std::unordered_set< exprt, irep_hash > expr_sett
Definition: value_set_fi.h:188
const_iterator find(T &&t) const
Definition: value_set_fi.h:96
void get_reference_set_sharing(const exprt &expr, object_mapt &dest, const namespacet &ns) const
Definition: value_set_fi.h:323
bool insert(object_mapt &dest, const exprt &src) const
Definition: value_set_fi.h:118
void do_free(const exprt &op, const namespacet &ns)
std::unordered_map< idt, entryt, string_hash > valuest
Definition: value_set_fi.h:199
offsett & operator[](object_numberingt::number_type i)
Definition: value_set_fi.h:87
unsigned to_target_index
Definition: value_set_fi.h:38
void add_var(const entryt &e)
Definition: value_set_fi.h:230
exprt to_expr(const object_map_dt::value_type &it) const
static const object_map_dt blank
Definition: value_set_fi.h:98
const_iterator end() const
Definition: value_set_fi.h:82
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
Definition: value_set_fi.h:113
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
void apply_code(const exprt &code, const namespacet &ns)
const_iterator cend() const
Definition: value_set_fi.h:83
std::unordered_set< idt, string_hash > gvs_recursion_sett
Definition: value_set_fi.h:201
unsigned to_function
Definition: value_set_fi.h:37
unsigned from_function
Definition: value_set_fi.h:37
void set_to(const irep_idt &function, unsigned inx)
Definition: value_set_fi.h:48
bool make_union(object_mapt &dest, const object_mapt &src) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &) const
std::unordered_set< exprt, irep_hash > expr_sett
int size
Definition: kdev_t.h:25
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
nonstd::optional< T > optionalt
Definition: optional.h:35
static object_numberingt object_numbering
Definition: value_set_fi.h:39
entryt & get_entry(const entryt &e)
Definition: value_set_fi.h:240
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)
TO_BE_DOCUMENTED.
Definition: namespace.h:74
entryt & get_entry(const idt &id, const std::string &suffix)
Definition: value_set_fi.h:235
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
bool make_union(const value_set_fit &new_values)
Definition: value_set_fi.h:274
const_iterator begin() const
Definition: value_set_fi.h:78
void get_value_set(const exprt &expr, std::list< exprt > &dest, const namespacet &ns) const
typename Map::mapped_type number_type
Definition: numbering.h:24
void flatten(const entryt &e, object_mapt &dest) const
valuest values
Definition: value_set_fi.h:263
std::vector< exprt > operandst
Definition: expr.h:45
void do_end_function(const exprt &lhs, const namespacet &ns)
const_iterator cbegin() const
Definition: value_set_fi.h:79
std::unordered_set< idt, string_hash > assign_recursion_sett
Definition: value_set_fi.h:203
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
bool insert(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
Definition: value_set_fi.h:131
data_typet::const_iterator const_iterator
Definition: value_set_fi.h:73
Base class for all expressions.
Definition: expr.h:42
Reference Counting.
data_typet::iterator iterator
Definition: value_set_fi.h:71
void dereference_rec(const exprt &src, exprt &dest) const
static hash_numbering< irep_idt, irep_id_hash > function_numbering
Definition: value_set_fi.h:40
bool offset_is_zero(const offsett &offset) const
Definition: value_set_fi.h:59
const T & read() const
reference_counting< object_map_dt > object_mapt
Definition: value_set_fi.h:106
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns)
void add_var(const idt &id, const std::string &suffix)
Definition: value_set_fi.h:225
object_mapt object_map
Definition: value_set_fi.h:173
std::map< object_numberingt::number_type, offsett > data_typet
Definition: value_set_fi.h:66
entryt(const idt &_identifier, const std::string _suffix)
Definition: value_set_fi.h:181
bool insert(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
Definition: value_set_fi.h:123
void add_vars(const std::list< entryt > &vars)
Definition: value_set_fi.h:250
Definition: kdev_t.h:24
irep_idt idt
Definition: value_set_fi.h:54
unsigned from_target_index
Definition: value_set_fi.h:38
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value...
Definition: value_set_fi.h:58