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)
40 lines
1.5 KiB
Diff
40 lines
1.5 KiB
Diff
# UNDF: UNDF-2026-000001264
|
|
# CWE-668: Leaked Context -- LEAN_THREAD_PTR(g_opts) not reset at task boundaries
|
|
#
|
|
# Defect: g_opts is set per elaboration invocation but never cleared on task
|
|
# completion. Thread pool reuse causes new task to inherit prior task's trace
|
|
# options. Incorrect trace output; potential info leak across elab contexts.
|
|
#
|
|
# Fix: reset g_opts to nullptr in thread finalizer / task boundary cleanup.
|
|
# Consistent with reset_thread_local() pattern used elsewhere in runtime.
|
|
#
|
|
# Complexity gate: correctness -- trace output isolated per task under concurrent elaboration
|
|
--- a/src/kernel/trace.cpp
|
|
+++ b/src/kernel/trace.cpp
|
|
@@ -6,10 +6,11 @@ Author: Leonardo de Moura
|
|
*/
|
|
#include <vector>
|
|
#include <string>
|
|
#include "util/io.h"
|
|
#include "util/option_declarations.h"
|
|
#include "library/elab_environment.h"
|
|
#include "kernel/local_ctx.h"
|
|
#include "kernel/trace.h"
|
|
+#include "runtime/thread.h"
|
|
|
|
namespace lean {
|
|
LEAN_THREAD_PTR(const options, g_opts);
|
|
@@ -52,7 +53,14 @@ std::ostream & operator<<(std::ostream & ios, tclass const & c) {
|
|
}
|
|
|
|
void initialize_trace() {
|
|
+ // Register a reset function so that reset_thread_local() (called before
|
|
+ // each task starts on a reused thread) clears g_opts to nullptr.
|
|
+ // Without this, a thread-pool thread retains the prior elaboration task's
|
|
+ // trace options and leaks them into the next task's trace output.
|
|
+ register_thread_local_reset_fn([]() {
|
|
+ g_opts = nullptr;
|
|
+ });
|
|
}
|
|
|
|
void finalize_trace() {
|