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 
309  void clear()
310  {
311  values.clear();
312  }
313 
321  const entryt *find_entry(const idt &id) const;
322 
333  entryt &get_entry(
334  const entryt &e, const typet &type,
335  const namespacet &ns);
336 
340  void output(
341  const namespacet &ns,
342  std::ostream &out) const;
343 
347 
352  bool make_union(object_mapt &dest, const object_mapt &src) const;
353 
357  bool make_union(const valuest &new_values);
358 
361  bool make_union(const value_sett &new_values)
362  {
363  return make_union(new_values.values);
364  }
365 
371  void guard(
372  const exprt &expr,
373  const namespacet &ns);
374 
382  const codet &code,
383  const namespacet &ns)
384  {
385  apply_code_rec(code, ns);
386  }
387 
401  void assign(
402  const exprt &lhs,
403  const exprt &rhs,
404  const namespacet &ns,
405  bool is_simplified,
406  bool add_to_sets);
407 
415  void do_function_call(
416  const irep_idt &function,
417  const exprt::operandst &arguments,
418  const namespacet &ns);
419 
427  void do_end_function(
428  const exprt &lhs,
429  const namespacet &ns);
430 
438  void get_reference_set(
439  const exprt &expr,
440  value_setst::valuest &dest,
441  const namespacet &ns) const;
442 
452  bool eval_pointer_offset(
453  exprt &expr,
454  const namespacet &ns) const;
455 
456 protected:
463  void get_value_set(
464  const exprt &expr,
465  object_mapt &dest,
466  const namespacet &ns,
467  bool is_simplified) const;
468 
472  const exprt &expr,
473  object_mapt &dest,
474  const namespacet &ns) const
475  {
476  get_reference_set_rec(expr, dest, ns);
477  }
478 
481  const exprt &expr,
482  object_mapt &dest,
483  const namespacet &ns) const;
484 
486  void dereference_rec(
487  const exprt &src,
488  exprt &dest) const;
489 
497  const exprt &src,
498  const irep_idt &component_name,
499  const namespacet &ns);
500 
501  // Subclass customisation points:
502 
503 protected:
505  virtual void get_value_set_rec(
506  const exprt &expr,
507  object_mapt &dest,
508  const std::string &suffix,
509  const typet &original_type,
510  const namespacet &ns) const;
511 
513  virtual void assign_rec(
514  const exprt &lhs,
515  const object_mapt &values_rhs,
516  const std::string &suffix,
517  const namespacet &ns,
518  bool add_to_sets);
519 
521  virtual void apply_code_rec(
522  const codet &code,
523  const namespacet &ns);
524 
525  private:
531  const exprt &rhs,
532  const namespacet &,
533  object_mapt &rhs_values) const
534  {
535  // unused parameters
536  (void)rhs;
537  (void)rhs_values;
538  }
539 
545  const exprt &lhs,
546  const exprt &rhs,
547  const namespacet &)
548  {
549  // unused parameters
550  (void)lhs;
551  (void)rhs;
552  }
553 };
554 
555 #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:544
The type of an expression, extends irept.
Definition: type.h:27
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:1151
expr_sett & get(const idt &identifier, const std::string &suffix)
Appears to be unimplemented.
Object Numbering.
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
Definition: value_set.cpp:252
virtual void apply_code_rec(const codet &code, const namespacet &ns)
Subclass customisation point for applying code to this domain:
Definition: value_set.cpp:1468
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See get_reference_set.
Definition: value_set.cpp:993
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:320
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:960
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:530
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:1273
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:267
Value Set Propagation.
const entryt * find_entry(const idt &id) const
Finds an entry in this value-set.
Definition: value_set.cpp:54
idt
Definition: irep_ids.cpp:30
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:1410
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
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:378
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:35
typename Map::mapped_type number_type
Definition: numbering.h:24
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:57
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's return value to a given LHS expression.
Definition: value_set.cpp:1456
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:978
Base class for all expressions.
Definition: expr.h:54
Reference Counting.
void set(object_mapt &dest, const object_map_dt::value_type &it) const
Sets an entry in object map dest to match an existing entry it from a different map.
Definition: value_set.h:170
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:309
bool make_union(const value_sett &new_values)
Merges an entire existing value_sett's data into this one.
Definition: value_set.h:361
void output(const namespacet &ns, std::ostream &out) const
Pretty-print this value-set.
Definition: value_set.cpp:103
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
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:193
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:61
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:1591
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:471
std::string suffix
Definition: value_set.h:241
valuest values
Stores the LHS ID -> RHS expression set map.
Definition: value_set.h:346
void apply_code(const codet &code, const namespacet &ns)
Transforms this value-set by executing a given statement against it.
Definition: value_set.h:381
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' 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:1625