reachability_tree.h

Go to the documentation of this file.

#ifndef REACHABILITY_TREE_H_
#define REACHABILITY_TREE_H_
 
#include <deque>
#include <map>
#include <goto-programs/goto_program.h>
#include <goto-symex/scheduler/execution_state.h>
#include <goto-symex/engine/goto_symex.h>
#include <goto-symex/state/renaming.h>
#include <goto-symex/equation/symex_target_equation.h>
 
#include <unordered_map>
#include <unordered_set>
#include <util/message/message.h>
#include <util/config/options.h>

inline bool is_esbmc_internal_symbol(const std::string &n)
{
  return n == "c:@__ESBMC_alloc" || n == "c:@__ESBMC_alloc_size" ||
         n == "c:@__ESBMC_is_dynamic" ||
         n == "c:@__ESBMC_blocked_threads_count" ||
         n == "c:@__ESBMC_rounding_mode" ||
         n.find("c:pthread_lib") != std::string::npos;
}

 
class reachability_treet
{
public:
  reachability_treet(
    goto_functionst &goto_functions,
    const namespacet &ns,
    optionst &opts,
    std::shared_ptr<symex_targett> target,
    contextt &context);

  virtual ~reachability_treet() = default;

  void setup_for_new_explore();

  execution_statet &get_cur_state();
  const execution_statet &get_cur_state() const;

  bool reset_to_unexplored_state();

  bool has_more_states();

  int get_CS_bound() const;

  int get_ileave_direction_from_user() const;

  bool check_thread_viable(unsigned int tid, bool quiet) const;

  void mark_active_thread_explored();

  bool check_for_hash_collision() const;

  void post_hash_collision_cleanup();

  void update_hash_collision_set();

  void remove_hash_collision_entry();

  void create_next_state();

  bool step_next_state();

  unsigned int decide_ileave_direction(execution_statet &ex_state);

  void print_ileave_trace() const;

  bool is_has_complete_formula();

  void go_next_state();

  void switch_to_next_execution_state();
 
  // Interface for bmc operation goes here

  goto_symext::symex_resultt get_next_formula();

  goto_symext::symex_resultt generate_schedule_formula();

  bool setup_next_formula();

  goto_functionst &goto_functions;
  contextt &permanent_context;
  bool has_complete_formula;
  bool state_hashing;
  bool directed_interleavings;
  const namespacet &ns;
  optionst &options;
  bool cs_bound_pruned;

  struct reduction_statst
  {
    unsigned long peak_threads = 1;
    unsigned long schedules_explored = 0;
    unsigned long pruned_by_mpor = 0;
    unsigned long pruned_by_hash = 0;
    unsigned long pruned_by_sleep = 0;
    unsigned long pruned_by_cs_bound = 0;
 
    bool is_concurrent() const
    {
      return peak_threads > 1;
    }
  };
  reduction_statst reduction_stats;

  void report_reduction_stats() const;

  void mark_search_truncated();
 
protected:
  struct scheduler_framet
  {
    std::vector<bool> explored_threads;
    std::map<unsigned int, execution_statet::transition_footprintt> sleeping;
 
    void ensure_thread_count(unsigned int count);
    void reset(unsigned int count);
    void mark_all_explored(unsigned int count);
    bool is_explored(unsigned int tid) const;
    void mark_explored(unsigned int tid);
    bool is_sleeping(unsigned int tid) const;
  };
 
  struct exploration_framet
  {
    std::shared_ptr<execution_statet> state;
    scheduler_framet scheduler;
    unsigned int entered_via = UINT_MAX;
    bool exhaustive = true;
  };
 
  scheduler_framet &get_cur_scheduler_frame();
  const scheduler_framet &get_cur_scheduler_frame() const;

  void wake_dependent_sleepers();
 
  bool dfs_explore_thread(unsigned int tid);
  void erase_current_frame();

  void drain_to_unexplored(bool add_leak_checks);

  std::list<exploration_framet> exploration_frames;
  std::list<exploration_framet>::iterator cur_frame_it;
  std::shared_ptr<symex_targett> schedule_target;
  std::shared_ptr<symex_targett> target_template;
  int CS_bound;
  int TS_slice;
  unsigned int schedule_total_claims;
  unsigned int schedule_remaining_claims;
  unsigned int schedule_simplified_claims;
  unsigned int schedule_bounded_loop_truncations;
  unsigned int next_thread_id;
  bool por;
  bool sleep_sets;
  std::unordered_map<std::size_t, int> hit_hashes;
  bool interactive_ileaves;
  bool schedule;
  bool smt_during_symex;
 
  /* Map to store the expression and thread ID,
   * which that expression belongs to. */
  std::unordered_map<expr2tc, std::list<unsigned int>, irep2_hash> vars_map;
  /* associative container that contains global writes in */
  std::unordered_set<expr2tc, irep2_hash> is_global;

  std::unordered_set<irep_idt, irep_id_hash> ever_written_globals;

  std::unordered_set<irep_idt, irep_id_hash> address_taken_globals;

  std::unordered_set<irep_idt, irep_id_hash> address_taken_locals;

  bool any_indirect_write = false;

  bool readonly_global_opt = false;

  void scan_program_writes();

  void scan_address_taken();
 
public:
  static bool has_shared_lifetime(const symbolt &s)
  {
    return s.static_lifetime || s.get_type().is_dynamic_set();
  }
 
  bool is_address_taken_local(const irep_idt &name) const
  {
    return address_taken_locals.count(name) != 0;
  }

  bool is_shared_storage(const symbolt &s) const
  {
    return has_shared_lifetime(s) || address_taken_locals.count(s.id) != 0;
  }

  bool may_be_written(const irep_idt &name) const
  {
    if (!readonly_global_opt || address_taken_locals.count(name) != 0)
      return true;
    // A direct, named write somewhere in the program.
    if (ever_written_globals.count(name) != 0)
      return true;
    // A write through an unresolved pointer can only target a global whose
    // address has escaped; a never-address-taken global stays read-only.
    return any_indirect_write && address_taken_globals.count(name) != 0;
  }
 
protected:
  friend class execution_statet;
  friend void build_goto_symex_classes();
};
 
#endif /* REACHABILITY_TREE_H_ */