`lean_alloc_ctor` crashes under mimalloc for constructors larger than `MI_SMALL_SIZE_MAX`

[cpehle]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

lean_alloc_ctor(0, 121, 80) can crash under the mimalloc-backed runtime allocation path.

The allocation is a valid Lean-small constructor, but its size exceeds mimalloc’s mi_malloc_small limit. Lean currently calls mi_malloc_small(sz) unconditionally from
lean_alloc_small_object under LEAN_MIMALLOC.

On 64-bit platforms, the constructor size is:

sizeof(lean_ctor_object) + 121 * sizeof(void*) + 80
= 8 + 968 + 80
= 1056 bytes

Lean’s small-object limit is 4096 bytes, but mimalloc’s MI_SMALL_SIZE_MAX is 128 * sizeof(void*), i.e. 1024 bytes on 64-bit. So Lean can pass a Lean-small object that is too large for mimalloc’s direct-small allocation API.

Context

This was reproduced with a direct C runtime allocation against upstream origin/master at:

7559185

The relevant code path is in src/include/lean/lean.h:

#ifdef LEAN_MIMALLOC
      sz = lean_align(sz, LEAN_OBJECT_SIZE_DELTA);
      void * mem = mi_malloc_small(sz);

Possible fixes include either using mi_malloc(sz) for this path, or configuring Lean’s vendored mimalloc build so that MI_SMALL_SIZE_MAX >= LEAN_MAX_SMALL_OBJECT_SIZE.

Steps to Reproduce

1. Save this as repro.c:

     #include <lean/lean.h>
     #include <stdio.h>

     static void fill_ctor(lean_object * o) {
         for (unsigned i = 0; i < lean_ctor_num_objs(o); i++) {
             lean_ctor_set(o, i, lean_box(i));
         }

         uint8_t * scalars = lean_ctor_scalar_cptr(o);
         for (unsigned i = 0; i < 80; i++) {
             scalars[i] = (uint8_t)i;
         }
     }

     int main(void) {
         for (unsigned iter = 0; iter < 100000; iter++) {
             lean_object * o = lean_alloc_ctor(0, 121, 80);
             fill_ctor(o);
             lean_dec(o);
         }

         puts("ok");
         return 0;
     }

2. Build it against an affected Lean toolchain/runtime:

     cc repro.c \
       -I/path/to/lean/include \
       -L/path/to/lean/lib/lean \
       -Wl,-rpath,/path/to/lean/lib/lean \
       -lleanshared \
       -o repro

3. Run it:

     ./repro

Actual result:

Segmentation fault / exit 139

Expected result:

ok

[hargoniX]

Thanks for the bug report! This is addressed in #7786 which is currently waiting for mimalloc upstream to mark a new release but will hopefully be merged soon.

[cpehle]

Ok great. I was able to produce a local fix, but if there will be an upstream fix that sounds even better.