Any formal execution definition of exception handling?

[sys5867]

Hello.

I'm interested in formal execution definition of WASM with exception handling proposal included.

What I now think is that the try catch end block semantics with throw instruction can be described in reduction rules, similar to PLDI'17 MVP spec paper.

Also, I heard from @aheejin that @rossberg has done some work on the formal spec of the proposal.

Are there in-progress works related to formal definition of exception handling?

[rossberg]

There is nothing written up in publishable form yet. So let me just dump the rules as an extension to the PLDI paper (or rather, the somewhat updated CACM version) in ASCII art here. Hope that helps answering your question. :)

Abstract Syntax

Value Types

t ::= ... | exnref

Exception Types

et ::= t*

Instructions

e ::= ... | throw x | rethrow | try ft e* catch e* end | br_on_exn l x

Exceptions

exn ::= ex* exception et | ex* exception et im

Modules

mod ::= module ... exn*

Typing

Contexts

C ::= {..., exn et*}

Rules

C_exn(x) = t*
----------------------------
C |- throw x : t1* t* -> t2*

--------------------------------
C |- rethrow : t1* exnref -> t2*

ft = t1* -> t2*
C, label t2* |- e1* : t1* -> t2*
C, label t2* |- e2* : exnref -> t2*
-----------------------------------
C |- try ft e1* catch e2* end : ft

C_label(l) = C_exn(x)
-------------------------------------
C |- br_on_exn l x : exnref -> exnref

Reduction

Stores

S ::= {..., exn ei*}

Exception Instances

ei ::= {type et}

Module Instances

m ::= {..., exn a*}

Values

v ::= ... | exn a v*

Administrative Instructions

e ::= ... | throw a | catch_n{e*} e* end | exn a v*

Throw Contexts

T ::= v* [_] e* | label_n{e*} T end | catch_n{e*} T end | frame_n{F} T end

Rules

F; throw x  -->  F; throw a
  (iff F_exn(x) = a)

v^n (try ft e1* catch e2* end)  -->  catch_m{e2*} (label_m{} v^n e1* end) end)
  (iff ft = t1^n -> t2^m)

catch_m{e*} v^m end  -->  v^m

S; F; catch_m{e*} T[v^n (throw a)] end  -->  S; F; label_m{} (exn a v^n) e* end
  (iff S_exn(a) = {typ t^n})

(exn a v*) rethrow  -->  v* (throw a)

ref.null rethrow  -->  trap

F; (exn a v*) (br_on_exn l x)  -->  F; v* (br l)
  (iff F_exn(x) = a)

F; (exn a v*) (br_on_exn l x)  -->  F; (exn a v*)
  (iff F_exn(x) =/= a)

F; ref.null (br_on_exn l x)  -->  F; trap

[sys5867]

Thank you for the response!
I have additional questions about the semantics provided.

In the proposal, br_on_exn pops the exnref values from the stack and instead pushes the exception's argument values on top of the stack, if given exception index matches. The typing rule for br_on_exn then should assume exnref value on the top, and result in t* values afterwards. In other words, the typing rule should be,

C_label(l) = C_exn(x) = t*
-------------------------------------------
C |- br_on_exn l x : exnref -> t*

Also in the reduction rule, exception values are represented as exn a v*. Reduction rules for rethrow and br_on_exn assumes that exception arguments v* resides in operand stack. In implementation, where exception argument values are actually stored? From my understanding, only exnref value stays at the stack and exception arguments are stored in linear memory space, where the exnref value points to. Is this correct interpretation, or am I missing something?

[rossberg]

No, the typing rule for br_on_exn is correct as given. Keep in mind that the values are only pushed onto the stack if the branch is taken, while the typing rule describes the stack manipulation of linear execution.

Exnref is an abstract (reference) type. It is an implementation detail how and where its argument values are stored. It is separate from any linear memory.

[rossberg]

@sys5867, sorry, as was just pointed out to me by @ioannad, there indeed was a bug in the typing rules for br_on_exn: the t* in the conclusion should not be there, the overall type should just be exnref -> exnref. Fixed now.

[ioannad]

@rossberg , with the addition of throw contexts, invoke might end up in a state where it neither succeeded with values nor has trapped, but is some throw context with a throw waiting for its catching try block. The simplest example is when invoking the function wasm_throw defined below:

(module  
   (type (func))
   (exception (export "exn") (type 0))
   (func (export "wasm_throw") (type 0)
      throw 0))

Invoking wasm_throw gets "stuck" in the state store; frame_1{F'} label_1 {} (throw tag) end end, where tag is the event address of exn, and F' the frame with the above module's instance.

I suppose this is the case meant by "the embedder defines how to handle the uncaught exception". But in this case it is not true any more that "Reduction terminates when a thread’s instruction sequence has been reduced to a result, that is, either a sequence of values or to a trap." (e.g., in the definition of evaluation contexts).

Should some other form of "result" (which is not a sequence of values or a trap) be defined to cover such cases of unresolved throw contexts?

[rossberg]

@ioannad, yes, correct: with exceptions we will naturally need to extend the notion of result to include throw a. And the rules for reducing evaluation contexts will also need a couple of extra rules to get there.

Basically, it all needs to mirror what we have for traps. Except that there also is the try rule to intercept a throw.