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
12#include <util/arith_tools.h>
13#include <util/c_types.h>
14#include <util/pointer_expr.h>
15#include <util/std_expr.h>
16
17#include <ostream>
18
20
22 const typet &type)
24{
25 PRECONDITION(type.id() == ID_pointer);
26}
27
29 const typet &type,
30 bool top,
31 bool bottom)
32 : abstract_pointer_objectt(type, top, bottom)
33{
34 PRECONDITION(type.id() == ID_pointer);
35}
36
38 const typet &new_type,
40 : abstract_pointer_objectt(new_type, old.is_top(), old.is_bottom()),
41 value_stack(old.value_stack)
42{
43}
44
46 const exprt &expr,
47 const abstract_environmentt &environment,
48 const namespacet &ns)
49 : abstract_pointer_objectt(expr, environment, ns),
50 value_stack(expr, environment, ns)
51{
52 PRECONDITION(expr.type().id() == ID_pointer);
54 {
55 set_top();
56 }
57 else
58 {
60 }
61}
62
64 const abstract_object_pointert &other,
65 const widen_modet &widen_mode) const
66{
67 auto cast_other =
68 std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
69 if(cast_other)
70 return merge_constant_pointers(cast_other, widen_mode);
71
72 return abstract_pointer_objectt::merge(other, widen_mode);
73}
74
76 abstract_object_pointert other) const
77{
78 auto cast_other =
79 std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
80
81 if(value_stack.is_top_value() || cast_other->value_stack.is_top_value())
82 return false;
83
84 if(value_stack.depth() != cast_other->value_stack.depth())
85 return false;
86
87 for(size_t d = 0; d != value_stack.depth() - 1; ++d)
88 if(
90 cast_other->value_stack.target_expression(d))
91 return false;
92
93 return true;
94}
95
97{
99 return nil_exprt();
101}
102
104 abstract_object_pointert other) const
105{
106 auto cast_other =
107 std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
108
109 if(value_stack.is_top_value() || cast_other->value_stack.is_top_value())
110 return nil_exprt();
111
112 return minus_exprt(
114 cast_other->value_stack.offset_expression());
115}
116
120 const widen_modet &widen_mode) const
121{
122 if(is_bottom())
123 return std::make_shared<constant_pointer_abstract_objectt>(*other);
124
125 bool matching_pointers =
126 value_stack.to_expression() == other->value_stack.to_expression();
127
128 if(matching_pointers)
129 return shared_from_this();
130
131 return abstract_pointer_objectt::merge(other, widen_mode);
132}
133
135{
136 if(is_top() || is_bottom())
137 {
139 }
140 else
141 {
142 // TODO(tkiley): I think we would like to eval this before using it
143 // in the to_constant.
144 return value_stack.to_expression();
145 }
146}
147
149 std::ostream &out,
150 const ai_baset &ai,
151 const namespacet &ns) const
152{
154 {
156 }
157 else
158 {
159 out << "ptr ->(";
160 const exprt &value = value_stack.to_expression();
161 if(value.id() == ID_address_of)
162 {
163 const auto &addressee = to_address_of_expr(value).object();
164 if(addressee.id() == ID_symbol)
165 {
166 const symbol_exprt &symbol_pointed_to(to_symbol_expr(addressee));
167
168 out << symbol_pointed_to.get_identifier();
169 }
170 else if(addressee.id() == ID_dynamic_object)
171 {
172 out << addressee.get(ID_identifier);
173 }
174 else if(addressee.id() == ID_index)
175 {
176 auto const &array_index = to_index_expr(addressee);
177 auto const &array = array_index.array();
178 if(array.id() == ID_symbol)
179 {
180 auto const &array_symbol = to_symbol_expr(array);
181 out << array_symbol.get_identifier() << "[";
182 if(array_index.index().id() == ID_constant)
183 out << to_constant_expr(array_index.index()).get_value();
184 else
185 out << "?";
186 out << "]";
187 }
188 }
189 }
190
191 out << ")";
192 }
193}
194
196 const abstract_environmentt &env,
197 const namespacet &ns) const
198{
200 {
201 // Return top if dereferencing a null pointer or we are top
202 bool is_value_top = is_top() || value_stack.is_top_value();
203 return env.abstract_object_factory(
204 type().subtype(), ns, is_value_top, !is_value_top);
205 }
206 else
207 {
208 return env.eval(
210 }
211}
212
214 abstract_environmentt &environment,
215 const namespacet &ns,
216 const std::stack<exprt> &stack,
217 const abstract_object_pointert &new_value,
218 bool merging_write) const
219{
220 if(is_top() || is_bottom())
221 {
222 environment.havoc("Writing to a 2value pointer");
223 return shared_from_this();
224 }
225
227 return std::make_shared<constant_pointer_abstract_objectt>(
228 type(), true, false);
229
230 if(stack.empty())
231 {
232 // We should not be changing the type of an abstract object
233 PRECONDITION(new_value->type() == ns.follow(type().subtype()));
234
235 // Get an expression that we can assign to
237 if(merging_write)
238 {
239 abstract_object_pointert pointed_value = environment.eval(value, ns);
240 abstract_object_pointert merged_value =
241 abstract_objectt::merge(pointed_value, new_value, widen_modet::no)
242 .object;
243 environment.assign(value, merged_value, ns);
244 }
245 else
246 {
247 environment.assign(value, new_value, ns);
248 }
249 }
250 else
251 {
253 abstract_object_pointert pointed_value = environment.eval(value, ns);
254 abstract_object_pointert modified_value =
255 environment.write(pointed_value, new_value, stack, ns, merging_write);
256 environment.assign(value, modified_value, ns);
257 // but the pointer itself does not change!
258 }
259
260 return shared_from_this();
261}
262
264 const typet &new_type,
265 const abstract_environmentt &environment,
266 const namespacet &ns) const
267{
268 INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
269
270 // Get an expression that we can assign to
272 if(value.id() == ID_dynamic_object)
273 {
274 auto &env = const_cast<abstract_environmentt &>(environment);
275
276 auto heap_array_type = array_typet(new_type.subtype(), nil_exprt());
277 auto array_object =
278 environment.abstract_object_factory(heap_array_type, ns, true, false);
279 auto heap_symbol = symbol_exprt(value.get(ID_identifier), heap_array_type);
280 env.assign(heap_symbol, array_object, ns);
281 auto heap_address = address_of_exprt(
282 index_exprt(heap_symbol, from_integer(0, signed_size_type())));
283 auto new_pointer = std::make_shared<constant_pointer_abstract_objectt>(
284 heap_address, env, ns);
285 return new_pointer;
286 }
287
288 return std::make_shared<constant_pointer_abstract_objectt>(new_type, *this);
289}
290
292 abstract_object_statisticst &statistics,
294 const abstract_environmentt &env,
295 const namespacet &ns) const
296{
297 abstract_pointer_objectt::get_statistics(statistics, visited, env, ns);
298 // don't bother following nullptr
299 if(!is_top() && !is_bottom() && !value_stack.is_top_value())
300 {
301 read_dereference(env, ns)->get_statistics(statistics, visited, env, ns);
302 }
303 statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
304}
305
307 const exprt &expr,
308 const std::vector<abstract_object_pointert> &operands,
309 const abstract_environmentt &environment,
310 const namespacet &ns) const
311{
312 auto &rhs = operands.back();
313
314 if(same_target(rhs))
315 return environment.eval(offset_from(rhs), ns);
316
318 expr, operands, environment, ns);
319}
320
321static exprt to_bool_expr(bool v)
322{
323 if(v)
324 return true_exprt();
325 return false_exprt();
326}
327
329 irep_idt const &id,
330 exprt const &lhs,
331 exprt const &rhs)
332{
333 auto const &lhs_member = to_member_expr(lhs).get_component_name();
334 auto const &rhs_member = to_member_expr(rhs).get_component_name();
335
336 if(id == ID_equal)
337 return to_bool_expr(lhs_member == rhs_member);
338 if(id == ID_notequal)
339 return to_bool_expr(lhs_member != rhs_member);
340 return nil_exprt();
341}
342
344 irep_idt const &id,
345 exprt const &lhs,
346 exprt const &rhs)
347{
348 auto const &lhs_identifier = to_symbol_expr(lhs).get_identifier();
349 auto const &rhs_identifier = to_symbol_expr(rhs).get_identifier();
350
351 if(id == ID_equal)
352 return to_bool_expr(lhs_identifier == rhs_identifier);
353 if(id == ID_notequal)
354 return to_bool_expr(lhs_identifier != rhs_identifier);
355 return nil_exprt();
356}
357
359 const exprt &expr,
360 const std::vector<abstract_object_pointert> &operands,
361 const abstract_environmentt &environment,
362 const namespacet &ns) const
363{
364 auto rhs = std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(
365 operands.back());
366
367 if(is_top() || rhs->is_top())
368 return nil_exprt();
369
370 if(same_target(rhs)) // rewrite in terms of pointer offset
371 {
372 auto lhs_offset = offset();
373 auto rhs_offset = rhs->offset();
374
375 if(lhs_offset.id() == ID_member)
377 expr.id(), lhs_offset, rhs_offset);
378 if(lhs_offset.id() == ID_symbol)
379 return symbol_ptr_comparison_expr(expr.id(), lhs_offset, rhs_offset);
380
381 return binary_relation_exprt(lhs_offset, expr.id(), rhs_offset);
382 }
383
384 // not same target, can only eval == and !=
385 if(expr.id() == ID_equal)
386 return false_exprt();
387 if(expr.id() == ID_notequal)
388 return true_exprt();
389 return nil_exprt();
390}
391
393 const exprt &name) const
394{
395 return equal_exprt(name, value_stack.to_expression());
396}
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:84
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:119
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:674
const irep_idt & get_value() const
Definition std_expr.h:2815
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
The Boolean constant false.
Definition std_expr.h:2865
Array index operator.
Definition std_expr.h:1328
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
const irep_idt & id() const
Definition irep.h:396
irep_idt get_component_name() const
Definition std_expr.h:2681
static memory_sizet from_bytes(std::size_t bytes)
Binary minus.
Definition std_expr.h:973
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:2874
Expression to hold a symbol (variable)
Definition std_expr.h:80
const irep_idt & get_identifier() const
Definition std_expr.h:109
The Boolean constant true.
Definition std_expr.h:2856
The type of an expression, extends irept.
Definition type.h:29
const typet & subtype() const
Definition type.h:48
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.
#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:1391
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.
abstract_object_pointert object