CBMC
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 pointer_object_exprt(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 object_size_exprt(pointer, size_type());
36 }
37 
38 exprt pointer_offset(const exprt &pointer)
39 {
40  return pointer_offset_exprt(pointer, size_type());
41 }
42 
43 exprt deallocated(const exprt &pointer, const namespacet &ns)
44 {
45  // we check __CPROVER_deallocated!
46  const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "deallocated");
47 
48  return same_object(pointer, deallocated_symbol.symbol_expr());
49 }
50 
51 exprt dead_object(const exprt &pointer, const namespacet &ns)
52 {
53  // we check __CPROVER_dead_object!
54  const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "dead_object");
55 
56  return same_object(pointer, deallocated_symbol.symbol_expr());
57 }
58 
59 exprt null_object(const exprt &pointer)
60 {
61  null_pointer_exprt null_pointer(to_pointer_type(pointer.type()));
62  return same_object(null_pointer, pointer);
63 }
64 
65 exprt integer_address(const exprt &pointer)
66 {
67  null_pointer_exprt null_pointer(to_pointer_type(pointer.type()));
68  return and_exprt(same_object(null_pointer, pointer),
69  notequal_exprt(null_pointer, pointer));
70 }
71 
73  const exprt &pointer,
74  const exprt &access_size)
75 {
76  exprt object_offset = pointer_offset(pointer);
77 
78  exprt object_size_expr=object_size(pointer);
79 
80  std::size_t max_width = std::max(
81  to_bitvector_type(object_offset.type()).get_width(),
82  to_bitvector_type(object_size_expr.type()).get_width());
83 
84  // We add the size to the offset, if given.
85  if(access_size.is_not_nil())
86  {
87  // This is
88  // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer)
89  // We enlarge all bit-vectors to avoid an overflow on the addition.
90 
91  max_width =
92  std::max(max_width, to_bitvector_type(access_size.type()).get_width());
93 
94  auto type = unsignedbv_typet(max_width + 1);
95 
96  auto sum = plus_exprt(
97  typecast_exprt::conditional_cast(object_offset, type),
98  typecast_exprt::conditional_cast(access_size, type));
99 
100  return binary_relation_exprt(
101  sum, ID_gt, typecast_exprt::conditional_cast(object_size_expr, type));
102  }
103  else
104  {
105  // This is
106  // POINTER_OFFSET(p)>=OBJECT_SIZE(pointer)
107 
108  auto type = unsignedbv_typet(max_width);
109 
110  return binary_relation_exprt(
111  typecast_exprt::conditional_cast(object_offset, type),
112  ID_ge,
113  typecast_exprt::conditional_cast(object_size_expr, type));
114  }
115 }
116 
118  const exprt &pointer,
119  const exprt &offset)
120 {
121  exprt p_offset=pointer_offset(pointer);
122 
123  exprt zero=from_integer(0, p_offset.type());
124 
125  if(offset.is_not_nil())
126  {
127  p_offset = plus_exprt(
128  p_offset, typecast_exprt::conditional_cast(offset, p_offset.type()));
129  }
130 
131  return binary_relation_exprt(std::move(p_offset), ID_lt, std::move(zero));
132 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Boolean AND.
Definition: std_expr.h:2120
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
std::size_t get_width() const
Definition: std_types.h:925
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_not_nil() const
Definition: irep.h:372
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
Disequality.
Definition: std_expr.h:1420
The null pointer constant.
Definition: pointer_expr.h:909
Expression for finding the size (in bytes) of the object a pointer points to.
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
A numerical identifier for the object a pointer points to.
The offset (in bytes) of a pointer relative to the object.
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:2076
Fixed-width bit-vector with unsigned binary interpretation.
#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:93
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt integer_address(const exprt &pointer)
exprt deallocated(const exprt &pointer, const namespacet &ns)
exprt object_size(const exprt &pointer)
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
exprt dead_object(const exprt &pointer, const namespacet &ns)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_object(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.
API to expression classes.
Symbol table entry.
#define size_type
Definition: unistd.c:347