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 exprt good_dynamic = not_exprt{deallocated(pointer, ns)};
95 
96  const not_exprt not_null(null_pointer(pointer));
97 
98  const not_exprt not_invalid{is_invalid_pointer_exprt{pointer}};
99 
100  const and_exprt good_bounds{
102  not_exprt{object_upper_bound(pointer, size_of_expr_opt.value())}};
103 
104  return and_exprt(not_null, not_invalid, good_dynamic, good_bounds);
105 }
106 
107 exprt null_object(const exprt &pointer)
108 {
110  return same_object(null_pointer, pointer);
111 }
112 
113 exprt integer_address(const exprt &pointer)
114 {
116  return and_exprt(same_object(null_pointer, pointer),
117  notequal_exprt(null_pointer, pointer));
118 }
119 
120 exprt null_pointer(const exprt &pointer)
121 {
123  return same_object(pointer, null_pointer);
124 }
125 
127  const exprt &pointer,
128  const exprt &offset)
129 {
130  return object_lower_bound(pointer, offset);
131 }
132 
134  const exprt &pointer,
135  const namespacet &ns,
136  const exprt &access_size)
137 {
138  // this is
139  // POINTER_OFFSET(p)+access_size>__CPROVER_malloc_size
140 
141  exprt malloc_size=dynamic_size(ns);
142 
143  exprt object_offset=pointer_offset(pointer);
144 
145  // need to add size
146  irep_idt op=ID_ge;
147  exprt sum=object_offset;
148 
149  if(access_size.is_not_nil())
150  {
151  op=ID_gt;
152 
153  sum = plus_exprt(
154  typecast_exprt::conditional_cast(object_offset, access_size.type()),
155  access_size);
156  }
157 
158  return binary_relation_exprt(
159  typecast_exprt::conditional_cast(sum, malloc_size.type()), op, malloc_size);
160 }
161 
163  const exprt &pointer,
164  const exprt &access_size)
165 {
166  // this is
167  // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer)
168 
169  exprt object_size_expr=object_size(pointer);
170 
171  exprt object_offset=pointer_offset(pointer);
172 
173  // need to add size
174  irep_idt op=ID_ge;
175  exprt sum=object_offset;
176 
177  if(access_size.is_not_nil())
178  {
179  op=ID_gt;
180 
181  sum = plus_exprt(
182  typecast_exprt::conditional_cast(object_offset, access_size.type()),
183  access_size);
184  }
185 
186  return binary_relation_exprt(
187  typecast_exprt::conditional_cast(sum, object_size_expr.type()),
188  op,
189  object_size_expr);
190 }
191 
193  const exprt &pointer,
194  const exprt &offset)
195 {
196  exprt p_offset=pointer_offset(pointer);
197 
198  exprt zero=from_integer(0, p_offset.type());
199 
200  if(offset.is_not_nil())
201  {
202  p_offset = plus_exprt(
203  p_offset, typecast_exprt::conditional_cast(offset, p_offset.type()));
204  }
205 
206  return binary_relation_exprt(std::move(p_offset), ID_lt, std::move(zero));
207 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
unsignedbv_typet size_type()
Definition: c_types.cpp:58
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
Boolean AND.
Definition: std_expr.h:1920
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
The Boolean type.
Definition: std_types.h:36
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_not_nil() const
Definition: irep.h:391
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2820
Boolean negation.
Definition: std_expr.h:2127
Disequality.
Definition: std_expr.h:1283
The null pointer constant.
Definition: pointer_expr.h:703
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
Symbol table entry.
Definition: symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
Generic base class for unary expressions.
Definition: std_expr.h:281
#define CPROVER_PREFIX
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt integer_address(const exprt &pointer)
exprt dynamic_object_lower_bound(const exprt &pointer, const exprt &offset)
exprt deallocated(const exprt &pointer, const namespacet &ns)
exprt object_size(const exprt &pointer)
exprt malloc_object(const exprt &pointer, const namespacet &ns)
exprt dynamic_size(const namespacet &ns)
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
exprt good_pointer(const exprt &pointer)
exprt dead_object(const exprt &pointer, const namespacet &ns)
exprt same_object(const exprt &p1, const exprt &p2)
exprt dynamic_object(const exprt &pointer)
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
exprt null_object(const exprt &pointer)
exprt null_pointer(const exprt &pointer)
exprt pointer_object(const exprt &p)
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Various predicates over pointers in programs.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
API to expression classes.
Symbol table entry.