Aliasing of exception names

[fpottier]

Paulo de Vilhena (@DeVilhena-Paulo) and I would like to point out that in OCaml there can be aliasing between exception names, and ask how Gospel (and its tools) face this issue.

The problem stems from two main sources, we believe:

• The possibility of declaring exception E1 = E2. This causes the static names E1 and E2 to refer to the same dynamic name.

• The possibility of writing a functor with two parameters M1 and M2, each of which declares an exception E, and of instantiating this functor with twice the same module M. This causes the static names M1.E and M2.E to refer to the same dynamic name.

In summary, the fact that two exceptions E1 and E2 have different static names does not imply that these exceptions have distinct dynamic names. In some situations, it is possible to tell that they do have distinct dynamic names; this is typically the case when the definitions of these exceptions are local and visible. Most of the time, however, because of separate compilation and abstraction barriers, it is impossible to tell.

Naïvely ignoring this problem can lead to unsound reasoning: if E1 and E2 denote the same dynamic name, then an exception handler that appears to catch just E1 actually catches both E1 and E2. (@mariojppereira , does Cameleer defend against this danger, and if so, how?)

To work around this problem in Gospel, we believe that we may need:

• a way of publishing disjointness or uniqueness hypotheses; and/or
• a way of publishing a uniqueness fact.

For instance, a function (or functor) whose verification needs E1 and E2 to denote distinct dynamic names might publish the hypothesis E1 ≠ E2. (A more lightweight syntax may be needed, in order to avoid publishing a quadratic number of hypotheses. A separating conjunction of uniqueness hypotheses is a possibility.)

A module that creates a fresh exception name (by declaring exception E) might publish the fact that it uniquely owns this name. A functor that takes two parameters M1 and M2 might require unique ownership tokens for both M1.E and M2.E, which implies that these static names must denote distinct dynamic names.

The details are unclear to us; we believe that this topic might deserve discussion.

[mariojppereira]

Cameleer does not currently support aliasing of exception names (but fails with a very bad error message; I will work on this).

From the Gospel perspective, I have the following understanding:

• Officially, Gospel is a behavioral interface specification language. If my understanding is correct, one cannot declare exceptions aliasing in OCaml interface files. Hence, the question "might be solved" implicitly.
• Now, when it comes to effectively extend Gospel to support OCaml implementations, that is a different story. I agree we need to introduce some disjointedness annotation for exceptions.

[mariojppereira]

In order to support exceptions aliasing in Cameleer, since Why3 does not support exceptions aliasing, I am thinking about a very ad-hoc to solve this. Consider E1 and E2 are aliased exceptions. The OCaml code features a try ... with E2 -> ... block. Would it be correct to translate it as follows

  try ... with E2 | E1 -> ...

?

Meaning, I would have to collect the disjointedness permission and build a disjoint-set to fill a try ... with block with all the aliased exceptions.

[fpottier]

@mariojppereira, your proposal (which is to make it clear in the code that the handler catches both E1 and E2) makes sense, but this assumes that we know for sure that the static names E1 and E2 denote the same dynamic exception name.

I think we need to answer at least the following two questions:

• Which information to we want to keep track of? Do we want to always know with certainty whether two exception names denote the same name or denote distinct names? Or is it acceptable to allow a third situation, where we do not know with certainty (and therefore must be conservative)?
• By what means do we keep track of this information? We probably need new forms and declarations and hypotheses, e.g., "I assume that these exception names are distinct", or "I claim that this exception name is unique".