Skip to content

Commit 7e83556

Browse files
committed
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.
1 parent 490439d commit 7e83556

File tree

5 files changed

+23
-22
lines changed

5 files changed

+23
-22
lines changed

src/goto-analyzer/unreachable_instructions.cpp

+5-4
Original file line numberDiff line numberDiff line change
@@ -167,7 +167,7 @@ void unreachable_instructions(
167167
{
168168
json_arrayt json_result;
169169

170-
std::set<irep_idt> called=
170+
std::unordered_set<irep_idt> called=
171171
compute_called_functions(goto_model);
172172

173173
const namespacet ns(goto_model.symbol_table);
@@ -289,9 +289,10 @@ static void xml_output_function(
289289
x.set_attribute("last line", id2string(last_location.get_line()));
290290
}
291291

292+
template <class T>
292293
static void list_functions(
293294
const goto_modelt &goto_model,
294-
const std::set<irep_idt> called,
295+
const T called,
295296
const optionst &options,
296297
std::ostream &os,
297298
bool unreachable)
@@ -387,7 +388,7 @@ void unreachable_functions(
387388
else
388389
options.set_option("text", true);
389390

390-
std::set<irep_idt> called = compute_called_functions(goto_model);
391+
std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
391392

392393
list_functions(goto_model, called, options, os, true);
393394
}
@@ -403,7 +404,7 @@ void reachable_functions(
403404
else
404405
options.set_option("text", true);
405406

406-
std::set<irep_idt> called = compute_called_functions(goto_model);
407+
std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
407408

408409
list_functions(goto_model, called, options, os, false);
409410
}

src/goto-programs/compute_called_functions.cpp

+10-10
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
1616
/// get all functions whose address is taken
1717
void compute_address_taken_functions(
1818
const exprt &src,
19-
std::set<irep_idt> &address_taken)
19+
std::unordered_set<irep_idt> &address_taken)
2020
{
2121
forall_operands(it, src)
2222
compute_address_taken_functions(*it, address_taken);
@@ -35,7 +35,7 @@ void compute_address_taken_functions(
3535
/// get all functions in the expression
3636
void compute_functions(
3737
const exprt &src,
38-
std::set<irep_idt> &address_taken)
38+
std::unordered_set<irep_idt> &address_taken)
3939
{
4040
forall_operands(it, src)
4141
compute_functions(*it, address_taken);
@@ -48,7 +48,7 @@ void compute_functions(
4848
/// get all functions whose address is taken
4949
void compute_address_taken_functions(
5050
const goto_programt &goto_program,
51-
std::set<irep_idt> &address_taken)
51+
std::unordered_set<irep_idt> &address_taken)
5252
{
5353
forall_goto_program_instructions(it, goto_program)
5454
{
@@ -60,27 +60,27 @@ void compute_address_taken_functions(
6060
/// get all functions whose address is taken
6161
void compute_address_taken_functions(
6262
const goto_functionst &goto_functions,
63-
std::set<irep_idt> &address_taken)
63+
std::unordered_set<irep_idt> &address_taken)
6464
{
6565
forall_goto_functions(it, goto_functions)
6666
compute_address_taken_functions(it->second.body, address_taken);
6767
}
6868

6969
/// get all functions whose address is taken
70-
std::set<irep_idt> compute_address_taken_functions(
70+
std::unordered_set<irep_idt> compute_address_taken_functions(
7171
const goto_functionst &goto_functions)
7272
{
73-
std::set<irep_idt> address_taken;
73+
std::unordered_set<irep_idt> address_taken;
7474
compute_address_taken_functions(goto_functions, address_taken);
7575
return address_taken;
7676
}
7777

7878
/// computes the functions that are (potentially) called
79-
std::set<irep_idt> compute_called_functions(
79+
std::unordered_set<irep_idt> compute_called_functions(
8080
const goto_functionst &goto_functions)
8181
{
82-
std::set<irep_idt> working_queue;
83-
std::set<irep_idt> functions;
82+
std::unordered_set<irep_idt> working_queue;
83+
std::unordered_set<irep_idt> functions;
8484

8585
// start from entry point
8686
working_queue.insert(goto_functions.entry_point());
@@ -121,7 +121,7 @@ std::set<irep_idt> compute_called_functions(
121121
}
122122

123123
/// computes the functions that are (potentially) called
124-
std::set<irep_idt> compute_called_functions(
124+
std::unordered_set<irep_idt> compute_called_functions(
125125
const goto_modelt &goto_model)
126126
{
127127
return compute_called_functions(goto_model.goto_functions);

src/goto-programs/compute_called_functions.h

+5-5
Original file line numberDiff line numberDiff line change
@@ -18,18 +18,18 @@ Author: Daniel Kroening, [email protected]
1818

1919
void compute_address_taken_functions(
2020
const exprt &,
21-
std::set<irep_idt> &);
21+
std::unordered_set<irep_idt> &);
2222

2323
void compute_address_taken_functions(
2424
const goto_programt &,
25-
std::set<irep_idt> &);
25+
std::unordered_set<irep_idt> &);
2626

2727
void compute_address_taken_functions(
2828
const goto_functionst &,
29-
std::set<irep_idt> &);
29+
std::unordered_set<irep_idt> &);
3030

3131
// computes the functions that are (potentially) called
32-
std::set<irep_idt> compute_called_functions(const goto_functionst &);
33-
std::set<irep_idt> compute_called_functions(const goto_modelt &);
32+
std::unordered_set<irep_idt> compute_called_functions(const goto_functionst &);
33+
std::unordered_set<irep_idt> compute_called_functions(const goto_modelt &);
3434

3535
#endif // CPROVER_GOTO_PROGRAMS_COMPUTE_CALLED_FUNCTIONS_H

src/goto-programs/link_to_library.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ void link_to_library(
4545

4646
while(true)
4747
{
48-
std::set<irep_idt> called_functions=
48+
std::unordered_set<irep_idt> called_functions=
4949
compute_called_functions(goto_functions);
5050

5151
// eliminate those for which we already have a body

src/goto-programs/remove_function_pointers.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ class remove_function_pointerst:public messaget
6161
goto_programt &goto_program,
6262
goto_programt::targett target);
6363

64-
std::set<irep_idt> address_taken;
64+
std::unordered_set<irep_idt> address_taken;
6565

6666
typedef std::map<irep_idt, code_typet> type_mapt;
6767
type_mapt type_map;
@@ -81,7 +81,7 @@ class remove_function_pointerst:public messaget
8181
goto_programt &dest);
8282

8383
void compute_address_taken_in_symbols(
84-
std::set<irep_idt> &address_taken)
84+
std::unordered_set<irep_idt> &address_taken)
8585
{
8686
const symbol_tablet &symbol_table=ns.get_symbol_table();
8787

0 commit comments

Comments
 (0)