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.