Skip to content

Commit 6228ed3

Browse files
committed
Slice global inits: use improved call graph
No behavioural change intended; should simply replace a graph walk with one that the call graph code can now perform by itself.
1 parent d136bbc commit 6228ed3

File tree

1 file changed

+16
-39
lines changed

1 file changed

+16
-39
lines changed

src/goto-programs/slice_global_inits.cpp

+16-39
Original file line numberDiff line numberDiff line change
@@ -25,48 +25,24 @@ Date: December 2016
2525
#include <goto-programs/goto_functions.h>
2626
#include <goto-programs/remove_skip.h>
2727

28+
#include <linking/static_lifetime_init.h>
29+
2830
void slice_global_inits(goto_modelt &goto_model)
2931
{
3032
// gather all functions reachable from the entry point
31-
32-
call_grapht call_graph(goto_model);
33-
const call_grapht::grapht &graph=call_graph.graph;
34-
goto_functionst &goto_functions=goto_model.goto_functions;
35-
36-
std::list<irep_idt> worklist;
37-
std::unordered_set<irep_idt, irep_id_hash> functions_reached;
38-
3933
const irep_idt entry_point=goto_functionst::entry_point();
34+
goto_functionst &goto_functions=goto_model.goto_functions;
4035

41-
goto_functionst::function_mapt::const_iterator e_it;
42-
e_it=goto_functions.function_map.find(entry_point);
43-
44-
if(e_it==goto_functions.function_map.end())
36+
if(!goto_functions.function_map.count(entry_point))
4537
throw "entry point not found";
4638

47-
worklist.push_back(entry_point);
48-
49-
do
50-
{
51-
const irep_idt id=worklist.front();
52-
worklist.pop_front();
53-
54-
functions_reached.insert(id);
55-
56-
const auto &p=graph.equal_range(id);
57-
58-
for(auto it=p.first; it!=p.second; it++)
59-
{
60-
const irep_idt callee=it->second;
61-
62-
if(functions_reached.find(callee)==functions_reached.end())
63-
worklist.push_back(callee);
64-
}
65-
}
66-
while(!worklist.empty());
67-
68-
const irep_idt initialize=CPROVER_PREFIX "initialize";
69-
functions_reached.erase(initialize);
39+
// Get the call graph restricted to functions reachable from
40+
// the entry point:
41+
call_grapht call_graph =
42+
call_grapht::create_from_root_function(goto_model, entry_point, false);
43+
const auto directed_graph = call_graph.get_directed_graph();
44+
INVARIANT(
45+
!directed_graph.empty(), "At least __CPROVER_start should be reachable");
7046

7147
// gather all symbols used by reachable functions
7248

@@ -88,10 +64,11 @@ void slice_global_inits(goto_modelt &goto_model)
8864

8965
symbol_collectort visitor;
9066

91-
assert(!functions_reached.empty());
92-
93-
for(const irep_idt &id : functions_reached)
67+
for(std::size_t node_idx = 0; node_idx < directed_graph.size(); ++node_idx)
9468
{
69+
const irep_idt &id = directed_graph[node_idx].function;
70+
if(id == INITIALIZE_FUNCTION)
71+
continue;
9572
const goto_functionst::goto_functiont &goto_function
9673
=goto_functions.function_map.at(id);
9774
const goto_programt &goto_program=goto_function.body;
@@ -108,7 +85,7 @@ void slice_global_inits(goto_modelt &goto_model)
10885
// now remove unnecessary initializations
10986

11087
goto_functionst::function_mapt::iterator f_it;
111-
f_it=goto_functions.function_map.find(initialize);
88+
f_it=goto_functions.function_map.find(INITIALIZE_FUNCTION);
11289
assert(f_it!=goto_functions.function_map.end());
11390

11491
goto_programt &goto_program=f_it->second.body;

0 commit comments

Comments
 (0)