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  symex_printf(state, lhs, side_effect_expr);
58  else if(statement==ID_gcc_builtin_va_arg_next)
59  symex_gcc_builtin_va_arg_next(state, lhs, side_effect_expr);
60  else
61  throw "symex_assign: unexpected side effect: "+id2string(statement);
62  }
63  else
64  {
66 
67  // Let's hide return value assignments.
68  if(lhs.id()==ID_symbol &&
69  id2string(to_symbol_expr(lhs).get_identifier()).find(
70  "#return_value!")!=std::string::npos)
72 
73  // We hide if we are in a hidden function.
74  if(state.top().hidden_function)
76 
77  // We hide if we are executing a hidden instruction.
78  if(state.source.pc->source_location.get_hide())
80 
81  guardt guard; // NOT the state guard!
82  symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);
83  }
84 }
85 
87  const exprt &lhs,
88  const exprt &what)
89 {
90  assert(lhs.id()!=ID_symbol);
91  exprt tmp_what=what;
92 
93  if(tmp_what.id()!=ID_symbol)
94  {
95  assert(tmp_what.operands().size()>=1);
96  tmp_what.op0().make_nil();
97  }
98 
99  exprt new_lhs=lhs;
100 
101  exprt *p=&new_lhs;
102 
103  while(p->is_not_nil())
104  {
105  assert(p->id()!=ID_symbol);
106  assert(p->operands().size()>=1);
107  p=&p->op0();
108  }
109 
110  assert(p->is_nil());
111 
112  *p=tmp_what;
113  return new_lhs;
114 }
115 
117  statet &state,
118  const exprt &lhs,
119  const exprt &full_lhs,
120  const exprt &rhs,
121  guardt &guard,
122  assignment_typet assignment_type)
123 {
124  if(lhs.id()==ID_symbol &&
125  lhs.get_bool(ID_C_SSA_symbol))
127  state, to_ssa_expr(lhs), full_lhs, rhs, guard, assignment_type);
128  else if(lhs.id()==ID_index)
130  state, to_index_expr(lhs), full_lhs, rhs, guard, assignment_type);
131  else if(lhs.id()==ID_member)
132  {
133  const typet &type=ns.follow(to_member_expr(lhs).struct_op().type());
134  if(type.id()==ID_struct)
136  state, to_member_expr(lhs), full_lhs, rhs, guard, assignment_type);
137  else if(type.id()==ID_union)
138  {
139  // should have been replaced by byte_extract
140  throw "symex_assign_rec: unexpected assignment to union member";
141  }
142  else
143  throw
144  "symex_assign_rec: unexpected assignment to member of `"+
145  type.id_string()+"'";
146  }
147  else if(lhs.id()==ID_if)
149  state, to_if_expr(lhs), full_lhs, rhs, guard, assignment_type);
150  else if(lhs.id()==ID_typecast)
152  state, to_typecast_expr(lhs), full_lhs, rhs, guard, assignment_type);
153  else if(lhs.id() == ID_string_constant ||
154  lhs.id() == ID_null_object ||
155  lhs.id() == "zero_string" ||
156  lhs.id() == "is_zero_string" ||
157  lhs.id() == "zero_string_length")
158  {
159  // ignore
160  }
161  else if(lhs.id()==ID_byte_extract_little_endian ||
162  lhs.id()==ID_byte_extract_big_endian)
163  {
165  state, to_byte_extract_expr(lhs), full_lhs, rhs, guard, assignment_type);
166  }
167  else if(lhs.id()==ID_complex_real ||
168  lhs.id()==ID_complex_imag)
169  {
170  // this is stuff like __real__ x = 1;
171  assert(lhs.operands().size()==1);
172 
173  exprt new_rhs=exprt(ID_complex, lhs.op0().type());
174  new_rhs.operands().resize(2);
175 
176  if(lhs.id()==ID_complex_real)
177  {
178  new_rhs.op0()=rhs;
179  new_rhs.op1()=unary_exprt(ID_complex_imag, lhs.op0(), lhs.type());
180  }
181  else
182  {
183  new_rhs.op0()=unary_exprt(ID_complex_real, lhs.op0(), lhs.type());
184  new_rhs.op1()=rhs;
185  }
186 
188  state, lhs.op0(), full_lhs, new_rhs, guard, assignment_type);
189  }
190  else
191  throw "assignment to `"+lhs.id_string()+"' not handled";
192 }
193 
195  statet &state,
196  const ssa_exprt &lhs, // L1
197  const exprt &full_lhs,
198  const exprt &rhs,
199  guardt &guard,
200  assignment_typet assignment_type)
201 {
202  // do not assign to L1 objects that have gone out of scope --
203  // pointer dereferencing may yield such objects; parameters do not
204  // have an L2 entry set up beforehand either, so exempt them from
205  // this check (all other L1 objects should have seen a declaration)
206  const symbolt *s;
207  if(!ns.lookup(lhs.get_object_name(), s) &&
208  !s->is_parameter &&
209  !lhs.get_level_1().empty() &&
210  state.level2.current_count(lhs.get_identifier())==0)
211  return;
212 
213  exprt ssa_rhs=rhs;
214 
215  // put assignment guard into the rhs
216  if(!guard.is_true())
217  {
218  if_exprt tmp_ssa_rhs;
219  tmp_ssa_rhs.type()=ssa_rhs.type();
220  tmp_ssa_rhs.cond()=guard.as_expr();
221  tmp_ssa_rhs.true_case()=ssa_rhs;
222  tmp_ssa_rhs.false_case()=lhs;
223  tmp_ssa_rhs.swap(ssa_rhs);
224  }
225 
226  state.rename(ssa_rhs, ns);
227  do_simplify(ssa_rhs);
228 
229  ssa_exprt ssa_lhs=lhs;
230  state.assignment(
231  ssa_lhs,
232  ssa_rhs,
233  ns,
234  options.get_bool_option("simplify"),
237 
238  exprt ssa_full_lhs=full_lhs;
239  ssa_full_lhs=add_to_lhs(ssa_full_lhs, ssa_lhs);
240  const bool record_events=state.record_events;
241  state.record_events=false;
242  state.rename(ssa_full_lhs, ns);
243  state.record_events=record_events;
244 
245  guardt tmp_guard(state.guard);
246  tmp_guard.append(guard);
247 
248  // do the assignment
249  const symbolt &symbol =
251 
252  if(symbol.is_auxiliary)
254 
256  log.debug(),
257  [this, &ssa_lhs](messaget::mstreamt &mstream) {
258  mstream << "Assignment to " << ssa_lhs.get_identifier()
259  << " [" << pointer_offset_bits(ssa_lhs.type(), ns) << " bits]"
260  << messaget::eom;
261  });
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  with_exprt new_rhs(lhs_array, lhs_index, rhs);
340  new_rhs.type() = lhs_type;
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() == 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  with_exprt new_rhs(lhs_struct, exprt(ID_member_name), rhs);
413  new_rhs.op1().set(ID_component_name, component_name);
414 
415  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
416 
418  state, lhs_struct, new_full_lhs, new_rhs, guard, assignment_type);
419  #endif
420 }
421 
423  statet &state,
424  const if_exprt &lhs,
425  const exprt &full_lhs,
426  const exprt &rhs,
427  guardt &guard,
428  assignment_typet assignment_type)
429 {
430  // we have (c?a:b)=e;
431 
432  guardt old_guard=guard;
433 
434  exprt renamed_guard=lhs.cond();
435  state.rename(renamed_guard, ns);
436  do_simplify(renamed_guard);
437 
438  if(!renamed_guard.is_false())
439  {
440  guard.add(renamed_guard);
442  state, lhs.true_case(), full_lhs, rhs, guard, assignment_type);
443  guard.swap(old_guard);
444  }
445 
446  if(!renamed_guard.is_true())
447  {
448  guard.add(not_exprt(renamed_guard));
450  state, lhs.false_case(), full_lhs, rhs, guard, assignment_type);
451  guard.swap(old_guard);
452  }
453 }
454 
456  statet &state,
457  const byte_extract_exprt &lhs,
458  const exprt &full_lhs,
459  const exprt &rhs,
460  guardt &guard,
461  assignment_typet assignment_type)
462 {
463  // we have byte_extract_X(object, offset)=value
464  // turn into object=byte_update_X(object, offset, value)
465 
466  exprt new_rhs;
467 
468  if(lhs.id()==ID_byte_extract_little_endian)
469  new_rhs.id(ID_byte_update_little_endian);
470  else if(lhs.id()==ID_byte_extract_big_endian)
471  new_rhs.id(ID_byte_update_big_endian);
472  else
473  UNREACHABLE;
474 
475  new_rhs.copy_to_operands(lhs.op(), lhs.offset(), rhs);
476  new_rhs.type()=lhs.op().type();
477 
478  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
479 
481  state, lhs.op(), new_full_lhs, new_rhs, guard, assignment_type);
482 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
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:3230
exprt & true_case()
Definition: std_expr.h:3395
semantic type conversion
Definition: std_expr.h:2111
const bool allow_pointer_unsoundness
Definition: goto_symex.h:206
bool is_nil() const
Definition: irep.h:102
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
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:3672
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:3710
bool is_false() const
Definition: expr.cpp:131
bool constant_propagation
Definition: goto_symex.h:215
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:3361
exprt & cond()
Definition: std_expr.h:3385
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:1287
Extract member of struct or union.
Definition: std_expr.h:3871
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:237
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
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:3696
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:4510
exprt & rhs()
Definition: std_code.h:213
bool is_parameter
Definition: symbol.h:68
Symbolic Execution.
messaget log
Definition: goto_symex.h:241
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
symex_target_equationt & target
Definition: goto_symex.h:238
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:3955
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
exprt & false_case()
Definition: std_expr.h:3405
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:202
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:3461
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:3895
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:250
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:243
const std::string & id_string() const
Definition: irep.h:192
void swap(irept &irep)
Definition: irep.h:231
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:3720
virtual void symex_printf(statet &, const exprt &lhs, const exprt &rhs)
mstreamt & debug() const
Definition: message.h:332
An expression containing a side effect.
Definition: std_code.h:1238
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:61
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:130
Assignment.
Definition: std_code.h:195
void add(const exprt &expr)
Definition: guard.cpp:64
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
const irep_idt & get_statement() const
Definition: std_code.h:1253
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)