cprover
symex_assign.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_symex.h"
13 
14 #include <util/byte_operators.h>
15 #include <util/cprover_prefix.h>
16 
17 #include <util/c_types.h>
18 
19 #include "goto_symex_state.h"
20 
21 // #define USE_UPDATE
22 
24  statet &state,
25  const code_assignt &code)
26 {
27  code_assignt deref_code=code;
28 
29  clean_expr(deref_code.lhs(), state, true);
30  clean_expr(deref_code.rhs(), state, false);
31 
32  symex_assign(state, deref_code);
33 }
34 
36  statet &state,
37  const code_assignt &code)
38 {
39  exprt lhs=code.lhs();
40  exprt rhs=code.rhs();
41 
42  replace_nondet(lhs);
43  replace_nondet(rhs);
44 
45  if(rhs.id()==ID_side_effect)
46  {
47  const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
48  const irep_idt &statement=side_effect_expr.get_statement();
49 
50  if(statement==ID_function_call)
51  {
52  assert(!side_effect_expr.operands().empty());
53 
54  if(side_effect_expr.op0().id()!=ID_symbol)
55  throw "symex_assign: expected symbol as function";
56 
57  const irep_idt &identifier=
58  to_symbol_expr(side_effect_expr.op0()).get_identifier();
59 
60  throw "symex_assign: unexpected function call: "+id2string(identifier);
61  }
62  else if(statement==ID_cpp_new ||
63  statement==ID_cpp_new_array)
64  symex_cpp_new(state, lhs, side_effect_expr);
65  else if(statement==ID_malloc)
66  symex_malloc(state, lhs, side_effect_expr);
67  else if(statement==ID_printf)
68  symex_printf(state, lhs, side_effect_expr);
69  else if(statement==ID_gcc_builtin_va_arg_next)
70  symex_gcc_builtin_va_arg_next(state, lhs, side_effect_expr);
71  else
72  throw "symex_assign: unexpected side effect: "+id2string(statement);
73  }
74  else
75  {
77 
78  // Let's hide return value assignments.
79  if(lhs.id()==ID_symbol &&
80  id2string(to_symbol_expr(lhs).get_identifier()).find(
81  "#return_value!")!=std::string::npos)
83 
84  // We hide if we are in a hidden function.
85  if(state.top().hidden_function)
87 
88  // We hide if we are executing a hidden instruction.
89  if(state.source.pc->source_location.get_hide())
91 
92  guardt guard; // NOT the state guard!
93  symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);
94  }
95 }
96 
98  const exprt &lhs,
99  const exprt &what)
100 {
101  assert(lhs.id()!=ID_symbol);
102  exprt tmp_what=what;
103 
104  if(tmp_what.id()!=ID_symbol)
105  {
106  assert(tmp_what.operands().size()>=1);
107  tmp_what.op0().make_nil();
108  }
109 
110  exprt new_lhs=lhs;
111 
112  exprt *p=&new_lhs;
113 
114  while(p->is_not_nil())
115  {
116  assert(p->id()!=ID_symbol);
117  assert(p->operands().size()>=1);
118  p=&p->op0();
119  }
120 
121  assert(p->is_nil());
122 
123  *p=tmp_what;
124  return new_lhs;
125 }
126 
128  statet &state,
129  const exprt &lhs,
130  const exprt &full_lhs,
131  const exprt &rhs,
132  guardt &guard,
133  assignment_typet assignment_type)
134 {
135  if(lhs.id()==ID_symbol &&
136  lhs.get_bool(ID_C_SSA_symbol))
138  state, to_ssa_expr(lhs), full_lhs, rhs, guard, assignment_type);
139  else if(lhs.id()==ID_index)
141  state, to_index_expr(lhs), full_lhs, rhs, guard, assignment_type);
142  else if(lhs.id()==ID_member)
143  {
144  const typet &type=ns.follow(to_member_expr(lhs).struct_op().type());
145  if(type.id()==ID_struct)
147  state, to_member_expr(lhs), full_lhs, rhs, guard, assignment_type);
148  else if(type.id()==ID_union)
149  {
150  // should have been replaced by byte_extract
151  throw "symex_assign_rec: unexpected assignment to union member";
152  }
153  else
154  throw
155  "symex_assign_rec: unexpected assignment to member of `"+
156  type.id_string()+"'";
157  }
158  else if(lhs.id()==ID_if)
160  state, to_if_expr(lhs), full_lhs, rhs, guard, assignment_type);
161  else if(lhs.id()==ID_typecast)
163  state, to_typecast_expr(lhs), full_lhs, rhs, guard, assignment_type);
164  else if(lhs.id()==ID_string_constant ||
165  lhs.id()=="NULL-object" ||
166  lhs.id()=="zero_string" ||
167  lhs.id()=="is_zero_string" ||
168  lhs.id()=="zero_string_length")
169  {
170  // ignore
171  }
172  else if(lhs.id()==ID_byte_extract_little_endian ||
173  lhs.id()==ID_byte_extract_big_endian)
174  {
176  state, to_byte_extract_expr(lhs), full_lhs, rhs, guard, assignment_type);
177  }
178  else if(lhs.id()==ID_complex_real ||
179  lhs.id()==ID_complex_imag)
180  {
181  // this is stuff like __real__ x = 1;
182  assert(lhs.operands().size()==1);
183 
184  exprt new_rhs=exprt(ID_complex, lhs.op0().type());
185  new_rhs.operands().resize(2);
186 
187  if(lhs.id()==ID_complex_real)
188  {
189  new_rhs.op0()=rhs;
190  new_rhs.op1()=unary_exprt(ID_complex_imag, lhs.op0(), lhs.type());
191  }
192  else
193  {
194  new_rhs.op0()=unary_exprt(ID_complex_real, lhs.op0(), lhs.type());
195  new_rhs.op1()=rhs;
196  }
197 
199  state, lhs.op0(), full_lhs, new_rhs, guard, assignment_type);
200  }
201  else
202  throw "assignment to `"+lhs.id_string()+"' not handled";
203 }
204 
206  statet &state,
207  const ssa_exprt &lhs, // L1
208  const exprt &full_lhs,
209  const exprt &rhs,
210  guardt &guard,
211  assignment_typet assignment_type)
212 {
213  // do not assign to L1 objects that have gone out of scope --
214  // pointer dereferencing may yield such objects; parameters do not
215  // have an L2 entry set up beforehand either, so exempt them from
216  // this check (all other L1 objects should have seen a declaration)
217  const symbolt *s;
218  if(!ns.lookup(lhs.get_object_name(), s) &&
219  !s->is_parameter &&
220  !lhs.get_level_1().empty() &&
221  state.level2.current_count(lhs.get_identifier())==0)
222  return;
223 
224  exprt ssa_rhs=rhs;
225 
226  // put assignment guard into the rhs
227  if(!guard.is_true())
228  {
229  if_exprt tmp_ssa_rhs;
230  tmp_ssa_rhs.type()=ssa_rhs.type();
231  tmp_ssa_rhs.cond()=guard.as_expr();
232  tmp_ssa_rhs.true_case()=ssa_rhs;
233  tmp_ssa_rhs.false_case()=lhs;
234  tmp_ssa_rhs.swap(ssa_rhs);
235  }
236 
237  state.rename(ssa_rhs, ns);
238  do_simplify(ssa_rhs);
239 
240  ssa_exprt ssa_lhs=lhs;
241  state.assignment(
242  ssa_lhs,
243  ssa_rhs,
244  ns,
245  options.get_bool_option("simplify"),
247 
248  exprt ssa_full_lhs=full_lhs;
249  ssa_full_lhs=add_to_lhs(ssa_full_lhs, ssa_lhs);
250  const bool record_events=state.record_events;
251  state.record_events=false;
252  state.rename(ssa_full_lhs, ns);
253  state.record_events=record_events;
254 
255  guardt tmp_guard(state.guard);
256  tmp_guard.append(guard);
257 
258  // do the assignment
259  const symbolt &symbol=ns.lookup(ssa_lhs.get_original_expr());
260  if(symbol.is_auxiliary)
262 
264  tmp_guard.as_expr(),
265  ssa_lhs,
266  ssa_full_lhs, add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
267  ssa_rhs,
268  state.source,
269  assignment_type);
270 }
271 
273  statet &state,
274  const typecast_exprt &lhs,
275  const exprt &full_lhs,
276  const exprt &rhs,
277  guardt &guard,
278  assignment_typet assignment_type)
279 {
280  // these may come from dereferencing on the lhs
281 
282  assert(lhs.operands().size()==1);
283 
284  exprt rhs_typecasted=rhs;
285  rhs_typecasted.make_typecast(lhs.op0().type());
286 
287  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
288 
290  state, lhs.op0(), new_full_lhs, rhs_typecasted, guard, assignment_type);
291 }
292 
294  statet &state,
295  const index_exprt &lhs,
296  const exprt &full_lhs,
297  const exprt &rhs,
298  guardt &guard,
299  assignment_typet assignment_type)
300 {
301  // lhs must be index operand
302  // that takes two operands: the first must be an array
303  // the second is the index
304 
305  if(lhs.operands().size()!=2)
306  throw "index must have two operands";
307 
308  const exprt &lhs_array=lhs.array();
309  const exprt &lhs_index=lhs.index();
310  const typet &lhs_type=ns.follow(lhs_array.type());
311 
312  if(lhs_type.id()!=ID_array)
313  throw "index must take array type operand, but got `"+
314  lhs_type.id_string()+"'";
315 
316  #ifdef USE_UPDATE
317 
318  // turn
319  // a[i]=e
320  // into
321  // a'==UPDATE(a, [i], e)
322 
323  update_exprt new_rhs(lhs_type);
324  new_rhs.old()=lhs_array;
325  new_rhs.designator().push_back(index_designatort(lhs_index));
326  new_rhs.new_value()=rhs;
327 
328  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
329 
331  state, lhs_array, new_full_lhs, new_rhs, guard, assignment_type);
332 
333  #else
334  // turn
335  // a[i]=e
336  // into
337  // a'==a WITH [i:=e]
338 
339  exprt new_rhs(ID_with, lhs_type);
340  new_rhs.copy_to_operands(lhs_array, lhs_index, rhs);
341 
342  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
343 
345  state, lhs_array, new_full_lhs, new_rhs, guard, assignment_type);
346  #endif
347 }
348 
350  statet &state,
351  const member_exprt &lhs,
352  const exprt &full_lhs,
353  const exprt &rhs,
354  guardt &guard,
355  assignment_typet assignment_type)
356 {
357  // Symbolic execution of a struct member assignment.
358 
359  // lhs must be member operand, which
360  // takes one operand, which must be a structure.
361 
362  exprt lhs_struct=lhs.op0();
363 
364  // typecasts involved? C++ does that for inheritance.
365  if(lhs_struct.id()==ID_typecast)
366  {
367  assert(lhs_struct.operands().size()==1);
368 
369  if(lhs_struct.op0().id()=="NULL-object")
370  {
371  // ignore, and give up
372  return;
373  }
374  else
375  {
376  // remove the type cast, we assume that the member is there
377  exprt tmp=lhs_struct.op0();
378  const typet &op0_type=ns.follow(tmp.type());
379 
380  if(op0_type.id()==ID_struct)
381  lhs_struct=tmp;
382  else
383  return; // ignore and give up
384  }
385  }
386 
387  const irep_idt &component_name=lhs.get_component_name();
388 
389  #ifdef USE_UPDATE
390 
391  // turn
392  // a.c=e
393  // into
394  // a'==UPDATE(a, .c, e)
395 
396  update_exprt new_rhs(lhs_struct.type());
397  new_rhs.old()=lhs_struct;
398  new_rhs.designator().push_back(member_designatort(component_name));
399  new_rhs.new_value()=rhs;
400 
401  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
402 
404  state, lhs_struct, new_full_lhs, new_rhs, guard, assignment_type);
405 
406  #else
407  // turn
408  // a.c=e
409  // into
410  // a'==a WITH [c:=e]
411 
412  exprt new_rhs(ID_with, lhs_struct.type());
413  new_rhs.copy_to_operands(lhs_struct, exprt(ID_member_name), rhs);
414  new_rhs.op1().set(ID_component_name, component_name);
415 
416  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
417 
419  state, lhs_struct, new_full_lhs, new_rhs, guard, assignment_type);
420  #endif
421 }
422 
424  statet &state,
425  const if_exprt &lhs,
426  const exprt &full_lhs,
427  const exprt &rhs,
428  guardt &guard,
429  assignment_typet assignment_type)
430 {
431  // we have (c?a:b)=e;
432 
433  guardt old_guard=guard;
434 
435  exprt renamed_guard=lhs.cond();
436  state.rename(renamed_guard, ns);
437  do_simplify(renamed_guard);
438 
439  if(!renamed_guard.is_false())
440  {
441  guard.add(renamed_guard);
443  state, lhs.true_case(), full_lhs, rhs, guard, assignment_type);
444  guard.swap(old_guard);
445  }
446 
447  if(!renamed_guard.is_true())
448  {
449  guard.add(not_exprt(renamed_guard));
451  state, lhs.false_case(), full_lhs, rhs, guard, assignment_type);
452  guard.swap(old_guard);
453  }
454 }
455 
457  statet &state,
458  const byte_extract_exprt &lhs,
459  const exprt &full_lhs,
460  const exprt &rhs,
461  guardt &guard,
462  assignment_typet assignment_type)
463 {
464  // we have byte_extract_X(object, offset)=value
465  // turn into object=byte_update_X(object, offset, value)
466 
467  exprt new_rhs;
468 
469  if(lhs.id()==ID_byte_extract_little_endian)
470  new_rhs.id(ID_byte_update_little_endian);
471  else if(lhs.id()==ID_byte_extract_big_endian)
472  new_rhs.id(ID_byte_update_big_endian);
473  else
474  assert(false);
475 
476  new_rhs.copy_to_operands(lhs.op(), lhs.offset(), rhs);
477  new_rhs.type()=lhs.op().type();
478 
479  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
480 
482  state, lhs.op(), new_full_lhs, new_rhs, guard, assignment_type);
483 }
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:19
The type of an expression.
Definition: type.h:20
exprt as_expr() const
Definition: guard.h:43
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
Boolean negation.
Definition: std_expr.h:2648
exprt & true_case()
Definition: std_expr.h:2805
semantic type conversion
Definition: std_expr.h:1725
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
symex_targett & target
Definition: goto_symex.h:105
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
virtual void symex_assign(statet &state, const code_assignt &code)
goto_programt::const_targett pc
Definition: symex_target.h:32
exprt & op0()
Definition: expr.h:84
void append(const guardt &guard)
Definition: guard.h:36
Operator to update elements in structs and arrays.
Definition: std_expr.h:3039
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
void symex_assign_byte_extract(statet &state, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
const irep_idt & get_identifier() const
Definition: std_expr.h:120
exprt::operandst & designator()
Definition: std_expr.h:3077
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
virtual void symex_gcc_builtin_va_arg_next(statet &state, const exprt &lhs, const side_effect_exprt &code)
void symex_assign_if(statet &state, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
bool is_false() const
Definition: expr.cpp:140
bool constant_propagation
Definition: goto_symex.h:94
Symbolic Execution.
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
bool is_true() const
Definition: expr.cpp:133
optionst options
Definition: goto_symex.h:96
Definition: guard.h:19
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
void replace_nondet(exprt &expr)
Definition: goto_symex.cpp:25
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1023
Extract member of struct or union.
Definition: std_expr.h:3214
const irep_idt get_level_1() const
Definition: ssa_expr.h:112
goto_symex_statet::level2t level2
void symex_assign_symbol(statet &state, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
static exprt add_to_lhs(const exprt &lhs, const exprt &what)
virtual void symex_printf(statet &state, const exprt &lhs, const exprt &rhs)
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
Expression classes for byte-level operators.
exprt & old()
Definition: std_expr.h:3063
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
The NIL expression.
Definition: std_expr.h:3764
exprt & rhs()
Definition: std_code.h:162
bool is_parameter
Definition: symbol.h:71
Symbolic Execution.
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
exprt & op1()
Definition: expr.h:87
Generic base class for unary expressions.
Definition: std_expr.h:221
void clean_expr(exprt &expr, statet &state, bool write)
void symex_assign_struct_member(statet &state, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
exprt & false_case()
Definition: std_expr.h:2815
void symex_assign_rec(statet &state, const code_assignt &code)
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)=0
virtual void symex_malloc(statet &state, const exprt &lhs, const side_effect_exprt &code)
exprt & index()
Definition: std_expr.h:1208
unsigned current_count(const irep_idt &identifier) const
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value)
irep_idt get_object_name() const
Definition: ssa_expr.h:46
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
irep_idt get_component_name() const
Definition: std_expr.h:3249
void make_nil()
Definition: irep.h:243
const std::string & id_string() const
Definition: irep.h:192
void swap(irept &irep)
Definition: irep.h:231
bool is_auxiliary
Definition: symbol.h:71
exprt & new_value()
Definition: std_expr.h:3087
An expression containing a side effect.
Definition: std_code.h:997
operandst & operands()
Definition: expr.h:70
TO_BE_DOCUMENTED.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const namespacet & ns
Definition: goto_symex.h:104
bool empty() const
Definition: dstring.h:61
exprt & array()
Definition: std_expr.h:1198
void make_typecast(const typet &_type)
Definition: expr.cpp:90
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
void symex_assign_typecast(statet &state, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
Assignment.
Definition: std_code.h:144
void add(const exprt &expr)
Definition: guard.cpp:64
void symex_assign_array(statet &state, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
const irep_idt & get_statement() const
Definition: std_code.h:1012
array index operator
Definition: std_expr.h:1170
symex_targett::sourcet source