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_is_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 {
87  const pointer_typet &pointer_type = to_pointer_type(pointer.type());
88  const typet &dereference_type=pointer_type.subtype();
89 
90  const auto size_of_expr_opt = size_of_expr(dereference_type, ns);
91  CHECK_RETURN(size_of_expr_opt.has_value());
92 
93  const or_exprt good_dynamic_tmp1(
94  not_exprt(malloc_object(pointer, ns)),
95  and_exprt(
97  not_exprt(
98  dynamic_object_upper_bound(pointer, ns, size_of_expr_opt.value()))));
99 
100  const and_exprt good_dynamic_tmp2(
101  not_exprt(deallocated(pointer, ns)), good_dynamic_tmp1);
102 
103  const or_exprt good_dynamic(
104  not_exprt(dynamic_object(pointer)), good_dynamic_tmp2);
105 
106  const not_exprt not_null(null_pointer(pointer));
107 
108  const not_exprt not_invalid{is_invalid_pointer_exprt{pointer}};
109 
110  const or_exprt bad_other(
111  object_lower_bound(pointer, nil_exprt()),
112  object_upper_bound(pointer, size_of_expr_opt.value()));
113 
114  const or_exprt good_other(dynamic_object(pointer), not_exprt(bad_other));
115 
116  return and_exprt(
117  not_null,
118  not_invalid,
119  good_dynamic,
120  good_other);
121 }
122 
123 exprt null_object(const exprt &pointer)
124 {
126  return same_object(null_pointer, pointer);
127 }
128 
129 exprt integer_address(const exprt &pointer)
130 {
132  return and_exprt(same_object(null_pointer, pointer),
133  notequal_exprt(null_pointer, pointer));
134 }
135 
136 exprt null_pointer(const exprt &pointer)
137 {
139  return same_object(pointer, null_pointer);
140 }
141 
143  const exprt &pointer,
144  const exprt &offset)
145 {
146  return object_lower_bound(pointer, offset);
147 }
148 
150  const exprt &pointer,
151  const namespacet &ns,
152  const exprt &access_size)
153 {
154  // this is
155  // POINTER_OFFSET(p)+access_size>__CPROVER_malloc_size
156 
157  exprt malloc_size=dynamic_size(ns);
158 
159  exprt object_offset=pointer_offset(pointer);
160 
161  // need to add size
162  irep_idt op=ID_ge;
163  exprt sum=object_offset;
164 
165  if(access_size.is_not_nil())
166  {
167  op=ID_gt;
168 
169  sum = plus_exprt(
170  typecast_exprt::conditional_cast(object_offset, access_size.type()),
171  access_size);
172  }
173 
174  return binary_relation_exprt(
175  typecast_exprt::conditional_cast(sum, malloc_size.type()), op, malloc_size);
176 }
177 
179  const exprt &pointer,
180  const exprt &access_size)
181 {
182  // this is
183  // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer)
184 
185  exprt object_size_expr=object_size(pointer);
186 
187  exprt object_offset=pointer_offset(pointer);
188 
189  // need to add size
190  irep_idt op=ID_ge;
191  exprt sum=object_offset;
192 
193  if(access_size.is_not_nil())
194  {
195  op=ID_gt;
196 
197  sum = plus_exprt(
198  typecast_exprt::conditional_cast(object_offset, access_size.type()),
199  access_size);
200  }
201 
202  return binary_relation_exprt(
203  typecast_exprt::conditional_cast(sum, object_size_expr.type()),
204  op,
205  object_size_expr);
206 }
207 
209  const exprt &pointer,
210  const exprt &offset)
211 {
212  exprt p_offset=pointer_offset(pointer);
213 
214  exprt zero=from_integer(0, p_offset.type());
215 
216  if(offset.is_not_nil())
217  {
218  p_offset = plus_exprt(
219  p_offset, typecast_exprt::conditional_cast(offset, p_offset.type()));
220  }
221 
222  return binary_relation_exprt(std::move(p_offset), ID_lt, std::move(zero));
223 }
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:150
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:2021
typet::subtype
const typet & subtype() const
Definition: type.h:47
pointer_object
exprt pointer_object(const exprt &p)
Definition: pointer_predicates.cpp:22
arith_tools.h
good_pointer_def
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:83
null_pointer
exprt null_pointer(const exprt &pointer)
Definition: pointer_predicates.cpp:136
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
pointer_predicates.h
Various predicates over pointers in programs.
and_exprt
Boolean AND.
Definition: std_expr.h:2137
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
exprt
Base class for all expressions.
Definition: expr.h:53
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:269
good_pointer
exprt good_pointer(const exprt &pointer)
Definition: pointer_predicates.cpp:78
bool_typet
The Boolean type.
Definition: std_types.h:37
dynamic_object
exprt dynamic_object(const exprt &pointer)
Definition: pointer_predicates.cpp:71
namespace.h
equal_exprt
Equality.
Definition: std_expr.h:1190
notequal_exprt
Disequality.
Definition: std_expr.h:1248
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:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
or_exprt
Boolean OR.
Definition: std_expr.h:2245
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
object_upper_bound
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
Definition: pointer_predicates.cpp:178
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
deallocated
exprt deallocated(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:50
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:58
integer_address
exprt integer_address(const exprt &pointer)
Definition: pointer_predicates.cpp:129
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:32
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
cprover_prefix.h
object_lower_bound
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Definition: pointer_predicates.cpp:208
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition: pointer_predicates.cpp:37
null_object
exprt null_object(const exprt &pointer)
Definition: pointer_predicates.cpp:123
malloc_object
exprt malloc_object(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:42
dynamic_object_upper_bound
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
Definition: pointer_predicates.cpp:149
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:99
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
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:27
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
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:142
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
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:66
c_types.h
not_exprt
Boolean negation.
Definition: std_expr.h:2843