From df1b1f0d6beb500669b824e2a25ca73e0dd7ee45 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 29 Aug 2026 13:11:24 +0000 Subject: [PATCH 1/3] fix: use the correct calling convention when over-applying a closure in `lean_apply_m` This PR fixes a crash when more than 16 arguments are applied at once to a closure whose arity is at most 16. Deeply nested monad stacks can produce such applications, and the result was memory corruption rather than a clean call. `lean_apply_m` handles applications of more than 16 arguments. Its over-application branch invoked the closure through `FNN`, which passes arguments as an array. That convention is only correct for closures whose arity exceeds `LEAN_CLOSURE_MAX_ARGS`; below that the generated code takes its arguments separately, so the callee received the argument array in its first parameter and register garbage in the rest. The fixed-arity `lean_apply_N` functions already guard this, `lean_apply_15` even asserting `arity > 16` immediately before its `FNN` call. The over-application branch now applies the first `arity - fixed` arguments via `lean_apply_n`, which dispatches on the count and consumes the closure, and continues with the remainder. --- src/runtime/apply.cpp | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/src/runtime/apply.cpp b/src/runtime/apply.cpp index cb24a9b364cb..2205a5830fc5 100644 --- a/src/runtime/apply.cpp +++ b/src/runtime/apply.cpp @@ -890,12 +890,21 @@ if (arity == fixed + n) { lean_dec_ref(f); return r; } else if (arity < fixed + n) { - obj ** args = static_cast(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT - for (unsigned i = 0; i < fixed; i++) { lean_inc(fx(i)); args[i] = fx(i); } - for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i]; - obj * new_f = FNN(f)(args); - lean_dec_ref(f); - return lean_apply_n(new_f, n+fixed-arity, &as[arity-fixed]); + unsigned m = arity - fixed; + obj * new_f; + if (arity > LEAN_CLOSURE_MAX_ARGS) { + // `f`'s code takes its arguments as an array + obj ** args = static_cast(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT + for (unsigned i = 0; i < fixed; i++) { lean_inc(fx(i)); args[i] = fx(i); } + for (unsigned i = 0; i < m; i++) args[fixed+i] = as[i]; + new_f = FNN(f)(args); + lean_dec_ref(f); + } else { + // `f`'s code takes `arity` separate arguments, so it must not be invoked through `FNN`; + // `lean_apply_n` dispatches on `m` and consumes `f`. + new_f = lean_apply_n(f, m, as); + } + return lean_apply_n(new_f, n - m, &as[m]); } else { return fix_args(f, n, as); } From 216e13541be47e287fe166a1d3cfd7c265220c0d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 31 Aug 2026 15:04:29 +0000 Subject: [PATCH 2/3] fix: apply the `lean_apply_m` over-application fix in `script/apply.lean` `src/runtime/apply.cpp` is generated and carries a "DO NOT EDIT" header, so the fix has to live in `mkApplyM` in the generator. Regenerating now reproduces the committed `apply.cpp`. Also correct the generator path in the generated header, which still pointed at the long-gone `../../gen/apply.lean`. --- script/apply.lean | 23 ++++++++++++++++------- src/runtime/apply.cpp | 2 +- 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/script/apply.lean b/script/apply.lean index e072b45e1fb8..626f610b0f8e 100644 --- a/script/apply.lean +++ b/script/apply.lean @@ -132,12 +132,21 @@ if (arity == fixed + n) \{ lean_dec_ref(f); return r; } else if (arity < fixed + n) \{ - obj ** args = static_cast(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT - for (unsigned i = 0; i < fixed; i++) \{ lean_inc(fx(i)); args[i] = fx(i); } - for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i]; - obj * new_f = FNN(f)(args); - lean_dec_ref(f); - return lean_apply_n(new_f, n+fixed-arity, &as[arity-fixed]); + unsigned m = arity - fixed; + obj * new_f; + if (arity > LEAN_CLOSURE_MAX_ARGS) \{ + // `f`'s code takes its arguments as an array + obj ** args = static_cast(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT + for (unsigned i = 0; i < fixed; i++) \{ lean_inc(fx(i)); args[i] = fx(i); } + for (unsigned i = 0; i < m; i++) args[fixed+i] = as[i]; + new_f = FNN(f)(args); + lean_dec_ref(f); + } else \{ + // `f`'s code takes `arity` separate arguments, so it must not be invoked through `FNN`; + // `lean_apply_n` dispatches on `m` and consumes `f`. + new_f = lean_apply_n(f, m, as); + } + return lean_apply_n(new_f, n - m, &as[m]); } else \{ return fix_args(f, n, as); } @@ -186,7 +195,7 @@ Author: Leonardo de Moura def mkApplyCpp (max : Nat) : M Unit := do mkCopyright emit "// DO NOT EDIT, this is an automatically generated file -// Generated using script: ../../gen/apply.lean +// Generated using script: script/apply.lean #include \"runtime/apply.h\" namespace lean { #define obj lean_object diff --git a/src/runtime/apply.cpp b/src/runtime/apply.cpp index 2205a5830fc5..4fa46faf7a72 100644 --- a/src/runtime/apply.cpp +++ b/src/runtime/apply.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ // DO NOT EDIT, this is an automatically generated file -// Generated using script: ../../gen/apply.lean +// Generated using script: script/apply.lean #include "runtime/apply.h" namespace lean { #define obj lean_object From 7439c664a3800802223f3df4095eb85abd50a96a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 31 Aug 2026 15:19:36 +0000 Subject: [PATCH 3/3] test: add a regression test for `lean_apply_m` over-application Applies 20 arguments in one call to a chain of arity-1 closures, which segfaults without the `lean_apply_m` fix. --- tests/compile/apply_m_overapp.lean | 22 +++++++++++++++++++ .../compile/apply_m_overapp.lean.out.expected | 1 + 2 files changed, 23 insertions(+) create mode 100644 tests/compile/apply_m_overapp.lean create mode 100644 tests/compile/apply_m_overapp.lean.out.expected diff --git a/tests/compile/apply_m_overapp.lean b/tests/compile/apply_m_overapp.lean new file mode 100644 index 000000000000..f039eaa182ac --- /dev/null +++ b/tests/compile/apply_m_overapp.lean @@ -0,0 +1,22 @@ +/-! +This is a regression test reproducer for #14969. + +Applying more than `closureMaxArgs` arguments at once to a closure of smaller arity used the +array calling convention, which is only correct above that arity, and crashed. `Chain` keeps +every closure at arity 1, and `f` is opaque in `apply20` so that all 20 arguments are applied +in a single `lean_apply_m` call. +-/ + +abbrev Chain : Nat → Type + | 0 => Nat + | n + 1 => Nat → Chain n + +def mk : (n : Nat) → Chain n + | 0 => 42 + | n + 1 => fun _ => mk n + +@[noinline] def apply20 (f : Chain 20) : Nat := + f 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 + +def main : IO Unit := + IO.println (apply20 (mk 20)) diff --git a/tests/compile/apply_m_overapp.lean.out.expected b/tests/compile/apply_m_overapp.lean.out.expected new file mode 100644 index 000000000000..d81cc0710eb6 --- /dev/null +++ b/tests/compile/apply_m_overapp.lean.out.expected @@ -0,0 +1 @@ +42