cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
11
void
scope_treet::add
(
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> &
31
scope_treet::get_declaration
(
node_indext
index)
32
{
33
PRECONDITION
(index <
scope_graph
.size());
34
return
scope_graph
[index].declaration;
35
}
36
37
const
ancestry_resultt
scope_treet::get_nearest_common_ancestor_info
(
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
95
void
scope_treet::set_current_node
(
node_indext
val)
96
{
97
current_node
= val;
98
}
99
100
void
scope_treet::descend_tree
()
101
{
102
node_indext
current_node
=
get_current_node
();
103
if
(
current_node
!= 0)
104
{
105
set_current_node
(
scope_graph
[
current_node
].in.begin()->first);
106
}
107
}
108
109
node_indext
scope_treet::get_current_node
()
const
110
{
111
return
current_node
;
112
}
113
114
scope_treet::scope_nodet::scope_nodet
(
115
codet
destructor,
116
std::optional<declaration_statet>
declaration
)
117
:
destructor_value
(
std
::move(destructor)),
declaration
(
std
::move(
declaration
))
118
{
119
}
ancestry_resultt
Result of an attempt to find ancestor information about two nodes.
Definition
scope_tree.h:25
codet
Data structure for representing an arbitrary statement in a program.
Definition
std_code_base.h:29
destructor_and_idt
Result of a tree query holding both destructor codet and the ID of the node that held it.
Definition
scope_tree.h:50
scope_treet::scope_nodet::scope_nodet
scope_nodet()=default
scope_treet::scope_nodet::destructor_value
std::optional< codet > destructor_value
Definition
scope_tree.h:184
scope_treet::scope_nodet::declaration
std::optional< declaration_statet > declaration
Definition
scope_tree.h:185
scope_treet::current_node
node_indext current_node
Definition
scope_tree.h:198
scope_treet::scope_graph
grapht< scope_nodet > scope_graph
Definition
scope_tree.h:197
scope_treet::get_declaration
std::optional< declaration_statet > & get_declaration(node_indext index)
Fetches the declaration value for the passed-in node index.
Definition
scope_tree.cpp:31
scope_treet::add
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
scope_treet::descend_tree
void descend_tree()
Walks the current node down to its child.
Definition
scope_tree.cpp:100
scope_treet::set_current_node
void set_current_node(std::optional< node_indext > val)
Sets the current node.
Definition
scope_tree.cpp:89
scope_treet::get_destructors
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
scope_treet::get_destructor
std::optional< codet > & get_destructor(node_indext index)
Fetches the destructor value for the passed-in node index.
Definition
scope_tree.cpp:24
scope_treet::get_current_node
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
scope_treet::get_nearest_common_ancestor_info
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
STL namespace.
scope_tree.h
node_indext
std::size_t node_indext
Definition
scope_tree.h:19
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition
invariant.h:423
ansi-c
goto-conversion
scope_tree.cpp
Generated by
1.17.0