Skip to content

Commit 40e213b

Browse files
committed
option for goto-instrument to remove functions unreachable from the entry point
1 parent 972c4c7 commit 40e213b

File tree

5 files changed

+102
-46
lines changed

5 files changed

+102
-46
lines changed

src/analyses/call_graph.cpp

+49-18
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Author: Daniel Kroening, [email protected]
1313

1414
/*******************************************************************\
1515
16-
Function: call_grapht::call_grapht
16+
Function: call_grapht::operator()
1717
1818
Inputs:
1919
@@ -23,23 +23,7 @@ Function: call_grapht::call_grapht
2323
2424
\*******************************************************************/
2525

26-
call_grapht::call_grapht()
27-
{
28-
}
29-
30-
/*******************************************************************\
31-
32-
Function: call_grapht::call_grapht
33-
34-
Inputs:
35-
36-
Outputs:
37-
38-
Purpose:
39-
40-
\*******************************************************************/
41-
42-
call_grapht::call_grapht(const goto_functionst &goto_functions)
26+
void call_grapht::operator()()
4327
{
4428
forall_goto_functions(f_it, goto_functions)
4529
{
@@ -96,6 +80,53 @@ void call_grapht::add(
9680

9781
/*******************************************************************\
9882
83+
Function: call_grapht::compute_reachable
84+
85+
Inputs:
86+
87+
Outputs:
88+
89+
Purpose:
90+
91+
\*******************************************************************/
92+
93+
void call_grapht::compute_reachable(
94+
const irep_idt entry_point,
95+
std::unordered_set<irep_idt, irep_id_hash> &reachable_functions)
96+
{
97+
assert(reachable_functions.empty());
98+
99+
std::list<irep_idt> worklist;
100+
101+
const goto_functionst::function_mapt::const_iterator e_it=
102+
goto_functions.function_map.find(entry_point);
103+
104+
assert(e_it!=goto_functions.function_map.end());
105+
106+
worklist.push_back(entry_point);
107+
108+
do
109+
{
110+
const irep_idt id=worklist.front();
111+
worklist.pop_front();
112+
113+
reachable_functions.insert(id);
114+
115+
const auto &p=graph.equal_range(id);
116+
117+
for(auto it=p.first; it!=p.second; it++)
118+
{
119+
const irep_idt callee=it->second;
120+
121+
if(reachable_functions.find(callee)==reachable_functions.end())
122+
worklist.push_back(callee);
123+
}
124+
}
125+
while(!worklist.empty());
126+
}
127+
128+
/*******************************************************************\
129+
99130
Function: call_grapht::output_dot
100131
101132
Inputs:

src/analyses/call_graph.h

+11-2
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,17 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include <iosfwd>
1313
#include <map>
14+
#include <unordered_set>
1415

1516
#include <goto-programs/goto_functions.h>
1617

1718
class call_grapht
1819
{
1920
public:
20-
call_grapht();
21-
explicit call_grapht(const goto_functionst &);
21+
explicit call_grapht(const goto_functionst &goto_functions) :
22+
goto_functions(goto_functions) {}
23+
24+
void operator()();
2225

2326
void output_dot(std::ostream &out) const;
2427
void output(std::ostream &out) const;
@@ -29,7 +32,13 @@ class call_grapht
2932

3033
void add(const irep_idt &caller, const irep_idt &callee);
3134

35+
void compute_reachable(
36+
const irep_idt entry_point,
37+
std::unordered_set<irep_idt, irep_id_hash> &reachable_functions);
38+
3239
protected:
40+
const goto_functionst &goto_functions;
41+
3342
void add(const irep_idt &function,
3443
const goto_programt &body);
3544
};

src/goto-instrument/goto_instrument_parse_options.cpp

+35
Original file line numberDiff line numberDiff line change
@@ -1144,6 +1144,40 @@ void goto_instrument_parse_optionst::instrument_goto_program()
11441144
slice_global_inits(ns, goto_functions);
11451145
}
11461146

1147+
if(cmdline.isset("remove-unreachable-functions"))
1148+
{
1149+
status() << "Removing functions that are not reachable from the entry point"
1150+
<< eom;
1151+
1152+
const irep_idt &entry_point=goto_functionst::entry_point();
1153+
1154+
goto_functionst::function_mapt::const_iterator e_it;
1155+
e_it=goto_functions.function_map.find(entry_point);
1156+
1157+
if(e_it==goto_functions.function_map.end())
1158+
throw "entry point not found";
1159+
1160+
call_grapht call_graph(goto_functions);
1161+
call_graph();
1162+
1163+
std::unordered_set<irep_idt, irep_id_hash> reachable_functions;
1164+
call_graph.compute_reachable(entry_point, reachable_functions);
1165+
1166+
for(goto_functionst::function_mapt::iterator it=
1167+
goto_functions.function_map.begin();
1168+
it!=goto_functions.function_map.end();)
1169+
{
1170+
const irep_idt &id=it->first;
1171+
1172+
if(reachable_functions.find(id)==reachable_functions.end())
1173+
it=goto_functions.function_map.erase(it);
1174+
else
1175+
it++;
1176+
}
1177+
1178+
goto_functions.update();
1179+
}
1180+
11471181
if(cmdline.isset("string-abstraction"))
11481182
{
11491183
status() << "String Abstraction" << eom;
@@ -1508,6 +1542,7 @@ void goto_instrument_parse_optionst::help()
15081542
" --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*)
15091543
" --property id slice with respect to specific property only\n" // NOLINT(*)
15101544
" --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*)
1545+
" --remove-unreachable-functions remove unreachable functions\n"
15111546
"\n"
15121547
"Further transformations:\n"
15131548
" --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*)

src/goto-instrument/goto_instrument_parse_options.h

+1
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,7 @@ Author: Daniel Kroening, [email protected]
5353
"(show-struct-alignment)(interval-analysis)(show-intervals)" \
5454
"(show-uninitialized)(show-locations)" \
5555
"(full-slice)(reachability-slice)(slice-global-inits)" \
56+
"(remove-unreachable-functions)" \
5657
"(inline)(partial-inline)(function-inline):(log):" \
5758
"(remove-function-pointers)" \
5859
"(show-claims)(show-properties)(property):" \

src/goto-programs/slice_global_inits.cpp

+6-26
Original file line numberDiff line numberDiff line change
@@ -40,39 +40,19 @@ void slice_global_inits(
4040
{
4141
// gather all functions reachable from the entry point
4242

43-
call_grapht call_graph(goto_functions);
44-
const call_grapht::grapht &graph=call_graph.graph;
45-
46-
std::list<irep_idt> worklist;
47-
std::unordered_set<irep_idt, irep_id_hash> functions_reached;
48-
4943
const irep_idt entry_point=goto_functionst::entry_point();
5044

51-
goto_functionst::function_mapt::const_iterator e_it;
52-
e_it=goto_functions.function_map.find(entry_point);
45+
const goto_functionst::function_mapt::const_iterator e_it=
46+
goto_functions.function_map.find(entry_point);
5347

5448
if(e_it==goto_functions.function_map.end())
5549
throw "entry point not found";
5650

57-
worklist.push_back(entry_point);
58-
59-
do
60-
{
61-
const irep_idt id=worklist.front();
62-
worklist.pop_front();
63-
64-
functions_reached.insert(id);
65-
66-
const auto &p=graph.equal_range(id);
67-
68-
for(auto it=p.first; it!=p.second; it++)
69-
{
70-
const irep_idt callee=it->second;
51+
call_grapht call_graph(goto_functions);
52+
call_graph();
7153

72-
if(functions_reached.find(callee)==functions_reached.end())
73-
worklist.push_back(callee);
74-
}
75-
} while(!worklist.empty());
54+
std::unordered_set<irep_idt, irep_id_hash> functions_reached;
55+
call_graph.compute_reachable(entry_point, functions_reached);
7656

7757
const irep_idt initialize=CPROVER_PREFIX "initialize";
7858
functions_reached.erase(initialize);

0 commit comments

Comments
 (0)