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 #include "goto_symex_is_constant.h"
14 
15 #include <algorithm>
16 
17 #include <util/exception_utils.h>
18 #include <util/expr_util.h>
19 #include <util/invariant.h>
21 #include <util/simplify_expr.h>
22 #include <util/std_expr.h>
23 
26 
28  goto_symex_statet &current_state,
29  goto_statet &jump_taken_state,
30  goto_statet &jump_not_taken_state,
31  const exprt &original_guard,
32  const exprt &new_guard,
33  const namespacet &ns)
34 {
35  // It would be better to call try_filter_value_sets after apply_condition,
36  // and pass nullptr for value sets which apply_condition successfully updated
37  // already. However, try_filter_value_sets calls rename to do constant
38  // propagation, and apply_condition can update the constant propagator. Since
39  // apply condition will never succeed on both jump_taken_state and
40  // jump_not_taken_state, it should be possible to pass a reference to an
41  // unmodified goto_statet to use for renaming. But renaming needs a
42  // goto_symex_statet, not just a goto_statet, and we only have access to one
43  // of those. A future improvement would be to split rename into two parts:
44  // one part on goto_symex_statet which is non-const and deals with
45  // l2 thread reads, and one part on goto_statet which is const and could be
46  // used in try_filter_value_sets.
47 
49  current_state,
50  original_guard,
51  jump_taken_state.value_set,
52  &jump_taken_state.value_set,
53  &jump_not_taken_state.value_set,
54  ns);
55 
57  return;
58 
59  jump_taken_state.apply_condition(new_guard, current_state, ns);
60 
61  // Could use not_exprt + simplify, but let's avoid paying that cost on quite
62  // a hot path:
63  const exprt negated_new_guard = boolean_negate(new_guard);
64  jump_not_taken_state.apply_condition(negated_new_guard, current_state, ns);
65 }
66 
79  const irep_idt &operation,
80  const symbol_exprt &symbol_expr,
81  const exprt &other_operand,
82  const value_sett &value_set,
83  const irep_idt language_mode,
84  const namespacet &ns)
85 {
86  const constant_exprt *constant_expr =
87  expr_try_dynamic_cast<constant_exprt>(other_operand);
88  const exprt other_without_typecast = skip_typecast(other_operand);
89 
90  if(
91  other_without_typecast.id() != ID_address_of &&
92  (!constant_expr || constant_expr->get_value() != ID_NULL))
93  {
94  return {};
95  }
96 
97  const ssa_exprt *ssa_symbol_expr =
98  expr_try_dynamic_cast<ssa_exprt>(symbol_expr);
99 
100  ssa_exprt l1_expr{*ssa_symbol_expr};
101  l1_expr.remove_level_2();
102  const std::vector<exprt> value_set_elements =
103  value_set.get_value_set(l1_expr, ns);
104 
105  bool constant_found = false;
106 
107  for(const auto &value_set_element : value_set_elements)
108  {
109  if(
110  value_set_element.id() == ID_unknown ||
111  value_set_element.id() == ID_invalid ||
113  to_object_descriptor_expr(value_set_element).root_object()) ||
114  to_object_descriptor_expr(value_set_element).offset().id() == ID_unknown)
115  {
116  // We can't conclude anything about the value-set
117  return {};
118  }
119 
120  if(!constant_found)
121  {
123  value_set_element, false, language_mode))
124  {
125  continue;
126  }
127 
130  value_set_element, symbol_expr, ns);
131 
132  if(skip_typecast(value.pointer) == other_without_typecast)
133  {
134  constant_found = true;
135  // We can't break because we have to make sure we find any instances of
136  // ID_unknown or ID_invalid
137  }
138  }
139  }
140 
141  if(!constant_found)
142  {
143  // The symbol cannot possibly have the value \p other_operand because it
144  // isn't in the symbol's value-set
145  return operation == ID_equal ? make_renamed<L2>(false_exprt{})
146  : make_renamed<L2>(true_exprt{});
147  }
148  else if(value_set_elements.size() == 1)
149  {
150  // The symbol must have the value \p other_operand because it is the only
151  // thing in the symbol's value-set
152  return operation == ID_equal ? make_renamed<L2>(true_exprt{})
153  : make_renamed<L2>(false_exprt{});
154  }
155  else
156  {
157  return {};
158  }
159 }
160 
169  const renamedt<exprt, L2> &renamed_expr,
170  const value_sett &value_set,
171  const irep_idt &language_mode,
172  const namespacet &ns)
173 {
174  const exprt &expr = renamed_expr.get();
175 
176  if(expr.id() != ID_equal && expr.id() != ID_notequal)
177  return {};
178 
179  if(!can_cast_type<pointer_typet>(to_binary_expr(expr).op0().type()))
180  return {};
181 
182  exprt lhs = to_binary_expr(expr).op0(), rhs = to_binary_expr(expr).op1();
184  std::swap(lhs, rhs);
185 
186  const symbol_exprt *symbol_expr_lhs =
187  expr_try_dynamic_cast<symbol_exprt>(lhs);
188 
189  if(!symbol_expr_lhs)
190  return {};
191 
192  if(!goto_symex_is_constantt()(rhs))
193  return {};
194 
196  expr.id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns);
197 }
198 
200  renamedt<exprt, L2> condition,
201  const value_sett &value_set,
202  const irep_idt &language_mode,
203  const namespacet &ns)
204 {
206  condition,
207  [&value_set, &language_mode, &ns](const renamedt<exprt, L2> &expr) {
209  expr, value_set, language_mode, ns);
210  });
211 
212  return condition;
213 }
214 
216 {
217  PRECONDITION(state.reachable);
218 
219  const goto_programt::instructiont &instruction=*state.source.pc;
220 
221  exprt new_guard = clean_expr(instruction.get_condition(), state, false);
222 
223  renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);
224  renamed_guard = try_evaluate_pointer_comparisons(
225  std::move(renamed_guard), state.value_set, language_mode, ns);
227  renamed_guard.simplify(ns);
228  new_guard = renamed_guard.get();
229 
230  if(new_guard.is_false())
231  {
232  target.location(state.guard.as_expr(), state.source);
233 
234  // next instruction
235  symex_transition(state);
236  return; // nothing to do
237  }
238 
239  target.goto_instruction(state.guard.as_expr(), renamed_guard, state.source);
240 
242  !instruction.targets.empty(), "goto should have at least one target");
243 
244  // we only do deterministic gotos for now
246  instruction.targets.size() == 1, "no support for non-deterministic gotos");
247 
248  goto_programt::const_targett goto_target=
249  instruction.get_target();
250 
251  const bool backward = instruction.is_backwards_goto();
252 
253  if(backward)
254  {
255  // is it label: goto label; or while(cond); - popular in SV-COMP
256  if(
258  // label: goto label; or do {} while(cond);
259  (goto_target == state.source.pc ||
260  // while(cond);
261  (instruction.incoming_edges.size() == 1 &&
262  *instruction.incoming_edges.begin() == goto_target &&
263  goto_target->is_goto() && new_guard.is_true())))
264  {
265  // generate assume(false) or a suitable negation if this
266  // instruction is a conditional goto
267  if(new_guard.is_true())
268  symex_assume_l2(state, false_exprt());
269  else
270  symex_assume_l2(state, not_exprt(new_guard));
271 
272  // next instruction
273  symex_transition(state);
274  return;
275  }
276 
277  const auto loop_id =
279 
280  unsigned &unwind = state.call_stack().top().loop_iterations[loop_id].count;
281  unwind++;
282 
283  if(should_stop_unwind(state.source, state.call_stack(), unwind))
284  {
285  // we break the loop
286  loop_bound_exceeded(state, new_guard);
287 
288  // next instruction
289  symex_transition(state);
290  return;
291  }
292 
293  if(new_guard.is_true())
294  {
295  // we continue executing the loop
296  if(check_break(loop_id, unwind))
297  {
298  should_pause_symex = true;
299  }
300  symex_transition(state, goto_target, true);
301  return; // nothing else to do
302  }
303  }
304 
305  // No point executing both branches of an unconditional goto.
306  if(
307  new_guard.is_true() && // We have an unconditional goto, AND
308  // either there are no reachable blocks between us and the target in the
309  // surrounding scope (because state.guard == true implies there is no path
310  // around this GOTO instruction)
311  (state.guard.is_true() ||
312  // or there is another block, but we're doing path exploration so
313  // we're going to skip over it for now and return to it later.
315  {
317  instruction.targets.size() > 0,
318  "Instruction is an unconditional goto with no target: " +
319  instruction.code.pretty());
320  symex_transition(state, instruction.get_target(), true);
321  return;
322  }
323 
324  goto_programt::const_targett new_state_pc, state_pc;
325  symex_targett::sourcet original_source=state.source;
326 
327  if(!backward)
328  {
329  new_state_pc=goto_target;
330  state_pc=state.source.pc;
331  state_pc++;
332 
333  // skip dead instructions
334  if(new_guard.is_true())
335  while(state_pc!=goto_target && !state_pc->is_target())
336  ++state_pc;
337 
338  if(state_pc==goto_target)
339  {
340  symex_transition(state, goto_target, false);
341  return; // nothing else to do
342  }
343  }
344  else
345  {
346  new_state_pc=state.source.pc;
347  new_state_pc++;
348  state_pc=goto_target;
349  }
350 
351  // Normally the next instruction to execute would be state_pc and we save
352  // new_state_pc for later. But if we're executing from a saved state, then
353  // new_state_pc should be the state that we saved from earlier, so let's
354  // execute that instead.
355  if(state.has_saved_jump_target)
356  {
357  INVARIANT(
358  new_state_pc == state.saved_target,
359  "Tried to explore the other path of a branch, but the next "
360  "instruction along that path is not the same as the instruction "
361  "that we saved at the branch point. Saved instruction is " +
362  state.saved_target->code.pretty() +
363  "\nwe were intending "
364  "to explore " +
365  new_state_pc->code.pretty() +
366  "\nthe "
367  "instruction we think we saw on a previous path exploration is " +
368  state_pc->code.pretty());
369  goto_programt::const_targett tmp = new_state_pc;
370  new_state_pc = state_pc;
371  state_pc = tmp;
372 
373  log.debug() << "Resuming from jump target '" << state_pc->source_location
374  << "'" << log.eom;
375  }
376  else if(state.has_saved_next_instruction)
377  {
378  log.debug() << "Resuming from next instruction '"
379  << state_pc->source_location << "'" << log.eom;
380  }
382  {
383  // We should save both the instruction after this goto, and the target of
384  // the goto.
385 
386  path_storaget::patht next_instruction(target, state);
387  next_instruction.state.saved_target = state_pc;
388  next_instruction.state.has_saved_next_instruction = true;
389 
390  path_storaget::patht jump_target(target, state);
391  jump_target.state.saved_target = new_state_pc;
392  jump_target.state.has_saved_jump_target = true;
393  // `forward` tells us where the branch we're _currently_ executing is
394  // pointing to; this needs to be inverted for the branch that we're saving,
395  // so let its truth value for `backwards` be the same as ours for `forward`.
396 
397  log.debug() << "Saving next instruction '"
398  << next_instruction.state.saved_target->source_location << "'"
399  << log.eom;
400  log.debug() << "Saving jump target '"
401  << jump_target.state.saved_target->source_location << "'"
402  << log.eom;
403  path_storage.push(next_instruction);
404  path_storage.push(jump_target);
405 
406  // It is now up to the caller of symex to decide which path to continue
407  // executing. Signal to the caller that states have been pushed (therefore
408  // symex has not yet completed and must be resumed), and bail out.
409  should_pause_symex = true;
410  return;
411  }
412 
413  // put a copy of the current state into the state-queue, to be used by
414  // merge_gotos when we visit new_state_pc
415  framet::goto_state_listt &goto_state_list =
416  state.call_stack().top().goto_state_map[new_state_pc];
417 
418  // On an unconditional GOTO we don't need our state, as it will be overwritten
419  // by merge_goto. Therefore we move it onto goto_state_list instead of copying
420  // as usual.
421  if(new_guard.is_true())
422  {
423  // The move here only moves goto_statet, the base class of goto_symex_statet
424  // and not the entire thing.
425  goto_state_list.emplace_back(state.source, std::move(state));
426 
427  symex_transition(state, state_pc, backward);
428 
430  state.reachable = false;
431  }
432  else
433  {
434  goto_state_list.emplace_back(state.source, state);
435 
436  symex_transition(state, state_pc, backward);
437 
439  {
440  // This doesn't work for --paths (single-path mode) yet, as in multi-path
441  // mode we remove the implied constants at a control-flow merge, but in
442  // single-path mode we don't run merge_gotos.
443  auto &taken_state = backward ? state : goto_state_list.back().second;
444  auto &not_taken_state = backward ? goto_state_list.back().second : state;
445 
447  state,
448  taken_state,
449  not_taken_state,
450  instruction.get_condition(),
451  new_guard,
452  ns);
453  }
454 
455  // produce new guard symbol
456  exprt guard_expr;
457 
458  if(
459  new_guard.id() == ID_symbol ||
460  (new_guard.id() == ID_not &&
461  to_not_expr(new_guard).op().id() == ID_symbol))
462  {
463  guard_expr=new_guard;
464  }
465  else
466  {
467  symbol_exprt guard_symbol_expr =
469  exprt new_rhs = boolean_negate(new_guard);
470 
471  ssa_exprt new_lhs =
472  state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns).get();
473  new_lhs =
474  state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get();
475 
476  guardt guard{true_exprt{}, guard_manager};
477 
479  log.debug(),
480  [this, &new_lhs](messaget::mstreamt &mstream) {
481  mstream << "Assignment to " << new_lhs.get_identifier()
482  << " [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
483  << messaget::eom;
484  });
485 
487  guard.as_expr(),
488  new_lhs, new_lhs, guard_symbol_expr,
489  new_rhs,
490  original_source,
492 
493  guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns).get();
494  }
495 
496  if(state.has_saved_jump_target)
497  {
498  if(!backward)
499  state.guard.add(guard_expr);
500  else
501  state.guard.add(boolean_negate(guard_expr));
502  }
503  else
504  {
505  goto_statet &new_state = goto_state_list.back().second;
506  if(!backward)
507  {
508  new_state.guard.add(guard_expr);
509  state.guard.add(boolean_negate(guard_expr));
510  }
511  else
512  {
513  state.guard.add(guard_expr);
514  new_state.guard.add(boolean_negate(guard_expr));
515  }
516  }
517  }
518 }
519 
521 {
522  PRECONDITION(!state.reachable);
523  // This is like symex_goto, except the state is unreachable. We try to take
524  // some arbitrary choice that maintains the state guard in a reasonable state
525  // in order that it simplifies properly when states are merged (in
526  // merge_gotos). Note we can't try to evaluate the actual GOTO guard because
527  // our constant propagator might be out of date, since we haven't been
528  // executing assign instructions.
529 
530  // If the guard is already false then there's no value in this state; just
531  // carry on and check the next instruction.
532  if(state.guard.is_false())
533  {
534  symex_transition(state);
535  return;
536  }
537 
538  const goto_programt::instructiont &instruction = *state.source.pc;
539  PRECONDITION(instruction.is_goto());
540  goto_programt::const_targett goto_target = instruction.get_target();
541 
542  auto queue_unreachable_state_at_target = [&]() {
543  framet::goto_state_listt &goto_state_list =
544  state.call_stack().top().goto_state_map[goto_target];
545  goto_statet new_state(state.guard_manager);
546  new_state.guard = state.guard;
547  new_state.reachable = false;
548  goto_state_list.emplace_back(state.source, std::move(new_state));
549  };
550 
551  if(instruction.get_condition().is_true())
552  {
553  if(instruction.is_backwards_goto())
554  {
555  // Give up trying to salvage the guard
556  // (this state's guard is squashed, without queueing it at the target)
557  }
558  else
559  {
560  // Take the branch:
561  queue_unreachable_state_at_target();
562  }
563 
564  state.guard.add(false_exprt());
565  }
566  else
567  {
568  // Arbitrarily assume a conditional branch is not-taken, except for when
569  // there's an incoming backedge, when we guess that the taken case is less
570  // likely to lead to that backedge than the not-taken case.
571  bool maybe_loop_head = std::any_of(
572  instruction.incoming_edges.begin(),
573  instruction.incoming_edges.end(),
574  [&instruction](const goto_programt::const_targett predecessor) {
575  return predecessor->location_number > instruction.location_number;
576  });
577 
578  if(instruction.is_backwards_goto() || !maybe_loop_head)
579  {
580  // Assume branch not taken (fall through)
581  }
582  else
583  {
584  // Assume branch taken:
585  queue_unreachable_state_at_target();
586  state.guard.add(false_exprt());
587  }
588  }
589 
590  symex_transition(state);
591 }
592 
593 bool goto_symext::check_break(const irep_idt &loop_id, unsigned unwind)
594 {
595  // dummy implementation
596  return false;
597 }
598 
600 {
601  framet &frame = state.call_stack().top();
602 
603  // first, see if this is a target at all
604  auto state_map_it = frame.goto_state_map.find(state.source.pc);
605 
606  if(state_map_it==frame.goto_state_map.end())
607  return; // nothing to do
608 
609  // we need to merge
610  framet::goto_state_listt &state_list = state_map_it->second;
611 
612  for(auto list_it = state_list.rbegin(); list_it != state_list.rend();
613  ++list_it)
614  {
615  merge_goto(list_it->first, std::move(list_it->second), state);
616  }
617 
618  // clean up to save some memory
619  frame.goto_state_map.erase(state_map_it);
620 }
621 
622 static guardt
624 {
625  // adjust guard, even using guards from unreachable states. This helps to
626  // shrink the state guard if the incoming edge is from a path that was
627  // truncated by config.unwind, config.depth or an assume-false instruction.
628 
629  // Note when an unreachable state contributes its guard, merging it in is
630  // optional, since the formula already implies the unreachable guard is
631  // impossible. Therefore we only integrate it when to do so simplifies the
632  // state guard.
633 
634  // This function can trash either state's guards, since goto_state is dying
635  // and state's guard will shortly be overwritten.
636 
637  if(
638  (goto_state.reachable && state.reachable) ||
639  state.guard.disjunction_may_simplify(goto_state.guard))
640  {
641  state.guard |= goto_state.guard;
642  return std::move(state.guard);
643  }
644  else if(!state.reachable && goto_state.reachable)
645  {
646  return std::move(goto_state.guard);
647  }
648  else
649  {
650  return std::move(state.guard);
651  }
652 }
653 
655  const symex_targett::sourcet &,
656  goto_statet &&goto_state,
657  statet &state)
658 {
659  // check atomic section
660  if(state.atomic_section_id != goto_state.atomic_section_id)
662  "atomic sections differ across branches",
663  state.source.pc->source_location);
664 
665  // Merge guards. Don't write this to `state` yet because we might move
666  // goto_state over it below.
667  guardt new_guard = merge_state_guards(goto_state, state);
668 
669  // Merge constant propagator, value-set etc. only if the incoming state is
670  // reachable:
671  if(goto_state.reachable)
672  {
673  if(!state.reachable)
674  {
675  // Important to note that we're moving into our base class here.
676  // Note this overwrites state.guard, but we restore it below.
677  static_cast<goto_statet &>(state) = std::move(goto_state);
678  }
679  else
680  {
681  // do SSA phi functions
682  phi_function(goto_state, state);
683 
684  // merge value sets
685  state.value_set.make_union(goto_state.value_set);
686 
687  // adjust depth
688  state.depth = std::min(state.depth, goto_state.depth);
689  }
690  }
691 
692  // Save the new state guard
693  state.guard = std::move(new_guard);
694 }
695 
711 static void merge_names(
712  const goto_statet &goto_state,
713  goto_symext::statet &dest_state,
714  const namespacet &ns,
715  const guardt &diff_guard,
716  messaget &log,
717  const bool do_simplify,
718  symex_target_equationt &target,
719  const incremental_dirtyt &dirty,
720  const ssa_exprt &ssa,
721  const unsigned goto_count,
722  const unsigned dest_count)
723 {
724  const irep_idt l1_identifier = ssa.get_identifier();
725  const irep_idt &obj_identifier = ssa.get_object_name();
726 
727  if(obj_identifier == goto_symext::statet::guard_identifier())
728  return; // just a guard, don't bother
729 
730  if(goto_count == dest_count)
731  return; // not at all changed
732 
733  // changed - but only on a branch that is now dead, and the other branch is
734  // uninitialized/invalid
735  if(
736  (!dest_state.reachable && goto_count == 0) ||
737  (!goto_state.reachable && dest_count == 0))
738  {
739  return;
740  }
741 
742  // field sensitivity: only merge on individual fields
743  if(dest_state.field_sensitivity.is_divisible(ssa))
744  return;
745 
746  // shared variables are renamed on every access anyway, we don't need to
747  // merge anything
748  const symbolt &symbol = ns.lookup(obj_identifier);
749 
750  // shared?
751  if(
752  dest_state.atomic_section_id == 0 && dest_state.threads.size() >= 2 &&
753  (symbol.is_shared() || dirty(symbol.name)))
754  {
755  return; // no phi nodes for shared stuff
756  }
757 
758  // don't merge (thread-)locals across different threads, which
759  // may have been introduced by symex_start_thread (and will
760  // only later be removed from level2.current_names by pop_frame
761  // once the thread is executed)
762  const irep_idt level_0 = ssa.get_level_0();
763  if(!level_0.empty() && level_0 != std::to_string(dest_state.source.thread_nr))
764  return;
765 
766  exprt goto_state_rhs = ssa, dest_state_rhs = ssa;
767 
768  {
769  const auto p_it = goto_state.propagation.find(l1_identifier);
770 
771  if(p_it.has_value())
772  goto_state_rhs = *p_it;
773  else
774  to_ssa_expr(goto_state_rhs).set_level_2(goto_count);
775  }
776 
777  {
778  const auto p_it = dest_state.propagation.find(l1_identifier);
779 
780  if(p_it.has_value())
781  dest_state_rhs = *p_it;
782  else
783  to_ssa_expr(dest_state_rhs).set_level_2(dest_count);
784  }
785 
786  exprt rhs;
787 
788  // Don't add a conditional to the assignment when:
789  // 1. Either guard is false, so we can't follow that branch.
790  // 2. Either identifier is of generation zero, and so hasn't been
791  // initialized and therefore an invalid target.
792 
793  // These rules only apply to dynamic objects and locals.
794  if(!dest_state.reachable)
795  rhs = goto_state_rhs;
796  else if(!goto_state.reachable)
797  rhs = dest_state_rhs;
798  else if(goto_count == 0)
799  rhs = dest_state_rhs;
800  else if(dest_count == 0)
801  rhs = goto_state_rhs;
802  else
803  {
804  rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);
805  if(do_simplify)
806  simplify(rhs, ns);
807  }
808 
809  dest_state.record_events.push(false);
810  const ssa_exprt new_lhs =
811  dest_state.assignment(ssa, rhs, ns, true, true).get();
812  dest_state.record_events.pop();
813 
814  log.conditional_output(
815  log.debug(), [ns, &new_lhs](messaget::mstreamt &mstream) {
816  mstream << "Assignment to " << new_lhs.get_identifier() << " ["
817  << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
818  << messaget::eom;
819  });
820 
821  target.assignment(
822  true_exprt(),
823  new_lhs,
824  new_lhs,
825  new_lhs.get_original_expr(),
826  rhs,
827  dest_state.source,
829 }
830 
832  const goto_statet &goto_state,
833  statet &dest_state)
834 {
835  if(
836  goto_state.get_level2().current_names.empty() &&
837  dest_state.get_level2().current_names.empty())
838  return;
839 
840  guardt diff_guard = goto_state.guard;
841  // this gets the diff between the guards
842  diff_guard -= dest_state.guard;
843 
846  dest_state.get_level2().current_names, delta_view, false);
847 
848  for(const auto &delta_item : delta_view)
849  {
850  const ssa_exprt &ssa = delta_item.m.first;
851  unsigned goto_count = delta_item.m.second;
852  unsigned dest_count = !delta_item.is_in_both_maps()
853  ? 0
854  : delta_item.get_other_map_value().second;
855 
856  merge_names(
857  goto_state,
858  dest_state,
859  ns,
860  diff_guard,
861  log,
863  target,
865  ssa,
866  goto_count,
867  dest_count);
868  }
869 
870  delta_view.clear();
872  goto_state.get_level2().current_names, delta_view, false);
873 
874  for(const auto &delta_item : delta_view)
875  {
876  if(delta_item.is_in_both_maps())
877  continue;
878 
879  const ssa_exprt &ssa = delta_item.m.first;
880  unsigned goto_count = 0;
881  unsigned dest_count = delta_item.m.second;
882 
883  merge_names(
884  goto_state,
885  dest_state,
886  ns,
887  diff_guard,
888  log,
890  target,
892  ssa,
893  goto_count,
894  dest_count);
895  }
896 }
897 
899  statet &state,
900  const exprt &guard)
901 {
902  const unsigned loop_number=state.source.pc->loop_number;
903 
904  exprt negated_cond;
905 
906  if(guard.is_true())
907  negated_cond=false_exprt();
908  else
909  negated_cond=not_exprt(guard);
910 
912  {
914  {
915  // Generate VCC for unwinding assertion.
916  vcc(
917  negated_cond,
918  "unwinding assertion loop " + std::to_string(loop_number),
919  state);
920  }
921 
922  // generate unwinding assumption, unless we permit partial loops
923  symex_assume_l2(state, negated_cond);
924 
926  {
927  // add to state guard to prevent further assignments
928  state.guard.add(negated_cond);
929  }
930  }
931 }
932 
934  const symex_targett::sourcet &,
935  const call_stackt &,
936  unsigned)
937 {
938  // by default, we keep going
939  return false;
940 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
guard_exprt
Definition: guard_expr.h:27
sharing_mapt< irep_idt, std::pair< ssa_exprt, std::size_t > >::delta_viewt
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
Definition: sharing_map.h:439
goto_symext::clean_expr
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
Definition: symex_clean_expr.cpp:233
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
can_cast_expr< symbol_exprt >
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:174
goto_symext::symex_assume_l2
void symex_assume_l2(statet &, const exprt &cond)
Definition: symex_main.cpp:222
symex_configt::self_loops_to_assumptions
bool self_loops_to_assumptions
Definition: symex_config.h:29
sharing_mapt::get_delta_view
void get_delta_view(const sharing_mapt &other, delta_viewt &delta_view, const bool only_common=true) const
Get a delta view of the elements in the map.
Definition: sharing_map.h:936
value_set_dereferencet::valuet
Return value for build_reference_to; see that method for documentation.
Definition: value_set_dereference.h:70
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:218
symex_configt::partial_loops
bool partial_loops
Definition: symex_config.h:35
goto_statet::apply_condition
void apply_condition(const exprt &condition, const goto_symex_statet &previous_state, const namespacet &ns)
Given a condition that must hold on this path, propagate as much knowledge as possible.
Definition: goto_state.cpp:42
merge_names
static void merge_names(const goto_statet &goto_state, goto_symext::statet &dest_state, const namespacet &ns, const guardt &diff_guard, messaget &log, const bool do_simplify, symex_target_equationt &target, const incremental_dirtyt &dirty, const ssa_exprt &ssa, const unsigned goto_count, const unsigned dest_count)
Helper function for phi_function which merges the names of an identifier for two different states.
Definition: symex_goto.cpp:711
goto_symext::symex_unreachable_goto
void symex_unreachable_goto(statet &state)
Symbolically execute a GOTO instruction in the context of unreachable code.
Definition: symex_goto.cpp:520
ssa_exprt::remove_level_2
void remove_level_2()
goto_symex_statet::assignment
NODISCARD renamedt< ssa_exprt, L2 > assignment(ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
Definition: goto_symex_state.cpp:76
ssa_exprt::get_level_0
const irep_idt get_level_0() const
Definition: ssa_expr.h:63
L1
@ L1
Definition: renamed.h:18
goto_symext::try_filter_value_sets
void try_filter_value_sets(goto_symex_statet &state, exprt condition, const value_sett &original_value_set, value_sett *jump_taken_value_set, value_sett *jump_not_taken_value_set, const namespacet &ns)
Try to filter value sets based on whether possible values of a pointer-typed symbol make the conditio...
Definition: symex_main.cpp:784
goto_symex_statet::guard_identifier
static irep_idt guard_identifier()
Definition: goto_symex_state.h:141
goto_statet::reachable
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition: goto_state.h:58
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:492
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:43
goto_symext::target
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:264
value_set_dereference.h
Pointer Dereferencing.
goto_symex_statet::has_saved_jump_target
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
Definition: goto_symex_state.h:219
goto_symext::path_storage
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:797
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2087
renamedt::simplify
void simplify(const namespacet &ns)
Definition: renamed.h:39
goto_symex_statet::guard_manager
guard_managert & guard_manager
Definition: goto_symex_state.h:72
goto_symext::guard_manager
guard_managert & guard_manager
Used to create guards.
Definition: goto_symex.h:261
symex_targett::sourcet::thread_nr
unsigned thread_nr
Definition: symex_target.h:39
invariant.h
value_set_dereferencet::should_ignore_value
static bool should_ignore_value(const exprt &what, bool exclude_null_derefs, const irep_idt &language_mode)
Determine whether possible alias what should be ignored when replacing a pointer by its referees.
Definition: value_set_dereference.cpp:407
value_sett
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:45
exprt
Base class for all expressions.
Definition: expr.h:54
goto_symext::merge_gotos
void merge_gotos(statet &state)
Merge all branches joining at the current program point.
Definition: symex_goto.cpp:599
ssa_exprt::get_object_name
irep_idt get_object_name() const
guard_exprt::is_true
bool is_true() const
Definition: guard_expr.h:63
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:64
goto_symex_statet::rename_ssa
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
bool_typet
The Boolean type.
Definition: std_types.h:37
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:371
messaget::eom
static eomt eom
Definition: message.h:297
guardt
guard_exprt guardt
Definition: guard.h:27
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
call_stackt
Definition: call_stack.h:15
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
renamedt::get
const underlyingt & get() const
Definition: renamed.h:34
goto_symex_is_constant.h
GOTO Symex constant propagation.
goto_symext::should_stop_unwind
virtual bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind)
Determine whether to unwind a loop.
Definition: symex_goto.cpp:933
value_sett::make_union
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
Definition: value_set.cpp:285
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
incorrect_goto_program_exceptiont
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Definition: exception_utils.h:90
goto_statet::propagation
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:67
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
is_failed_symbol
bool is_failed_symbol(const exprt &expr)
Return true if, and only if, expr is the result of failed dereferencing.
Definition: add_failed_symbols.h:39
goto_programt::loop_id
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:726
goto_symext::log
messaget log
The messaget to write log messages to.
Definition: goto_symex.h:276
symex_target_equationt::location
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
Definition: symex_target_equation.cpp:173
to_object_descriptor_expr
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: pointer_expr.h:88
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
goto_symex_statet::threads
std::vector< threadt > threads
Definition: goto_symex_state.h:198
goto_symext::merge_goto
virtual void merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state)
Merge a single branch, the symbolic state of which is held in goto_state, into the current overall sy...
Definition: symex_goto.cpp:654
goto_symex_statet::call_stack
call_stackt & call_stack()
Definition: goto_symex_state.h:147
goto_symex_statet::has_saved_next_instruction
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
Definition: goto_symex_state.h:223
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
call_stackt::top
framet & top()
Definition: call_stack.h:17
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
goto_symext::symex_goto
virtual void symex_goto(statet &state)
Symbolically execute a GOTO instruction.
Definition: symex_goto.cpp:215
value_set_dereferencet::valuet::pointer
exprt pointer
Definition: value_set_dereference.h:73
path_storaget::push
virtual void push(const patht &)=0
Add a path to resume to the storage.
goto_statet::depth
unsigned depth
Distance from entry.
Definition: goto_state.h:35
selectively_mutate
void selectively_mutate(renamedt< exprt, level > &renamed, typename renamedt< exprt, level >::mutator_functiont get_mutated_expr)
This permits replacing subexpressions of the renamed value, so long as each replacement is consistent...
Definition: renamed.h:89
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:183
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
value_sett::get_value_set
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
Definition: value_set.cpp:352
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:49
guard_exprt::add
void add(const exprt &expr)
Definition: guard_expr.cpp:40
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
symex_configt::doing_path_exploration
bool doing_path_exploration
Definition: symex_config.h:23
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:128
symex_configt::unwinding_assertions
bool unwinding_assertions
Definition: symex_config.h:33
goto_symex.h
Symbolic Execution.
goto_statet::guard
guardt guard
Definition: goto_state.h:54
framet::loop_iterations
std::unordered_map< irep_idt, loop_infot > loop_iterations
Definition: frame.h:71
goto_programt::instructiont::is_backwards_goto
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:508
try_evaluate_pointer_comparison
static optionalt< renamedt< exprt, L2 > > try_evaluate_pointer_comparison(const irep_idt &operation, const symbol_exprt &symbol_expr, const exprt &other_operand, const value_sett &value_set, const irep_idt language_mode, const namespacet &ns)
Try to evaluate a simple pointer comparison.
Definition: symex_goto.cpp:78
goto_symext::phi_function
void phi_function(const goto_statet &goto_state, statet &dest_state)
Merge the SSA assignments from goto_state into dest_state.
Definition: symex_goto.cpp:831
symex_configt::simplify_opt
bool simplify_opt
Definition: symex_config.h:31
sharing_mapt::empty
bool empty() const
Check if map is empty.
Definition: sharing_map.h:360
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2524
guard_exprt::disjunction_may_simplify
bool disjunction_may_simplify(const guard_exprt &other_guard)
Returns true if operator|= with other_guard may result in a simpler expression.
Definition: guard_expr.cpp:127
path_storaget::dirty
incremental_dirtyt dirty
Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...
Definition: path_storage.h:116
symbolt::is_shared
bool is_shared() const
Definition: symbol.h:95
irept::id
const irep_idt & id() const
Definition: irep.h:407
dstringt::empty
bool empty() const
Definition: dstring.h:88
false_exprt
The Boolean constant false.
Definition: std_expr.h:2726
framet
Stack frames – these are used for function calls and for exceptions.
Definition: frame.h:21
goto_symex_is_constantt
Definition: goto_symex_is_constant.h:19
guard_exprt::is_false
bool is_false() const
Definition: guard_expr.h:68
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
path_storaget::patht
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:42
goto_statet
Container for data that varies per program point, e.g.
Definition: goto_state.h:32
symex_transition
void symex_transition(goto_symext::statet &state)
Transition to the next instruction, which increments the internal program counter and initializes the...
Definition: symex_main.cpp:150
goto_symex_statet::field_sensitivity
field_sensitivityt field_sensitivity
Definition: goto_symex_state.h:124
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
goto_programt::instructiont::is_goto
bool is_goto() const
Definition: goto_program.h:429
simplify_expr.h
framet::goto_state_listt
std::list< std::pair< symex_targett::sourcet, goto_statet > > goto_state_listt
Definition: frame.h:24
can_cast_type< pointer_typet >
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: std_types.h:1520
goto_symext::ns
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:256
expr_util.h
Deprecated expression utility functions.
symex_targett::assignment_typet::PHI
@ PHI
symex_target_equationt::goto_instruction
virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)
Record a goto instruction.
Definition: symex_target_equation.cpp:302
goto_symext::check_break
virtual bool check_break(const irep_idt &loop_id, unsigned unwind)
Defines condition for interrupting symbolic execution for a specific loop.
Definition: symex_goto.cpp:593
ssa_exprt::set_level_2
void set_level_2(std::size_t i)
symex_level2t::current_names
symex_renaming_levelt current_names
Definition: renaming_level.h:77
goto_symext::language_mode
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:239
field_sensitivityt::is_divisible
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
Definition: field_sensitivity.cpp:350
goto_programt::instructiont::incoming_edges
std::set< targett > incoming_edges
Definition: goto_program.h:399
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2067
path_storaget::patht::state
goto_symex_statet state
Definition: path_storage.h:44
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_statet::atomic_section_id
unsigned atomic_section_id
Threads.
Definition: goto_state.h:72
symex_configt::constant_propagation
bool constant_propagation
Definition: symex_config.h:27
goto_statet::get_level2
const symex_level2t & get_level2() const
Definition: goto_state.h:41
goto_symext::vcc
virtual void vcc(const exprt &, const std::string &msg, statet &)
Definition: symex_main.cpp:185
messaget::conditional_output
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
Definition: message.cpp:138
goto_symext::symex_config
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:183
value_set_dereferencet::build_reference_to
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
Definition: value_set_dereference.cpp:444
goto_symex_statet::record_events
std::stack< bool > record_events
Definition: goto_symex_state.h:212
symex_targett::assignment_typet::GUARD
@ GUARD
messaget::mstreamt
Definition: message.h:224
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:551
goto_symext::loop_bound_exceeded
virtual void loop_bound_exceeded(statet &state, const exprt &guard)
Definition: symex_goto.cpp:898
goto_symex_statet::rename
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
goto_symex_statet::saved_target
goto_programt::const_targett saved_target
Definition: goto_symex_state.h:216
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38
messaget::debug
mstreamt & debug() const
Definition: message.h:429
framet::goto_state_map
std::map< goto_programt::const_targett, goto_state_listt > goto_state_map
Definition: frame.h:28
add_failed_symbols.h
Pointer Dereferencing.
goto_symext::apply_goto_condition
void apply_goto_condition(goto_symex_statet &current_state, goto_statet &jump_taken_state, goto_statet &jump_not_taken_state, const exprt &original_guard, const exprt &new_guard, const namespacet &ns)
Propagate constants and points-to information implied by a GOTO condition.
Definition: symex_goto.cpp:27
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
incremental_dirtyt
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
Definition: dirty.h:119
symex_targett::sourcet::function_id
irep_idt function_id
Definition: symex_target.h:40
true_exprt
The Boolean constant true.
Definition: std_expr.h:2717
goto_programt::instructiont::get_condition
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:350
constant_exprt
A constant literal expression.
Definition: std_expr.h:2668
merge_state_guards
static guardt merge_state_guards(goto_statet &goto_state, goto_symex_statet &state)
Definition: symex_goto.cpp:623
binary_exprt::op1
exprt & op1()
Definition: expr.h:106
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
std_expr.h
API to expression classes.
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2676
goto_statet::value_set
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:47
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::instructiont::get_target
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:375
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:27
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
try_evaluate_pointer_comparisons
renamedt< exprt, L2 > try_evaluate_pointer_comparisons(renamedt< exprt, L2 > condition, const value_sett &value_set, const irep_idt &language_mode, const namespacet &ns)
Try to evaluate pointer comparisons where they can be trivially determined using the value-set.
Definition: symex_goto.cpp:199
goto_symext::should_pause_symex
bool should_pause_symex
Set when states are pushed onto the workqueue If this flag is set at the end of a symbolic execution ...
Definition: goto_symex.h:165
not_exprt
Boolean negation.
Definition: std_expr.h:2042
symex_target_equationt::assignment
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 local variable.
Definition: symex_target_equation.cpp:117