cprover
pointer_predicates.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Various predicates over pointers in programs
4 
5 Author: 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 
28 exprt same_object(const exprt &p1, const exprt &p2)
29 {
30  return equal_exprt(pointer_object(p1), pointer_object(p2));
31 }
32 
33 exprt object_size(const exprt &pointer)
34 {
35  return unary_exprt(ID_object_size, pointer, size_type());
36 }
37 
38 exprt pointer_offset(const exprt &pointer)
39 {
40  return unary_exprt(ID_pointer_offset, pointer, signed_size_type());
41 }
42 
43 exprt malloc_object(const exprt &pointer, const namespacet &ns)
44 {
45  // we check __CPROVER_malloc_object!
46  const symbolt &malloc_object_symbol=ns.lookup(CPROVER_PREFIX "malloc_object");
47 
48  return same_object(pointer, malloc_object_symbol.symbol_expr());
49 }
50 
51 exprt deallocated(const exprt &pointer, const namespacet &ns)
52 {
53  // we check __CPROVER_deallocated!
54  const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "deallocated");
55 
56  return same_object(pointer, deallocated_symbol.symbol_expr());
57 }
58 
59 exprt dead_object(const exprt &pointer, const namespacet &ns)
60 {
61  // we check __CPROVER_dead_object!
62  const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "dead_object");
63 
64  return same_object(pointer, deallocated_symbol.symbol_expr());
65 }
66 
68 {
69  return ns.lookup(CPROVER_PREFIX "malloc_size").symbol_expr();
70 }
71 
72 exprt dynamic_object(const exprt &pointer)
73 {
74  exprt dynamic_expr(ID_is_dynamic_object, bool_typet());
75  dynamic_expr.copy_to_operands(pointer);
76  return dynamic_expr;
77 }
78 
79 exprt good_pointer(const exprt &pointer)
80 {
81  return unary_exprt(ID_good_pointer, pointer, bool_typet());
82 }
83 
85  const exprt &pointer,
86  const namespacet &ns)
87 {
88  const pointer_typet &pointer_type = to_pointer_type(pointer.type());
89  const typet &dereference_type=pointer_type.subtype();
90 
91  const auto size_of_expr_opt = size_of_expr(dereference_type, ns);
92  CHECK_RETURN(size_of_expr_opt.has_value());
93 
94  const exprt good_dynamic = not_exprt{deallocated(pointer, ns)};
95 
96  const not_exprt not_null(null_pointer(pointer));
97 
98  const not_exprt not_invalid{is_invalid_pointer_exprt{pointer}};
99 
100  const and_exprt good_bounds{
102  not_exprt{object_upper_bound(pointer, size_of_expr_opt.value())}};
103 
104  return and_exprt(not_null, not_invalid, good_dynamic, good_bounds);
105 }
106 
107 exprt null_object(const exprt &pointer)
108 {
110  return same_object(null_pointer, pointer);
111 }
112 
113 exprt integer_address(const exprt &pointer)
114 {
116  return and_exprt(same_object(null_pointer, pointer),
117  notequal_exprt(null_pointer, pointer));
118 }
119 
120 exprt null_pointer(const exprt &pointer)
121 {
123  return same_object(pointer, null_pointer);
124 }
125 
127  const exprt &pointer,
128  const exprt &offset)
129 {
130  return object_lower_bound(pointer, offset);
131 }
132 
134  const exprt &pointer,
135  const namespacet &ns,
136  const exprt &access_size)
137 {
138  // this is
139  // POINTER_OFFSET(p)+access_size>__CPROVER_malloc_size
140 
141  exprt malloc_size=dynamic_size(ns);
142 
143  exprt object_offset=pointer_offset(pointer);
144 
145  // need to add size
146  irep_idt op=ID_ge;
147  exprt sum=object_offset;
148 
149  if(access_size.is_not_nil())
150  {
151  op=ID_gt;
152 
153  sum = plus_exprt(
154  typecast_exprt::conditional_cast(object_offset, access_size.type()),
155  access_size);
156  }
157 
158  return binary_relation_exprt(
159  typecast_exprt::conditional_cast(sum, malloc_size.type()), op, malloc_size);
160 }
161 
163  const exprt &pointer,
164  const exprt &access_size)
165 {
166  // this is
167  // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer)
168 
169  exprt object_size_expr=object_size(pointer);
170 
171  exprt object_offset=pointer_offset(pointer);
172 
173  // need to add size
174  irep_idt op=ID_ge;
175  exprt sum=object_offset;
176 
177  if(access_size.is_not_nil())
178  {
179  op=ID_gt;
180 
181  sum = plus_exprt(
182  typecast_exprt::conditional_cast(object_offset, access_size.type()),
183  access_size);
184  }
185 
186  return binary_relation_exprt(
187  typecast_exprt::conditional_cast(sum, object_size_expr.type()),
188  op,
189  object_size_expr);
190 }
191 
193  const exprt &pointer,
194  const exprt &offset)
195 {
196  exprt p_offset=pointer_offset(pointer);
197 
198  exprt zero=from_integer(0, p_offset.type());
199 
200  if(offset.is_not_nil())
201  {
202  p_offset = plus_exprt(
203  p_offset, typecast_exprt::conditional_cast(offset, p_offset.type()));
204  }
205 
206  return binary_relation_exprt(std::move(p_offset), ID_lt, std::move(zero));
207 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
typet::subtype
const typet & subtype() const
Definition: type.h:47
pointer_object
exprt pointer_object(const exprt &p)
Definition: pointer_predicates.cpp:23
arith_tools.h
good_pointer_def
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:84
null_pointer
exprt null_pointer(const exprt &pointer)
Definition: pointer_predicates.cpp:120
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
typet
The type of an expression, extends irept.
Definition: type.h:28
pointer_predicates.h
Various predicates over pointers in programs.
and_exprt
Boolean AND.
Definition: std_expr.h:1920
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:914
exprt
Base class for all expressions.
Definition: expr.h:54
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
good_pointer
exprt good_pointer(const exprt &pointer)
Definition: pointer_predicates.cpp:79
bool_typet
The Boolean type.
Definition: std_types.h:36
dynamic_object
exprt dynamic_object(const exprt &pointer)
Definition: pointer_predicates.cpp:72
namespace.h
equal_exprt
Equality.
Definition: std_expr.h:1225
notequal_exprt
Disequality.
Definition: std_expr.h:1283
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
null_pointer_exprt
The null pointer constant.
Definition: pointer_expr.h:703
nil_exprt
The NIL expression.
Definition: std_expr.h:2820
object_upper_bound
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
Definition: pointer_predicates.cpp:162
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
pointer_expr.h
API to expression classes for Pointers.
deallocated
exprt deallocated(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:51
signed_size_type
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
dead_object
exprt dead_object(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:59
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
integer_address
exprt integer_address(const exprt &pointer)
Definition: pointer_predicates.cpp:113
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
symbol.h
Symbol table entry.
object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:33
cprover_prefix.h
object_lower_bound
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Definition: pointer_predicates.cpp:192
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition: pointer_predicates.cpp:38
null_object
exprt null_object(const exprt &pointer)
Definition: pointer_predicates.cpp:107
malloc_object
exprt malloc_object(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:43
dynamic_object_upper_bound
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
Definition: pointer_predicates.cpp:133
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
same_object
exprt same_object(const exprt &p1, const exprt &p2)
Definition: pointer_predicates.cpp:28
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:279
is_invalid_pointer_exprt
Definition: pointer_predicates.h:54
dynamic_object_lower_bound
exprt dynamic_object_lower_bound(const exprt &pointer, const exprt &offset)
Definition: pointer_predicates.cpp:126
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
std_expr.h
API to expression classes.
dynamic_size
exprt dynamic_size(const namespacet &ns)
Definition: pointer_predicates.cpp:67
c_types.h
not_exprt
Boolean negation.
Definition: std_expr.h:2127