goto_symex.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbolic Execution
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
 
#include <util/message.h>
 
#include "complexity_limiter.h"
#include "shadow_memory.h"
#include "symex_config.h"
#include "symex_target_equation.h"
 
class address_of_exprt;
class function_application_exprt;
class goto_symex_statet;
class path_storaget;
class shadow_memory_field_definitionst;
class side_effect_exprt;
class symex_assignt;
class typet;
 
class goto_symext
{
public:
  typedef goto_symex_statet statet;
 
  goto_symext(
    message_handlert &mh,
    const symbol_table_baset &outer_symbol_table,
    symex_target_equationt &_target,
    const optionst &options,
    path_storaget &path_storage,
    guard_managert &guard_manager)
    : should_pause_symex(false),
      symex_config(options),
      outer_symbol_table(outer_symbol_table),
      ns(outer_symbol_table),
      guard_manager(guard_manager),
      target(_target),
      atomic_section_counter(0),
      log(mh),
      path_storage(path_storage),
      path_segment_vccs(0),
      _total_vccs(std::numeric_limits<unsigned>::max()),
      _remaining_vccs(std::numeric_limits<unsigned>::max()),
      complexity_module(mh, options),
      shadow_memory(
        std::bind(
          &goto_symext::symex_assign,
          this,
          std::placeholders::_1,
          std::placeholders::_2,
          std::placeholders::_3),
        ns,
        mh)
  {
  }
  goto_symext( {…}
 
  virtual ~goto_symext() = default;
 
  typedef
    std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
    get_goto_functiont;
 
  static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model);
 
  [[nodiscard]] virtual symbol_tablet symex_from_entry_point_of(
    const get_goto_functiont &get_goto_function,
    const shadow_memory_field_definitionst &fields);
 
  virtual void initialize_path_storage_from_entry_point_of(
    const get_goto_functiont &get_goto_function,
    symbol_table_baset &new_symbol_table,
    const shadow_memory_field_definitionst &fields);
 
  [[nodiscard]] virtual symbol_tablet resume_symex_from_saved_state(
    const get_goto_functiont &get_goto_function,
    const statet &saved_state,
    symex_target_equationt *saved_equation);
 
  [[nodiscard]] virtual symbol_tablet
  symex_with_state(statet &state, const get_goto_functiont &get_goto_functions);
 
  bool should_pause_symex;
 
  bool ignore_assertions = false;
 
  virtual bool check_break(const irep_idt &loop_id, unsigned unwind);
 
protected:
  const symex_configt symex_config;
 
  std::unique_ptr<statet>
  initialize_entry_point_state(const get_goto_functiont &get_goto_function);
 
  void symex_threaded_step(
    statet &state,
    const get_goto_functiont &get_goto_function);
 
  virtual void
  symex_step(const get_goto_functiont &get_goto_function, statet &state);
 
  void execute_next_instruction(
    const get_goto_functiont &get_goto_function,
    statet &state);
 
  void kill_instruction_local_symbols(statet &state);
 
  void print_symex_step(statet &state);
 
  messaget::mstreamt &
  print_callstack_entry(const symex_targett::sourcet &target);
 
public:
 
  irep_idt language_mode;
 
protected:
  const symbol_table_baset &outer_symbol_table;
 
  namespacet ns;
 
  guard_managert &guard_manager;
 
  symex_target_equationt &target;
 
  unsigned atomic_section_counter;
 
  std::vector<symbol_exprt> instruction_local_symbols;
 
  mutable messaget log;
 
  friend class symex_dereference_statet;
 
  exprt clean_expr(exprt expr, statet &state, bool write);
 
  void trigger_auto_object(const exprt &, statet &);
  void initialize_auto_object(const exprt &, statet &);
 
  void process_array_expr(statet &, exprt &);
  exprt make_auto_object(const typet &, statet &);
  virtual void dereference(exprt &, statet &, bool write);
 
  symbol_exprt cache_dereference(exprt &dereference_result, statet &state);
  void dereference_rec(
    exprt &expr,
    statet &state,
    bool write,
    bool is_in_quantifier);
  exprt address_arithmetic(
    const exprt &,
    statet &,
    bool keep_array);
 
  virtual void symex_goto(statet &state);
  void symex_unreachable_goto(statet &state);
  void symex_set_return_value(statet &state, const exprt &return_value);
  virtual void symex_start_thread(statet &state);
  virtual void symex_atomic_begin(statet &state);
  virtual void symex_atomic_end(statet &state);
  virtual void symex_decl(statet &state);
  virtual void symex_decl(statet &state, const symbol_exprt &expr);
  virtual void symex_dead(statet &state);
  void symex_dead(statet &state, const symbol_exprt &symbol_expr);
  virtual void symex_other(statet &state);
 
