CBMC
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
16#include <util/sharing_map.h>
17
18#include "object_numbering.h"
19#include "value_sets.h"
20
21#include <unordered_set>
22
23class namespacet;
24class xmlt;
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
80 typedef std::optional<exprt> offsett;
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
149 bool insert(
150 object_mapt &dest,
152 const offsett &offset) const;
153
154 enum class insert_actiont
155 {
156 INSERT,
158 NONE
159 };
160
168 const object_mapt &dest,
170 const offsett &offset) const;
171
178 bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
179 {
180 return insert(dest, object_numbering.number(expr), offset);
181 }
182
187 struct entryt
188 {
191 std::string suffix;
192
194 {
195 }
196
197 entryt(const irep_idt &_identifier, const std::string &_suffix)
198 : identifier(_identifier), suffix(_suffix)
199 {
200 }
201
202 bool operator==(const entryt &other) const
203 {
204 // Note that the object_map comparison below is duplicating the code of
205 // operator== defined in reference_counting.h because old versions of
206 // clang (3.7 and 3.8) do not resolve the template instantiation correctly
207 return identifier == other.identifier && suffix == other.suffix &&
208 (object_map.get_d() == other.object_map.get_d() ||
209 object_map.read() == other.object_map.read());
210 }
211 bool operator!=(const entryt &other) const
212 {
213 return !(*this==other);
214 }
215 };
216
231
238 std::vector<exprt> get_value_set(exprt expr, const namespacet &ns) const;
239
240 void clear()
241 {
242 values.clear();
243 }
244
251 const entryt *find_entry(const irep_idt &id) const;
252
265 void update_entry(
266 const entryt &e,
267 const typet &type,
268 const object_mapt &new_values,
269 bool add_to_sets);
270
274 void output(std::ostream &out, const std::string &indent = "") const;
275
277 xmlt output_xml(void) const;
278
282
287 bool make_union(object_mapt &dest, const object_mapt &src) const;
288
293 bool make_union_would_change(const object_mapt &dest, const object_mapt &src)
294 const;
295
299 bool make_union(const valuest &new_values);
300
304 {
305 return make_union(new_values.values);
306 }
307
313 void guard(
314 const exprt &expr,
315 const namespacet &ns);
316
324 const codet &code,
325 const namespacet &ns)
326 {
327 apply_code_rec(code, ns);
328 }
329
343 void assign(
344 const exprt &lhs,
345 const exprt &rhs,
346 const namespacet &ns,
347 bool is_simplified,
348 bool add_to_sets);
349
357 void do_function_call(
358 const irep_idt &function,
359 const exprt::operandst &arguments,
360 const namespacet &ns);
361
369 void do_end_function(
370 const exprt &lhs,
371 const namespacet &ns);
372
381 const exprt &expr,
383 const namespacet &ns) const;
384
395 exprt &expr,
396 const namespacet &ns) const;
397
405 std::optional<irep_idt> get_index_of_symbol(
406 irep_idt identifier,
407 const typet &type,
408 const std::string &suffix,
409 const namespacet &ns) const;
410
416 const irep_idt &index,
417 const std::unordered_set<exprt, irep_hash> &values_to_erase);
418
419 void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns);
420
421protected:
429 get_value_set(exprt expr, const namespacet &ns, bool is_simplified) const;
430
434 const exprt &expr,
435 object_mapt &dest,
436 const namespacet &ns) const
437 {
438 get_reference_set_rec(expr, dest, ns);
439 }
440
443 const exprt &expr,
444 object_mapt &dest,
445 const namespacet &ns) const;
446
448 void dereference_rec(
449 const exprt &src,
450 exprt &dest) const;
451
452 void erase_symbol_rec(
453 const typet &type,
454 const std::string &erase_prefix,
455 const namespacet &ns);
456
459 const std::string &erase_prefix,
460 const namespacet &ns);
461
462protected:
463 // Subclass customisation points:
464
473 virtual void get_value_set_rec(
474 const exprt &expr,
475 object_mapt &dest,
477 const std::string &suffix,
478 const typet &original_type,
479 const namespacet &ns) const;
480
482 virtual void assign_rec(
483 const exprt &lhs,
484 const object_mapt &values_rhs,
485 const std::string &suffix,
486 const namespacet &ns,
487 bool add_to_sets);
488
490 virtual void apply_code_rec(
491 const codet &code,
492 const namespacet &ns);
493
494private:
500 const exprt &rhs,
501 const namespacet &,
502 object_mapt &rhs_values) const
503 {
504 // unused parameters
505 (void)rhs;
507 }
508
514 const exprt &lhs,
515 const exprt &rhs,
516 const namespacet &)
517 {
518 // unused parameters
519 (void)lhs;
520 (void)rhs;
521 }
522};
523
524#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: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:230
bool make_union(const value_sett &new_values)
Merges an entire existing value_sett's data into this one.
Definition value_set.h:303
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
std::optional< exprt > offsett
Represents the offset into an object: either some (possibly constant) expression, or an unknown value...
Definition value_set.h:80
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:281
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:240
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.
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:178
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
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:433
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:513
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:499
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:323
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:188
irep_idt identifier
Definition value_set.h:190
entryt(const irep_idt &_identifier, const std::string &_suffix)
Definition value_set.h:197
bool operator!=(const entryt &other) const
Definition value_set.h:211
std::string suffix
Definition value_set.h:191
bool operator==(const entryt &other) const
Definition value_set.h:202
object_mapt object_map
Definition value_set.h:189
Value Set Propagation.