cprover
dereference.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "dereference.h"
13 
14 #ifdef DEBUG
15 #include <iostream>
16 #include <util/format_expr.h>
17 #endif
18 
19 #include <util/std_expr.h>
20 #include <util/byte_operators.h>
22 #include <util/base_type.h>
23 #include <util/simplify_expr.h>
24 #include <util/arith_tools.h>
25 
26 #include <util/c_types.h>
27 
29 {
30  if(pointer.type().id()!=ID_pointer)
31  throw "dereference expected pointer type, but got "+
32  pointer.type().pretty();
33 
34  // type of the object
35  const typet &type=pointer.type().subtype();
36 
37  #ifdef DEBUG
38  std::cout << "DEREF: " << format(pointer) << '\n';
39  #endif
40 
41  return dereference_rec(
42  pointer,
43  from_integer(0, index_type()), // offset
44  type);
45 }
46 
51  const exprt &object,
52  const exprt &offset,
53  const typet &type)
54 {
55  const typet &object_type=ns.follow(object.type());
56  const typet &dest_type=ns.follow(type);
57 
58  // is the object an array with matching subtype?
59 
60  exprt simplified_offset=simplify_expr(offset, ns);
61 
62  // check if offset is zero
63  if(simplified_offset.is_zero())
64  {
65  // check type
66  if(base_type_eq(object_type, dest_type, ns))
67  {
68  return object; // trivial case
69  }
70  else if(type_compatible(object_type, dest_type))
71  {
72  // the type differs, but we can do this with a typecast
73  return typecast_exprt(object, dest_type);
74  }
75  }
76 
77  if(object.id()==ID_index)
78  {
79  const index_exprt &index_expr=to_index_expr(object);
80 
81  exprt index=index_expr.index();
82 
83  // multiply index by object size
84  exprt size=size_of_expr(object_type, ns);
85 
86  if(size.is_nil())
87  throw "dereference failed to get object size for index";
88 
89  index.make_typecast(simplified_offset.type());
90  size.make_typecast(index.type());
91 
92  const plus_exprt new_offset(simplified_offset, mult_exprt(index, size));
93 
94  return read_object(index_expr.array(), new_offset, type);
95  }
96  else if(object.id()==ID_member)
97  {
98  const member_exprt &member_expr=to_member_expr(object);
99 
100  const typet &compound_type=
101  ns.follow(member_expr.struct_op().type());
102 
103  if(compound_type.id()==ID_struct)
104  {
105  const struct_typet &struct_type=
106  to_struct_type(compound_type);
107 
109  struct_type, member_expr.get_component_name(), ns);
110 
111  if(member_offset.is_nil())
112  throw "dereference failed to get member offset";
113 
114  member_offset.make_typecast(simplified_offset.type());
115 
116  const plus_exprt new_offset(simplified_offset, member_offset);
117 
118  return read_object(member_expr.struct_op(), new_offset, type);
119  }
120  else if(compound_type.id()==ID_union)
121  {
122  // Unions are easy: the offset is always zero,
123  // so simply pass down.
124  return read_object(member_expr.struct_op(), offset, type);
125  }
126  }
127 
128  // check if we have an array with the right subtype
129  if(object_type.id()==ID_array &&
130  base_type_eq(object_type.subtype(), dest_type, ns))
131  {
132  // check proper alignment
133  exprt size=size_of_expr(dest_type, ns);
134 
135  if(size.is_not_nil())
136  {
137  mp_integer size_constant, offset_constant;
138  if(!to_integer(simplify_expr(size, ns), size_constant) &&
139  !to_integer(simplified_offset, offset_constant) &&
140  (offset_constant%size_constant)==0)
141  {
142  // Yes! Can use index expression!
143  mp_integer index_constant=offset_constant/size_constant;
144  exprt index_expr=from_integer(index_constant, size.type());
145  return index_exprt(object, index_expr, dest_type);
146  }
147  }
148  }
149 
150  // give up and use byte_extract
151  return byte_extract_exprt(
152  byte_extract_id(), object, simplified_offset, dest_type);
153 }
154 
158  const exprt &address,
159  const exprt &offset,
160  const typet &type)
161 {
162  if(address.id()==ID_address_of)
163  {
164  const address_of_exprt &address_of_expr=to_address_of_expr(address);
165 
166  const exprt &object=address_of_expr.object();
167 
168  return read_object(object, offset, type);
169  }
170  else if(address.id()==ID_typecast)
171  {
172  const typecast_exprt &typecast_expr=to_typecast_expr(address);
173 
174  return dereference_typecast(typecast_expr, offset, type);
175  }
176  else if(address.id()==ID_plus)
177  {
178  // pointer arithmetic
179  if(address.operands().size()<2)
180  throw "plus with less than two operands";
181 
182  return dereference_plus(address, offset, type);
183  }
184  else if(address.id()==ID_if)
185  {
186  const if_exprt &if_expr=to_if_expr(address);
187 
188  return dereference_if(if_expr, offset, type);
189  }
190  else if(address.id()==ID_constant)
191  {
192  const typet result_type=ns.follow(address.type()).subtype();
193 
194  // pointer-typed constant
195  if(to_constant_expr(address).get_value()==ID_NULL) // NULL
196  {
197  // we turn this into (type *)0
198  exprt zero=from_integer(0, index_type());
199  return dereference_rec(
200  typecast_exprt(zero, address.type()), offset, type);
201  }
202  else
203  throw "dereferencet: unexpected pointer constant "+address.pretty();
204  }
205  else
206  {
207  throw "failed to dereference `"+address.id_string()+"'";
208  }
209 }
210 
219  const if_exprt &expr,
220  const exprt &offset,
221  const typet &type)
222 {
223  // push down the if, do recursive call
224  exprt true_case=dereference_rec(expr.true_case(), offset, type);
225  exprt false_case=dereference_rec(expr.false_case(), offset, type);
226 
227  return if_exprt(expr.cond(), true_case, false_case);
228 }
229 
234  const exprt &expr,
235  const exprt &offset,
236  const typet &type)
237 {
238  exprt pointer=expr.op0();
239  exprt integer=expr.op1();
240 
241  // need not be binary
242  if(expr.operands().size()>2)
243  {
244  assert(expr.op0().type().id()==ID_pointer);
245 
246  exprt::operandst plus_ops(
247  ++expr.operands().begin(), expr.operands().end());
248  integer.operands().swap(plus_ops);
249  }
250 
251  if(ns.follow(integer.type()).id()==ID_pointer)
252  std::swap(pointer, integer);
253 
254  // multiply integer by object size
255  exprt size=size_of_expr(pointer.type().subtype(), ns);
256  if(size.is_nil())
257  throw "dereference failed to get object size for pointer arithmetic";
258 
259  // make types of offset and size match
260  if(size.type()!=integer.type())
261  integer.make_typecast(size.type());
262 
263  const plus_exprt new_offset(offset, mult_exprt(size, integer));
264 
265  return dereference_rec(pointer, new_offset, type);
266 }
267 
277  const typecast_exprt &expr,
278  const exprt &offset,
279  const typet &type)
280 {
281  const exprt &op=expr.op();
282  const typet &op_type=ns.follow(op.type());
283 
284  // pointer type cast?
285  if(op_type.id()==ID_pointer)
286  return dereference_rec(op, offset, type); // just pass down
287  else if(op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv)
288  {
289  // We got an integer-typed address A. We turn this
290  // into integer_dereference(A+offset),
291  // and then let some other layer worry about it.
292 
293  exprt integer=op;
294 
295  if(!offset.is_zero())
296  integer=
297  plus_exprt(offset, typecast_exprt(op, offset.type()));
298 
299  return unary_exprt(ID_integer_dereference, integer, type);
300  }
301  else
302  throw "dereferencet: unexpected cast";
303 }
304 
308  const typet &object_type,
309  const typet &dereference_type) const
310 {
311  if(dereference_type.id()==ID_empty)
312  return true; // always ok
313 
314  if(base_type_eq(object_type, dereference_type, ns))
315  return true; // ok, they just match
316 
317  // check for struct prefixes
318 
319  if(object_type.id()==ID_struct &&
320  dereference_type.id()==ID_struct)
321  {
322  if(to_struct_type(dereference_type).is_prefix_of(
323  to_struct_type(object_type)))
324  return true; // ok, dereference_type is a prefix of object_type
325  }
326 
327  // any code is ok
328  if(dereference_type.id()==ID_code &&
329  object_type.id()==ID_code)
330  return true;
331 
332  // bit vectors of same size are ok
333  if((object_type.id()==ID_signedbv || object_type.id()==ID_unsignedbv) &&
334  (dereference_type.id()==ID_signedbv ||
335  dereference_type.id()==ID_unsignedbv))
336  {
337  return object_type.get(ID_width)==dereference_type.get(ID_width);
338  }
339 
340  // Any pointer to pointer is always ok,
341  // but should likely check that width is the same.
342  if(object_type.id()==ID_pointer &&
343  dereference_type.id()==ID_pointer)
344  return true;
345 
346  // really different
347 
348  return false;
349 }
pointer_offset_size.h
format
static format_containert< T > format(const T &o)
Definition: format.h:35
typet::subtype
const typet & subtype() const
Definition: type.h:38
to_integer
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
arith_tools.h
dereferencet::dereference_typecast
exprt dereference_typecast(const typecast_exprt &expr, const exprt &offset, const typet &type)
Attempt to dereference the object at address expr + offset and of type type.
Definition: dereference.cpp:276
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
address_of_exprt::object
exprt & object()
Definition: std_expr.h:3265
typet
The type of an expression, extends irept.
Definition: type.h:27
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
dereferencet::read_object
exprt read_object(const exprt &object, const exprt &offset, const typet &type)
Definition: dereference.cpp:50
member_offset_expr
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:230
struct_typet::is_prefix_of
bool is_prefix_of(const struct_typet &other) const
Returns true if the struct is a prefix of other, i.e., if this struct has n components then the compo...
Definition: std_types.cpp:106
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
exprt
Base class for all expressions.
Definition: expr.h:54
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:331
exprt::op0
exprt & op0()
Definition: expr.h:84
simplify_expr
exprt simplify_expr(const exprt &src, const namespacet &ns)
Definition: simplify_expr.cpp:2325
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3465
dereferencet::operator()
exprt operator()(const exprt &pointer)
Dereference the given pointer-expression.
Definition: dereference.cpp:28
byte_extract_id
irep_idt byte_extract_id()
Definition: byte_operators.cpp:13
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
byte_operators.h
Expression classes for byte-level operators.
base_type.h
size_of_expr
exprt size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:292
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
base_type_eq
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3931
irept::id_string
const std::string & id_string() const
Definition: irep.h:262
exprt::op1
exprt & op1()
Definition: expr.h:87
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
index_exprt::index
exprt & index()
Definition: std_expr.h:1631
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
dereferencet::dereference_plus
exprt dereference_plus(const exprt &expr, const exprt &offset, const typet &type)
Attempt to dereference the object at address expr + offset and of type type.
Definition: dereference.cpp:233
dereferencet::ns
const namespacet & ns
Definition: dereference.h:39
simplify_expr.h
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
dereferencet::dereference_rec
exprt dereference_rec(const exprt &address, const exprt &offset, const typet &type)
Attempt to dereference the object at address address + offset and of type type.
Definition: dereference.cpp:157
format_expr.h
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3455
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3445
byte_extract_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:25
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3915
exprt::operands
operandst & operands()
Definition: expr.h:78
dereference.h
index_exprt
Array index operator.
Definition: std_expr.h:1595
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
std_expr.h
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:4403
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:24
c_types.h
dereferencet::type_compatible
bool type_compatible(const typet &object_type, const typet &dereference_type) const
Check that it is ok to cast an object of type object_type to deference_type.
Definition: dereference.cpp:307
dereferencet::dereference_if
exprt dereference_if(const if_exprt &expr, const exprt &offset, const typet &type)
Attempt to dereference the object at address expr + offset and of type type.
Definition: dereference.cpp:218
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423