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