cprover
Loading...
Searching...
No Matches
pointer_predicates.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Various predicates over pointers in programs
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "pointer_predicates.h"
13
14#include "arith_tools.h"
15#include "c_types.h"
16#include "cprover_prefix.h"
17#include "namespace.h"
18#include "pointer_expr.h"
19#include "pointer_offset_size.h"
20#include "std_expr.h"
21#include "symbol.h"
22
24{
25 return unary_exprt(ID_pointer_object, p, size_type());
26}
27
28exprt same_object(const exprt &p1, const exprt &p2)
29{
31}
32
33exprt object_size(const exprt &pointer)
34{
35 return unary_exprt(ID_object_size, pointer, size_type());
36}
37
38exprt pointer_offset(const exprt &pointer)
39{
40 return unary_exprt(ID_pointer_offset, pointer, signed_size_type());
41}
42
43exprt deallocated(const exprt &pointer, const namespacet &ns)
44{
45 // we check __CPROVER_deallocated!
46 const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "deallocated");
47
48 return same_object(pointer, deallocated_symbol.symbol_expr());
49}
50
51exprt dead_object(const exprt &pointer, const namespacet &ns)
52{
53 // we check __CPROVER_dead_object!
54 const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "dead_object");
55
56 return same_object(pointer, deallocated_symbol.symbol_expr());
57}
58
59exprt dynamic_object(const exprt &pointer)
60{
61 exprt dynamic_expr(ID_is_dynamic_object, bool_typet());
62 dynamic_expr.copy_to_operands(pointer);
63 return dynamic_expr;
64}
65
66exprt good_pointer(const exprt &pointer)
67{
68 return unary_exprt(ID_good_pointer, pointer, bool_typet());
69}
70
72 const exprt &pointer,
73 const namespacet &ns)
74{
76 const typet &dereference_type = pointer_type.base_type();
77
78 const auto size_of_expr_opt = size_of_expr(dereference_type, ns);
79 CHECK_RETURN(size_of_expr_opt.has_value());
80
81 const exprt good_dynamic = not_exprt{deallocated(pointer, ns)};
82
83 const not_exprt not_null(null_pointer(pointer));
84
85 const not_exprt not_invalid{is_invalid_pointer_exprt{pointer}};
86
87 const and_exprt good_bounds{
89 not_exprt{object_upper_bound(pointer, size_of_expr_opt.value())}};
90
91 return and_exprt(not_null, not_invalid, good_dynamic, good_bounds);
92}
93
94exprt null_object(const exprt &pointer)
95{
97 return same_object(null_pointer, pointer);
98}
99
101{
103 return and_exprt(same_object(null_pointer, pointer),
104 notequal_exprt(null_pointer, pointer));
105}
106
107exprt null_pointer(const exprt &pointer)
108{
110 return same_object(pointer, null_pointer);
111}
112
114 const exprt &pointer,
115 const exprt &access_size)
116{
117 // this is
118 // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer)
119
120 exprt object_size_expr=object_size(pointer);
121
122 exprt object_offset=pointer_offset(pointer);
123
124 // need to add size
125 irep_idt op=ID_ge;
126 exprt sum=object_offset;
127
128 if(access_size.is_not_nil())
129 {
130 op=ID_gt;
131
132 sum = plus_exprt(
133 typecast_exprt::conditional_cast(object_offset, access_size.type()),
134 access_size);
135 }
136
138 typecast_exprt::conditional_cast(sum, object_size_expr.type()),
139 op,
140 object_size_expr);
141}
142
144 const exprt &pointer,
145 const exprt &offset)
146{
147 exprt p_offset=pointer_offset(pointer);
148
149 exprt zero=from_integer(0, p_offset.type());
150
151 if(offset.is_not_nil())
152 {
153 p_offset = plus_exprt(
154 p_offset, typecast_exprt::conditional_cast(offset, p_offset.type()));
155 }
156
157 return binary_relation_exprt(std::move(p_offset), ID_lt, std::move(zero));
158}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
unsignedbv_typet size_type()
Definition c_types.cpp:68
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
signedbv_typet signed_size_type()
Definition c_types.cpp:84
Boolean AND.
Definition std_expr.h:1974
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
The Boolean type.
Definition std_types.h:36
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
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:129
typet & type()
Return the type of the expression.
Definition expr.h:82
bool is_not_nil() const
Definition irep.h:380
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:2874
Boolean negation.
Definition std_expr.h:2181
Disequality.
Definition std_expr.h:1283
The null pointer constant.
The plus expression Associativity is not specified.
Definition std_expr.h:914
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
Symbol table entry.
Definition symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:281
#define CPROVER_PREFIX
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt integer_address(const exprt &pointer)
exprt deallocated(const exprt &pointer, const namespacet &ns)
exprt object_size(const exprt &pointer)
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
exprt good_pointer(const exprt &pointer)
exprt dead_object(const exprt &pointer, const namespacet &ns)
exprt same_object(const exprt &p1, const exprt &p2)
exprt dynamic_object(const exprt &pointer)
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
exprt null_object(const exprt &pointer)
exprt null_pointer(const exprt &pointer)
exprt pointer_object(const exprt &p)
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Various predicates over pointers in programs.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
API to expression classes.
Symbol table entry.