goto_symex_state.h

Go to the documentation of this file.

#ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
 
#include <cassert>
#include <cstdint>
#include <climits>
#include <cstdio>
#include <cstring>
#include <goto-programs/goto_functions.h>
#include <goto-symex/state/renaming.h>
#include <goto-symex/symex_invariant.h>
#include <goto-symex/equation/symex_target.h>
#include <pointer-analysis/value_set.h>
#include <set>
#include <stack>
#include <string>
#include <irep2/irep2_guard.h>
#include <util/base/i2string.h>
#include <irep2/irep2.h>
#include <memory>
#include <vector>
#include <goto-symex/waypoint.h>
 
class execution_statet; // forward decl

 
class goto_symex_statet
{
public:
  class merge_statet; // forward dec
  class framet;       // forward dec

  goto_symex_statet(
    renaming::level2t &l2,
    value_sett &vs,
    const namespacet &_ns,
    bool no_propagation);

  goto_symex_statet(
    const goto_symex_statet &state,
    renaming::level2t &l2,
    value_sett &vs);
 
  goto_symex_statet(goto_symex_statet const &) = default;
 
  goto_symex_statet &operator=(const goto_symex_statet &state);
 
  // Types
 
  typedef std::list<merge_statet> merge_state_listt;
  typedef std::map<goto_programt::const_targett, merge_state_listt>
    merge_state_mapt;
  typedef std::vector<framet> call_stackt;
  typedef persistent_set<
    renaming::level2t::name_record,
    renaming::level2t::name_rec_hash>
    variable_name_sett;

  class merge_statet
  {
  public:
    unsigned num_instructions;
    std::shared_ptr<renaming::level2t> level2_ptr;
    renaming::level2t &level2;
    value_sett value_set;
    guard2tc guard;
    unsigned int thread_id;
    renaming::level1t::current_namest level1_names;
    variable_name_sett local_variables;
    // interval_domaint::interval_map; see snapshot_interval_domain
    std::shared_ptr<void> interval_snapshot;
    BigInt stack_frame_total;
 
    explicit merge_statet(const goto_symex_statet &s)
      : num_instructions(s.num_instructions),
        level2_ptr(s.level2.clone()),
        level2(*level2_ptr),
        value_set(s.value_set),
        guard(s.guard),
        thread_id(s.source.thread_nr),
        level1_names(s.top().level1.current_names),
        local_variables(s.top().local_variables),
        stack_frame_total(s.top().stack_frame_total)
    {
    }
 
    explicit merge_statet(const merge_statet &s)
      : num_instructions(s.num_instructions),
        level2_ptr(s.level2_ptr->clone()),
        level2(*level2_ptr),
        value_set(s.value_set),
        guard(s.guard),
        thread_id(s.thread_id),
        level1_names(s.level1_names),
        local_variables(s.local_variables),
        interval_snapshot(s.interval_snapshot),
        stack_frame_total(s.stack_frame_total)
    {
    }
 
    merge_statet &operator=(const merge_statet &)
    {
      abort();
    }
 
  public:
    ~merge_statet() = default;
 
  protected:
  };

  class framet
  {
  public:
    irep_idt function_identifier;
    merge_state_mapt merge_state_map;
    renaming::level1t level1;
    symex_targett::sourcet calling_location;

    goto_programt::const_targett end_of_function;
    expr2tc return_value;

    std::list<std::pair<goto_programt::const_targett, expr2tc>>
      cur_function_ptr_targets;
    goto_programt::const_targett function_ptr_call_loc;
    goto_programt::const_targett function_ptr_combine_target;
    expr2tc orig_func_ptr_call;

    void grow_stack_frame(const expr2tc &expr);

    void decrease_stack_frame_size(const expr2tc &expr);

    variable_name_sett declaration_history;
    variable_name_sett local_variables;
    std::vector<expr2tc> alloca_objects;

    unsigned int va_index;

    unsigned int va_cursor;

    guard2tc entry_guard;

    bool hidden;

    BigInt stack_frame_total;
 
