CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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;
25class xmlt;
26
44{
45public:
49
51 : location_number(other.location_number), values(std::move(other.values))
52 {
53 }
54
55 virtual ~value_sett() = default;
56
57 value_sett(const value_sett &other) = default;
58
59 value_sett &operator=(const value_sett &other) = delete;
60
62 {
63 values = std::move(other.values);
64 return *this;
65 }
66
69 virtual bool field_sensitive(const irep_idt &id, const typet &type);
70
74
78
81 typedef std::optional<mp_integer> offsett;
82
88 using object_map_dt = std::map<object_numberingt::number_type, offsett>;
89
91
96 exprt to_expr(const object_map_dt::value_type &it) const;
97
111
117 void set(object_mapt &dest, const object_map_dt::value_type &it) const
118 {
119 dest.write()[it.first]=it.second;
120 }
121
128 bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
129 {
130 return insert(dest, it.first, it.second);
131 }
132
138 bool insert(object_mapt &dest, const exprt &src) const
139 {
140 return insert(dest, object_numbering.number(src), offsett());
141 }
142
149 bool insert(
150 object_mapt &dest,
151 const exprt &src,
152 const mp_integer &offset_value) const
153 {
154 return insert(dest, object_numbering.number(src), offsett(offset_value));
155 }
156
164 bool insert(
165 object_mapt &dest,
167 const offsett &offset) const;
168
169 enum class insert_actiont
170 {
171 INSERT,
173 NONE
174 };
175
183 const object_mapt &dest,
185 const offsett &offset) const;
186
193 bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
194 {
195 return insert(dest, object_numbering.number(expr), offset);
196 }
197
202 struct entryt
203 {
206 std::string suffix;
207
209 {
210 }
211
212 entryt(const irep_idt &_identifier, const std::string &_suffix)
213 : identifier(_identifier), suffix(_suffix)
214 {
215 }
216
217 bool operator==(const entryt &other) const
218 {
219 // Note that the object_map comparison below is duplicating the code of
220 // operator== defined in reference_counting.h because old versions of
221 // clang (3.7 and 3.8) do not resolve the template instantiation correctly
222 return identifier == other.identifier && suffix == other.suffix &&
223 (object_map.get_d() == other.object_map.get_d() ||
224 object_map.read() == other.object_map.read());
225 }
226 bool operator!=(const entryt &other) const
227 {
228 return !(*this==other);
229 }
230 };
231
246
253 std::vector<exprt> get_value_set(exprt expr, const namespacet &ns) const;
254
255 void clear()
256 {
257 values.clear();
258 }
259
266 const entryt *find_entry(const irep_idt &id) const;
267
280 void update_entry(
281 const entryt &e,
282 const typet &type,
283 const object_mapt &new_values,
284 bool add_to_sets);
285
289 void output(std::ostream &out, const std::string &indent = "") const;
290
292 xmlt output_xml(void) const;
293
297
302 bool make_union(object_mapt &dest, const object_mapt &src) const;
303
308 bool make_union_would_change(const object_mapt &dest, const object_mapt &src)
309 const;
310
314 bool make_union(const valuest &new_values);
315
319 {
320 return make_union(new_values.values);
321 }
322
328 void guard(
329 const exprt &expr,
330 const namespacet &ns);
331
339 const codet &code,
340 const namespacet &ns)
341 {
342 apply_code_rec(code, ns);
343 }
344
358 void assign(
359 const exprt &lhs,
360 const exprt &rhs,
361 const namespacet &ns,
362 bool is_simplified,
363 bool add_to_sets);
364
372 void do_function_call(
373 const irep_idt &function,
374 const exprt::operandst &arguments,
375 const namespacet &ns);
376
384 void do_end_function(
385 const exprt &lhs,
386 const namespacet &ns);
387
396 const exprt &expr,
398 const namespacet &ns) const;
399
410 exprt &expr,
411 const namespacet &ns) const;
412
420 std::optional<irep_idt> get_index_of_symbol(
421 irep_idt identifier,
422 const typet &type,
423 const std::string &suffix,
424 const namespacet &ns) const;
425
431 const irep_idt &index,
432 const std::unordered_set<exprt, irep_hash> &values_to_erase);
433
434 void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns);
435
436protected:
444 get_value_set(exprt expr, const namespacet &ns, bool is_simplified) const;
445
449 const exprt &expr,
450 object_mapt &dest,
451 const namespacet &ns) const
452 {
453 get_reference_set_rec(expr, dest, ns);
454 }
455
458 const exprt &expr,
459 object_mapt &dest,
460 const namespacet &ns) const;
461
463 void dereference_rec(
464 const exprt &src,
465 exprt &dest) const;
466
467 void erase_symbol_rec(
468 const typet &type,
469 const std::string &erase_prefix,
470 const namespacet &ns);
471
474 const std::string &erase_prefix,
475 const namespacet &ns);
476
477protected:
478 // Subclass customisation points:
479
488 virtual void get_value_set_rec(
489 const exprt &expr,
490 object_mapt &dest,
492 const std::string &suffix,
493 const typet &original_type,
494 const namespacet &ns) const;
495
497 virtual void assign_rec(
498 const exprt &lhs,
499 const object_mapt &values_rhs,
500 const std::string &suffix,
501 const namespacet &ns,
502 bool add_to_sets);
503
505 virtual void apply_code_rec(
506 const codet &code,
507 const namespacet &ns);
508
509private:
515 const exprt &rhs,
516 const namespacet &,
517 object_mapt &rhs_values) const
518 {
519 // unused parameters
520 (void)rhs;
522 }
523
529 const exprt &lhs,
530 const exprt &rhs,
531 const namespacet &)
532 {
533 // unused parameters
534 (void)lhs;
535 (void)rhs;
536 }
537};
538
539#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:562
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:38
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
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:131
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:44
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:245
bool make_union(const value_sett &new_values)
Merges an entire existing value_sett's data into this one.
Definition value_set.h:318
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:58
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:50
virtual void get_value_set_rec(const exprt &expr, object_mapt &dest, bool &includes_nondet_pointer, const std::string &suffix, const typet &original_type, const namespacet &ns) const
Subclass customisation point for recursion over RHS expression.
xmlt output_xml(void) const
Output the value set formatted as XML.
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:296
unsigned location_number
Matches the location_number field of the instruction that corresponds to this value_sett instance in ...
Definition value_set.h:73
void clear()
Definition value_set.h:255
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:77
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:128
void erase_struct_union_symbol(const struct_union_typet &struct_union_type, const std::string &erase_prefix, const namespacet &ns)
std::optional< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
Definition value_set.h:81
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:149
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:64
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:193
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:110
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:117
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:46
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:61
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:43
bool insert(object_mapt &dest, const exprt &src) const
Adds an expression to an object map, with unknown offset.
Definition value_set.h:138
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:448
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:528
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:88
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:514
std::optional< 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.
void apply_code(const codet &code, const namespacet &ns)
Transforms this value-set by executing a given statement against it.
Definition value_set.h:338
void erase_symbol_rec(const typet &type, const std::string &erase_prefix, const namespacet &ns)
Definition xml.h:21
STL namespace.
Object Numbering.
Reference Counting.
Sharing map.
Represents a row of a value_sett.
Definition value_set.h:203
irep_idt identifier
Definition value_set.h:205
entryt(const irep_idt &_identifier, const std::string &_suffix)
Definition value_set.h:212
bool operator!=(const entryt &other) const
Definition value_set.h:226
std::string suffix
Definition value_set.h:206
bool operator==(const entryt &other) const
Definition value_set.h:217
object_mapt object_map
Definition value_set.h:204
Value Set Propagation.