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 clear()
216  {
217  values.clear();
218  }
219 
220  void add_var(const idt &id, const std::string &suffix)
221  {
222  get_entry(id, suffix);
223  }
224 
225  void add_var(const entryt &e)
226  {
228  }
229 
230  entryt &get_entry(const idt &id, const std::string &suffix)
231  {
232  return get_entry(entryt(id, suffix));
233  }
234 
236  {
237  std::string index=id2string(e.identifier)+e.suffix;
238 
239  std::pair<valuest::iterator, bool> r=
240  values.insert(std::pair<idt, entryt>(index, e));
241 
242  return r.first->second;
243  }
244 
245  void add_vars(const std::list<entryt> &vars)
246  {
247  for(std::list<entryt>::const_iterator
248  it=vars.begin();
249  it!=vars.end();
250  it++)
251  add_var(*it);
252  }
253 
254  void output(
255  const namespacet &ns,
256  std::ostream &out) const;
257 
259 
260  bool changed;
261 
262  // true = added something new
263  bool make_union(object_mapt &dest, const object_mapt &src) const;
264 
265  // true = added something new
266  bool make_union(const valuest &new_values);
267 
268  // true = added something new
269  bool make_union(const value_set_fit &new_values)
270  {
271  return make_union(new_values.values);
272  }
273 
274  void apply_code(
275  const exprt &code,
276  const namespacet &ns);
277 
278  void assign(
279  const exprt &lhs,
280  const exprt &rhs,
281  const namespacet &ns);
282 
283  void do_function_call(
284  const irep_idt &function,
285  const exprt::operandst &arguments,
286  const namespacet &ns);
287 
288  // edge back to call site
289  void do_end_function(
290  const exprt &lhs,
291  const namespacet &ns);
292 
293  void get_reference_set(
294  const exprt &expr,
295  expr_sett &expr_set,
296  const namespacet &ns) const;
297 
298 protected:
300  const exprt &expr,
301  expr_sett &expr_set,
302  const namespacet &ns) const;
303 
304  void get_value_set_rec(
305  const exprt &expr,
306  object_mapt &dest,
307  const std::string &suffix,
308  const typet &original_type,
309  const namespacet &ns,
310  gvs_recursion_sett &recursion_set) const;
311 
312 
313  void get_value_set(
314  const exprt &expr,
315  object_mapt &dest,
316  const namespacet &ns) const;
317 
319  const exprt &expr,
320  object_mapt &dest,
321  const namespacet &ns) const
322  {
323  get_reference_set_sharing_rec(expr, dest, ns);
324  }
325 
327  const exprt &expr,
328  object_mapt &dest,
329  const namespacet &ns) const;
330 
331  void dereference_rec(
332  const exprt &src,
333  exprt &dest) const;
334 
335  void assign_rec(
336  const exprt &lhs,
337  const object_mapt &values_rhs,
338  const std::string &suffix,
339  const namespacet &ns,
340  assign_recursion_sett &recursion_set);
341 
342  void flatten(const entryt &e, object_mapt &dest) const;
343 
344  void flatten_rec(
345  const entryt&,
346  object_mapt&,
347  flatten_seent&) const;
348 };
349 
350 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H
The type of an expression, extends irept.
Definition: type.h:27
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:44
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:318
bool insert(object_mapt &dest, const exprt &src) const
Definition: value_set_fi.h:118
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
Object Numbering.
unsigned to_target_index
Definition: value_set_fi.h:38
void add_var(const entryt &e)
Definition: value_set_fi.h:225
expr_sett & get(const idt &identifier, const std::string &suffix)
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
void set(object_mapt &dest, const object_map_dt::value_type &it) const
Definition: value_set_fi.h:108
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:235
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
entryt & get_entry(const idt &id, const std::string &suffix)
Definition: value_set_fi.h:230
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:269
const_iterator begin() const
Definition: value_set_fi.h:78
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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:258
std::vector< exprt > operandst
Definition: expr.h:57
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:54
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:220
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:245
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