execution_state.h

Go to the documentation of this file.

#ifndef EXECUTION_STATE_H_
#define EXECUTION_STATE_H_
 
#include <algorithm>
#include <deque>
#include <goto-symex/engine/goto_symex.h>
#include <goto-symex/state/goto_symex_state.h>
#include <goto-symex/state/renaming.h>
#include <goto-symex/equation/symex_target.h>
 
#include <list>
#include <map>
#include <memory>
#include <optional>
#include <set>
#include <irep2/irep2.h>
#include <util/message/message.h>
#include <util/irep/std_expr.h>
 
class reachability_treet;

 
class execution_statet : public goto_symext
{
public:
  class ex_state_level2t; // Forward dec
  // Convenience typedef
  typedef goto_symex_statet::merge_statet merge_statet;

  struct parked_patht
  {
    goto_programt::const_targett target;
    goto_symex_statet::merge_state_listt::iterator snapshot;
  };
 
  struct transition_resultt
  {
    unsigned int thread_id = 0;
    std::optional<guard2tc> parent_guard;
    std::optional<parked_patht> parked;
  };
 
public:
  execution_statet(
    const goto_functionst &goto_functions,
    const namespacet &ns,
    reachability_treet *art,
    std::shared_ptr<symex_targett> _target,
    contextt &context,
    std::shared_ptr<ex_state_level2t> l2init,
    optionst &options);

  execution_statet(const execution_statet &ex);
  execution_statet &operator=(const execution_statet &ex) = delete;

  virtual ~execution_statet() = default;
 
  // Types

  class ex_state_level2t : public renaming::level2t
  {
  public:
    ex_state_level2t(execution_statet &ref);
    ~ex_state_level2t() override = default;
    std::shared_ptr<renaming::level2t> clone() const override;
    void rename(expr2tc &lhs_symbol, unsigned count) override;
    void rename(expr2tc &identifier) override;
 
    execution_statet *owner;
  };

  class state_hashing_level2t : public ex_state_level2t
  {
  public:
    state_hashing_level2t(execution_statet &ref);
    ~state_hashing_level2t() override = default;
    std::shared_ptr<renaming::level2t> clone() const override;
    void make_assignment(
      expr2tc &lhs_symbol,
      const expr2tc &const_value,
      const expr2tc &assigned_value) override;
    std::size_t generate_l2_state_hash() const;
    typedef std::map<irep_idt, std::size_t> current_state_hashest;
    current_state_hashest current_hashes;
  };
 
  // Macros

  void increment_context_switch()
  {
    CS_number++;
  }

  int get_context_switch() const
  {
    return CS_number;
  }

  unsigned int get_active_state_number() const
  {
    return active_thread;
  }

  void set_thread_start_data(unsigned int tid, const expr2tc &argdata)
  {
    if (tid >= thread_start_data.size())
    {
      log_error("Setting thread data for nonexistant thread {}", tid);
      abort();
    }
 
    thread_start_data[tid] = argdata;
  }

  const expr2tc &get_thread_start_data(unsigned int tid) const
  {
    if (tid >= thread_start_data.size())
    {
      log_error("Setting thread data for nonexistant thread {}", tid);
      abort();
    }
 
    return thread_start_data[tid];
  }
 
  // Methods

  virtual std::shared_ptr<execution_statet> clone() const = 0;

  void symex_step(reachability_treet &art) override;
 
  void symex_end_function(
    reachability_treet &art,
    const goto_programt::instructiont &instruction);

  void symex_assign(
    const expr2tc &code,
    const bool hidden,
    const guard2tc &guard) override;

  void claim(const expr2tc &expr, const std::string &msg) override;

  void symex_goto(const expr2tc &old_guard) override;

  void assume(const expr2tc &assumption) override;

  void defer_assumption(const expr2tc &assumption) override;

  void symex_printf(const expr2tc &lhs, expr2tc &code) override;

  void note_bounded_loop_truncation() override;

  unsigned int &get_dynamic_counter() override;

  unsigned int &get_nondet_counter() override;

  static void reset_dynamic_counter();

  expr2tc get_guard_identifier();

  goto_symex_statet &get_active_state();
  const goto_symex_statet &get_active_state() const;

  unsigned int get_active_atomic_number() const;

  void increment_active_atomic_number();

  void decrement_active_atomic_number();

  void switch_to_thread(unsigned int i);

  bool is_cur_state_guard_false(const expr2tc &guard);

  void execute_guard();

  bool check_if_ileaves_blocked();

  bool all_threads_terminal() const;

  unsigned int add_thread(const goto_programt *prog);

  void end_thread();

  void update_after_switch_point();
 
  void preserve_last_paths(const transition_resultt &transition);
  void cull_all_paths();
  void restore_last_paths();
 
  void record_parked_path(
    goto_programt::const_targett target,
    statet::merge_state_listt::iterator parked) override;

  void analyze_assign(const expr2tc &assign);

  void analyze_read(const expr2tc &expr);

  enum class access_kindt
  {
    READ,
    WRITE
  };

  void get_expr_globals(
    const namespacet &ns,
    const expr2tc &expr,
    std::set<expr2tc> &global_list,
    access_kindt kind,
    bool under_deref = false);

  expr2tc resolve_pointer_target(
    const namespacet &ns,
    const expr2tc &ptr,
    bool &to_global,
    bool through_deref);

  void record_aggregate_held_target(
    const namespacet &ns,
    const expr2tc &expr,
    std::set<expr2tc> &global_list,
    access_kindt kind);

  void record_access_key(
    const expr2tc &key,
    std::set<expr2tc> &global_list,
    access_kindt kind);

  bool check_mpor_dependency(unsigned int j, unsigned int l) const;

  struct transition_footprintt
  {
    std::set<expr2tc> reads, writes;
  };

  transition_footprintt last_transition_footprint(unsigned int tid) const
  {
    return {thread_last_reads.at(tid), thread_last_writes.at(tid)};
  }

  bool
  check_mpor_dependency(unsigned int j, const transition_footprintt &fp) const;

  void calculate_mpor_constraints();

  bool is_transition_blocked_by_mpor() const
  {
    return mpor_says_no;
  }

  const std::vector<std::vector<int>> &get_dependency_chain() const
  {
    return dependency_chain;
  }

  const std::vector<unsigned int> &get_thread_last_transition() const
  {
    return thread_last_transition;
  }

  void force_cswitch()
  {
    cswitch_forced = true;
  }

  bool has_cswitch_point_occured() const;

  bool can_execution_continue() const;

  std::size_t generate_hash() const;

  std::size_t update_hash_for_assignment(const expr2tc &rhs);

  void print_stack_traces(unsigned int indent = 0) const;

  void switch_to_monitor();

  void switch_away_from_monitor();

  void kill_monitor_thread();

  void analyze_args(const expr2tc &expr) override;
 
public:
  std::vector<goto_symex_statet> threads_state;
  std::vector<std::list<std::pair<goto_programt::const_targett, merge_statet>>>
    preserved_paths;
  std::vector<unsigned int> atomic_numbers;
  std::vector<expr2tc> thread_start_data;
  unsigned int last_active_thread;
  transition_resultt last_transition;
  std::shared_ptr<ex_state_level2t> state_level2;
  value_sett global_value_set;
  unsigned int active_thread;
  static constexpr const char *guard_execution_name =
    "execution_statet::\\guard_exec";
  irep_idt guard_execution;
  unsigned nondet_count;
  static thread_local unsigned dynamic_counter;
  unsigned int node_id;
  bool interleaving_unviable;
  bool main_returned;
  unsigned int monitor_tid;
  bool tid_is_set;
  unsigned int monitor_from_tid;
  bool mon_from_tid;
  unsigned int thread_cswitch_threshold;
 
protected:
  int CS_number;
  std::vector<std::set<expr2tc>> thread_last_reads;
  std::vector<std::set<expr2tc>> thread_last_writes;
  std::vector<std::vector<int>> dependency_chain;
  std::vector<unsigned int> thread_last_transition;
  unsigned int transition_ordinal;
  bool mpor_says_no;
  bool cswitch_forced;

  bool symex_trace;
  bool smt_during_symex;
  bool smt_thread_guard;
  bool no_propagation;

  void copy_derived_from(const execution_statet &ex);
 
  // Static stuff:
 
public:
  // thread_local so parallel symex threads (--k-induction-parallel)
  // don't race on this counter. Each thread's interleaving exploration
  // numbers its own nodes; cross-thread numbering isn't meaningful.
  static thread_local unsigned int node_count;
 
  friend void build_goto_symex_classes();
};

 
class dfs_execution_statet : public execution_statet
{
public:
  dfs_execution_statet(
    const goto_functionst &goto_functions,
    const namespacet &ns,
    reachability_treet *art,
    std::shared_ptr<symex_targett> _target,
    contextt &context,
    optionst &options)
    : execution_statet(
        goto_functions,
        ns,
        art,
        std::move(_target),
        context,
        options.get_bool_option("state-hashing")
          ? std::shared_ptr<state_hashing_level2t>(
              new state_hashing_level2t(*this))
          : std::shared_ptr<ex_state_level2t>(new ex_state_level2t(*this)),
        options) {};
 
  dfs_execution_statet(const dfs_execution_statet &ref) = default;
  std::shared_ptr<execution_statet> clone() const override;
  ~dfs_execution_statet() override;
};

 
class schedule_execution_statet : public execution_statet
{
public:
  schedule_execution_statet(
    const goto_functionst &goto_functions,
    const namespacet &ns,
    reachability_treet *art,
    std::shared_ptr<symex_targett> _target,
    contextt &context,
    optionst &options,
    unsigned int *ptotal_claims,
    unsigned int *premaining_claims,
    unsigned int *psimplified_claims,
    unsigned int *ptruncations)
    : execution_statet(
        goto_functions,
        ns,
        art,
        std::move(_target),
        context,
        std::shared_ptr<ex_state_level2t>(new ex_state_level2t(*this)),
        options)
  {
    this->ptotal_claims = ptotal_claims;
    this->premaining_claims = premaining_claims;
    this->psimplified_claims = psimplified_claims;
    this->ptruncations = ptruncations;
    *ptotal_claims = 0;
    *premaining_claims = 0;
    *psimplified_claims = 0;
    *ptruncations = 0;
  };
 
  schedule_execution_statet(const schedule_execution_statet &ref) = default;
  std::shared_ptr<execution_statet> clone() const override;
  ~schedule_execution_statet() override;
  void claim(const expr2tc &expr, const std::string &msg) override;
  void note_bounded_loop_truncation() override
  {
    goto_symext::note_bounded_loop_truncation();
    ++*ptruncations;
  }
 
  unsigned int *ptotal_claims;
  unsigned int *premaining_claims;
  unsigned int *psimplified_claims;
  // Each --schedule path runs in its own execution state, so the count has to
  // accumulate outside them like the claim counts do.
  unsigned int *ptruncations;
};
 
#endif /* EXECUTION_STATE_H_ */