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

assertion failure exclusively with 4.06.1+rc1 #7713

Closed
vicuna opened this issue Jan 21, 2018 · 15 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link

commented Jan 21, 2018

Original bug ID: 7713
Reporter: aha
Assigned to: @maranget
Status: resolved (set by @xavierleroy on 2018-06-09T08:43:31Z)
Resolution: fixed
Priority: normal
Severity: minor
Fixed in version: 4.06.1
Category: typing
Monitored by: @nojb @gasche

Bug description

The following code snippet triggers an assert failure with the first release candidate of OCaml 4.06.1. All previous OCaml versions and 4.07.0+trunk accept it:

exception A of int
exception B of (int * int)

let f g =
try
g ()
with
| A(1|2) -> 1
| B(1,2) -> 2

Fatal error: exception File "typing/parmatch.ml", line 177, characters 12-18: Assertion failed

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 21, 2018

Comment author: @nojb

Introduced in 7f5f82d.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 21, 2018

Comment author: @gasche

The good news is that it works on trunk, which means that we have already fixed this and need to find the right commits to backport -- my guess (but I haven't investigated the issue yet) would be that merging #1550 should fix the issue.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 22, 2018

Comment author: @trefis

I think f5619dc might be enough (but backporting the whole PR probably makes more sense).

What surprises me though is that I didn't expect #1459 to change the behavior of parmatch...

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 22, 2018

Comment author: @trefis

And indeed:

    OCaml version 4.06.1+rc1

exception A of int

exception B of int * int;;
exception A of int
exception B of int * int

let f g = try g () with A (1 | 2) -> 1 | B (1, 2) -> 2;;

val f : (unit -> int) -> int =

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 22, 2018

Comment author: @trefis

Interesting, it doesn't fail with the toplevel, but fails with ocamlc.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 22, 2018

Comment author: @trefis

The full backtrace is:

Fatal error: exception File "typing/parmatch.ml", line 177, characters 12-18: Assertion failed
Raised at file "typing/parmatch.ml", line 177, characters 12-24
Called from file "typing/parmatch.ml", line 158, characters 7-18
Called from file "bytecomp/matching.ml", line 659, characters 26-40
Called from file "bytecomp/matching.ml", line 657, characters 8-150
Called from file "bytecomp/matching.ml", line 1102, characters 24-46
Called from file "bytecomp/matching.ml", line 1125, characters 29-41
Called from file "bytecomp/matching.ml", line 1134, characters 25-66
Called from file "bytecomp/matching.ml", line 2695, characters 6-81
Called from file "bytecomp/matching.ml", line 2516, characters 36-64
Called from file "bytecomp/matching.ml", line 2558, characters 14-47
Called from file "bytecomp/matching.ml", line 2648, characters 28-64
Called from file "bytecomp/matching.ml", line 2698, characters 6-145
Called from file "bytecomp/matching.ml", line 2884, characters 30-73
Called from file "bytecomp/translcore.ml", line 824, characters 15-78
Called from file "bytecomp/translcore.ml", line 1074, characters 30-46
Called from file "bytecomp/translcore.ml", line 1081, characters 9-35
Called from file "list.ml", line 82, characters 20-23
Called from file "bytecomp/translcore.ml", line 1204, characters 9-29
Called from file "bytecomp/translcore.ml", line 703, characters 8-213
Called from file "bytecomp/translobj.ml", line 182, characters 17-20
Re-raised at file "bytecomp/translobj.ml", line 199, characters 4-13
Called from file "bytecomp/translcore.ml", line 1213, characters 20-35
Called from file "bytecomp/translmod.ml", line 519, characters 10-48
Called from file "bytecomp/translmod.ml", line 536, characters 12-73
Called from file "bytecomp/translmod.ml", line 536, characters 12-73
Called from file "bytecomp/translobj.ml", line 98, characters 19-23
Called from file "bytecomp/translmod.ml", line 671, characters 4-130
Called from file "bytecomp/translmod.ml", line 682, characters 4-55
Called from file "utils/misc.ml", line 28, characters 20-27
Re-raised at file "utils/misc.ml", line 28, characters 50-57
Called from file "driver/compile.ml" (inlined), line 67, characters 15-18
Called from file "driver/compile.ml", line 90, characters 10-127
Re-raised at file "driver/compile.ml", line 118, characters 6-13
Called from file "utils/misc.ml", line 28, characters 20-27
Re-raised at file "utils/misc.ml", line 28, characters 50-57
Called from file "driver/compenv.ml", line 563, characters 6-35
Called from file "list.ml", line 100, characters 12-15
Called from file "driver/compenv.ml", line 639, characters 2-61
Called from file "driver/main.ml", line 139, characters 6-147
Re-raised at file "parsing/location.ml", line 465, characters 14-25
Re-raised at file "parsing/location.ml", line 465, characters 14-25
Re-raised at file "parsing/location.ml", line 465, characters 14-25
Re-raised at file "parsing/location.ml", line 465, characters 14-25
Re-raised at file "parsing/location.ml", line 465, characters 14-25
Re-raised at file "parsing/location.ml", line 465, characters 14-25
Called from file "parsing/location.ml" (inlined), line 470, characters 31-61
Called from file "driver/main.ml", line 200, characters 4-35
Called from file "driver/main.ml", line 204, characters 2-9

Which makes more sense (that is: in a way, the issue comes from matching, not parmatch)

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 22, 2018

Comment author: @trefis

And to confirm: cherry-picking f5619dc is enough to make the issue disappear.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 22, 2018

Comment author: @nojb

Is it possible to explain why the comment "(* By typing *)" in parmatch.ml is wrong?

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 22, 2018

Comment author: @trefis

nojebar: given the way we build "pattern matrices" we can't always assume that patterns in the same column of a matrix will be of the same type. Indeed we can easily produce counter examples using GADTs, as show cased here : https://github.com/ocaml/ocaml/blob/trunk/typing/parmatch.ml#L47 (introduced by #1550).
As for pattern matching compilation (which is what causes problem here), we build our matrices in a slightly different way (because we have to assume that extensible constructors might be aliases of each other) and end up introducing incoherence in our matrices, see for example #1493 . That is also what happens in this MPR.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 22, 2018

Comment author: @trefis

(N.B. the discrepancy I thought I observed between ocaml and ocamlc was obviously due to the fact that I forgot some parentheses when playing in the toplevel! Sorry for the noise.)

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 22, 2018

Comment author: @maranget

So do we cherry-pick or merge-in the whole PR 1550 ?

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 22, 2018

Comment author: @gasche

Is it possible to explain why the comment "(* By typing *)" in parmatch.ml is wrong?

I think you should have received the email titled "A note on pattern matching and 4.06.1", that I sent to caml-devel on December 19th, and explains the issue -- it also predicts that bugs such as this one may arise in the 4.06 branch.

Luc, Thomas: re. merging vs. cherry-picking, I'm not sure which one we want, and also which one Damien will be comfortable merging in the release branch.

I would like to understand whether we are confident that cherry-picking f5619dc would be sufficient to "silence" miscompilations without wrong-code generation or degradation to currently-correct warnings. Thomas, if you investigated the issue (I haven't yet), have you analyzed the usages of Parmatch in Matching, and are you confindent that this commit is "enough" for this class of issues?

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 22, 2018

Comment author: @trefis

Yes,f5619dc is the only commit of #1550 that affects Matching so it should be enough to cherry-pick it to fix that issue.

Another question is: if we cherry-pick only that commit, in what kind of state do we leave Parmatch? Do we expose ourselves to other new bugs?
I think it's most likely fine, but I haven't thought hard about it.

Separately, I can confirm that a few weeks I managed to build janestreet's codebase with the whole GPR backported on 4.06.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jan 23, 2018

Comment author: @maranget

I am in favor of backporting the whole pull request #1550. This very PR shows that not doing so was a mistake.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jun 9, 2018

Comment author: @xavierleroy

Fixed in 4.06.1 by backport, commit b2ac599

@vicuna vicuna closed this Jun 9, 2018

@vicuna vicuna added the typing label Mar 14, 2019

@vicuna vicuna added the bug label Mar 20, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.