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 <map>
17 #include <set>
18 #include <unordered_set>
19 
20 #include <util/mp_arith.h>
21 #include <util/namespace.h>
23 
24 #include "object_numbering.h"
25 
27 {
28 public:
30  {
31  }
32 
37 
38  void set_from(const irep_idt &function, unsigned inx)
39  {
40  from_function = function_numbering.number(function);
41  from_target_index = inx;
42  }
43 
44  void set_to(const irep_idt &function, unsigned inx)
45  {
46  to_function = function_numbering.number(function);
47  to_target_index = inx;
48  }
49 
50  typedef irep_idt idt;
51 
52  class objectt
53  {
54  public:
56  {
57  }
58 
59  explicit objectt(const mp_integer &_offset):
60  offset(_offset),
61  offset_is_set(true)
62  {
63  }
64 
67  bool offset_is_zero() const
68  { return offset_is_set && offset.is_zero(); }
69  };
70 
71  class object_map_dt:public std::map<unsigned, objectt>
72  {
73  public:
75  static const object_map_dt blank;
76  };
77 
78  exprt to_expr(object_map_dt::const_iterator it) const;
79 
81 
82  void set(object_mapt &dest, object_map_dt::const_iterator it) const
83  {
84  dest.write()[it->first]=it->second;
85  }
86 
87  bool insert(object_mapt &dest, object_map_dt::const_iterator it) const
88  {
89  return insert(dest, it->first, it->second);
90  }
91 
92  bool insert(object_mapt &dest, const exprt &src) const
93  {
94  return insert(dest, object_numbering.number(src), objectt());
95  }
96 
97  bool insert(
98  object_mapt &dest,
99  const exprt &src,
100  const mp_integer &offset) const
101  {
102  return insert(dest, object_numbering.number(src), objectt(offset));
103  }
104 
105  bool insert(object_mapt &dest, unsigned n, const objectt &object) const
106  {
107  if(dest.read().find(n)==dest.read().end())
108  {
109  // new
110  dest.write()[n]=object;
111  return true;
112  }
113  else
114  {
115  objectt &old=dest.write()[n];
116 
117  if(old.offset_is_set && object.offset_is_set)
118  {
119  if(old.offset==object.offset)
120  return false;
121  else
122  {
123  old.offset_is_set=false;
124  return true;
125  }
126  }
127  else if(!old.offset_is_set)
128  return false;
129  else
130  {
131  old.offset_is_set=false;
132  return true;
133  }
134  }
135  }
136 
137  bool insert(object_mapt &dest, const exprt &expr, const objectt &object) const
138  {
139  return insert(dest, object_numbering.number(expr), object);
140  }
141 
142  struct entryt
143  {
144  object_mapt object_map;
146  std::string suffix;
147 
149  {
150  }
151 
152  entryt(const idt &_identifier, const std::string _suffix):
153  identifier(_identifier),
154  suffix(_suffix)
155  {
156  }
157  };
158 
159  typedef std::unordered_set<exprt, irep_hash> expr_sett;
160 
161  typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
162 
163  #ifdef USE_DSTRING
164  typedef std::map<idt, entryt> valuest;
165  typedef std::set<idt> flatten_seent;
166  typedef std::unordered_set<idt, irep_id_hash> gvs_recursion_sett;
167  typedef std::unordered_set<idt, irep_id_hash> recfind_recursion_sett;
168  typedef std::unordered_set<idt, irep_id_hash> assign_recursion_sett;
169  #else
170  typedef std::unordered_map<idt, entryt, string_hash> valuest;
171  typedef std::unordered_set<idt, string_hash> flatten_seent;
172  typedef std::unordered_set<idt, string_hash> gvs_recursion_sett;
173  typedef std::unordered_set<idt, string_hash> recfind_recursion_sett;
174  typedef std::unordered_set<idt, string_hash> assign_recursion_sett;
175  #endif
176 
177  void get_value_set(
178  const exprt &expr,
179  std::list<exprt> &dest,
180  const namespacet &ns) const;
181 
182  expr_sett &get(
183  const idt &identifier,
184  const std::string &suffix);
185 
186  void make_any()
187  {
188  values.clear();
189  }
190 
191  void clear()
192  {
193  values.clear();
194  }
195 
196  void add_var(const idt &id, const std::string &suffix)
197  {
198  get_entry(id, suffix);
199  }
200 
201  void add_var(const entryt &e)
202  {
204  }
205 
206  entryt &get_entry(const idt &id, const std::string &suffix)
207  {
208  return get_entry(entryt(id, suffix));
209  }
210 
212  {
213  std::string index=id2string(e.identifier)+e.suffix;
214 
215  std::pair<valuest::iterator, bool> r=
216  values.insert(std::pair<idt, entryt>(index, e));
217 
218  return r.first->second;
219  }
220 
221  void add_vars(const std::list<entryt> &vars)
222  {
223  for(std::list<entryt>::const_iterator
224  it=vars.begin();
225  it!=vars.end();
226  it++)
227  add_var(*it);
228  }
229 
230  void output(
231  const namespacet &ns,
232  std::ostream &out) const;
233 
234  valuest values;
235 
236  bool changed;
237 
238  // true = added something new
239  bool make_union(object_mapt &dest, const object_mapt &src) const;
240 
241  // true = added something new
242  bool make_union(const valuest &new_values);
243 
244  // true = added something new
245  bool make_union(const value_set_fit &new_values)
246  {
247  return make_union(new_values.values);
248  }
249 
250  void apply_code(
251  const exprt &code,
252  const namespacet &ns);
253 
254  void assign(
255  const exprt &lhs,
256  const exprt &rhs,
257  const namespacet &ns);
258 
259  void do_function_call(
260  const irep_idt &function,
261  const exprt::operandst &arguments,
262  const namespacet &ns);
263 
264  // edge back to call site
265  void do_end_function(
266  const exprt &lhs,
267  const namespacet &ns);
268 
269  void get_reference_set(
270  const exprt &expr,
271  expr_sett &expr_set,
272  const namespacet &ns) const;
273 
274 protected:
276  const exprt &expr,
277  expr_sett &expr_set,
278  const namespacet &ns) const;
279 
280  void get_value_set_rec(
281  const exprt &expr,
282  object_mapt &dest,
283  const std::string &suffix,
284  const typet &original_type,
285  const namespacet &ns,
286  gvs_recursion_sett &recursion_set) const;
287 
288 
289  void get_value_set(
290  const exprt &expr,
291  object_mapt &dest,
292  const namespacet &ns) const;
293 
295  const exprt &expr,
296  object_mapt &dest,
297  const namespacet &ns) const
298  {
299  get_reference_set_sharing_rec(expr, dest, ns);
300  }
301 
303  const exprt &expr,
304  object_mapt &dest,
305  const namespacet &ns) const;
306 
307  void dereference_rec(
308  const exprt &src,
309  exprt &dest) const;
310 
311  void assign_rec(
312  const exprt &lhs,
313  const object_mapt &values_rhs,
314  const std::string &suffix,
315  const namespacet &ns,
316  assign_recursion_sett &recursion_set);
317 
318  void do_free(
319  const exprt &op,
320  const namespacet &ns);
321 
322  void flatten(const entryt &e, object_mapt &dest) const;
323 
324  void flatten_rec(
325  const entryt&,
326  object_mapt&,
327  flatten_seent&) const;
328 };
329 
330 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H
The type of an expression.
Definition: type.h:20
void output(const namespacet &ns, std::ostream &out) const
void set_from(const irep_idt &function, unsigned inx)
Definition: value_set_fi.h:38
static int8_t r
Definition: irep_hash.h:59
std::unordered_set< unsigned int > dynamic_object_id_sett
Definition: value_set_fi.h:161
BigInt mp_integer
Definition: mp_arith.h:19
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:173
std::unordered_set< idt, string_hash > flatten_seent
Definition: value_set_fi.h:171
std::unordered_set< exprt, irep_hash > expr_sett
Definition: value_set_fi.h:159
void get_reference_set_sharing(const exprt &expr, object_mapt &dest, const namespacet &ns) const
Definition: value_set_fi.h:294
bool insert(object_mapt &dest, const exprt &src) const
Definition: value_set_fi.h:92
bool insert(object_mapt &dest, const exprt &expr, const objectt &object) const
Definition: value_set_fi.h:137
void do_free(const exprt &op, const namespacet &ns)
std::unordered_map< idt, entryt, string_hash > valuest
Definition: value_set_fi.h:170
unsigned to_target_index
Definition: value_set_fi.h:34
exprt to_expr(object_map_dt::const_iterator it) const
void add_var(const entryt &e)
Definition: value_set_fi.h:201
bool insert(object_mapt &dest, const exprt &src, const mp_integer &offset) const
Definition: value_set_fi.h:97
static const object_map_dt blank
Definition: value_set_fi.h:75
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
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)
std::unordered_set< idt, string_hash > gvs_recursion_sett
Definition: value_set_fi.h:172
unsigned to_function
Definition: value_set_fi.h:33
unsigned from_function
Definition: value_set_fi.h:33
void set_to(const irep_idt &function, unsigned inx)
Definition: value_set_fi.h:44
bool make_union(object_mapt &dest, const object_mapt &src) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &) const
bool insert(object_mapt &dest, unsigned n, const objectt &object) const
Definition: value_set_fi.h:105
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
static object_numberingt object_numbering
Definition: value_set_fi.h:35
entryt & get_entry(const entryt &e)
Definition: value_set_fi.h:211
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:62
entryt & get_entry(const idt &id, const std::string &suffix)
Definition: value_set_fi.h:206
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:245
void get_value_set(const exprt &expr, std::list< exprt > &dest, const namespacet &ns) const
objectt(const mp_integer &_offset)
Definition: value_set_fi.h:59
void flatten(const entryt &e, object_mapt &dest) const
valuest values
Definition: value_set_fi.h:234
std::vector< exprt > operandst
Definition: expr.h:49
void do_end_function(const exprt &lhs, const namespacet &ns)
std::unordered_set< idt, string_hash > assign_recursion_sett
Definition: value_set_fi.h:174
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
Base class for all expressions.
Definition: expr.h:46
Reference Counting.
void dereference_rec(const exprt &src, exprt &dest) const
static hash_numbering< irep_idt, irep_id_hash > function_numbering
Definition: value_set_fi.h:36
const T & read() const
reference_counting< object_map_dt > object_mapt
Definition: value_set_fi.h:80
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:196
bool offset_is_zero() const
Definition: value_set_fi.h:67
object_mapt object_map
Definition: value_set_fi.h:144
bool insert(object_mapt &dest, object_map_dt::const_iterator it) const
Definition: value_set_fi.h:87
entryt(const idt &_identifier, const std::string _suffix)
Definition: value_set_fi.h:152
number_type number(const T &a)
Definition: numbering.h:80
void add_vars(const std::list< entryt > &vars)
Definition: value_set_fi.h:221
irep_idt idt
Definition: value_set_fi.h:50
unsigned from_target_index
Definition: value_set_fi.h:34