Re: [MLton] Finding source code corresponding to failed type check of SSA after simplification

--===============7328467355626009249==
Content-Type: multipart/alternative; boundary="000000000000c5e65106461dd101"

--000000000000c5e65106461dd101
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

On Tue, Dec 16, 2025 at 6:37=E2=80=AFPM David Wang <[email protected]> w=
rote:

> I have now updated the instructions in the `Readme.md` and created a
> branch
> <https://github.com/david-wang-0/temporal-planning-certification/tree/com=
pilation>,
> where the problematic SML code produced by Isabelle is included.  Once th=
e
> dependencies are obtained using `git submodule update --init`, the comman=
ds
> `$ cd ML` and `$ make build_certifier_verbose` should work without
> involving Isabelle. `$ make build_certifier_verbose` emits the type
> checking error and `$ make build_certifier_unsafe` creates an executable
> that terminates with a segmentation fault.
>

Thanks; I was able to reproduce both the type error and the segmentation
fault.

Compiling with `-type-check true` (and without `-const 'MLton.safe
false'`), I observe:

         splitTypes2 starting
            splitTypes2:typeCheck starting
               splitTypes2:typeCheck raised: Fail: TypeError (SSA):
Ssa.TypeCheck.primApp (Array_copyArray(dBMEntry_0) ((dBMEntry_0) array,
word64, (dBMEntry_1) array, word64, word64)) in val _: unit =3D prim
Array_copyArray[dBMEntry_0] (x_2, global_0, x_1, global_0, x_0) in L_0 in
x_3
            splitTypes2:typeCheck raised in 0.12 + 0.00 (0% GC)
         splitTypes2 raised in 0.29 + 0.00 (0% GC)

