From 026e93f0078e71bc58789aaee26a7ef63392ce1f Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 29 May 2018 15:15:58 +0200 Subject: [PATCH 1/2] function-pointer-removal: drop unused set The compute_called_functions method maintains two sets, 'done' and 'functions'. The set 'done' is only used to determine whether an element can be skipped. Since the content of the two sets is the same, the set 'done' can be dropped, and 'functions' can be used instead. Hence, this commit drops the set 'done'. Furthermore, the return value of insert includes a bool that indicates the success of the insert operation. In case insertion failed, the element has been present already, so that we can merge the find+insert into a single insert operation. Fixes: #1783 --- src/goto-programs/compute_called_functions.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/goto-programs/compute_called_functions.cpp b/src/goto-programs/compute_called_functions.cpp index 774325ab904..48cb2c96a94 100644 --- a/src/goto-programs/compute_called_functions.cpp +++ b/src/goto-programs/compute_called_functions.cpp @@ -80,7 +80,6 @@ std::set compute_called_functions( const goto_functionst &goto_functions) { std::set working_queue; - std::set done; std::set functions; // start from entry point @@ -91,12 +90,9 @@ std::set compute_called_functions( irep_idt id=*working_queue.begin(); working_queue.erase(working_queue.begin()); - if(done.find(id)!=done.end()) + if(!functions.insert(id).second) continue; - functions.insert(id); - done.insert(id); - const goto_functionst::function_mapt::const_iterator f_it= goto_functions.function_map.find(id); From 52ab0881fc077c54ec4b3c09225c15734cb2ab77 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Mon, 14 May 2018 11:34:45 +0200 Subject: [PATCH 2/2] called_functions: use unordered_set Instead of using an ordered set, use a faster unordered set. This way, running the algorithms against larger code bases should result in decreased run times, while on small programs the run time might slightly increase. As this function is used in function pointer removal, and in code that computes unreachable functions, the type change had to be propagated to the related classes as well. --- .../unreachable_instructions.cpp | 20 +++++++------- .../compute_called_functions.cpp | 26 +++++++++---------- src/goto-programs/compute_called_functions.h | 10 +++---- src/goto-programs/link_to_library.cpp | 2 +- .../remove_function_pointers.cpp | 6 ++--- 5 files changed, 32 insertions(+), 32 deletions(-) diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index bae1266ee89..760aceae75e 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -167,8 +167,7 @@ void unreachable_instructions( { json_arrayt json_result; - std::set called= - compute_called_functions(goto_model); + std::unordered_set called = compute_called_functions(goto_model); const namespacet ns(goto_model.symbol_table); @@ -291,7 +290,7 @@ static void xml_output_function( static void list_functions( const goto_modelt &goto_model, - const std::set called, + const std::unordered_set &called, const optionst &options, std::ostream &os, bool unreachable) @@ -387,7 +386,7 @@ void unreachable_functions( else options.set_option("text", true); - std::set called = compute_called_functions(goto_model); + std::unordered_set called = compute_called_functions(goto_model); list_functions(goto_model, called, options, os, true); } @@ -403,17 +402,16 @@ void reachable_functions( else options.set_option("text", true); - std::set called = compute_called_functions(goto_model); + std::unordered_set called = compute_called_functions(goto_model); list_functions(goto_model, called, options, os, false); } - -std::set compute_called_functions_from_ai( +std::unordered_set compute_called_functions_from_ai( const goto_modelt &goto_model, const ai_baset &ai) { - std::set called; + std::unordered_set called; forall_goto_functions(f_it, goto_model.goto_functions) { @@ -436,7 +434,8 @@ bool static_unreachable_functions( message_handlert &message_handler, std::ostream &out) { - std::set called = compute_called_functions_from_ai(goto_model, ai); + std::unordered_set called = + compute_called_functions_from_ai(goto_model, ai); list_functions(goto_model, called, options, out, true); @@ -450,7 +449,8 @@ bool static_reachable_functions( message_handlert &message_handler, std::ostream &out) { - std::set called = compute_called_functions_from_ai(goto_model, ai); + std::unordered_set called = + compute_called_functions_from_ai(goto_model, ai); list_functions(goto_model, called, options, out, false); diff --git a/src/goto-programs/compute_called_functions.cpp b/src/goto-programs/compute_called_functions.cpp index 48cb2c96a94..6592f603537 100644 --- a/src/goto-programs/compute_called_functions.cpp +++ b/src/goto-programs/compute_called_functions.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com /// get all functions whose address is taken void compute_address_taken_functions( const exprt &src, - std::set &address_taken) + std::unordered_set &address_taken) { forall_operands(it, src) compute_address_taken_functions(*it, address_taken); @@ -35,7 +35,7 @@ void compute_address_taken_functions( /// get all functions in the expression void compute_functions( const exprt &src, - std::set &address_taken) + std::unordered_set &address_taken) { forall_operands(it, src) compute_functions(*it, address_taken); @@ -48,7 +48,7 @@ void compute_functions( /// get all functions whose address is taken void compute_address_taken_functions( const goto_programt &goto_program, - std::set &address_taken) + std::unordered_set &address_taken) { forall_goto_program_instructions(it, goto_program) { @@ -60,27 +60,27 @@ void compute_address_taken_functions( /// get all functions whose address is taken void compute_address_taken_functions( const goto_functionst &goto_functions, - std::set &address_taken) + std::unordered_set &address_taken) { forall_goto_functions(it, goto_functions) compute_address_taken_functions(it->second.body, address_taken); } /// get all functions whose address is taken -std::set compute_address_taken_functions( - const goto_functionst &goto_functions) +std::unordered_set +compute_address_taken_functions(const goto_functionst &goto_functions) { - std::set address_taken; + std::unordered_set address_taken; compute_address_taken_functions(goto_functions, address_taken); return address_taken; } /// computes the functions that are (potentially) called -std::set compute_called_functions( - const goto_functionst &goto_functions) +std::unordered_set +compute_called_functions(const goto_functionst &goto_functions) { - std::set working_queue; - std::set functions; + std::unordered_set working_queue; + std::unordered_set functions; // start from entry point working_queue.insert(goto_functions.entry_point()); @@ -119,8 +119,8 @@ std::set compute_called_functions( } /// computes the functions that are (potentially) called -std::set compute_called_functions( - const goto_modelt &goto_model) +std::unordered_set +compute_called_functions(const goto_modelt &goto_model) { return compute_called_functions(goto_model.goto_functions); } diff --git a/src/goto-programs/compute_called_functions.h b/src/goto-programs/compute_called_functions.h index c11d16921c5..02482c40d26 100644 --- a/src/goto-programs/compute_called_functions.h +++ b/src/goto-programs/compute_called_functions.h @@ -18,18 +18,18 @@ Author: Daniel Kroening, kroening@kroening.com void compute_address_taken_functions( const exprt &, - std::set &); + std::unordered_set &); void compute_address_taken_functions( const goto_programt &, - std::set &); + std::unordered_set &); void compute_address_taken_functions( const goto_functionst &, - std::set &); + std::unordered_set &); // computes the functions that are (potentially) called -std::set compute_called_functions(const goto_functionst &); -std::set compute_called_functions(const goto_modelt &); +std::unordered_set compute_called_functions(const goto_functionst &); +std::unordered_set compute_called_functions(const goto_modelt &); #endif // CPROVER_GOTO_PROGRAMS_COMPUTE_CALLED_FUNCTIONS_H diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp index 9bb9e0d75bd..05b7a863059 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/goto-programs/link_to_library.cpp @@ -45,7 +45,7 @@ void link_to_library( while(true) { - std::set called_functions= + std::unordered_set called_functions = compute_called_functions(goto_functions); // eliminate those for which we already have a body diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 419c6d2f3ba..ff8f7292f17 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -61,7 +61,7 @@ class remove_function_pointerst:public messaget goto_programt &goto_program, goto_programt::targett target); - std::set address_taken; + std::unordered_set address_taken; typedef std::map type_mapt; type_mapt type_map; @@ -80,8 +80,8 @@ class remove_function_pointerst:public messaget code_function_callt &function_call, goto_programt &dest); - void compute_address_taken_in_symbols( - std::set &address_taken) + void + compute_address_taken_in_symbols(std::unordered_set &address_taken) { const symbol_tablet &symbol_table=ns.get_symbol_table();