Skip to content

Commit d6bdee6

Browse files
tautschnigtautschnig
authored
Merge pull request #2369 from polgreen/disconnect_unreachable
Disconnect unreachable nodes in a graph
2 parents 0498da9 + 67c056b commit d6bdee6

File tree

3 files changed

+264
-0
lines changed

3 files changed

+264
-0
lines changed

‎src/util/graph.h

+40
Original file line numberDiff line numberDiff line change
@@ -252,6 +252,9 @@ class grapht
252252
std::vector<node_indext>
253253
get_reachable(const std::vector<node_indext> &src, bool forwards) const;
254254

255+
void disconnect_unreachable(node_indext src);
256+
void disconnect_unreachable(const std::vector<node_indext> &src);
257+
255258
void make_chordal();
256259

257260
// return value: number of connected subgraphs
@@ -461,6 +464,43 @@ void grapht<N>::visit_reachable(node_indext src)
461464
nodes[index].visited = true;
462465
}
463466

467+
/// Removes any edges between nodes in a graph that are unreachable from
468+
/// a given start node. Used for computing cone of influence,
469+
/// by disconnecting unreachable nodes and then performing backwards
470+
/// reachability.
471+
/// Note nodes are not actually removed from the vector nodes, because
472+
/// this requires renumbering node indices. This copies the way nodes
473+
/// are "removed" in make_chordal.
474+
/// \param src: start node
475+
template <class N>
476+
void grapht<N>::disconnect_unreachable(node_indext src)
477+
{
478+
const std::vector<node_indext> source_nodes(1, src);
479+
disconnect_unreachable(source_nodes);
480+
}
481+
482+
/// Removes any edges between nodes in a graph that are unreachable
483+
/// from a vector of start nodes.
484+
/// \param src: vector of indices of start nodes
485+
template <class N>
486+
void grapht<N>::disconnect_unreachable(const std::vector<node_indext> &src)
487+
{
488+
std::vector<node_indext> reachable = get_reachable(src, true);
489+
std::sort(reachable.begin(), reachable.end());
490+
std::size_t reachable_idx = 0;
491+
for(std::size_t i = 0; i < nodes.size(); i++)
492+
{
493+
if(reachable_idx >= reachable.size())
494+
remove_edges(i);
495+
else if(i == reachable[reachable_idx])
496+
reachable_idx++;
497+
else if(i > reachable[reachable_idx])
498+
throw "error disconnecting unreachable nodes";
499+
else
500+
remove_edges(i);
501+
}
502+
}
503+
464504
/// Add to `set`, nodes that are reachable from `set`.
465505
///
466506
/// This implements a depth first search using a stack: at each step we pop a

‎unit/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ SRC = unit_tests.cpp \
99
SRC += unit_tests.cpp \
1010
analyses/ai/ai_simplify_lhs.cpp \
1111
analyses/call_graph.cpp \
12+
analyses/disconnect_unreachable_nodes_in_graph.cpp \
1213
analyses/does_remove_const/does_expr_lose_const.cpp \
1314
analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
1415
analyses/does_remove_const/is_type_at_least_as_const_as.cpp \

‎unit/analyses/disconnect_unreachable_nodes_in_graph.cpp

