From 334fa475b4345f80a4e196ff921ff0bcf10f21e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 27 Oct 2025 11:16:59 +0100 Subject: [PATCH] fix: use general allocator for closures (#10982) This PR changes the closure allocator to use the general allocator instead of the small object one. This is because users may create closures with a gigantic amount of closed variables which in turn boost the size of the closure beyond the small object threshold. This issue was uncovered by #10979. Detecting that the small object threshold is at fault requires building mimalloc in debug mode at which point it yields: ``` mimalloc: assertion failed: at "/home/henrik/lean4/build/debug/mimalloc/src/mimalloc/src/alloc.c":132, mi_heap_malloc_small_zero assertion: "size <= MI_SMALL_SIZE_MAX" ``` The generated code at fault here looks as follows: ```c LEAN_EXPORT lean_object* l_initExec___at___00res_spec__0(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; x_2 = lean_alloc_closure((void*)(l_initializer_ext___at___00initExec___at___00res_spec__0_spec__0___lam__0___boxed), 3, 0); x_3 = l_initExec___redArg___closed__0; x_4 = l_initExec___redArg___closed__1; x_5 = l_instMonadLiftNonDetT___closed__0; x_6 = l_initExec___redArg___closed__2; x_7 = l_initExec___at___00res_spec__0___closed__0; lean_inc_ref(x_2); x_8 = lean_alloc_closure((void*)(l_initExec___at___00res_spec__0___lam__29___boxed), 213, 212); lean_closure_set(x_8, 0, x_3); lean_closure_set(x_8, 1, x_2); lean_closure_set(x_8, 2, x_4); lean_closure_set(x_8, 3, x_3); lean_closure_set(x_8, 4, x_4); lean_closure_set(x_8, 5, x_3); lean_closure_set(x_8, 6, x_4); lean_closure_set(x_8, 7, x_3); lean_closure_set(x_8, 8, x_4); lean_closure_set(x_8, 9, x_3); lean_closure_set(x_8, 10, x_4); lean_closure_set(x_8, 11, x_3); lean_closure_set(x_8, 12, x_4); lean_closure_set(x_8, 13, x_3); lean_closure_set(x_8, 14, x_4); lean_closure_set(x_8, 15, x_5); lean_closure_set(x_8, 16, x_6); lean_closure_set(x_8, 17, x_5); lean_closure_set(x_8, 18, x_5); lean_closure_set(x_8, 19, x_5); lean_closure_set(x_8, 20, x_5); lean_closure_set(x_8, 21, x_5); lean_closure_set(x_8, 22, x_5); ... ``` With the crash happening in `lean_alloc_closure` where we unconditionally invoke the small allocator which cannot cope with closures this large. Hopefully changing this to the general purpose allocator doesn't have too much of an impact on performance. Closes: #10979 --- src/include/lean/lean.h | 2 +- tests/compiler/large_closure_bug.lean | 258 ++++++++++++++++++ .../large_closure_bug.lean.expected.out | 1 + 3 files changed, 260 insertions(+), 1 deletion(-) create mode 100644 tests/compiler/large_closure_bug.lean create mode 100644 tests/compiler/large_closure_bug.lean.expected.out diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 922538497b..b3ae906c79 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -715,7 +715,7 @@ static inline lean_object ** lean_closure_arg_cptr(lean_object * o) { return lea static inline lean_obj_res lean_alloc_closure(void * fun, unsigned arity, unsigned num_fixed) { assert(arity > 0); assert(num_fixed < arity); - lean_closure_object * o = (lean_closure_object*)lean_alloc_small_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed); + lean_closure_object * o = (lean_closure_object*)lean_alloc_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed); lean_set_st_header((lean_object*)o, LeanClosure, 0); o->m_fun = fun; o->m_arity = arity; diff --git a/tests/compiler/large_closure_bug.lean b/tests/compiler/large_closure_bug.lean new file mode 100644 index 0000000000..b0710b0994 --- /dev/null +++ b/tests/compiler/large_closure_bug.lean @@ -0,0 +1,258 @@ +import Lean +import Std + +abbrev IteratedProd (ts : List Type) : Type := + ts.foldr Prod Unit + +abbrev IteratedArrow (codomain : Type) (ts : List Type) : Type := + ts.foldr (· → ·) codomain + +section IteratedProdInstances + +macro "infer_instance_for_iterated_prod" : tactic => + `(tactic| repeat' (first | infer_instance | constructor )) + +end IteratedProdInstances + +section SingleField + +variable (fieldDomain : List Type) (FieldCodomain : Type) + +local macro "⌞" t1:ident t2:ident* "⌟" : term => `($t1 $(Lean.mkIdent `fieldDomain) $t2:ident*) +local macro "⌞_" t1:ident t2:ident* "⌟" : term => `(⌞ $t1 $(Lean.mkIdent `FieldCodomain) $t2:ident* ⌟) + +abbrev FieldUpdatePat : Type := IteratedProd (fieldDomain.map Option) + +abbrev CanonicalField : Type := IteratedArrow FieldCodomain fieldDomain + +abbrev FieldUpdateDescr := List (⌞ FieldUpdatePat ⌟ × ⌞_ CanonicalField ⌟) + +class FieldRepresentation (FieldTypeConcrete : Type) where + set : ⌞_ FieldUpdateDescr ⌟ → FieldTypeConcrete → FieldTypeConcrete + +instance canonicalFieldRepresentation {fieldDomain : List Type} {FieldCodomain : Type} : + (⌞_ FieldRepresentation ⌟) (⌞_ CanonicalField ⌟) where + set favs fc := favs.foldr (init := fc) fun (_, v) _ => v + +end SingleField + +inductive NonDetT (m : Type u -> Type v) : (α : Type u) -> Type _ where + | pure {α} (ret : α) : NonDetT m α + | vis {α} {β} (x : m β) (f : β → NonDetT m α) : NonDetT m α + +def NonDetT.bind (x : NonDetT m α) (f : α → NonDetT m β) : NonDetT m β := + match x with + | pure ret => f ret + | vis x f' => vis x fun y => bind (f' y) f + +instance : Monad (NonDetT m) where + pure := NonDetT.pure + bind := NonDetT.bind + +instance : MonadLift m (NonDetT m) where + monadLift x := NonDetT.vis x pure + +abbrev VeilM (σ α : Type) := NonDetT ((StateT σ (ExceptT Int Option))) α + +inductive ExtractNonDet {m} : {α : Type u} -> NonDetT m α -> Type _ where + | pure {α} : ∀ (x : α), ExtractNonDet (NonDetT.pure x) + | vis {α} {β} (x : m β) (f : β → NonDetT m α) : + (∀ y, ExtractNonDet (f y)) → ExtractNonDet (.vis x f) + +set_option linter.unusedVariables false in +def ExtractNonDet.bind : + (_ : ExtractNonDet x) -> (_ : ∀ y, ExtractNonDet (f y)) -> ExtractNonDet (x >>= f) + | .pure x, inst => by + dsimp [Bind.bind, NonDetT.bind]; exact (inst x) + | .vis x f inst, inst' => by + dsimp [Bind.bind, NonDetT.bind]; constructor + intro y; apply ExtractNonDet.bind <;> solve_by_elim + +instance ExtractNonDet.pure' : ExtractNonDet (Pure.pure (f := NonDetT m) x) := by + dsimp [Pure.pure, NonDetT.pure]; constructor + +instance ExtractNonDet.liftM (x : m α) : + ExtractNonDet (liftM (n := NonDetT m) x) := by + dsimp [_root_.liftM, monadLift, MonadLift.monadLift]; constructor + intro y; apply ExtractNonDet.pure' + +macro "extract_step" : tactic => + `(tactic| + first + | apply ExtractNonDet.bind + | apply ExtractNonDet.pure' + | apply ExtractNonDet.liftM + | split ) + +macro "extract_tactic" : tactic => + `(tactic| repeat' (intros; extract_step <;> try dsimp)) + +abbrev VeilExecM (ε σ α : Type) := σ → Option (Except ε (α × σ)) + +def NonDetT.extract {α : Type} : (s : VeilM σ α) → (ex : ExtractNonDet s) → VeilExecM Int σ α + | .pure x, _ => fun s => (Option.some (Except.ok (x, s))) + | .vis x f, .vis _ _ _ => + fun s => + match x s with + | Option.some (Except.ok (y, s')) => + extract (f y) (by rename_i a ; exact a y) s' + | Option.none => (Option.none) + | Option.some (Except.error e) => (Option.some (Except.error e)) + +inductive State.Label : Type where + | m_client_request + | m_marked_client_request + +def State.Label.toDomain (l : State.Label) : List Type := + State.Label.casesOn l [Bool] [Bool, Bool, Bool] + +structure State (χ : State.Label → Type) where mk :: + m_client_request : χ State.Label.m_client_request + m_marked_client_request : χ State.Label.m_marked_client_request + +def initializer.ext {χ : State.Label → Type} + [χ_rep : (f : State.Label) → + FieldRepresentation (State.Label.toDomain f) Bool (χ f)] : VeilM (State χ) Unit := +do + let mut __veil_state := (← MonadState.get) + let mut m_client_request_conc := __veil_state.m_client_request + let mut m_marked_client_request_conc := __veil_state.m_marked_client_request + + let __veil_bind_m_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())), + (fun _ => (false)))] m_client_request_conc + m_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request }))) + let __veil_bind_m_marked_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())), + (fun _ _ _ => (false)))] m_marked_client_request_conc + m_marked_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_marked_client_request, + { st with m_marked_client_request := __veil_bind_m_marked_client_request }))) + + -- NOTE: the following are just multiple copy & pastes of the do-elements above + let __veil_bind_m_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())), + (fun _ => (false)))] m_client_request_conc + m_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request }))) + let __veil_bind_m_marked_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())), + (fun _ _ _ => (false)))] m_marked_client_request_conc + m_marked_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_marked_client_request, + { st with m_marked_client_request := __veil_bind_m_marked_client_request }))) + + let __veil_bind_m_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())), + (fun _ => (false)))] m_client_request_conc + m_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request }))) + let __veil_bind_m_marked_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())), + (fun _ _ _ => (false)))] m_marked_client_request_conc + m_marked_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_marked_client_request, + { st with m_marked_client_request := __veil_bind_m_marked_client_request }))) + + let __veil_bind_m_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())), + (fun _ => (false)))] m_client_request_conc + m_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request }))) + let __veil_bind_m_marked_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())), + (fun _ _ _ => (false)))] m_marked_client_request_conc + m_marked_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_marked_client_request, + { st with m_marked_client_request := __veil_bind_m_marked_client_request }))) + + let __veil_bind_m_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())), + (fun _ => (false)))] m_client_request_conc + m_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request }))) + let __veil_bind_m_marked_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())), + (fun _ _ _ => (false)))] m_marked_client_request_conc + m_marked_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_marked_client_request, + { st with m_marked_client_request := __veil_bind_m_marked_client_request }))) + + let __veil_bind_m_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())), + (fun _ => (false)))] m_client_request_conc + m_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request }))) + let __veil_bind_m_marked_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())), + (fun _ _ _ => (false)))] m_marked_client_request_conc + m_marked_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_marked_client_request, + { st with m_marked_client_request := __veil_bind_m_marked_client_request }))) + + let __veil_bind_m_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())), + (fun _ => (false)))] m_client_request_conc + m_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request }))) + let __veil_bind_m_marked_client_request := + (χ_rep _).set + [((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())), + (fun _ _ _ => (false)))] m_marked_client_request_conc + m_marked_client_request_conc ← + MonadState.modifyGet + (fun st => + ((__veil_bind_m_marked_client_request, + { st with m_marked_client_request := __veil_bind_m_marked_client_request }))) + +def initExec (χ : State.Label → Type) [χ_rep : ∀ f, FieldRepresentation (State.Label.toDomain f) Bool (χ f)] + : VeilExecM Int (State χ) Unit := + NonDetT.extract (@initializer.ext χ χ_rep) (by (extract_tactic)) + +def res := initExec (fun f => CanonicalField ( (State.Label.toDomain) f) Bool) { + m_client_request := fun _ => false, + m_marked_client_request := fun _ _ _ => false + } + +def main : IO Unit := + IO.println s!"{[res].length}" diff --git a/tests/compiler/large_closure_bug.lean.expected.out b/tests/compiler/large_closure_bug.lean.expected.out new file mode 100644 index 0000000000..d00491fd7e --- /dev/null +++ b/tests/compiler/large_closure_bug.lean.expected.out @@ -0,0 +1 @@ +1