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 or_exprt good_dynamic_tmp1(
95  not_exprt(malloc_object(pointer, ns)),
96  and_exprt(
98  not_exprt(
99  dynamic_object_upper_bound(pointer, ns, size_of_expr_opt.value()))));
100 
101  const and_exprt good_dynamic_tmp2(
102  not_exprt(deallocated(pointer, ns)), good_dynamic_tmp1);
103 
104  const or_exprt good_dynamic(
105  not_exprt(dynamic_object(pointer)), good_dynamic_tmp2);
106 
107  const not_exprt not_null(null_pointer(pointer));
108 
109  const not_exprt not_invalid{is_invalid_pointer_exprt{pointer}};
110 
111  const or_exprt bad_other(
112  object_lower_bound(pointer, nil_exprt()),
113  object_upper_bound(pointer, size_of_expr_opt.value()));
114 
115  const or_exprt good_other(dynamic_object(pointer), not_exprt(bad_other));
116 
117  return and_exprt(
118  not_null,
119  not_invalid,
120  good_dynamic,
121  good_other);
122 }
123 
124 exprt null_object(const exprt &pointer)
125 {
127  return same_object(null_pointer, pointer);
128 }
129 
130 exprt integer_address(const exprt &pointer)
131 {
133  return and_exprt(same_object(null_pointer, pointer),
134  notequal_exprt(null_pointer, pointer));
135 }
136 
137 exprt null_pointer(const exprt &pointer)
138 {
140  return same_object(pointer, null_pointer);
141 }
142 
144  const exprt &pointer,
145  const exprt &offset)
146 {
147  return object_lower_bound(pointer, offset);
148 }
149 
151  const exprt &pointer,
152  const namespacet &ns,
153  const exprt &access_size)
154 {
155  // this is
156  // POINTER_OFFSET(p)+access_size>__CPROVER_malloc_size
157 
158  exprt malloc_size=dynamic_size(ns);
159 
160  exprt object_offset=pointer_offset(pointer);
161 
162  // need to add size
163  irep_idt op=ID_ge;
164  exprt sum=object_offset;
165 
166  if(access_size.is_not_nil())
167  {
168  op=ID_gt;
169 
170  sum = plus_exprt(
171  typecast_exprt::conditional_cast(object_offset, access_size.type()),
172  access_size);
173  }
174 
175  return binary_relation_exprt(
176  typecast_exprt::conditional_cast(sum, malloc_size.type()), op, malloc_size);
177 }
178 
180  const exprt &pointer,
181  const exprt &access_size)
182 {
183  // this is
184  // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer)
185 
186  exprt object_size_expr=object_size(pointer);
187 
188  exprt object_offset=pointer_offset(pointer);
189 
190  // need to add size
191  irep_idt op=ID_ge;
192  exprt sum=object_offset;
193 
194  if(access_size.is_not_nil())
195  {
196  op=ID_gt;
197 
198  sum = plus_exprt(
199  typecast_exprt::conditional_cast(object_offset, access_size.type()),
200  access_size);
201  }
202 
203  return binary_relation_exprt(
204  typecast_exprt::conditional_cast(sum, object_size_expr.type()),
205  op,
206  object_size_expr);
207 }
208 
210  const exprt &pointer,
211  const exprt &offset)
212 {
213  exprt p_offset=pointer_offset(pointer);
214 
215  exprt zero=from_integer(0, p_offset.type());
216 
217  if(offset.is_not_nil())
218  {
219  p_offset = plus_exprt(
220  p_offset, typecast_exprt::conditional_cast(offset, p_offset.type()));
221  }
222 
223  return binary_relation_exprt(std::move(p_offset), ID_lt, std::move(zero));
224 }
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:137
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:1788
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:137
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
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:1834
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
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:1139
notequal_exprt
Disequality.
Definition: std_expr.h:1197
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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:141
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
or_exprt
Boolean OR.
Definition: std_expr.h:1942
null_pointer_exprt
The null pointer constant.
Definition: pointer_expr.h:461
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
object_upper_bound
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
Definition: pointer_predicates.cpp:179
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
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:130
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:209
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:124
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:150
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:100
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:278
is_invalid_pointer_exprt
Definition: pointer_predicates.h:48
dynamic_object_lower_bound
exprt dynamic_object_lower_bound(const exprt &pointer, const exprt &offset)
Definition: pointer_predicates.cpp:143
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:2041