Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007432OCamltypingpublic2016-12-15 15:382016-12-17 02:38
Assigned Togarrigue 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.05.0 +dev/beta1/beta2/beta3/rc1 
Summary0007432: Linking modules compiled with -labels and -nolabels is not safe
DescriptionThe -labels and -nolabels modes of the compiler have different views of type equality. There are some types that are considered equal with -nolabels, but incompatible with -labels.

It's possible, therefore, to pass a witness of type equality (compiled with -nolabels) to a function compiled (with -labels) under the assumption that no such witness can exist, leading to a crash.

Here's a demonstration:

    $ cat
    type (_,_) eql = Refl : ('a, 'a) eql
    type s = x:int -> y:float -> unit
    type t = y:int -> x:float -> unit
    let eql : (s, t) eql = Refl
    $ cat
    open A

    type silly = {silly: 'a.'a}

    let f : [`L of (s, t) eql | `R of silly] -> 'a =
       function `R {silly} -> silly
    let () = print_endline (f (`L A.eql))
    $ ocamlopt -c -nolabels && ocamlopt -c && ocamlopt a.cmx b.cmx -o a.out
    $ ./a.out
    Segmentation fault
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
garrigue (manager)
2016-12-17 02:38

Fixed by commit 6e694c6.

mcomp was already doing the right thing (ignoring labels for non-optional arguments), but unify has to do the same thing when in Pattern mode.

- Issue History
Date Modified Username Field Change
2016-12-15 15:38 yallop New Issue
2016-12-17 02:38 garrigue Note Added: 0017021
2016-12-17 02:38 garrigue Status new => resolved
2016-12-17 02:38 garrigue Fixed in Version => 4.05.0 +dev/beta1/beta2/beta3/rc1
2016-12-17 02:38 garrigue Resolution open => fixed
2016-12-17 02:38 garrigue Assigned To => garrigue
2017-02-23 16:45 doligez Category OCaml typing => typing

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker