Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006505OCamlOCaml typingpublic2014-07-31 15:152014-08-21 08:17
Reporterchoeger 
Assigned Togarrigue 
PriorityhighSeveritycrashReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.01.0 
Target VersionFixed in Version4.02.0+dev 
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:

https://github.com/AMSUN-Berlin/ocsimrun/tree/typecheck_bug [^]

I encountered something that seems to be a type-error that went unnoticed by OCaml 4.01
In sim.ml I put a record (sim_state) in my extensible state monad (e.g. here: https://github.com/AMSUN-Berlin/ocsimrun/blob/typecheck_bug/simulation/sim.ml#L193 [^] ), and in my test-case, I get an option value (e.g. here: https://github.com/AMSUN-Berlin/ocsimrun/blob/typecheck_bug/tests/simTests.ml#L50 [^] ). Obviously, I made a simple mistake in sim.ml, 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 https://github.com/AMSUN-Berlin/ocsimrun.git [^]

git checkout typecheck_bug

To build:

oasis setup && ./configure && make

And run the test:

./simTests.native

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 bang.ml [^] (538 bytes) 2014-07-31 20:00 [Show Content]

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

-  Notes
(0011959)
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.
(0011961)
yallop (developer)
2014-07-31 20:00

Here's a simpler example:

   $ cat bang.ml
   module M :
   sig
     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 =
   struct
     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
   end

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

   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 bang.ml
   Segmentation fault
(0011962)
choeger (reporter)
2014-07-31 20:21

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

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

module M :
  sig
    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
  end

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.
(0011967)
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 bang.ml, 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.
(0011969)
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
(0011970)
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.

- 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: bang.ml
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


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker