cprover
goto_symex.h
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 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
13 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
14 
15 #include <util/options.h>
16 #include <util/message.h>
17 
19 
20 #include "complexity_limiter.h"
21 #include "path_storage.h"
22 #include "symex_config.h"
23 
24 class byte_extract_exprt;
26 class typet;
27 class code_typet;
28 class symbol_tablet;
29 class code_assignt;
31 class exprt;
32 class goto_symex_statet;
33 class if_exprt;
34 class index_exprt;
35 class symbol_exprt;
36 class member_exprt;
37 class namespacet;
38 class side_effect_exprt;
39 class symex_assignt;
40 class typecast_exprt;
41 
48 {
49 public:
52 
63  message_handlert &mh,
65  symex_target_equationt &_target,
66  const optionst &options,
69  : should_pause_symex(false),
70  symex_config(options),
74  target(_target),
76  log(mh),
79  _total_vccs(std::numeric_limits<unsigned>::max()),
80  _remaining_vccs(std::numeric_limits<unsigned>::max()),
81  complexity_module(mh, options)
82  {
83  }
84 
86  virtual ~goto_symext() = default;
87 
93  typedef
94  std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
96 
105 
116  virtual void symex_from_entry_point_of(
118  symbol_tablet &new_symbol_table);
119 
123  symbol_tablet &new_symbol_table);
124 
135  virtual void resume_symex_from_saved_state(
137  const statet &saved_state,
138  symex_target_equationt *saved_equation,
139  symbol_tablet &new_symbol_table);
140 
153  virtual void symex_with_state(
154  statet &state,
155  const get_goto_functiont &get_goto_functions,
156  symbol_tablet &new_symbol_table);
157 
166 
169  bool ignore_assertions = false;
170 
179  virtual bool check_break(const irep_idt &loop_id, unsigned unwind);
180 
181 protected:
184 
189  std::unique_ptr<statet>
191 
197  void symex_threaded_step(
198  statet &state,
200 
208  virtual void
210 
221  statet &state);
222 
227 
230  void print_symex_step(statet &state);
231 
234 
235 public:
236 
240 
241 protected:
248 
257 
262 
265 
269 
273  std::vector<symbol_exprt> instruction_local_symbols;
274 
276  mutable messaget log;
277 
279 
289  exprt clean_expr(exprt expr, statet &state, bool write);
290 
291  void trigger_auto_object(const exprt &, statet &);
292  void initialize_auto_object(const exprt &, statet &);
293 
298  void process_array_expr(statet &, exprt &);
299  exprt make_auto_object(const typet &, statet &);
300  virtual void dereference(exprt &, statet &, bool write);
301 
302  symbol_exprt cache_dereference(exprt &dereference_result, statet &state);
303  void dereference_rec(
304  exprt &expr,
305  statet &state,
306  bool write,
307  bool is_in_quantifier);
309  const exprt &,
310  statet &,
311  bool keep_array);
312 
315  virtual void symex_goto(statet &state);
321  virtual void symex_start_thread(statet &state);
324  virtual void symex_atomic_begin(statet &state);
327  virtual void symex_atomic_end(statet &state);
330  virtual void symex_decl(statet &state);
335  virtual void symex_decl(statet &state, const symbol_exprt &expr);
338  virtual void symex_dead(statet &state);
342  void symex_dead(statet &state, const symbol_exprt &symbol_expr);
345  virtual void symex_other(statet &state);
346 
348 
359  goto_symex_statet &current_state,
360  goto_statet &jump_taken_state,
361  goto_statet &jump_not_taken_state,
362  const exprt &original_guard,
363  const exprt &new_guard,
364  const namespacet &ns);
365 
383  exprt condition,
384  const value_sett &original_value_set,
385  value_sett *jump_taken_value_set,
386  value_sett *jump_not_taken_value_set,
387  const namespacet &ns);
388 
389  virtual void vcc(
390  const exprt &,
391  const std::string &msg,
392  statet &);
393 
398  virtual void symex_assume(statet &state, const exprt &cond);
399  void symex_assume_l2(statet &, const exprt &cond);
400 
405  void merge_gotos(statet &state);
406 
413  virtual void merge_goto(
414  const symex_targett::sourcet &source,
415  goto_statet &&goto_state,
416  statet &state);
417 
421  void phi_function(const goto_statet &goto_state, statet &dest_state);
422 
428  virtual bool should_stop_unwind(
429  const symex_targett::sourcet &source,
430  const call_stackt &context,
431  unsigned unwind);
432 
433  virtual void loop_bound_exceeded(statet &state, const exprt &guard);
434 
437  virtual void no_body(const irep_idt &identifier)
438  {
439  }
440 
448  virtual void symex_function_call(
450  statet &state,
451  const code_function_callt &code);
452 
455  virtual void symex_end_of_function(statet &);
456 
466  virtual void symex_function_call_symbol(
468  statet &state,
469  const code_function_callt &code);
470 
481  virtual void symex_function_call_code(
483  statet &state,
484  const code_function_callt &call);
485 
486  virtual bool get_unwind_recursion(
487  const irep_idt &identifier,
488  unsigned thread_nr,
489  unsigned unwind);
490 
498  const irep_idt &function_identifier,
499  const goto_functionst::goto_functiont &goto_function,
500  statet &state,
501  const exprt::operandst &arguments);
502 
503  // exceptions
506  void symex_throw(statet &state);
509  void symex_catch(statet &state);
510 
511  virtual void do_simplify(exprt &expr);
512 
518  void symex_assign(statet &state, const exprt &lhs, const exprt &rhs);
519 
529  statet &state,
531  const exprt &lhs,
532  const exprt &rhs);
533 
541  statet &state,
543  const function_application_exprt &f_l1);
544 
554  statet &state,
556  const function_application_exprt &f_l1);
557 
567  statet &state,
569  const function_application_exprt &f_l1);
570 
580  statet &state,
582  const function_application_exprt &f_l1);
583 
593  statet &state,
595  const function_application_exprt &f_l1);
596 
606  statet &state,
608  const function_application_exprt &f_l1);
609 
624  statet &state,
626  const function_application_exprt &f_l1);
627 
637  statet &state,
639  const function_application_exprt &f_l1);
640 
643  statet &state,
645  const function_application_exprt &f_l1);
646 
649  statet &state,
651  const function_application_exprt &f_l1,
652  bool to_upper);
653 
656  statet &state,
658  const function_application_exprt &f_l1);
659 
681  statet &state,
683  const ssa_exprt &length,
684  const constant_exprt &new_length,
685  const ssa_exprt &char_array,
686  const array_exprt &new_char_array);
687 
697  statet &state,
699  const std::string &aux_symbol_name,
700  const ssa_exprt &char_array,
701  const array_exprt &new_char_array);
702 
714  statet &state,
716  const array_exprt &new_char_array,
717  const address_of_exprt &string_data);
718 
720  try_evaluate_constant_string(const statet &state, const exprt &content);
721 
722  // clang-format off
725  const statet &state,
726  const exprt &expr);
727  // clang-format on
728 
729  // havocs the given object
730  void havoc_rec(statet &state, const guardt &guard, const exprt &dest);
731 
733 
739  void lift_lets(statet &, exprt &);
740 
745  void lift_let(statet &state, const let_exprt &let_expr);
746 
747  virtual void
748  symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &);
749 
755  virtual void symex_allocate(
756  statet &state,
757  const exprt &lhs,
758  const side_effect_exprt &code);
762  virtual void symex_cpp_delete(statet &state, const codet &code);
768  virtual void
769  symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code);
779  virtual void symex_fkt(statet &state, const code_function_callt &code);
783  virtual void symex_printf(statet &state, const exprt &rhs);
787  virtual void symex_input(statet &state, const codet &code);
791  virtual void symex_output(statet &state, const codet &code);
792 
794  static unsigned dynamic_counter;
795 
796  void rewrite_quantifiers(exprt &, statet &);
797 
803 
804 public:
814  std::size_t path_segment_vccs;
815 
816 protected:
824 
827 
829 
830 public:
831  unsigned get_total_vccs() const
832  {
833  INVARIANT(
834  _total_vccs != std::numeric_limits<unsigned>::max(),
835  "symex_threaded_step should have been executed at least once before "
836  "attempting to read total_vccs");
837  return _total_vccs;
838  }
839 
840  unsigned get_remaining_vccs() const
841  {
842  INVARIANT(
843  _remaining_vccs != std::numeric_limits<unsigned>::max(),
844  "symex_threaded_step should have been executed at least once before "
845  "attempting to read remaining_vccs");
846  return _remaining_vccs;
847  }
848 
849  void validate(const validation_modet vm) const
850  {
851  target.validate(ns, vm);
852  }
853 };
854 
862 
863 void symex_transition(
866  bool is_backwards_goto);
867 
879  renamedt<exprt, L2> condition,
880  const value_sett &value_set,
881  const irep_idt &language_mode,
882  const namespacet &ns);
883 
884 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
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:326
guard_exprt
Definition: guard_expr.h:27
goto_symext::clean_expr
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
Definition: symex_clean_expr.cpp:233
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:70
goto_symext::cache_dereference
symbol_exprt cache_dereference(exprt &dereference_result, statet &state)
Definition: symex_dereference.cpp:198
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:593
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:223
symex_dereference_statet::state
goto_symext::statet & state
Definition: symex_dereference_state.h:34
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:532
symex_configt
Configuration used for a symbolic execution.
Definition: symex_config.h:17
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:749
goto_symext::dynamic_counter
static unsigned dynamic_counter
A monotonically increasing index for each created dynamic object.
Definition: goto_symex.h:794
goto_symext::symex_function_call_code
virtual void symex_function_call_code(const get_goto_functiont &get_goto_function, statet &state, const code_function_callt &call)
Symbolic execution of a function call by inlining.
Definition: symex_function_call.cpp:221
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:785
optionst
Definition: options.h:23
goto_symext::try_evaluate_constant_string
optionalt< std::reference_wrapper< const array_exprt > > try_evaluate_constant_string(const statet &state, const exprt &content)
Definition: goto_symex.cpp:344
typet
The type of an expression, extends irept.
Definition: type.h:28
goto_symext::address_arithmetic
exprt address_arithmetic(const exprt &, statet &, bool keep_array)
Transforms an lvalue expression by replacing any dereference operations it contains with explicit ref...
Definition: symex_dereference.cpp:43
goto_symext::symex_printf
virtual void symex_printf(statet &state, const exprt &rhs)
Symbolically execute an OTHER instruction that does a CPP printf
Definition: symex_builtin_functions.cpp:368
goto_symext::constant_propagate_case_change
bool constant_propagate_case_change(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1, bool to_upper)
Attempt to constant propagate case changes, both upper and lower.
Definition: goto_symex.cpp:946
goto_symext::constant_propagate_delete
bool constant_propagate_delete(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate deleting a substring from a string.
Definition: goto_symex.cpp:701
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:383
path_storaget
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:38
goto_symext::path_storage
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:802
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
goto_symext::constant_propagate_trim
bool constant_propagate_trim(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate trim operations.
Definition: goto_symex.cpp:1116
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
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
goto_symext::guard_manager
guard_managert & guard_manager
Used to create guards.
Definition: goto_symex.h:261
goto_symext::constant_propagate_set_char_at
bool constant_propagate_set_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate setting the char at the given index.
Definition: goto_symex.cpp:876
goto_symext::symex_fkt
virtual void symex_fkt(statet &state, const code_function_callt &code)
Symbolically execute a FUNCTION_CALL instruction for a function whose name starts with CPROVER_FKT_PR...
Definition: symex_builtin_functions.cpp:539
goto_symext::symex_cpp_new
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes.
Definition: symex_builtin_functions.cpp:467
goto_symext::get_new_string_data_symbol
const symbolt & get_new_string_data_symbol(statet &state, symex_assignt &symex_assign, const std::string &aux_symbol_name, const ssa_exprt &char_array, const array_exprt &new_char_array)
Installs a new symbol in the symbol table to represent the given character array, and assigns the cha...
Definition: goto_symex.cpp:280
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:480
goto_symext::statet
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
Definition: goto_symex.h:51
value_sett
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:45
exprt
Base class for all expressions.
Definition: expr.h:54
goto_symext::merge_gotos
void merge_gotos(statet &state)
Merge all branches joining at the current program point.
Definition: symex_goto.cpp:611
options.h
Options.
goto_symext::constant_propagate_delete_char_at
bool constant_propagate_delete_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate deleting a character from a string.
Definition: goto_symex.cpp:628
goto_symext::lift_let
void lift_let(statet &state, const let_exprt &let_expr)
Execute a single let expression, which should not have any nested let expressions (use lift_lets inst...
Definition: symex_clean_expr.cpp:185
symex_assignt
Functor for symex assignment.
Definition: symex_assign.h:26
goto_symext::symex_dead
virtual void symex_dead(statet &state)
Symbolically execute a DEAD instruction.
Definition: symex_dead.cpp:19
goto_symext::symex_catch
void symex_catch(statet &state)
Symbolically execute a CATCH instruction.
Definition: symex_catch.cpp:14
goto_symext::trigger_auto_object
void trigger_auto_object(const exprt &, statet &)
Definition: auto_objects.cpp:77
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
call_stackt
Definition: call_stack.h:15
goto_symext::complexity_module
complexity_limitert complexity_module
Definition: goto_symex.h:828
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:405
path_storage.h
Storage of symbolic execution paths to resume.
goto_symext::should_stop_unwind
virtual bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind)
Determine whether to unwind a loop.
Definition: symex_goto.cpp:945
goto_symext::get_unwind_recursion
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
Definition: symex_function_call.cpp:34
goto_symext::assign_string_constant
void assign_string_constant(statet &state, symex_assignt &symex_assign, const ssa_exprt &length, const constant_exprt &new_length, const ssa_exprt &char_array, const array_exprt &new_char_array)
Assign constant string length and string data given by a char array to given ssa variables.
Definition: goto_symex.cpp:236
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:814
goto_symext::log
messaget log
The messaget to write log messages to.
Definition: goto_symex.h:276
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
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_symext::associate_array_to_pointer
void associate_array_to_pointer(statet &state, symex_assignt &symex_assign, const array_exprt &new_char_array, const address_of_exprt &string_data)
Generate array to pointer association primitive.
Definition: goto_symex.cpp:316
goto_symext::parameter_assignments
void parameter_assignments(const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)
Iterates over arguments and assigns them to the parameters, which are symbols whose name and type are...
Definition: symex_function_call.cpp:39
goto_symext::merge_goto
virtual void merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state)
Merge a single branch, the symbolic state of which is held in goto_state, into the current overall sy...
Definition: symex_goto.cpp:666
goto_symext::constant_propagate_string_concat
bool constant_propagate_string_concat(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate string concatenation.
Definition: goto_symex.cpp:412
goto_symext::constant_propagate_integer_to_string
bool constant_propagate_integer_to_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate converting an integer to a string.
Definition: goto_symex.cpp:549
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_symext::process_array_expr
void process_array_expr(statet &, exprt &)
Given an expression, find the root object and the offset into it.
Definition: symex_clean_expr.cpp:136
goto_symext::dereference
virtual void dereference(exprt &, statet &, bool write)
Replace all dereference operations within expr with explicit references to the objects they may refer...
Definition: symex_dereference.cpp:480
goto_symext::symex_goto
virtual void symex_goto(statet &state)
Symbolically execute a GOTO instruction.
Definition: symex_goto.cpp:227
abstract_goto_model.h
Abstract interface to eager or lazy GOTO models.
goto_symext::symex_cpp_delete
virtual void symex_cpp_delete(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP delete
Definition: symex_builtin_functions.cpp:529
goto_symext::constant_propagate_empty_string
void constant_propagate_empty_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Create an empty string constant.
Definition: goto_symex.cpp:384
goto_symext::constant_propagate_string_substring
bool constant_propagate_string_substring(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate getting a substring of a string.
Definition: goto_symex.cpp:462
goto_symext::symex_decl
virtual void symex_decl(statet &state)
Symbolically execute a DECL instruction.
Definition: symex_decl.cpp:16
goto_symext::_remaining_vccs
unsigned _remaining_vccs
Definition: goto_symex.h:825
goto_symext::constant_propagate_set_length
bool constant_propagate_set_length(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate setting the length of a string.
Definition: goto_symex.cpp:795
goto_symext::symex_allocate
virtual void symex_allocate(statet &state, const exprt &lhs, const side_effect_exprt &code)
Symbolically execute an assignment instruction that has an allocate on the right hand side.
Definition: symex_builtin_functions.cpp:49
goto_symext::initialize_auto_object
void initialize_auto_object(const exprt &, statet &)
Definition: auto_objects.cpp:37
goto_symext::symex_va_start
virtual void symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &)
Definition: symex_builtin_functions.cpp:249
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:471
goto_symext::validate
void validate(const validation_modet vm) const
Definition: goto_symex.h:849
goto_symext::dereference_rec
void dereference_rec(exprt &expr, statet &state, bool write, bool is_in_quantifier)
If expr is a dereference_exprt, replace it with explicit references to the objects it may point to.
Definition: symex_dereference.cpp:258
symex_dereference_statet::ns
const namespacet & ns
Definition: symex_dereference_state.h:35
goto_symext
The main class for the forward symbolic simulator.
Definition: goto_symex.h:48
symex_dereference_statet
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
Definition: symex_dereference_state.h:26
goto_symext::phi_function
void phi_function(const goto_statet &goto_state, statet &dest_state)
Merge the SSA assignments from goto_state into dest_state.
Definition: symex_goto.cpp:843
goto_symext::symex_input
virtual void symex_input(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP input.
Definition: symex_builtin_functions.cpp:423
goto_symext::symex_end_of_function
virtual void symex_end_of_function(statet &)
Symbolically execute a END_FUNCTION instruction.
Definition: symex_function_call.cpp:405
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:194
goto_symext::make_auto_object
exprt make_auto_object(const typet &, statet &)
Definition: auto_objects.cpp:19
goto_symext::symex_function_call_symbol
virtual void symex_function_call_symbol(const get_goto_functiont &get_goto_function, statet &state, const code_function_callt &code)
Symbolic execution of a call to a function call.
Definition: symex_function_call.cpp:191
goto_symext::goto_symext
goto_symext(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager)
Construct a goto_symext to execute a particular program.
Definition: goto_symex.h:62
code_typet
Base type of functions.
Definition: std_types.h:533
validation_modet
validation_modet
Definition: validation_mode.h:13
message_handlert
Definition: message.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_symext::do_simplify
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:33
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:302
goto_statet
Container for data that varies per program point, e.g.
Definition: goto_state.h:32
symex_transition
void symex_transition(goto_symext::statet &state)
Transition to the next instruction, which increments the internal program counter and initializes the...
Definition: symex_main.cpp:151
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_symext::havoc_rec
void havoc_rec(statet &state, const guardt &guard, const exprt &dest)
Definition: symex_other.cpp:19
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
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
goto_symext::~goto_symext
virtual ~goto_symext()=default
A virtual destructor allowing derived classes to be cleaned up correctly.
try_evaluate_pointer_comparisons
renamedt< exprt, L2 > try_evaluate_pointer_comparisons(renamedt< exprt, L2 > condition, const value_sett &value_set, const irep_idt &language_mode, const namespacet &ns)
Try to evaluate pointer comparisons where they can be trivially determined using the value-set.
Definition: symex_goto.cpp:211
goto_symext::check_break
virtual bool check_break(const irep_idt &loop_id, unsigned unwind)
Defines condition for interrupting symbolic execution for a specific loop.
Definition: symex_goto.cpp:605
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
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:603
goto_symext::atomic_section_counter
unsigned atomic_section_counter
A monotonically increasing index for each encountered ATOMIC_BEGIN instruction.
Definition: goto_symex.h:268
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_symext::assignment_typet
symex_targett::assignment_typet assignment_typet
Definition: goto_symex.h:732
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:203
goto_symext::vcc
virtual void vcc(const exprt &, const std::string &msg, statet &)
Definition: symex_main.cpp:186
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:494
goto_symext::lift_lets
void lift_lets(statet &, exprt &)
Execute any let expressions in expr using symex_assignt::assign_symbol.
Definition: symex_clean_expr.cpp:204
symex_target_equationt::validate
void validate(const namespacet &ns, const validation_modet vm) const
Definition: symex_target_equation.h:285
goto_symext::_total_vccs
unsigned _total_vccs
Definition: goto_symex.h:825
goto_symext::symex_config
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:183
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
goto_symext::constant_propagate_assignment_with_side_effects
bool constant_propagate_assignment_with_side_effects(statet &state, symex_assignt &symex_assign, const exprt &lhs, const exprt &rhs)
Attempt to constant propagate side effects of the assignment (if any)
Definition: goto_symex.cpp:162
goto_symext::print_callstack_entry
messaget::mstreamt & print_callstack_entry(const symex_targett::sourcet &target)
Definition: symex_main.cpp:503
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
messaget::mstreamt
Definition: message.h:224
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:564
goto_symext::loop_bound_exceeded
virtual void loop_bound_exceeded(statet &state, const exprt &guard)
Definition: symex_goto.cpp:910
complexity_limiter.h
Symbolic Execution.
goto_symext::try_evaluate_constant
static optionalt< std::reference_wrapper< const constant_exprt > > try_evaluate_constant(const statet &state, const exprt &expr)
Definition: goto_symex.cpp:365
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
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_symext::apply_goto_condition
void apply_goto_condition(goto_symex_statet &current_state, goto_statet &jump_taken_state, goto_statet &jump_not_taken_state, const exprt &original_guard, const exprt &new_guard, const namespacet &ns)
Propagate constants and points-to information implied by a GOTO condition.
Definition: symex_goto.cpp:27
index_exprt
Array index operator.
Definition: std_expr.h:1242
goto_symext::no_body
virtual void no_body(const irep_idt &identifier)
Log a warning that a function has no body.
Definition: goto_symex.h:437
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
complexity_limitert
Symex complexity module.
Definition: complexity_limiter.h:46
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
goto_symext::get_total_vccs
unsigned get_total_vccs() const
Definition: goto_symex.h:831
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
message.h
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:177
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
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:511
goto_symext::symex_assert
void symex_assert(const goto_programt::instructiont &, statet &)
Definition: symex_main.cpp:158
goto_symext::constant_propagate_replace
bool constant_propagate_replace(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant proagate character replacement.
Definition: goto_symex.cpp:1008
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
goto_symext::symex_assign
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:39
goto_symext::rewrite_quantifiers
void rewrite_quantifiers(exprt &, statet &)
Definition: symex_main.cpp:255
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1381
goto_symext::symex_other
virtual void symex_other(statet &state)
Symbolically execute an OTHER instruction.
Definition: symex_other.cpp:74
goto_symext::symex_start_thread
virtual void symex_start_thread(statet &state)
Symbolically execute a START_THREAD instruction.
Definition: symex_start_thread.cpp:20
goto_symext::symex_output
virtual void symex_output(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP output.
Definition: symex_builtin_functions.cpp:445
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:27
let_exprt
A let expression.
Definition: std_expr.h:2804
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1898
statet
unsigned int statet
Definition: trace_automaton.h:24
symex_config.h
Symbolic Execution.
goto_symext::get_remaining_vccs
unsigned get_remaining_vccs() const
Definition: goto_symex.h:840
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
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35