Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Type parameter handling bug? #362

Closed
nwf-msr opened this issue Oct 31, 2023 · 10 comments
Closed

Type parameter handling bug? #362

nwf-msr opened this issue Oct 31, 2023 · 10 comments

Comments

@nwf-msr
Copy link
Contributor

nwf-msr commented Oct 31, 2023

Compiling

$include <result.sail>

union U ('a: Type) = { U1 : 'a }

type V = U(unit)

val main : unit -> unit
function main () = let r : result(V, unit) = Err(()) in ()

with f9db302 (and so probably the just-cut 0.17 release, I'm sorry) causes sail to die an inglorious death, croaking out Fatal error: exception Not_found and leaving behind an empty output file.

Confusingly, this is a minimized version of a much larger sail program that has been accepted without complaint in the past, so I am not sure what the actual preconditions for tripping over this are. This particular input seems fatal to the 0.15 and 0.16 installations I have handy, though.

Replacing the type V definition with type V = unit seems to result in successful compilation, so it seems like it's something to do with the fact that U is parametric?

@Alasdair
Copy link
Collaborator

I think the root cause is because U is never constructed it gets lost when the types are being monomorphised.

Adding any line that constructs U(unit) should work around this, i.e. a let x : V = U1(()). That might be why you didn't notice it in a larger program maybe?

@nwf-msr
Copy link
Contributor Author

nwf-msr commented Oct 31, 2023

I am pretty sure the larger program instantiates all its types, though, but I will attempt to check.

@Alasdair
Copy link
Collaborator

Should be fixed by #363

@nwf-msr
Copy link
Contributor Author

nwf-msr commented Oct 31, 2023

That fixes something, but my full program is still throwing the same unpleasant result. Lemme minimize it again.

@Alasdair
Copy link
Collaborator

Could try using OCAMLRUNPARAM=b to get a backtrace

@nwf-msr
Copy link
Contributor Author

nwf-msr commented Oct 31, 2023

TIL. If it helps:

Raised at Stdlib__List.find in file "list.ml", line 224, characters 10-25
Called from Libsail__Jib_compile.Make.sort_ctype_defs.(fun) in file "src/lib/jib_compile.ml", line 2065, characters 36-108
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Libsail__Jib_compile.Make.sort_ctype_defs in file "src/lib/jib_compile.ml", line 2065, characters 6-113
Called from Libsail__Jib_compile.Make.compile_ast in file "src/lib/jib_compile.ml", line 2128, characters 16-43
Called from C_backend.compile_ast in file "src/sail_c_backend/c_backend.ml", line 1990, characters 21-51
Called from Sail_plugin_c.c_target in file "src/sail_c_backend/sail_plugin_c.ml", line 163, characters 2-71
Called from Sail.run_sail in file "src/bin/sail.ml", line 298, characters 2-73
Called from Sail.main in file "src/bin/sail.ml", line 438, characters 46-68
Called from Sail in file "src/bin/sail.ml", line 465, characters 10-17

@Alasdair
Copy link
Collaborator

I'm not sure how that find would fail, so a minimized example would be useful.

@nwf-msr
Copy link
Contributor Author

nwf-msr commented Oct 31, 2023

Sorry, meetings. Not quite minimized, but pretty small:

$include <result.sail>

union P ('a: Type) = { P1 : 'a }
union U = { U1 : P(unit) }
type T = result({'n, 'n > 0. (U, int('n))}, unit)

val main : unit -> unit
function main () = let _ : T = Err(()) in ()

Replacing union U = { ... } with type U = P(unit) causes compilation to succeed, as does replacing type T's RHS with result(U, unit).

@Alasdair
Copy link
Collaborator

Alasdair commented Nov 1, 2023

Thanks, I think this should be fixed by #364

I think this was triggered by some recent optimisations to avoid copying definitions during monomorphisation, so I've put my opam release on hold for now.

@nwf-msr
Copy link
Contributor Author

nwf-msr commented Nov 3, 2023

That looks to have done it; thanks!

@nwf-msr nwf-msr closed this as completed Nov 3, 2023
Alasdair added a commit to Alasdair/opam-repository that referenced this issue Nov 13, 2023
CHANGES:

Updated 0.17 release with bugfixes for:

* Issue 362 rems-project/sail#362

Additionally includes patches for better ASL to Sail compatibility
nberth pushed a commit to nberth/opam-repository that referenced this issue Jun 18, 2024
CHANGES:

Updated 0.17 release with bugfixes for:

* Issue 362 rems-project/sail#362

Additionally includes patches for better ASL to Sail compatibility
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants