Merge pull request #2032 from tautschnig/replace-rename-performance

Improve performance replace_symbolt/rename_symbolt

Author: tautschnig

src/util/rename.cpp

@@ -8,10 +8,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "rename.h"
 
-#include <algorithm>
+#include <string>
 
 #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;
-}

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

src/util/rename_symbol.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #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<typet&>(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<const typet&>(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<typet&>(modifiable_expr->add(ID_C_c_sizeof_type)));
+    }
 
-  if(va_arg_type.is_not_nil() &&
-     !rename(static_cast<typet&>(dest.add(ID_C_va_arg_type))))
-    result=false;
+    const typet &va_arg_type =
+      static_cast<const typet&>(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<typet&>(modifiable_expr->add(ID_C_va_arg_type)));
+    }
+  }
 
   return result;
 }

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<typet &>(dest.add(ID_C_c_sizeof_type));
+  const typet &c_sizeof_type =
+    static_cast<const typet&>(dest.find(ID_C_c_sizeof_type));
+  if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type))
+    result &= replace(static_cast<typet&>(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<typet &>(dest.add(ID_C_va_arg_type));
-
-    if(!replace(type))
-      result=false;
-  }
+  const typet &va_arg_type =
+    static_cast<const typet&>(dest.find(ID_C_va_arg_type));
+  if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type))
+    result &= replace(static_cast<typet&>(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;