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_offset_size.h"
19 #include "std_expr.h"
20 #include "symbol.h"
21 
23 {
24  return unary_exprt(ID_pointer_object, p, size_type());
25 }
26 
27 exprt same_object(const exprt &p1, const exprt &p2)
28 {
29  return equal_exprt(pointer_object(p1), pointer_object(p2));
30 }
31 
32 exprt object_size(const exprt &pointer)
33 {
34  return unary_exprt(ID_object_size, pointer, size_type());
35 }
36 
37 exprt pointer_offset(const exprt &pointer)
38 {
39  return unary_exprt(ID_pointer_offset, pointer, signed_size_type());
40 }
41 
42 exprt malloc_object(const exprt &pointer, const namespacet &ns)
43 {
44  // we check __CPROVER_malloc_object!
45  const symbolt &malloc_object_symbol=ns.lookup(CPROVER_PREFIX "malloc_object");
46 
47  return same_object(pointer, malloc_object_symbol.symbol_expr());
48 }
49 
50 exprt deallocated(const exprt &pointer, const namespacet &ns)
51 {
52  // we check __CPROVER_deallocated!
53  const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "deallocated");
54 
55  return same_object(pointer, deallocated_symbol.symbol_expr());
56 }
57 
58 exprt dead_object(const exprt &pointer, const namespacet &ns)
59 {
60  // we check __CPROVER_dead_object!
61  const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "dead_object");
62 
63  return same_object(pointer, deallocated_symbol.symbol_expr());
64 }
65 
67 {
68  return ns.lookup(CPROVER_PREFIX "malloc_size").symbol_expr();
69 }
70 
71 exprt pointer_object_has_type(const exprt &pointer, const typet &type)
72 {
73  return false_exprt();
74 }
75 
76 exprt dynamic_object(const exprt &pointer)
77 {
78  exprt dynamic_expr(ID_dynamic_object, bool_typet());
79  dynamic_expr.copy_to_operands(pointer);
80  return dynamic_expr;
81 }
82 
83 exprt good_pointer(const exprt &pointer)
84 {
85  return unary_exprt(ID_good_pointer, pointer, bool_typet());
86 }
87 
89  const exprt &pointer,
90  const namespacet &ns)
91 {
93  const typet &dereference_type=pointer_type.subtype();
94 
95  const or_exprt good_dynamic_tmp1(
96  not_exprt(malloc_object(pointer, ns)),
97  and_exprt(
99  not_exprt(
101  pointer, dereference_type, ns, size_of_expr(dereference_type, ns)))));
102 
103  const and_exprt good_dynamic_tmp2(
104  not_exprt(deallocated(pointer, ns)), good_dynamic_tmp1);
105 
106  const or_exprt good_dynamic(
107  not_exprt(dynamic_object(pointer)), good_dynamic_tmp2);
108 
109  const not_exprt not_null(null_pointer(pointer));
110 
111  const not_exprt not_invalid(invalid_pointer(pointer));
112 
113  const or_exprt bad_other(
114  object_lower_bound(pointer, ns, nil_exprt()),
116  pointer, dereference_type, ns, size_of_expr(dereference_type, ns)));
117 
118  const or_exprt good_other(dynamic_object(pointer), not_exprt(bad_other));
119 
120  return and_exprt(
121  not_null,
122  not_invalid,
123  good_dynamic,
124  good_other);
125 }
126 
127 exprt null_object(const exprt &pointer)
128 {
130  return same_object(null_pointer, pointer);
131 }
132 
133 exprt integer_address(const exprt &pointer)
134 {
136  return and_exprt(same_object(null_pointer, pointer),
137  notequal_exprt(null_pointer, pointer));
138 }
139 
140 exprt null_pointer(const exprt &pointer)
141 {
143  return same_object(pointer, null_pointer);
144 }
145 
146 exprt invalid_pointer(const exprt &pointer)
147 {
148  return unary_exprt(ID_invalid_pointer, pointer, bool_typet());
149 }
150 
152  const exprt &pointer,
153  const namespacet &ns,
154  const exprt &offset)
155 {
156  return object_lower_bound(pointer, ns, offset);
157 }
158 
160  const exprt &pointer,
161  const typet &dereference_type,
162  const namespacet &ns,
163  const exprt &access_size)
164 {
165  // this is
166  // POINTER_OFFSET(p)+access_size>__CPROVER_malloc_size
167 
168  exprt malloc_size=dynamic_size(ns);
169 
170  exprt object_offset=pointer_offset(pointer);
171 
172  // need to add size
173  irep_idt op=ID_ge;
174  exprt sum=object_offset;
175 
176  if(access_size.is_not_nil())
177  {
178  op=ID_gt;
179 
180  if(ns.follow(object_offset.type())!=
181  ns.follow(access_size.type()))
182  object_offset.make_typecast(access_size.type());
183  sum=plus_exprt(object_offset, access_size);
184  }
185 
186  if(ns.follow(sum.type())!=
187  ns.follow(malloc_size.type()))
188  sum.make_typecast(malloc_size.type());
189 
190  return binary_relation_exprt(sum, op, malloc_size);
191 }
192 
194  const exprt &pointer,
195  const typet &dereference_type,
196  const namespacet &ns,
197  const exprt &access_size)
198 {
199  // this is
200  // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer)
201 
202  exprt object_size_expr=object_size(pointer);
203 
204  exprt object_offset=pointer_offset(pointer);
205 
206  // need to add size
207  irep_idt op=ID_ge;
208  exprt sum=object_offset;
209 
210  if(access_size.is_not_nil())
211  {
212  op=ID_gt;
213 
214  if(ns.follow(object_offset.type())!=
215  ns.follow(access_size.type()))
216  object_offset.make_typecast(access_size.type());
217  sum=plus_exprt(object_offset, access_size);
218  }
219 
220 
221  if(ns.follow(sum.type())!=
222  ns.follow(object_size_expr.type()))
223  sum.make_typecast(object_size_expr.type());
224 
225  return binary_relation_exprt(sum, op, object_size_expr);
226 }
227 
229  const exprt &pointer,
230  const namespacet &ns,
231  const exprt &offset)
232 {
233  exprt p_offset=pointer_offset(pointer);
234 
235  exprt zero=from_integer(0, p_offset.type());
236  assert(zero.is_not_nil());
237 
238  if(offset.is_not_nil())
239  {
240  if(ns.follow(p_offset.type())!=ns.follow(offset.type()))
241  p_offset=
242  plus_exprt(p_offset, typecast_exprt(offset, p_offset.type()));
243  else
244  p_offset=plus_exprt(p_offset, offset);
245  }
246 
247  return binary_relation_exprt(p_offset, ID_lt, zero);
248 }
The type of an expression.
Definition: type.h:22
exprt size_of_expr(const typet &type, const namespacet &ns)
Boolean negation.
Definition: std_expr.h:3230
semantic type conversion
Definition: std_expr.h:2111
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
bool is_not_nil() const
Definition: irep.h:103
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
Symbol table entry.
boolean OR
Definition: std_expr.h:2391
#define CPROVER_PREFIX
exprt object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
The null pointer constant.
Definition: std_expr.h:4520
typet & type()
Definition: expr.h:56
unsignedbv_typet size_type()
Definition: c_types.cpp:58
The proper Booleans.
Definition: std_types.h:34
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
exprt deallocated(const exprt &pointer, const namespacet &ns)
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
exprt null_object(const exprt &pointer)
equality
Definition: std_expr.h:1354
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:111
The NIL expression.
Definition: std_expr.h:4510
The pointer type.
Definition: std_types.h:1426
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:2255
API to expression classes.
exprt integer_address(const exprt &pointer)
Generic base class for unary expressions.
Definition: std_expr.h:303
inequality
Definition: std_expr.h:1406
TO_BE_DOCUMENTED.
Definition: namespace.h:74
The plus expression.
Definition: std_expr.h:893
exprt pointer_object_has_type(const exprt &pointer, const typet &type)
const typet & follow(const typet &) const
Definition: namespace.cpp:55
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:4499
Pointer Logic.
exprt malloc_object(const exprt &pointer, const namespacet &ns)
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:42
exprt pointer_offset(const exprt &pointer)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
exprt dynamic_object(const exprt &pointer)
exprt null_pointer(const exprt &pointer)
const typet & subtype() const
Definition: type.h:33
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:84
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130