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

@@ -21,22 +21,14 @@ Author: Daniel Kroening, [email protected]
 #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;
 }

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)
   {

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));
 }