CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
object_tracking.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#include "object_tracking.h"
4
5#include <util/arith_tools.h>
6#include <util/c_types.h>
9#include <util/std_code.h>
10#include <util/std_expr.h>
12
17
19{
20 auto current = std::ref(address_of.object());
21 while(
22 !(can_cast_expr<symbol_exprt>(current) ||
26 {
27 if(const auto index = expr_try_dynamic_cast<index_exprt>(current.get()))
28 {
29 // For the case `my_array[bar]` the base expression is `my_array`.
30 current = index->array();
31 continue;
32 }
33 if(const auto member = expr_try_dynamic_cast<member_exprt>(current.get()))
34 {
35 // For the case `my_struct.field_name` the base expression is `my_struct`.
36 current = member->compound();
37 continue;
38 }
40 false,
41 "Unable to find base object of expression: " +
42 current.get().pretty(1, 0));
43 }
44 return current.get();
45}
46
56
58{
60 // Using unique_id = 1, so 0 is the NULL object, 1 is the invalid object and
61 // other valid objects have unique_id > 1.
62 invalid_pointer_object.unique_id = 1;
65 invalid_pointer_object.is_dynamic = false;
67}
68
82
85static bool is_dynamic(const exprt &object)
86{
87 // This check corresponds to the symbols created in
88 // `goto_symext::symex_allocate`, which implements the `__CPROVER_allocate`
89 // intrinsic function used by the standard library models.
90 const bool dynamic_type = object.type().get_bool(ID_C_dynamic);
91 if(dynamic_type)
92 return true;
93 const auto symbol = expr_try_dynamic_cast<symbol_exprt>(object);
95 symbol && symbol->get_identifier().starts_with(SYMEX_DYNAMIC_PREFIX);
96 return symbol_is_dynamic;
97}
98
100 const exprt &expression,
101 const namespacet &ns,
102 smt_object_mapt &object_map)
103{
105 expression, [&](const exprt &object_base) -> void {
106 const auto find_result = object_map.find(object_base);
107 if(find_result != object_map.cend())
108 return;
109 const auto size = size_of_expr(object_base.type(), ns);
110 INVARIANT(size, "Objects are expected to have well defined size");
113 object.unique_id = object_map.size();
114 object.size = *size;
115 object.is_dynamic = is_dynamic(object_base);
116 object_map.emplace_hint(find_result, object_base, std::move(object));
117 });
118}
119
121 const exprt &expression,
122 const smt_object_mapt &object_map)
123{
124 bool all_objects_tracked = true;
126 expression, [&](const exprt &object_base) -> void {
127 const auto find_result = object_map.find(object_base);
128 if(find_result != object_map.cend())
129 return;
130 all_objects_tracked = false;
131 });
132 return all_objects_tracked;
133}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
empty_typet void_type()
Definition c_types.cpp:245
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A constant literal expression.
Definition std_expr.h:3117
Base class for all expressions.
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
The null pointer constant.
exprt make_invalid_pointer_expr()
Create the invalid pointer constant.
exprt find_object_base_expression(const address_of_exprt &address_of)
The model of addresses we use consists of a unique object identifier and an offset.
void track_expression_objects(const exprt &expression, const namespacet &ns, smt_object_mapt &object_map)
Finds all the object expressions in the given expression and adds them to the object map for cases wh...
bool objects_are_already_tracked(const exprt &expression, const smt_object_mapt &object_map)
Finds whether all base object expressions in the given expression are already tracked in the given ob...
static decision_procedure_objectt make_invalid_pointer_object()
smt_object_mapt initial_smt_object_map()
Constructs an initial object map containing the null object.
static decision_procedure_objectt make_null_object()
static bool is_dynamic(const exprt &object)
This function returns true for heap allocated objects or false for stack allocated objects.
Data structures and algorithms used by smt2_incremental_decision_proceduret to track data about the o...
void find_object_base_expressions(const exprt &expression, const output_object_functiont &output_object)
Arbitrary expressions passed to the decision procedure may have multiple address of operations as its...
std::unordered_map< exprt, decision_procedure_objectt, irep_hash > smt_object_mapt
Mapping from an object's base expression to the set of information about it which we track.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt null_object(const exprt &pointer)
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
Information the decision procedure holds about each object.
exprt base_expression
The expression for the root of the object.
#define size_type
Definition unistd.c:186