Email Gateway (Oct 06 2026 at 10:59): Email Gateway (Oct 06 2026 at 10:59):From: "Becker, Hanno" <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I see recurring crashes in Poly/ML's 64_32 mode on ARM64.
It appears that a raw value can be spilled onto the ML stack and then interpreted as an object during GC. I leave the proper diagnosis and proper fix to the experts.
I tested the reproducer below with polyml-5.9.2-2, polyml-5.9.2-4, and polyml-5.9.2-5 shipped in Isabelle-2026-RC3. It’s an artificial example, but the problem was encountered “in the wild”.
$ poly < reproducer.sml
poly: .../polyml-5.9.2-4/src/libpolyml/quick_gc.cpp:394: virtual PolyObject* QuickGCScanner::ScanObjectAddress(PolyObject*): Assertion `space != 0' failed.
Regards,
Hanno
===
reproducer.sml:
fun f (s: string) (a1: int ref) (a2: int ref) (a3: int ref) (a4: int ref) (a5: int ref) (a6: int ref) (a7: int ref) (a8: int ref) (a9: int ref) (a10: int ref) (a11: int ref) (a12: int ref) =
let val ch = String.sub (s, 1) in (
(a1, a2),
(a2, a3, a4, a5),
(a3, a4, a5, a6, a7, a8),
(a4, a5, a6, a7, a8, a9, a10, a11),
(a5, a6, a7, a8, a9, a10, a11, a12, a1, a2),
(a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5),
(a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8),
(a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11),
(a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2),
(a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5),
(a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8),
(a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11),
(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2),
(a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5),
(a3, a4),
(a4, a5, a6, a7),
(a5, a6, a7, a8, a9, a10),
(a6, a7, a8, a9, a10, a11, a12, a1),
(a7, a8, a9, a10, a11, a12, a1, a2, a3, a4),
(a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7),
(a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10),
(a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1),
(a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4),
(a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7),
(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10),
(a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1),
(a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4),
(a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7),
(a5, a6),
(a6, a7, a8, a9),
(a7, a8, a9, a10, a11, a12),
(a8, a9, a10, a11, a12, a1, a2, a3),
(a9, a10, a11, a12, a1, a2, a3, a4, a5, a6),
(a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9),
(a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12),
(a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3),
(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6),
(a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9),
(a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12),
(a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3),
(a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6),
(a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9)
) end;
fun work 0 acc = acc
| work n acc =
let val t = f "xyz" (ref 1) (ref 2) (ref 3) (ref 4) (ref 5) (ref 6)
(ref 7) (ref 8) (ref 9) (ref 10) (ref 11) (ref 12)
in work (n - 1) (acc + !(#1 (#1 t))) end;
val _ = work 2000000 0;
Last updated: Oct 08 2026 at 21:07 UTC