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  CHECK_RETURN(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, extends irept.
Definition: type.h:27
exprt size_of_expr(const typet &type, const namespacet &ns)
Boolean negation.
Definition: std_expr.h:3308
Semantic type conversion.
Definition: std_expr.h:2277
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
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:2531
#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)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
The null pointer constant.
Definition: std_expr.h:4471
typet & type()
Return the type of the expression.
Definition: expr.h:68
unsignedbv_typet size_type()
Definition: c_types.cpp:58
The Boolean type.
Definition: std_types.h:28
Symbol table entry.
Definition: symbol.h:27
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
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:1484
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:121
The NIL expression.
Definition: std_expr.h:4461
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
exprt pointer_object(const exprt &p)
Boolean AND.
Definition: std_expr.h:2409
API to expression classes.
exprt integer_address(const exprt &pointer)
Generic base class for unary expressions.
Definition: std_expr.h:331
Disequality.
Definition: std_expr.h:1545
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
exprt object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
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:54
exprt pointer_offset(const exprt &pointer)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
exprt dynamic_object(const exprt &pointer)
exprt null_pointer(const exprt &pointer)
const typet & subtype() const
Definition: type.h:38
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)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166