From 2fbecc3545deeb3216d67a15858f9c7e23a0340f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 24 Jun 2026 08:29:14 +0000 Subject: [PATCH] util: amortise symbol_table_baset::next_unused_suffix next_unused_suffix(prefix) restarted its linear scan from 0 on every call, so allocating N names that share a prefix (as the object factory does) costs O(N^2). Add a per-prefix "next search-start" hint to the base so repeated allocation under the same prefix is amortised O(1). The hint is looked up with try_emplace so the common cache-hit path does not construct/copy the prefix key. The returned suffix is now unused but no longer necessarily the smallest; no caller relies on minimality. This generalises a hint cache that symbol_table_buildert already maintained with the same relaxed semantics, so its now-redundant override (and duplicate cache) is removed; the builder resets the inherited cache on clear(), as does symbol_tablet. namespacet::smallest_unused_suffix's docstring is updated to describe the relaxed, now-stateful contract. It no longer over-claims a global cross-table guarantee: with multiple tables the result is the maximum of each table's per-table value, which is unused in every table only when the tables allocate suffixes monotonically from 0 (as auto-generated symbols do); the single-table common case yields a globally unused suffix. A thread-safety note is added to the base cache. Unit tests cover the new semantics: repeated allocation returns distinct increasing suffixes; uniqueness still holds after erase + re-allocation; clear() resets the hint so allocation restarts at 0; and the same holds through a symbol_table_buildert wrapper, exercising the inherited (no longer overridden) implementation and the builder's cache reset. Co-authored-by: Kiro --- src/util/namespace.h | 22 +++++-- src/util/symbol_table.h | 1 + src/util/symbol_table_base.h | 42 ++++++++++++- src/util/symbol_table_builder.h | 30 ++------- unit/util/symbol_table.cpp | 105 ++++++++++++++++++++++++++++++++ 5 files changed, 168 insertions(+), 32 deletions(-) diff --git a/src/util/namespace.h b/src/util/namespace.h index 1594fea198d..5e0a11d79d7 100644 --- a/src/util/namespace.h +++ b/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; diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index a6fa8b798fe..3f740f991f9 100644 --- a/src/util/symbol_table.h +++ b/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 diff --git a/src/util/symbol_table_base.h b/src/util/symbol_table_base.h index 976d108f4b7..f3acc4ac727 100644 --- a/src/util/symbol_table_base.h +++ b/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 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 & diff --git a/src/util/symbol_table_builder.h b/src/util/symbol_table_builder.h index 28046919de6..19d8be0f53d 100644 --- a/src/util/symbol_table_builder.h +++ b/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 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 diff --git a/unit/util/symbol_table.cpp b/unit/util/symbol_table.cpp index 88371873147..87b30e6c2c7 100644 --- a/unit/util/symbol_table.cpp +++ b/unit/util/symbol_table.cpp @@ -5,6 +5,7 @@ #include // IWYU pragma: keep #include #include +#include #include #include @@ -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); +}