Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006505OCamltypingpublic2014-07-31 15:152017-09-24 17:33
Assigned Togarrigue 
PlatformOSOS Version
Product Version4.01.0 
Target VersionFixed in Version4.04.0 +dev / +beta1 / +beta2 
Summary0006505: Missed Type-error leads to a segfault upon record access
DescriptionThis is a rather large and complex codebase, so forgive me that this bug report is not (yet) in a usable form. I hope for the active help from OCaml devs here to nail down the exact source and a minimal triggering example.

Anyway. In the code found here: [^]

I encountered something that seems to be a type-error that went unnoticed by OCaml 4.01
In I put a record (sim_state) in my extensible state monad (e.g. here: [^] ), and in my test-case, I get an option value (e.g. here: [^] ). Obviously, I made a simple mistake in, but the typechecker won't take notice of it.

In the consequence, this test program crashes with a segmentation fault.
Steps To ReproduceThe branch is already somewhat stripped down. To compile it, you will need the dependencies (all installable via opam):

opam install pa_monad_custom, batteries, pa_comprehension, ounit

Then you can checkout the demonstration code:

git clone [^]

git checkout typecheck_bug

To build:

oasis setup && ./configure && make

And run the test:


Additional InformationAs mentioned, I am aware that the code is quite large. Any help/hints to strip it down further is appreciated. Unfortunately, I don't have the time to dig it out all alone, but I felt such a bug is too important to be left unnoticed.

TagsNo tags attached.
Attached Files? file icon [^] (538 bytes) 2014-07-31 20:00 [Show Content]

- Relationships
related to 0005343closedgarrigue ocaml -rectypes is unsound wrt module subtyping 
parent of 0006496closedgarrigue Assertion triggered by recursive class type 

-  Notes
doligez (administrator)
2014-07-31 17:47

I followed your steps to reproduce, but "make" doesn't seem to build "simTest.native" or any other executable.
yallop (developer)
2014-07-31 20:00

