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/message.h>
16 
17 #include "complexity_limiter.h"
18 #include "symex_config.h"
19 
20 class address_of_exprt;
23 class goto_symex_statet;
24 class path_storaget;
25 class side_effect_exprt;
26 class symex_assignt;
27 class typet;
28 
35 {
36 public:
39 
50  message_handlert &mh,
52  symex_target_equationt &_target,
53  const optionst &options,
56  : should_pause_symex(false),
57  symex_config(options),
61  target(_target),
63  log(mh),
66  _total_vccs(std::numeric_limits<unsigned>::max()),
67  _remaining_vccs(std::numeric_limits<unsigned>::max()),
68  complexity_module(mh, options)
69  {
70  }
71 
73  virtual ~goto_symext() = default;
74 
80  typedef
81  std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
83 
92 
103  virtual void symex_from_entry_point_of(
105  symbol_tablet &new_symbol_table);
106 
110  symbol_tablet &new_symbol_table);
111 
122  virtual void resume_symex_from_saved_state(
124  const statet &saved_state,
125  symex_target_equationt *saved_equation,
126  symbol_tablet &new_symbol_table);
127 
140  virtual void symex_with_state(
141  statet &state,
142  const get_goto_functiont &get_goto_functions,
143  symbol_tablet &new_symbol_table);
144 
153 
156  bool ignore_assertions = false;
157 
166  virtual bool check_break(const irep_idt &loop_id, unsigned unwind);
167 
168 protected:
171 
176  std::unique_ptr<statet>
178 
184  void symex_threaded_step(
185  statet &state,
187 
195  virtual void
197 
208  statet &state);
209 
214 
217  void print_symex_step(statet &state);
218 
221 
222 public:
223 
227 
228 protected:
235 
244 
249 
252 
256 
260  std::vector<symbol_exprt> instruction_local_symbols;
261 
263  mutable messaget log;
264 
266 
276  exprt clean_expr(exprt expr, statet &state, bool write);
277 
278  void trigger_auto_object(const exprt &, statet &);
279  void initialize_auto_object(const exprt &, statet &);
280 
285  void process_array_expr(statet &, exprt &);
286  exprt make_auto_object(const typet &, statet &);
287  virtual void dereference(exprt &, statet &, bool write);
288 
289  symbol_exprt cache_dereference(exprt &dereference_result, statet &state);
290  void dereference_rec(
291  exprt &expr,
292  statet &state,
293  bool write,
294  bool is_in_quantifier);
296  const exprt &,
297  statet &,
298  bool keep_array);
299 
302  virtual void symex_goto(statet &state);
309  void symex_set_return_value(statet &state, const exprt &return_value);
312  virtual void symex_start_thread(statet &state);
315  virtual void symex_atomic_begin(statet &state);
318  virtual void symex_atomic_end(statet &state);
321  virtual void symex_decl(statet &state);
326  virtual void symex_decl(statet &state, const symbol_exprt &expr);
329  virtual void symex_dead(statet &state);
333  void symex_dead(statet &state, const symbol_exprt &symbol_expr);
336  virtual void symex_other(statet &state);
337 
339 
350  goto_symex_statet &current_state,
351  goto_statet &jump_taken_state,
352  goto_statet &jump_not_taken_state,
353  const exprt &original_guard,
354  const exprt &new_guard,
355  const namespacet &ns);
356 
374  exprt condition,
375  const value_sett &original_value_set,
376  value_sett *jump_taken_value_set,
377  value_sett *jump_not_taken_value_set,
378  const namespacet &ns);
379 
380  virtual void vcc(
381  const exprt &,
382  const std::string &msg,
383  statet &);
384 
389  virtual void symex_assume(statet &state, const exprt &cond);
390  void symex_assume_l2(statet &, const exprt &cond);
391 
396  void merge_gotos(statet &state);
397 
404  virtual void merge_goto(
405  const symex_targett::sourcet &source,
406  goto_statet &&goto_state,
407  statet &state);
408 
412  void phi_function(const goto_statet &goto_state, statet &dest_state);
413 
419  virtual bool should_stop_unwind(
420  const symex_targett::sourcet &source,
421  const call_stackt &context,
422  unsigned unwind);
423 
424  virtual void loop_bound_exceeded(statet &state, const exprt &guard);
425 
428  virtual void no_body(const irep_idt &identifier)
429  {
430  }
431 
439  virtual void symex_function_call(
441  statet &state,
442  const goto_programt::instructiont &instruction);
443 
446  virtual void symex_end_of_function(statet &);
447 
455  virtual void symex_function_call_symbol(
457  statet &state,
458  const exprt &lhs,
459  const symbol_exprt &function,
460  const exprt::operandst &arguments);
461 
474  virtual void symex_function_call_post_clean(
476  statet &state,
477  const exprt &cleaned_lhs,
478  const symbol_exprt &function,
479  const exprt::operandst &cleaned_arguments);
480 
481  virtual bool get_unwind_recursion(
482  const irep_idt &identifier,
483  unsigned thread_nr,
484  unsigned unwind);
485 
493  const irep_idt &function_identifier,
494  const goto_functionst::goto_functiont &goto_function,
495  statet &state,
496  const exprt::operandst &arguments);
497 
498  // exceptions
501  void symex_throw(statet &state);
504  void symex_catch(statet &state);
505 
506  virtual void do_simplify(exprt &expr);
507 
513  void symex_assign(statet &state, const exprt &lhs, const exprt &rhs);
514 
524  statet &state,
526  const exprt &lhs,
527  const exprt &rhs);
528 
536  statet &state,
538  const function_application_exprt &f_l1);
539 
549  statet &state,
551  const function_application_exprt &f_l1);
552 
562  statet &state,
564  const function_application_exprt &f_l1);
565 
575  statet &state,
577  const function_application_exprt &f_l1);
578 
588  statet &state,
590  const function_application_exprt &f_l1);
591 
601  statet &state,
603  const function_application_exprt &f_l1);
604 
619  statet &state,
621  const function_application_exprt &f_l1);
622 
632  statet &state,
634  const function_application_exprt &f_l1);
635 
638  statet &state,
640  const function_application_exprt &f_l1);
641 
644  statet &state,
646  const function_application_exprt &f_l1,
647  bool to_upper);
648 
651  statet &state,
653  const function_application_exprt &f_l1);
654 
676  statet &state,
678  const ssa_exprt &length,
679  const constant_exprt &new_length,
680  const ssa_exprt &char_array,
681  const array_exprt &new_char_array);
682 
692  statet &state,
694  const std::string &aux_symbol_name,
695  const ssa_exprt &char_array,
696  const array_exprt &new_char_array);
697 
709  statet &state,
711  const array_exprt &new_char_array,
712  const address_of_exprt &string_data);
713 
715  try_evaluate_constant_string(const statet &state, const exprt &content);
716 
717  // clang-format off
720  const statet &state,
721  const exprt &expr);
722  // clang-format on
723 
724  // havocs the given object
725  void havoc_rec(statet &state, const guardt &guard, const exprt &dest);
726 
728 
734  void lift_lets(statet &, exprt &);
735 
740  void lift_let(statet &state, const let_exprt &let_expr);
741 
742  virtual void
743  symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &);
744 
750  virtual void symex_allocate(
751  statet &state,
752  const exprt &lhs,
753  const side_effect_exprt &code);
757  virtual void symex_cpp_delete(statet &state, const codet &code);
763  virtual void
764  symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code);
765 
769  virtual void symex_printf(statet &state, const exprt &rhs);
773  virtual void symex_input(statet &state, const codet &code);
777  virtual void symex_output(statet &state, const codet &code);
778 
780  static unsigned dynamic_counter;
781 
782  void rewrite_quantifiers(exprt &, statet &);
783 
789 
790 public:
800  std::size_t path_segment_vccs;
801 
802 protected:
810 
813 
815 
816 public:
817  unsigned get_total_vccs() const
818  {
819  INVARIANT(
820  _total_vccs != std::numeric_limits<unsigned>::max(),
821  "symex_threaded_step should have been executed at least once before "
822  "attempting to read total_vccs");
823  return _total_vccs;
824  }
825 
826  unsigned get_remaining_vccs() const
827  {
828  INVARIANT(
829  _remaining_vccs != std::numeric_limits<unsigned>::max(),
830  "symex_threaded_step should have been executed at least once before "
831  "attempting to read remaining_vccs");
832  return _remaining_vccs;
833  }
834 
835  void validate(const validation_modet vm) const
836  {
837  target.validate(ns, vm);
838  }
839 };
840 
848 
849 void symex_transition(
852  bool is_backwards_goto);
853 
865  renamedt<exprt, L2> condition,
866  const value_sett &value_set,
867  const irep_idt &language_mode,
868  const namespacet &ns);
869 
870 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
Abstract interface to eager or lazy GOTO models.
Operator to return the address of an object.
Definition: pointer_expr.h:361
Array constructor from list of elements.
Definition: std_expr.h:1476
codet representation of a function call statement.
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
Symex complexity module.
A constant literal expression.
Definition: std_expr.h:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
Application of (mathematical) function.
::goto_functiont goto_functiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
instructionst::const_iterator const_targett
Definition: goto_program.h:593
Container for data that varies per program point, e.g.
Definition: goto_state.h:32
Central data structure: state.
The main class for the forward symbolic simulator.
Definition: goto_symex.h:35
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:957
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
void rewrite_quantifiers(exprt &, statet &)
Definition: symex_main.cpp:254
virtual void symex_function_call_symbol(const get_goto_functiont &get_goto_function, statet &state, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments)
Symbolic execution of a call to a function call.
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:30
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:202
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
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:617
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:814
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
Definition: goto_symex.h:38
virtual void symex_atomic_begin(statet &state)
Symbolically execute an ATOMIC_BEGIN instruction.
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:226
void symex_set_return_value(statet &state, const exprt &return_value)
Symbolically execute a SET_RETURN_VALUE instruction.
virtual void no_body(const irep_idt &identifier)
Log a warning that a function has no body.
Definition: goto_symex.h:428
virtual void vcc(const exprt &, const std::string &msg, statet &)
Definition: symex_main.cpp:185
virtual void symex_input(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP input.
bool ignore_assertions
If this flag is set to true then assertions will be temporarily ignored by the symbolic executions.
Definition: goto_symex.h:156
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:493
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:592
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:629
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:877
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:163
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...
virtual void symex_goto(statet &state)
Symbolically execute a GOTO instruction.
Definition: symex_goto.cpp:230
unsigned get_remaining_vccs() const
Definition: goto_symex.h:826
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
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:702
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:49
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:855
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:788
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:404
void havoc_rec(statet &state, const guardt &guard, const exprt &dest)
Definition: symex_other.cpp:20
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:385
unsigned _total_vccs
Definition: goto_symex.h:811
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:251
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
virtual void symex_cpp_delete(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP delete
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:947
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.
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:550
guard_managert & guard_manager
Used to create guards.
Definition: goto_symex.h:248
unsigned atomic_section_counter
A monotonically increasing index for each encountered ATOMIC_BEGIN instruction.
Definition: goto_symex.h:255
void symex_assert(const goto_programt::instructiont &, statet &)
Definition: symex_main.cpp:157
unsigned get_total_vccs() const
Definition: goto_symex.h:817
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:479
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:382
virtual void loop_bound_exceeded(statet &state, const exprt &guard)
Definition: symex_goto.cpp:922
bool constant_propagate_trim(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate trim operations.
virtual void symex_dead(statet &state)
Symbolically execute a DEAD instruction.
Definition: symex_dead.cpp:16
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program being executed.
Definition: goto_symex.h:234
static optionalt< std::reference_wrapper< const constant_exprt > > try_evaluate_constant(const statet &state, const exprt &expr)
Definition: goto_symex.cpp:366
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:325
std::size_t path_segment_vccs
Number of VCCs generated during the run of this goto_symext object.
Definition: goto_symex.h:800
virtual void symex_start_thread(statet &state)
Symbolically execute a START_THREAD instruction.
void initialize_auto_object(const exprt &, statet &)
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:470
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...
virtual void symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:243
void trigger_auto_object(const exprt &, statet &)
void lift_lets(statet &, exprt &)
Execute any let expressions in expr using symex_assignt::assign_symbol.
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
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:678
virtual void symex_end_of_function(statet &)
Symbolically execute a END_FUNCTION instruction.
static unsigned dynamic_counter
A monotonically increasing index for each created dynamic object.
Definition: goto_symex.h:780
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
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:40
exprt make_auto_object(const typet &, statet &)
void print_symex_step(statet &state)
Prints the route of symex as it walks through the code.
Definition: symex_main.cpp:510
virtual void symex_printf(statet &state, const exprt &rhs)
Symbolically execute an OTHER instruction that does a CPP printf
virtual void symex_output(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP output.
void symex_throw(statet &state)
Symbolically execute a THROW instruction.
Definition: symex_throw.cpp:14
exprt address_arithmetic(const exprt &, statet &, bool keep_array)
Transforms an lvalue expression by replacing any dereference operations it contains with explicit ref...
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:281
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:317
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:34
unsigned _remaining_vccs
Definition: goto_symex.h:811
virtual void symex_other(statet &state)
Symbolically execute an OTHER instruction.
Definition: symex_other.cpp:75
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:82
virtual void symex_function_call_post_clean(const get_goto_functiont &get_goto_function, statet &state, const exprt &cleaned_lhs, const symbol_exprt &function, const exprt::operandst &cleaned_arguments)
Symbolic execution of a function call by inlining.
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.
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:796
symbol_exprt cache_dereference(exprt &dereference_result, statet &state)
messaget log
The messaget to write log messages to.
Definition: goto_symex.h:263
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:170
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:152
virtual void dereference(exprt &, statet &, bool write)
Replace all dereference operations within expr with explicit references to the objects they may refer...
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:463
void symex_assume_l2(statet &, const exprt &cond)
Definition: symex_main.cpp:222
void merge_gotos(statet &state)
Merge all branches joining at the current program point.
Definition: symex_goto.cpp:623
symex_targett::assignment_typet assignment_typet
Definition: goto_symex.h:727
virtual ~goto_symext()=default
A virtual destructor allowing derived classes to be cleaned up correctly.
bool constant_propagate_replace(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant proagate character replacement.
messaget::mstreamt & print_callstack_entry(const symex_targett::sourcet &target)
Definition: symex_main.cpp:502
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.
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:260
void validate(const validation_modet vm) const
Definition: goto_symex.h:835
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:413
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 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:237
optionalt< std::reference_wrapper< const array_exprt > > try_evaluate_constant_string(const statet &state, const exprt &content)
Definition: goto_symex.cpp:345
void process_array_expr(statet &, exprt &)
Given an expression, find the root object and the offset into it.
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:602
A let expression.
Definition: std_expr.h:2973
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:38
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:33
An expression containing a side effect.
Definition: std_code.h:1450
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
Functor for symex assignment.
Definition: symex_assign.h:26
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
void validate(const namespacet &ns, const validation_modet vm) const
The type of an expression, extends irept.
Definition: type.h:29
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:43
Symbolic Execution.
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:214
void symex_transition(goto_symext::statet &state)
Transition to the next instruction, which increments the internal program counter and initializes the...
Definition: symex_main.cpp:150
nonstd::optional< T > optionalt
Definition: optional.h:35
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
Configuration used for a symbolic execution.
Definition: symex_config.h:17
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
Symbolic Execution.
unsigned int statet
validation_modet