From 3c32607020c48cd58a3494007566e12f92fafd84 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 17 Mar 2026 10:24:57 +0100 Subject: [PATCH] fix: incorrect borrow annotation on `demangleBtLinCStr` leading to segfault on panic (#12939) --- src/Lean/Compiler/NameDemangling.lean | 6 +----- src/runtime/object.cpp | 6 ++---- 2 files changed, 3 insertions(+), 9 deletions(-) diff --git a/src/Lean/Compiler/NameDemangling.lean b/src/Lean/Compiler/NameDemangling.lean index 235a6006d4..0570409b09 100644 --- a/src/Lean/Compiler/NameDemangling.lean +++ b/src/Lean/Compiler/NameDemangling.lean @@ -333,11 +333,7 @@ public def demangleBtLine (line : String) : Option String := do return pfx ++ demangled ++ sfx @[export lean_demangle_bt_line_cstr] -def demangleBtLineCStr (line : @& String) : String := +def demangleBtLineCStr (line : String) : String := (demangleBtLine line).getD "" -@[export lean_demangle_symbol_cstr] -def demangleSymbolCStr (symbol : @& String) : String := - (demangleSymbol symbol).getD "" - end Lean.Name.Demangle diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index aefb0064ab..313f2462fb 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -34,7 +34,7 @@ Author: Leonardo de Moura // Lean-exported demangler from Lean.Compiler.NameDemangling. // Declared as a weak symbol so leanrt doesn't require libLean at link time. // When the Lean demangler is linked in, it overrides this stub. -extern "C" __attribute__((weak)) lean_object * lean_demangle_bt_line_cstr(lean_object * s) { +extern "C" __attribute__((weak)) lean_obj_res lean_demangle_bt_line_cstr(lean_obj_arg s) { lean_dec(s); return lean_mk_string(""); } @@ -150,11 +150,9 @@ static void print_backtrace(bool force_stderr) { if (result_str[0] != '\0') { panic_eprintln(result_str, force_stderr); lean_dec(result); - lean_dec(line_obj); continue; } lean_dec(result); - lean_dec(line_obj); } panic_eprintln(symbols[i], force_stderr); } @@ -791,7 +789,7 @@ class task_manager { // idle before picking up new work. // But during shutdown, we skip this throttling: // because the finalizer might have called m_queue_cv.notify_all() for the last - // time, we don't want to get stuck behind the wait(). + // time, we don't want to get stuck behind the wait(). if (!m_shutting_down && m_std_workers.size() - m_idle_std_workers >= m_max_std_workers) { m_queue_cv.wait(lock);