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