Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006787OCamltypingpublic2015-02-19 00:162016-12-07 11:49
Reportermkoconnor 
Assigned Togarrigue 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version4.02.1 
Target VersionFixed in Version4.02.2+dev / +rc1 
Summary0006787: soundness bug with polymorphic variants
DescriptionThe code below (also attached) gives a function which interprets an int as a string and produces a segfault when run. I think this code is roughly minimal (e.g., I think the [revapply] function is necessary).

let revapply x f = f x

module Contravariant : sig
  type -'a t
  val create : unit -> [< `Foo] t
end = struct
  type 'a t = unit
  let create () = ()
end

module M : sig
  val int_to_string : [ `Bar of int ] -> string
end = struct
  let int_to_string x =
    let x =
      revapply x (fun (`Bar int) -> (`Bar int), Contravariant.create ())
    in
    revapply x (fun ((`Bar int), _) -> (int : string))
end

let () = Printf.printf "%s" (M.int_to_string (`Bar 0))
Steps To ReproduceCompile trial.ml with ocamlc or ocamlopt.opt and run.
TagsNo tags attached.
Attached Files? file icon trial.ml [^] (463 bytes) 2015-02-19 00:16 [Show Content]

- Relationships

-  Notes
(0013311)
lpw25 (developer)
2015-02-19 01:12

I've got it down to the following case:

            OCaml version 4.02.1

    # let revapply x f = f x

      let f x (g : [< `Foo]) =
        let y = `Bar x, g in
          revapply y (fun ((`Bar i), _) -> i)

      let segfault = (f 0 `Foo : string);;

    Process ocaml-toplevel segmentation fault
(0013312)
garrigue (manager)
2015-02-19 08:06

Interestingly, the bug does not occur with -principal.
And it seems to have been introduced in 4.01 (4.00 is ok).
(0013313)
hnrgrgr (developer)
2015-02-19 10:59

By using `git bisect`, the bug was introduced with commit 13221 :

  https://github.com/ocaml/ocaml/commit/c4d1bf8b774bf171f5aec0cf862c600f7328abeb [^]
(0013314)
garrigue (manager)
2015-02-19 11:05

Fixed in trunk and 4.02 at revisions 15851 and 15852.

Some code added to allow the propagation of type information to patterns was breaking the invariant that two different polymorphic variant types should not share the same row variable.
(0013948)
lpw25 (developer)
2015-05-18 22:05
edited on: 2015-05-18 22:05

In case anyone comes across this elsewhere, one of the ways this bug can manifest itself is as code which takes the wrong branch on a match with polymorphic variants in it. For example:

  module Monad : sig
    type 'a t
    val return : 'a -> 'a t
    val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t
    val run : 'a t -> 'a
  end = struct
    type 'a t = 'a
    let return x = x
    let ( >>= ) m k = k m
    let run m = m
  end

  open Monad

  let foo x =
      match x with
      | `Error -> return `Error
      | `Ok y ->
        match y with
        | `Left | `Right -> return (`Ok y)

  let bar x =
    foo x
    >>= function
    | `Error -> return 1
    | `Ok `Left -> return 2
    | `Ok `Right -> return 3

  let () =
    Printf.printf "%d\n" (run (bar (`Ok `Right)))

will print 2 instead of 3 as the wrong branch is taken in `bar`.


- Issue History
Date Modified Username Field Change
2015-02-19 00:16 mkoconnor New Issue
2015-02-19 00:16 mkoconnor File Added: trial.ml
2015-02-19 01:12 lpw25 Note Added: 0013311
2015-02-19 08:06 garrigue Note Added: 0013312
2015-02-19 10:59 hnrgrgr Note Added: 0013313
2015-02-19 11:05 garrigue Note Added: 0013314
2015-02-19 11:05 garrigue Status new => resolved
2015-02-19 11:05 garrigue Fixed in Version => 4.02.2+dev / +rc1
2015-02-19 11:05 garrigue Resolution open => fixed
2015-02-19 11:05 garrigue Assigned To => garrigue
2015-05-18 22:05 lpw25 Note Added: 0013948
2015-05-18 22:05 lpw25 Note Edited: 0013948 View Revisions
2015-05-19 12:29 shinwell Severity minor => major
2016-12-07 11:49 xleroy Status resolved => closed
2017-02-23 16:45 doligez Category OCaml typing => typing


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker