Bugs with pattern-matching and exceptions

Bugs with pattern-matching and exceptions

[Louis Gesbert]

There seems to be some problems with exceptions related to pattern-matching
in Ocaml.

First, exceptions don't support marshalling. This problem is already known,
but yet undocumented. The problem doesn't arises when an exception is
marshalled or unmarshalled however, but only when you try to pattern-match
the un-marshalled value -- which, in my experience, hangs the program --.
Equality tests work fine. I managed to build a workaround for this problem
using ugly Obj code, but some feedback on wether this problem is going to
be solved in future versions of Caml would be appreciated.

More recently, I discovered a far worse bug which leads to some
inconsistency. Ocaml offers a syntax " exception E' = E " to create an
alias to an exception, which I have hardly ever seen used (with reason, it
seems). See the following code:

# exception E;;
exception E
# exception E' = E;;
exception E'
# exception E;;
exception E
# E;;
- : exn = E
# E';;
- : exn = E
(* At this stage, E and E' should be two distinct exceptions both called E.
Nothing wrong yet, that kind of weird situation can also be created with
types (redefining a type when objects of this type exist) *)
# E = E';;
- : bool = true
# match E with E' -> true | _ -> false;;
- : bool = false

The exceptions are equal, but don't match according to the toplevel... my
opinion is that they should be different in both cases: they were defined
separately with two different definitions of "exception E".
When E is parametrised with a type, this can lead to a failure of the type
system (objects of type t = T are shown as int = 0 !)

This is with Caml 3.08.3, but it doesn't seem to have been corrected in
earlier versions. Any ideas ? If the structure exception E = F is
considered useful, a stronger semantics should be attached to it, but is it
really ?

These two problems point to the handling of pattern-matching of exceptions,
maybe not the marshalling of exceptions itself. Could someone explain where
this weakness comes from (implementation of the extensible variable type ?)

Regards,
Louis Gesbert

Re: [Caml-list] Bugs with pattern-matching and exceptions

[Alain Frisch]

Louis Gesbert wrote:
> More recently, I discovered a far worse bug which leads to some
> inconsistency. Ocaml offers a syntax " exception E' = E " to create an
> alias to an exception, which I have hardly ever seen used (with reason, it
> seems).

The problem you raise is not related to the "exception E' = E" 
construction. E.g.:

# exception E of int;;
exception E of int
# let x = E 1;;
val x : exn = E 1
# exception E of bool;;
exception E of bool
# let y = E true;;
val y : exn = E true
# x = y;;
- : bool = true

Comparing values of different types can be unsafe, I guess, when the 
values are custom blocks.

Exception definitions are generative. The equality of two exception 
constructors, as checked by pattern matching, is implemented as 
reference (pointer) equality. Concretely, the identity of an exception 
constructor is a "string ref", whose content corresponds to the 
displayed name of the exception. Unfortunately, the generic comparison
function has no way to know that the blocks under consideration are 
exceptions and that the constructoes should thus be compared physically. 
For equality, this would be quite simple to patch (e.g. reserve a 
special GC tag to indicate exception blocks). For the total ordering, 
one could e.g. generate a globally unique integer identifier (pointer 
comparison does not work because blocks can be moved by the GC).

The other solution is to keep ourselves from using generic comparison 
for exceptions and to rely only on pattern matching.

-- Alain

Re: [Caml-list] Bugs with pattern-matching and exceptions

[Jacques Garrigue]

From: Louis Gesbert <louis.gesbert@laposte.net>

> # exception E' = E;;
> # match E with E' -> true | _ -> false;;
> - : bool = false
>
> This is with Caml 3.08.3, but it doesn't seem to have been corrected in
> earlier versions. Any ideas ? If the structure exception E = F is
> considered useful, a stronger semantics should be attached to it, but is it
> really ?

In general bugs are not corrected in _earlier_ versions :-)
This is fixed in 3.09.

# exception E' = E;;
# match E with E' -> true | _ -> false;;
- : bool = true

Jacques Garrigue

Re: [Caml-list] Bugs with pattern-matching and exceptions

[Alain Frisch]

Jacques Garrigue wrote:
> This is fixed in 3.09.
> 
> # exception E' = E;;
> # match E with E' -> true | _ -> false;;
> - : bool = true

This worked also in 3.08 and is not what Louis complained about
("exception E;; exception E'=E;; exception E;; E=E'" returning true).
I think there is and was really no bug in the pattern matching, just a 
weird behavior of the generic comparison function on exception values.

-- Alain

Re: [Caml-list] Bugs with pattern-matching and exceptions

[Louis Gesbert]

> Can you reproduce this failure of the type system in the top-level
> without using marshalling? I haven't been able to.

Yes, this was without marshalling: when you use an alias to an exception
which has been redefined afterwards, some type information seems to be lost
by the top-level.

# type t = X;;
type t = X
# exception E of t;;
exception E of t
# exception E' = E;;
exception E' of t
# E' X;;
- : exn = E X
# exception E of string;;
exception E of string
# E' X;;
- : exn = E 0

Here we alias E with E', then redefine E (no matter with what), and E'
shows its argument as int... However, this seems to be only a problem with
the toplevel pretty-printer, not a real type problem since I didn't manage
to make O'Caml accept badly typed expressions this way. This is with O'Caml
3.09.1.

