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  DEPRECATED(SINCE(2019, 05, 22, "Unused"))
84  bool offset_is_zero(const offsett &offset) const
85  {
86  return offset && offset->is_zero();
87  }
88 
94  using object_map_dt = std::map<object_numberingt::number_type, offsett>;
95 
97 
102  exprt to_expr(const object_map_dt::value_type &it) const;
103 
117 
123  void set(object_mapt &dest, const object_map_dt::value_type &it) const
124  {
125  dest.write()[it.first]=it.second;
126  }
127 
134  bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
135  {
136  return insert(dest, it.first, it.second);
137  }
138 
144  bool insert(object_mapt &dest, const exprt &src) const
145  {
146  return insert(dest, object_numbering.number(src), offsett());
147  }
148 
155  bool insert(
156  object_mapt &dest,
157  const exprt &src,
158  const mp_integer &offset_value) const
159  {
160  return insert(dest, object_numbering.number(src), offsett(offset_value));
161  }
162 
170  bool insert(
171  object_mapt &dest,
173  const offsett &offset) const;
174 
175  enum class insert_actiont
176  {
177  INSERT,
178  RESET_OFFSET,
179  NONE
180  };
181 
189  const object_mapt &dest,
191  const offsett &offset) const;
192 
199  bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
200  {
201  return insert(dest, object_numbering.number(expr), offset);
202  }
203 
208  struct entryt
209  {
212  std::string suffix;
213 
215  {
216  }
217 
218  entryt(const irep_idt &_identifier, const std::string &_suffix)
219  : identifier(_identifier), suffix(_suffix)
220  {
221  }
222 
223  bool operator==(const entryt &other) const
224  {
225  // Note that the object_map comparison below is duplicating the code of
226  // operator== defined in reference_counting.h because old versions of
227  // clang (3.7 and 3.8) do not resolve the template instantiation correctly
228  return identifier == other.identifier && suffix == other.suffix &&
229  (object_map.get_d() == other.object_map.get_d() ||
230  object_map.read() == other.object_map.read());
231  }
232  bool operator!=(const entryt &other) const
233  {
234  return !(*this==other);
235  }
236  };
237 
240  DEPRECATED(SINCE(2019, 05, 22, "Only used in deprecated function"))
241  typedef std::set<exprt> expr_sett;
242 
246  DEPRECATED(SINCE(2019, 05, 22, "Unused"))
247  typedef std::set<unsigned int> dynamic_object_id_sett;
248 
263 
266  DEPRECATED(
267  SINCE(2019, 05, 22, "Use get_value_set(exprt, const namespacet &) instead"))
268  void get_value_set(
269  exprt expr,
270  value_setst::valuest &dest,
271  const namespacet &ns) const;
272 
279  std::vector<exprt> get_value_set(exprt expr, const namespacet &ns) const;
280 
282  DEPRECATED(SINCE(2019, 05, 22, "Unimplemented"))
283  expr_sett &get(const irep_idt &identifier, const std::string &suffix);
284 
285  void clear()
286  {
287  values.clear();
288  }
289 
296  const entryt *find_entry(const irep_idt &id) const;
297 
310  void update_entry(
311  const entryt &e,
312  const typet &type,
313  const object_mapt &new_values,
314  bool add_to_sets);
315 
319  void output(std::ostream &out, const std::string &indent = "") const;
320 
321  DEPRECATED(SINCE(2019, 06, 11, "Use the version without ns argument"))
322  void output(
323  const namespacet &ns,
324  std::ostream &out,
325  const std::string &indent = "") const;
326 
330 
335  bool make_union(object_mapt &dest, const object_mapt &src) const;
336 
341  bool make_union_would_change(const object_mapt &dest, const object_mapt &src)
342  const;
343 
347  bool make_union(const valuest &new_values);
348 
351  bool make_union(const value_sett &new_values)
352  {
353  return make_union(new_values.values);
354  }
355 
361  void guard(
362  const exprt &expr,
363  const namespacet &ns);
364 
372  const codet &code,
373  const namespacet &ns)
374  {
375  apply_code_rec(code, ns);
376  }
377 
391  void assign(
392  const exprt &lhs,
393  const exprt &rhs,
394  const namespacet &ns,
395  bool is_simplified,
396  bool add_to_sets);
397 
405  void do_function_call(
406  const irep_idt &function,
407  const exprt::operandst &arguments,
408  const namespacet &ns);
409 
417  void do_end_function(
418  const exprt &lhs,
419  const namespacet &ns);
420 
428  void get_reference_set(
429  const exprt &expr,
430  value_setst::valuest &dest,
431  const namespacet &ns) const;
432 
442  bool eval_pointer_offset(
443  exprt &expr,
444  const namespacet &ns) const;
445 
454  irep_idt identifier,
455  const typet &type,
456  const std::string &suffix,
457  const namespacet &ns) const;
458 
464  const irep_idt &index,
465  const std::unordered_set<exprt, irep_hash> &values_to_erase);
466 
467  void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns);
468 
469 protected:
472  DEPRECATED(
473  SINCE(2019, 05, 22, "Use the version returning object_mapt instead"))
474  void get_value_set(
475  exprt expr,
476  object_mapt &dest,
477  const namespacet &ns,
478  bool is_simplified) const;
479 
487  get_value_set(exprt expr, const namespacet &ns, bool is_simplified) const;
488 
492  const exprt &expr,
493  object_mapt &dest,
494  const namespacet &ns) const
495  {
496  get_reference_set_rec(expr, dest, ns);
497  }
498 
501  const exprt &expr,
502  object_mapt &dest,
503  const namespacet &ns) const;
504 
506  void dereference_rec(
507  const exprt &src,
508  exprt &dest) const;
509 
510  void erase_symbol_rec(
511  const typet &type,
512  const std::string &erase_prefix,
513  const namespacet &ns);
514 
516  const struct_union_typet &struct_union_type,
517  const std::string &erase_prefix,
518  const namespacet &ns);
519 
520  // Subclass customisation points:
521 
522 protected:
524  virtual void get_value_set_rec(
525  const exprt &expr,
526  object_mapt &dest,
527  const std::string &suffix,
528  const typet &original_type,
529  const namespacet &ns) const;
530 
532  virtual void assign_rec(
533  const exprt &lhs,
534  const object_mapt &values_rhs,
535  const std::string &suffix,
536  const namespacet &ns,
537  bool add_to_sets);
538 
540  virtual void apply_code_rec(
541  const codet &code,
542  const namespacet &ns);
543 
544  private:
550  const exprt &rhs,
551  const namespacet &,
552  object_mapt &rhs_values) const
553  {
554  // unused parameters
555  (void)rhs;
556  (void)rhs_values;
557  }
558 
564  const exprt &lhs,
565  const exprt &rhs,
566  const namespacet &)
567  {
568  // unused parameters
569  (void)lhs;
570  (void)rhs;
571  }
572 };
573 
574 #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:371
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:1749
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:275
value_sett::get_value_set
void get_value_set(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:359
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:1525
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:1019
sharing_mapt
A map implemented as a tree where subtrees can be shared between different maps.
Definition: sharing_map.h:180
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:211
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:1203
typet
The type of an expression, extends irept.
Definition: type.h:29
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:57
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:1714
template_numberingt
Definition: numbering.h:22
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:155
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::offset_is_zero
bool offset_is_zero(const offsett &offset) const
Definition: value_set.h:84
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:1338
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:53
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:308
value_sett::insert_actiont::RESET_OFFSET
@ RESET_OFFSET
value_sett::get
expr_sett & get(const irep_idt &identifier, const std::string &suffix)
Appears to be unimplemented.
value_sett::entryt::entryt
entryt(const irep_idt &_identifier, const std::string &_suffix)
Definition: value_set.h:218
value_sett::entryt::object_map
object_mapt object_map
Definition: value_set.h:210
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
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:549
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:293
template_numberingt::number
number_type number(const key_type &a)
Definition: numbering.h:37
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:1049
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:116
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:176
value_sett::expr_sett
std::set< exprt > expr_sett
Set of expressions; only used for the get API, not for internal data representation.
Definition: value_set.h:241
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:96
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:144
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:1732
value_sett::entryt::entryt
entryt()
Definition: value_set.h:214
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:1467
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:94
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:199
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
reference_counting< object_map_dt, empty_object_map >
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
sharing_mapt::clear
void clear()
Clear map.
Definition: sharing_map.h:343
value_sett::dynamic_object_id_sett
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:247
template_numberingt::number_type
typename Map::mapped_type number_type
Definition: numbering.h:24
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:487
value_sett::entryt::suffix
std::string suffix
Definition: value_set.h:212
value_setst
Definition: value_sets.h:22
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:144
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:134
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
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:1513
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:436
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:1034
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:232
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:123
value_sett::entryt
Represents a row of a value_sett.
Definition: value_set.h:209
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:1679
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:223
value_sett::entryt::operator==
bool operator==(const entryt &other) const
Definition: value_set.h:223
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:563
value_sett::guard
void guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
Definition: value_set.cpp:1647
value_sett::value_sett
value_sett()
Definition: value_set.h:47
value_sett::clear
void clear()
Definition: value_set.h:285
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:329