[isabelle] Poly/ML crash in 64_32 mode · Mirror: Isabelle Users Mailing List

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.

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;

Email Gateway (Oct 09 2026 at 12:51):

I started to have a look at this report and have the following
preliminary analysis. (Read this with a grain of salt, as I am looking
at the code generator for the first time.)

The compiler runs out of registers while constructing the tuples and
temporarily saves values on the ML stack. The garbage collector scans
that stack to find live objects. Ordinary ML integers carry a tag that
distinguishes them from pointers, but compiler-generated tuple lengths
are raw, untagged numbers. Saving those lengths on the scanned stack can
therefore make GC mistake a number for a pointer.

The register allocator has a spill-selection heuristic and a fallback
used when actual register assignment fails. The normal heuristic ranks
untagged values last; the fallback lacks the corresponding restriction.

A tentative change would make the ARM64 fallback skip RegPropUntagged
and RegPropMultiple, alongside RegPropStack. This could prevent
selection of untagged temporaries and conditional-result registers that
must not be spilled.

However, I am still puzzled by the fact the x86 does not exhibit the
same behaviour; its code does not seem to have special check for this,
but I failed to produce a SML program proving that this could still happen.

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) (a11: int ref) (a12: int ref) =
let val ch = String.sub (s, 1) in (
(a1, a2),
(a3, a4),
(a5, a6),
(a6, a7),
(a7, a8),
(a9, a1),
(a11, a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a1, a11, a12, a1,
a2, a3, a4, a5, a6, a7, a8),
(a12, a1, a2, a3, a4, a5, a6, a7, a8, a9, a1, a11, a12, a1, a2, a3,
a4, a5, a6, a7, a8, a9, a1, a11),
(a1, a2),
(a2, a3),
(a3, a4),
(a4, a5),
(a5, a6),
(a6, a7),
(a7, a8),
(a8, a9),
(a9, a1),
(a12, a1),
(a1, a2, a3, a4, a5, a6, a7, a8, a9, a1, a11, a12, a1, a2, a3, a4,
a5, a6, a7, a8, a9, a1),
(a2, a3)
) end;

fun work 0 acc = acc
| work n acc =
let val t = f "xyz" (ref 0) (ref 0) (ref 0) (ref 0) (ref 0) (ref 0)
(ref 0) (ref 0) (ref 0) (ref 0) (ref 0)
in work (n - 1) (acc + !(#1 (#1 t))) end;

val result = work 2000000 0
val _ = if result = 0 then () else raise Fail "wrong result";

Email Gateway (Oct 09 2026 at 12:53):

Hi,
Thank you for reporting this and cutting it down to a workable example.
I do sometimes check the Isabelle mailing lists for reports like this
but generally the best way to report a problem with Poly/ML is to raise
an issue on the Poly/ML GitHub site at https://github.com/polyml/polyml.

Email Gateway (Oct 12 2026 at 13:16):

at this rather late stage of the Isabelle2026 release process, I need to
distinguish isabelle-users threads that are relevant to it from those that are
for later ("Not now, not for this release").

So I have collected the attached examples bad1.ML + bad2.ML from this thread
and made some quick tests on the following machine:

- bad1.ML: OK
- bad2.ML: crash of poly
Isabelle2023, Isabelle2024, Isabelle2025, Isabelle2025-2:

On Isabelle2026-RC3, it does work for arm64-darwin and x86_64_32-darwin. (For
Isabelle2026-RC4 the x86_64 variants of Poly/ML will be included in the
regular macos_arm distribution again --- they were absent before, due to the
split of "macos" vs. "macos_arm".)

Overall it looks like the arm64_32 codegenerator was never quite right for
this rather unusual use of Poly/ML. The example appears to emulate mutable
records, but we never do that in Isabelle/ML as far as I can tell.

My current conclusion: This incident is not relevant for the Isabelle2026, and
there is plenty of time to revisit ARM64 code generation later, not in a rush.

Side-remark: It is certainly possible to break Poly/ML, Isabelle/ML,
Isabelle/Scala in many ways, by using it in so far unprecented ways. Our usual
working assumption is that applications are somewhere in the inhabitable area
defined by Isabelle Distribution + AFP, which is already quite a lot of open
space and variance.

Email Gateway (Oct 12 2026 at 13:31):

I can see that this has been fixed on the Poly/ML repository already, so users who experience the issue can upgrade manually. Many thanks for the fast turnaround, Dave.

CAUTION: This email originated from outside of the organization. Do not click links or open attachments unless you can confirm the sender and know the content is safe.

at this rather late stage of the Isabelle2026 release process, I need to
distinguish isabelle-users threads that are relevant to it from those that are
for later ("Not now, not for this release").

So I have collected the attached examples bad1.ML + bad2.ML from this thread
and made some quick tests on the following machine:

- bad1.ML: OK
- bad2.ML: crash of poly
Isabelle2023, Isabelle2024, Isabelle2025, Isabelle2025-2:

My current conclusion: This incident is not relevant for the Isabelle2026, and
there is plenty of time to revisit ARM64 code generation later, not in a rush.

Email Gateway (Oct 12 2026 at 14:19):

Here David Matthews says "Do not include untagged or cached untagged registers
in the set of registers to be pushed. Fixes #320 subject to testing."

I sincerely hope that the difference of a proper release --- of anything, not
just Poly/ML + Isabelle --- vs. arbitrary repository versions is clear. Or
maybe not?

Anyway, as long there is no additional reasoning, I leave this thread as "not
relevant for the Isabelle2026 release".

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Poly/ML crash in 64_32 mode

Email Gateway (Oct 06 2026 at 10:59):

Email Gateway (Oct 09 2026 at 12:51):

Email Gateway (Oct 09 2026 at 12:53):

Email Gateway (Oct 12 2026 at 13:16):

Email Gateway (Oct 12 2026 at 13:31):

Email Gateway (Oct 12 2026 at 14:19):