diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp index c226e2c73ab..3458c1f628f 100644 --- a/src/analyses/call_graph.cpp +++ b/src/analyses/call_graph.cpp @@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ -Function: call_grapht::call_grapht +Function: call_grapht::operator() Inputs: @@ -23,23 +23,7 @@ Function: call_grapht::call_grapht \*******************************************************************/ -call_grapht::call_grapht() -{ -} - -/*******************************************************************\ - -Function: call_grapht::call_grapht - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -call_grapht::call_grapht(const goto_functionst &goto_functions) +void call_grapht::operator()() { forall_goto_functions(f_it, goto_functions) { @@ -96,6 +80,53 @@ void call_grapht::add( /*******************************************************************\ +Function: call_grapht::compute_reachable + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void call_grapht::compute_reachable( + const irep_idt entry_point, + std::unordered_set &reachable_functions) +{ + assert(reachable_functions.empty()); + + std::list worklist; + + const goto_functionst::function_mapt::const_iterator e_it= + goto_functions.function_map.find(entry_point); + + assert(e_it!=goto_functions.function_map.end()); + + worklist.push_back(entry_point); + + do + { + const irep_idt id=worklist.front(); + worklist.pop_front(); + + reachable_functions.insert(id); + + const auto &p=graph.equal_range(id); + + for(auto it=p.first; it!=p.second; it++) + { + const irep_idt callee=it->second; + + if(reachable_functions.find(callee)==reachable_functions.end()) + worklist.push_back(callee); + } + } + while(!worklist.empty()); +} + +/*******************************************************************\ + Function: call_grapht::output_dot Inputs: diff --git a/src/analyses/call_graph.h b/src/analyses/call_graph.h index 3410410f3d4..18b3e88d6b8 100644 --- a/src/analyses/call_graph.h +++ b/src/analyses/call_graph.h @@ -11,14 +11,17 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include class call_grapht { public: - call_grapht(); - explicit call_grapht(const goto_functionst &); + explicit call_grapht(const goto_functionst &goto_functions) : + goto_functions(goto_functions) {} + + void operator()(); void output_dot(std::ostream &out) const; void output(std::ostream &out) const; @@ -29,7 +32,13 @@ class call_grapht void add(const irep_idt &caller, const irep_idt &callee); + void compute_reachable( + const irep_idt entry_point, + std::unordered_set &reachable_functions); + protected: + const goto_functionst &goto_functions; + void add(const irep_idt &function, const goto_programt &body); }; diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 3cbbac3a55b..e5e829f01e0 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1173,6 +1173,40 @@ void goto_instrument_parse_optionst::instrument_goto_program() slice_global_inits(ns, goto_functions); } + if(cmdline.isset("remove-unreachable-functions")) + { + status() << "Removing functions that are not reachable from the entry point" + << eom; + + const irep_idt &entry_point=goto_functionst::entry_point(); + + goto_functionst::function_mapt::const_iterator e_it; + e_it=goto_functions.function_map.find(entry_point); + + if(e_it==goto_functions.function_map.end()) + throw "entry point not found"; + + call_grapht call_graph(goto_functions); + call_graph(); + + std::unordered_set reachable_functions; + call_graph.compute_reachable(entry_point, reachable_functions); + + for(goto_functionst::function_mapt::iterator it= + goto_functions.function_map.begin(); + it!=goto_functions.function_map.end();) + { + const irep_idt &id=it->first; + + if(reachable_functions.find(id)==reachable_functions.end()) + it=goto_functions.function_map.erase(it); + else + it++; + } + + goto_functions.update(); + } + if(cmdline.isset("string-abstraction")) { status() << "String Abstraction" << eom; @@ -1538,6 +1572,7 @@ void goto_instrument_parse_optionst::help() " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*) " --property id slice with respect to specific property only\n" // NOLINT(*) " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*) + " --remove-unreachable-functions remove unreachable functions\n" "\n" "Further transformations:\n" " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 1db5f0bdb4d..f3b797a33b2 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -53,6 +53,7 @@ Author: Daniel Kroening, kroening@kroening.com "(show-struct-alignment)(interval-analysis)(show-intervals)" \ "(show-uninitialized)(show-locations)" \ "(full-slice)(reachability-slice)(slice-global-inits)" \ + "(remove-unreachable-functions)" \ "(inline)(partial-inline)(function-inline):(log):" \ "(remove-function-pointers)" \ "(show-claims)(show-properties)(property):" \ diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp index 5e58888d366..643c716531c 100644 --- a/src/goto-programs/slice_global_inits.cpp +++ b/src/goto-programs/slice_global_inits.cpp @@ -40,40 +40,19 @@ void slice_global_inits( { // gather all functions reachable from the entry point - call_grapht call_graph(goto_functions); - const call_grapht::grapht &graph=call_graph.graph; - - std::list worklist; - std::unordered_set functions_reached; - const irep_idt entry_point=goto_functionst::entry_point(); - goto_functionst::function_mapt::const_iterator e_it; - e_it=goto_functions.function_map.find(entry_point); + const goto_functionst::function_mapt::const_iterator e_it= + goto_functions.function_map.find(entry_point); if(e_it==goto_functions.function_map.end()) throw "entry point not found"; - worklist.push_back(entry_point); - - do - { - const irep_idt id=worklist.front(); - worklist.pop_front(); - - functions_reached.insert(id); - - const auto &p=graph.equal_range(id); - - for(auto it=p.first; it!=p.second; it++) - { - const irep_idt callee=it->second; + call_grapht call_graph(goto_functions); + call_graph(); - if(functions_reached.find(callee)==functions_reached.end()) - worklist.push_back(callee); - } - } - while(!worklist.empty()); + std::unordered_set functions_reached; + call_graph.compute_reachable(entry_point, functions_reached); const irep_idt initialize=CPROVER_PREFIX "initialize"; functions_reached.erase(initialize);