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 cb24a9b364cb..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 @@ -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); } 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