Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005992OCamlOCaml backend (code generation)public2013-04-19 02:042013-04-26 00:54
Reporteryallop 
Assigned Tomaranget 
PrioritynormalSeveritymajorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0005992: Crash when pattern-matching lazy values modifies the scrutinee
Description$ cat lazypatterns.ml
type ('a, 'b) eq = Refl : ('a, 'a) eq

let cast (type a) (type b) (Refl : (a, b) eq) (x : a) = (x : b)

type ('a, 'b) either = L of 'a | R of 'b

type e = ((bool, bool) eq, (int, string) eq) either

let f : unit Lazy.t * unit Lazy.t * bool ref * e -> string = function
  | lazy (), _, {contents=false}, L x -> "ok"
  | _, lazy (), {contents=true}, L x -> "ok"
  | _, _, _, R refl -> cast refl 0 ^ "not ok"

let s = ref false
let set_true = lazy (s := true)
let set_false = lazy (s := false)

let _ = f (set_true, set_false, s, L Refl)
$ ocaml lazypatterns.ml
Segmentation fault (core dumped)
TagsNo tags attached.
Attached Filesdiff file icon lazypatterns.diff [^] (1,946 bytes) 2013-04-21 19:39 [Show Content]

- Relationships

-  Notes
(0009160)
meyer (developer)
2013-04-19 02:30
edited on: 2013-04-19 02:30

I can't reproduce crash on 4.00.1 32 bits Linux. Could you provide a gdb backtrace?

thanks

(0009161)
yallop (developer)
2013-04-19 02:37
edited on: 2013-04-19 02:37

It appears to crash with ocamlc, but raise Match_failure with ocamlopt.

 Program received signal SIGSEGV, Segmentation fault.
 0x000000000040f56a in caml_ml_string_length ()
 (gdb) where
 #0 0x000000000040f56a in caml_ml_string_length ()
 #1 0x000000000041c4fe in caml_interprete ()
 #2 0x000000000041dcb1 in caml_main ()
 0000003 0x000000000041b1fc in main ()

(0009162)
garrigue (manager)
2013-04-19 06:29

Interesting.
But I don't think this is related to GADTs.

let f = function
 | lazy (), _, {contents=None} -> "None", 0
 | _, lazy (), {contents=Some x} -> "Some", x

let s = ref None
let set_true = lazy (s := Some 1)
let set_false = lazy (s := None)

let _ = f (set_true, set_false, s)

Lazy patterns are not supposed to have side-effects, but what should we do when they have?
(0009163)
lefessan (developer)
2013-04-19 09:38

It is a known bug, lazy evaluation in pattern matching introduces the possibility to have side-effects that modify the values being pattern matched (it was actually discussed last Monday during the "bug meeting" that the local core team had).

We should probably change the way the pattern-matching is compiled in the presence of a combination of lazy values and mutable values, to have a less efficient but safer execution.
(0009164)
frisch (developer)
2013-04-19 16:09
edited on: 2013-04-19 16:13

When-guards can already change parts of the scrutinee. This is less powerful than lazy patterns, since this cannot be done within a single branch, but I guess there are some provisions to avoid bad surprises in that case (or not?). Could we use the same technique for lazy patterns?

(0009167)
lpw25 (developer)
2013-04-21 11:33

> When-guards can already change parts of the scrutinee. This is less powerful than lazy patterns, since this cannot be done within a single branch, but I guess there are some provisions to avoid bad surprises in that case (or not?).

This is done by always assuming that patterns containing when-guards are non-exhaustive, so that they raise a match failure exception instead of seg fault. As in the following example:

  $ cat bad-when.ml
  let g guard = function
    | (), _, {contents=false}, None -> "false"
    | _, _, _, _ when guard () -> "guard"
    | _, (), {contents=true}, None -> "true"
    | _, _, _, Some s -> s ^ "not ok"

  let s = ref true
  let _ = print_string (g (fun () -> s := false;false) ((), (), s, None))

  $ ocaml bad-when.ml
  Exception: Match_failure ("bad-when.ml", 1, 14).

The same thing could probably be done for lazy patterns.
(0009171)
lpw25 (developer)
2013-04-21 19:41

> The same thing could probably be done for lazy patterns.

I've attached a patch that does this. It certainly fixes Jeremy's example:

  ./ocaml ~/lazypatterns.ml
  Exception: Match_failure ("/home/leo/lazypatterns.ml", 9, 61).
(0009172)
lefessan (developer)
2013-04-21 20:27

I have two concerns with this solution:
(1) what is the semantics ? Currently, I cannot explain the semantics of "when" guards in the presence of side effects. For example:
## let x = ref 0;;
let _ =
    match x with
      { contents = 1 } -> 1
    | { contents = 0 } when (x := 1; false) -> 2
    | { contents = 1 } -> 2
    | _ -> 3
Warning 11: this match case is unused.
- : int = 3

For me, this is already a bug : the semantics should be that clauses are tested one line after the other one, and so, line "| { contents = 1 } -> 2" should be triggered, which is not the case. Using the same solution means increasing the problem instead of solving it...

(2) I think that, since pattern-matching is compiled on the typed tree, we should use the information that the matched value is immutable to enable optimal compilation only when it preserves the semantics, i.e. in the absence of either mutable values, OR in the absence of when/lazy constructs.
(0009173)
lpw25 (developer)
2013-04-21 20:56
edited on: 2013-04-21 20:58

> (1) what is the semantics ?

A relaxed semantics: the ordering between effects and matches is unspecified and any program relying on it is essentially incorrect. Of course a more well-specified semantics could be implemented, but only at the expense of efficiency.

> Using the same solution means increasing the problem instead of solving it...

These are really separate problems. One is a soundness bug due to using "incorrect" exhaustiveness information to guide an optimisation. The other is about whether matching in the presence of side-effects should have a well-specified semantics.

> (2) I think that, since pattern-matching is compiled on the typed tree, we should use the information that the matched value is immutable to enable optimal compilation only when it preserves the semantics, i.e. in the absence of either mutable values, OR in the absence of when/lazy constructs.

I certainly agree that the patterns only need to be marked as non-exhaustive if they access mutable values.

(0009175)
yallop (developer)
2013-04-22 10:08

I agree with Leo that there are two distinct issues here: the optimization based on the mistaken assumption of exhaustiveness, and the question of the order of evaluation for pattern matching. It's clear that we need to be more careful about assuming exhaustiveness when the match includes both lazy patterns and mutable data.

I agree with Fabrice that the current behaviour of both lazy patterns and guards is unsatisfactory with respect to ordering. People writing OCaml programs will generally assume that the semantics of matching is to consider the pattern cases top-to-bottom, left-to-right. Although the manual is careful to avoid actually saying anything about the order of matching, several OCaml books say that matching is sequential:

   "When a match expression is evaluated, the expression expression to be matched is first evaluated, and its value is compared with the patterns in order."
   Introduction to Objective Caml
   Jason Hickey

   "The expression expr is matched sequentially to the various patterns p1, ..., pn."
   Developing Applications With OCaml
   Emmanuel Chailloux, Pascal Manoury, Bruno Pagano

   "Cases are explored in a top-down fashion: when a branch fails, the analysis resumes with the next possible branch. However, the analysis stops as soon as the branch is successful; then, its right hand side is evaluated and returned as result."
   Using, Understanding, and Unraveling The OCaml Language From Practice to Theory and vice versa
   Didier Rémy
(0009177)
frisch (developer)
2013-04-22 11:51

In addition to changing the compilation scheme in presence of both mutable fields in the pattern *and* the possibility of side-effects (when-guard or lazy patterns), it would be good to report this as a warning.
(0009205)
maranget (manager)
2013-04-25 15:56

The bug is now fixed, in the sense that the proposed example
does not segfault any longer.


Luc
(0009208)
xleroy (administrator)
2013-04-25 16:41
edited on: 2013-04-25 16:54

@lefessan:

> what is the semantics ? Currently, I cannot explain the semantics of "when" guards in the presence of side effects.

It is entirely unspecified when those side effects occur w.r.t. the matching operation itself.

> For me, this is already a bug : the semantics should be that clauses are tested one line after the other one

I disagree. Pattern-matching is such an essential operation of the language that we want full liberty to compile in whatever testing order is efficient. And code such as your example should never be written in the first place.

@yallop:

> Although the manual is careful to avoid actually saying anything about the order of matching, several OCaml books say that matching is sequential:

They are all wrong.

(0009216)
yallop (developer)
2013-04-26 00:54

Thanks, Luc!

- Issue History
Date Modified Username Field Change
2013-04-19 02:04 yallop New Issue
2013-04-19 02:30 meyer Note Added: 0009160
2013-04-19 02:30 meyer Note Edited: 0009160 View Revisions
2013-04-19 02:37 yallop Note Added: 0009161
2013-04-19 02:37 yallop Note Edited: 0009161 View Revisions
2013-04-19 06:29 garrigue Note Added: 0009162
2013-04-19 09:38 lefessan Note Added: 0009163
2013-04-19 09:38 lefessan Status new => confirmed
2013-04-19 16:09 frisch Note Added: 0009164
2013-04-19 16:13 frisch Note Edited: 0009164 View Revisions
2013-04-21 11:33 lpw25 Note Added: 0009167
2013-04-21 19:39 lpw25 File Added: lazypatterns.diff
2013-04-21 19:41 lpw25 Note Added: 0009171
2013-04-21 20:27 lefessan Note Added: 0009172
2013-04-21 20:56 lpw25 Note Added: 0009173
2013-04-21 20:57 lpw25 Note Edited: 0009173 View Revisions
2013-04-21 20:58 lpw25 Note Edited: 0009173 View Revisions
2013-04-22 02:52 garrigue Assigned To => maranget
2013-04-22 02:52 garrigue Status confirmed => assigned
2013-04-22 10:08 yallop Note Added: 0009175
2013-04-22 11:51 frisch Note Added: 0009177
2013-04-25 15:55 maranget Status assigned => resolved
2013-04-25 15:55 maranget Resolution open => fixed
2013-04-25 15:56 maranget Note Added: 0009205
2013-04-25 16:41 xleroy Note Added: 0009208
2013-04-25 16:54 xleroy Note Edited: 0009208 View Revisions
2013-04-26 00:54 yallop Note Added: 0009216


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker