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 "c_types.h"
15 #include "cprover_prefix.h"
16 #include "namespace.h"
17 #include "std_expr.h"
18 #include "expr_util.h"
19 #include "arith_tools.h"
20 #include "pointer_offset_size.h"
21 #include "config.h"
22 #include "symbol.h"
23 
25 {
26  return unary_exprt(ID_pointer_object, p, size_type());
27 }
28 
29 exprt same_object(const exprt &p1, const exprt &p2)
30 {
31  return equal_exprt(pointer_object(p1), pointer_object(p2));
32 }
33 
34 exprt object_size(const exprt &pointer)
35 {
36  return unary_exprt(ID_object_size, pointer, size_type());
37 }
38 
39 exprt pointer_offset(const exprt &pointer)
40 {
41  return unary_exprt(ID_pointer_offset, pointer, signed_size_type());
42 }
43 
44 exprt malloc_object(const exprt &pointer, const namespacet &ns)
45 {
46  // we check __CPROVER_malloc_object!
47  const symbolt &malloc_object_symbol=ns.lookup(CPROVER_PREFIX "malloc_object");
48 
49  return same_object(pointer, malloc_object_symbol.symbol_expr());
50 }
51 
52 exprt deallocated(const exprt &pointer, const namespacet &ns)
53 {
54  // we check __CPROVER_deallocated!
55  const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "deallocated");
56 
57  return same_object(pointer, deallocated_symbol.symbol_expr());
58 }
59 
60 exprt dead_object(const exprt &pointer, const namespacet &ns)
61 {
62  // we check __CPROVER_dead_object!
63  const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "dead_object");
64 
65  return same_object(pointer, deallocated_symbol.symbol_expr());
66 }
67 
69 {
70  return ns.lookup(CPROVER_PREFIX "malloc_size").symbol_expr();
71 }
72 
73 exprt pointer_object_has_type(const exprt &pointer, const typet &type)
74 {
75  return false_exprt();
76 }
77 
78 exprt dynamic_object(const exprt &pointer)
79 {
80  exprt dynamic_expr(ID_dynamic_object, bool_typet());
81  dynamic_expr.copy_to_operands(pointer);
82  return dynamic_expr;
83 }
84 
85 exprt good_pointer(const exprt &pointer)
86 {
87  return unary_exprt(ID_good_pointer, pointer, bool_typet());
88 }
89 
91  const exprt &pointer,
92  const namespacet &ns)
93 {
95  const typet &dereference_type=pointer_type.subtype();
96 
97  exprt good_dynamic_tmp1=
98  or_exprt(
99  not_exprt(malloc_object(pointer, ns)),
100  and_exprt(
101  not_exprt(
103  pointer,
104  ns,
105  nil_exprt())),
106  not_exprt(
108  pointer,
109  dereference_type,
110  ns,
111  size_of_expr(dereference_type, ns)))));
112 
113  exprt good_dynamic_tmp2=
114  and_exprt(not_exprt(deallocated(pointer, ns)),
115  good_dynamic_tmp1);
116 
117  exprt good_dynamic=
119  good_dynamic_tmp2);
120 
121  exprt not_null=
122  not_exprt(null_pointer(pointer));
123 
124  exprt not_invalid=
125  not_exprt(invalid_pointer(pointer));
126 
127  exprt bad_other=
128  or_exprt(object_lower_bound(pointer, ns, nil_exprt()),
130  pointer,
131  dereference_type,
132  ns,
133  size_of_expr(dereference_type, ns)));
134 
135  exprt good_other=
136  or_exprt(dynamic_object(pointer),
137  not_exprt(bad_other));
138 
139  return and_exprt(
140  not_null,
141  not_invalid,
142  good_dynamic,
143  good_other);
144 }
145 
146 exprt null_object(const exprt &pointer)
147 {
149  return same_object(null_pointer, pointer);
150 }
151 
152 exprt integer_address(const exprt &pointer)
153 {
155  return and_exprt(same_object(null_pointer, pointer),
156  notequal_exprt(null_pointer, pointer));
157 }
158 
159 exprt null_pointer(const exprt &pointer)
160 {
162  return same_object(pointer, null_pointer);
163 }
164 
165 exprt invalid_pointer(const exprt &pointer)
166 {
167  return unary_exprt(ID_invalid_pointer, pointer, bool_typet());
168 }
169 
171  const exprt &pointer,
172  const namespacet &ns,
173  const exprt &offset)
174 {
175  return object_lower_bound(pointer, ns, offset);
176 }
177 
179  const exprt &pointer,
180  const typet &dereference_type,
181  const namespacet &ns,
182  const exprt &access_size)
183 {
184  // this is
185  // POINTER_OFFSET(p)+access_size>__CPROVER_malloc_size
186 
187  exprt malloc_size=dynamic_size(ns);
188 
189  exprt object_offset=pointer_offset(pointer);
190 
191  // need to add size
192  irep_idt op=ID_ge;
193  exprt sum=object_offset;
194 
195  if(access_size.is_not_nil())
196  {
197  op=ID_gt;
198 
199  if(ns.follow(object_offset.type())!=
200  ns.follow(access_size.type()))
201  object_offset.make_typecast(access_size.type());
202  sum=plus_exprt(object_offset, access_size);
203  }
204 
205  if(ns.follow(sum.type())!=
206  ns.follow(malloc_size.type()))
207  sum.make_typecast(malloc_size.type());
208 
209  return binary_relation_exprt(sum, op, malloc_size);
210 }
211 
213  const exprt &pointer,
214  const typet &dereference_type,
215  const namespacet &ns,
216  const exprt &access_size)
217 {
218  // this is
219  // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer)
220 
221  exprt object_size_expr=object_size(pointer);
222 
223  exprt object_offset=pointer_offset(pointer);
224 
225  // need to add size
226  irep_idt op=ID_ge;
227  exprt sum=object_offset;
228 
229  if(access_size.is_not_nil())
230  {
231  op=ID_gt;
232 
233  if(ns.follow(object_offset.type())!=
234  ns.follow(access_size.type()))
235  object_offset.make_typecast(access_size.type());
236  sum=plus_exprt(object_offset, access_size);
237  }
238 
239 
240  if(ns.follow(sum.type())!=
241  ns.follow(object_size_expr.type()))
242  sum.make_typecast(object_size_expr.type());
243 
244  return binary_relation_exprt(sum, op, object_size_expr);
245 }
246 
248  const exprt &pointer,
249  const namespacet &ns,
250  const exprt &offset)
251 {
252  exprt p_offset=pointer_offset(pointer);
253 
254  exprt zero=from_integer(0, p_offset.type());
255  assert(zero.is_not_nil());
256 
257  if(offset.is_not_nil())
258  {
259  if(ns.follow(p_offset.type())!=ns.follow(offset.type()))
260  p_offset=
261  plus_exprt(p_offset, typecast_exprt(offset, p_offset.type()));
262  else
263  p_offset=plus_exprt(p_offset, offset);
264  }
265 
266  return binary_relation_exprt(p_offset, ID_lt, zero);
267 }
The type of an expression.
Definition: type.h:20
exprt size_of_expr(const typet &type, const namespacet &ns)
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
Boolean negation.
Definition: std_expr.h:2648
semantic type conversion
Definition: std_expr.h:1725
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
bool is_not_nil() const
Definition: irep.h:104
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
Symbol table entry.
boolean OR
Definition: std_expr.h:1968
#define CPROVER_PREFIX
exprt object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
Deprecated expression utility functions.
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
The null pointer constant.
Definition: std_expr.h:3774
typet & type()
Definition: expr.h:60
unsignedbv_typet size_type()
Definition: c_types.cpp:57
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
exprt deallocated(const exprt &pointer, const namespacet &ns)
signedbv_typet signed_size_type()
Definition: c_types.cpp:73
exprt null_object(const exprt &pointer)
equality
Definition: std_expr.h:1082
exprt good_pointer(const exprt &pointer)
exprt object_size(const exprt &pointer)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
The NIL expression.
Definition: std_expr.h:3764
The pointer type.
Definition: std_types.h:1343
exprt object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
exprt pointer_object(const exprt &p)
boolean AND
Definition: std_expr.h:1852
API to expression classes.
exprt integer_address(const exprt &pointer)
Generic base class for unary expressions.
Definition: std_expr.h:221
inequality
Definition: std_expr.h:1124
TO_BE_DOCUMENTED.
Definition: namespace.h:62
The plus expression.
Definition: std_expr.h:702
exprt pointer_object_has_type(const exprt &pointer, const typet &type)
Various predicates over pointers in programs.
exprt dynamic_object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
The boolean constant false.
Definition: std_expr.h:3753
Pointer Logic.
exprt malloc_object(const exprt &pointer, const namespacet &ns)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1377
exprt dynamic_object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
exprt dynamic_size(const namespacet &ns)
exprt invalid_pointer(const exprt &pointer)
Base class for all expressions.
Definition: expr.h:46
exprt pointer_offset(const exprt &pointer)
exprt dynamic_object(const exprt &pointer)
exprt null_pointer(const exprt &pointer)
const typet & subtype() const
Definition: type.h:31
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt dead_object(const exprt &pointer, const namespacet &ns)
exprt same_object(const exprt &p1, const exprt &p2)
void make_typecast(const typet &_type)
Definition: expr.cpp:90