Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007241OCamltypingpublic2016-04-25 19:132018-06-06 16:39
Reporterstedolan 
Assigned Tomaranget 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0007241: Pattern matching with mutable and lazy patterns is unsound
DescriptionOptimised pattern matching skips checking conditions that seem redundant. However, since OCaml supports pattern-matching mutable fields, and code execution during matching via "lazy" patterns, the truth of some conditions can vary during matching.

This can cause seemingly-impossible cases to be taken, if forcing lazy values causes mutations that confuse the optimised matching logic. Due to the presence of GADTs, taking an impossible case is a soundness issue.

For example, this program segfaults:

    type (_, _) eq = Refl : ('a, 'a) eq
    type (_, _) deq = Deq : ('a, 'x) eq option * ('x, 'b) eq option -> ('a, 'b) deq
    
    let deq1 = Deq (Some Refl, None)
    let deq2 = Deq (None, Some Refl)
    
    type ('a, 'b) t = {
      a : bool;
      mutable b : ('a, 'b) deq;
      mutable c : int Lazy.t
    }
    
    let g (type a) (type b) : (a, b) t -> (a, b) eq = function
    | { a = true; b = Deq (None, _) }
    | { a = true; b = Deq (Some _, _); c = lazy 1 }
    | { a = false }
    | { b = Deq (_, None) } ->
       assert false
    | { b = Deq (Some Refl, Some Refl) } ->
       Refl
    
    let bad =
      let r = { a = true; b = deq1; c = lazy 1 } in
      r.c <- lazy (r.b <- deq2; 2);
      g r
    
    let castint (type a) (Refl : (int, a) eq) (x : int) : a = x
    let _ = print_string (castint bad 42)

This program uses mutation to change a field from "deq1" to "deq2" during matching, making it seem like the impossible "Deq (Some Refl, Some Refl)". (The behaviour is very dependent on the exact sequence of cases in "g", and seemingly-equivalent programs will often give different behaviour).
TagsNo tags attached.
Attached Files

- Relationships
related to 0005992closedmaranget Crash when pattern-matching lazy values modifies the scrutinee 

-  Notes
(0015846)
stedolan (developer)
2016-04-25 19:25
edited on: 2016-04-25 19:35

Playing with it a bit more, the example can be simplified to the following, which does not use laziness:

    type app = App : ('x -> unit) option * 'x -> app
    
    let app1 = App (Some print_string, "hello")
    let app2 = App (None, 42)
    
    type t = {
      a : bool;
      mutable b : app
    }
    
    let f = function
    | { a = false } -> assert false
    | { a = true; b = App (None, _) } -> assert false
    | { a = true; b = App (Some _, _) } as r
        when (r.b <- app2; false) -> assert false
    | { b = App (Some f, x) } ->
       f x

    let _ = f { a = true; b = app1 }

The issue is not the type-equality behaviour of GADTs, but the existential quantification. In this example, mutation causes the optimised pattern-matching to confuse the values bound under two different existential quantifiers. Either lazy patterns (as in the original example) or when guards (above) are enough to cause mutation during matching.

(0015859)
bvaugon (developer)
2016-04-26 11:48

Remarks, the "when" is also broken. For example, the following code crash in the similar way:

type (_, _) eq = Refl : ('a, 'a) eq
type (_, _) deq = Deq : ('a, 'x) eq option * ('x, 'b) eq option -> ('a, 'b) deq
    
let deq1 = Deq (Some Refl, None)
let deq2 = Deq (None, Some Refl)
    
type ('a, 'b) t = {
  a : bool;
  mutable b : ('a, 'b) deq;
}
    
let r = { a = true; b = deq1 }

let g (type a) (type b) : (a, b) t -> (a, b) eq = function
  | { a = true; b = Deq (Some _, _) } when (r.b <- deq2; false) ->
    assert false
  | { a = true; b = Deq (None, _) }
  | { a = false }
  | { b = Deq (_, None) } ->
    assert false
  | { b = Deq (Some Refl, Some Refl) } ->
    Refl

let bad = g r
    
let castint (type a) (Refl : (int, a) eq) (x : int) : a = x
let _ = print_string (castint bad 42)
(0016063)
frisch (developer)
2016-07-13 09:53

I did not try to produce an example, and this would be more tricky, but even without lazy or when guards, it is impossible to guarantee that arbitrary code won't be executed during pattern matching as soon as patterns need to allocate (e.g. to read from a float from unboxed records or arrays). These allocations can trigger the GC and thus finalizer which could modify mutable parts of the matched value. It might be possible to delay these allocations (at least until the "when" guard), but this would probably require some refactoring of the PM compiler. (Of course, the pattern can "traverse" the unboxed floats.)
(0016067)
frisch (developer)
2016-07-13 13:19

Setting Target version to "later", since there is no clear resolution plan.
(0016081)
garrigue (manager)
2016-07-19 07:40

I don't even think that one needs existentials to do that.
Here is an example in core ocaml; it segfaults even after fixing Matching.check_partial (which currently only downgrade if the same pattern contains both mutable and lazy)

type u = {a: bool; mutable b: int option}

let f x =
  match x with
    {a=false} -> 0
  | {b=None} -> 1
  | _ when (x.b <- None; false) -> 2
  | {a=true; b=Some y} -> y

let _ = f {a=true; b=Some 5}

The (insufficient) fix in matching.ml is

let check_partial is_mutable is_lazy pat_act_list = function
  | Partial -> Partial
  | Total ->
      if
        pat_act_list = [] || (* allow empty case list *)
        List.exists (fun (pats, _) -> is_mutable pats) pat_act_list &&
        List.exists (fun (pats, lam) -> is_guarded lam || is_lazy pats)
          pat_act_list
      then Partial
      else Total
(0016083)
frisch (developer)
2016-07-19 10:20

Frightening. Jacques: do you agree with my guess that this could even occur without when guards (with patterns that allocates and GC alarms/finalizers)?
(0017279)
xleroy (administrator)
2017-02-16 11:11

Currenty worked on at https://github.com/ocaml/ocaml/pull/717 [^]

- Issue History
Date Modified Username Field Change
2016-04-25 19:13 stedolan New Issue
2016-04-25 19:25 stedolan Note Added: 0015846
2016-04-25 19:28 yallop Relationship added related to 0005992
2016-04-25 19:34 stedolan Note Edited: 0015846 View Revisions
2016-04-25 19:35 stedolan Note Edited: 0015846 View Revisions
2016-04-26 11:48 bvaugon Note Added: 0015859
2016-05-03 11:29 doligez Status new => acknowledged
2016-05-03 11:29 doligez Target Version => 4.04.0 +dev / +beta1 / +beta2
2016-07-13 09:53 frisch Note Added: 0016063
2016-07-13 13:19 frisch Note Added: 0016067
2016-07-13 13:19 frisch Target Version 4.04.0 +dev / +beta1 / +beta2 => later
2016-07-19 07:40 garrigue Note Added: 0016081
2016-07-19 10:20 frisch Note Added: 0016083
2017-02-16 11:11 xleroy Note Added: 0017279
2017-02-16 11:11 xleroy Target Version later => 4.06.0 +dev/beta1/beta2/rc1
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-03-09 13:39 shinwell Assigned To => maranget
2017-03-09 13:39 shinwell Status acknowledged => assigned
2017-10-13 21:06 frisch Target Version 4.06.0 +dev/beta1/beta2/rc1 => 4.07.0+dev/beta2/rc1/rc2
2018-06-06 16:39 doligez Target Version 4.07.0+dev/beta2/rc1/rc2 =>


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker