From df1b1f0d6beb500669b824e2a25ca73e0dd7ee45 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 29 Aug 2026 13:11:24 +0000 Subject: [PATCH] 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); }