russell@unturf.com
ae6e04c5bd
lean4-0004: collapse 3-phase lock in ir_interpreter lookup_symbol to single unique_lock lean4-0005: replace IO.Ref JobQueue with Std.Mutex in Lake job registry lean4-0006: register thread-local reset for g_opts in kernel/trace.cpp lean4-0007: build unordered_set of override keys outside env-var loop (Windows)
55 lines
2.7 KiB
Diff
55 lines
2.7 KiB
Diff
# 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;
|
|
}
|