cprover
symex_goto.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 <algorithm>
15 
16 #include <util/invariant.h>
18 #include <util/std_expr.h>
19 
20 #include <analyses/dirty.h>
21 
23 {
24  const goto_programt::instructiont &instruction=*state.source.pc;
25  statet::framet &frame=state.top();
26 
27  exprt old_guard=instruction.guard;
28  clean_expr(old_guard, state, false);
29 
30  exprt new_guard=old_guard;
31  state.rename(new_guard, ns);
32  do_simplify(new_guard);
33 
34  if(new_guard.is_false() ||
35  state.guard.is_false())
36  {
37  if(!state.guard.is_false())
38  target.location(state.guard.as_expr(), state.source);
39 
40  // next instruction
41  symex_transition(state);
42  return; // nothing to do
43  }
44 
45  target.goto_instruction(state.guard.as_expr(), new_guard, state.source);
46 
48  !instruction.targets.empty(), "goto should have at least one target");
49 
50  // we only do deterministic gotos for now
51  if(instruction.targets.size()!=1)
52  throw "no support for non-deterministic gotos";
53 
54  goto_programt::const_targett goto_target=
55  instruction.get_target();
56 
57  bool forward=!instruction.is_backwards_goto();
58 
59  if(!forward) // backwards?
60  {
61  // is it label: goto label; or while(cond); - popular in SV-COMP
62  if(
64  (goto_target == state.source.pc ||
65  (instruction.incoming_edges.size() == 1 &&
66  *instruction.incoming_edges.begin() == goto_target)))
67  {
68  // generate assume(false) or a suitable negation if this
69  // instruction is a conditional goto
70  exprt negated_cond;
71 
72  if(new_guard.is_true())
73  negated_cond=false_exprt();
74  else
75  negated_cond=not_exprt(new_guard);
76 
77  symex_assume(state, negated_cond);
78 
79  // next instruction
80  symex_transition(state);
81  return;
82  }
83 
84  unsigned &unwind=
85  frame.loop_iterations[goto_programt::loop_id(*state.source.pc)].count;
86  unwind++;
87 
88  // continue unwinding?
89  if(get_unwind(state.source, state.call_stack(), unwind))
90  {
91  // no!
92  loop_bound_exceeded(state, new_guard);
93 
94  // next instruction
95  symex_transition(state);
96  return;
97  }
98 
99  if(new_guard.is_true())
100  {
101  symex_transition(state, goto_target, true);
102  return; // nothing else to do
103  }
104  }
105 
106  exprt simpl_state_guard = state.guard.as_expr();
107  do_simplify(simpl_state_guard);
108 
109  // No point executing both branches of an unconditional goto.
110  if(
111  new_guard.is_true() && // We have an unconditional goto, AND
112  // either there are no blocks between us and the target in the
113  // surrounding scope
114  (simpl_state_guard.is_true() ||
115  // or there is another block, but we're doing path exploration so
116  // we're going to skip over it for now and return to it later.
118  {
120  instruction.targets.size() > 0,
121  "Instruction is an unconditional goto with no target: " +
122  instruction.code.pretty());
123  symex_transition(state, instruction.get_target(), true);
124  return;
125  }
126 
127  goto_programt::const_targett new_state_pc, state_pc;
128  symex_targett::sourcet original_source=state.source;
129 
130  if(forward)
131  {
132  new_state_pc=goto_target;
133  state_pc=state.source.pc;
134  state_pc++;
135 
136  // skip dead instructions
137  if(new_guard.is_true())
138  while(state_pc!=goto_target && !state_pc->is_target())
139  ++state_pc;
140 
141  if(state_pc==goto_target)
142  {
143  symex_transition(state, goto_target);
144  return; // nothing else to do
145  }
146  }
147  else
148  {
149  new_state_pc=state.source.pc;
150  new_state_pc++;
151  state_pc=goto_target;
152  }
153 
154  // Normally the next instruction to execute would be state_pc and we save
155  // new_state_pc for later. But if we're executing from a saved state, then
156  // new_state_pc should be the state that we saved from earlier, so let's
157  // execute that instead.
158  if(state.has_saved_jump_target)
159  {
160  INVARIANT(
161  new_state_pc == state.saved_target,
162  "Tried to explore the other path of a branch, but the next "
163  "instruction along that path is not the same as the instruction "
164  "that we saved at the branch point. Saved instruction is " +
165  state.saved_target->code.pretty() +
166  "\nwe were intending "
167  "to explore " +
168  new_state_pc->code.pretty() +
169  "\nthe "
170  "instruction we think we saw on a previous path exploration is " +
171  state_pc->code.pretty());
172  goto_programt::const_targett tmp = new_state_pc;
173  new_state_pc = state_pc;
174  state_pc = tmp;
175 
176  log.debug() << "Resuming from jump target '" << state_pc->source_location
177  << "'" << log.eom;
178  }
179  else if(state.has_saved_next_instruction)
180  {
181  log.debug() << "Resuming from next instruction '"
182  << state_pc->source_location << "'" << log.eom;
183  }
184  else if(doing_path_exploration)
185  {
186  // We should save both the instruction after this goto, and the target of
187  // the goto.
188 
189  path_storaget::patht next_instruction(target, state);
190  next_instruction.state.saved_target = state_pc;
191  next_instruction.state.has_saved_next_instruction = true;
192  next_instruction.state.saved_target_is_backwards = !forward;
193 
194  path_storaget::patht jump_target(target, state);
195  jump_target.state.saved_target = new_state_pc;
196  jump_target.state.has_saved_jump_target = true;
197  // `forward` tells us where the branch we're _currently_ executing is
198  // pointing to; this needs to be inverted for the branch that we're saving,
199  // so let its truth value for `backwards` be the same as ours for `forward`.
200  jump_target.state.saved_target_is_backwards = forward;
201 
202  log.debug() << "Saving next instruction '"
203  << next_instruction.state.saved_target->source_location << "'"
204  << log.eom;
205  log.debug() << "Saving jump target '"
206  << jump_target.state.saved_target->source_location << "'"
207  << log.eom;
208  path_storage.push(next_instruction, jump_target);
209 
210  // It is now up to the caller of symex to decide which path to continue
211  // executing. Signal to the caller that states have been pushed (therefore
212  // symex has not yet completed and must be resumed), and bail out.
213  should_pause_symex = true;
214  return;
215  }
216 
217  // put into state-queue
218  statet::goto_state_listt &goto_state_list=
219  state.top().goto_state_map[new_state_pc];
220 
221  goto_state_list.push_back(statet::goto_statet(state));
222 
223  symex_transition(state, state_pc, !forward);
224 
225  // adjust guards
226  if(new_guard.is_true())
227  {
228  state.guard.make_false();
229  }
230  else
231  {
232  // produce new guard symbol
233  exprt guard_expr;
234 
235  if(new_guard.id()==ID_symbol ||
236  (new_guard.id()==ID_not &&
237  new_guard.operands().size()==1 &&
238  new_guard.op0().id()==ID_symbol))
239  guard_expr=new_guard;
240  else
241  {
242  symbol_exprt guard_symbol_expr=
244  exprt new_rhs=new_guard;
245  new_rhs.make_not();
246 
247  ssa_exprt new_lhs(guard_symbol_expr);
248  state.rename(new_lhs, ns, goto_symex_statet::L1);
249  state.assignment(new_lhs, new_rhs, ns, true, false);
250 
251  guardt guard;
252 
254  log.debug(),
255  [this, &new_lhs](messaget::mstreamt &mstream) {
256  mstream << "Assignment to " << new_lhs.get_identifier()
257  << " [" << pointer_offset_bits(new_lhs.type(), ns) << " bits]"
258  << messaget::eom;
259  });
260 
262  guard.as_expr(),
263  new_lhs, new_lhs, guard_symbol_expr,
264  new_rhs,
265  original_source,
267 
268  guard_expr=guard_symbol_expr;
269  guard_expr.make_not();
270  state.rename(guard_expr, ns);
271  }
272 
273  if(state.has_saved_jump_target)
274  {
275  if(forward)
276  state.guard.add(guard_expr);
277  else
278  {
279  guard_expr.make_not();
280  state.guard.add(guard_expr);
281  }
282  }
283  else
284  {
285  statet::goto_statet &new_state = goto_state_list.back();
286  if(forward)
287  {
288  new_state.guard.add(guard_expr);
289  guard_expr.make_not();
290  state.guard.add(guard_expr);
291  }
292  else
293  {
294  state.guard.add(guard_expr);
295  guard_expr.make_not();
296  new_state.guard.add(guard_expr);
297  }
298  }
299  }
300 }
301 
302 void goto_symext::symex_step_goto(statet &state, bool taken)
303 {
304  const goto_programt::instructiont &instruction=*state.source.pc;
305 
306  exprt guard(instruction.guard);
307  dereference(guard, state, false);
308  state.rename(guard, ns);
309 
310  if(!taken)
311  guard.make_not();
312 
313  state.guard.guard_expr(guard);
314  do_simplify(guard);
315 
316  target.assumption(state.guard.as_expr(), guard, state.source);
317 }
318 
320 {
321  statet::framet &frame=state.top();
322 
323  // first, see if this is a target at all
324  statet::goto_state_mapt::iterator state_map_it=
325  frame.goto_state_map.find(state.source.pc);
326 
327  if(state_map_it==frame.goto_state_map.end())
328  return; // nothing to do
329 
330  // we need to merge
331  statet::goto_state_listt &state_list=state_map_it->second;
332 
333  for(statet::goto_state_listt::reverse_iterator
334  list_it=state_list.rbegin();
335  list_it!=state_list.rend();
336  list_it++)
337  merge_goto(*list_it, state);
338 
339  // clean up to save some memory
340  frame.goto_state_map.erase(state_map_it);
341 }
342 
344  const statet::goto_statet &goto_state,
345  statet &state)
346 {
347  // check atomic section
348  if(state.atomic_section_id!=goto_state.atomic_section_id)
349  throw "atomic sections differ across branches";
350 
351  // do SSA phi functions
352  phi_function(goto_state, state);
353 
354  merge_value_sets(goto_state, state);
355 
356  // adjust guard
357  state.guard|=goto_state.guard;
358 
359  // adjust depth
360  state.depth=std::min(state.depth, goto_state.depth);
361 }
362 
364  const statet::goto_statet &src,
365  statet &dest)
366 {
367  if(dest.guard.is_false())
368  {
369  dest.value_set=src.value_set;
370  return;
371  }
372 
373  dest.value_set.make_union(src.value_set);
374 }
375 
377  const statet::goto_statet &goto_state,
378  statet &dest_state)
379 {
380  // go over all variables to see what changed
381  std::unordered_set<ssa_exprt, irep_hash> variables;
382 
383  goto_state.level2_get_variables(variables);
384  dest_state.level2.get_variables(variables);
385 
386  guardt diff_guard;
387 
388  if(!variables.empty())
389  {
390  diff_guard=goto_state.guard;
391 
392  // this gets the diff between the guards
393  diff_guard-=dest_state.guard;
394  }
395 
396  for(std::unordered_set<ssa_exprt, irep_hash>::const_iterator
397  it=variables.begin();
398  it!=variables.end();
399  it++)
400  {
401  const irep_idt l1_identifier=it->get_identifier();
402  const irep_idt &obj_identifier=it->get_object_name();
403 
404  if(obj_identifier==guard_identifier)
405  continue; // just a guard, don't bother
406 
407  if(goto_state.level2_current_count(l1_identifier)==
408  dest_state.level2.current_count(l1_identifier))
409  continue; // not at all changed
410 
411  // changed!
412 
413  // shared variables are renamed on every access anyway, we don't need to
414  // merge anything
415  const symbolt &symbol=ns.lookup(obj_identifier);
416 
417  // shared?
418  if(
419  dest_state.atomic_section_id == 0 && dest_state.threads.size() >= 2 &&
420  (symbol.is_shared() || (dest_state.dirty)(symbol.name)))
421  continue; // no phi nodes for shared stuff
422 
423  // don't merge (thread-)locals across different threads, which
424  // may have been introduced by symex_start_thread (and will
425  // only later be removed from level2.current_names by pop_frame
426  // once the thread is executed)
427  if(!it->get_level_0().empty() &&
428  it->get_level_0()!=std::to_string(dest_state.source.thread_nr))
429  continue;
430 
431  exprt goto_state_rhs=*it, dest_state_rhs=*it;
432 
433  {
434  goto_symex_statet::propagationt::valuest::const_iterator p_it=
435  goto_state.propagation.values.find(l1_identifier);
436 
437  if(p_it!=goto_state.propagation.values.end())
438  goto_state_rhs=p_it->second;
439  else
440  to_ssa_expr(goto_state_rhs).set_level_2(
441  goto_state.level2_current_count(l1_identifier));
442  }
443 
444  {
445  goto_symex_statet::propagationt::valuest::const_iterator p_it=
446  dest_state.propagation.values.find(l1_identifier);
447 
448  if(p_it!=dest_state.propagation.values.end())
449  dest_state_rhs=p_it->second;
450  else
451  to_ssa_expr(dest_state_rhs).set_level_2(
452  dest_state.level2.current_count(l1_identifier));
453  }
454 
455  exprt rhs;
456 
457  // Don't add a conditional to the assignment when:
458  // 1. Either guard is false, so we can't follow that branch.
459  // 2. Either identifier is of generation zero, and so hasn't been
460  // initialized and therefor an invalid target.
461  if(dest_state.guard.is_false())
462  rhs=goto_state_rhs;
463  else if(goto_state.guard.is_false())
464  rhs=dest_state_rhs;
465  else if(goto_state.level2_current_count(l1_identifier) == 0)
466  {
467  rhs = dest_state_rhs;
468  }
469  else if(dest_state.level2.current_count(l1_identifier) == 0)
470  {
471  rhs = goto_state_rhs;
472  }
473  else
474  {
475  rhs=if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);
476  do_simplify(rhs);
477  }
478 
479  ssa_exprt new_lhs=*it;
480  const bool record_events=dest_state.record_events;
481  dest_state.record_events=false;
482  dest_state.assignment(new_lhs, rhs, ns, true, true);
483  dest_state.record_events=record_events;
484 
486  log.debug(),
487  [this, &new_lhs](messaget::mstreamt &mstream) {
488  mstream << "Assignment to " << new_lhs.get_identifier()
489  << " [" << pointer_offset_bits(new_lhs.type(), ns) << " bits]"
490  << messaget::eom;
491  });
492 
494  true_exprt(),
495  new_lhs, new_lhs, new_lhs.get_original_expr(),
496  rhs,
497  dest_state.source,
499  }
500 }
501 
503  statet &state,
504  const exprt &guard)
505 {
506  const unsigned loop_number=state.source.pc->loop_number;
507 
508  exprt negated_cond;
509 
510  if(guard.is_true())
511  negated_cond=false_exprt();
512  else
513  negated_cond=not_exprt(guard);
514 
515  bool unwinding_assertions=
516  options.get_bool_option("unwinding-assertions");
517 
518  bool partial_loops=
519  options.get_bool_option("partial-loops");
520 
521  if(!partial_loops)
522  {
523  if(unwinding_assertions)
524  {
525  // Generate VCC for unwinding assertion.
526  vcc(negated_cond,
527  "unwinding assertion loop "+std::to_string(loop_number),
528  state);
529 
530  // add to state guard to prevent further assignments
531  state.guard.add(negated_cond);
532  }
533  else
534  {
535  // generate unwinding assumption, unless we permit partial loops
536  symex_assume(state, negated_cond);
537  }
538  }
539 }
540 
542  const symex_targett::sourcet &,
544  unsigned)
545 {
546  // by default, we keep going
547  return false;
548 }
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
irep_idt name
The unique identifier.
Definition: symbol.h:43
exprt as_expr() const
Definition: guard.h:43
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
bool is_shared() const
Definition: symbol.h:96
irep_idt guard_identifier
Definition: goto_symex.h:281
goto_programt::const_targett pc
Definition: symex_target.h:32
void guard_expr(exprt &dest) const
Definition: guard.cpp:19
void level2_get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
class goto_symex_statet::propagationt propagation
virtual void symex_goto(statet &)
Definition: symex_goto.cpp:22
std::set< targett > incoming_edges
Definition: goto_program.h:226
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
Variables whose address is taken.
virtual void symex_transition(statet &, goto_programt::const_targett to, bool is_backwards_goto=false)
Definition: symex_main.cpp:24
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
const irep_idt & get_identifier() const
Definition: std_expr.h:128
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
record an assumption
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
Definition: value_set.cpp:245
bool is_false() const
Definition: expr.cpp:131
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)
record a goto instruction
virtual bool get_unwind(const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind)
Definition: symex_goto.cpp:541
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
Definition: symex_goto.cpp:343
virtual void symex_step_goto(statet &, bool taken)
Definition: symex_goto.cpp:302
The trinary if-then-else operator.
Definition: std_expr.h:3359
bool is_true() const
Definition: expr.cpp:124
Definition: guard.h:19
loop_iterationst loop_iterations
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
typet & type()
Definition: expr.h:56
The proper Booleans.
Definition: std_types.h:34
void set_level_2(unsigned i)
Definition: ssa_expr.h:95
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
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:202
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:374
void get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
unsigned level2_current_count(const irep_idt &identifier) const
targetst targets
The list of successor instructions.
Definition: goto_program.h:198
unsigned depth
distance from entry
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
virtual void dereference(exprt &, statet &, const bool write)
goto_symex_statet::level2t level2
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:239
bool self_loops_to_assumptions
Definition: goto_symex.h:218
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
The boolean constant true.
Definition: std_expr.h:4486
source_locationt source_location
Definition: message.h:214
Symbolic Execution.
virtual void symex_assume(statet &, const exprt &cond)
Definition: symex_main.cpp:75
messaget log
Definition: goto_symex.h:243
API to expression classes.
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
symex_target_equationt & target
Definition: goto_symex.h:240
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
Definition: symex_goto.cpp:363
instructionst::const_iterator const_targett
Definition: goto_program.h:398
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:583
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
path_storaget & path_storage
Definition: goto_symex.h:470
incremental_dirtyt dirty
goto_state_mapt goto_state_map
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
virtual void loop_bound_exceeded(statet &, const exprt &guard)
Definition: symex_goto.cpp:502
The boolean constant false.
Definition: std_expr.h:4497
Pointer Logic.
void phi_function(const statet::goto_statet &goto_state, statet &)
Definition: symex_goto.cpp:376
const optionst & options
Definition: goto_symex.h:204
virtual void vcc(const exprt &, const std::string &msg, statet &)
Definition: symex_main.cpp:48
std::vector< framet > call_stackt
void make_not()
Definition: expr.cpp:91
void clean_expr(exprt &, statet &, bool write)
unsigned current_count(const irep_idt &identifier) const
goto_programt::const_targett saved_target
bool should_pause_symex
Have states been pushed onto the workqueue?
Definition: goto_symex.h:177
Base class for all expressions.
Definition: expr.h:42
call_stackt & call_stack()
void make_false()
Definition: expr.cpp:150
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
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
virtual void location(const exprt &guard, const sourcet &source)
just record a location
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:28
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
void merge_gotos(statet &)
Definition: symex_goto.cpp:319
Expression to hold a symbol (variable)
Definition: std_expr.h:90
mstreamt & debug() const
Definition: message.h:332
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
virtual void push(const patht &next_instruction, const patht &jump_target)=0
Add paths to resume to the storage.
std::list< goto_statet > goto_state_listt
operandst & operands()
Definition: expr.h:66
const bool doing_path_exploration
Definition: goto_symex.h:207
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
goto_symex_statet state
Definition: path_storage.h:31
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
void add(const exprt &expr)
Definition: guard.cpp:64
symex_targett::sourcet source