scope_tree.h

Go to the documentation of this file.

/*******************************************************************\
 
 Module: Scope Tree
 
 Author: John Dumbell, john.dumbell@diffblue.com
 
\*******************************************************************/
 
#ifndef CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
#define CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
 
#include <util/graph.h>
#include <util/std_code_base.h>
 
#include <goto-programs/goto_program.h>
 
#include <unordered_set>
 
typedef std::size_t node_indext;
 
class ancestry_resultt
{
public:
  explicit ancestry_resultt(node_indext node)
    : common_ancestor(node),
      left_depth_below_common_ancestor(0),
      right_depth_below_common_ancestor(0)
  {
  }
  ancestry_resultt(
    node_indext node,
    std::size_t left_pre_size,
    std::size_t right_pre_size)
    : common_ancestor(node),
      left_depth_below_common_ancestor(left_pre_size),
      right_depth_below_common_ancestor(right_pre_size)
  {
  }
  node_indext common_ancestor;
  std::size_t left_depth_below_common_ancestor;
  std::size_t right_depth_below_common_ancestor;
};
 
class destructor_and_idt
{
public:
  destructor_and_idt(const codet &code, node_indext id)
    : destructor(code), node_id(id)
  {
  }
 
  const codet destructor;
  node_indext node_id;
};
 
class scope_treet
{
public:
  struct declaration_statet
  {
    goto_programt::targett instruction;
    std::unordered_set<irep_idt, irep_id_hash> accounted_flags;
  };
 
  scope_treet()
  {
    // We add a default node to the graph to act as a root for path traversal.
    this->scope_graph.add_node();
  }
 
  void add(
    const codet &destructor,
    std::optional<goto_programt::targett> declaration);
 
  std::optional<codet> &get_destructor(node_indext index);
 
  std::optional<declaration_statet> &get_declaration(node_indext index);
 
  const std::vector<destructor_and_idt> get_destructors(
    std::optional<node_indext> end_index = {},
    std::optional<node_indext> starting_index = {});
 
  const ancestry_resultt get_nearest_common_ancestor_info(
    node_indext left_index,
    node_indext right_index);
 
  void set_current_node(std::optional<node_indext> val);
 
  void set_current_node(node_indext val);
 
  node_indext get_current_node() const;
 
  void descend_tree();
 
  void output_dot(std::ostream &os) const
  {
    scope_graph.output_dot(os);
  }
 
private:
  class scope_nodet : public graph_nodet<empty_edget>
  {
  public:
    scope_nodet() = default;
 
    explicit scope_nodet(
      codet destructor,
      std::optional<declaration_statet> declaration);
 
    std::optional<codet> destructor_value;
    std::optional<declaration_statet> declaration;
 
    std::string dot_attributes(const node_indext &n) const override
    {
      if(!declaration.has_value())
        return "";
 
      return id2string(
        declaration->instruction->decl_symbol().get_identifier());
    }
  };
 
  grapht<scope_nodet> scope_graph;
  node_indext current_node = 0;
};
 
#endif // CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H