CBMC
scope_tree.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Scope Tree
4 
5  Author: John Dumbell, john.dumbell@diffblue.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
10 #define CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
11 
12 #include <util/graph.h>
13 #include <util/std_code_base.h>
14 
16 
17 #include <unordered_set>
18 
19 typedef std::size_t node_indext;
20 
25 {
26 public:
28  : common_ancestor(node),
31  {
32  }
34  node_indext node,
35  std::size_t left_pre_size,
36  std::size_t right_pre_size)
37  : common_ancestor(node),
38  left_depth_below_common_ancestor(left_pre_size),
39  right_depth_below_common_ancestor(right_pre_size)
40  {
41  }
45 };
46 
50 {
51 public:
53  : destructor(code), node_id(id)
54  {
55  }
56 
59 };
60 
93 {
94 public:
96  {
111  std::unordered_set<irep_idt, irep_id_hash> accounted_flags;
112  };
113 
115  {
116  // We add a default node to the graph to act as a root for path traversal.
117  this->scope_graph.add_node();
118  }
119 
124  void add(
125  const codet &destructor,
126  std::optional<goto_programt::targett> declaration);
127 
129  std::optional<codet> &get_destructor(node_indext index);
130 
132  std::optional<declaration_statet> &get_declaration(node_indext index);
133 
142  const std::vector<destructor_and_idt> get_destructors(
143  std::optional<node_indext> end_index = {},
144  std::optional<node_indext> starting_index = {});
145 
150  node_indext left_index,
151  node_indext right_index);
152 
156  void set_current_node(std::optional<node_indext> val);
157 
160  void set_current_node(node_indext val);
161 
164 
166  void descend_tree();
167 
169  void output_dot(std::ostream &os) const
170  {
171  scope_graph.output_dot(os);
172  }
173 
174 private:
175  class scope_nodet : public graph_nodet<empty_edget>
176  {
177  public:
178  scope_nodet() = default;
179 
180  explicit scope_nodet(
181  codet destructor,
182  std::optional<declaration_statet> declaration);
183 
184  std::optional<codet> destructor_value;
185  std::optional<declaration_statet> declaration;
186 
187  std::string dot_attributes(const node_indext &n) const override
188  {
189  if(!declaration.has_value())
190  return "";
191 
192  return id2string(
193  declaration->instruction->decl_symbol().get_identifier());
194  }
195  };
196 
199 };
200 
201 #endif // CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
Result of an attempt to find ancestor information about two nodes.
Definition: scope_tree.h:25
std::size_t left_depth_below_common_ancestor
Definition: scope_tree.h:43
ancestry_resultt(node_indext node)
Definition: scope_tree.h:27
std::size_t right_depth_below_common_ancestor
Definition: scope_tree.h:44
node_indext common_ancestor
Definition: scope_tree.h:42
ancestry_resultt(node_indext node, std::size_t left_pre_size, std::size_t right_pre_size)
Definition: scope_tree.h:33
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
Result of a tree query holding both destructor codet and the ID of the node that held it.
Definition: scope_tree.h:50
node_indext node_id
Definition: scope_tree.h:58
const codet destructor
Definition: scope_tree.h:57
destructor_and_idt(const codet &code, node_indext id)
Definition: scope_tree.h:52
instructionst::iterator targett
Definition: goto_program.h:614
This class represents a node in a directed graph.
Definition: graph.h:35
std::size_t node_indext
Definition: graph.h:37
A generic directed graph with a parametric node type.
Definition: graph.h:167
std::optional< codet > destructor_value
Definition: scope_tree.h:184
std::optional< declaration_statet > declaration
Definition: scope_tree.h:185
std::string dot_attributes(const node_indext &n) const override
Node with attributes suitable for Graphviz DOT format.
Definition: scope_tree.h:187
Tree to keep track of the destructors generated along each branch of a function.
Definition: scope_tree.h:93
node_indext current_node
Definition: scope_tree.h:198
grapht< scope_nodet > scope_graph
Definition: scope_tree.h:197
std::optional< declaration_statet > & get_declaration(node_indext index)
Fetches the declaration value for the passed-in node index.
Definition: scope_tree.cpp:31
void add(const codet &destructor, std::optional< goto_programt::targett > declaration)
Adds a destructor/declaration pair to the current stack, attaching it to the current node.
Definition: scope_tree.cpp:11
void output_dot(std::ostream &os) const
Output scope tree to os in dot format.
Definition: scope_tree.h:169
void descend_tree()
Walks the current node down to its child.
Definition: scope_tree.cpp:100
void set_current_node(std::optional< node_indext > val)
Sets the current node.
Definition: scope_tree.cpp:89
const std::vector< destructor_and_idt > get_destructors(std::optional< node_indext > end_index={}, std::optional< node_indext > starting_index={})
Builds a vector of destructors that start from starting_index and ends at end_index.
Definition: scope_tree.cpp:68
std::optional< codet > & get_destructor(node_indext index)
Fetches the destructor value for the passed-in node index.
Definition: scope_tree.cpp:24
node_indext get_current_node() const
Gets the node that the next addition will be added to as a child.
Definition: scope_tree.cpp:109
const ancestry_resultt get_nearest_common_ancestor_info(node_indext left_index, node_indext right_index)
Finds the nearest common ancestor of two nodes and then returns it.
Definition: scope_tree.cpp:37
Concrete Goto Program.
A Template Class for Graphs.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::size_t node_indext
Definition: scope_tree.h:19
std::unordered_set< irep_idt, irep_id_hash > accounted_flags
In order to handle user goto statements which jump into a scope the declaration may need to be follow...
Definition: scope_tree.h:111
goto_programt::targett instruction
This is an iterator which points to the instruction where the declaration takes place.
Definition: scope_tree.h:99