cprover
symex_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 "goto_symex.h"
13 
15 #include <util/arith_tools.h>
16 #include <util/base_type.h>
17 #include <util/byte_operators.h>
18 
21 #include <langapi/language_util.h>
22 
23 #include <util/c_types.h>
24 
26 
28  exprt &expr,
29  statet &state,
30  guardt &guard)
31 {
32  // Could be member, could be if, could be index.
33 
34  if(expr.id()==ID_member)
36  to_member_expr(expr).struct_op(), state, guard);
37  else if(expr.id()==ID_if)
38  {
39  // the condition is not an address
41  to_if_expr(expr).cond(), state, guard, false);
42 
43  // add to guard?
45  to_if_expr(expr).true_case(), state, guard);
47  to_if_expr(expr).false_case(), state, guard);
48  }
49  else if(expr.id()==ID_index)
50  {
51  // the index is not an address
53  to_index_expr(expr).index(), state, guard, false);
54 
55  // the array _is_ an address
57  to_index_expr(expr).array(), state, guard);
58  }
59  else
60  {
61  // give up and dereference
62 
63  dereference_rec(expr, state, guard, false);
64  }
65 }
66 
68 {
69  // Could be member, could be if, could be index.
70 
71  if(expr.id()==ID_member)
72  {
74  to_member_expr(expr).struct_op());
75  }
76  else if(expr.id()==ID_if)
77  {
78  return
79  is_index_member_symbol_if(to_if_expr(expr).true_case()) &&
80  is_index_member_symbol_if(to_if_expr(expr).false_case());
81  }
82  else if(expr.id()==ID_index)
83  {
84  return is_index_member_symbol_if(to_index_expr(expr).array());
85  }
86  else if(expr.id()==ID_symbol)
87  return true;
88  else
89  return false;
90 }
91 
94  const exprt &expr,
95  statet &state,
96  guardt &guard,
97  bool keep_array)
98 {
99  exprt result;
100 
101  if(expr.id()==ID_byte_extract_little_endian ||
102  expr.id()==ID_byte_extract_big_endian)
103  {
104  // address_of(byte_extract(op, offset, t)) is
105  // address_of(op) + offset with adjustments for arrays
106 
108 
109  // recursive call
110  result=address_arithmetic(be.op(), state, guard, keep_array);
111 
112  if(ns.follow(be.op().type()).id()==ID_array &&
113  result.id()==ID_address_of)
114  {
116 
117  // turn &a of type T[i][j] into &(a[0][0])
118  for(const typet *t=&(ns.follow(a.type().subtype()));
119  t->id()==ID_array && !base_type_eq(expr.type(), *t, ns);
120  t=&(ns.follow(*t).subtype()))
122  }
123 
124  // do (expr.type() *)(((char *)op)+offset)
125  result=typecast_exprt(result, pointer_type(char_type()));
126 
127  // there could be further dereferencing in the offset
128  exprt offset=be.offset();
129  dereference_rec(offset, state, guard, false);
130 
131  result=plus_exprt(result, offset);
132 
133  // treat &array as &array[0]
134  const typet &expr_type=ns.follow(expr.type());
135  typet dest_type_subtype;
136 
137  if(expr_type.id()==ID_array && !keep_array)
138  dest_type_subtype=expr_type.subtype();
139  else
140  dest_type_subtype=expr_type;
141 
142  result=typecast_exprt(result, pointer_type(dest_type_subtype));
143  }
144  else if(expr.id()==ID_index ||
145  expr.id()==ID_member)
146  {
148  ode.build(expr, ns);
149 
151  be.type()=expr.type();
152  be.op()=ode.root_object();
153  be.offset()=ode.offset();
154 
155  // recursive call
156  result=address_arithmetic(be, state, guard, keep_array);
157 
158  do_simplify(result);
159  }
160  else if(expr.id()==ID_dereference)
161  {
162  // ANSI-C guarantees &*p == p no matter what p is,
163  // even if it's complete garbage
164  // just grab the pointer, but be wary of further dereferencing
165  // in the pointer itself
166  result=to_dereference_expr(expr).pointer();
167  dereference_rec(result, state, guard, false);
168  }
169  else if(expr.id()==ID_if)
170  {
171  if_exprt if_expr=to_if_expr(expr);
172 
173  // the condition is not an address
174  dereference_rec(if_expr.cond(), state, guard, false);
175 
176  // recursive call
177  if_expr.true_case()=
178  address_arithmetic(if_expr.true_case(), state, guard, keep_array);
179  if_expr.false_case()=
180  address_arithmetic(if_expr.false_case(), state, guard, keep_array);
181 
182  result=if_expr;
183  }
184  else if(expr.id()==ID_symbol ||
185  expr.id()==ID_string_constant ||
186  expr.id()==ID_label ||
187  expr.id()==ID_array)
188  {
189  // give up, just dereference
190  result=expr;
191  dereference_rec(result, state, guard, false);
192 
193  // turn &array into &array[0]
194  if(ns.follow(result.type()).id()==ID_array && !keep_array)
195  result=index_exprt(result, from_integer(0, index_type()));
196 
197  // handle field-sensitive SSA symbol
198  mp_integer offset=0;
199  if(expr.id()==ID_symbol &&
200  expr.get_bool(ID_C_SSA_symbol))
201  {
202  offset=compute_pointer_offset(expr, ns);
203  assert(offset>=0);
204  }
205 
206  if(offset>0)
207  {
209  be.type()=expr.type();
210  be.op()=to_ssa_expr(expr).get_l1_object();
211  be.offset()=from_integer(offset, index_type());
212 
213  result=address_arithmetic(be, state, guard, keep_array);
214 
215  do_simplify(result);
216  }
217  else
218  result=address_of_exprt(result);
219  }
220  else
221  throw "goto_symext::address_arithmetic does not handle "+expr.id_string();
222 
223  const typet &expr_type=ns.follow(expr.type());
224  assert((expr_type.id()==ID_array && !keep_array) ||
225  base_type_eq(pointer_type(expr_type), result.type(), ns));
226 
227  return result;
228 }
229 
231  exprt &expr,
232  statet &state,
233  guardt &guard,
234  const bool write)
235 {
236  if(expr.id()==ID_dereference)
237  {
238  if(expr.operands().size()!=1)
239  throw "dereference takes one operand";
240 
241  exprt tmp1;
242  tmp1.swap(expr.op0());
243 
244  // first make sure there are no dereferences in there
245  dereference_rec(tmp1, state, guard, false);
246 
247  // we need to set up some elaborate call-backs
248  symex_dereference_statet symex_dereference_state(*this, state);
249 
251  ns,
253  options,
254  symex_dereference_state,
255  language_mode);
256 
257  // std::cout << "**** " << from_expr(ns, "", tmp1) << '\n';
258  exprt tmp2=
259  dereference.dereference(
260  tmp1,
261  guard,
262  write?
265  // std::cout << "**** " << from_expr(ns, "", tmp2) << '\n';
266 
267  expr.swap(tmp2);
268 
269  // this may yield a new auto-object
270  trigger_auto_object(expr, state);
271  }
272  else if(expr.id()==ID_index &&
273  to_index_expr(expr).array().id()==ID_member &&
274  to_array_type(ns.follow(to_index_expr(expr).array().type())).
275  size().is_zero())
276  {
277  // This is an expression of the form x.a[i],
278  // where a is a zero-sized array. This gets
279  // re-written into *(&x.a+i)
280 
281  index_exprt index_expr=to_index_expr(expr);
282 
283  address_of_exprt address_of_expr(index_expr.array());
284  address_of_expr.type()=pointer_type(expr.type());
285 
286  dereference_exprt tmp;
287  tmp.pointer()=plus_exprt(address_of_expr, index_expr.index());
288  tmp.type()=expr.type();
290 
291  // recursive call
292  dereference_rec(tmp, state, guard, write);
293 
294  expr.swap(tmp);
295  }
296  else if(expr.id()==ID_index &&
297  to_index_expr(expr).array().type().id()==ID_pointer)
298  {
299  // old stuff, will go away
300  assert(false);
301  }
302  else if(expr.id()==ID_address_of)
303  {
304  address_of_exprt &address_of_expr=to_address_of_expr(expr);
305 
306  exprt &object=address_of_expr.object();
307 
308  const typet &expr_type=ns.follow(expr.type());
309  expr=address_arithmetic(object, state, guard,
310  expr_type.subtype().id()==ID_array);
311  }
312  else if(expr.id()==ID_typecast)
313  {
314  exprt &tc_op=to_typecast_expr(expr).op();
315 
316  // turn &array into &array[0] when casting to pointer-to-element-type
317  if(tc_op.id()==ID_address_of &&
318  to_address_of_expr(tc_op).object().type().id()==ID_array &&
319  base_type_eq(
320  expr.type(),
321  pointer_type(to_address_of_expr(tc_op).object().type().subtype()),
322  ns))
323  {
324  expr=
326  index_exprt(
327  to_address_of_expr(tc_op).object(),
328  from_integer(0, index_type())));
329 
330  dereference_rec(expr, state, guard, write);
331  }
332  else
333  {
334  dereference_rec(tc_op, state, guard, write);
335  }
336  }
337  else
338  {
339  Forall_operands(it, expr)
340  dereference_rec(*it, state, guard, write);
341  }
342 }
343 
345  exprt &expr,
346  statet &state,
347  const bool write)
348 {
349  // The expression needs to be renamed to level 1
350  // in order to distinguish addresses of local variables
351  // from different frames. Would be enough to rename
352  // symbols whose address is taken.
353  assert(!state.call_stack().empty());
354  state.rename(expr, ns, goto_symex_statet::L1);
355 
356  // start the recursion!
357  guardt guard;
358  dereference_rec(expr, state, guard, write);
359  // dereferencing may introduce new symbol_exprt
360  // (like __CPROVER_memory)
361  state.rename(expr, ns, goto_symex_statet::L1);
362 }
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:19
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
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
const ssa_exprt get_l1_object() const
Definition: ssa_expr.h:53
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
void dereference_rec(exprt &expr, statet &state, guardt &guard, const bool write)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
virtual void dereference(exprt &expr, statet &state, const bool write)
virtual exprt dereference(const exprt &pointer, const guardt &guard, const modet mode)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
static bool is_index_member_symbol_if(const exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
const exprt & root_object() const
Definition: std_expr.h:1600
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
optionst options
Definition: goto_symex.h:96
Definition: guard.h:19
typet & type()
Definition: expr.h:60
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
Pointer Dereferencing.
exprt & op()
Definition: std_expr.h:1739
Pointer Dereferencing.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:2748
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 array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
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.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:150
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:123
Operator to dereference a pointer.
Definition: std_expr.h:2701
Symbolic Execution.
void trigger_auto_object(const exprt &expr, statet &state)
irep_idt byte_extract_id()
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1578
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
void dereference_rec_address_of(exprt &expr, statet &state, guardt &guard)
Pointer Logic.
mp_integer compute_pointer_offset(const exprt &expr, const namespacet &ns)
symbol_tablet & new_symbol_table
Definition: goto_symex.h:97
exprt & index()
Definition: std_expr.h:1208
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
Definition: goto_symex.h:101
Base class for all expressions.
Definition: expr.h:46
exprt & pointer()
Definition: std_expr.h:2727
const exprt & struct_op() const
Definition: std_expr.h:3270
call_stackt & call_stack()
source_locationt & add_source_location()
Definition: type.h:100
const source_locationt & source_location() const
Definition: expr.h:142
const std::string & id_string() const
Definition: irep.h:192
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
exprt address_arithmetic(const exprt &expr, statet &state, guardt &guard, bool keep_array)
Evaluate an ID_address_of expression.
operandst & operands()
Definition: expr.h:70
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const namespacet & ns
Definition: goto_symex.h:104
exprt & array()
Definition: std_expr.h:1198
bitvector_typet char_type()
Definition: c_types.cpp:113
Symbolic Execution of ANSI-C.
array index operator
Definition: std_expr.h:1170