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 dynamic_object(const exprt &pointer)
72 {
73  exprt dynamic_expr(ID_dynamic_object, bool_typet());
74  dynamic_expr.copy_to_operands(pointer);
75  return dynamic_expr;
76 }
77 
78 exprt good_pointer(const exprt &pointer)
79 {
80  return unary_exprt(ID_good_pointer, pointer, bool_typet());
81 }
82 
84  const exprt &pointer,
85  const namespacet &ns)
86 {
88  const typet &dereference_type=pointer_type.subtype();
89 
90  const or_exprt good_dynamic_tmp1(
91  not_exprt(malloc_object(pointer, ns)),
92  and_exprt(
94  not_exprt(
96  pointer, ns, size_of_expr(dereference_type, ns)))));
97 
98  const and_exprt good_dynamic_tmp2(
99  not_exprt(deallocated(pointer, ns)), good_dynamic_tmp1);
100 
101  const or_exprt good_dynamic(
102  not_exprt(dynamic_object(pointer)), good_dynamic_tmp2);
103 
104  const not_exprt not_null(null_pointer(pointer));
105 
106  const not_exprt not_invalid(invalid_pointer(pointer));
107 
108  const or_exprt bad_other(
109  object_lower_bound(pointer, ns, nil_exprt()),
111  pointer, ns, size_of_expr(dereference_type, ns)));
112 
113  const or_exprt good_other(dynamic_object(pointer), not_exprt(bad_other));
114 
115  return and_exprt(
116  not_null,
117  not_invalid,
118  good_dynamic,
119  good_other);
120 }
121 
122 exprt null_object(const exprt &pointer)
123 {
125  return same_object(null_pointer, pointer);
126 }
127 
128 exprt integer_address(const exprt &pointer)
129 {
131  return and_exprt(same_object(null_pointer, pointer),
132  notequal_exprt(null_pointer, pointer));
133 }
134 
135 exprt null_pointer(const exprt &pointer)
136 {
138  return same_object(pointer, null_pointer);
139 }
140 
141 exprt invalid_pointer(const exprt &pointer)
142 {
143  return unary_exprt(ID_invalid_pointer, pointer, bool_typet());
144 }
145 
147  const exprt &pointer,
148  const namespacet &ns,
149  const exprt &offset)
150 {
151  return object_lower_bound(pointer, ns, offset);
152 }
153 
155  const exprt &pointer,
156  const namespacet &ns,
157  const exprt &access_size)
158 {
159  // this is
160  // POINTER_OFFSET(p)+access_size>__CPROVER_malloc_size
161 
162  exprt malloc_size=dynamic_size(ns);
163 
164  exprt object_offset=pointer_offset(pointer);
165 
166  // need to add size
167  irep_idt op=ID_ge;
168  exprt sum=object_offset;
169 
170  if(access_size.is_not_nil())
171  {
172  op=ID_gt;
173 
174  if(ns.follow(object_offset.type())!=
175  ns.follow(access_size.type()))
176  object_offset.make_typecast(access_size.type());
177  sum=plus_exprt(object_offset, access_size);
178  }
179 
180  if(ns.follow(sum.type())!=
181  ns.follow(malloc_size.type()))
182  sum.make_typecast(malloc_size.type());
183 
184  return binary_relation_exprt(sum, op, malloc_size);
185 }
186 
188  const exprt &pointer,
189  const namespacet &ns,
190  const exprt &access_size)
191 {
192  // this is
193  // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer)
194 
195  exprt object_size_expr=object_size(pointer);
196 
197  exprt object_offset=pointer_offset(pointer);
198 
199  // need to add size
200  irep_idt op=ID_ge;
201  exprt sum=object_offset;
202 
203  if(access_size.is_not_nil())
204  {
205  op=ID_gt;
206 
207  if(ns.follow(object_offset.type())!=
208  ns.follow(access_size.type()))
209  object_offset.make_typecast(access_size.type());
210  sum=plus_exprt(object_offset, access_size);
211  }
212 
213 
214  if(ns.follow(sum.type())!=
215  ns.follow(object_size_expr.type()))
216  sum.make_typecast(object_size_expr.type());
217 
218  return binary_relation_exprt(sum, op, object_size_expr);
219 }
220 
222  const exprt &pointer,
223  const namespacet &ns,
224  const exprt &offset)
225 {
226  exprt p_offset=pointer_offset(pointer);
227 
228  exprt zero=from_integer(0, p_offset.type());
229  assert(zero.is_not_nil());
230 
231  if(offset.is_not_nil())
232  {
233  if(ns.follow(p_offset.type())!=ns.follow(offset.type()))
234  p_offset=
235  plus_exprt(p_offset, typecast_exprt(offset, p_offset.type()));
236  else
237  p_offset=plus_exprt(p_offset, offset);
238  }
239 
240  return binary_relation_exprt(p_offset, ID_lt, zero);
241 }
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:3228
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:173
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:4518
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)
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
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:4508
The pointer type.
Definition: std_types.h:1435
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 object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
const typet & follow(const typet &) const
Definition: namespace.cpp:55
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Various predicates over pointers in programs.
exprt dynamic_object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
Pointer Logic.
exprt malloc_object(const exprt &pointer, const namespacet &ns)
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:1459
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:136