cbmc-documentation/goto__symex_8h_source.html

/*******************************************************************\


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 "symex_config.h"


class address_of_exprt;

class code_function_callt;

class function_application_exprt;

class goto_symex_statet;

class path_storaget;

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_tablet &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)

  {

  }


  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);


  virtual void symex_from_entry_point_of(

    const get_goto_functiont &get_goto_function,

    symbol_tablet &new_symbol_table);


  virtual void initialize_path_storage_from_entry_point_of(

    const get_goto_functiont &get_goto_function,

    symbol_tablet &new_symbol_table);


  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);


  virtual void symex_with_state(

    statet &state,

    const get_goto_functiont &get_goto_functions,

    symbol_tablet &new_symbol_table);


  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_tablet &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 &,

    const std::string &msg,

    statet &);


  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 no_body(const irep_idt &identifier)

  {

  }


  virtual void symex_function_call(

    const get_goto_functiont &get_goto_function,

    statet &state,

    const goto_programt::instructiont &instruction);


  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);


  optionalt<std::reference_wrapper<const array_exprt>>

  try_evaluate_constant_string(const statet &state, const exprt &content);


  // clang-format off

  static optionalt<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);


  static unsigned dynamic_counter;


  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;


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_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;

  }


  void validate(const validation_modet vm) const

  {

    target.validate(ns, vm);

  }

};


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