CBMC
scope_tree.cpp
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 #include "scope_tree.h"
10 
12  const codet &destructor,
13  std::optional<goto_programt::targett> declaration)
14 {
15  auto previous_node = get_current_node();
16  using declaration_optt = std::optional<declaration_statet>;
17  auto declaration_opt =
18  declaration ? declaration_optt{{*declaration}} : declaration_optt{};
19  auto new_node = scope_graph.add_node(destructor, std::move(declaration_opt));
20  scope_graph.add_edge(previous_node, new_node);
21  current_node = new_node;
22 }
23 
24 std::optional<codet> &scope_treet::get_destructor(node_indext index)
25 {
26  PRECONDITION(index < scope_graph.size());
27  return scope_graph[index].destructor_value;
28 }
29 
30 std::optional<scope_treet::declaration_statet> &
32 {
33  PRECONDITION(index < scope_graph.size());
34  return scope_graph[index].declaration;
35 }
36 
38  node_indext left_index,
39  node_indext right_index)
40 {
41  std::size_t left_unique_count = 0, right_unique_count = 0;
42  while(right_index != left_index)
43  {
44  if(right_index > left_index)
45  {
46  auto edge_map = scope_graph[right_index].in;
47  INVARIANT(
48  !edge_map.empty(),
49  "Node at index " + std::to_string(right_index) +
50  " has no parent, can't find an ancestor.");
51  right_index = edge_map.begin()->first, right_unique_count++;
52  }
53  else
54  {
55  auto edge_map = scope_graph[left_index].in;
56  INVARIANT(
57  !edge_map.empty(),
58  "Node at index " + std::to_string(left_index) +
59  " has no parent, can't find an ancestor.");
60  left_index = edge_map.begin()->first, left_unique_count++;
61  }
62  }
63 
64  // At this point it doesn't matter which index we return as both are the same.
65  return {right_index, left_unique_count, right_unique_count};
66 }
67 
68 const std::vector<destructor_and_idt> scope_treet::get_destructors(
69  std::optional<node_indext> end_index,
70  std::optional<node_indext> starting_index)
71 {
72  node_indext next_id = starting_index.value_or(get_current_node());
73  node_indext end_id = end_index.value_or(0);
74 
75  std::vector<destructor_and_idt> codes;
76  while(next_id > end_id)
77  {
78  auto node = scope_graph[next_id];
79  auto &destructor = node.destructor_value;
80  if(destructor)
81  codes.emplace_back(destructor_and_idt(*destructor, next_id));
82 
83  next_id = node.in.begin()->first;
84  }
85 
86  return codes;
87 }
88 
89 void scope_treet::set_current_node(std::optional<node_indext> val)
90 {
91  if(val)
92  set_current_node(*val);
93 }
94 
96 {
97  current_node = val;
98 }
99 
101 {
103  if(current_node != 0)
104  {
105  set_current_node(scope_graph[current_node].in.begin()->first);
106  }
107 }
108 
110 {
111  return current_node;
112 }
113 
115  codet destructor,
116  std::optional<declaration_statet> declaration)
117  : destructor_value(std::move(destructor)), declaration(std::move(declaration))
118 {
119 }
Result of an attempt to find ancestor information about two nodes.
Definition: scope_tree.h:25
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 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 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
std::size_t node_indext
Definition: scope_tree.h:19
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.