if_except with block params (multi-value proposal)

[binji]

The if_except true branch extracts the values from the exception and pushes them on to the stack. The multi-value proposal also allows you to have block params. How do these two features interact?

e.g.

(except $e i64)
...
(func
  try
    ...
  catch
    if_except (param i32) $e
      ;; what is on the stack here?
      ...

[binji]

Same question w/ catch blocks, now that I think of it:

...
try (param i32)
  ...
catch
  ;; what is on the stack here?
  ;;   * [i32 except_ref]
  ;;   * [except_ref i32]
  ;;   * [except_ref]
  ...

[eholk]

Huh, interesting question.

My first instinct is to same any block params are pushed onto the stack first, and then the exception values in the case of if_except or the exception ref in the case of catch. I think of block params as letting you see into the stack before control transferred to your block, and this interpretation seems consistent with that.

[binji]

Yeah, that's what I was thinking too, at least for if_except. catch seems different to me, though, since it may happen much later when the stack is completely different, so you'd have to save the params somewhere to push later when the exception is thrown.

[rossberg]

Catch shouldn't get the block params, they have already been consumed at that point.

FWIW, in the context of investigating effect handlers with a couple of collaborators, I have recently spelled out the formal semantics for the exception proposal, which I had meant to post for a while. Maybe it helps.

Abstract Syntax

Exception definitions

exn ::= exception <exntype>
exntype ::= [<valtype>*]

Value types

valtype ::= ... | exn

Instructions

instr ::= ...
  | throw <exnidx>
  | rethrow
  | try <functype> <instr>* catch <instr>* end
  | handle <functype> <exnidx> <instr>* else <instr>* end

Administrative instructions

instr ::= ...
  | catch_n{<instr>*} <instr>* end   (active catch handler)
  | thrown <exnaddr> <val>*          (ongoing throw)
  | caught <exnaddr> <val>*          (caught exception)

val ::= ... | caught a v*

Typing

Contexts

C ::= { ..., exn <exntype>* }

Instructions

C.exn(x) = [t*]
---------------------------------------
C |- throw x : [t1* t*] -> [t2*]

----------------------------------------
C |- rethrow : [t1* exn] -> [t2*]

ft = [t1*] -> [t2*]
C,label [t2*] |- instr1* : ft
C,label [t2*] |- instr2* : [exn] -> [t2*]
------------------------------------------------------------------
C |- try ft instr1* catch instr2* end : ft

ft = [t1*] -> [t2*]
C.exn(x) = [t*]
C,label [t2*] |- instr1* : [t1* t*] -> [t2*]
C,label [t2*] |- instr2* : [t1* exn] -> [t2*]
----------------------------------------------------------------------
C |- handle ft x instr1* else instr2* end : [t1* exn] -> [t2*]

(Note the lack of t1* on the stack in the catch block)

Administrative instructions (for soundness proof)

S; C,label [t2*] |- instr* : [t1*] -> [t2*]
S; C,label [t2*] |- instr0* : [exn] -> [t2*]
-------------------------------------------------------
S; C |- catch_n{instr0*} instr* end : [t1*] -> [t2*]

S.exn(a) = [t*]
(C |- v : t)*
-----------------------------
S; C |- thrown a v* : [t1*] -> [t2*]

S.exn(a) = [t*]
(C |- v : t)*
----------------------------------------------------
S; C |- caught a v* : [] -> [exn]

Execution

Module instance

moduleinst ::= {..., exn <exnaddr>*}

Store

S ::= {..., exn <exntype>*}

Throw contexts

ET ::= val* _ instr* | label_n{instr*} ET end | frame_n{F} ET end

Reduction

F; v^n (throw x)  -->  F; (thrown a v^n)
  iff F.module.exn(x) = a
      S.exn(a) = [t^n]

(caught a v^n) rethrow  -->  (thrown a v^n)

v^n (try ft instr1* catch instr2* end)  -->  catch_m{instr2*} (label_m{} v^n instr1* end) end
  iff ft = [t1^n] -> [t2^m]

catch_m{instr*} v* end  -->  v*

S; F; catch_m{instr*} ET[(thrown a v^n)] end  -->  S'; F; label_m{} (caught a v^n) instr* end
  iff S.exn(a) = [t^n]

F; v1^n (caught a v*) handle ft x instr1* else instr2* end  -->  F; label_m{} v1^n v* instr1* end
  iff F.module.exn(x) = a
      ft = [t1^n] -> [t2^m]

F; v1^n (caught a v*) handle ft x instr1* else instr2* end  -->  F; label_m{} v1^n (caught a v*) instr2* end
  iff F.module.exn(x) =/= a
      ft = [t1^n] -> [t2^m]

[aheejin]

Now we switched to br_on_exn, so closing this.