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 
14 #include <util/arith_tools.h>
15 #include <util/base_type.h>
16 #include <util/byte_operators.h>
17 #include <util/c_types.h>
18 #include <util/invariant.h>
20 
22 
24 
26  exprt &expr,
27  statet &state,
28  guardt &guard)
29 {
30  // Could be member, could be if, could be index.
31 
32  if(expr.id()==ID_member)
34  to_member_expr(expr).struct_op(), state, guard);
35  else if(expr.id()==ID_if)
36  {
37  // the condition is not an address
39  to_if_expr(expr).cond(), state, guard, false);
40 
41  // add to guard?
43  to_if_expr(expr).true_case(), state, guard);
45  to_if_expr(expr).false_case(), state, guard);
46  }
47  else if(expr.id()==ID_index)
48  {
49  // the index is not an address
51  to_index_expr(expr).index(), state, guard, false);
52 
53  // the array _is_ an address
55  to_index_expr(expr).array(), state, guard);
56  }
57  else
58  {
59  // give up and dereference
60 
61  dereference_rec(expr, state, guard, false);
62  }
63 }
64 
66 {
67  // Could be member, could be if, could be index.
68 
69  if(expr.id()==ID_member)
70  {
72  to_member_expr(expr).struct_op());
73  }
74  else if(expr.id()==ID_if)
75  {
76  return
77  is_index_member_symbol_if(to_if_expr(expr).true_case()) &&
78  is_index_member_symbol_if(to_if_expr(expr).false_case());
79  }
80  else if(expr.id()==ID_index)
81  {
82  return is_index_member_symbol_if(to_index_expr(expr).array());
83  }
84  else if(expr.id()==ID_symbol)
85  return true;
86  else
87  return false;
88 }
89 
92  const exprt &expr,
93  statet &state,
94  guardt &guard,
95  bool keep_array)
96 {
97  exprt result;
98 
99  if(expr.id()==ID_byte_extract_little_endian ||
100  expr.id()==ID_byte_extract_big_endian)
101  {
102  // address_of(byte_extract(op, offset, t)) is
103  // address_of(op) + offset with adjustments for arrays
104 
106 
107  // recursive call
108  result=address_arithmetic(be.op(), state, guard, keep_array);
109 
110  if(ns.follow(be.op().type()).id()==ID_array &&
111  result.id()==ID_address_of)
112  {
114 
115  // turn &a of type T[i][j] into &(a[0][0])
116  for(const typet *t=&(ns.follow(a.type().subtype()));
117  t->id()==ID_array && !base_type_eq(expr.type(), *t, ns);
118  t=&(ns.follow(*t).subtype()))
120  }
121 
122  // do (expr.type() *)(((char *)op)+offset)
123  result=typecast_exprt(result, pointer_type(char_type()));
124 
125  // there could be further dereferencing in the offset
126  exprt offset=be.offset();
127  dereference_rec(offset, state, guard, false);
128 
129  result=plus_exprt(result, offset);
130 
131  // treat &array as &array[0]
132  const typet &expr_type=ns.follow(expr.type());
133  typet dest_type_subtype;
134 
135  if(expr_type.id()==ID_array && !keep_array)
136  dest_type_subtype=expr_type.subtype();
137  else
138  dest_type_subtype=expr_type;
139 
140  result=typecast_exprt(result, pointer_type(dest_type_subtype));
141  }
142  else if(expr.id()==ID_index ||
143  expr.id()==ID_member)
144  {
146  ode.build(expr, ns);
147 
148  const byte_extract_exprt be(
149  byte_extract_id(), ode.root_object(), ode.offset(), expr.type());
150 
151  // recursive call
152  result=address_arithmetic(be, state, guard, keep_array);
153 
154  do_simplify(result);
155  }
156  else if(expr.id()==ID_dereference)
157  {
158  // ANSI-C guarantees &*p == p no matter what p is,
159  // even if it's complete garbage
160  // just grab the pointer, but be wary of further dereferencing
161  // in the pointer itself
162  result=to_dereference_expr(expr).pointer();
163  dereference_rec(result, state, guard, false);
164  }
165  else if(expr.id()==ID_if)
166  {
167  if_exprt if_expr=to_if_expr(expr);
168 
169  // the condition is not an address
170  dereference_rec(if_expr.cond(), state, guard, false);
171 
172  // recursive call
173  if_expr.true_case()=
174  address_arithmetic(if_expr.true_case(), state, guard, keep_array);
175  if_expr.false_case()=
176  address_arithmetic(if_expr.false_case(), state, guard, keep_array);
177 
178  result=if_expr;
179  }
180  else if(expr.id()==ID_symbol ||
181  expr.id()==ID_string_constant ||
182  expr.id()==ID_label ||
183  expr.id()==ID_array)
184  {
185  // give up, just dereference
186  result=expr;
187  dereference_rec(result, state, guard, false);
188 
189  // turn &array into &array[0]
190  if(ns.follow(result.type()).id()==ID_array && !keep_array)
191  result=index_exprt(result, from_integer(0, index_type()));
192 
193  // handle field-sensitive SSA symbol
194  mp_integer offset=0;
195  if(expr.id()==ID_symbol &&
196  expr.get_bool(ID_C_SSA_symbol))
197  {
198  offset=compute_pointer_offset(expr, ns);
199  PRECONDITION(offset >= 0);
200  }
201 
202  if(offset>0)
203  {
204  const byte_extract_exprt be(
205  byte_extract_id(),
206  to_ssa_expr(expr).get_l1_object(),
207  from_integer(offset, index_type()),
208  expr.type());
209 
210  result=address_arithmetic(be, state, guard, keep_array);
211 
212  do_simplify(result);
213  }
214  else
215  result=address_of_exprt(result);
216  }
217  else
218  throw "goto_symext::address_arithmetic does not handle "+expr.id_string();
219 
220  const typet &expr_type=ns.follow(expr.type());
221  INVARIANT((expr_type.id()==ID_array && !keep_array) ||
222  base_type_eq(pointer_type(expr_type), result.type(), ns),
223  "either non-persistent array or pointer to result");
224 
225  return result;
226 }
227 
229  exprt &expr,
230  statet &state,
231  guardt &guard,
232  const bool write)
233 {
234  if(expr.id()==ID_dereference)
235  {
236  if(expr.operands().size()!=1)
237  throw "dereference takes one operand";
238 
239  bool expr_is_not_null = false;
240 
241  if(state.threads.size() == 1)
242  {
243  const irep_idt &expr_function = state.source.pc->function;
244  if(!expr_function.empty())
245  {
246  dereference_exprt to_check = to_dereference_expr(expr);
247  state.get_original_name(to_check);
248 
249  expr_is_not_null =
250  safe_pointers.at(expr_function).is_safe_dereference(
251  to_check, state.source.pc);
252  }
253  }
254 
255  exprt tmp1;
256  tmp1.swap(expr.op0());
257 
258  // first make sure there are no dereferences in there
259  dereference_rec(tmp1, state, guard, false);
260 
261  // we need to set up some elaborate call-backs
262  symex_dereference_statet symex_dereference_state(*this, state);
263 
265  ns,
266  state.symbol_table,
267  options,
268  symex_dereference_state,
270  expr_is_not_null);
271 
272  // std::cout << "**** " << format(tmp1) << '\n';
273  exprt tmp2=
274  dereference.dereference(
275  tmp1,
276  guard,
277  write?
280  // std::cout << "**** " << format(tmp2) << '\n';
281 
282  expr.swap(tmp2);
283 
284  // this may yield a new auto-object
285  trigger_auto_object(expr, state);
286  }
287  else if(expr.id()==ID_index &&
288  to_index_expr(expr).array().id()==ID_member &&
289  to_array_type(ns.follow(to_index_expr(expr).array().type())).
290  size().is_zero())
291  {
292  // This is an expression of the form x.a[i],
293  // where a is a zero-sized array. This gets
294  // re-written into *(&x.a+i)
295 
296  index_exprt index_expr=to_index_expr(expr);
297 
298  address_of_exprt address_of_expr(index_expr.array());
299  address_of_expr.type()=pointer_type(expr.type());
300 
301  dereference_exprt tmp;
302  tmp.pointer()=plus_exprt(address_of_expr, index_expr.index());
303  tmp.type()=expr.type();
305 
306  // recursive call
307  dereference_rec(tmp, state, guard, write);
308 
309  expr.swap(tmp);
310  }
311  else if(expr.id()==ID_index &&
312  to_index_expr(expr).array().type().id()==ID_pointer)
313  {
314  // old stuff, will go away
315  UNREACHABLE;
316  }
317  else if(expr.id()==ID_address_of)
318  {
319  address_of_exprt &address_of_expr=to_address_of_expr(expr);
320 
321  exprt &object=address_of_expr.object();
322 
323  const typet &expr_type=ns.follow(expr.type());
324  expr=address_arithmetic(object, state, guard,
325  expr_type.subtype().id()==ID_array);
326  }
327  else if(expr.id()==ID_typecast)
328  {
329  exprt &tc_op=to_typecast_expr(expr).op();
330 
331  // turn &array into &array[0] when casting to pointer-to-element-type
332  if(tc_op.id()==ID_address_of &&
333  to_address_of_expr(tc_op).object().type().id()==ID_array &&
334  base_type_eq(
335  expr.type(),
336  pointer_type(to_address_of_expr(tc_op).object().type().subtype()),
337  ns))
338  {
339  expr=
341  index_exprt(
342  to_address_of_expr(tc_op).object(),
343  from_integer(0, index_type())));
344 
345  dereference_rec(expr, state, guard, write);
346  }
347  else
348  {
349  dereference_rec(tc_op, state, guard, write);
350  }
351  }
352  else
353  {
354  Forall_operands(it, expr)
355  dereference_rec(*it, state, guard, write);
356  }
357 }
358 
360  exprt &expr,
361  statet &state,
362  const bool write)
363 {
364  // The expression needs to be renamed to level 1
365  // in order to distinguish addresses of local variables
366  // from different frames. Would be enough to rename
367  // symbols whose address is taken.
368  PRECONDITION(!state.call_stack().empty());
369  state.rename(expr, ns, goto_symex_statet::L1);
370 
371  // start the recursion!
372  guardt guard;
373  dereference_rec(expr, state, guard, write);
374  // dereferencing may introduce new symbol_exprt
375  // (like __CPROVER_memory)
376  state.rename(expr, ns, goto_symex_statet::L1);
377 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
The type of an expression.
Definition: type.h:22
exprt & true_case()
Definition: std_expr.h:3393
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
goto_programt::const_targett pc
Definition: symex_target.h:32
exprt & object()
Definition: std_expr.h:3178
exprt & op0()
Definition: expr.h:72
const exprt & op() const
Definition: std_expr.h:340
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
static bool is_index_member_symbol_if(const exprt &expr)
const exprt & root_object() const
Definition: std_expr.h:1966
The trinary if-then-else operator.
Definition: std_expr.h:3359
exprt & cond()
Definition: std_expr.h:3383
Definition: guard.h:19
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:3199
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:19
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
Pointer Dereferencing.
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3326
void get_original_name(exprt &expr) const
virtual void dereference(exprt &, statet &, const bool write)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:239
const irep_idt & id() const
Definition: irep.h:259
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:154
Expression classes for byte-level operators.
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Definition: goto_symex.h:472
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:121
Operator to dereference a pointer.
Definition: std_expr.h:3282
Symbolic Execution.
exprt address_arithmetic(const exprt &, statet &, guardt &, bool keep_array)
Evaluate an ID_address_of expression.
irep_idt byte_extract_id()
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1945
The plus expression.
Definition: std_expr.h:893
void dereference_rec(exprt &, statet &, guardt &, const bool write)
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Operator to return the address of an object.
Definition: std_expr.h:3168
exprt & false_case()
Definition: std_expr.h:3403
Pointer Logic.
mp_integer compute_pointer_offset(const exprt &expr, const namespacet &ns)
const optionst & options
Definition: goto_symex.h:204
exprt & index()
Definition: std_expr.h:1496
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:222
void dereference_rec_address_of(exprt &, statet &, guardt &)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
exprt & pointer()
Definition: std_expr.h:3305
const exprt & struct_op() const
Definition: std_expr.h:3909
void trigger_auto_object(const exprt &, statet &)
call_stackt & call_stack()
source_locationt & add_source_location()
Definition: type.h:102
const source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:271
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
const std::string & id_string() const
Definition: irep.h:262
void swap(irept &irep)
Definition: irep.h:303
#define Forall_operands(it, expr)
Definition: expr.h:23
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)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bool empty() const
Definition: dstring.h:73
exprt & array()
Definition: std_expr.h:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
bitvector_typet char_type()
Definition: c_types.cpp:114
Symbolic Execution of ANSI-C.
array index operator
Definition: std_expr.h:1462
symex_targett::sourcet source