Skip to content

Commit 7439c66

Browse files
committed
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.
1 parent 216e135 commit 7439c66

2 files changed

Lines changed: 23 additions & 0 deletions

File tree

‎tests/compile/apply_m_overapp.lean‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
/-!
2+
This is a regression test reproducer for #14969.
3+
4+
Applying more than `closureMaxArgs` arguments at once to a closure of smaller arity used the
5+
array calling convention, which is only correct above that arity, and crashed. `Chain` keeps
6+
every closure at arity 1, and `f` is opaque in `apply20` so that all 20 arguments are applied
7+
in a single `lean_apply_m` call.
8+
-/
9+
10+
abbrev Chain : Nat → Type
11+
| 0 => Nat
12+
| n + 1 => Nat → Chain n
13+
14+
def mk : (n : Nat) → Chain n
15+
| 0 => 42
16+
| n + 1 => fun _ => mk n
17+
18+
@[noinline] def apply20 (f : Chain 20) : Nat :=
19+
f 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
20+
21+
def main : IO Unit :=
22+
IO.println (apply20 (mk 20))
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
42

0 commit comments

Comments
 (0)