Skip to content

Commit 6f71ff6

Browse files
committed
replace_symbolt: stop early if there is nothing to replace with
rename_symbolt already uses a similar optimisation. This code is heavily used during linking of goto binaries, and this simple optimisation reduces linking time by 28% on experiments conducted on the Linux kernel.
1 parent e6a9127 commit 6f71ff6

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

src/util/replace_symbol.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -119,6 +119,9 @@ bool replace_symbolt::replace(
119119

120120
bool replace_symbolt::have_to_replace(const exprt &dest) const
121121
{
122+
if(expr_map.empty() && type_map.empty())
123+
return false;
124+
122125
// first look at type
123126

124127
if(have_to_replace(dest.type()))
@@ -211,6 +214,9 @@ bool replace_symbolt::replace(typet &dest) const
211214

212215
bool replace_symbolt::have_to_replace(const typet &dest) const
213216
{
217+
if(expr_map.empty() && type_map.empty())
218+
return false;
219+
214220
if(dest.has_subtype())
215221
if(have_to_replace(dest.subtype()))
216222
return true;

0 commit comments

Comments
 (0)