    framet(unsigned int thread_id, const namespacet *ns = nullptr)
      : return_value(expr2tc()),
        va_index(UINT_MAX),
        va_cursor(UINT_MAX),
        hidden(false),
        stack_frame_total(0)
    {
      level1.thread_id = thread_id;
      level1.ns = ns;
    }
  };
 
  // Macros
  void current_name(expr2tc &symirep) const
  {
    current_name(level2, symirep);
  }

  void current_name(const renaming::level2t &plevel2, expr2tc &symirep) const
  {
    top().level1.get_ident_name(symirep);
    plevel2.get_ident_name(symirep);
  }

  void current_name(const merge_statet &merge_state, expr2tc &symirep) const
  {
    current_name(merge_state.level2, symirep);
  }

  inline framet &top()
  {
    SYMEX_INVARIANT(!call_stack.empty(), "no activation record to read");
    return call_stack.back();
  }
 
  inline const framet &top() const
  {
    SYMEX_INVARIANT(!call_stack.empty(), "no activation record to read");
    return call_stack.back();
  }

  BigInt total_stack_size() const;

  inline framet &new_frame(unsigned int thread_id)
  {
    call_stack.emplace_back(thread_id, &ns);
    return call_stack.back();
  }

  inline void pop_frame()
  {
    SYMEX_INVARIANT(!call_stack.empty(), "no activation record to pop");
    // I6: a dropped merge snapshot silently discards the paths it holds.
    SYMEX_INVARIANT(
      call_stack.back().merge_state_map.empty(),
      "activation record popped with unmerged path snapshots");
    call_stack.pop_back();
  }

  inline const framet &previous_frame()
  {
    // Indexed rather than `*(--(--end()))`, which at size 1 forms a pointer
    // before the start of the vector ([expr.add]/4).
    SYMEX_INVARIANT(
      call_stack.size() >= 2, "no caller frame beneath the current one");
    return call_stack[call_stack.size() - 2];
  }
 
  // Methods

  void initialize(
    const goto_programt::const_targett &start,
    const goto_programt::const_targett &end,
    const goto_programt *prog,
    unsigned int thread_id);

  void rename(expr2tc &expr);
 
  void rename_type(expr2tc &expr);
  void rename_array_sizes(type2tc &type);

  void rename_address(expr2tc &expr);
 
  void rename_address(expr2tc &expr, const std::set<irep_idt> &bound);

  void rename_quantified(expr2tc &expr, const std::set<irep_idt> &bound);

  void assignment(expr2tc &lhs, const expr2tc &rhs);

  expr2tc shallow_array_update(const expr2tc &rhs, const expr2tc &l1_lhs) const;

  bool constant_propagation(const expr2tc &expr) const;

  expr2tc pin_symbolic_updates(const expr2tc &rhs, const expr2tc &l2_lhs) const;

  bool constant_propagation_reference(const expr2tc &expr) const;

  void get_original_name(expr2tc &expr) const;

  void print_stack_trace(unsigned int indent, std::ostream &os) const;

  std::vector<stack_framet> gen_stack_trace() const;

  void fixup_renamed_type(expr2tc &expr, const type2tc &orig_type);
 
  // Members

  unsigned num_instructions;

  bool thread_ended;

  guard2tc guard;
  guard2tc global_guard;
  symex_targett::sourcet source;
  std::map<irep_idt, unsigned> variable_instance_nums;
  typedef std::unordered_map<unsigned, BigInt> loop_iterationst;
  loop_iterationst loop_iterations;
  std::map<irep_idt, BigInt> function_unwind;

  bool use_value_set;
  bool no_propagation = false;
  renaming::level2t &level2;
  value_sett &value_set;

  call_stackt call_stack;

  const namespacet &ns;

  std::map<expr2tc, unsigned> realloc_map;
 
  // --- Violation-witness replay state ---

  std::vector<std::vector<waypoint>> witness_segs;
  size_t cur_seg;
  bool witness_target_reached;

  std::unordered_map<irep_idt, bool> cycle_branch_map;
 
  void advance_witness_position();
};
 
#endif