cprover
Loading...
Searching...
No Matches
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/prefix.h>
10#include <util/std_code.h>
11#include <util/std_expr.h>
13
18
20{
21 auto current = std::ref(address_of.object());
22 while(
23 !(can_cast_expr<symbol_exprt>(current) ||
27 {
28 if(const auto index = expr_try_dynamic_cast<index_exprt>(current.get()))
29 {
30 // For the case `my_array[bar]` the base expression is `my_array`.
31 current = index->array();
32 continue;
33 }
34 if(const auto member = expr_try_dynamic_cast<member_exprt>(current.get()))
35 {
36 // For the case `my_struct.field_name` the base expression is `my_struct`.
37 current = member->compound();
38 continue;
39 }
41 false,
42 "Unable to find base object of expression: " +
43 current.get().pretty(1, 0));
44 }
45 return current.get();
46}
47
57
59{
60 decision_procedure_objectt invalid_pointer_object;
61 // Using unique_id = 1, so 0 is the NULL object, 1 is the invalid object and
62 // other valid objects have unique_id > 1.
63 invalid_pointer_object.unique_id = 1;
64 invalid_pointer_object.base_expression = make_invalid_pointer_expr();
65 invalid_pointer_object.size = from_integer(0, size_type());
66 invalid_pointer_object.is_dynamic = false;
67 return invalid_pointer_object;
68}
69
71{
72 smt_object_mapt object_map;
74 exprt null_object_base = null_object.base_expression;
75 object_map.emplace(std::move(null_object_base), std::move(null_object));
76 decision_procedure_objectt invalid_pointer_object =
78 exprt invalid_pointer_object_base = invalid_pointer_object.base_expression;
79 object_map.emplace(
80 std::move(invalid_pointer_object_base), std::move(invalid_pointer_object));
81 return object_map;
82}
83
86static bool is_dynamic(const exprt &object)
87{
88 // This check corresponds to the symbols created in
89 // `goto_symext::symex_allocate`, which implements the `__CPROVER_allocate`
90 // intrinsic function used by the standard library models.
91 const bool dynamic_type = object.type().get_bool(ID_C_dynamic);
92 if(dynamic_type)
93 return true;
94 const auto symbol = expr_try_dynamic_cast<symbol_exprt>(object);
95 bool symbol_is_dynamic =
96 symbol &&
97 has_prefix(id2string(symbol->get_identifier()), SYMEX_DYNAMIC_PREFIX);
98 return symbol_is_dynamic;
99}
100
102 const exprt &expression,
103 const namespacet &ns,
104 smt_object_mapt &object_map)
105{
107 expression, [&](const exprt &object_base) -> void {
108 const auto find_result = object_map.find(object_base);
109 if(find_result != object_map.cend())
110 return;
111 const auto size = size_of_expr(object_base.type(), ns);
112 INVARIANT(size, "Objects are expected to have well defined size");
114 object.base_expression = object_base;
115 object.unique_id = object_map.size();
116 object.size = *size;
117 object.is_dynamic = is_dynamic(object_base);
118 object_map.emplace_hint(find_result, object_base, std::move(object));
119 });
120}
121
123 const exprt &expression,
124 const smt_object_mapt &object_map)
125{
126 bool all_objects_tracked = true;
128 expression, [&](const exprt &object_base) -> void {
129 const auto find_result = object_map.find(object_base);
130 if(find_result != object_map.cend())
131 return;
132 all_objects_tracked = false;
133 });
134 return all_objects_tracked;
135}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
unsignedbv_typet size_type()
Definition c_types.cpp:55
empty_typet void_type()
Definition c_types.cpp:250
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
Operator to return the address of an object.
A constant literal expression.
Definition std_expr.h:2942
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
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.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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.
optionalt< 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
bool can_cast_expr< code_labelt >(const exprt &base)
Definition std_code.h:994
API to expression classes.
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition std_expr.h:2976
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:206
bool can_cast_expr< string_constantt >(const exprt &base)
Information the decision procedure holds about each object.
exprt base_expression
The expression for the root of the object.
bool is_dynamic
This is true for heap allocated objects and false for stack allocated.
std::size_t unique_id
Number which uniquely identifies this particular object.
exprt size
Expression which evaluates to the size of the object in bytes.