cprover
abstract_pointer_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 
11 
12 #include <util/pointer_expr.h>
13 
15 
17  : abstract_objectt(t)
18 {
19  PRECONDITION(t.id() == ID_pointer);
20 }
21 
23  const typet &type,
24  bool top,
25  bool bottom)
26  : abstract_objectt(type, top, bottom)
27 {
28  PRECONDITION(type.id() == ID_pointer);
29 }
30 
32  const exprt &e,
33  const abstract_environmentt &environment,
34  const namespacet &ns)
35  : abstract_objectt(e, environment, ns)
36 {
37  PRECONDITION(e.type().id() == ID_pointer);
38 }
39 
40 static bool is_dereference(const exprt &expr);
41 static bool is_typecast_from_void_ptr(const exprt &expr);
42 
44  const exprt &expr,
45  const std::vector<abstract_object_pointert> &operands,
46  const abstract_environmentt &environment,
47  const namespacet &ns) const
48 {
49  if(is_dereference(expr))
50  return read_dereference(environment, ns);
51 
53  return typecast_from_void_ptr(expr, operands, environment, ns);
54 
55  if(is_ptr_diff(expr))
56  return eval_ptr_diff(expr, operands, environment, ns);
57 
58  if(is_ptr_comparison(expr))
59  return eval_ptr_comparison(expr, operands, environment, ns);
60 
62  expr, operands, environment, ns);
63 }
64 
66  abstract_environmentt &environment,
67  const namespacet &ns,
68  const std::stack<exprt> &stack,
69  const exprt &specifier,
70  const abstract_object_pointert &value,
71  bool merging_write) const
72 {
73  return write_dereference(environment, ns, stack, value, merging_write);
74 }
75 
77  abstract_object_statisticst &statistics,
78  abstract_object_visitedt &visited,
79  const abstract_environmentt &env,
80  const namespacet &ns) const
81 {
82  abstract_objectt::get_statistics(statistics, visited, env, ns);
83  ++statistics.number_of_pointers;
84 }
85 
87  const exprt &expr,
88  const std::vector<abstract_object_pointert> &operands,
89  const abstract_environmentt &environment,
90  const namespacet &ns) const
91 {
92  auto pointer =
93  std::dynamic_pointer_cast<const abstract_pointer_objectt>(operands.front());
94  if(pointer)
95  return pointer->typecast(expr.type(), environment, ns);
96 
98  expr, operands, environment, ns);
99 }
100 
102  const exprt &expr,
103  const std::vector<abstract_object_pointert> &operands,
104  const abstract_environmentt &environment,
105  const namespacet &ns) const
106 {
107  if(is_top() || operands[1]->is_top())
108  return environment.eval(nil_exprt(), ns);
109 
110  return ptr_diff(expr, operands, environment, ns);
111 }
112 
114  const exprt &expr,
115  const std::vector<abstract_object_pointert> &operands,
116  const abstract_environmentt &environment,
117  const namespacet &ns) const
118 {
119  auto result = ptr_comparison_expr(expr, operands, environment, ns);
120  return environment.eval(result, ns);
121 }
122 
123 static bool is_dereference(const exprt &expr)
124 {
125  return expr.id() == ID_dereference;
126 }
127 
128 static bool is_typecast_from_void_ptr(const exprt &expr)
129 {
130  if(expr.id() != ID_typecast)
131  return false;
132 
133  const typecast_exprt &tce = to_typecast_expr(expr);
134  return tce.op().id() == ID_symbol && is_void_pointer(tce.op().type());
135 }
bool is_ptr_comparison(const exprt &expr)
bool is_ptr_diff(const exprt &expr)
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.
static bool is_dereference(const exprt &expr)
static bool is_typecast_from_void_ptr(const exprt &expr)
The base of all pointer abstractions.
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
virtual bool is_top() const
Find out if the abstract object is top.
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.
typet t
To enforce copy-on-write these are private and have read-only accessors.
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
abstract_object_pointert eval_ptr_diff(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
abstract_object_pointert typecast_from_void_ptr(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of an abstract object.
virtual 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 =0
Evaluate writing to a pointer's value.
virtual exprt ptr_comparison_expr(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const =0
virtual abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const =0
A helper function to read elements from an array.
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
virtual abstract_object_pointert ptr_diff(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const =0
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
abstract_object_pointert eval_ptr_comparison(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
abstract_pointer_objectt(const typet &type)
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
const irep_idt & id() const
Definition: irep.h:407
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
Semantic type conversion.
Definition: std_expr.h:1866
The type of an expression, extends irept.
Definition: type.h:28
const exprt & op() const
Definition: std_expr.h:293
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
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900