+223
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,223 @@
1+
/*******************************************************************\
2+
3+
Module: Unit test for graph class functions
4+
5+
Author:
6+
7+
\*******************************************************************/
8+
9+
#include <iostream>
10+
11+
#include <testing-utils/catch.hpp>
12+
13+
#include <analyses/call_graph.h>
14+
#include <analyses/call_graph_helpers.h>
15+
16+
#include <util/std_code.h>
17+
#include <util/symbol_table.h>
18+
19+
#include <goto-programs/goto_convert_functions.h>
20+
21+
static symbolt
22+
create_void_function_symbol(const irep_idt &name, const codet &code)
23+
{
24+
const code_typet void_function_type({}, empty_typet());
25+
symbolt function;
26+
function.name = name;
27+
function.type = void_function_type;
28+
function.mode = ID_java;
29+
function.value = code;
30+
return function;
31+
}
32+
33+
static bool multimap_key_matches(
34+
const std::multimap<irep_idt, irep_idt> &map,
35+
const irep_idt &key,
36+
const std::set<irep_idt> &values)
37+
{
38+
auto matching_values = map.equal_range(key);
39+
std::set<irep_idt> matching_set;
40+
for(auto it = matching_values.first; it != matching_values.second; ++it)
41+
matching_set.insert(it->second);
42+
return matching_set == values;
43+
}
44+
45+
SCENARIO("graph", "[core][util][graph]")
46+
{
47+
GIVEN("Some cyclic function calls")
48+
{
49+
// Create code like:
50+
// void A()
51+
// {
52+
// A();
53+
// B();
54+
// B();
55+
// }
56+
// void B()
57+
// {
58+
// C();
59+
// D();
60+
// }
61+
// void C() { }
62+
// void D() { }
63+
// void E()
64+
// {
65+
// F();
66+
// G();
67+
// }
68+
// void F() { }
69+
// void G() { }
70+
71+
goto_modelt goto_model;
72+
code_typet void_function_type({}, empty_typet());
73+
74+
{
75+
code_blockt calls;
76+
code_function_callt call1;
77+
call1.function() = symbol_exprt("A", void_function_type);
78+
code_function_callt call2;
79+
call2.function() = symbol_exprt("B", void_function_type);
80+
calls.move_to_operands(call1);
81+
calls.move_to_operands(call2);
82+
83+
goto_model.symbol_table.add(create_void_function_symbol("A", calls));
84+
}
85+
86+
{
87+
code_blockt calls;
88+
code_function_callt call1;
89+
call1.function() = symbol_exprt("C", void_function_type);
90+
code_function_callt call2;
91+
call2.function() = symbol_exprt("D", void_function_type);
92+
calls.move_to_operands(call1);
93+
calls.move_to_operands(call2);
94+
95+
goto_model.symbol_table.add(create_void_function_symbol("B", calls));
96+
}
97+
98+
{
99+
code_blockt calls;
100+
code_function_callt call1;
101+
call1.function() = symbol_exprt("F", void_function_type);
102+
code_function_callt call2;
103+
call2.function() = symbol_exprt("G", void_function_type);
104+
calls.move_to_operands(call1);
105+
calls.move_to_operands(call2);
106+
107+
goto_model.symbol_table.add(create_void_function_symbol("E", calls));
108+
}
109+
110+
goto_model.symbol_table.add(create_void_function_symbol("C", code_skipt()));
111+
goto_model.symbol_table.add(create_void_function_symbol("D", code_skipt()));
112+
goto_model.symbol_table.add(create_void_function_symbol("F", code_skipt()));
113+
goto_model.symbol_table.add(create_void_function_symbol("G", code_skipt()));
114+
115+
stream_message_handlert msg(std::cout);
116+
goto_convert(goto_model, msg);
117+
118+
call_grapht call_graph_from_goto_functions(goto_model);
119+
120+
WHEN("A call graph is constructed from the GOTO functions")
121+
{
122+
THEN("We expect A -> { A, B, B }, B -> { C, D }, E -> { F, G }")
123+
{
124+
const auto &check_graph = call_graph_from_goto_functions.edges;
125+
REQUIRE(check_graph.size() == 6);
126+
REQUIRE(multimap_key_matches(check_graph, "A", {"A", "B", "B"}));
127+
REQUIRE(multimap_key_matches(check_graph, "B", {"C", "D"}));
128+
REQUIRE(multimap_key_matches(check_graph, "E", {"F", "G"}));
129+
}
130+
}
131+
132+
WHEN("The call graph is exported as a grapht")
133+
{
134+
call_grapht::directed_grapht exported =
135+
call_graph_from_goto_functions.get_directed_graph();
136+
137+
typedef call_grapht::directed_grapht::node_indext node_indext;
138+
std::map<irep_idt, node_indext> nodes_by_name;
139+
for(node_indext i = 0; i < exported.size(); ++i)
140+
nodes_by_name[exported[i].function] = i;
141+
142+
THEN("We expect 7 nodes")
143+
{
144+
REQUIRE(exported.size() == 7);
145+
}
146+
147+
THEN("We expect edges A -> { A, B }, B -> { C, D }, E -> { F, G }")
148+
{
149+
// Note that means the extra A -> B edge has gone away (the grapht
150+
// structure can't represent the parallel edge)
151+
REQUIRE(exported.has_edge(nodes_by_name["A"], nodes_by_name["A"]));
152+
REQUIRE(exported.has_edge(nodes_by_name["A"], nodes_by_name["B"]));
153+
REQUIRE(exported.has_edge(nodes_by_name["B"], nodes_by_name["C"]));
154+
REQUIRE(exported.has_edge(nodes_by_name["B"], nodes_by_name["D"]));
155+
REQUIRE(exported.has_edge(nodes_by_name["E"], nodes_by_name["F"]));
156+
REQUIRE(exported.has_edge(nodes_by_name["E"], nodes_by_name["G"]));
157+
}
158+
159+
THEN("We expect G to have predecessors {E}")
160+
{
161+
std::set<irep_idt> predecessors = get_callers(exported, "G");
162+
REQUIRE(predecessors.size() == 1);
163+
REQUIRE(predecessors.count("E"));
164+
}
165+
166+
THEN("We expect F to have predecessors {E}")
167+
{
168+
std::set<irep_idt> predecessors = get_callers(exported, "F");
169+
REQUIRE(predecessors.size() == 1);
170+
REQUIRE(predecessors.count("E"));
171+
}
172+
173+
THEN("We expect {E} to be able to reach E")
174+
{
175+
std::set<irep_idt> predecessors = get_reaching_functions(exported, "E");
176+
REQUIRE(predecessors.size() == 1);
177+
REQUIRE(predecessors.count("E"));
178+
}
179+
}
180+
181+
WHEN("functions unreachable from A in the grapht are disconnected")
182+
{
183+
call_grapht::directed_grapht exported =
184+
call_graph_from_goto_functions.get_directed_graph();
185+
186+
typedef call_grapht::directed_grapht::node_indext node_indext;
187+
std::map<irep_idt, node_indext> nodes_by_name;
188+
for(node_indext i = 0; i < exported.size(); ++i)
189+
nodes_by_name[exported[i].function] = i;
190+
191+
exported.disconnect_unreachable(nodes_by_name["A"]);
192+
193+
THEN("We expect edges A -> { A, B }, B -> { C, D }")
194+
{
195+
REQUIRE(exported.has_edge(nodes_by_name["A"], nodes_by_name["A"]));
196+
REQUIRE(exported.has_edge(nodes_by_name["A"], nodes_by_name["B"]));
197+
REQUIRE(exported.has_edge(nodes_by_name["B"], nodes_by_name["C"]));
198+
REQUIRE(exported.has_edge(nodes_by_name["B"], nodes_by_name["D"]));
199+
}
200+
201+
THEN("We expect {E} to be able to reach E")
202+
{
203+
std::set<irep_idt> predecessors = get_reaching_functions(exported, "E");
204+
REQUIRE(predecessors.size() == 1);
205+
REQUIRE(predecessors.count("E"));
206+
}
207+
208+
THEN("We expect {F} to be able to reach F")
209+
{
210+
std::set<irep_idt> predecessors = get_reaching_functions(exported, "F");
211+
REQUIRE(predecessors.size() == 1);
212+
REQUIRE(predecessors.count("F"));
213+
}
214+
215+
THEN("We expect {G} to be able to reach G")
216+
{
217+
std::set<irep_idt> predecessors = get_reaching_functions(exported, "G");
218+
REQUIRE(predecessors.size() == 1);
219+
REQUIRE(predecessors.count("G"));
220+
}
221+
}
222+
}
223+
}

0 commit comments

Comments
 (0)