From ff25b2cffd01f81b1bf89ded2473f6172e551ff6 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 29 May 2018 15:11:44 +0100
Subject: [PATCH] get_max: do not parse every symbol name in the symbol table

The typical case is that we have a small number of entries with the same
prefix. Just perform that small number of name lookups (which are
constant time after the log-time conversion from a string to an
irep_idt). This speeds up function pointer removal on a build of the
Linux kernel from 4610 seconds to just 86 seconds.

Also rename get_max to smallest_unused_suffix to disambiguate the case
of a symbol not being present, which in turn simplifies the use.
---
 src/util/namespace.cpp | 36 +++++++++++++-----------------------
 src/util/namespace.h   | 14 +++++++-------
 src/util/rename.cpp    |  2 +-
 3 files changed, 21 insertions(+), 31 deletions(-)

diff --git a/src/util/namespace.cpp b/src/util/namespace.cpp
index 5c98d53019e..255b97c8eb9 100644
--- a/src/util/namespace.cpp
+++ b/src/util/namespace.cpp
@@ -21,22 +21,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "string2int.h"
 #include "symbol_table.h"
 
-unsigned get_max(
+static std::size_t smallest_unused_suffix(
   const std::string &prefix,
   const symbol_tablet::symbolst &symbols)
 {
-  unsigned max_nr=0;
+  std::size_t max_nr = 0;
 
-  for(const auto &symbol_pair : symbols)
-  {
-    if(has_prefix(id2string(symbol_pair.first), prefix))
-    {
-      max_nr = std::max(
-        unsafe_string2unsigned(
-          id2string(symbol_pair.first).substr(prefix.size())),
-        max_nr);
-    }
-  }
+  while(symbols.find(prefix + std::to_string(max_nr)) != symbols.end())
+    ++max_nr;
 
   return max_nr;
 }
@@ -122,15 +114,15 @@ void namespace_baset::follow_macros(exprt &expr) const
     follow_macros(*it);
 }
 
-unsigned namespacet::get_max(const std::string &prefix) const
+std::size_t namespacet::smallest_unused_suffix(const std::string &prefix) const
 {
-  unsigned m=0;
+  std::size_t m = 0;
 
   if(symbol_table1!=nullptr)
-    m=std::max(m, ::get_max(prefix, symbol_table1->symbols));
+    m = std::max(m, ::smallest_unused_suffix(prefix, symbol_table1->symbols));
 
   if(symbol_table2!=nullptr)
-    m=std::max(m, ::get_max(prefix, symbol_table2->symbols));
+    m = std::max(m, ::smallest_unused_suffix(prefix, symbol_table2->symbols));
 
   return m;
 }
@@ -166,15 +158,13 @@ bool namespacet::lookup(
   return true;
 }
 
-unsigned multi_namespacet::get_max(const std::string &prefix) const
+std::size_t
+multi_namespacet::smallest_unused_suffix(const std::string &prefix) const
 {
-  unsigned m=0;
+  std::size_t m = 0;
 
-  for(symbol_table_listt::const_iterator
-      it=symbol_table_list.begin();
-      it!=symbol_table_list.end();
-      it++)
-    m=std::max(m, ::get_max(prefix, (*it)->symbols));
+  for(const auto &st : symbol_table_list)
+    m = std::max(m, ::smallest_unused_suffix(prefix, st->symbols));
 
   return m;
 }
diff --git a/src/util/namespace.h b/src/util/namespace.h
index a0edab235f3..94fdbe5df1c 100644
--- a/src/util/namespace.h
+++ b/src/util/namespace.h
@@ -53,12 +53,12 @@ class namespace_baset
   const typet &follow_tag(const struct_tag_typet &) const;
   const typet &follow_tag(const c_enum_tag_typet &) const;
 
-  /// Returns the maximum integer n such that there is a symbol (in some of the
-  /// symbol tables) whose name is of the form "AB" where A is \p prefix and B
-  /// is n.  Symbols where B is not a number count as if B was equal to 0.
+  /// Returns the minimal integer n such that there is no symbol (in any of the
+  /// symbol tables) whose name is of the form "An" where A is \p prefix.
   /// The intended use case is finding the next available symbol name for a
   /// sequence of auto-generated symbols.
-  virtual unsigned get_max(const std::string &prefix) const=0;
+  virtual std::size_t
+  smallest_unused_suffix(const std::string &prefix) const = 0;
 
   /// Searches for a symbol named \p name. Iff found, set \p symbol to point to
   /// the symbol and return false; else \p symbol is unmodified and `true` is
@@ -100,8 +100,8 @@ class namespacet:public namespace_baset
   /// tables.
   bool lookup(const irep_idt &name, const symbolt *&symbol) const override;
 
-  /// See documentation for namespace_baset::get_max().
-  unsigned get_max(const std::string &prefix) const override;
+  /// See documentation for namespace_baset::smallest_unused_suffix().
+  std::size_t smallest_unused_suffix(const std::string &prefix) const override;
 
   const symbol_tablet &get_symbol_table() const
   {
@@ -130,7 +130,7 @@ class multi_namespacet:public namespacet
   using namespace_baset::lookup;
 
   bool lookup(const irep_idt &name, const symbolt *&symbol) const override;
-  unsigned get_max(const std::string &prefix) const override;
+  std::size_t smallest_unused_suffix(const std::string &prefix) const override;
 
   void add(const symbol_tablet &symbol_table)
   {
diff --git a/src/util/rename.cpp b/src/util/rename.cpp
index 17645508ebf..8f5c769d423 100644
--- a/src/util/rename.cpp
+++ b/src/util/rename.cpp
@@ -32,5 +32,5 @@ void get_new_name(irep_idt &new_name, const namespacet &ns, char delimiter)
 
   std::string prefix = id2string(new_name) + delimiter;
 
-  new_name=prefix+std::to_string(ns.get_max(prefix)+1);
+  new_name = prefix + std::to_string(ns.smallest_unused_suffix(prefix));
 }