Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007713OCamltypingpublic2018-01-21 20:272018-06-09 10:43
Reporteraha 
Assigned Tomaranget 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.06.1 
Summary0007713: assertion failure exclusively with 4.06.1+rc1
DescriptionThe 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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0018838)
nojebar (developer)
2018-01-21 21:24

Introduced in https://github.com/ocaml/ocaml/commit/7f5f82dc9cbc99f5b3ef1dc6cfd43fffb143f4ce. [^]
(0018839)
gasche (developer)
2018-01-21 21:53

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 https://github.com/ocaml/ocaml/pull/1550/ [^] should fix the issue.
(0018842)
trefis (manager)
2018-01-22 10:52

I think https://github.com/ocaml/ocaml/pull/1550/commits/f5619dc10ac0436e29a9525031fa04b2759aa2a7 [^] might be enough (but backporting the whole PR probably makes more sense).

What surprises me though is that I didn't expect GPR#1459 to change the behavior of parmatch...
(0018843)
trefis (manager)
2018-01-22 10:56

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 = <fun>
(0018844)
trefis (manager)
2018-01-22 11:08

Interesting, it doesn't fail with the toplevel, but fails with ocamlc.
(0018845)
trefis (manager)
2018-01-22 11:11

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)
(0018846)
trefis (manager)
2018-01-22 11:13

And to confirm: cherry-picking https://github.com/ocaml/ocaml/pull/1550/commits/f5619dc10ac0436e29a9525031fa04b2759aa2a7 [^] is enough to make the issue disappear.
(0018847)
nojebar (developer)
2018-01-22 11:17

Is it possible to explain why the comment "(* By typing *)" in parmatch.ml is wrong?
(0018848)
trefis (manager)
2018-01-22 11:38

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 GPR#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 https://github.com/ocaml/ocaml/pull/1493 [^] . That is also what happens in this MPR.
(0018849)
trefis (manager)
2018-01-22 11:53

(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.)
(0018850)
maranget (manager)
2018-01-22 14:28

So do we cherry-pick or merge-in the whole PR 1550 ?
(0018851)
gasche (developer)
2018-01-22 14:59

> 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 https://github.com/ocaml/ocaml/pull/1550/commits/f5619dc10ac0436e29a9525031fa04b2759aa2a7 [^] 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?
(0018852)
trefis (manager)
2018-01-22 15:28

Yes,f5619dc is the only commit of GPR#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.
(0018855)
maranget (manager)
2018-01-23 15:23
edited on: 2018-01-24 15:39

I am in favor of backporting the whole pull request https://github.com/ocaml/ocaml/pull/1550/. [^] This very PR shows that not doing so was a mistake.

(0019169)
xleroy (administrator)
2018-06-09 10:43

Fixed in 4.06.1 by backport, commit b2ac599

- Issue History
Date Modified Username Field Change
2018-01-21 20:27 aha New Issue
2018-01-21 21:24 nojebar Note Added: 0018838
2018-01-21 21:25 nojebar Assigned To => maranget
2018-01-21 21:25 nojebar Status new => assigned
2018-01-21 21:53 gasche Note Added: 0018839
2018-01-22 10:52 trefis Note Added: 0018842
2018-01-22 10:56 trefis Note Added: 0018843
2018-01-22 11:08 trefis Note Added: 0018844
2018-01-22 11:11 trefis Note Added: 0018845
2018-01-22 11:13 trefis Note Added: 0018846
2018-01-22 11:17 nojebar Note Added: 0018847
2018-01-22 11:38 trefis Note Added: 0018848
2018-01-22 11:53 trefis Note Added: 0018849
2018-01-22 14:28 maranget Note Added: 0018850
2018-01-22 14:59 gasche Note Added: 0018851
2018-01-22 15:28 trefis Note Added: 0018852
2018-01-23 15:23 maranget Note Added: 0018855
2018-01-24 15:39 maranget Note Edited: 0018855 View Revisions
2018-06-09 10:43 xleroy Note Added: 0019169
2018-06-09 10:43 xleroy Status assigned => resolved
2018-06-09 10:43 xleroy Resolution open => fixed
2018-06-09 10:43 xleroy Fixed in Version => 4.06.1


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker