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 
31 {
32  if(pointer.type().id()!=ID_pointer)
33  throw "dereference expected pointer type, but got "+
34  pointer.type().pretty();
35 
36  // type of the object
37  const typet &type=pointer.type().subtype();
38 
39  #ifdef DEBUG
40  std::cout << "DEREF: " << format(pointer) << '\n';
41  #endif
42 
43  return dereference_rec(
44  pointer,
45  from_integer(0, index_type()), // offset
46  type);
47 }
48 
50  const exprt &object,
51  const exprt &offset,
52  const typet &type)
53 {
54  const typet &object_type=ns.follow(object.type());
55  const typet &dest_type=ns.follow(type);
56 
57  // is the object an array with matching subtype?
58 
59  exprt simplified_offset=simplify_expr(offset, ns);
60 
61  // check if offset is zero
62  if(simplified_offset.is_zero())
63  {
64  // check type
65  if(base_type_eq(object_type, dest_type, ns))
66  {
67  return object; // trivial case
68  }
69  else if(type_compatible(object_type, dest_type))
70  {
71  // the type differs, but we can do this with a typecast
72  return typecast_exprt(object, dest_type);
73  }
74  }
75 
76  if(object.id()==ID_index)
77  {
78  const index_exprt &index_expr=to_index_expr(object);
79 
80  exprt index=index_expr.index();
81 
82  // multiply index by object size
83  exprt size=size_of_expr(object_type, ns);
84 
85  if(size.is_nil())
86  throw "dereference failed to get object size for index";
87 
88  index.make_typecast(simplified_offset.type());
89  size.make_typecast(index.type());
90 
91  const plus_exprt new_offset(simplified_offset, mult_exprt(index, size));
92 
93  return read_object(index_expr.array(), new_offset, type);
94  }
95  else if(object.id()==ID_member)
96  {
97  const member_exprt &member_expr=to_member_expr(object);
98 
99  const typet &compound_type=
100  ns.follow(member_expr.struct_op().type());
101 
102  if(compound_type.id()==ID_struct)
103  {
104  const struct_typet &struct_type=
105  to_struct_type(compound_type);
106 
108  struct_type, member_expr.get_component_name(), ns);
109 
110  if(member_offset.is_nil())
111  throw "dereference failed to get member offset";
112 
113  member_offset.make_typecast(simplified_offset.type());
114 
115  const plus_exprt new_offset(simplified_offset, member_offset);
116 
117  return read_object(member_expr.struct_op(), new_offset, type);
118  }
119  else if(compound_type.id()==ID_union)
120  {
121  // Unions are easy: the offset is always zero,
122  // so simply pass down.
123  return read_object(member_expr.struct_op(), offset, type);
124  }
125  }
126 
127  // check if we have an array with the right subtype
128  if(object_type.id()==ID_array &&
129  base_type_eq(object_type.subtype(), dest_type, ns))
130  {
131  // check proper alignment
132  exprt size=size_of_expr(dest_type, ns);
133 
134  if(size.is_not_nil())
135  {
136  mp_integer size_constant, offset_constant;
137  if(!to_integer(simplify_expr(size, ns), size_constant) &&
138  !to_integer(simplified_offset, offset_constant) &&
139  (offset_constant%size_constant)==0)
140  {
141  // Yes! Can use index expression!
142  mp_integer index_constant=offset_constant/size_constant;
143  exprt index_expr=from_integer(index_constant, size.type());
144  return index_exprt(object, index_expr, dest_type);
145  }
146  }
147  }
148 
149  // give up and use byte_extract
150  return byte_extract_exprt(
151  byte_extract_id(), object, simplified_offset, dest_type);
152 }
153 
155  const exprt &address,
156  const exprt &offset,
157  const typet &type)
158 {
159  if(address.id()==ID_address_of)
160  {
161  const address_of_exprt &address_of_expr=to_address_of_expr(address);
162 
163  const exprt &object=address_of_expr.object();
164 
165  return read_object(object, offset, type);
166  }
167  else if(address.id()==ID_typecast)
168  {
169  const typecast_exprt &typecast_expr=to_typecast_expr(address);
170 
171  return dereference_typecast(typecast_expr, offset, type);
172  }
173  else if(address.id()==ID_plus)
174  {
175  // pointer arithmetic
176  if(address.operands().size()<2)
177  throw "plus with less than two operands";
178 
179  return dereference_plus(address, offset, type);
180  }
181  else if(address.id()==ID_if)
182  {
183  const if_exprt &if_expr=to_if_expr(address);
184 
185  return dereference_if(if_expr, offset, type);
186  }
187  else if(address.id()==ID_constant)
188  {
189  const typet result_type=ns.follow(address.type()).subtype();
190 
191  // pointer-typed constant
192  if(to_constant_expr(address).get_value()==ID_NULL) // NULL
193  {
194  // we turn this into (type *)0
195  exprt zero=from_integer(0, index_type());
196  return dereference_rec(
197  typecast_exprt(zero, address.type()), offset, type);
198  }
199  else
200  throw "dereferencet: unexpected pointer constant "+address.pretty();
201  }
202  else
203  {
204  throw "failed to dereference `"+address.id_string()+"'";
205  }
206 }
207 
209  const if_exprt &expr,
210  const exprt &offset,
211  const typet &type)
212 {
213  // push down the if, do recursive call
214  exprt true_case=dereference_rec(expr.true_case(), offset, type);
215  exprt false_case=dereference_rec(expr.false_case(), offset, type);
216 
217  return if_exprt(expr.cond(), true_case, false_case);
218 }
219 
221  const exprt &expr,
222  const exprt &offset,
223  const typet &type)
224 {
225  exprt pointer=expr.op0();
226  exprt integer=expr.op1();
227 
228  // need not be binary
229  if(expr.operands().size()>2)
230  {
231  assert(expr.op0().type().id()==ID_pointer);
232 
233  exprt::operandst plus_ops(
234  ++expr.operands().begin(), expr.operands().end());
235  integer.operands().swap(plus_ops);
236  }
237 
238  if(ns.follow(integer.type()).id()==ID_pointer)
239  std::swap(pointer, integer);
240 
241  // multiply integer by object size
242  exprt size=size_of_expr(pointer.type().subtype(), ns);
243  if(size.is_nil())
244  throw "dereference failed to get object size for pointer arithmetic";
245 
246  // make types of offset and size match
247  if(size.type()!=integer.type())
248  integer.make_typecast(size.type());
249 
250  const plus_exprt new_offset(offset, mult_exprt(size, integer));
251 
252  return dereference_rec(pointer, new_offset, type);
253 }
254 
256  const typecast_exprt &expr,
257  const exprt &offset,
258  const typet &type)
259 {
260  const exprt &op=expr.op();
261  const typet &op_type=ns.follow(op.type());
262 
263  // pointer type cast?
264  if(op_type.id()==ID_pointer)
265  return dereference_rec(op, offset, type); // just pass down
266  else if(op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv)
267  {
268  // We got an integer-typed address A. We turn this
269  // into integer_dereference(A+offset),
270  // and then let some other layer worry about it.
271 
272  exprt integer=op;
273 
274  if(!offset.is_zero())
275  integer=
276  plus_exprt(offset, typecast_exprt(op, offset.type()));
277 
278  return unary_exprt(ID_integer_dereference, integer, type);
279  }
280  else
281  throw "dereferencet: unexpected cast";
282 }
283 
285  const typet &object_type,
286  const typet &dereference_type) const
287 {
288  if(dereference_type.id()==ID_empty)
289  return true; // always ok
290 
291  if(base_type_eq(object_type, dereference_type, ns))
292  return true; // ok, they just match
293 
294  // check for struct prefixes
295 
296  if(object_type.id()==ID_struct &&
297  dereference_type.id()==ID_struct)
298  {
299  if(to_struct_type(dereference_type).is_prefix_of(
300  to_struct_type(object_type)))
301  return true; // ok, dereference_type is a prefix of object_type
302  }
303 
304  // any code is ok
305  if(dereference_type.id()==ID_code &&
306  object_type.id()==ID_code)
307  return true;
308 
309  // bit vectors of same size are ok
310  if((object_type.id()==ID_signedbv || object_type.id()==ID_unsignedbv) &&
311  (dereference_type.id()==ID_signedbv ||
312  dereference_type.id()==ID_unsignedbv))
313  {
314  return object_type.get(ID_width)==dereference_type.get(ID_width);
315  }
316 
317  // Any pointer to pointer is always ok,
318  // but should likely check that width is the same.
319  if(object_type.id()==ID_pointer &&
320  dereference_type.id()==ID_pointer)
321  return true;
322 
323  // really different
324 
325  return false;
326 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
The type of an expression.
Definition: type.h:22
exprt size_of_expr(const typet &type, const namespacet &ns)
exprt & true_case()
Definition: std_expr.h:3395
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
bool is_nil() const
Definition: irep.h:102
bool is_not_nil() const
Definition: irep.h:103
exprt & object()
Definition: std_expr.h:3180
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
exprt simplify_expr(const exprt &src, const namespacet &ns)
const exprt & op() const
Definition: std_expr.h:340
exprt dereference_rec(const exprt &address, const exprt &offset, const typet &type)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
const namespacet & ns
Definition: dereference.h:52
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
exprt dereference_if(const if_exprt &expr, const exprt &offset, const typet &type)
const irep_idt & get_value() const
Definition: std_expr.h:4441
The trinary if-then-else operator.
Definition: std_expr.h:3361
exprt & cond()
Definition: std_expr.h:3385
typet & type()
Definition: expr.h:56
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:3201
Structure type.
Definition: std_types.h:297
exprt dereference_typecast(const typecast_exprt &expr, const exprt &offset, const typet &type)
Extract member of struct or union.
Definition: std_expr.h:3871
const irep_idt & id() const
Definition: irep.h:189
Expression classes for byte-level operators.
bool type_compatible(const typet &object_type, const typet &dereference_type) const
API to expression classes.
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
Generic base class for unary expressions.
Definition: std_expr.h:303
irep_idt byte_extract_id()
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
The plus expression.
Definition: std_expr.h:893
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
Operator to return the address of an object.
Definition: std_expr.h:3170
exprt & false_case()
Definition: std_expr.h:3405
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4465
std::vector< exprt > operandst
Definition: expr.h:45
binary multiplication
Definition: std_expr.h:1017
Pointer Logic.
bool is_prefix_of(const struct_typet &other) const
Definition: std_types.cpp:76
exprt & index()
Definition: std_expr.h:1496
Base class for all expressions.
Definition: expr.h:42
const exprt & struct_op() const
Definition: std_expr.h:3911
exprt dereference_plus(const exprt &expr, const exprt &offset, const typet &type)
irep_idt get_component_name() const
Definition: std_expr.h:3895
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
const std::string & id_string() const
Definition: irep.h:192
bool is_zero() const
Definition: expr.cpp:161
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
Base Type Computation.
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt operator()(const exprt &pointer)
Definition: dereference.cpp:30
Pointer Dereferencing.
exprt & array()
Definition: std_expr.h:1486
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
exprt read_object(const exprt &object, const exprt &offset, const typet &type)
Definition: dereference.cpp:49
array index operator
Definition: std_expr.h:1462
static format_containert< T > format(const T &o)
Definition: format.h:35