cprover
value_set.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_H
13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_H
14 
15 #include <set>
16 
17 #include <util/mp_arith.h>
19 
20 #include "object_numbering.h"
21 #include "value_sets.h"
22 
23 class namespacet;
24 
42 {
43 public:
45  {
46  }
47 
48  static bool field_sensitive(
49  const irep_idt &id,
50  const typet &type,
51  const namespacet &);
52 
55  unsigned location_number;
56 
60 
61  typedef irep_idt idt;
62 
66  bool offset_is_zero(const offsett &offset) const
67  {
68  return offset && offset->is_zero();
69  }
70 
79  {
80  typedef std::map<object_numberingt::number_type, offsett> data_typet;
82 
83  public:
84  // NOLINTNEXTLINE(readability/identifiers)
85  typedef data_typet::iterator iterator;
86  // NOLINTNEXTLINE(readability/identifiers)
87  typedef data_typet::const_iterator const_iterator;
88  // NOLINTNEXTLINE(readability/identifiers)
89  typedef data_typet::value_type value_type;
90  // NOLINTNEXTLINE(readability/identifiers)
91  typedef data_typet::key_type key_type;
92 
93  iterator begin() { return data.begin(); }
94  const_iterator begin() const { return data.begin(); }
95  const_iterator cbegin() const { return data.cbegin(); }
96 
97  iterator end() { return data.end(); }
98  const_iterator end() const { return data.end(); }
99  const_iterator cend() const { return data.cend(); }
100 
101  size_t size() const { return data.size(); }
102  bool empty() const { return data.empty(); }
103 
104  void erase(key_type i) { data.erase(i); }
105  void erase(const_iterator it) { data.erase(it); }
106 
108  {
109  return data[i];
110  }
112  {
113  return data.at(i);
114  }
115  const offsett &at(key_type i) const
116  {
117  return data.at(i);
118  }
119 
120  template <typename It>
121  void insert(It b, It e) { data.insert(b, e); }
122 
123  template <typename T>
124  const_iterator find(T &&t) const { return data.find(std::forward<T>(t)); }
125 
126  static const object_map_dt blank;
127 
128  object_map_dt()=default;
129 
130  bool operator==(const object_map_dt &other) const
131  {
132  return data==other.data;
133  }
134  bool operator!=(const object_map_dt &other) const
135  {
136  return !(*this==other);
137  }
138 
139  protected:
140  ~object_map_dt()=default;
141  };
142 
147  exprt to_expr(const object_map_dt::value_type &it) const;
148 
162 
168  void set(object_mapt &dest, const object_map_dt::value_type &it) const
169  {
170  dest.write()[it.first]=it.second;
171  }
172 
179  bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
180  {
181  return insert(dest, it.first, it.second);
182  }
183 
189  bool insert(object_mapt &dest, const exprt &src) const
190  {
191  return insert(dest, object_numbering.number(src), offsett());
192  }
193 
200  bool insert(
201  object_mapt &dest,
202  const exprt &src,
203  const mp_integer &offset_value) const
204  {
205  return insert(dest, object_numbering.number(src), offsett(offset_value));
206  }
207 
215  bool insert(
216  object_mapt &dest,
218  const offsett &offset) const;
219 
226  bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
227  {
228  return insert(dest, object_numbering.number(expr), offset);
229  }
230 
235  struct entryt
236  {
239  std::string suffix;
240 
242  {
243  }
244 
245  entryt(const idt &_identifier, const std::string &_suffix):
246  identifier(_identifier),
247  suffix(_suffix)
248  {
249  }
250 
251  bool operator==(const entryt &other) const
252  {
253  return
254  identifier==other.identifier &&
255  suffix==other.suffix &&
256  object_map==other.object_map;
257  }
258  bool operator!=(const entryt &other) const
259  {
260  return !(*this==other);
261  }
262  };
263 
266  typedef std::set<exprt> expr_sett;
267 
271  typedef std::set<unsigned int> dynamic_object_id_sett;
272 
286  #ifdef USE_DSTRING
287  typedef std::map<idt, entryt> valuest;
288  #else
289  typedef std::unordered_map<idt, entryt, string_hash> valuest;
290  #endif
291 
297  void get_value_set(
298  const exprt &expr,
299  value_setst::valuest &dest,
300  const namespacet &ns) const;
301 
303  expr_sett &get(
304  const idt &identifier,
305  const std::string &suffix);
306 
308  void make_any()
309  {
310  values.clear();
311  }
312 
313  void clear()
314  {
315  values.clear();
316  }
317 
328  entryt &get_entry(
329  const entryt &e, const typet &type,
330  const namespacet &ns);
331 
335  void output(
336  const namespacet &ns,
337  std::ostream &out) const;
338 
342 
347  bool make_union(object_mapt &dest, const object_mapt &src) const;
348 
352  bool make_union(const valuest &new_values);
353 
356  bool make_union(const value_sett &new_values)
357  {
358  return make_union(new_values.values);
359  }
360 
366  void guard(
367  const exprt &expr,
368  const namespacet &ns);
369 
377  const codet &code,
378  const namespacet &ns)
379  {
380  apply_code_rec(code, ns);
381  }
382 
396  void assign(
397  const exprt &lhs,
398  const exprt &rhs,
399  const namespacet &ns,
400  bool is_simplified,
401  bool add_to_sets);
402 
410  void do_function_call(
411  const irep_idt &function,
412  const exprt::operandst &arguments,
413  const namespacet &ns);
414 
422  void do_end_function(
423  const exprt &lhs,
424  const namespacet &ns);
425 
433  void get_reference_set(
434  const exprt &expr,
435  value_setst::valuest &dest,
436  const namespacet &ns) const;
437 
447  bool eval_pointer_offset(
448  exprt &expr,
449  const namespacet &ns) const;
450 
451 protected:
458  void get_value_set(
459  const exprt &expr,
460  object_mapt &dest,
461  const namespacet &ns,
462  bool is_simplified) const;
463 
467  const exprt &expr,
468  object_mapt &dest,
469  const namespacet &ns) const
470  {
471  get_reference_set_rec(expr, dest, ns);
472  }
473 
476  const exprt &expr,
477  object_mapt &dest,
478  const namespacet &ns) const;
479 
481  void dereference_rec(
482  const exprt &src,
483  exprt &dest) const;
484 
488  void do_free(
489  const exprt &op,
490  const namespacet &ns);
491 
499  const exprt &src,
500  const irep_idt &component_name,
501  const namespacet &ns);
502 
503  // Subclass customisation points:
504 
505 protected:
507  virtual void get_value_set_rec(
508  const exprt &expr,
509  object_mapt &dest,
510  const std::string &suffix,
511  const typet &original_type,
512  const namespacet &ns) const;
513 
515  virtual void assign_rec(
516  const exprt &lhs,
517  const object_mapt &values_rhs,
518  const std::string &suffix,
519  const namespacet &ns,
520  bool add_to_sets);
521 
523  virtual void apply_code_rec(
524  const codet &code,
525  const namespacet &ns);
526 
527  private:
533  const exprt &rhs,
534  const namespacet &ns,
535  object_mapt &rhs_values) const
536  {
537  }
538 
544  const exprt &lhs,
545  const exprt &rhs,
546  const namespacet &ns)
547  {
548  }
549 };
550 
551 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H
The type of an expression.
Definition: type.h:22
bool insert(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
Adds an expression to an object map, with known offset.
Definition: value_set.h:200
BigInt mp_integer
Definition: mp_arith.h:22
number_type number(const key_type &a)
Definition: numbering.h:37
bool offset_is_zero(const offsett &offset) const
Definition: value_set.h:66
Represents a row of a value_sett.
Definition: value_set.h:235
object_mapt object_map
Definition: value_set.h:237
void erase(key_type i)
Definition: value_set.h:104
entryt(const idt &_identifier, const std::string &_suffix)
Definition: value_set.h:245
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Transforms this value-set by executing executing the assignment lhs := rhs against it...
Definition: value_set.cpp:1088
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
Definition: value_set.cpp:245
virtual void apply_code_rec(const codet &code, const namespacet &ns)
Subclass customisation point for applying code to this domain:
Definition: value_set.cpp:1491
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See get_reference_set.
Definition: value_set.cpp:926
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
Definition: value_set.cpp:313
static const object_map_dt blank
Definition: value_set.h:126
const_iterator end() const
Definition: value_set.h:98
static object_numberingt object_numbering
Global shared object numbering, used to abbreviate expressions stored in value sets.
Definition: value_set.h:59
void insert(It b, It e)
Definition: value_set.h:121
void dereference_rec(const exprt &src, exprt &dest) const
Sets dest to src with any wrapping typecasts removed.
Definition: value_set.cpp:893
const_iterator cend() const
Definition: value_set.h:99
virtual void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
Subclass customisation point for recursion over LHS expression:
Definition: value_set.cpp:1296
virtual void apply_assign_side_effects(const exprt &lhs, const exprt &rhs, const namespacet &ns)
Subclass customisation point to apply global side-effects to this domain, after RHS values are read b...
Definition: value_set.h:543
std::map< object_numberingt::number_type, offsett > data_typet
Definition: value_set.h:80
offsett & operator[](key_type i)
Definition: value_set.h:107
const_iterator begin() const
Definition: value_set.h:94
static bool field_sensitive(const irep_idt &id, const typet &type, const namespacet &)
Definition: value_set.cpp:39
irep_idt idt
Definition: value_set.h:61
bool operator!=(const entryt &other) const
Definition: value_set.h:258
bool eval_pointer_offset(exprt &expr, const namespacet &ns) const
Tries to resolve any pointer_offset_exprt expressions in expr to constant integers using this value-s...
Definition: value_set.cpp:260
Value Set Propagation.
const offsett & at(key_type i) const
Definition: value_set.h:115
std::set< exprt > expr_sett
Set of expressions; only used for the get API, not for internal data representation.
Definition: value_set.h:266
int size
Definition: kdev_t.h:25
nonstd::optional< T > optionalt
Definition: optional.h:35
data_typet::value_type value_type
Definition: value_set.h:89
bool operator==(const entryt &other) const
Definition: value_set.h:251
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Transforms this value-set by executing the actual -> formal parameter assignments for a particular ca...
Definition: value_set.cpp:1433
TO_BE_DOCUMENTED.
Definition: namespace.h:74
data_typet::const_iterator const_iterator
Definition: value_set.h:87
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value...
Definition: value_set.h:65
virtual void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
Subclass customisation point for recursion over RHS expression:
Definition: value_set.cpp:347
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:41
bool insert(object_mapt &dest, const exprt &src) const
Adds an expression to an object map, with unknown offset.
Definition: value_set.h:189
typename Map::mapped_type number_type
Definition: numbering.h:24
void make_any()
Clears value set (not used in the CBMC repository)
Definition: value_set.h:308
bool operator!=(const object_map_dt &other) const
Definition: value_set.h:134
const_iterator cbegin() const
Definition: value_set.h:95
virtual void adjust_assign_rhs_values(const exprt &rhs, const namespacet &ns, object_mapt &rhs_values) const
Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set b...
Definition: value_set.h:532
std::vector< exprt > operandst
Definition: expr.h:45
const_iterator find(T &&t) const
Definition: value_set.h:124
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
Merges an existing entry into an object map.
Definition: value_set.h:179
std::unordered_map< idt, entryt, string_hash > valuest
Map representing the entire value set, mapping from string LHS IDs to RHS expression sets...
Definition: value_set.h:289
void do_end_function(const exprt &lhs, const namespacet &ns)
Transforms this value-set by assigning this function&#39;s return value to a given LHS expression...
Definition: value_set.cpp:1479
bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
Adds an expression and offset to an object map.
Definition: value_set.h:226
void erase(const_iterator it)
Definition: value_set.h:105
void get_reference_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets the set of expressions that expr may refer to, according to this value set.
Definition: value_set.cpp:911
Base class for all expressions.
Definition: expr.h:42
Reference Counting.
bool operator==(const object_map_dt &other) const
Definition: value_set.h:130
std::set< unsigned int > dynamic_object_id_sett
Set of dynamic object numbers, equivalent to a set of dynamic_object_exprts with corresponding IDs...
Definition: value_set.h:271
Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances)...
Definition: value_set.h:78
value_sett()
Definition: value_set.h:44
void clear()
Definition: value_set.h:313
bool make_union(const value_sett &new_values)
Merges an entire existing value_sett&#39;s data into this one.
Definition: value_set.h:356
void output(const namespacet &ns, std::ostream &out) const
Pretty-print this value-set.
Definition: value_set.cpp:96
A statement in a programming language.
Definition: std_code.h:21
offsett & at(key_type i)
Definition: value_set.h:111
exprt to_expr(const object_map_dt::value_type &it) const
Converts an object_map_dt entry object_number -> offset into an object_descriptor_exprt with ...
Definition: value_set.cpp:186
entryt & get_entry(const entryt &e, const typet &type, const namespacet &ns)
Gets or inserts an entry in this value-set.
Definition: value_set.cpp:54
data_typet::iterator iterator
Definition: value_set.h:85
void guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
Definition: value_set.cpp:1624
void do_free(const exprt &op, const namespacet &ns)
Marks objects that may be pointed to by op as maybe-invalid.
Definition: value_set.cpp:1216
std::list< exprt > valuest
Definition: value_sets.h:28
void get_reference_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See the other overload of get_reference_set.
Definition: value_set.h:466
std::string suffix
Definition: value_set.h:239
valuest values
Stores the LHS ID -> RHS expression set map.
Definition: value_set.h:341
void apply_code(const codet &code, const namespacet &ns)
Transforms this value-set by executing a given statement against it.
Definition: value_set.h:376
size_t size() const
Definition: value_set.h:101
data_typet::key_type key_type
Definition: value_set.h:91
Definition: kdev_t.h:24
unsigned location_number
Matches the location_number field of the instruction that corresponds to this value_sett instance in ...
Definition: value_set.h:55
reference_counting< object_map_dt > object_mapt
Reference-counts instances of object_map_dt, such that multiple instructions&#39; value_sett instances ca...
Definition: value_set.h:161
exprt make_member(const exprt &src, const irep_idt &component_name, const namespacet &ns)
Extracts a member from a struct- or union-typed expression.
Definition: value_set.cpp:1658