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 #include <type_traits>
17 #include <unordered_set>
18 
19 #include <util/mp_arith.h>
21 #include <util/sharing_map.h>
22 
23 #include "object_numbering.h"
24 #include "value_sets.h"
25 
26 class namespacet;
27 
45 {
46 public:
48  {
49  }
50 
52  : location_number(other.location_number), values(std::move(other.values))
53  {
54  }
55 
56  virtual ~value_sett() = default;
57 
58  value_sett(const value_sett &other) = default;
59 
60  value_sett &operator=(const value_sett &other) = delete;
61 
63  {
64  values = std::move(other.values);
65  return *this;
66  }
67 
70  virtual bool field_sensitive(const irep_idt &id, const typet &type);
71 
74  unsigned location_number;
75 
79 
83 
89  using object_map_dt = std::map<object_numberingt::number_type, offsett>;
90 
92 
97  exprt to_expr(const object_map_dt::value_type &it) const;
98 
112 
118  void set(object_mapt &dest, const object_map_dt::value_type &it) const
119  {
120  dest.write()[it.first]=it.second;
121  }
122 
129  bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
130  {
131  return insert(dest, it.first, it.second);
132  }
133 
139  bool insert(object_mapt &dest, const exprt &src) const
140  {
141  return insert(dest, object_numbering.number(src), offsett());
142  }
143 
150  bool insert(
151  object_mapt &dest,
152  const exprt &src,
153  const mp_integer &offset_value) const
154  {
155  return insert(dest, object_numbering.number(src), offsett(offset_value));
156  }
157 
165  bool insert(
166  object_mapt &dest,
168  const offsett &offset) const;
169 
170  enum class insert_actiont
171  {
172  INSERT,
173  RESET_OFFSET,
174  NONE
175  };
176 
184  const object_mapt &dest,
186  const offsett &offset) const;
187 
194  bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
195  {
196  return insert(dest, object_numbering.number(expr), offset);
197  }
198 
203  struct entryt
204  {
207  std::string suffix;
208 
210  {
211  }
212 
213  entryt(const irep_idt &_identifier, const std::string &_suffix)
214  : identifier(_identifier), suffix(_suffix)
215  {
216  }
217 
218  bool operator==(const entryt &other) const
219  {
220  // Note that the object_map comparison below is duplicating the code of
221  // operator== defined in reference_counting.h because old versions of
222  // clang (3.7 and 3.8) do not resolve the template instantiation correctly
223  return identifier == other.identifier && suffix == other.suffix &&
224  (object_map.get_d() == other.object_map.get_d() ||
225  object_map.read() == other.object_map.read());
226  }
227  bool operator!=(const entryt &other) const
228  {
229  return !(*this==other);
230  }
231  };
232 
247 
254  std::vector<exprt> get_value_set(exprt expr, const namespacet &ns) const;
255 
256  void clear()
257  {
258  values.clear();
259  }
260 
267  const entryt *find_entry(const irep_idt &id) const;
268 
281  void update_entry(
282  const entryt &e,
283  const typet &type,
284  const object_mapt &new_values,
285  bool add_to_sets);
286 
290  void output(std::ostream &out, const std::string &indent = "") const;
291 
295 
300  bool make_union(object_mapt &dest, const object_mapt &src) const;
301 
306  bool make_union_would_change(const object_mapt &dest, const object_mapt &src)
307  const;
308 
312  bool make_union(const valuest &new_values);
313 
316  bool make_union(const value_sett &new_values)
317  {
318  return make_union(new_values.values);
319  }
320 
326  void guard(
327  const exprt &expr,
328  const namespacet &ns);
329 
337  const codet &code,
338  const namespacet &ns)
339  {
340  apply_code_rec(code, ns);
341  }
342 
356  void assign(
357  const exprt &lhs,
358  const exprt &rhs,
359  const namespacet &ns,
360  bool is_simplified,
361  bool add_to_sets);
362 
370  void do_function_call(
371  const irep_idt &function,
372  const exprt::operandst &arguments,
373  const namespacet &ns);
374 
382  void do_end_function(
383  const exprt &lhs,
384  const namespacet &ns);
385 
393  void get_reference_set(
394  const exprt &expr,
395  value_setst::valuest &dest,
396  const namespacet &ns) const;
397 
407  bool eval_pointer_offset(
408  exprt &expr,
409  const namespacet &ns) const;
410 
419  irep_idt identifier,
420  const typet &type,
421  const std::string &suffix,
422  const namespacet &ns) const;
423 
429  const irep_idt &index,
430  const std::unordered_set<exprt, irep_hash> &values_to_erase);
431 
432  void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns);
433 
434 protected:
442  get_value_set(exprt expr, const namespacet &ns, bool is_simplified) const;
443 
447  const exprt &expr,
448  object_mapt &dest,
449  const namespacet &ns) const
450  {
451  get_reference_set_rec(expr, dest, ns);
452  }
453 
456  const exprt &expr,
457  object_mapt &dest,
458  const namespacet &ns) const;
459 
461  void dereference_rec(
462  const exprt &src,
463  exprt &dest) const;
464 
465  void erase_symbol_rec(
466  const typet &type,
467  const std::string &erase_prefix,
468  const namespacet &ns);
469 
471  const struct_union_typet &struct_union_type,
472  const std::string &erase_prefix,
473  const namespacet &ns);
474 
475  // Subclass customisation points:
476 
477 protected:
479  virtual void get_value_set_rec(
480  const exprt &expr,
481  object_mapt &dest,
482  const std::string &suffix,
483  const typet &original_type,
484  const namespacet &ns) const;
485 
487  virtual void assign_rec(
488  const exprt &lhs,
489  const object_mapt &values_rhs,
490  const std::string &suffix,
491  const namespacet &ns,
492  bool add_to_sets);
493 
495  virtual void apply_code_rec(
496  const codet &code,
497  const namespacet &ns);
498 
499  private:
505  const exprt &rhs,
506  const namespacet &,
507  object_mapt &rhs_values) const
508  {
509  // unused parameters
510  (void)rhs;
511  (void)rhs_values;
512  }
513 
519  const exprt &lhs,
520  const exprt &rhs,
521  const namespacet &)
522  {
523  // unused parameters
524  (void)lhs;
525  (void)rhs;
526  }
527 };
528 
529 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H
value_sett::apply_code
void apply_code(const codet &code, const namespacet &ns)
Transforms this value-set by executing a given statement against it.
Definition: value_set.h:336
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
value_sett::erase_symbol
void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns)
Definition: value_set.cpp:1713
value_sett::make_union_would_change
bool make_union_would_change(const object_mapt &dest, const object_mapt &src) const
Determines whether merging two RHS expression sets would cause any change.
Definition: value_set.cpp:267
value_sett::apply_code_rec
virtual void apply_code_rec(const codet &code, const namespacet &ns)
Subclass customisation point for applying code to this domain:
Definition: value_set.cpp:1489
value_sett::location_number
unsigned location_number
Matches the location_number field of the instruction that corresponds to this value_sett instance in ...
Definition: value_set.h:74
mp_arith.h
value_sett::dereference_rec
void dereference_rec(const exprt &src, exprt &dest) const
Sets dest to src with any wrapping typecasts removed.
Definition: value_set.cpp:982
sharing_mapt< irep_idt, entryt >
value_sett::get_insert_action
insert_actiont get_insert_action(const object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
Determines what would happen if object number n was inserted into map dest with offset offset – the p...
Definition: value_set.cpp:98
value_sett::entryt::identifier
irep_idt identifier
Definition: value_set.h:206
value_sett::assign
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:1168
typet
The type of an expression, extends irept.
Definition: type.h:28
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:57
numberingt< exprt, irep_hash >
value_sett::find_entry
const entryt * find_entry(const irep_idt &id) const
Finds an entry in this value-set.
Definition: value_set.cpp:53
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
value_sett::erase_struct_union_symbol
void erase_struct_union_symbol(const struct_union_typet &struct_union_type, const std::string &erase_prefix, const namespacet &ns)
Definition: value_set.cpp:1678
value_sett::insert
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:150
value_sett::object_numbering
static object_numberingt object_numbering
Global shared object numbering, used to abbreviate expressions stored in value sets.
Definition: value_set.h:78
value_sett::assign_rec
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:1302
reference_counting::get_d
dt * get_d() const
Definition: reference_counting.h:114
value_sett
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:45
exprt
Base class for all expressions.
Definition: expr.h:54
object_numbering.h
Object Numbering.
value_sett::eval_pointer_offset
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:300
value_sett::insert_actiont::RESET_OFFSET
@ RESET_OFFSET
value_sett::entryt::entryt
entryt(const irep_idt &_identifier, const std::string &_suffix)
Definition: value_set.h:213
value_sett::entryt::object_map
object_mapt object_map
Definition: value_set.h:205
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
value_sett::adjust_assign_rhs_values
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:504
value_sett::operator=
value_sett & operator=(const value_sett &other)=delete
value_sett::make_union
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
Definition: value_set.cpp:285
value_sett::get_reference_set_rec
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See get_reference_set.
Definition: value_set.cpp:1012
value_sett::object_mapt
reference_counting< object_map_dt, empty_object_map > object_mapt
Reference-counts instances of object_map_dt, such that multiple instructions' value_sett instances ca...
Definition: value_set.h:111
value_sets.h
Value Set Propagation.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
value_sett::insert_actiont
insert_actiont
Definition: value_set.h:171
value_sett::~value_sett
virtual ~value_sett()=default
value_sett::empty_object_map
static const object_map_dt empty_object_map
Definition: value_set.h:91
value_setst::valuest
std::list< exprt > valuest
Definition: value_sets.h:28
value_sett::output
void output(std::ostream &out, const std::string &indent="") const
Pretty-print this value-set.
Definition: value_set.cpp:136
value_sett::get_value_set
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
Definition: value_set.cpp:352
value_sett::operator=
value_sett & operator=(value_sett &&other)
Definition: value_set.h:62
value_sett::erase_symbol_rec
void erase_symbol_rec(const typet &type, const std::string &erase_prefix, const namespacet &ns)
Definition: value_set.cpp:1696
value_sett::entryt::entryt
entryt()
Definition: value_set.h:209
value_sett::do_function_call
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:1431
value_sett::object_map_dt
std::map< object_numberingt::number_type, offsett > object_map_dt
Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances).
Definition: value_set.h:89
value_sett::insert
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:194
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
reference_counting< object_map_dt, empty_object_map >
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
sharing_mapt::clear
void clear()
Clear map.
Definition: sharing_map.h:366
value_sett::offsett
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
Definition: value_set.h:82
value_sett::get_value_set_rec
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:450
value_sett::entryt::suffix
std::string suffix
Definition: value_set.h:207
value_sett::insert
bool insert(object_mapt &dest, const exprt &src) const
Adds an expression to an object map, with unknown offset.
Definition: value_set.h:139
value_sett::valuest
sharing_mapt< irep_idt, entryt > valuest
Map representing the entire value set, mapping from string LHS IDs to RHS expression sets.
Definition: value_set.h:246
value_sett::insert
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
Merges an existing element into an object map.
Definition: value_set.h:129
value_sett::value_sett
value_sett(value_sett &&other)
Definition: value_set.h:51
value_sett::insert_actiont::INSERT
@ INSERT
value_sett::do_end_function
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:1477
numberingt::number
number_type number(const key_type &a)
Definition: numbering.h:37
value_sett::insert_actiont::NONE
@ NONE
reference_counting.h
Reference Counting.
value_sett::get_index_of_symbol
optionalt< irep_idt > get_index_of_symbol(irep_idt identifier, const typet &type, const std::string &suffix, const namespacet &ns) const
Get the index of the symbol and suffix.
Definition: value_set.cpp:396
value_sett::update_entry
void update_entry(const entryt &e, const typet &type, const object_mapt &new_values, bool add_to_sets)
Adds or replaces an entry in this value-set.
Definition: value_set.cpp:59
reference_counting::read
const T & read() const
Definition: reference_counting.h:69
value_sett::get_reference_set
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:997
value_sett::make_union
bool make_union(const value_sett &new_values)
Merges an entire existing value_sett's data into this one.
Definition: value_set.h:316
reference_counting::write
T & write()
Definition: reference_counting.h:76
value_sett::field_sensitive
virtual bool field_sensitive(const irep_idt &id, const typet &type)
Determines whether an identifier of a given type should have its fields distinguished.
Definition: value_set.cpp:41
value_sett::entryt::operator!=
bool operator!=(const entryt &other) const
Definition: value_set.h:227
value_sett::get_reference_set
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:446
value_sett::set
void set(object_mapt &dest, const object_map_dt::value_type &it) const
Sets an element in object map dest to match an existing element it from a different map.
Definition: value_set.h:118
value_sett::entryt
Represents a row of a value_sett.
Definition: value_set.h:204
value_sett::value_sett
value_sett(const value_sett &other)=default
value_sett::erase_values_from_entry
void erase_values_from_entry(const irep_idt &index, const std::unordered_set< exprt, irep_hash > &values_to_erase)
Update the entry stored at index by erasing any values listed in values_to_erase.
Definition: value_set.cpp:1643
sharing_map.h
Sharing map.
value_sett::to_expr
exprt to_expr(const object_map_dt::value_type &it) const
Converts an object_map_dt element object_number -> offset into an object_descriptor_exprt with ....
Definition: value_set.cpp:215
value_sett::entryt::operator==
bool operator==(const entryt &other) const
Definition: value_set.h:218
value_sett::apply_assign_side_effects
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:518
value_sett::guard
void guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
Definition: value_set.cpp:1611
value_sett::value_sett
value_sett()
Definition: value_set.h:47
numberingt< exprt, irep_hash >::number_type
std::size_t number_type
Definition: numbering.h:24
value_sett::clear
void clear()
Definition: value_set.h:256
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
value_sett::values
valuest values
Stores the LHS ID -> RHS expression set map.
Definition: value_set.h:294