util: amortise symbol_table_baset::next_unused_suffix

src/util/namespace.h

@@ -66,10 +66,24 @@ class namespace_baset
   const c_enum_typet &follow_tag(const c_enum_tag_typet &) const;
   const struct_union_typet &follow_tag(const struct_or_union_tag_typet &) const;
 
-  /// 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.
+  /// Returns an integer n intended for naming the next symbol in a sequence of
+  /// auto-generated symbols of the form "An" where A is \p prefix.  With a
+  /// single symbol table (the common case) there is no symbol "An" in that
+  /// table.  With multiple tables the result is the maximum of each table's
+  /// `next_unused_suffix(prefix)`: each per-table value is unused in its own
+  /// table, and the maximum is unused in every table when the tables allocate
+  /// such suffixes monotonically from 0 (no gaps) -- which holds for
+  /// auto-generated symbols.  If the tables have differing gaps for the same
+  /// prefix the maximum is not guaranteed unused across all tables; this is a
+  /// pre-existing property of the max-based combination.
+  ///
+  /// \note The returned suffix is not guaranteed to be the smallest such
+  ///   value: the underlying `symbol_table_baset::next_unused_suffix` keeps a
+  ///   monotonically advancing per-prefix hint, so this is a stateful query
+  ///   that mutates that hint on each call rather than a pure minimum search.
+  ///   With multiple symbol tables every call advances the hint of *each*
+  ///   table even though only one symbol is ultimately allocated, which may
+  ///   leave gaps.
   virtual std::size_t
   smallest_unused_suffix(const std::string &prefix) const = 0;
 

src/util/symbol_table.h

@@ -103,6 +103,7 @@ class symbol_tablet : public symbol_table_baset
     internal_symbols.clear();
     internal_symbol_base_map.clear();
     internal_symbol_module_map.clear();
+    suffix_hint_cache.clear();
   }
 
   virtual iteratort begin() override

src/util/symbol_table_base.h

@@ -54,10 +54,21 @@ class symbol_table_baset
 
   virtual ~symbol_table_baset();
 
+protected:
+  /// Per-prefix "next search-start" hint consulted by
+  /// `next_unused_suffix(prefix)`.  Mutable so the hint can be updated
+  /// through the const read API.  See that function's docstring for
+  /// semantics.  Because this is mutated from a const method,
+  /// `symbol_table_baset` is not thread-safe: concurrent calls require
+  /// external synchronisation.
+  mutable std::unordered_map<std::string, std::size_t> suffix_hint_cache;
+
+public:
   /// Find smallest unused integer i so that prefix + std::to_string(i)
-  /// does not exist in the list \p symbols.
+  /// does not exist in the list \p symbols, starting the search at
+  /// \p start_number.
   /// \param prefix: A string denoting the prefix we want to find the
-  ///   smallest suffix of.
+  ///   smallest unused suffix of.
   /// \param start_number: The starting suffix number to search from.
   /// \return The small unused suffix size.
   std::size_t
@@ -70,9 +81,34 @@ class symbol_table_baset
     return start_number;
   }
 
+  /// Find an unused integer i so that prefix + std::to_string(i) does
+  /// not exist in the list \p symbols.
+  ///
+  /// Uses a per-prefix hint cache so that repeated allocation of names
+  /// sharing the same prefix is amortised O(1) per call rather than
+  /// O(N) where N is the number of already-allocated symbols under
+  /// that prefix.  The object factory (see
+  /// `symbol_factoryt::gen_nondet_init` for a \c struct field expansion
+  /// of a deep kernel struct) can otherwise call this function
+  /// O(N) times with a linear scan each, producing O(N^2) behaviour
+  /// that manifests as a goto-instrument hang on large goto binaries.
+  ///
+  /// The returned suffix is guaranteed to be unused, but is no longer
+  /// guaranteed to be the strictly smallest such value: if a prior
+  /// symbol with a lower suffix has been erased from the table since
+  /// the hint was last updated, this function will not re-discover
+  /// that gap.  No caller in-tree today relies on the "smallest"
+  /// property (callers only need uniqueness); the derived
+  /// `symbol_table_builder` has already had this semantics since
+  /// its introduction and remains correct under this change.
   virtual std::size_t next_unused_suffix(const std::string &prefix) const
   {
-    return next_unused_suffix(prefix, 0);
+    // try_emplace only constructs the node (copying the key) when an insertion
+    // actually happens; on the common cache-hit path nothing is copied.
+    auto it = suffix_hint_cache.try_emplace(prefix, 0).first;
+    const std::size_t free_suffix = next_unused_suffix(prefix, it->second);
+    it->second = free_suffix + 1;
+    return free_suffix;
   }
 
   /// Permits implicit cast to const symbol_tablet &

