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
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
40static bool is_dereference(const exprt &expr);
41static 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
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
123static bool is_dereference(const exprt &expr)
124{
125 return expr.id() == ID_dereference;
126}
127
128static 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:396
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
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
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:96
#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:1954