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  virtual ~value_sett() = default;
49 
50  static bool field_sensitive(
51  const irep_idt &id,
52  const typet &type,
53  const namespacet &);
54 
57  unsigned location_number;
58 
62 
63  typedef irep_idt idt;
64 
68  bool offset_is_zero(const offsett &offset) const
69  {
70  return offset && offset->is_zero();
71  }
72 
81  {
82  typedef std::map<object_numberingt::number_type, offsett> data_typet;
84 
85  public:
86  // NOLINTNEXTLINE(readability/identifiers)
87  typedef data_typet::iterator iterator;
88  // NOLINTNEXTLINE(readability/identifiers)
89  typedef data_typet::const_iterator const_iterator;
90  // NOLINTNEXTLINE(readability/identifiers)
91  typedef data_typet::value_type value_type;
92  // NOLINTNEXTLINE(readability/identifiers)
93  typedef data_typet::key_type key_type;
94 
95  iterator begin() { return data.begin(); }
96  const_iterator begin() const { return data.begin(); }
97  const_iterator cbegin() const { return data.cbegin(); }
98 
99  iterator end() { return data.end(); }
100  const_iterator end() const { return data.end(); }
101  const_iterator cend() const { return data.cend(); }
102 
103  size_t size() const { return data.size(); }
104  bool empty() const { return data.empty(); }
105 
106  void erase(key_type i) { data.erase(i); }
107  void erase(const_iterator it) { data.erase(it); }
108 
110  {
111  return data[i];
112  }
114  {
115  return data.at(i);
116  }
117  const offsett &at(key_type i) const
118  {
119  return data.at(i);
120  }
121 
122  template <typename It>
123  void insert(It b, It e) { data.insert(b, e); }
124 
125  template <typename T>
126  const_iterator find(T &&t) const { return data.find(std::forward<T>(t)); }
127 
128  static const object_map_dt blank;
129 
130  object_map_dt()=default;
131 
132  bool operator==(const object_map_dt &other) const
133  {
134  return data==other.data;
135  }
136  bool operator!=(const object_map_dt &other) const
137  {
138  return !(*this==other);
139  }
140 
141  protected:
142  ~object_map_dt()=default;
143  };
144 
149  exprt to_expr(const object_map_dt::value_type &it) const;
150 
164 
170  void set(object_mapt &dest, const object_map_dt::value_type &it) const
171  {
172  dest.write()[it.first]=it.second;
173  }
174 
181  bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
182  {
183  return insert(dest, it.first, it.second);
184  }
185 
191  bool insert(object_mapt &dest, const exprt &src) const
192  {
193  return insert(dest, object_numbering.number(src), offsett());
194  }
195 
202  bool insert(
203  object_mapt &dest,
204  const exprt &src,
205  const mp_integer &offset_value) const
206  {
207  return insert(dest, object_numbering.number(src), offsett(offset_value));
208  }
209 
217  bool insert(
218  object_mapt &dest,
220  const offsett &offset) const;
221 
228  bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
229  {
230  return insert(dest, object_numbering.number(expr), offset);
231  }
232 
237  struct entryt
238  {
241  std::string suffix;
242 
244  {
245  }
246 
247  entryt(const idt &_identifier, const std::string &_suffix):
248  identifier(_identifier),
249  suffix(_suffix)
250  {
251  }
252 
253  bool operator==(const entryt &other) const
254  {
255  return
256  identifier==other.identifier &&
257  suffix==other.suffix &&
258  object_map==other.object_map;
259  }
260  bool operator!=(const entryt &other) const
261  {
262  return !(*this==other);
263  }
264  };
265 
268  typedef std::set<exprt> expr_sett;
269 
273  typedef std::set<unsigned int> dynamic_object_id_sett;
274 
288  #ifdef USE_DSTRING
289  typedef std::map<idt, entryt> valuest;
290  #else
291  typedef std::unordered_map<idt, entryt, string_hash> valuest;
292  #endif
293 
299  void get_value_set(
300  const exprt &expr,
301  value_setst::valuest &dest,
302  const namespacet &ns) const;
303 
305  expr_sett &get(
306  const idt &identifier,
307  const std::string &suffix);
308 
310  void make_any()
311  {
312  values.clear();
313  }
314 
315  void clear()
316  {
317  values.clear();
318  }
319 
330  entryt &get_entry(
331  const entryt &e, const typet &type,
332  const namespacet &ns);
333 
337  void output(
338  const namespacet &ns,
339  std::ostream &out) const;
340 
344 
349  bool make_union(object_mapt &dest, const object_mapt &src) const;
350 
354  bool make_union(const valuest &new_values);
355 
358  bool make_union(const value_sett &new_values)
359  {
360  return make_union(new_values.values);
361  }
362 
368  void guard(
369  const exprt &expr,
370  const namespacet &ns);
371 
379  const codet &code,
380  const namespacet &ns)
381  {
382  apply_code_rec(code, ns);
383  }
384 
398  void assign(
399  const exprt &lhs,
400  const exprt &rhs,
401  const namespacet &ns,
402  bool is_simplified,
403  bool add_to_sets);
404 
412  void do_function_call(
413  const irep_idt &function,
414  const exprt::operandst &arguments,
415  const namespacet &ns);
416 
424  void do_end_function(
425  const exprt &lhs,
426  const namespacet &ns);
427 
435  void get_reference_set(
436  const exprt &expr,
437  value_setst::valuest &dest,
438  const namespacet &ns) const;
439 
449  bool eval_pointer_offset(
450  exprt &expr,
451  const namespacet &ns) const;
452 
453 protected:
460  void get_value_set(
461  const exprt &expr,
462  object_mapt &dest,
463  const namespacet &ns,
464  bool is_simplified) const;
465 
469  const exprt &expr,
470  object_mapt &dest,
471  const namespacet &ns) const
472  {
473  get_reference_set_rec(expr, dest, ns);
474  }
475 
478  const exprt &expr,
479  object_mapt &dest,
480  const namespacet &ns) const;
481 
483  void dereference_rec(
484  const exprt &src,
485  exprt &dest) const;
486 
490  void do_free(
491  const exprt &op,
492  const namespacet &ns);
493 
501  const exprt &src,
502  const irep_idt &component_name,
503  const namespacet &ns);
504 
505  // Subclass customisation points:
506 
507 protected:
509  virtual void get_value_set_rec(
510  const exprt &expr,
511  object_mapt &dest,
512  const std::string &suffix,
513  const typet &original_type,
514  const namespacet &ns) const;
515 
517  virtual void assign_rec(
518  const exprt &lhs,
519  const object_mapt &values_rhs,
520  const std::string &suffix,
521  const namespacet &ns,
522  bool add_to_sets);
523 
525  virtual void apply_code_rec(
526  const codet &code,
527  const namespacet &ns);
528 
529  private:
535  const exprt &rhs,
536  const namespacet &,
537  object_mapt &rhs_values) const
538  {
539  }
540 
546  const exprt &lhs,
547  const exprt &rhs,
548  const namespacet &)
549  {
550  }
551 };
552 
553 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H
virtual void apply_assign_side_effects(const exprt &lhs, const exprt &rhs, const namespacet &)
Subclass customisation point to apply global side-effects to this domain, after RHS values are read b...
Definition: value_set.h:545
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:202
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:68
Represents a row of a value_sett.
Definition: value_set.h:237
object_mapt object_map
Definition: value_set.h:239
void erase(key_type i)
Definition: value_set.h:106
entryt(const idt &_identifier, const std::string &_suffix)
Definition: value_set.h:247
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:1153
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:1556
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See get_reference_set.
Definition: value_set.cpp:991
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:128
const_iterator end() const
Definition: value_set.h:100
static object_numberingt object_numbering
Global shared object numbering, used to abbreviate expressions stored in value sets.
Definition: value_set.h:61
void insert(It b, It e)
Definition: value_set.h:123
void dereference_rec(const exprt &src, exprt &dest) const
Sets dest to src with any wrapping typecasts removed.
Definition: value_set.cpp:958
virtual void adjust_assign_rhs_values(const exprt &rhs, const namespacet &, 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:534
const_iterator cend() const
Definition: value_set.h:101
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:1361
std::map< object_numberingt::number_type, offsett > data_typet
Definition: value_set.h:82
offsett & operator[](key_type i)
Definition: value_set.h:109
const_iterator begin() const
Definition: value_set.h:96
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:63
bool operator!=(const entryt &other) const
Definition: value_set.h:260
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:117
std::set< exprt > expr_sett
Set of expressions; only used for the get API, not for internal data representation.
Definition: value_set.h:268
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:91
bool operator==(const entryt &other) const
Definition: value_set.h:253
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:1498
TO_BE_DOCUMENTED.
Definition: namespace.h:74
data_typet::const_iterator const_iterator
Definition: value_set.h:89
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value...
Definition: value_set.h:67
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:371
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:191
virtual ~value_sett()=default
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:310
bool operator!=(const object_map_dt &other) const
Definition: value_set.h:136
const_iterator cbegin() const
Definition: value_set.h:97
std::vector< exprt > operandst
Definition: expr.h:45
const_iterator find(T &&t) const
Definition: value_set.h:126
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:181
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:291
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:1544
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:228
void erase(const_iterator it)
Definition: value_set.h:107
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:976
Base class for all expressions.
Definition: expr.h:42
Reference Counting.
bool operator==(const object_map_dt &other) const
Definition: value_set.h:132
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:273
Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances)...
Definition: value_set.h:80
value_sett()
Definition: value_set.h:44
void clear()
Definition: value_set.h:315
bool make_union(const value_sett &new_values)
Merges an entire existing value_sett&#39;s data into this one.
Definition: value_set.h:358
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:113
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:87
void guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
Definition: value_set.cpp:1689
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:1281
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:468
std::string suffix
Definition: value_set.h:241
valuest values
Stores the LHS ID -> RHS expression set map.
Definition: value_set.h:343
void apply_code(const codet &code, const namespacet &ns)
Transforms this value-set by executing a given statement against it.
Definition: value_set.h:378
size_t size() const
Definition: value_set.h:103
data_typet::key_type key_type
Definition: value_set.h:93
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:57
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:163
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:1723