From 6f71ff64120afb7e2547bcee8a83df6d1d917787 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 22 Mar 2018 12:56:58 +0000 Subject: [PATCH 1/4] 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. --- src/util/replace_symbol.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index 14765af113f..f9667514cf7 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -119,6 +119,9 @@ bool replace_symbolt::replace( bool replace_symbolt::have_to_replace(const exprt &dest) const { + if(expr_map.empty() && type_map.empty()) + return false; + // first look at type if(have_to_replace(dest.type())) @@ -211,6 +214,9 @@ bool replace_symbolt::replace(typet &dest) const bool replace_symbolt::have_to_replace(const typet &dest) const { + if(expr_map.empty() && type_map.empty()) + return false; + if(dest.has_subtype()) if(have_to_replace(dest.subtype())) return true; From 54e5b85c2478f76c88a4e2e6e628343e8ad53f60 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 22 Mar 2018 12:29:55 +0000 Subject: [PATCH 2/4] Use a const expr to avoid unnecessary detach While dest.type() is passed as const reference, dest itself is not const in this context and thus irept::add will be used instead of irept::find. This, in turn, results in unnecessary calls to detach and thus breaks sharing and causes memory allocation. This change reduces linking time in some Linux kernel experiments by a further 10%. --- src/util/rename_symbol.cpp | 3 ++- src/util/replace_symbol.cpp | 29 ++++++++++------------------- 2 files changed, 12 insertions(+), 20 deletions(-) diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp index 59b257b09a0..710f21365a6 100644 --- a/src/util/rename_symbol.cpp +++ b/src/util/rename_symbol.cpp @@ -32,7 +32,8 @@ bool rename_symbolt::rename(exprt &dest) const // first look at type - if(have_to_rename(dest.type())) + const exprt &const_dest(dest); + if(have_to_rename(const_dest.type())) if(!rename(dest.type())) result=false; diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index f9667514cf7..25970620982 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -35,7 +35,8 @@ bool replace_symbolt::replace( // first look at type - if(have_to_replace(dest.type())) + const exprt &const_dest(dest); + if(have_to_replace(const_dest.type())) if(!replace(dest.type())) result=false; @@ -94,25 +95,15 @@ bool replace_symbolt::replace( result=false; } - const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type); - - if(c_sizeof_type.is_not_nil()) - { - typet &type=static_cast(dest.add(ID_C_c_sizeof_type)); - - if(!replace(type)) - result=false; - } + const typet &c_sizeof_type = + static_cast(dest.find(ID_C_c_sizeof_type)); + if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type)) + result &= replace(static_cast(dest.add(ID_C_c_sizeof_type))); - const irept &va_arg_type=dest.find(ID_C_va_arg_type); - - if(va_arg_type.is_not_nil()) - { - typet &type=static_cast(dest.add(ID_C_va_arg_type)); - - if(!replace(type)) - result=false; - } + const typet &va_arg_type = + static_cast(dest.find(ID_C_va_arg_type)); + if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type)) + result &= replace(static_cast(dest.add(ID_C_va_arg_type))); return result; } From 430d402046177208ee015c95e4e87e49ba2a7b20 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 22 Mar 2018 11:02:01 +0000 Subject: [PATCH 3/4] Use exprt::depth_iterator in rename_symbolt --- src/util/rename_symbol.cpp | 70 +++++++++++++++++++++----------------- 1 file changed, 39 insertions(+), 31 deletions(-) diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp index 710f21365a6..bdd2ca799ba 100644 --- a/src/util/rename_symbol.cpp +++ b/src/util/rename_symbol.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "rename_symbol.h" +#include "expr_iterator.h" #include "std_types.h" #include "std_expr.h" @@ -30,45 +31,52 @@ bool rename_symbolt::rename(exprt &dest) const { bool result=true; - // first look at type - - const exprt &const_dest(dest); - if(have_to_rename(const_dest.type())) - if(!rename(dest.type())) - result=false; - - // now do expression itself - - if(!have_to_rename(dest)) - return result; - - if(dest.id()==ID_symbol) + for(auto it = dest.depth_begin(), end = dest.depth_end(); it != end; ++it) { - expr_mapt::const_iterator it= - expr_map.find(to_symbol_expr(dest).get_identifier()); + exprt * modifiable_expr = nullptr; - if(it!=expr_map.end()) + // first look at type + if(have_to_rename(it->type())) { - to_symbol_expr(dest).set_identifier(it->second); - return false; + modifiable_expr = &it.mutate(); + result &= rename(modifiable_expr->type()); } - } - - Forall_operands(it, dest) - if(!rename(*it)) - result=false; - const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type); + // now do expression itself + if(it->id()==ID_symbol) + { + expr_mapt::const_iterator entry = + expr_map.find(to_symbol_expr(*it).get_identifier()); - if(c_sizeof_type.is_not_nil() && - !rename(static_cast(dest.add(ID_C_c_sizeof_type)))) - result=false; + if(entry != expr_map.end()) + { + if(!modifiable_expr) + modifiable_expr = &it.mutate(); + to_symbol_expr(*modifiable_expr).set_identifier(entry->second); + result = false; + } + } - const irept &va_arg_type=dest.find(ID_C_va_arg_type); + const typet &c_sizeof_type = + static_cast(it->find(ID_C_c_sizeof_type)); + if(c_sizeof_type.is_not_nil() && have_to_rename(c_sizeof_type)) + { + if(!modifiable_expr) + modifiable_expr = &it.mutate(); + result &= + rename(static_cast(modifiable_expr->add(ID_C_c_sizeof_type))); + } - if(va_arg_type.is_not_nil() && - !rename(static_cast(dest.add(ID_C_va_arg_type)))) - result=false; + const typet &va_arg_type = + static_cast(it->find(ID_C_va_arg_type)); + if(va_arg_type.is_not_nil() && have_to_rename(va_arg_type)) + { + if(!modifiable_expr) + modifiable_expr = &it.mutate(); + result &= + rename(static_cast(modifiable_expr->add(ID_C_va_arg_type))); + } + } return result; } From 20d2445335f8b8c563a8a856c34fcb1df38274b9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 22 Mar 2018 13:17:38 +0000 Subject: [PATCH 4/4] Remove unused rename(expr, old_id, new_id) There is rename_symbolt providing the same functionality, and it is actually used and optimised. cr https://code.amazon.com/reviews/CR-1629519 --- src/util/rename.cpp | 34 +--------------------------------- src/util/rename.h | 6 ------ 2 files changed, 1 insertion(+), 39 deletions(-) diff --git a/src/util/rename.cpp b/src/util/rename.cpp index 52977ab8c6a..b0fdf8d3219 100644 --- a/src/util/rename.cpp +++ b/src/util/rename.cpp @@ -8,10 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "rename.h" -#include +#include #include "symbol.h" -#include "expr.h" #include "namespace.h" /// automated variable renaming @@ -35,34 +34,3 @@ void get_new_name(irep_idt &new_name, const namespacet &ns) new_name=prefix+std::to_string(ns.get_max(prefix)+1); } - -/// automated variable renaming -/// \par parameters: expression, old name, new name -/// \return modifies the expression returns false iff something was renamed -bool rename(exprt &expr, const irep_idt &old_name, - const irep_idt &new_name) -{ - bool result=true; - - if(expr.id()==ID_symbol) - { - if(expr.get(ID_identifier)==old_name) - { - expr.set(ID_identifier, new_name); - result=false; - } - } - else - { - if(expr.id()==ID_address_of) - { - // TODO - } - else - Forall_operands(it, expr) - if(!rename(*it, old_name, new_name)) - result=false; - } - - return result; -} diff --git a/src/util/rename.h b/src/util/rename.h index 691f877d3a1..8e9269e02be 100644 --- a/src/util/rename.h +++ b/src/util/rename.h @@ -26,10 +26,4 @@ void get_new_name(symbolt &symbol, void get_new_name(irep_idt &new_name, const namespacet &ns); -// true: did nothing -// false: renamed something in the expression - -bool rename(exprt &expr, const irep_idt &old_name, - const irep_idt &new_name); - #endif // CPROVER_UTIL_RENAME_H