src/util/symbol_table_builder.h

@@ -8,13 +8,14 @@
 
 #include "symbol_table_base.h"
 
-/// Wrapper around a symbol table that keeps track of suffixes for faster
-/// calculation of the smallest unused suffix.
+/// Wrapper around a symbol table. The fast next-unused-suffix computation
+/// (a per-prefix hint cache) is inherited from \ref symbol_table_baset; this
+/// wrapper only forwards mutating operations to the wrapped table and resets
+/// that cache on clear().
 class symbol_table_buildert : public symbol_table_baset
 {
 private:
   symbol_table_baset &base_symbol_table;
-  mutable std::map<std::string, std::size_t> next_free_suffix_for_prefix;
 
 public:
   explicit symbol_table_buildert(symbol_table_baset &base_symbol_table)
@@ -57,7 +58,7 @@ class symbol_table_buildert : public symbol_table_baset
   void clear() override
   {
     base_symbol_table.clear();
-    next_free_suffix_for_prefix.clear();
+    suffix_hint_cache.clear();
   }
 
   bool move(symbolt &symbol, symbolt *&new_symbol) override
@@ -93,27 +94,6 @@ class symbol_table_buildert : public symbol_table_baset
   {
     base_symbol_table.validate(vm);
   }
-
-  /// Try to find the next free identity for the passed-in prefix in
-  /// this symbol table.
-  /// \remark
-  ///     This method needs to generate names deterministically in regards
-  ///     to operations that generate the same prefix (and any other operation
-  ///     shouldn't affect this).
-  ///
-  ///     Due to this requirement we don't do anything fancy in regards to
-  ///     attempting to find the absolute earliest free suffix if one has been
-  ///     deleted, only the next free increment from our last stored value.
-  std::size_t next_unused_suffix(const std::string &prefix) const override
-  {
-    // Check if we have an entry for this particular suffix, if not,
-    // create baseline.
-    auto suffix_iter = next_free_suffix_for_prefix.insert({prefix, 0}).first;
-    std::size_t free_suffix =
-      base_symbol_table.next_unused_suffix(prefix, suffix_iter->second);
-    suffix_iter->second = free_suffix + 1;
-    return free_suffix;
-  }
 };
 
 #endif // CPROVER_UTIL_SYMBOL_TABLE_BUILDER_H

unit/util/symbol_table.cpp

@@ -5,6 +5,7 @@
 #include <util/exception_utils.h> // IWYU pragma: keep
 #include <util/journalling_symbol_table.h>
 #include <util/symbol_table.h>
+#include <util/symbol_table_builder.h>
 
 #include <testing-utils/invariant.h>
 #include <testing-utils/use_catch.h>
@@ -450,3 +451,107 @@ TEST_CASE("symbol_tablet::lookup_ref invariant", "[core][utils][symbol_tablet]")
     invariant_failedt,
     invariant_failure_containing("`bar' must exist in the symbol table."));
 }