I guess this is linked to the problems of equality and marshalling:
exceptions are non-standard variant types which confuse the run-time in
some dark corners.

Re: [Caml-list] Bugs with pattern-matching and exceptions

[Louis Gesbert]

> >  However, if you try to pattern-match against it, the process just hangs.
>
> Can you give an example to reproduce that?  The program above works fine.

My mistake, O'Caml didn't hang: the complex situation where this
problem occured just led to a deadlock, the states of the processes
having become inconsistent (two of them could make different decisions
out of the same data, depending on wether it was locally created or
received from another).

> More precisely, it doesn't distinguish an exception constructor from
> a string reference. Marshalling and unmarshalling produce a shallow
> copy.

Thanks, that explains it.

> I don't see a good semantics for such a program, except considering that
> unmarshalled exceptions must always be different (w.r.t. pattern
> matching) from exceptions defined in the current program, which AFAIK is
> the current semantics.

Right, that's an interesting problem. I wasn't aware exceptions were
imperative to that extent, being registered dynamically whenever
defined: they look much more like type definitions at first. The
always-different semantics doesn't feel satisfying to me however,
neither does the fact that an exception can escape the scope of the
types it includes (thus becoming a black box). We fall back to the
debate about local exceptions here.

However, couldn't a semantics where exceptions defined in local
modules are always different, but other kinds of exceptions are
compared with an incremented global counter be consistent ? The main
issue is that there is no unique id for an exception, it is shown as
Mod.Exn but Mod as well as Exn can be redefined... hence the pointer
comparison, as I understand it. Note that exceptions defined in local
modules are already somewhat different from the others (unprefixed):

# module M1 = struct exception E end
  let module M2 = struct exception E end
  in M1.E,M2.E
  - : exn * exn = (M1.E, E)

The point is, most often you won't redefine your exceptions and there is no
ambiguity in Mod.Exn, so it would be very satisfactory for the exception
exchange to work in that case. A semantics that allows that and handles
more difficult cases probably exists.

Some inconsistency remains anyway with always-different marshalled
exceptions (although they might be imputed to the unsafe marshalling):
an unmarshalled exception is of type exn, but you can't raise it (or
you will get a Failure "input_value: bad object").

Whatever the solution, I think we need a very clear semantics
here. That exceptions shouldn't be marshalled should at least be
mentioned in the Marshal documentation.

Regards,
Louis

Re: [Caml-list] Bugs with pattern-matching and exceptions

[Alain Frisch]

Louis Gesbert wrote:
> Let's suppose we have two processes running the exact same compiled program.

I guess exceptions are too dynamic for this criterion to be useful.
You could imagine an implementation of exception equality based on 
unique integers assigned sequentially to exception constructors when 
they are created. But this doesn't work in general. Consider:

let f b =
   let module M = struct exception E end in
   if b then Marshal.to_channel stdout M.E []
   else match Marshal.from_channel stdin with
      | M.E -> print_endline "Equal"
      | _ -> print_endline "Not equal"

let () =
   if (Array.length Sys.argv >= 2) then f true else f false

I don't see a good semantics for such a program, except considering that 
unmarshalled exceptions must always be different (w.r.t. pattern 
matching) from exceptions defined in the current program, which AFAIK is 
the current semantics.

> However, if you try to pattern-match against it, the process just hangs.

Can you give an example to reproduce that?  The program above works fine.

leoville ~/bug $ ./exn x | ./exn
Not equal

> As I understand it, the constructor Ex of the variant type exn is
> represented by a pointer in (Ex "arg"), and this pointer is kept as-is by
> the marshaller which doesn't understand the particular structure of
> exceptions.

More precisely, it doesn't distinguish an exception constructor from a 
string reference. Marshalling and unmarshalling produce a shallow copy.


-- Alain

Re: [Caml-list] Bugs with pattern-matching and exceptions

[Louis Gesbert]

> Marshalling is known to be type unsafe, of course, so that's "not a
> problem" although it would be nice to have type-safe marshalling.

I don't agree here, there really *is* a problem with marshalling
exceptions, independently from type safety: it doesn't work. This problem
has already been mentionned on the list (and in the bug tracker), which is
why I didn't describe it in detail. However, it would be nice to have a
word from the caml team about it.

Let's suppose we have two processes running the exact same compiled program.
- Process A marshalls an exception (Ex "arg")
- Process A transmits the resulting string to process B
- Process B unmarshalls the string, and makes sure to type it as an
exception. Since we have the same compiled program, exception Ex is defined
in the same way in A and B.
- On process B, the exception *seems* right, and you can test equality.
However, if you try to pattern-match against it, the process just hangs.

As I understand it, the constructor Ex of the variant type exn is
represented by a pointer in (Ex "arg"), and this pointer is kept as-is by
the marshaller which doesn't understand the particular structure of
exceptions.

The (awfully ugly ;-)) workaround I used (I *really* needed to marshal
exceptions, you see...) is to extract the constructor (as a string) and the
parameters from the exception, using Obj, marshal the couple and deal with
it on the receiving hand.

> However, what happens with dynamically loaded bytecode that declares
> new exceptions? Perhaps there is some unsoundness there... :-)

Yes, that could be worth looking into, but I don't actually think it makes
the problem worse since the structure of exceptions is already dynamic.

Thanks for the pointers :-)
Louis