CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
constant_pointer_abstract_object.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity
4
5 Author: Thomas Kiley, thomas.kiley@diffblue.com
6
7\*******************************************************************/
8
10
11#include <util/arith_tools.h>
12#include <util/c_types.h>
13#include <util/pointer_expr.h>
14#include <util/std_expr.h>
15
17
19
20#include <ostream>
21
23 const typet &type,
24 bool top,
25 bool bottom)
26 : abstract_pointer_objectt(type, top, bottom)
27{
29}
30
32 const typet &new_type,
34 : abstract_pointer_objectt(new_type, old.is_top(), old.is_bottom()),
35 value_stack(old.value_stack)
36{
37}
38
40 const exprt &expr,
41 const abstract_environmentt &environment,
42 const namespacet &ns)
43 : abstract_pointer_objectt(expr, environment, ns),
44 value_stack(expr, environment, ns)
45{
46 PRECONDITION(expr.type().id() == ID_pointer);
48 {
49 set_top();
50 }
51 else
52 {
54 }
55}
56
58 const abstract_object_pointert &other,
59 const widen_modet &widen_mode) const
60{
61 auto cast_other =
62 std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
63 if(cast_other)
65
67}
68
70 abstract_object_pointert other) const
71{
72 auto cast_other =
73 std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
74
75 if(value_stack.is_top_value() || cast_other->value_stack.is_top_value())
76 return false;
77
78 if(value_stack.depth() != cast_other->value_stack.depth())
79 return false;
80
81 for(size_t d = 0; d != value_stack.depth() - 1; ++d)
82 if(
84 cast_other->value_stack.target_expression(d))
85 return false;
86
87 return true;
88}
89
96
98 abstract_object_pointert other) const
99{
100 auto cast_other =
101 std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
102
103 if(value_stack.is_top_value() || cast_other->value_stack.is_top_value())
104 return nil_exprt();
105
106 return minus_exprt(
108 cast_other->value_stack.offset_expression());
109}
110
114 const widen_modet &widen_mode) const
115{
116 if(is_bottom())
117 return std::make_shared<constant_pointer_abstract_objectt>(*other);
118
119 bool matching_pointers =
120 value_stack.to_expression() == other->value_stack.to_expression();
121
123 return shared_from_this();
124
126}
127
129{
130 if(is_top() || is_bottom())
131 {
133 }
134 else
135 {
136 // TODO(tkiley): I think we would like to eval this before using it
137 // in the to_constant.
138 return value_stack.to_expression();
139 }
140}
141
143 std::ostream &out,
144 const ai_baset &ai,
145 const namespacet &ns) const
146{
148 {
150 }
151 else
152 {
153 out << "ptr ->(";
154 const exprt &value = value_stack.to_expression();
155 if(value.id() == ID_address_of)
156 {
157 const auto &addressee = to_address_of_expr(value).object();
158 if(addressee.id() == ID_symbol)
159 {
161
162 out << symbol_pointed_to.get_identifier();
163 }
164 else if(addressee.id() == ID_dynamic_object)
165 {
166 out << addressee.get(ID_identifier);
167 }
168 else if(addressee.id() == ID_index)
169 {
170 auto const &array_index = to_index_expr(addressee);
171 auto const &array = array_index.array();
172 if(array.id() == ID_symbol)
173 {
174 auto const &array_symbol = to_symbol_expr(array);
175 out << array_symbol.get_identifier() << "[";
176 if(array_index.index().is_constant())
177 out << to_constant_expr(array_index.index()).get_value();
178 else
179 out << "?";
180 out << "]";
181 }
182 }
183 }
184
185 out << ")";
186 }
187}
188
191 const namespacet &ns) const
192{
194 {
195 // Return top if dereferencing a null pointer or we are top
197 return env.abstract_object_factory(
198 to_pointer_type(type()).base_type(), ns, is_value_top, !is_value_top);
199 }
200 else
201 {
202 return env.eval(
204 }
205}
206
208 abstract_environmentt &environment,
209 const namespacet &ns,
210 const std::stack<exprt> &stack,
211 const abstract_object_pointert &new_value,
212 bool merging_write) const
213{
214 if(is_top() || is_bottom())
215 {
216 environment.havoc("Writing to a 2value pointer");
217 return shared_from_this();
218 }
219
221 return std::make_shared<constant_pointer_abstract_objectt>(
222 type(), true, false);
223
224 if(stack.empty())
225 {
226 // We should not be changing the type of an abstract object
227 PRECONDITION(new_value->type() == to_pointer_type(type()).base_type());
228
229 // Get an expression that we can assign to
231 if(merging_write)
232 {
233 abstract_object_pointert pointed_value = environment.eval(value, ns);
236 .object;
237 environment.assign(value, merged_value, ns);
238 }
239 else
240 {
241 environment.assign(value, new_value, ns);
242 }
243 }
244 else
245 {
247 abstract_object_pointert pointed_value = environment.eval(value, ns);
249 environment.write(pointed_value, new_value, stack, ns, merging_write);
250 environment.assign(value, modified_value, ns);
251 // but the pointer itself does not change!
252 }
253
254 return shared_from_this();
255}
256
258 const typet &new_type,
259 const abstract_environmentt &environment,
260 const namespacet &ns) const
261{
262 INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
263
264 // Get an expression that we can assign to
266 if(value.id() == ID_dynamic_object)
267 {
268 auto &env = const_cast<abstract_environmentt &>(environment);
269
270 auto heap_array_type =
272 auto array_object =
273 environment.abstract_object_factory(heap_array_type, ns, true, false);
275 env.assign(heap_symbol, array_object, ns);
278 auto new_pointer = std::make_shared<constant_pointer_abstract_objectt>(
279 heap_address, env, ns);
280 return new_pointer;
281 }
282
283 return std::make_shared<constant_pointer_abstract_objectt>(new_type, *this);
284}
285
287 abstract_object_statisticst &statistics,
290 const namespacet &ns) const
291{
292 abstract_pointer_objectt::get_statistics(statistics, visited, env, ns);
293 // don't bother following nullptr
294 if(!is_top() && !is_bottom() && !value_stack.is_top_value())
295 {
296 read_dereference(env, ns)->get_statistics(statistics, visited, env, ns);
297 }
298 statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
299}
300
302 const exprt &expr,
303 const std::vector<abstract_object_pointert> &operands,
304 const abstract_environmentt &environment,
305 const namespacet &ns) const
306{
307 auto &rhs = operands.back();
308
309 if(same_target(rhs))
310 return environment.eval(offset_from(rhs), ns);
311
313 expr, operands, environment, ns);
314}
315
316static exprt to_bool_expr(bool v)
317{
318 if(v)
319 return true_exprt();
320 return false_exprt();
321}
322
324 irep_idt const &id,
325 exprt const &lhs,
326 exprt const &rhs)
327{
328 auto const &lhs_member = to_member_expr(lhs).get_component_name();
329 auto const &rhs_member = to_member_expr(rhs).get_component_name();
330
331 if(id == ID_equal)
333 if(id == ID_notequal)
335 return nil_exprt();
336}
337
339 irep_idt const &id,
340 exprt const &lhs,
341 exprt const &rhs)
342{
343 auto const &lhs_identifier = to_symbol_expr(lhs).get_identifier();
344 auto const &rhs_identifier = to_symbol_expr(rhs).get_identifier();
345
346 if(id == ID_equal)
348 if(id == ID_notequal)
350 return nil_exprt();
351}
352
354 const exprt &expr,
355 const std::vector<abstract_object_pointert> &operands,
356 const abstract_environmentt &environment,
357 const namespacet &ns) const
358{
359 auto rhs = std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(
360 operands.back());
361
362 if(is_top() || rhs->is_top())
363 return nil_exprt();
364
365 if(same_target(rhs)) // rewrite in terms of pointer offset
366 {
367 auto lhs_offset = offset();
368 auto rhs_offset = rhs->offset();
369
370 if(lhs_offset.id() == ID_member)
372 expr.id(), lhs_offset, rhs_offset);
373 if(lhs_offset.id() == ID_symbol)
375
377 }
378
379 // not same target, can only eval == and !=
380 if(expr.id() == ID_equal)
381 return false_exprt();
382 if(expr.id() == ID_notequal)
383 return true_exprt();
384 return nil_exprt();
385}
386
An abstract version of a program environment.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Statistics gathering for the variable senstivity domain.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
signedbv_typet signed_size_type()
Definition c_types.cpp:66
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
virtual void havoc(const std::string &havoc_string)
This should be used as a default case / everything else has failed The string is so that I can easily...
virtual abstract_object_pointert write(const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write)
Used within assign to do the actual dispatch.
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
virtual bool assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
virtual exprt to_constant() const
Converts to a constant expression if possible.
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
Interface for transforms.
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
Operator to return the address of an object.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Arrays with given size.
Definition std_types.h:807
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
abstract_object_pointert merge(const abstract_object_pointert &op1, const widen_modet &widen_mode) const override
Set this abstract object to be the result of merging this abstract object.
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
A helper function to dereference a value from a pointer.
abstract_object_pointert ptr_diff(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
sharing_ptrt< constant_pointer_abstract_objectt > constant_pointer_abstract_pointert
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Print the value of the pointer.
abstract_object_pointert merge_constant_pointers(const constant_pointer_abstract_pointert &other, const widen_modet &widen_mode) const
Merges two constant pointers.
bool same_target(abstract_object_pointert other) const
exprt ptr_comparison_expr(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
exprt offset_from(abstract_object_pointert other) const
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
exprt to_constant() const override
To try and find a constant expression for this abstract object.
abstract_object_pointert typecast(const typet &new_type, const abstract_environmentt &environment, const namespacet &ns) const override
abstract_object_pointert write_dereference(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a pointers value.
constant_pointer_abstract_objectt(const typet &type, bool top, bool bottom)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3199
Array index operator.
Definition std_expr.h:1470
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:388
static memory_sizet from_bytes(std::size_t bytes)
Binary minus.
Definition std_expr.h:1061
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3208
Expression to hold a symbol (variable)
Definition std_expr.h:131
The Boolean constant true.
Definition std_expr.h:3190
The type of an expression, extends irept.
Definition type.h:29
exprt target_expression(size_t depth) const
exprt offset_expression() const
bool is_top_value() const
Is the stack representing an unknown value and hence can't be written to or read from.
exprt to_expression() const
Convert the stack to an expression that can be used to write to.
size_t depth() const
static exprt to_bool_expr(bool v)
exprt struct_member_ptr_comparison_expr(irep_idt const &id, exprt const &lhs, exprt const &rhs)
exprt symbol_ptr_comparison_expr(irep_idt const &id, exprt const &lhs, exprt const &rhs)
An abstraction of a pointer that tracks a single pointer.
API to expression classes for Pointers.
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.