Here's a simpler example:

   $ cat
   module M :
     type 'o is_an_object = < .. > as 'o
     and 'o abs constraint 'o = 'o is_an_object
     val abs : 'o is_an_object -> 'o abs
     val unabs : 'o abs -> 'o
   end =
     type 'o is_an_object = < .. > as 'o
     and 'o abs = 'o constraint 'o = 'o is_an_object
     let abs v = v
     let unabs v = v

   class c =
     val _y = (None : 'o M.abs option )
     method get_y = _y
     method set_y y = {<_y = y>}

   let c' = (new c)#set_y (Some (M.abs (object end)))
   let _ = match c'#get_y with
       Some y -> (M.unabs y)#bang
     | None -> ()

   $ ocaml
   Segmentation fault
choeger (reporter)
2014-07-31 20:21

@dolligez: Sorry, you have to run
./configure --enable-tests
garrigue (manager)
2014-08-01 06:25

In yallop's example, yhe problem here is apparent in the signature inferred for M:

module M :
    type 'o is_an_object = 'o constraint 'o = < .. >
    and 'a abs constraint 'a = 'a is_an_object
    val abs : ('a is_an_object as 'a) is_an_object -> 'a abs
    val unabs : ('a is_an_object as 'a) abs -> 'a

The type ('a is_an_object as 'a) does not make sense.
It ends up hiding the fact it contains a free type variable, which allows in turn the class to leak it.
garrigue (manager)
2014-08-02 05:27

Fixed in branch 4.02, at revision 15038.

Thank you Jeremy for providing a compact reproduction case.
Since opam's batteries don't compile with 4.02, I have only tried with, which now gives:

Error: The definition of abs contains a cycle:
       'a is_an_object as 'a

Actually, I'm rather surprised you could trigger this bug just by sheer chance, because it is a conjunction of a lot of things.
Basically, what happened is that, in order to allow polymorphic uses of abbreviations in mutually recursive type definitions, checking proper use of abbreviations is delayed until a second phase, one the types are defined. However, it only checked that each abbreviation is contractive (i.e. doesn't expand to itself).
In your case, what happens is that, a combination of constraints during type definition ends up creating a non-contractive recursive type inside the definition of abs. This was not checked, at it was assumed that checking for each abbreviation to be contractive would be sufficient.
Why is it bad? The first reason is it can make the typechecker loop. However, this didn't occur here.
What happened is that this non-contractive recursive type ended up hiding a type variable, very much as in PR#5343.
This hidden type variable could then be used to change the type of anything, as in another already known problem with constraints / GADTs.
The fix is to check for cycles in all type definitions. This is made efficient by assuming that only freshly defined types may initiate such a cycle.
choeger (reporter)
2014-08-03 22:07

Does that mean, you cannot define a constraint now, where you use the a type variable on the rhs of object methods? I am relying on the ability to express class type constraints, where methods deliver a new object of the class that fulfills the constraint.

i.e. an iterator would have the type:

type 'a iterator = <next : 'a option ; ..> as 'a
garrigue (manager)
2014-08-04 02:27

No, the algorithm just checked that you are not creating "black holes", I.e. cycles that do not contain any type constructor. A cycle going through an object type is fine.
garrigue (manager)
2016-06-13 06:37

Looking at the output of the test case, the behavior with or without -principal is different, so I reopen this report. (Not dangerous, but disturbing)
stedolan (developer)
2016-06-19 14:48

The problem still seems to be there. The recursion in 'abs' is inessential, and here's a slight variant without it:

$ ocaml -version
The OCaml toplevel, version 4.03.0
$ cat
module M :
  type 'o is_an_object = < .. > as 'o
  and ('k,'o) abs constraint 'k = 'o is_an_object
  val abs : 'o is_an_object -> ('o,'o) abs
  val unabs : ('o, 'o) abs -> 'o
end =
  type 'o is_an_object = < .. > as 'o
  and ('k,'o) abs = 'o constraint 'k = 'o is_an_object
  let abs v = v
  let unabs v = v

class c =
  val _y = (None : ('o,'o) M.abs option )
  method get_y = _y
  method set_y y = {<_y = y>}

let c' = (new c)#set_y (Some (M.abs (object end)))
let _ = match c'#get_y with
    Some y -> (M.unabs y)#bang
  | None -> ()
$ ocaml
Segmentation fault
stedolan (developer)
2016-06-19 15:12

Hmm, this seems to be a regression. My version does not segfault in 4.02.1, while in 4.03 even this shorter program crashes:

  type 'o is_an_object = < .. > as 'o
  and ('k,'l) abs = 'l constraint 'k = 'l is_an_object
  let y : ('o, 'o) abs = object end
  let _ = y#bang

Very oddly, in 4.02.1 this program does not crash when run with "ocaml", but does crash when copy-pasted into the toplevel.
lpw25 (developer)
2016-06-21 17:34
edited on: 2016-06-21 17:35

Same issue for polymorphic variants:

  type 'v is_a_variant = [> ] as 'v
  and ('k,'l) abs = 'l constraint 'k = 'l is_a_variant
  let x : ('a, 'a) abs = `Foo 6
  let () = print_endline (match x with `Bar s -> s)

garrigue (manager)
2016-06-22 03:52

New reports fixed in trunk by commit 3c14f2e.
The issue was orthogonal: unfy_var was missing one check.

Still working on the problem with -principal.
garrigue (manager)
2016-07-05 11:10

Fixed in trunk by commit 848c20f.

In order to properly fix this in the -principal case to, had to make the handling of recursive types more restrictive in mutually recursive definitions.
They are now seen as non-contractive, meaning that the following definition is rejected:
  type 'a u = < x : 'a>
  and 'a t = 'a t u;;
while the non-recursive version is fine:
  type 'a u = < x : 'a>
  type 'a t = 'a t u;;

Error messages are not so good, but I see no easy way to avoid it.

- Issue History
Date Modified Username Field Change
2014-07-31 15:15 choeger New Issue
2014-07-31 17:47 doligez Note Added: 0011959
2014-07-31 17:47 doligez Assigned To => doligez
2014-07-31 17:47 doligez Status new => feedback
2014-07-31 20:00 yallop Note Added: 0011961
2014-07-31 20:00 yallop File Added:
2014-07-31 20:21 choeger Note Added: 0011962
2014-07-31 20:21 choeger Status feedback => assigned
2014-08-01 06:15 garrigue Relationship added related to 0005343
2014-08-01 06:16 garrigue Assigned To doligez => garrigue
2014-08-01 06:25 garrigue Note Added: 0011964
2014-08-02 05:27 garrigue Note Added: 0011967
2014-08-02 05:27 garrigue Status assigned => resolved
2014-08-02 05:27 garrigue Fixed in Version => 4.02.0+dev
2014-08-02 05:27 garrigue Resolution open => fixed
2014-08-03 22:07 choeger Note Added: 0011969
2014-08-04 02:27 garrigue Note Added: 0011970
2014-08-21 08:17 garrigue Relationship added parent of 0006496
2016-06-13 06:37 garrigue Note Added: 0015979
2016-06-13 06:37 garrigue Status resolved => confirmed
2016-06-13 06:37 garrigue Priority high => low
2016-06-19 14:48 stedolan Note Added: 0015985
2016-06-19 15:12 stedolan Note Added: 0015986
2016-06-21 17:34 lpw25 Note Added: 0015992
2016-06-21 17:35 lpw25 Note Edited: 0015992 View Revisions
2016-06-22 03:52 garrigue Note Added: 0015993
2016-07-05 11:10 garrigue Note Added: 0016035
2016-07-05 11:10 garrigue Status confirmed => resolved
2016-07-05 11:10 garrigue Fixed in Version 4.02.0+dev => 4.04.0 +dev / +beta1 / +beta2
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-09-24 17:33 xleroy Status resolved => closed

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker