cprover
Loading...
Searching...
No Matches
value_set.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set
4
5Author: 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 <unordered_set>
16
17#include <util/mp_arith.h>
19#include <util/sharing_map.h>
20
21#include "object_numbering.h"
22#include "value_sets.h"
23
24class namespacet;
25
43{
44public:
48
50 : location_number(other.location_number), values(std::move(other.values))
51 {
52 }
53
54 virtual ~value_sett() = default;
55
56 value_sett(const value_sett &other) = default;
57
58 value_sett &operator=(const value_sett &other) = delete;
59
61 {
62 values = std::move(other.values);
63 return *this;
64 }
65
68 virtual bool field_sensitive(const irep_idt &id, const typet &type);
69
73
77
81
87 using object_map_dt = std::map<object_numberingt::number_type, offsett>;
88
90
95 exprt to_expr(const object_map_dt::value_type &it) const;
96
110
116 void set(object_mapt &dest, const object_map_dt::value_type &it) const
117 {
118 dest.write()[it.first]=it.second;
119 }
120
127 bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
128 {
129 return insert(dest, it.first, it.second);
130 }
131
137 bool insert(object_mapt &dest, const exprt &src) const
138 {
139 return insert(dest, object_numbering.number(src), offsett());
140 }
141
148 bool insert(
150 const exprt &src,
151 const mp_integer &offset_value) const
152 {
153 return insert(dest, object_numbering.number(src), offsett(offset_value));
154 }
155
163 bool insert(
166 const offsett &offset) const;
167
168 enum class insert_actiont
169 {
170 INSERT,
172 NONE
173 };
174
182 const object_mapt &dest,
184 const offsett &offset) const;
185
192 bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
193 {
194 return insert(dest, object_numbering.number(expr), offset);
195 }
196
201 struct entryt
202 {
205 std::string suffix;
206
208 {
209 }
210
211 entryt(const irep_idt &_identifier, const std::string &_suffix)
212 : identifier(_identifier), suffix(_suffix)
213 {
214 }
215
216 bool operator==(const entryt &other) const
217 {
218 // Note that the object_map comparison below is duplicating the code of
219 // operator== defined in reference_counting.h because old versions of
220 // clang (3.7 and 3.8) do not resolve the template instantiation correctly
221 return identifier == other.identifier && suffix == other.suffix &&
222 (object_map.get_d() == other.object_map.get_d() ||
223 object_map.read() == other.object_map.read());
224 }
225 bool operator!=(const entryt &other) const
226 {
227 return !(*this==other);
228 }
229 };
230
245
252 std::vector<exprt> get_value_set(exprt expr, const namespacet &ns) const;
253
254 void clear()
255 {
256 values.clear();
257 }
258
265 const entryt *find_entry(const irep_idt &id) const;
266
279 void update_entry(
280 const entryt &e,
281 const typet &type,
282 const object_mapt &new_values,
283 bool add_to_sets);
284
288 void output(std::ostream &out, const std::string &indent = "") const;
289
293
298 bool make_union(object_mapt &dest, const object_mapt &src) const;
299
304 bool make_union_would_change(const object_mapt &dest, const object_mapt &src)
305 const;
306
310 bool make_union(const valuest &new_values);
311
315 {
316 return make_union(new_values.values);
317 }
318
324 void guard(
325 const exprt &expr,
326 const namespacet &ns);
327
335 const codet &code,
336 const namespacet &ns)
337 {
338 apply_code_rec(code, ns);
339 }
340
354 void assign(
355 const exprt &lhs,
356 const exprt &rhs,
357 const namespacet &ns,
358 bool is_simplified,
359 bool add_to_sets);
360
368 void do_function_call(
369 const irep_idt &function,
370 const exprt::operandst &arguments,
371 const namespacet &ns);
372
380 void do_end_function(
381 const exprt &lhs,
382 const namespacet &ns);
383
392 const exprt &expr,
394 const namespacet &ns) const;
395
406 exprt &expr,
407 const namespacet &ns) const;
408
417 irep_idt identifier,
418 const typet &type,
419 const std::string &suffix,
420 const namespacet &ns) const;
421
427 const irep_idt &index,
428 const std::unordered_set<exprt, irep_hash> &values_to_erase);
429
430 void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns);
431
432protected:
440 get_value_set(exprt expr, const namespacet &ns, bool is_simplified) const;
441
445 const exprt &expr,
447 const namespacet &ns) const
448 {
449 get_reference_set_rec(expr, dest, ns);
450 }
451
454 const exprt &expr,
456 const namespacet &ns) const;
457
459 void dereference_rec(
460 const exprt &src,
461 exprt &dest) const;
462
463 void erase_symbol_rec(
464 const typet &type,
465 const std::string &erase_prefix,
466 const namespacet &ns);
467
470 const std::string &erase_prefix,
471 const namespacet &ns);
472
473 // Subclass customisation points:
474
475protected:
477 virtual void get_value_set_rec(
478 const exprt &expr,
480 const std::string &suffix,
481 const typet &original_type,
482 const namespacet &ns) const;
483
485 virtual void assign_rec(
486 const exprt &lhs,
487 const object_mapt &values_rhs,
488 const std::string &suffix,
489 const namespacet &ns,
490 bool add_to_sets);
491
493 virtual void apply_code_rec(
494 const codet &code,
495 const namespacet &ns);
496
497 private:
503 const exprt &rhs,
504 const namespacet &,
505 object_mapt &rhs_values) const
506 {
507 // unused parameters
508 (void)rhs;
510 }
511
517 const exprt &lhs,
518 const exprt &rhs,
519 const namespacet &)
520 {
521 // unused parameters
522 (void)lhs;
523 (void)rhs;
524 }
525};
526
527#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
const T & read() const
void clear()
Clear map.
Base type for structs and unions.
Definition std_types.h:62
Expression to hold a symbol (variable)
Definition std_expr.h:80
The type of an expression, extends irept.
Definition type.h:29
std::list< exprt > valuest
Definition value_sets.h:28
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition value_set.h:43
virtual void apply_code_rec(const codet &code, const namespacet &ns)
Subclass customisation point for applying code to this domain:
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:244
bool make_union(const value_sett &new_values)
Merges an entire existing value_sett's data into this one.
Definition value_set.h:314
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.
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...
const entryt * find_entry(const irep_idt &id) const
Finds an entry in this value-set.
Definition value_set.cpp:55
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
value_sett(value_sett &&other)
Definition value_set.h:49
void output(std::ostream &out, const std::string &indent="") const
Pretty-print this value-set.
void dereference_rec(const exprt &src, exprt &dest) const
Sets dest to src with any wrapping typecasts removed.
void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns)
valuest values
Stores the LHS ID -> RHS expression set map.
Definition value_set.h:292
unsigned location_number
Matches the location_number field of the instruction that corresponds to this value_sett instance in ...
Definition value_set.h:72
void clear()
Definition value_set.h:254
value_sett(const value_sett &other)=default
static object_numberingt object_numbering
Global shared object numbering, used to abbreviate expressions stored in value sets.
Definition value_set.h:76
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:127
void erase_struct_union_symbol(const struct_union_typet &struct_union_type, const std::string &erase_prefix, const namespacet &ns)
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See get_reference_set.
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:148
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 ....
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.
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:61
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.
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:192
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:109
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:
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...
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:116
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
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:43
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
Definition value_set.h:80
void guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
value_sett & operator=(value_sett &&other)
Definition value_set.h:60
virtual ~value_sett()=default
value_sett & operator=(const value_sett &other)=delete
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.
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.
static const object_map_dt empty_object_map
Definition value_set.h:40
bool insert(object_mapt &dest, const exprt &src) const
Adds an expression to an object map, with unknown offset.
Definition value_set.h:137
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...
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:444
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:
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.
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:516
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:87
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:502
void apply_code(const codet &code, const namespacet &ns)
Transforms this value-set by executing a given statement against it.
Definition value_set.h:334
void erase_symbol_rec(const typet &type, const std::string &erase_prefix, const namespacet &ns)
STL namespace.
Object Numbering.
Reference Counting.
Sharing map.
Represents a row of a value_sett.
Definition value_set.h:202
irep_idt identifier
Definition value_set.h:204
entryt(const irep_idt &_identifier, const std::string &_suffix)
Definition value_set.h:211
bool operator!=(const entryt &other) const
Definition value_set.h:225
std::string suffix
Definition value_set.h:205
bool operator==(const entryt &other) const
Definition value_set.h:216
object_mapt object_map
Definition value_set.h:203
Value Set Propagation.