# UNDF: UNDF-2026-000001262
# CWE-362: Race Condition -- double-checked locking in ir_interpreter lookup_symbol
#
# Defect: m_symbol_cache.find(fn) read without lock before shared_lock acquire.
#   On weakly-ordered architectures: stale/partial cache entry visible to caller.
#   Pattern: read-without-lock -> shared_lock -> unlock -> unique_lock -> insert.
#
# Fix: restructure to single lock phase. m_symbol_cache is instance-local (safe
#   to read without global lock). g_native_symbol_cache access consolidated under
#   one exclusive lock acquisition, eliminating the unsafe unlock+relock sequence.
#
# Complexity gate: correctness -- no data races under ThreadSanitizer
--- a/src/library/ir_interpreter.cpp
+++ b/src/library/ir_interpreter.cpp
@@ -826,26 +826,22 @@ namespace lean {
     /** \brief Return cached lookup result for given unmangled function name in the current binary. */
     symbol_cache_entry lookup_symbol(name const & fn) {
+        // m_symbol_cache is instance-local: no global lock needed for this check.
         auto e = m_symbol_cache.find(fn);
         if (e != m_symbol_cache.end()) {
             return e->second;
         }
-        std::shared_lock<std::shared_mutex> lock(*g_native_symbol_cache_mutex);
-        auto ne = g_native_symbol_cache->find(fn);
+        // Acquire exclusive lock once for all g_native_symbol_cache access.
+        // Eliminates the shared -> unlock -> unique upgrade sequence and its
+        // associated race window between the two acquisitions.
+        std::unique_lock<std::shared_mutex> lock(*g_native_symbol_cache_mutex);
+        auto ne = g_native_symbol_cache->find(fn);
         if (ne != g_native_symbol_cache->end()) {
             symbol_cache_entry e_new { get_decl(fn), ne->second };
+            lock.unlock();
             m_symbol_cache.insert({ fn, e_new });
             return e_new;
         }
-        lock.unlock();
-        std::unique_lock<std::shared_mutex> unique_lock(*g_native_symbol_cache_mutex);
-        ne = g_native_symbol_cache->find(fn);
-        if (ne != g_native_symbol_cache->end()) {
-            symbol_cache_entry e_new { get_decl(fn), ne->second };
-            m_symbol_cache.insert({ fn, e_new });
-            return e_new;
-        }
         symbol_cache_entry e_new { get_decl(fn), {nullptr, false} };
         if (m_prefer_native || decl_tag(e_new.m_decl) == decl_kind::Extern || has_init_attribute(m_env, fn)) {
             string_ref mangled = get_symbol_stem(m_env, fn);
@@ -862,6 +858,8 @@ namespace lean {
                 }
             }
         }
         g_native_symbol_cache->insert({ fn, e_new.m_native });
+        lock.unlock();
         m_symbol_cache.insert({ fn, e_new });
         return e_new;
     }