  void symex_assert(const goto_programt::instructiont &, statet &);
 
  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);
 
  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);
 
  virtual void vcc(
    const exprt &cond,
    const irep_idt &property_id,
    const std::string &msg,
    statet &state);
 
  virtual void symex_assume(statet &state, const exprt &cond);
  void symex_assume_l2(statet &, const exprt &cond);
 
  void merge_gotos(statet &state);
 
  virtual void merge_goto(
    const symex_targett::sourcet &source,
    goto_statet &&goto_state,
    statet &state);
 
  void phi_function(const goto_statet &goto_state, statet &dest_state);
 
  virtual bool should_stop_unwind(
    const symex_targett::sourcet &source,
    const call_stackt &context,
    unsigned unwind);
 
  virtual void loop_bound_exceeded(statet &state, const exprt &guard);
 
  virtual void symex_function_call(
    const get_goto_functiont &get_goto_function,
    statet &state,
    const goto_programt::instructiont &instruction);
 
  virtual void locality(
    const irep_idt &function_identifier,
    goto_symext::statet &state,
    const goto_functionst::goto_functiont &goto_function);
 
  virtual void symex_end_of_function(statet &);
 
  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);
 
  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);
 
  virtual bool get_unwind_recursion(
    const irep_idt &identifier,
    unsigned thread_nr,
    unsigned unwind);
 
  void parameter_assignments(
    const irep_idt &function_identifier,
    const goto_functionst::goto_functiont &goto_function,
    statet &state,
    const exprt::operandst &arguments);
 
  // exceptions
  void symex_throw(statet &state);
  void symex_catch(statet &state);
 
  virtual void do_simplify(exprt &expr);
 
  void symex_assign(statet &state, const exprt &lhs, const exprt &rhs);
 
  bool constant_propagate_assignment_with_side_effects(
    statet &state,
    symex_assignt &symex_assign,
    const exprt &lhs,
    const exprt &rhs);
 
  void constant_propagate_empty_string(
    statet &state,
    symex_assignt &symex_assign,
    const function_application_exprt &f_l1);
 
  bool constant_propagate_string_concat(
    statet &state,
    symex_assignt &symex_assign,
    const function_application_exprt &f_l1);
 
  bool constant_propagate_string_substring(
    statet &state,
    symex_assignt &symex_assign,
    const function_application_exprt &f_l1);
 
  bool constant_propagate_integer_to_string(
    statet &state,
    symex_assignt &symex_assign,
    const function_application_exprt &f_l1);
 
  bool constant_propagate_delete_char_at(
    statet &state,
    symex_assignt &symex_assign,
    const function_application_exprt &f_l1);
 
  bool constant_propagate_delete(
    statet &state,
    symex_assignt &symex_assign,
    const function_application_exprt &f_l1);
 
  bool constant_propagate_set_length(
    statet &state,
    symex_assignt &symex_assign,
    const function_application_exprt &f_l1);
 
  bool constant_propagate_set_char_at(
    statet &state,
    symex_assignt &symex_assign,
    const function_application_exprt &f_l1);
 
  bool constant_propagate_trim(
    statet &state,
    symex_assignt &symex_assign,
    const function_application_exprt &f_l1);
 
  bool constant_propagate_case_change(
    statet &state,
    symex_assignt &symex_assign,
    const function_application_exprt &f_l1,
    bool to_upper);
 
  bool constant_propagate_replace(
    statet &state,
    symex_assignt &symex_assign,
    const function_application_exprt &f_l1);
 
  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);
 
  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);
 
  void associate_array_to_pointer(
    statet &state,
    symex_assignt &symex_assign,
    const array_exprt &new_char_array,
    const address_of_exprt &string_data);
 
  std::optional<std::reference_wrapper<const array_exprt>>
  try_evaluate_constant_string(const statet &state, const exprt &content);
 
  // clang-format off
  static std::optional<std::reference_wrapper<const constant_exprt>>
  try_evaluate_constant(
    const statet &state,
    const exprt &expr);
  // clang-format on
 
  // havocs the given object
  void havoc_rec(statet &state, const guardt &guard, const exprt &dest);
 
  typedef symex_targett::assignment_typet assignment_typet;
 
  void lift_lets(statet &, exprt &);
 
  void lift_let(statet &state, const let_exprt &let_expr);
 
  virtual void
  symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &);
 
  virtual void symex_allocate(
    statet &state,
    const exprt &lhs,
    const side_effect_exprt &code);
  virtual void symex_cpp_delete(statet &state, const codet &code);
  virtual void
  symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code);
 
  virtual void symex_printf(statet &state, const exprt &rhs);
  virtual void symex_input(statet &state, const codet &code);
  virtual void symex_output(statet &state, const codet &code);
 
  void rewrite_quantifiers(exprt &, statet &);
 
  path_storaget &path_storage;
 
public:
  std::size_t path_segment_vccs;
 
protected:
 
  unsigned _total_vccs, _remaining_vccs;
 
  complexity_limitert complexity_module;
 
  shadow_memoryt shadow_memory;
 
public:
  unsigned get_total_vccs() const
  {
    INVARIANT(
      _total_vccs != std::numeric_limits<unsigned>::max(),
      "symex_threaded_step should have been executed at least once before "
      "attempting to read total_vccs");
    return _total_vccs;
  }
  unsigned get_total_vccs() const {…}
 
  unsigned get_remaining_vccs() const
  {
    INVARIANT(
      _remaining_vccs != std::numeric_limits<unsigned>::max(),
      "symex_threaded_step should have been executed at least once before "
      "attempting to read remaining_vccs");
    return _remaining_vccs;
  }
  unsigned get_remaining_vccs() const {…}
 
  void validate(const validation_modet vm) const
  {
    target.validate(ns, vm);
  }
  void validate(const validation_modet vm) const {…}
};
class goto_symext {…};
 
void symex_transition(goto_symext::statet &state);
 
void symex_transition(
  goto_symext::statet &,
  goto_programt::const_targett to,
  bool is_backwards_goto);
 
renamedt<exprt, L2> try_evaluate_pointer_comparisons(
  renamedt<exprt, L2> condition,
  const value_sett &value_set,
  const irep_idt &language_mode,
  const namespacet &ns);
 
#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H