cprover
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  {
59  set_not_top();
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 {
153  if(is_top() || is_bottom() || value_stack.is_top_value())
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 {
199  if(is_top() || is_bottom() || value_stack.is_top_value())
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,
293  abstract_object_visitedt &visited,
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 
321 static 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)
Definition: arith_tools.cpp:99
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
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.
Definition: pointer_expr.h:341
exprt & object()
Definition: pointer_expr.h:350
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:2761
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:2811
Array index operator.
Definition: std_expr.h:1328
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
irep_idt get_component_name() const
Definition: std_expr.h:2627
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:2820
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:2802
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
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.
Definition: pointer_expr.h:79
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.
abstract_object_pointert object