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 diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp index 59b257b09a0..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,44 +31,52 @@ bool rename_symbolt::rename(exprt &dest) const { bool result=true; - // first look at type - - if(have_to_rename(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; } diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index 14765af113f..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,31 +95,24 @@ 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)); + 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))); - if(!replace(type)) - result=false; - } - - 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; } 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 +205,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;