cprover
Loading...
Searching...
No Matches
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/namespace.h>
14#include <util/pointer_expr.h>
15#include <util/std_expr.h>
16
18
20
21#include <ostream>
22
24 const typet &type,
25 bool top,
26 bool bottom)
27 : abstract_pointer_objectt(type, top, bottom)
28{
30}
31
33 const typet &new_type,
35 : abstract_pointer_objectt(new_type, old.is_top(), old.is_bottom()),
36 value_stack(old.value_stack)
37{
38}
39
41 const exprt &expr,
42 const abstract_environmentt &environment,
43 const namespacet &ns)
44 : abstract_pointer_objectt(expr, environment, ns),
45 value_stack(expr, environment, ns)
46{
47 PRECONDITION(expr.type().id() == ID_pointer);
49 {
50 set_top();
51 }
52 else
53 {
55 }
56}
57
59 const abstract_object_pointert &other,
60 const widen_modet &widen_mode) const
61{
62 auto cast_other =
63 std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
64 if(cast_other)
66
68}
69
71 abstract_object_pointert other) const
72{
73 auto cast_other =
74 std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
75
76 if(value_stack.is_top_value() || cast_other->value_stack.is_top_value())
77 return false;
78
79 if(value_stack.depth() != cast_other->value_stack.depth())
80 return false;
81
82 for(size_t d = 0; d != value_stack.depth() - 1; ++d)
83 if(
85 cast_other->value_stack.target_expression(d))
86 return false;
87
88 return true;
89}
90
97
99 abstract_object_pointert other) const
100{
101 auto cast_other =
102 std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
103
104 if(value_stack.is_top_value() || cast_other->value_stack.is_top_value())
105 return nil_exprt();
106
107 return minus_exprt(
109 cast_other->value_stack.offset_expression());
110}
111
115 const widen_modet &widen_mode) const
116{
117 if(is_bottom())
118 return std::make_shared<constant_pointer_abstract_objectt>(*other);
119
120 bool matching_pointers =
121 value_stack.to_expression() == other->value_stack.to_expression();
122
124 return shared_from_this();
125
127}
128
130{
131 if(is_top() || is_bottom())
132 {
134 }
135 else
136 {
137 // TODO(tkiley): I think we would like to eval this before using it
138 // in the to_constant.
139 return value_stack.to_expression();
140 }
141}
142
144 std::ostream &out,
145 const ai_baset &ai,
146 const namespacet &ns) const
147{
149 {
151 }
152 else
153 {
154 out << "ptr ->(";
155 const exprt &value = value_stack.to_expression();
156 if(value.id() == ID_address_of)
157 {
158 const auto &addressee = to_address_of_expr(value).object();
159 if(addressee.id() == ID_symbol)
160 {
162
163 out << symbol_pointed_to.get_identifier();
164 }
165 else if(addressee.id() == ID_dynamic_object)
166 {
167 out << addressee.get(ID_identifier);
168 }
169 else if(addressee.id() == ID_index)
170 {
171 auto const &array_index = to_index_expr(addressee);
172 auto const &array = array_index.array();
173 if(array.id() == ID_symbol)
174 {
175 auto const &array_symbol = to_symbol_expr(array);
176 out << array_symbol.get_identifier() << "[";
177 if(array_index.index().is_constant())
178 out << to_constant_expr(array_index.index()).get_value();
179 else
180 out << "?";
181 out << "]";
182 }
183 }
184 }
185
186 out << ")";
187 }
188}
189
192 const namespacet &ns) const
193{
195 {
196 // Return top if dereferencing a null pointer or we are top
198 return env.abstract_object_factory(
199 to_pointer_type(type()).base_type(), ns, is_value_top, !is_value_top);
200 }
201 else
202 {
203 return env.eval(
205 }
206}
207
209 abstract_environmentt &environment,
210 const namespacet &ns,
211 const std::stack<exprt> &stack,
212 const abstract_object_pointert &new_value,
213 bool merging_write) const
214{
215 if(is_top() || is_bottom())
216 {
217 environment.havoc("Writing to a 2value pointer");
218 return shared_from_this();
219 }
220
222 return std::make_shared<constant_pointer_abstract_objectt>(
223 type(), true, false);
224
225 if(stack.empty())
226 {
227 // We should not be changing the type of an abstract object
229 new_value->type() == ns.follow(to_pointer_type(type()).base_type()));
230
231 // Get an expression that we can assign to
233 if(merging_write)
234 {
235 abstract_object_pointert pointed_value = environment.eval(value, ns);
238 .object;
239 environment.assign(value, merged_value, ns);
240 }
241 else
242 {
243 environment.assign(value, new_value, ns);
244 }
245 }
246 else
247 {
249 abstract_object_pointert pointed_value = environment.eval(value, ns);
251 environment.write(pointed_value, new_value, stack, ns, merging_write);
252 environment.assign(value, modified_value, ns);
253 // but the pointer itself does not change!
254 }
255
256 return shared_from_this();
257}
258
260 const typet &new_type,
261 const abstract_environmentt &environment,
262 const namespacet &ns) const
263{
264 INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
265
266 // Get an expression that we can assign to
268 if(value.id() == ID_dynamic_object)
269 {
270 auto &env = const_cast<abstract_environmentt &>(environment);
271
272 auto heap_array_type =
274 auto array_object =
275 environment.abstract_object_factory(heap_array_type, ns, true, false);
277 env.assign(heap_symbol, array_object, ns);
280 auto new_pointer = std::make_shared<constant_pointer_abstract_objectt>(
281 heap_address, env, ns);
282 return new_pointer;
283 }
284
285 return std::make_shared<constant_pointer_abstract_objectt>(new_type, *this);
286}
287
289 abstract_object_statisticst &statistics,
292 const namespacet &ns) const
293{
294 abstract_pointer_objectt::get_statistics(statistics, visited, env, ns);
295 // don't bother following nullptr
296 if(!is_top() && !is_bottom() && !value_stack.is_top_value())
297 {
298 read_dereference(env, ns)->get_statistics(statistics, visited, env, ns);
299 }
300 statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
301}
302
304 const exprt &expr,
305 const std::vector<abstract_object_pointert> &operands,
306 const abstract_environmentt &environment,
307 const namespacet &ns) const
308{
309 auto &rhs = operands.back();
310
311 if(same_target(rhs))
312 return environment.eval(offset_from(rhs), ns);
313
315 expr, operands, environment, ns);
316}
317
318static exprt to_bool_expr(bool v)
319{
320 if(v)
321 return true_exprt();
322 return false_exprt();
323}
324
326 irep_idt const &id,
327 exprt const &lhs,
328 exprt const &rhs)
329{
330 auto const &lhs_member = to_member_expr(lhs).get_component_name();
331 auto const &rhs_member = to_member_expr(rhs).get_component_name();
332
333 if(id == ID_equal)
335 if(id == ID_notequal)
337 return nil_exprt();
338}
339
341 irep_idt const &id,
342 exprt const &lhs,
343 exprt const &rhs)
344{
345 auto const &lhs_identifier = to_symbol_expr(lhs).get_identifier();
346 auto const &rhs_identifier = to_symbol_expr(rhs).get_identifier();
347
348 if(id == ID_equal)
350 if(id == ID_notequal)
352 return nil_exprt();
353}
354
356 const exprt &expr,
357 const std::vector<abstract_object_pointert> &operands,
358 const abstract_environmentt &environment,
359 const namespacet &ns) const
360{
361 auto rhs = std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(
362 operands.back());
363
364 if(is_top() || rhs->is_top())
365 return nil_exprt();
366
367 if(same_target(rhs)) // rewrite in terms of pointer offset
368 {
369 auto lhs_offset = offset();
370 auto rhs_offset = rhs->offset();
371
372 if(lhs_offset.id() == ID_member)
374 expr.id(), lhs_offset, rhs_offset);
375 if(lhs_offset.id() == ID_symbol)
377
379 }
380
381 // not same target, can only eval == and !=
382 if(expr.id() == ID_equal)
383 return false_exprt();
384 if(expr.id() == ID_notequal)
385 return true_exprt();
386 return nil_exprt();
387}
388
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:71
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:118
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Arrays with given size.
Definition std_types.h:763
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
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
CLONE 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:39
Equality.
Definition std_expr.h:1306
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:3017
Array index operator.
Definition std_expr.h:1410
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:396
static memory_sizet from_bytes(std::size_t bytes)
Binary minus.
Definition std_expr.h:1006
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
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:3026
Expression to hold a symbol (variable)
Definition std_expr.h:113
The Boolean constant true.
Definition std_expr.h:3008
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:1478
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.