From 29eeb0d4e87c34bcec80f405cdad68dd1af0e54a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 22 Jul 2026 08:41:22 +0000 Subject: [PATCH] Share object maps in value_sett::make_union when destination is empty The object_mapt representation is reference counted precisely so that multiple owners can share one map, yet make_union built the union element by element even when the destination was empty. Value-set queries for a single symbol (via get_value_set_rec) arrive here with an empty destination, so each such query copied the symbol's entire object map, including one std::optional offset per element. Sharing the source map instead makes this constant time and removes the dominant allocation churn from value-set queries in symbolic execution. Co-authored-by: Kiro --- src/pointer-analysis/value_set.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index aad9ae75f69..3ac056bb9a8 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -319,6 +319,20 @@ bool value_sett::make_union_would_change( bool value_sett::make_union(object_mapt &dest, const object_mapt &src) const { + if(src.read().empty()) + return false; + + // If the destination is empty we can just share the (reference-counted) + // representation of `src` instead of inserting elements one by one. Queries + // over a single symbol repeatedly arrive here with an empty destination, so + // this turns an operation that is linear in the size of the value set (with + // all the allocation work that entails) into a constant-time one. + if(dest.read().empty()) + { + dest = src; + return true; + } + bool result=false; for(object_map_dt::const_iterator it=src.read().begin();