This is essentially the same type error that was reported at the end of
`ssaSimplify`.  The internal type checking error is complaining about a use
of the `Array_copyArray` primitive.  In particular, it seeing a use of the
primitive where the arguments have types `((dBMEntry_0) array, word64,
(dBMEntry_1) array, word64, word64)`.  This is an error because this
primitive is copying elements from one array to another (implementing the
SML Basis library `Array.copy` function and others), where the intention is
that it will be further implemented by a `memcpy`; that means that the
source and destination arrays must have the same types, but the destination
is a `dBMEntry_0 array` while the source is a `dBMEntry_1 array`.  The
`splitTypes` optimization pass looks for opportunities to "split" datatypes
--- essentially duplicate datatype definitions so that distinct uses (i.e.,
ones that don't flow into one another) can have distinct types and,
therefore, be further optimized separately.  Of course, the array elements
participating in `Array_copyArray` *do* flow into one another and so they
should have their types split.

A quick look at the `splitTypes` implementation confirms that it does not
do anything "special" for `Array_copyArray` (or `Array_copyVector`), so the
analysis was free to separate those types.  The fix is trivial (
https://github.com/MLton/mlton/pull/632) and eliminates the internal SSA
type-checking error when compiling with `-type-check true` (and without
`-const 'MLton.safe false'`).

Investigating the `-const 'MLton.safe false'` will require more effort.
And, there is a reasonable chance that it isn't a compiler error.  `-const
'MLton.safe false'` isn't an advertised feature and its behavior isn't
checked by regression tests (or necessarily considered when developing the
compiler).  For example, somewhere in the Basis Library  implementation,
there may be an `exp handle Subscript =3D> ...` that relies upon a bounds
check to be raised and handled; omitting the bounds check and unsafely
reading or writing outside the bounds of the array could have all kinds of
misbehaviors, including segfaults (either immediately, or some time
later).  Indeed, I observe a number of `exp handle Subscript =3D> ...`s in
the `plan_cert` code, though I might expect that none of that code is
actually executed if `plan_cert` is invoked with no arguments and is just
printing out its usage information.

--000000000000c5e65106461dd101
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div dir=3D"ltr"><div class=3D"gmail_default" style=3D"fon=
t-family:arial,sans-serif;font-size:large"><span style=3D"font-family:Arial=
,Helvetica,sans-serif;font-size:small">On Tue, Dec 16, 2025 at 6:37=E2=80=
=AFPM David Wang &lt;<a href=3D"mailto:[email protected]">david.wang@kcl=
.ac.uk</a>&gt; wrote:</span></div></div><div class=3D"gmail_quote gmail_quo=
te_container"><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px=
 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class=
=3D"msg8512650742742454124"><div dir=3D"ltr"><div id=3D"m_85126507427424541=
24Signature">
<div style=3D"font-family:Aptos,Aptos_EmbeddedFont,Aptos_MSFontService,Cali=
bri,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
I have now updated the instructions in the `Readme.md` and created a <a tit=
le=3D"https://github.com/david-wang-0/temporal-planning-certification/tree/=
compilation" id=3D"m_8512650742742454124OWA7fa8b145-057b-19d5-3f2e-95240e49=
a11a" href=3D"https://github.com/david-wang-0/temporal-planning-certificati=
on/tree/compilation" target=3D"_blank">
branch</a>, where the problematic SML code produced by Isabelle is included=
.=C2=A0 Once the dependencies are obtained using `git submodule update --in=
it`, the commands `$ cd ML` and `$ make build_certifier_verbose` should wor=
k without involving Isabelle. `$ make
 build_certifier_verbose` emits the type checking error and `$ make build_c=
ertifier_unsafe` creates an executable that terminates with a segmentation =
fault.=C2=A0</div></div></div></div></blockquote><div><br></div><div><div c=
lass=3D"gmail_default" style=3D"font-family:arial,sans-serif;font-size:larg=
e">Thanks; I was able to reproduce both the type error and the segmentation=
 fault.</div><div class=3D"gmail_default" style=3D"font-family:arial,sans-s=
erif;font-size:large"><br></div><div class=3D"gmail_default" style=3D"font-=
family:arial,sans-serif;font-size:large">Compiling with `-type-check true` =
(and without `-const &#39;MLton.safe false&#39;`), I observe:</div><div cla=
ss=3D"gmail_default" style=3D"font-family:arial,sans-serif;font-size:large"=
><br></div><div class=3D"gmail_default" style=3D"font-family:arial,sans-ser=
if;font-size:large">=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0splitTypes2 starting<=
br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 splitTypes2:typeCheck starting=
<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0splitTypes2:type=
Check raised: Fail: TypeError (SSA): Ssa.TypeCheck.primApp (Array_copyArray=
(dBMEntry_0) ((dBMEntry_0) array, word64, (dBMEntry_1) array, word64, word6=
4)) in val _: unit =3D prim Array_copyArray[dBMEntry_0] (x_2, global_0, x_1=
, global_0, x_0) in L_0 in x_3<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0=
 splitTypes2:typeCheck raised in 0.12 + 0.00 (0% GC)<br>=C2=A0 =C2=A0 =C2=
=A0 =C2=A0 =C2=A0splitTypes2 raised in 0.29 + 0.00 (0% GC)</div><div class=
=3D"gmail_default" style=3D"font-family:arial,sans-serif;font-size:large"><=
br></div><div class=3D"gmail_default" style=3D"font-family:arial,sans-serif=
;font-size:large">This is essentially the same type error that was reported=
 at the end of `ssaSimplify`.=C2=A0 The internal type checking error is com=
plaining about a use of the `Array_copyArray` primitive.=C2=A0 In particula=
r, it seeing a use of the primitive where the arguments have types `((dBMEn=
try_0) array, word64, (dBMEntry_1) array, word64, word64)`.=C2=A0 This is a=
n error because this primitive is copying elements from one array to anothe=
r (implementing the SML Basis library `Array.copy` function and others), wh=
ere the intention is that it will be further implemented by a `memcpy`; tha=
t means that the source and destination arrays must have the same types, bu=
t the destination is a `dBMEntry_0 array` while the source is a `dBMEntry_1=
 array`.=C2=A0 The `splitTypes` optimization pass looks for opportunities t=
o &quot;split&quot; datatypes --- essentially duplicate datatype definition=
s so that distinct uses (i.e., ones that don&#39;t flow into one another) c=
an have distinct types and, therefore, be further optimized separately.=C2=
=A0 Of course, the array elements participating in `Array_copyArray` *do* f=
low into one another and so they should have their types split.</div><div c=
lass=3D"gmail_default" style=3D"font-family:arial,sans-serif;font-size:larg=
e"><br></div><div class=3D"gmail_default" style=3D"font-family:arial,sans-s=
erif;font-size:large">A quick look at the `splitTypes` implementation confi=
rms that it does not do anything &quot;special&quot; for `Array_copyArray` =
(or `Array_copyVector`), so the analysis was free to separate those types.=
=C2=A0 The fix is trivial (<a href=3D"https://github.com/MLton/mlton/pull/6=
32">https://github.com/MLton/mlton/pull/632</a>) and eliminates the interna=
l SSA type-checking error when compiling with `-type-check true` (and witho=
ut `-const &#39;MLton.safe false&#39;`).</div></div><div class=3D"gmail_def=
ault" style=3D"font-family:arial,sans-serif;font-size:large"><br></div><div=
 class=3D"gmail_default" style=3D"font-family:arial,sans-serif;font-size:la=
rge">Investigating the `-const &#39;MLton.safe false&#39;` will require mor=
e effort.=C2=A0 And, there is a reasonable chance that it isn&#39;t a compi=
ler error.=C2=A0 `-const &#39;MLton.safe false&#39;` isn&#39;t an advertise=
d feature and its behavior isn&#39;t checked by regression tests (or necess=
arily considered when developing the compiler).=C2=A0 For example, somewher=
e in the Basis Library=C2=A0 implementation, there may be an `exp handle Su=
bscript =3D&gt; ...` that relies upon a bounds check to be raised and handl=
ed; omitting the bounds check and unsafely reading or writing outside the b=
ounds of the array could have all kinds of misbehaviors, including segfault=
s (either immediately, or some time later).=C2=A0 Indeed, I observe a numbe=
r of `exp handle Subscript =3D&gt; ...`s in the `plan_cert` code, though I =
might expect that none of that code is actually executed if `plan_cert` is =
invoked with no arguments and is just printing out its usage information.</=
div><div class=3D"gmail_default" style=3D"font-family:arial,sans-serif;font=
-size:large"><br></div></div></div>

--000000000000c5e65106461dd101--


--===============7328467355626009249==
Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Disposition: inline


--===============7328467355626009249==
Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Disposition: inline

_______________________________________________
MLton-devel mailing list
[email protected]; [email protected]
https://lists.sourceforge.net/lists/listinfo/mlton-devel

--===============7328467355626009249==--