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 <langapi/language_util.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: " << from_expr(ns, "", 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  exprt new_offset=plus_exprt(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  exprt new_offset=plus_exprt(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 binary_exprt(object, byte_extract_id(), simplified_offset, dest_type);
151 }
152 
154  const exprt &address,
155  const exprt &offset,
156  const typet &type)
157 {
158  if(address.id()==ID_address_of)
159  {
160  const address_of_exprt &address_of_expr=to_address_of_expr(address);
161 
162  const exprt &object=address_of_expr.object();
163 
164  return read_object(object, offset, type);
165  }
166  else if(address.id()==ID_typecast)
167  {
168  const typecast_exprt &typecast_expr=to_typecast_expr(address);
169 
170  return dereference_typecast(typecast_expr, offset, type);
171  }
172  else if(address.id()==ID_plus)
173  {
174  // pointer arithmetic
175  if(address.operands().size()<2)
176  throw "plus with less than two operands";
177 
178  return dereference_plus(address, offset, type);
179  }
180  else if(address.id()==ID_if)
181  {
182  const if_exprt &if_expr=to_if_expr(address);
183 
184  return dereference_if(if_expr, offset, type);
185  }
186  else if(address.id()==ID_constant)
187  {
188  const typet result_type=ns.follow(address.type()).subtype();
189 
190  // pointer-typed constant
191  if(to_constant_expr(address).get_value()==ID_NULL) // NULL
192  {
193  // we turn this into (type *)0
194  exprt zero=from_integer(0, index_type());
195  return dereference_rec(
196  typecast_exprt(zero, address.type()), offset, type);
197  }
198  else
199  throw "dereferencet: unexpected pointer constant "+address.pretty();
200  }
201  else
202  {
203  throw "failed to dereference `"+address.id_string()+"'";
204  }
205 }
206 
208  const if_exprt &expr,
209  const exprt &offset,
210  const typet &type)
211 {
212  // push down the if, do recursive call
213  exprt true_case=dereference_rec(expr.true_case(), offset, type);
214  exprt false_case=dereference_rec(expr.false_case(), offset, type);
215 
216  return if_exprt(expr.cond(), true_case, false_case);
217 }
218 
220  const exprt &expr,
221  const exprt &offset,
222  const typet &type)
223 {
224  exprt pointer=expr.op0();
225  exprt integer=expr.op1();
226 
227  // need not be binary
228  if(expr.operands().size()>2)
229  {
230  assert(expr.op0().type().id()==ID_pointer);
231 
232  exprt::operandst plus_ops(
233  ++expr.operands().begin(), expr.operands().end());
234  integer.operands().swap(plus_ops);
235  }
236 
237  if(ns.follow(integer.type()).id()==ID_pointer)
238  std::swap(pointer, integer);
239 
240  // multiply integer by object size
241  exprt size=size_of_expr(pointer.type().subtype(), ns);
242  if(size.is_nil())
243  throw "dereference failed to get object size for pointer arithmetic";
244 
245  // make types of offset and size match
246  if(size.type()!=integer.type())
247  integer.make_typecast(size.type());
248 
249  exprt new_offset=plus_exprt(offset, mult_exprt(size, integer));
250 
251  return dereference_rec(pointer, new_offset, type);
252 }
253 
255  const typecast_exprt &expr,
256  const exprt &offset,
257  const typet &type)
258 {
259  const exprt &op=expr.op();
260  const typet &op_type=ns.follow(op.type());
261 
262  // pointer type cast?
263  if(op_type.id()==ID_pointer)
264  return dereference_rec(op, offset, type); // just pass down
265  else if(op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv)
266  {
267  // We got an integer-typed address A. We turn this back (!)
268  // into *(type *)(A+offset), and then let some other layer
269  // worry about it.
270 
271  exprt integer=op;
272 
273  if(!offset.is_zero())
274  integer=
275  plus_exprt(offset, typecast_exprt(op, offset.type()));
276 
277  exprt new_typecast=
278  typecast_exprt(integer, pointer_type(type));
279 
280  return dereference_exprt(new_typecast, type);
281  }
282  else
283  throw "dereferencet: unexpected cast";
284 }
285 
287  const typet &object_type,
288  const typet &dereference_type) const
289 {
290  if(dereference_type.id()==ID_empty)
291  return true; // always ok
292 
293  if(base_type_eq(object_type, dereference_type, ns))
294  return true; // ok, they just match
295 
296  // check for struct prefixes
297 
298  if(object_type.id()==ID_struct &&
299  dereference_type.id()==ID_struct)
300  {
301  if(to_struct_type(dereference_type).is_prefix_of(
302  to_struct_type(object_type)))
303  return true; // ok, dereference_type is a prefix of object_type
304  }
305 
306  // any code is ok
307  if(dereference_type.id()==ID_code &&
308  object_type.id()==ID_code)
309  return true;
310 
311  // bit vectors of same size are ok
312  if((object_type.id()==ID_signedbv || object_type.id()==ID_unsignedbv) &&
313  (dereference_type.id()==ID_signedbv ||
314  dereference_type.id()==ID_unsignedbv))
315  {
316  return object_type.get(ID_width)==dereference_type.get(ID_width);
317  }
318 
319  // Any pointer to pointer is always ok,
320  // but should likely check that width is the same.
321  if(object_type.id()==ID_pointer &&
322  dereference_type.id()==ID_pointer)
323  return true;
324 
325  // really different
326 
327  return false;
328 }
The type of an expression.
Definition: type.h:20
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
exprt size_of_expr(const typet &type, const namespacet &ns)
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
exprt & true_case()
Definition: std_expr.h:2805
semantic type conversion
Definition: std_expr.h:1725
BigInt mp_integer
Definition: mp_arith.h:19
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
exprt & object()
Definition: std_expr.h:2608
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
exprt simplify_expr(const exprt &src, const namespacet &ns)
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:270
const namespacet & ns
Definition: dereference.h:52
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
exprt dereference_if(const if_exprt &expr, const exprt &offset, const typet &type)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
const irep_idt & get_value() const
Definition: std_expr.h:3702
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
typet & type()
Definition: expr.h:60
Structure type.
Definition: std_types.h:296
exprt & op()
Definition: std_expr.h:1739
exprt dereference_typecast(const typecast_exprt &expr, const exprt &offset, const typet &type)
Extract member of struct or union.
Definition: std_expr.h:3214
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
const irep_idt & id() const
Definition: irep.h:189
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:2629
Expression classes for byte-level operators.
bool type_compatible(const typet &object_type, const typet &dereference_type) const
A generic base class for binary expressions.
Definition: std_expr.h:471
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
Operator to dereference a pointer.
Definition: std_expr.h:2701
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
irep_idt byte_extract_id()
The plus expression.
Definition: std_expr.h:702
bitvector_typet index_type()
Definition: c_types.cpp:15
Operator to return the address of an object.
Definition: std_expr.h:2593
exprt & false_case()
Definition: std_expr.h:2815
std::vector< exprt > operandst
Definition: expr.h:49
binary multiplication
Definition: std_expr.h:806
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
Pointer Logic.
bool is_prefix_of(const struct_typet &other) const
Definition: std_types.cpp:76
exprt & index()
Definition: std_expr.h:1208
Base class for all expressions.
Definition: expr.h:46
const exprt & struct_op() const
Definition: std_expr.h:3270
exprt dereference_plus(const exprt &expr, const exprt &offset, const typet &type)
irep_idt get_component_name() const
Definition: std_expr.h:3249
const std::string & id_string() const
Definition: irep.h:192
bool is_zero() const
Definition: expr.cpp:236
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
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:1198
void make_typecast(const typet &_type)
Definition: expr.cpp:90
exprt read_object(const exprt &object, const exprt &offset, const typet &type)
Definition: dereference.cpp:49
array index operator
Definition: std_expr.h:1170