CBMC
symex_main.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 <util/exception_utils.h>
13 #include <util/expr_iterator.h>
14 #include <util/expr_util.h>
15 #include <util/format.h>
16 #include <util/format_expr.h>
17 #include <util/invariant.h>
18 #include <util/magic.h>
19 #include <util/mathematical_expr.h>
20 #include <util/replace_symbol.h>
21 #include <util/std_expr.h>
22 
24 
25 #include "goto_symex.h"
26 #include "path_storage.h"
27 
28 #include <memory>
29 
31  : max_depth(options.get_unsigned_int_option("depth")),
32  doing_path_exploration(options.is_set("paths")),
33  allow_pointer_unsoundness(
34  options.get_bool_option("allow-pointer-unsoundness")),
35  constant_propagation(options.get_bool_option("propagation")),
36  self_loops_to_assumptions(
37  options.get_bool_option("self-loops-to-assumptions")),
38  simplify_opt(options.get_bool_option("simplify")),
39  unwinding_assertions(options.get_bool_option("unwinding-assertions")),
40  partial_loops(options.get_bool_option("partial-loops")),
41  havoc_undefined_functions(
42  options.get_bool_option("havoc-undefined-functions")),
43  run_validation_checks(options.get_bool_option("validate-ssa-equation")),
44  show_symex_steps(options.get_bool_option("show-goto-symex-steps")),
45  show_points_to_sets(options.get_bool_option("show-points-to-sets")),
46  max_field_sensitivity_array_size(
47  options.is_set("no-array-field-sensitivity")
48  ? 0
49  : options.is_set("max-field-sensitivity-array-size")
50  ? options.get_unsigned_int_option(
51  "max-field-sensitivity-array-size")
53  complexity_limits_active(
54  options.get_signed_int_option("symex-complexity-limit") > 0),
55  cache_dereferences{options.get_bool_option("symex-cache-dereferences")}
56 {
57 }
58 
62 static void pop_exited_loops(
64  std::vector<framet::active_loop_infot> &active_loops)
65 {
66  while(!active_loops.empty())
67  {
68  if(!active_loops.back().loop.contains(to))
69  active_loops.pop_back();
70  else
71  break;
72  }
73 }
74 
76  goto_symext::statet &state,
78  bool is_backwards_goto)
79 {
80  if(!state.call_stack().empty())
81  {
82  // initialize the loop counter of any loop we are newly entering
83  // upon this transition; we are entering a loop if
84  // 1. the transition from state.source.pc to "to" is not a backwards goto
85  // or
86  // 2. we are arriving from an outer loop
87 
88  // TODO: This should all be replaced by natural loop analysis.
89  // This is because the way we detect loops is pretty imprecise.
90 
91  framet &frame = state.call_stack().top();
92  const goto_programt::instructiont &instruction=*to;
93  for(const auto &i_e : instruction.incoming_edges)
94  {
95  if(
96  i_e->is_backwards_goto() && i_e->get_target() == to &&
97  (!is_backwards_goto ||
98  state.source.pc->location_number > i_e->location_number))
99  {
100  const auto loop_id =
102  auto &current_loop_info = frame.loop_iterations[loop_id];
103  current_loop_info.count = 0;
104 
105  // We've found a loop, put it on the stack and say it's our current
106  // active loop.
107  if(
108  frame.loops_info && frame.loops_info->loop_map.find(to) !=
109  frame.loops_info->loop_map.end())
110  {
111  frame.active_loops.emplace_back(frame.loops_info->loop_map[to]);
112  }
113  }
114  }
115 
116  // Only do this if we have active loop analysis going.
117  if(!frame.active_loops.empty())
118  {
119  // Otherwise if we find we're transitioning out of a loop, make sure
120  // to remove any loops we're not currently iterating over.
121 
122  // Match the do-while pattern.
123  if(
124  state.source.pc->is_backwards_goto() &&
125  state.source.pc->location_number < to->location_number)
126  {
127  pop_exited_loops(to, frame.active_loops);
128  }
129 
130  // Match for-each or while.
131  for(const auto &incoming_edge : state.source.pc->incoming_edges)
132  {
133  if(
134  incoming_edge->is_backwards_goto() &&
135  incoming_edge->location_number < to->location_number)
136  {
137  pop_exited_loops(to, frame.active_loops);
138  }
139  }
140  }
141  }
142 
143  state.source.pc=to;
144 }
145 
147 {
149  ++next;
150  symex_transition(state, next, false);
151 }
152 
154  const goto_programt::instructiont &instruction,
155  statet &state)
156 {
157  exprt condition = clean_expr(instruction.condition(), state, false);
158 
159  // First, push negations in and perhaps convert existential quantifiers into
160  // universals:
161  if(has_subexpr(condition, ID_exists) || has_subexpr(condition, ID_forall))
162  do_simplify(condition);
163 
164  // Second, L2-rename universal quantifiers:
165  if(has_subexpr(condition, ID_forall))
166  rewrite_quantifiers(condition, state);
167 
168  // now rename, enables propagation
169  exprt l2_condition = state.rename(std::move(condition), ns).get();
170 
171  // now try simplifier on it
172  do_simplify(l2_condition);
173 
174  std::string msg = id2string(instruction.source_location().get_comment());
175  if(msg.empty())
176  msg = "assertion";
177 
178  vcc(
179  l2_condition, instruction.source_location().get_property_id(), msg, state);
180 }
181 
183  const exprt &condition,
184  const irep_idt &property_id,
185  const std::string &msg,
186  statet &state)
187 {
188  state.total_vccs++;
190 
191  if(condition.is_true())
192  return;
193 
194  const exprt guarded_condition = state.guard.guard_expr(condition);
195 
196  state.remaining_vccs++;
198  state.guard.as_expr(), guarded_condition, property_id, msg, state.source);
199 }
200 
201 void goto_symext::symex_assume(statet &state, const exprt &cond)
202 {
203  exprt simplified_cond = clean_expr(cond, state, false);
204  simplified_cond = state.rename(std::move(simplified_cond), ns).get();
205  do_simplify(simplified_cond);
206 
207  // It would be better to call try_filter_value_sets after apply_condition,
208  // but it is not currently possible. See the comment at the beginning of
209  // \ref apply_goto_condition for more information.
210 
212  state, cond, state.value_set, &state.value_set, nullptr, ns);
213 
214  // apply_condition must come after rename because it might change the
215  // constant propagator and the value-set and we read from those in rename
216  state.apply_condition(simplified_cond, state, ns);
217 
218  symex_assume_l2(state, simplified_cond);
219 }
220 
221 void goto_symext::symex_assume_l2(statet &state, const exprt &cond)
222 {
223  if(cond.is_true())
224  return;
225 
226  if(cond.is_false())
227  state.reachable = false;
228 
229  // we are willing to re-write some quantified expressions
230  exprt rewritten_cond = cond;
231  if(has_subexpr(rewritten_cond, ID_exists))
232  rewrite_quantifiers(rewritten_cond, state);
233 
234  if(state.threads.size()==1)
235  {
236  exprt tmp = state.guard.guard_expr(rewritten_cond);
237  target.assumption(state.guard.as_expr(), tmp, state.source);
238  }
239  // symex_target_equationt::convert_assertions would fail to
240  // consider assumptions of threads that have a thread-id above that
241  // of the thread containing the assertion:
242  // T0 T1
243  // x=0; assume(x==1);
244  // assert(x!=42); x=42;
245  else
246  state.guard.add(rewritten_cond);
247 
248  if(state.atomic_section_id!=0 &&
249  state.guard.is_false())
250  symex_atomic_end(state);
251 }
252 
254 {
255  const bool is_assert = state.source.pc->is_assert();
256 
257  if(
258  (is_assert && expr.id() == ID_forall) ||
259  (!is_assert && expr.id() == ID_exists))
260  {
261  // for assertions e can rewrite "forall X. P" to "P", and
262  // for assumptions we can rewrite "exists X. P" to "P"
263  // we keep the quantified variable unique by means of L2 renaming
264  auto &quant_expr = to_quantifier_expr(expr);
265  symbol_exprt tmp0 =
266  to_symbol_expr(to_ssa_expr(quant_expr.symbol()).get_original_expr());
267  symex_decl(state, tmp0);
268  instruction_local_symbols.push_back(tmp0);
269  exprt tmp = quant_expr.where();
270  rewrite_quantifiers(tmp, state);
271  quant_expr.swap(tmp);
272  }
273  else if(expr.id() == ID_or || expr.id() == ID_and)
274  {
275  for(auto &op : expr.operands())
276  rewrite_quantifiers(op, state);
277  }
278 }
279 
280 static void
281 switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb)
282 {
283  PRECONDITION(state.source.thread_nr < state.threads.size());
284  PRECONDITION(thread_nb < state.threads.size());
285 
286  // save PC
287  state.threads[state.source.thread_nr].pc = state.source.pc;
288  state.threads[state.source.thread_nr].atomic_section_id =
289  state.atomic_section_id;
290 
291  // get new PC
292  state.source.thread_nr = thread_nb;
293  state.source.pc = state.threads[thread_nb].pc;
294  state.source.function_id = state.threads[thread_nb].function_id;
295 
296  state.guard = state.threads[thread_nb].guard;
297  // A thread's initial state is certainly reachable:
298  state.reachable = true;
299 }
300 
302  statet &state, const get_goto_functiont &get_goto_function)
303 {
305 
306  _total_vccs = state.total_vccs;
308 
310  return;
311 
312  // is there another thread to execute?
313  if(state.call_stack().empty() &&
314  state.source.thread_nr+1<state.threads.size())
315  {
316  unsigned t=state.source.thread_nr+1;
317 #if 0
318  std::cout << "********* Now executing thread " << t << '\n';
319 #endif
320  switch_to_thread(state, t);
321  symex_transition(state, state.source.pc, false);
322  }
323 }
324 
326  statet &state,
327  const get_goto_functiont &get_goto_function)
328 {
329  // resets the namespace to only wrap a single symbol table, and does so upon
330  // destruction of an object of this type; instantiating the type is thus all
331  // that's needed to achieve a reset upon exiting this method
332  struct reset_namespacet
333  {
334  explicit reset_namespacet(namespacet &ns) : ns(ns)
335  {
336  }
337 
338  ~reset_namespacet()
339  {
340  // Get symbol table 1, the outer symbol table from the GOTO program
341  const symbol_table_baset &st = ns.get_symbol_table();
342  // Move a new namespace containing this symbol table over the top of the
343  // current one
344  ns = namespacet(st);
345  }
346 
347  namespacet &ns;
348  };
349 
350  // We'll be using ns during symbolic execution and it needs to know
351  // about the names minted in `state`, so make it point both to
352  // `state`'s symbol table and the symbol table of the original
353  // goto-program.
355 
356  // whichever way we exit this method, reset the namespace back to a sane state
357  // as state.symbol_table might go out of scope
358  reset_namespacet reset_ns(ns);
359 
360  PRECONDITION(state.call_stack().top().end_of_function->is_end_function());
361 
364  return state.symbol_table;
365 
366  while(!state.call_stack().empty())
367  {
368  state.has_saved_jump_target = false;
369  state.has_saved_next_instruction = false;
372  return state.symbol_table;
373  }
374 
375  // Clients may need to construct a namespace with both the names in
376  // the original goto-program and the names generated during symbolic
377  // execution, so return the names generated through symbolic execution
378  return state.symbol_table;
379 }
380 
382  const get_goto_functiont &get_goto_function,
383  const statet &saved_state,
384  symex_target_equationt *const saved_equation)
385 {
386  // saved_state contains a pointer to a symex_target_equationt that is
387  // almost certainly stale. This is because equations are owned by bmcts,
388  // and we construct a new bmct for every path that we execute. We're on a
389  // new path now, so the old bmct and the equation that it owned have now
390  // been deallocated. So, construct a new state from the old one, and make
391  // its equation member point to the (valid) equation passed as an argument.
392  statet state(saved_state, saved_equation);
393 
394  // Do NOT do the same initialization that `symex_with_state` does for a
395  // fresh state, as that would clobber the saved state's program counter
396  return symex_with_state(state, get_goto_function);
397 }
398 
399 std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
400  const get_goto_functiont &get_goto_function)
401 {
402  const irep_idt entry_point_id = goto_functionst::entry_point();
403 
404  const goto_functionst::goto_functiont *start_function;
405  try
406  {
407  start_function = &get_goto_function(entry_point_id);
408  }
409  catch(const std::out_of_range &)
410  {
411  throw unsupported_operation_exceptiont("the program has no entry point");
412  }
413 
414  // Get our path_storage pointer because this state will live beyond
415  // this instance of goto_symext, so we can't take the reference directly.
416  auto *storage = &path_storage;
417 
418  // create and prepare the state
419  auto state = std::make_unique<statet>(
420  symex_targett::sourcet(entry_point_id, start_function->body),
424  [storage](const irep_idt &id) { return storage->get_unique_l2_index(id); });
425 
426  CHECK_RETURN(!state->threads.empty());
427  CHECK_RETURN(!state->call_stack().empty());
428 
430  std::prev(start_function->body.instructions.end());
431  state->call_stack().top().end_of_function = limit;
432  state->call_stack().top().calling_location.pc =
433  state->call_stack().top().end_of_function;
434  state->call_stack().top().hidden_function = start_function->is_hidden();
435 
436  state->symex_target = &target;
437 
438  state->run_validation_checks = symex_config.run_validation_checks;
439 
440  // initialize support analyses
441  auto emplace_safe_pointers_result =
442  path_storage.safe_pointers.emplace(entry_point_id, local_safe_pointerst{});
443  if(emplace_safe_pointers_result.second)
444  emplace_safe_pointers_result.first->second(start_function->body);
445 
447  entry_point_id, *start_function);
448  state->dirty = &path_storage.dirty;
449 
450  // Only enable loop analysis when complexity is enabled.
452  {
453  // Set initial loop analysis.
454  path_storage.add_function_loops(entry_point_id, start_function->body);
455  state->call_stack().top().loops_info =
456  path_storage.get_loop_analysis(entry_point_id);
457  }
458 
459  // make the first step onto the instruction pointed to by the initial program
460  // counter
461  symex_transition(*state, state->source.pc, false);
462 
463  return state;
464 }
465 
467  const get_goto_functiont &get_goto_function,
468  const shadow_memory_field_definitionst &fields)
469 {
471  // Initialize declared shadow memory fields
472  state->shadow_memory.fields = fields;
473 
474  return symex_with_state(*state, get_goto_function);
475 }
476 
478  const get_goto_functiont &get_goto_function,
479  symbol_table_baset &new_symbol_table,
480  const shadow_memory_field_definitionst &fields)
481 {
483  // Initialize declared shadow memory fields
484  state->shadow_memory.fields = fields;
485 
486  path_storaget::patht entry_point_start(target, *state);
487  entry_point_start.state.saved_target = state->source.pc;
488  entry_point_start.state.has_saved_next_instruction = true;
489 
490  path_storage.push(entry_point_start);
491 }
492 
495 {
496  return [&goto_model](
497  const irep_idt &id) -> const goto_functionst::goto_functiont & {
498  return goto_model.get_goto_function(id);
499  };
500 }
501 
504 {
505  log.status() << source.function_id
506  << " location number: " << source.pc->location_number;
507 
508  return log.status();
509 }
510 
512 {
513  // If we're showing the route, begin outputting debug info, and don't print
514  // instructions we don't run.
515 
516  // We also skip dead instructions as they don't add much to step-based
517  // debugging and if there's no code block at this point.
518  if(
520  state.source.pc->type() == DEAD ||
521  (state.source.pc->code().is_nil() &&
522  state.source.pc->type() != END_FUNCTION))
523  {
524  return;
525  }
526 
527  if(state.source.pc->code().is_not_nil())
528  {
529  auto guard_expression = state.guard.as_expr();
530  std::size_t size = 0;
531  for(auto it = guard_expression.depth_begin();
532  it != guard_expression.depth_end();
533  ++it)
534  {
535  size++;
536  }
537 
538  log.status() << "[Guard size: " << size << "] "
539  << format(state.source.pc->code());
540 
541  if(
542  state.source.pc->source_location().is_not_nil() &&
543  !state.source.pc->source_location().get_java_bytecode_index().empty())
544  {
545  log.status()
546  << " bytecode index: "
547  << state.source.pc->source_location().get_java_bytecode_index();
548  }
549 
550  log.status() << messaget::eom;
551  }
552 
553  // Print the method we're returning too.
554  const auto &call_stack = state.threads[state.source.thread_nr].call_stack;
555  if(state.source.pc->type() == END_FUNCTION)
556  {
557  log.status() << messaget::eom;
558 
559  if(!call_stack.empty())
560  {
561  log.status() << "Returning to: ";
562  print_callstack_entry(call_stack.back().calling_location)
563  << messaget::eom;
564  }
565 
566  log.status() << messaget::eom;
567  }
568 
569  // On a function call print the entire call stack.
570  if(state.source.pc->type() == FUNCTION_CALL)
571  {
572  log.status() << messaget::eom;
573 
574  if(!call_stack.empty())
575  {
576  log.status() << "Call stack:" << messaget::eom;
577 
578  for(auto &frame : call_stack)
579  {
580  print_callstack_entry(frame.calling_location) << messaget::eom;
581  }
582 
584 
585  // Add the method we're about to enter with no location number.
586  log.status() << format(state.source.pc->call_function()) << messaget::eom
587  << messaget::eom;
588  }
589  }
590 }
591 
594  const get_goto_functiont &get_goto_function,
595  statet &state)
596 {
597  // Print debug statements if they've been enabled.
598  print_symex_step(state);
601 }
602 
604  const get_goto_functiont &get_goto_function,
605  statet &state)
606 {
607  PRECONDITION(!state.threads.empty());
608  PRECONDITION(!state.call_stack().empty());
609 
610  const goto_programt::instructiont &instruction=*state.source.pc;
611 
613  merge_gotos(state);
614 
615  // depth exceeded?
616  if(state.depth > symex_config.max_depth)
617  {
618  // Rule out this path:
619  symex_assume_l2(state, false_exprt());
620  }
621  state.depth++;
622 
623  // actually do instruction
624  switch(instruction.type())
625  {
626  case SKIP:
627  if(state.reachable)
628  target.location(state.guard.as_expr(), state.source);
629  symex_transition(state);
630  break;
631 
632  case END_FUNCTION:
633  // do even if !state.reachable to clear out frame created
634  // in symex_start_thread
635  symex_end_of_function(state);
636  symex_transition(state);
637  break;
638 
639  case LOCATION:
640  if(state.reachable)
641  target.location(state.guard.as_expr(), state.source);
642  symex_transition(state);
643  break;
644 
645  case GOTO:
646  if(state.reachable)
647  symex_goto(state);
648  else
649  symex_unreachable_goto(state);
650  break;
651 
652  case ASSUME:
653  if(state.reachable)
654  symex_assume(state, instruction.condition());
655  symex_transition(state);
656  break;
657 
658  case ASSERT:
659  if(state.reachable && !ignore_assertions)
660  symex_assert(instruction, state);
661  symex_transition(state);
662  break;
663 
664  case SET_RETURN_VALUE:
665  if(state.reachable)
666  symex_set_return_value(state, instruction.return_value());
667  symex_transition(state);
668  break;
669 
670  case ASSIGN:
671  if(state.reachable)
672  symex_assign(state, instruction.assign_lhs(), instruction.assign_rhs());
673 
674  symex_transition(state);
675  break;
676 
677  case FUNCTION_CALL:
678  if(state.reachable)
679  symex_function_call(get_goto_function, state, instruction);
680  else
681  symex_transition(state);
682  break;
683 
684  case OTHER:
685  if(state.reachable)
686  symex_other(state);
687  symex_transition(state);
688  break;
689 
690  case DECL:
691  if(state.reachable)
692  symex_decl(state);
693  symex_transition(state);
694  break;
695 
696  case DEAD:
697  symex_dead(state);
698  symex_transition(state);
699  break;
700 
701  case START_THREAD:
702  symex_start_thread(state);
703  symex_transition(state);
704  break;
705 
706  case END_THREAD:
707  // behaves like assume(0);
708  if(state.reachable)
709  state.reachable = false;
710  symex_transition(state);
711  break;
712 
713  case ATOMIC_BEGIN:
714  symex_atomic_begin(state);
715  symex_transition(state);
716  break;
717 
718  case ATOMIC_END:
719  symex_atomic_end(state);
720  symex_transition(state);
721  break;
722 
723  case CATCH:
724  symex_catch(state);
725  symex_transition(state);
726  break;
727 
728  case THROW:
729  symex_throw(state);
730  symex_transition(state);
731  break;
732 
733  case NO_INSTRUCTION_TYPE:
734  throw unsupported_operation_exceptiont("symex got NO_INSTRUCTION");
735 
736  case INCOMPLETE_GOTO:
737  DATA_INVARIANT(false, "symex got unexpected instruction type");
738  }
739 
740  complexity_violationt complexity_result =
742  if(complexity_result != complexity_violationt::NONE)
743  complexity_module.run_transformations(complexity_result, state);
744 }
745 
747 {
748  for(const auto &symbol_expr : instruction_local_symbols)
749  symex_dead(state, symbol_expr);
751 }
752 
758 static std::optional<symbol_exprt>
760 {
761  std::optional<symbol_exprt> return_value;
762  for(auto it = expr.depth_cbegin(); it != expr.depth_cend(); ++it)
763  {
764  const symbol_exprt *symbol_expr = expr_try_dynamic_cast<symbol_exprt>(*it);
765  if(symbol_expr && can_cast_type<pointer_typet>(symbol_expr->type()))
766  {
767  // If we already have a potential return value, check if it is the same
768  // symbol, and return an empty std::optional if not
769  if(return_value && *symbol_expr != *return_value)
770  {
771  return {};
772  }
773  return_value = *symbol_expr;
774  }
775  }
776 
777  // Either expr contains no pointer-typed symbols or it contains one unique
778  // pointer-typed symbol, possibly repeated multiple times
779  return return_value;
780 }
781 
783  goto_symex_statet &state,
784  exprt condition,
785  const value_sett &original_value_set,
786  value_sett *jump_taken_value_set,
787  value_sett *jump_not_taken_value_set,
788  const namespacet &ns)
789 {
790  condition = state.rename<L1>(std::move(condition), ns).get();
791 
792  std::optional<symbol_exprt> symbol_expr =
794 
795  if(!symbol_expr)
796  {
797  return;
798  }
799 
800  const pointer_typet &symbol_type = to_pointer_type(symbol_expr->type());
801 
802  const std::vector<exprt> value_set_elements =
803  original_value_set.get_value_set(*symbol_expr, ns);
804 
805  std::unordered_set<exprt, irep_hash> erase_from_jump_taken_value_set;
806  std::unordered_set<exprt, irep_hash> erase_from_jump_not_taken_value_set;
807  erase_from_jump_taken_value_set.reserve(value_set_elements.size());
808  erase_from_jump_not_taken_value_set.reserve(value_set_elements.size());
809 
810  // Try evaluating the condition with the symbol replaced by a pointer to each
811  // one of its possible values in turn. If that leads to a true for some
812  // value_set_element then we can delete it from the value set that will be
813  // used if the condition is false, and vice versa.
814  for(const exprt &value_set_element : value_set_elements)
815  {
816  if(
817  value_set_element.id() == ID_unknown ||
818  value_set_element.id() == ID_invalid)
819  {
820  continue;
821  }
822 
823  const bool exclude_null_derefs = false;
825  value_set_element, exclude_null_derefs, language_mode))
826  {
827  continue;
828  }
829 
832  value_set_element, *symbol_expr, ns);
833 
834  if(value.pointer.is_nil())
835  continue;
836 
837  exprt modified_condition(condition);
838 
839  address_of_aware_replace_symbolt replace_symbol{};
840  replace_symbol.insert(*symbol_expr, value.pointer);
841  replace_symbol(modified_condition);
842 
843  // This do_simplify() is needed for the following reason: if `condition` is
844  // `*p == a` and we replace `p` with `&a` then we get `*&a == a`. Suppose
845  // our constant propagation knows that `a` is `1`. Without this call to
846  // do_simplify(), state.rename() turns this into `*&a == 1` (because
847  // rename() doesn't do constant propagation inside addresses), which
848  // do_simplify() turns into `a == 1`, which cannot be evaluated as true
849  // without another round of constant propagation.
850  // It would be sufficient to replace this call to do_simplify() with
851  // something that just replaces `*&x` with `x` whenever it finds it.
852  do_simplify(modified_condition);
853 
854  state.record_events.push(false);
855  modified_condition = state.rename(std::move(modified_condition), ns).get();
856  state.record_events.pop();
857 
858  do_simplify(modified_condition);
859 
860  if(jump_taken_value_set && modified_condition.is_false())
861  {
862  erase_from_jump_taken_value_set.insert(value_set_element);
863  }
864  else if(jump_not_taken_value_set && modified_condition.is_true())
865  {
866  erase_from_jump_not_taken_value_set.insert(value_set_element);
867  }
868  }
869  if(jump_taken_value_set && !erase_from_jump_taken_value_set.empty())
870  {
871  auto entry_index = jump_taken_value_set->get_index_of_symbol(
872  symbol_expr->get_identifier(), symbol_type, "", ns);
873  jump_taken_value_set->erase_values_from_entry(
874  *entry_index, erase_from_jump_taken_value_set);
875  }
876  if(jump_not_taken_value_set && !erase_from_jump_not_taken_value_set.empty())
877  {
878  auto entry_index = jump_not_taken_value_set->get_index_of_symbol(
879  symbol_expr->get_identifier(), symbol_type, "", ns);
880  jump_not_taken_value_set->erase_values_from_entry(
881  *entry_index, erase_from_jump_not_taken_value_set);
882  }
883 }
Abstract interface to eager or lazy GOTO models.
virtual const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id)=0
Get a GOTO function by name, or throw if no such function exists.
Replace symbols with constants while maintaining syntactically valid expressions.
framet & top()
Definition: call_stack.h:17
complexity_violationt check_complexity(goto_symex_statet &state)
Checks the passed-in state to see if its become too complex for us to deal with, and if so set its gu...
void run_transformations(complexity_violationt complexity_violation, goto_symex_statet &current_state)
Runs a suite of transformations on the state and symex executable, performing whatever transformation...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
const_depth_iteratort depth_cend() const
Definition: expr.cpp:257
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
typet & type()
Return the type of the expression.
Definition: expr.h:84
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:255
operandst & operands()
Definition: expr.h:94
The Boolean constant false.
Definition: std_expr.h:3064
Stack frames – these are used for function calls and for exceptions.
Definition: solver_types.h:41
std::vector< active_loop_infot > active_loops
Definition: frame.h:75
std::unordered_map< irep_idt, loop_infot > loop_iterations
Definition: frame.h:77
goto_programt::const_targett end_of_function
Definition: frame.h:37
std::shared_ptr< lexical_loopst > loops_info
Definition: frame.h:74
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
const exprt & condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:366
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:258
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:214
std::set< targett, target_less_than > incoming_edges
Definition: goto_program.h:450
const source_locationt & source_location() const
Definition: goto_program.h:333
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:200
goto_program_instruction_typet type() const
What kind of instruction?
Definition: goto_program.h:344
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:792
instructionst::const_iterator const_targett
Definition: goto_program.h:615
guardt guard
Definition: goto_state.h:58
unsigned depth
Distance from entry.
Definition: goto_state.h:35
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition: goto_state.h:62
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:43
unsigned atomic_section_id
Threads.
Definition: goto_state.h:76
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:51
Central data structure: state.
goto_programt::const_targett saved_target
std::stack< bool > record_events
call_stackt & call_stack()
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...
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
symex_targett::sourcet source
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
std::vector< threadt > threads
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
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:782
virtual symbol_tablet symex_with_state(statet &state, const get_goto_functiont &get_goto_functions)
Symbolically execute the entire program starting from entry point.
Definition: symex_main.cpp:325
void rewrite_quantifiers(exprt &, statet &)
Definition: symex_main.cpp:253
virtual void symex_assume(statet &state, const exprt &cond)
Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption.
Definition: symex_main.cpp:201
void symex_threaded_step(statet &state, const get_goto_functiont &get_goto_function)
Invokes symex_step and verifies whether additional threads can be executed.
Definition: symex_main.cpp:301
void symex_unreachable_goto(statet &state)
Symbolically execute a GOTO instruction in the context of unreachable code.
Definition: symex_goto.cpp:544
complexity_limitert complexity_module
Definition: goto_symex.h:842
virtual void symex_atomic_begin(statet &state)
Symbolically execute an ATOMIC_BEGIN instruction.
const symbol_table_baset & outer_symbol_table
The symbol table associated with the goto-program being executed.
Definition: goto_symex.h:249
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:241
void symex_set_return_value(statet &state, const exprt &return_value)
Symbolically execute a SET_RETURN_VALUE instruction.
bool ignore_assertions
If this flag is set to true then assertions will be temporarily ignored by the symbolic executions.
Definition: goto_symex.h:171
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
Definition: symex_main.cpp:494
virtual void symex_step(const get_goto_functiont &get_goto_function, statet &state)
Called for each step in the symbolic execution This calls print_symex_step to print symex's current i...
Definition: symex_main.cpp:593
virtual void symex_goto(statet &state)
Symbolically execute a GOTO instruction.
Definition: symex_goto.cpp:230
virtual void symex_decl(statet &state)
Symbolically execute a DECL instruction.
Definition: symex_decl.cpp:18
void symex_catch(statet &state)
Symbolically execute a CATCH instruction.
Definition: symex_catch.cpp:14
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:816
std::unique_ptr< statet > initialize_entry_point_state(const get_goto_functiont &get_goto_function)
Initialize the symbolic execution and the given state with the beginning of the entry point function.
Definition: symex_main.cpp:399
unsigned _total_vccs
Definition: goto_symex.h:839
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:266
guard_managert & guard_manager
Used to create guards.
Definition: goto_symex.h:263
virtual symbol_tablet resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation)
Performs symbolic execution using a state and equation that have already been used to symbolically ex...
Definition: symex_main.cpp:381
void symex_assert(const goto_programt::instructiont &, statet &)
Definition: symex_main.cpp:153
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
virtual void symex_dead(statet &state)
Symbolically execute a DEAD instruction.
Definition: symex_dead.cpp:16
std::size_t path_segment_vccs
Number of VCCs generated during the run of this goto_symext object.
Definition: goto_symex.h:828
virtual void symex_start_thread(statet &state)
Symbolically execute a START_THREAD instruction.
virtual symbol_tablet symex_from_entry_point_of(const get_goto_functiont &get_goto_function, const shadow_memory_field_definitionst &fields)
Symbolically execute the entire program starting from entry point.
Definition: symex_main.cpp:466
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:258
virtual void vcc(const exprt &cond, const irep_idt &property_id, const std::string &msg, statet &state)
Symbolically execute a verification condition (assertion).
Definition: symex_main.cpp:182
void kill_instruction_local_symbols(statet &state)
Kills any variables in instruction_local_symbols (these are currently always let-bound variables defi...
Definition: symex_main.cpp:746
virtual void symex_end_of_function(statet &)
Symbolically execute a END_FUNCTION instruction.
void symex_assign(statet &state, const exprt &lhs, const exprt &rhs)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
Definition: goto_symex.cpp:38
void print_symex_step(statet &state)
Prints the route of symex as it walks through the code.
Definition: symex_main.cpp:511
void symex_throw(statet &state)
Symbolically execute a THROW instruction.
Definition: symex_throw.cpp:14
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:32
unsigned _remaining_vccs
Definition: goto_symex.h:839
virtual void symex_other(statet &state)
Symbolically execute an OTHER instruction.
Definition: symex_other.cpp:79
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
The type of delegate functions that retrieve a goto_functiont for a particular function identifier.
Definition: goto_symex.h:93
messaget log
The messaget to write log messages to.
Definition: goto_symex.h:278
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:185
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:167
void symex_assume_l2(statet &, const exprt &cond)
Definition: symex_main.cpp:221
void merge_gotos(statet &state)
Merge all branches joining at the current program point.
Definition: symex_goto.cpp:623
messaget::mstreamt & print_callstack_entry(const symex_targett::sourcet &target)
Definition: symex_main.cpp:503
std::vector< symbol_exprt > instruction_local_symbols
Variables that should be killed at the end of the current symex_step invocation.
Definition: goto_symex.h:275
virtual void symex_atomic_end(statet &state)
Symbolically execute an ATOMIC_END instruction.
virtual void symex_function_call(const get_goto_functiont &get_goto_function, statet &state, const goto_programt::instructiont &instruction)
Symbolically execute a FUNCTION_CALL instruction.
void execute_next_instruction(const get_goto_functiont &get_goto_function, statet &state)
Executes the instruction state.source.pc Case-switches over the type of the instruction being execute...
Definition: symex_main.cpp:603
virtual void initialize_path_storage_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_table_baset &new_symbol_table, const shadow_memory_field_definitionst &fields)
Puts the initial state of the entry point function into the path storage.
Definition: symex_main.cpp:477
void add(const exprt &expr)
Definition: guard_expr.cpp:38
exprt as_expr() const
Definition: guard_expr.h:46
bool is_false() const
Definition: guard_expr.h:65
exprt guard_expr(exprt expr) const
Return guard => dest or a simplified variant thereof if either guard or dest are trivial.
Definition: guard_expr.cpp:18
void populate_dirty_for_function(const irep_idt &id, const goto_functionst::goto_functiont &function)
Analyse the given function with dirtyt if it hasn't been seen before.
Definition: dirty.cpp:112
const irep_idt & id() const
Definition: irep.h:384
bool is_nil() const
Definition: irep.h:364
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
mstreamt & status() const
Definition: message.h:414
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:126
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
std::shared_ptr< lexical_loopst > get_loop_analysis(const irep_idt &function_id)
Definition: path_storage.h:131
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Map function identifiers to local_safe_pointerst instances.
Definition: path_storage.h:100
virtual void push(const patht &)=0
Add a path to resume to the storage.
void add_function_loops(const irep_idt &identifier, const goto_programt &body)
Generates a loop analysis for the instructions in goto_programt and keys it against function ID.
Definition: path_storage.h:120
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
The shadow memory field definitions.
const irep_idt & get_property_id() const
const irep_idt & get_comment() const
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:14
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void assertion(const exprt &guard, const exprt &cond, const irep_idt &property_id, const std::string &msg, const sourcet &source)
Record an assertion.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
void insert(const symbol_exprt &old_expr, const exprt &new_expr)
Thrown when we encounter an instruction, parameters to an instruction etc.
Return value for build_reference_to; see that method for documentation.
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
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.
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:44
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:391
void erase_values_from_entry(const irep_idt &index, const std::unordered_set< exprt, irep_hash > &values_to_erase)
Update the entry stored at index by erasing any values listed in values_to_erase.
Definition: value_set.cpp:1952
std::optional< irep_idt > get_index_of_symbol(irep_idt identifier, const typet &type, const std::string &suffix, const namespacet &ns) const
Get the index of the symbol and suffix.
Definition: value_set.cpp:452
complexity_violationt
What sort of symex-complexity violation has taken place.
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:141
Deprecated expression utility functions.
static format_containert< T > format(const T &o)
Definition: format.h:37
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
Symbolic Execution.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
Magic numbers used throughout the codebase.
constexpr std::size_t DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE
Limit the size of arrays for which field_sensitivity gets applied.
Definition: magic.h:21
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Storage of symbolic execution paths to resume.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:80
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
@ L1
Definition: renamed.h:24
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:42
goto_symex_statet state
Definition: path_storage.h:44
bool complexity_limits_active
Whether this run of symex is under complexity limits.
Definition: symex_config.h:56
unsigned max_depth
The maximum depth to take the execution to.
Definition: symex_config.h:23
std::size_t max_field_sensitivity_array_size
Maximum sizes for which field sensitivity will be applied to array cells.
Definition: symex_config.h:52
bool run_validation_checks
Should the additional validation checks be run? If this flag is set the checks for renaming (both lev...
Definition: symex_config.h:44
bool show_symex_steps
Prints out the path that symex is actively taking during execution, includes diagnostic information a...
Definition: symex_config.h:48
symex_configt(const optionst &options)
Construct a symex_configt using options specified in an optionst.
Definition: symex_main.cpp:30
bool doing_path_exploration
Definition: symex_config.h:25
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
goto_programt::const_targett pc
Definition: symex_target.h:42
void symex_transition(goto_symext::statet &state, goto_programt::const_targett to, bool is_backwards_goto)
Definition: symex_main.cpp:75
static void switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb)
Definition: symex_main.cpp:281
static void pop_exited_loops(const goto_programt::const_targett &to, std::vector< framet::active_loop_infot > &active_loops)
If 'to' is not an instruction in our currently top-most active loop, pop and re-check until we find a...
Definition: symex_main.cpp:62
static std::optional< symbol_exprt > find_unique_pointer_typed_symbol(const exprt &expr)
Check if an expression only contains one unique symbol (possibly repeated multiple times)
Definition: symex_main.cpp:759
Pointer Dereferencing.