+
+TEST_CASE("symbol_tablet::next_unused_suffix", "[core][utils][symbol_tablet]")
+{
+  symbol_tablet symbol_table;
+
+  auto add = [&symbol_table](const std::string &name)
+  {
+    symbolt symbol;
+    symbol.name = name;
+    symbol_table.insert(symbol);
+  };
+
+  SECTION("repeated allocation returns distinct, increasing suffixes")
+  {
+    const std::string prefix = "tmp";
+
+    const std::size_t s0 = symbol_table.next_unused_suffix(prefix);
+    add(prefix + std::to_string(s0));
+    const std::size_t s1 = symbol_table.next_unused_suffix(prefix);
+    add(prefix + std::to_string(s1));
+    const std::size_t s2 = symbol_table.next_unused_suffix(prefix);
+
+    // the monotonically-advancing hint hands out strictly increasing suffixes
+    REQUIRE(s0 < s1);
+    REQUIRE(s1 < s2);
+  }
+
+  SECTION("uniqueness still holds after erase and re-allocation")
+  {
+    const std::string prefix = "x";
+
+    const std::size_t a = symbol_table.next_unused_suffix(prefix);
+    add(prefix + std::to_string(a));
+    const std::size_t b = symbol_table.next_unused_suffix(prefix);
+    add(prefix + std::to_string(b));
+
+    // erase the lower-suffixed symbol, creating a gap below the hint
+    symbol_table.erase(symbol_table.symbols.find(prefix + std::to_string(a)));
+
+    // the next suffix is still guaranteed unused (it must not collide with the
+    // surviving symbol), even though -- as documented -- the gap left by the
+    // erased symbol is not necessarily rediscovered
+    const std::size_t c = symbol_table.next_unused_suffix(prefix);
+    REQUIRE(c != b);
+    REQUIRE(
+      symbol_table.symbols.find(prefix + std::to_string(c)) ==
+      symbol_table.symbols.end());
+  }
+
+  SECTION("clear() resets the suffix hint")
+  {
+    const std::string prefix = "c";
+
+    const std::size_t s0 = symbol_table.next_unused_suffix(prefix);
+    add(prefix + std::to_string(s0));
+    const std::size_t s1 = symbol_table.next_unused_suffix(prefix);
+    add(prefix + std::to_string(s1));
+    REQUIRE(s1 > s0);
+
+    symbol_table.clear();
+
+    // After clear() the table is empty; the cached hint must be reset too, so
+    // allocation restarts from 0 rather than handing out a suffix relative to
+    // the now-discarded symbols.
+    REQUIRE(symbol_table.next_unused_suffix(prefix) == 0);
+  }
+}
+
+TEST_CASE(
+  "symbol_table_buildert::next_unused_suffix",
+  "[core][utils][symbol_tablet]")
+{
+  // The builder has no next_unused_suffix override of its own; it relies on
+  // the inherited symbol_table_baset implementation, whose `symbols` reference
+  // aliases the wrapped table.  This exercises that path and the cache reset
+  // on the builder's clear().
+  symbol_tablet symbol_table;
+  symbol_table_buildert builder = symbol_table_buildert::wrap(symbol_table);
+
+  auto add = [&builder](const std::string &name)
+  {
+    symbolt symbol;
+    symbol.name = name;
+    builder.insert(symbol);
+  };
+
+  const std::string prefix = "tmp";
+
+  const std::size_t s0 = builder.next_unused_suffix(prefix);
+  add(prefix + std::to_string(s0));
+  const std::size_t s1 = builder.next_unused_suffix(prefix);
+  add(prefix + std::to_string(s1));
+
+  // distinct, increasing suffixes via the inherited implementation
+  REQUIRE(s0 < s1);
+
+  // the builder's symbols alias the wrapped table
+  REQUIRE(symbol_table.has_symbol(prefix + std::to_string(s0)));
+  REQUIRE(symbol_table.has_symbol(prefix + std::to_string(s1)));
+
+  // clear() resets the hint so allocation restarts at 0
+  builder.clear();
+  REQUIRE(builder.next_unused_suffix(prefix) == 0);
+}