diff --git a/README.md b/README.md index 26ff0e4c..40df53be 100644 --- a/README.md +++ b/README.md @@ -1,43 +1,17 @@ -[![Build Status](https://travis-ci.org/WebAssembly/spec.svg?branch=master)](https://travis-ci.org/WebAssembly/spec) +[![Build Status](https://travis-ci.org/WebAssembly/exception-handling.svg?branch=master)](https://travis-ci.org/WebAssembly/exception-handling) -# Exception handling +# Exception Handling Proposal for WebAssembly This repository holds a [proposal](https://github.com/WebAssembly/exception-handling/blob/master/proposals/Exceptions.md) for adding exception handling to WebAssembly. -The exception handling proposal depends on the [reference-types](https://github.com/WebAssembly/reference-types) proposal -and on the [multi-value](https://github.com/WebAssembly/multi-value) proposal. +* See the [proposal overview](proposals/Exceptions.md) for a summary of the proposal. -The repository is a clone -of [WebAssembly/spec](https://github.com/WebAssembly/spec), first rebased on the spec of its dependency [reference-types](https://github.com/WebAssembly/reference-types), and then merged with the other dependency [multi-value](https://github.com/WebAssembly/multi-value). +The repository is now based on the [reference types proposal](proposals/reference-types/Overview.md) and includes all respective changes. -The remainder of the document has contents of the two README files of the dependencies: [reference-types/README.md](https://github.com/WebAssembly/reference-types/blob/master/README.md) and [multi-value/README.md](https://github.com/WebAssembly/multi-value/blob/master/README.md). - -# Reference Types Proposal for WebAssembly - -[![Build Status](https://travis-ci.org/WebAssembly/reference-types.svg?branch=master)](https://travis-ci.org/WebAssembly/reference-types) - -This repository is a clone of [github.com/WebAssembly/spec/](https://github.com/WebAssembly/spec/). -It is meant for discussion, prototype specification and implementation of a proposal to add support for basic reference types to WebAssembly. - -* See the [overview](https://github.com/WebAssembly/reference-types/blob/master/proposals/reference-types/Overview.md) for a summary of the proposal. - -* See the [modified spec](https://webassembly.github.io/reference-types/) for details. - -# Multi-value Proposal for WebAssembly - -[![Build Status](https://travis-ci.org/WebAssembly/multi-value.svg?branch=master)](https://travis-ci.org/WebAssembly/multi-value) - -This repository is a clone of [github.com/WebAssembly/spec/](https://github.com/WebAssembly/spec/). -It is meant for discussion, prototype specification and implementation of a proposal to add support for returning multiple values to WebAssembly. - -* See the [overview](https://github.com/WebAssembly/multi-value/blob/master/proposals/multi-value/Overview.md) for a summary of the proposal. - -* See the [modified spec](https://webassembly.github.io/multi-value/) for details. - -Original `README` from upstream repository follows... +Original README from upstream repository follows... # spec diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index be20a535..fa7e3879 100644 --- a/document/core/appendix/algorithm.rst +++ b/document/core/appendix/algorithm.rst @@ -25,13 +25,13 @@ Types are representable as an enumeration. .. code-block:: pseudo - type val_type = I32 | I64 | F32 | F64 | Funcref | Externref + type val_type = I32 | I64 | F32 | F64 | Funcref | Exnref | Externref func is_num(t : val_type) : bool = return t = I32 || t = I64 || t = F32 || t = F64 func is_ref(t : val_type) : bool = - return t = Funcref || t = Externref + return t = Funcref || t = Exnref || t = Externref The algorithm uses two separate stacks: the *value stack* and the *control stack*. The former tracks the :ref:`types ` of operand values on the :ref:`stack `, @@ -210,6 +210,15 @@ Other instructions are checked in a similar manner. error_if(frame.opcode =/= if) push_ctrl(else, frame.start_types, frame.end_types) + case (try t1*->t2*) + pop_vals([t1*]) + push_ctrl(try, [t1*], [t2*]) + + case (catch) + let frame = pop_ctrl() + error_if(frame.opcode =/= try) + push_ctrl(catch, [exnref], frame.end_types) + case (br n)      error_if(ctrls.size() < n)       pop_vals(label_types(ctrls[n])) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index db83ae26..4f3e532b 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -76,7 +76,7 @@ Store .. math:: \begin{array}{lclll} - \F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\ + \F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon, ~\SEXNS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\ \end{array} @@ -539,6 +539,28 @@ Memories \end{array} +.. index:: exception, exception address, store, exception instance, exception type, function type +.. _embed-exn: + +Exceptions +~~~~~~~~~~ + +.. _embedd-exn-alloc: + +:math:`\F{exn\_alloc}(\store, \exntype) : (\store, \exnaddr)` +............................................................. + +1. Pre-condition: :math:`exntype` is :ref:`valid `. + +2. Let :math:`\exnaddr` be the result of :ref:`allocating an exception ` in :math:`\store` with :ref:`exception type ` :math:`\exntype`. + +3. Return the new store paired with :math:`\exnaddr`. + +.. math:: + \begin{array}{lclll} + \F{exn\_alloc}(S, \X{et}) &=& (S', \X{a}) && (\iff \allocexn(S, \X{et}) = S', \X{a}) \\ + \end{array} + .. index:: global, global address, store, global instance, global type, value .. _embed-global: diff --git a/document/core/appendix/implementation.rst b/document/core/appendix/implementation.rst index d5e53920..c51315b0 100644 --- a/document/core/appendix/implementation.rst +++ b/document/core/appendix/implementation.rst @@ -36,6 +36,7 @@ An implementation may impose restrictions on the following dimensions of a modul * the number of :ref:`functions ` in a :ref:`module `, including imports * the number of :ref:`tables ` in a :ref:`module `, including imports * the number of :ref:`memories ` in a :ref:`module `, including imports +* the number of :ref:`exceptions ` in a :ref:`module `, including imports * the number of :ref:`globals ` in a :ref:`module `, including imports * the number of :ref:`element segments ` in a :ref:`module ` * the number of :ref:`data segments ` in a :ref:`module ` @@ -123,6 +124,7 @@ Restrictions on the following dimensions may be imposed during :ref:`execution < * the number of allocated :ref:`function instances ` * the number of allocated :ref:`table instances ` * the number of allocated :ref:`memory instances ` +* the number of allocated :ref:`exception instances ` * the number of allocated :ref:`global instances ` * the size of a :ref:`table instance ` * the size of a :ref:`memory instance ` diff --git a/document/core/appendix/index-instructions.rst b/document/core/appendix/index-instructions.rst index 694b47d0..a12a2d5e 100644 --- a/document/core/appendix/index-instructions.rst +++ b/document/core/appendix/index-instructions.rst @@ -13,11 +13,11 @@ Instruction Binary Opcode Type :math:`\LOOP~\X{bt}` :math:`\hex{03}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` :math:`\IF~\X{bt}` :math:`\hex{04}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` :math:`\ELSE` :math:`\hex{05}` -(reserved) :math:`\hex{06}` -(reserved) :math:`\hex{07}` -(reserved) :math:`\hex{08}` -(reserved) :math:`\hex{09}` -(reserved) :math:`\hex{0A}` +:math:`\TRY~\X{bt}` :math:`\hex{06}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\CATCH` :math:`\hex{07}` +:math:`\THROW~x` :math:`\hex{08}` :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\RETHROW` :math:`\hex{09}` :math:`[t_1^\ast~\EXNREF] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\BRONEXN~l~x` :math:`\hex{0A}` :math:`[\EXNREF] \to [\EXNREF]` :ref:`validation ` :ref:`execution ` :math:`\END` :math:`\hex{0B}` :math:`\BR~l` :math:`\hex{0C}` :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` :math:`\BRIF~l` :math:`\hex{0D}` :math:`[t^\ast~\I32] \to [t^\ast]` :ref:`validation ` :ref:`execution ` diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst index dde34900..bfda65ed 100644 --- a/document/core/appendix/index-rules.rst +++ b/document/core/appendix/index-rules.rst @@ -18,6 +18,7 @@ Construct Judgement :ref:`Block type ` :math:`\vdashblocktype \blocktype \ok` :ref:`Table type ` :math:`\vdashtabletype \tabletype \ok` :ref:`Memory type ` :math:`\vdashmemtype \memtype \ok` +:ref:`Exception type ` :math:`\vdashexntype \exntype \ok` :ref:`Global type ` :math:`\vdashglobaltype \globaltype \ok` :ref:`External type ` :math:`\vdashexterntype \externtype \ok` :ref:`Instruction ` :math:`S;C \vdashinstr \instr : \functype` @@ -26,6 +27,7 @@ Construct Judgement :ref:`Function ` :math:`C \vdashfunc \func : \functype` :ref:`Table ` :math:`C \vdashtable \table : \tabletype` :ref:`Memory ` :math:`C \vdashmem \mem : \memtype` +:ref:`Exception ` :math:`C \vdashexn \exn : \exntype` :ref:`Global ` :math:`C \vdashglobal \global : \globaltype` :ref:`Element segment ` :math:`C \vdashelem \elem : \reftype` :ref:`Element mode ` :math:`C \vdashelemmode \elemmode : \reftype` @@ -54,6 +56,7 @@ Construct Judgement :ref:`Function instance ` :math:`S \vdashfuncinst \funcinst : \functype` :ref:`Table instance ` :math:`S \vdashtableinst \tableinst : \tabletype` :ref:`Memory instance ` :math:`S \vdashmeminst \meminst : \memtype` +:ref:`Exception instance ` :math:`S \vdashexninst \exninst : \exntype` :ref:`Global instance ` :math:`S \vdashglobalinst \globalinst : \globaltype` :ref:`Element instance ` :math:`S \vdasheleminst \eleminst \ok` :ref:`Data instance ` :math:`S \vdashdatainst \datainst \ok` @@ -97,6 +100,7 @@ Construct Judgement :ref:`Function instance ` :math:`\vdashfuncinstextends \funcinst_1 \extendsto \funcinst_2` :ref:`Table instance ` :math:`\vdashtableinstextends \tableinst_1 \extendsto \tableinst_2` :ref:`Memory instance ` :math:`\vdashmeminstextends \meminst_1 \extendsto \meminst_2` +:ref:`Exception instance ` :math:`\vdashexninstextends \exninst_1 \extendsto \exninst_2` :ref:`Global instance ` :math:`\vdashglobalinstextends \globalinst_1 \extendsto \globalinst_2` :ref:`Element instance ` :math:`\vdasheleminstextends \eleminst_1 \extendsto \eleminst_2` :ref:`Data instance ` :math:`\vdashdatainstextends \datainst_1 \extendsto \datainst_2` diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst index 413e6f0b..4942fb40 100644 --- a/document/core/appendix/index-types.rst +++ b/document/core/appendix/index-types.rst @@ -15,11 +15,13 @@ Category Constructor (reserved) :math:`\hex{7B}` .. :math:`\hex{71}` :ref:`Reference type ` |FUNCREF| :math:`\hex{70}` (-16 as |Bs7|) :ref:`Reference type ` |EXTERNREF| :math:`\hex{6F}` (-17 as |Bs7|) -(reserved) :math:`\hex{6E}` .. :math:`\hex{61}` +:ref:`Reference type ` |EXNREF| :math:`\hex{68}` (-18 as |Bs7|) +(reserved) :math:`\hex{6D}` .. :math:`\hex{61}` :ref:`Function type ` :math:`[\valtype^\ast] \to [\valtype^\ast]` :math:`\hex{60}` (-32 as |Bs7|) (reserved) :math:`\hex{5F}` .. :math:`\hex{41}` :ref:`Result type ` :math:`[\epsilon]` :math:`\hex{40}` (-64 as |Bs7|) :ref:`Table type ` :math:`\limits~\reftype` (none) :ref:`Memory type ` :math:`\limits` (none) +:ref:`Exception type ` :math:`\functype` (none) :ref:`Global type ` :math:`\mut~\valtype` (none) ======================================== =========================================== =============================================================================== diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 30cb620c..5caf20c2 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -67,14 +67,14 @@ Store Validity The following typing rules specify when a runtime :ref:`store ` :math:`S` is *valid*. A valid store must consist of -:ref:`function `, :ref:`table `, :ref:`memory `, :ref:`global `, and :ref:`module ` instances that are themselves valid, relative to :math:`S`. +:ref:`function `, :ref:`table `, :ref:`memory `, :ref:`exception `, :ref:`global `, and :ref:`module ` instances that are themselves valid, relative to :math:`S`. -To that end, each kind of instance is classified by a respective :ref:`function `, :ref:`table `, :ref:`memory `, or :ref:`global ` type. +To that end, each kind of instance is classified by a respective :ref:`function `, :ref:`table `, :ref:`memory `, :ref:`exception `, or :ref:`global ` type. Module instances are classified by *module contexts*, which are regular :ref:`contexts ` repurposed as module types describing the :ref:`index spaces ` defined by a module. -.. index:: store, function instance, table instance, memory instance, global instance, function type, table type, memory type, global type +.. index:: store, function instance, table instance, memory instance, exception instance, global instance, function type, table type, memory type, exception type, global type :ref:`Store ` :math:`S` ..................................... @@ -85,6 +85,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co * Each :ref:`memory instance ` :math:`\meminst_i` in :math:`S.\SMEMS` must be :ref:`valid ` with some :ref:`memory type ` :math:`\memtype_i`. +* Each :ref:`exception instance ` :math:`\exninst_i` in :math:`S.\SEXNS` must be :ref:`valid ` with some :ref:`exception type ` :math:`\exntype_i`. + * Each :ref:`global instance ` :math:`\globalinst_i` in :math:`S.\SGLOBALS` must be :ref:`valid ` with some :ref:`global type ` :math:`\globaltype_i`. * Each :ref:`element instance ` :math:`\eleminst_i` in :math:`S.\SELEMS` must be :ref:`valid `. @@ -103,6 +105,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \\ (S \vdashmeminst \meminst : \memtype)^\ast \qquad + (S \vdashexninst \exninst : \exntype)^\ast + \\ (S \vdashglobalinst \globalinst : \globaltype)^\ast \\ (S \vdasheleminst \eleminst \ok)^\ast @@ -113,6 +117,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \SFUNCS~\funcinst^\ast, \STABLES~\tableinst^\ast, \SMEMS~\meminst^\ast, + \SEXNS~\exninst^\ast, + \\ \SGLOBALS~\globalinst^\ast, \SELEMS~\eleminst^\ast, \SDATAS~\datainst^\ast \} @@ -253,6 +259,24 @@ Module instances are classified by *module contexts*, which are regular :ref:`co } +.. index:: exception type, exception instance, exception tag, function type +.. _valid-exninst: + +:ref:`Exception Instances ` :math:`\{ \EITYPE~\exntype \}` +........................................................................... + +* The :ref:`exception type ` :math:`\exntype` must be :ref:`valid `. + +* Then the exception instance is valid with :ref:`exception type ` :math:`\exntype`. + +.. math:: + \frac{ + \vdashexntype \exntype \ok + }{ + S \vdashexninst \{ \EITYPE~\exntype \} : \exntype + } + + .. index:: global type, global instance, value, mutability .. _valid-globalinst: @@ -291,7 +315,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \frac{ (S \vdash \reff : t)^\ast }{ - S \vdasheleminst \{ \EITYPE~t, \EIELEM~\reff^\ast \} \ok + S \vdasheleminst \{ \EIELEMTYPE~t, \EIELEM~\reff^\ast \} \ok } @@ -342,6 +366,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co * For each :ref:`memory address ` :math:`\memaddr_i` in :math:`\moduleinst.\MIMEMS`, the :ref:`external value ` :math:`\EVMEM~\memaddr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETMEM~\memtype_i`. +* For each :ref:`exception address ` :math:`\exnaddr_i` in :math:`\moduleinst.\MIEXNS`, the :ref:`external value ` :math:`\EVEXN~\exnaddr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETEXN~\exntype_i`. + * For each :ref:`global address ` :math:`\globaladdr_i` in :math:`\moduleinst.\MIGLOBALS`, the :ref:`external value ` :math:`\EVGLOBAL~\globaladdr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETGLOBAL~\globaltype_i`. * For each :ref:`element address ` :math:`\elemaddr_i` in :math:`\moduleinst.\MIELEMS`, the :ref:`element instance ` :math:`S.\SELEMS[\elemaddr_i]` must be :ref:`valid `. @@ -358,31 +384,26 @@ Module instances are classified by *module contexts*, which are regular :ref:`co * Let :math:`\memtype^\ast` be the concatenation of all :math:`\memtype_i` in order. +* Let :math:`\exntype^\ast` be the concatenation of all :math:`\exntype_i` in order. + * Let :math:`\globaltype^\ast` be the concatenation of all :math:`\globaltype_i` in order. -* Then the module instance is valid with :ref:`context ` :math:`\{\CTYPES~\functype^\ast, \CFUNCS~{\functype'}^\ast, \CTABLES~\tabletype^\ast, \CMEMS~\memtype^\ast, \CGLOBALS~\globaltype^\ast\}`. +* Then the module instance is valid with :ref:`context ` :math:`\{\CTYPES~\functype^\ast, \CFUNCS~{\functype'}^\ast, \CTABLES~\tabletype^\ast, \CMEMS~\memtype^\ast, \CEXNS~\exntype^\ast, \CGLOBALS~\globaltype^\ast\}`. .. math:: ~\\[-1ex] \frac{ - \begin{array}{@{}c@{}} - (\vdashfunctype \functype \ok)^\ast - \\ - (S \vdashexternval \EVFUNC~\funcaddr : \ETFUNC~\functype')^\ast - \qquad - (S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\tabletype)^\ast - \\ - (S \vdashexternval \EVMEM~\memaddr : \ETMEM~\memtype)^\ast - \qquad - (S \vdashexternval \EVGLOBAL~\globaladdr : \ETGLOBAL~\globaltype)^\ast - \\ - (S \vdasheleminst S.\SELEMS[\elemaddr] \ok)^\ast - \qquad - (S \vdashdatainst S.\SDATAS[\dataaddr] \ok)^\ast - \\ - (S \vdashexportinst \exportinst \ok)^\ast - \qquad - (\exportinst.\EINAME)^\ast ~\mbox{disjoint} + \begin{array}{@{}rcl@{}} + (\vdashfunctype \functype \ok)^\ast & \quad & + (S \vdashexternval \EVFUNC~\funcaddr : \ETFUNC~\functype')^\ast \\ + (S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\tabletype)^\ast & \quad & + (S \vdashexternval \EVMEM~\memaddr : \ETMEM~\memtype)^\ast \\ + (S \vdashexternval \EVEXN~\exnaddr : \ETEXN~\exntype)^\ast & \quad & + (S \vdashexternval \EVGLOBAL~\globaladdr : \ETGLOBAL~\globaltype)^\ast \\ + (S \vdasheleminst S.\SELEMS[\elemaddr] \ok)^\ast & \quad & + (S \vdashdatainst S.\SDATAS[\dataaddr] \ok)^\ast \\ + (S \vdashexportinst \exportinst \ok)^\ast & \quad & + (\exportinst.\EINAME)^\ast ~\mbox{disjoint} \\ \end{array} }{ S \vdashmoduleinst \{ @@ -391,6 +412,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \MIFUNCS & \funcaddr^\ast, \\ \MITABLES & \tableaddr^\ast, \\ \MIMEMS & \memaddr^\ast, \\ + \MIEXNS & \exnaddr^\ast, \\ \MIGLOBALS & \globaladdr^\ast, \\ \MIELEMS & \elemaddr^\ast, \\ \MIDATAS & \dataaddr^\ast, \\ @@ -400,6 +422,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \CFUNCS & {\functype'}^\ast, \\ \CTABLES & \tabletype^\ast, \\ \CMEMS & \memtype^\ast, \\ + \CEXNS & \exntype^\ast \\ \CGLOBALS & \globaltype^\ast ~\} \end{array} \end{array} @@ -554,6 +577,67 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera } +.. index:: exception address, exception type, function type, value type, exception tag + +:math:`\REFEXNADDR~\exnaddr~\val^\ast` +...................................... + +* The :ref:`external exception value ` :math:`\EVEXN~\exnaddr` must be :ref:`valid ` with :ref:`external exception type ` :math:`\ETEXN~[t^\ast]\to[]`. + +* Each :ref:`value ` :math:`\val_i` in :math:`\val^\ast` must be :ref:`valid ` with :ref:`value type ` :math:`t_i` in :math:`t^\ast`. + +* Then the instruction is valid with type :math:`[] \to [\EXNREF]`. + +.. math:: + \frac{ + S \vdashexternval \EVEXN~\exnaddr : \ETEXN~[t^\ast]\to[] + \qquad + (S \vdashval \val : t)^\ast + }{ + S; C \vdashadmininstr \REFEXNADDR~\exnaddr~\val^\ast : [] \to [\EXNREF] + } + + +.. index:: throw, throw context, exception address, exception tag + +:math:`\THROWADDR~\exnaddr` +........................... + +* The :ref:`external exception value ` :math:`\EVEXN~\exnaddr` must be :ref:`valid ` with :ref:`external exception type ` :math:`\ETEXN~[t^\ast]\to[]`. + +* Then the instruction is valid with type :math:`[t_1^\ast t^\ast] -> [t_2^\ast]` for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. + +.. math:: + \frac{ + S \vdashexternval \EVEXN~\exnaddr : \ETEXN~[t^\ast]\to[] + }{ + S; C \vdashadmininstr \THROWADDR~\exnaddr : [t_1^\ast t^\ast] \to [t_2^\ast] + } + +.. index:: catch, throw context + +:math:`\CATCH_n\{ \instr_0^\ast \} \instr^\ast \END` +.................................................... + +* The instruction sequence :math:`\instr_0^\ast` must be :ref:`valid ` with a type of the form :math:`[\EXNREF] \to [t^n]`. + +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t^n]` prepended to the |CLABELS| vector. + +* Under context :math:`C'`, + the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^n]`. + +* Then the compound instruction is valid with type :math:`[] \to [t^n]`. + +.. math:: + \frac{ + S; C \vdashinstrseq \instr_0^\ast : [\EXNREF] \to [t^n] + \qquad + S; C,\CLABELS\,[t^n] \vdashinstrseq \instr^\ast : [] \to [t^n] + }{ + S; C \vdashadmininstr \CATCH_n\{\instr_0^\ast\}~\instr^\ast~\END : [] \to [t^n] + } + + .. index:: function address, extern value, extern type, function type :math:`\INVOKE~\funcaddr` @@ -644,6 +728,8 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S' * The length of :math:`S.\SMEMS` must not shrink. +* The length of :math:`S.\SEXNS` must not shrink. + * The length of :math:`S.\SGLOBALS` must not shrink. * The length of :math:`S.\SELEMS` must not shrink. @@ -656,6 +742,8 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S' * For each :ref:`memory instance ` :math:`\meminst_i` in the original :math:`S.\SMEMS`, the new memory instance must be an :ref:`extension ` of the old. +* For each :ref:`exception instance ` :math:`\exninst_i` in the original :math:`S.\SEXNS`, the new exception instance must be an :ref:`extension ` of the old. + * For each :ref:`global instance ` :math:`\globalinst_i` in the original :math:`S.\SGLOBALS`, the new global instance must be an :ref:`extension ` of the old. * For each :ref:`element instance ` :math:`\eleminst_i` in the original :math:`S.\SELEMS`, the new global instance must be an :ref:`extension ` of the old. @@ -674,6 +762,9 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S' S_1.\SMEMS = \meminst_1^\ast & S_2.\SMEMS = {\meminst'_1}^\ast~\meminst_2^\ast & (\vdashmeminstextends \meminst_1 \extendsto \meminst'_1)^\ast \\ + S_1.\SEXNS = \exninst_1^\ast & + S_2.\SEXNS = {\exninst'_1}^\ast~\exninst_2^\ast & + (\vdashexninstextends \exninst_1 \extendsto \exninst'_1)^\ast \\ S_1.\SGLOBALS = \globalinst_1^\ast & S_2.\SGLOBALS = {\globalinst'_1}^\ast~\globalinst_2^\ast & (\vdashglobalinstextends \globalinst_1 \extendsto \globalinst'_1)^\ast \\ @@ -740,6 +831,21 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S' } +.. index:: exception instance +.. _extend-exninst: + +:ref:`Exception Instance ` :math:`\exninst` +........................................................... + +* An exception instance must remain unchanged. + +.. math:: + \frac{ + }{ + \vdashexninstextends \exninst \extendsto \exninst + } + + .. index:: global instance, value, mutability .. _extend-globalinst: diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 23ee4889..89843124 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -13,7 +13,7 @@ The only exception are :ref:`structured control instructions ` have varying encodings. For structured instructions, the instruction sequences forming nested blocks are terminated with explicit opcodes for |END| and |ELSE|. +:ref:`Control instructions ` have varying encodings. For structured instructions, the instruction sequences forming nested blocks are terminated with explicit opcodes for |END|, |ELSE|, and |CATCH|. :ref:`Block types ` are encoded in special compressed form, by either the byte :math:`\hex{40}` indicating the empty type, as a single :ref:`value type `, or as a :ref:`type index ` encoded as a positive :ref:`signed integer `. @@ -31,6 +31,10 @@ Control Instructions .. _binary-block: .. _binary-loop: .. _binary-if: +.. _binary-try: +.. _binary-throw: +.. _binary-rethrow: +.. _binary-br_on_exn: .. _binary-br: .. _binary-br_if: .. _binary-br_table: @@ -56,6 +60,12 @@ Control Instructions \hex{04}~~\X{bt}{:}\Bblocktype~~(\X{in}_1{:}\Binstr)^\ast~~ \hex{05}~~(\X{in}_2{:}\Binstr)^\ast~~\hex{0B} &\Rightarrow& \IF~\X{bt}~\X{in}_1^\ast~\ELSE~\X{in}_2^\ast~\END \\ &&|& + \hex{06}~~\X{bt}{:}\Bblocktype~~(\X{in}_1{:}\Binstr)^\ast~~ + \hex{07}~~(\X{in}_2{:}\Binstr)^\ast~~\hex{0B} + &\Rightarrow& \TRY~\X{bt}~\X{in}_1^\ast~\CATCH~\X{in}_2^\ast~\END \\ &&|& + \hex{08}~~x{:}\Bexnidx &\Rightarrow& \THROW~x \\ &&|& + \hex{09} &\Rightarrow& \RETHROW \\ &&|& + \hex{0A}~~l{:}\Blabelidx~~x{:}\Bexnidx &\Rightarrow& \BRONEXN~l~x \\ &&|& \hex{0C}~~l{:}\Blabelidx &\Rightarrow& \BR~l \\ &&|& \hex{0D}~~l{:}\Blabelidx &\Rightarrow& \BRIF~l \\ &&|& \hex{0E}~~l^\ast{:}\Bvec(\Blabelidx)~~l_N{:}\Blabelidx diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst index 8ff6e9d8..2928860f 100644 --- a/document/core/binary/modules.rst +++ b/document/core/binary/modules.rst @@ -9,11 +9,12 @@ except that :ref:`function definitions ` are split into two section This separation enables *parallel* and *streaming* compilation of the functions in a module. -.. index:: index, type index, function index, table index, memory index, global index, element index, data index, local index, label index +.. index:: index, type index, function index, table index, memory index, exception index, global index, element index, data index, local index, label index pair: binary format; type index pair: binary format; function index pair: binary format; table index pair: binary format; memory index + pair: binary format; exception index pair: binary format; global index pair: binary format; element index pair: binary format; data index @@ -23,6 +24,7 @@ except that :ref:`function definitions ` are split into two section .. _binary-funcidx: .. _binary-tableidx: .. _binary-memidx: +.. _binary-exnidx: .. _binary-globalidx: .. _binary-elemidx: .. _binary-dataidx: @@ -41,6 +43,7 @@ All :ref:`indices ` are encoded with their respective value. \production{function index} & \Bfuncidx &::=& x{:}\Bu32 &\Rightarrow& x \\ \production{table index} & \Btableidx &::=& x{:}\Bu32 &\Rightarrow& x \\ \production{memory index} & \Bmemidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{exception index} & \Bexnidx &::=& x{:}\Bu32 &\Rightarrow& x \\ \production{global index} & \Bglobalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ \production{element index} & \Belemidx &::=& x{:}\Bu32 &\Rightarrow& x \\ \production{data index} & \Bdataidx &::=& x{:}\Bu32 &\Rightarrow& x \\ @@ -100,6 +103,7 @@ Id Section 10 :ref:`code section ` 11 :ref:`data section ` 12 :ref:`data count section ` +13 :ref:`exception section ` == =============================================== @@ -146,7 +150,7 @@ It decodes into a vector of :ref:`function types ` that represe \end{array} -.. index:: ! import section, import, name, function type, table type, memory type, global type +.. index:: ! import section, import, name, function type, table type, memory type, global type, exception type pair: binary format; import pair: section; import .. _binary-import: @@ -170,7 +174,8 @@ It decodes into a vector of :ref:`imports ` that represent the |M \hex{00}~~x{:}\Btypeidx &\Rightarrow& \IDFUNC~x \\ &&|& \hex{01}~~\X{tt}{:}\Btabletype &\Rightarrow& \IDTABLE~\X{tt} \\ &&|& \hex{02}~~\X{mt}{:}\Bmemtype &\Rightarrow& \IDMEM~\X{mt} \\ &&|& - \hex{03}~~\X{gt}{:}\Bglobaltype &\Rightarrow& \IDGLOBAL~\X{gt} \\ + \hex{03}~~\X{gt}{:}\Bglobaltype &\Rightarrow& \IDGLOBAL~\X{gt} \\ &&|& + \hex{04}~~\X{et}{:}\Bexn &\Rightarrow& \IDEXN~\X{et} \\ \end{array} @@ -257,7 +262,7 @@ It decodes into a vector of :ref:`globals ` that represent the |M \end{array} -.. index:: ! export section, export, name, index, function index, table index, memory index, global index +.. index:: ! export section, export, name, index, function index, table index, memory index, exception index, global index pair: binary format; export pair: section; export .. _binary-export: @@ -281,7 +286,8 @@ It decodes into a vector of :ref:`exports ` that represent the |M \hex{00}~~x{:}\Bfuncidx &\Rightarrow& \EDFUNC~x \\ &&|& \hex{01}~~x{:}\Btableidx &\Rightarrow& \EDTABLE~x \\ &&|& \hex{02}~~x{:}\Bmemidx &\Rightarrow& \EDMEM~x \\ &&|& - \hex{03}~~x{:}\Bglobalidx &\Rightarrow& \EDGLOBAL~x \\ + \hex{03}~~x{:}\Bglobalidx &\Rightarrow& \EDGLOBAL~x \\ &&|& + \hex{04}~~x{:}\Bexnidx &\Rightarrow& \EDEXN~x \\ \end{array} @@ -328,21 +334,21 @@ It decodes into a vector of :ref:`element segments ` that represent \X{seg}^\ast{:}\Bsection_9(\Bvec(\Belem)) &\Rightarrow& \X{seg} \\ \production{element segment} & \Belem &::=& \hex{00}~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx) - &\Rightarrow& \{ \ETYPE~\FUNCREF, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|& + &\Rightarrow& \{ \EELEMTYPE~\FUNCREF, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|& \hex{01}~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx) - &\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EPASSIVE \} \\ &&|& + &\Rightarrow& \{ \EELEMTYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EPASSIVE \} \\ &&|& \hex{02}~~x{:}\Btableidx~~e{:}\Bexpr~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx) - &\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|& + &\Rightarrow& \{ \EELEMTYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|& \hex{03}~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx) - &\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EDECLARATIVE \} \\ &&|& + &\Rightarrow& \{ \EELEMTYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EDECLARATIVE \} \\ &&|& \hex{04}~~e{:}\Bexpr~~\X{el}^\ast{:}\Bvec(\Bexpr) - &\Rightarrow& \{ \ETYPE~\FUNCREF, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|& + &\Rightarrow& \{ \EELEMTYPE~\FUNCREF, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|& \hex{05}~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr) - &\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EPASSIVE \} \\ &&|& + &\Rightarrow& \{ \EELEMTYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EPASSIVE \} \\ &&|& \hex{06}~~x{:}\Btableidx~~e{:}\Bexpr~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr) - &\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|& + &\Rightarrow& \{ \EELEMTYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|& \hex{07}~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr) - &\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EDECLARATIVE \} \\ + &\Rightarrow& \{ \EELEMTYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EDECLARATIVE \} \\ \production{element kind} & \Belemkind &::=& \hex{00} &\Rightarrow& \FUNCREF \\ \end{array} @@ -476,7 +482,29 @@ It decodes into an optional :ref:`u32 ` that represents the number instead of deferring validation. -.. index:: module, section, type definition, function type, function, table, memory, global, element, data, start function, import, export, context, version +.. index:: ! exception section, exception, exception type, function type index + pair: binary format; exception + pair: section; exception +.. _binary-exn: +.. _binary-exnsec: + +Exception Section +~~~~~~~~~~~~~~~~~ + +The *exception section* has the id 13. +It decodes into a vector of :ref:`exceptions ` that represent the |MEXNS| +component of a :ref:`module `. + +.. math:: + \begin{array}{llclll} + \production{exception section} & \Bexnsec &::=& + \X{exception}^\ast{:}\Bsection_{13}(\Bvec(\Bexn)) &\Rightarrow& \X{exception}^\ast \\ + \production{exception} & \Bexn &::=& + \hex{00}~~\X{x}{:}\Btypeidx &\Rightarrow& \{ \ETYPE~\X{x} \} \\ + \end{array} + + +.. index:: module, section, type definition, function type, function, table, memory, exception, global, element, data, start function, import, export, context, version pair: binary format; module .. _binary-magic: .. _binary-version: @@ -518,6 +546,8 @@ Furthermore, it must be present if any :math:`data index ` occur \Bcustomsec^\ast \\ &&& \mem^\ast{:\,}\Bmemsec \\ &&& \Bcustomsec^\ast \\ &&& + \exn^\ast{:\,}\Bexnsec \\ &&& + \Bcustomsec^\ast \\ &&& \global^\ast{:\,}\Bglobalsec \\ &&& \Bcustomsec^\ast \\ &&& \export^\ast{:\,}\Bexportsec \\ &&& @@ -538,6 +568,7 @@ Furthermore, it must be present if any :math:`data index ` occur \MFUNCS~\func^n, \\ \MTABLES~\table^\ast, \\ \MMEMS~\mem^\ast, \\ + \MEXNS~\exn^\ast, \\ \MGLOBALS~\global^\ast, \\ \MELEMS~\elem^\ast, \\ \MDATAS~\data^m, \\ diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index 7c462e02..6fd08901 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -42,6 +42,7 @@ Reference Types \begin{array}{llclll@{\qquad\qquad}l} \production{reference type} & \Breftype &::=& \hex{70} &\Rightarrow& \FUNCREF \\ &&|& + \hex{68} &\Rightarrow& \EXNREF \\ &&|& \hex{6F} &\Rightarrow& \EXTERNREF \\ \end{array} @@ -168,3 +169,25 @@ Global Types \hex{00} &\Rightarrow& \MCONST \\ &&|& \hex{01} &\Rightarrow& \MVAR \\ \end{array} + + +.. index:: exception type, function type + pair: binary format; exception type +.. _binary-exntype: + +Exception Types +~~~~~~~~~~~~~~~ + +:ref:`Exception types ` are encoded by their function type. + +.. math:: + \begin{array}{llclll} + \production{exception type} & \Bexntype &::=& + \hex{00}~~ft{:}\Bfunctype &\Rightarrow& ft \\ + \end{array} + +The |Bfunctype| of an exception must have an empty result. + +.. note:: + In future versions of WebAssembly, + the preceding zero byte may encode additional flags. diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 20822a28..a123f9ce 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1615,6 +1615,121 @@ Control Instructions \end{array} +.. _exec-try: + +:math:`\TRY~\blocktype~\instr_1^\ast~\CATCH~\instr_2^\ast~\END` +............................................................... + +1. Assert: due to :ref:`validation `, :math:`\expand_F(\blocktype)` is defined. + +2. Let :math:`[t_1^n] \to [t_2^m]` be the :ref:`function type ` :math:`\expand_F(\blocktype)`. + +3. Assert: due to :ref:`validation `, there are at least :math:`n` values on the top of the stack. + +4. Pop the values :math:`\val^n` from the stack. + +5. Let :math:`L` be the label whose arity is :math:`m` and whose continuation is the end of the |TRY| instruction. + +6. Let :math:`H` be the exception handler whose arity is :math:`m` and whose continuation is the beginning of :math:`\instr_2^\ast`. + +7. :ref:`Enter ` the exception handler `H`. + +8. :ref:`Enter ` the block :math:`\val^n~\instr_1^\ast` with label :math:`L`. + +.. math:: + ~\\[-1ex] + \begin{array}{lcl@{\qquad}} + F; \val^n~(\TRY~\X{bt}~\instr_1^\ast~\CATCH~\instr_2^\ast~\END &\stepto& + \CATCHN_m\{\instr_2\}~(\LABEL_m \{\}~\val^n~\instr_1^\ast~\END)~\END \\ + \hspace{5ex}(\iff \expand_F(\X{bt}) = [t_1^n] \to [t_2^m]) &&\\ + \end{array} + + +.. _exec-throw: + +:math:`\THROW~x` +................ + +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIEXNS[x]` exists. + +3. Let :math:`a` be the :ref:`exception address ` :math:`F.\AMODULE.\MIEXNS[x]`. + +4. :ref:`Throw ` an exception with :ref:`exception address ` :math:`a`. + +.. math:: + ~\\[-1ex] + \begin{array}{lclr@{\qquad}l} + \THROW~x &\stepto& \THROWADDR~a & (\iff F.\AMODULE.\MIEXNS[x] = a) \\ + \end{array} + + +.. _exec-rethrow: + +:math:`\RETHROW` +................ + +1. Assert: due to :ref:`validation `, there is a value with :ref:`reference type ` :math:`\EXNREF` on top of the stack. + +2. Pop the :math:`\EXNREF` value from the stack. + +3. If the :math:`\EXNREF` value is :math:`\REFNULL~\EXNREF` then: + + a. Trap. + +4. Assert: :math:`\EXNREF` is of the form :math:`(\REFEXNADDR~a~\val^\ast)`. + +5. Put the values :math:`\val^\ast` on the stack. + +6. :ref:`Throw ` an exception with :ref:`exception address ` :math:`a`. + +.. math:: + ~\\[-1ex] + \begin{array}{lclr@{\qquad}} + (\REFNULL~\EXNREF)~\RETHROW &\stepto& \TRAP \\ + (\REFEXNADDR~a~\val^\ast)~\RETHROW &\stepto& \val^\ast~(\THROWADDR~a) \\ + \end{array} + + +.. _exec-br_on_exn: + +:math:`\BRONEXN~l~x` +.................... + +1. Assert: due to :ref:`validation `, there is a value with :ref:`reference type ` :math:`\EXNREF` on top of the stack. + +2. Pop the :math:`\EXNREF` value from the stack. + +3. If the :math:`\EXNREF` value is :math:`\REFNULL~\EXNREF` then: + + a. Trap. + +4. Assert: :math:`\EXNREF` is of the form :math:`(\REFEXNADDR~a~\val^\ast)`. + +5. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIEXNS[x]` exists. + +7. If :math:`F.\AMODULE.\MIEXNS[x]=a`, then: + + a. Put the values :math:`\val^\ast` on the stack. + + b. :ref:`Execute ` the instruction :math:`(\BR~l)`. + +8. Else: + + a. Put the value :math:`(\REFEXNADDR~a~\val^\ast)` back on the stack. + +.. math:: + ~\\[-1ex] + \begin{array}{lclr@{\qquad}l} + F; (\REFNULL~\EXNREF)~\BRONEXN~l~x &\stepto& F; \TRAP \\ + F; (\REFEXNADDR~a~\val^\ast)~\BRONEXN~l~x &\stepto& F; \val^\ast~(\BR~l) & (\iff F.\AMODULE.\MIEXNS[x] = a) \\ + F; (\REFEXNADDR~a~\val^\ast)~\BRONEXN~l~x &\stepto& F; (\REFEXNADDR~a~\val^\ast) & (\iff F.\AMODULE.\MIEXNS[x] \neq a) \\ + \end{array} + + .. _exec-br: :math:`\BR~l` @@ -1860,7 +1975,7 @@ Entering :math:`\instr^\ast` with label :math:`L` Exiting :math:`\instr^\ast` with label :math:`L` ................................................ -When the end of a block is reached without a jump or trap aborting it, then the following steps are performed. +When the end of a block is reached without a jump, exception, or trap aborting it, then the following steps are performed. 1. Let :math:`m` be the number of values on the top of the stack. @@ -1885,6 +2000,102 @@ When the end of a block is reached without a jump or trap aborting it, then the Therefore, execution of a loop falls off the end, unless a backwards branch is performed explicitly. +.. index:: exception handling, throw context + pair: handling; exception + +.. _exec-catch: + +Exception Handling +~~~~~~~~~~~~~~~~~~ + +The following auxiliary rules define the semantics of entering and exiting exception handlers through :ref:`try ` instructions and handling thrown exceptions. + +.. _exec-handler-enter: + +Entering an exception handler :math:`H` +....................................... + +1. Push :math:`H` onto the stack. + +.. note:: + No formal reduction rule is needed for installing an exception handler + because it is an :ref:`administrative instruction ` + that the :ref:`try ` instruction reduced to directly. + +.. _exec-handler-exit: + +Exiting an exception handler +............................ + +When the end of a :ref:`try ` instruction is reached without a jump, exception, or trap, then the following steps are performed. + +1. Let :math:`m` be the number of values on the top of the stack. + +2. Pop the values :math:`\val^m` from the stack. + +3. Assert: due to :ref:`validation `, the handler :math:`H` is now on the top of the stack. + +4. Pop the handler from the stack. + +5. Push :math:`\val^m` back to the stack. + +6. Jump to the position after the |END| of the originating |TRY| instruction associated with the handler :math:`H`. + +.. math:: + ~\\[-1ex] + \begin{array}{lcl@{\qquad}l} + \CATCHN_m\{instr^\ast\}~\val^m~\END &\stepto& \val^m + \end{array} + + +.. _exec-throwaddr: + +Throwing an exception with :ref:`exception address ` :math:`a` +.............................................................................. + +When a throw or a rethrow occurs, labels and call frames are popped if necessary, +until an exception handler is found on the top of the stack. + +1. Assert: due to validation, :math:`S.\SEXNS[a]` exists. + +2. Let :math:`[t^n] \to [t'^m]` be the :ref:`exception type ` :math:`S.\SEXNS[a].\EITYPE`. + +3. Assert: due to :ref:`validation `, there are :math:`n` values on the top of the stack. + +4. Pop the :math:`n` values :math:`\val^n` from the stack. + +5. While the stack is not empty and the top of the stack is not an exception handler, do: + + a. Pop the top element from the stack. + +6. Assert: The stack is now either empty or there is an exception handler on the top. + + +7. If there is an exception handler :math:`\CATCHN_m\{\instr^\ast\}` on the top of the stack, then: + + a. Pop the exception handler from the stack. + + b. Let :math:`L` be the label whose arity is :math:`m` and whose continuation is the end of the |TRY| instruction associated with the handler. + + c. Push the label :math:`L` on the stack. + + d. Enter the block :math:`\instr^\ast` with label :math:`L`. + + e. Push the :ref:`exception reference ` :math:`(\REFEXNADDR~a~\val^n)` to the stack. +8. Else the stack is empty. + +9. *TODO: return TBA administrative instruction for the unresolved throw.* + + +.. math:: + \begin{array}{rcl} + S;~F;~\CATCHN_m\{\instr^\ast\}~\XT[\val^n~(\THROWADDR~a)]~\END &\stepto& + S;~F;~\LABEL_m\{\}~(\REFEXNADDR~a~\val^n)~{\instr}^\ast~\END \\ + && \hspace{-12ex} (\iff S.\SEXNS[a]=\{\ETYPE~[t^n]\to[]\}) \\ + % S;\val^n~(\THROWADDR~a) & \stepto & TBA \\ + \end{array} + + .. index:: ! call, function, function instance, label, frame Function Calls @@ -1945,7 +2156,7 @@ Invocation of :ref:`function address ` :math:`a` Returning from a function ......................... -When the end of a function is reached without a jump (i.e., |RETURN|) or trap aborting it, then the following steps are performed. +When the end of a function is reached without a jump (i.e., |RETURN|), exception, or trap aborting it, then the following steps are performed. 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 35df503d..d45a3e85 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -68,6 +68,26 @@ The following auxiliary typing rules specify this typing relation relative to a } +.. index:: exception type, exception address, exception tag, function type +.. _valid-externval-exn: + +:math:`\EVEXN~a` +................ + +* The store entry :math:`S.\SEXNS[a]` must exist. + +* Let :math:`\exntype` be the function type :math:`S.\SEXNS[a].\EITYPE`. + +* Then :math:`\EVEXN~a` is valid with :ref:`external type ` :math:`\ETEXN~\exntype`. + +.. math:: + \frac{ + }{ + S \vdashexternval \EVEXN~a : \ETEXN~(S.\SEXNS[a].\EITYPE) + } + + + .. index:: global type, global address, value type, mutability .. _valid-externval-global: @@ -149,13 +169,32 @@ The following auxiliary typing rules specify this typing relation relative to a } +:ref:`Exception References ` :math:`\REFEXNADDR~a~\val^n` +............................................................................ + +* The external value :math:`\EVEXN~a` must be valid with :ref:`exception type ` :math:`[t^n]\to[]`. + +* Each value :math:`val_i` in :math:`\val^n` must have type :math:`t_i` in :math:`t^n`. + +* The value is valid with :ref:`reference type ` :math:`\EXNREF`. + +.. math:: + \frac{ + S \vdashexternval \EVEXN~a : [t^n]\to[] + \qquad + (S \vdashval \val : t)^n + }{ + S \vdashval \REFEXNADDR~a~\val^n : \EXNREF + } + + .. index:: ! allocation, store, address .. _alloc: Allocation ~~~~~~~~~~ -New instances of :ref:`functions `, :ref:`tables `, :ref:`memories `, and :ref:`globals ` are *allocated* in a :ref:`store ` :math:`S`, as defined by the following auxiliary functions. +New instances of :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`exceptions `, and :ref:`globals ` are *allocated* in a :ref:`store ` :math:`S`, as defined by the following auxiliary functions. .. index:: function, function instance, function address, module instance, function type @@ -277,6 +316,32 @@ New instances of :ref:`functions `, :ref:`tables ` +.................................. + +1. Let :math:`\exntype` be the :ref:`exception type ` to allocate. + +2. Let :math:`a` be the first free :ref:`exception address ` in :math:`S`. + +3. Let :math:`\exninst` be the :ref:`exception instance ` :math:`\{ \EITYPE~\exntype \}`. + +4. Append :math:`\exninst` to the |SEXNS| of :math:`S`. + +5. Return :math:`a`. + +.. math:: + \begin{array}{rlll} + \allocexn(S, \exntype) &=& S', \exnaddr \\[1ex] + \mbox{where:} \hfill \\ + \exnaddr &=& |S.\SEXNS| \\ + \exninst &=& \{ \EITYPE~\exntype \} \\ + S' &=& S \compose \{\SEXNS~\exninst\} \\ + \end{array} + + .. index:: global, global instance, global address, global type, value type, mutability, value .. _alloc-global: @@ -313,7 +378,7 @@ New instances of :ref:`functions `, :ref:`tables ` in :math:`S`. -3. Let :math:`\eleminst` be the :ref:`element instance ` :math:`\{ \EITYPE~t, \EIELEM~\reff^\ast \}`. +3. Let :math:`\eleminst` be the :ref:`element instance ` :math:`\{ \EIELEMTYPE~t, \EIELEM~\reff^\ast \}`. 4. Append :math:`\eleminst` to the |SELEMS| of :math:`S`. @@ -324,7 +389,7 @@ New instances of :ref:`functions `, :ref:`tables ` \end{array} -.. index:: module, module instance, function instance, table instance, memory instance, global instance, export instance, function address, table address, memory address, global address, function index, table index, memory index, global index, type, function, table, memory, global, import, export, external value, external type, matching +.. index:: module, module instance, function instance, table instance, memory instance, exception instance, global instance, export instance, function address, table address, memory address, exception address, global address, function index, table index, memory index, exception index, global index, type, function, table, memory, exception, global, import, export, external value, external type, matching .. _alloc-module: :ref:`Modules ` @@ -456,39 +521,49 @@ and list of :ref:`reference ` vectors for the module's :ref:`element a. Let :math:`\memaddr_i` be the :ref:`memory address ` resulting from :ref:`allocating ` :math:`\mem_i.\MTYPE`. -5. For each :ref:`global ` :math:`\global_i` in :math:`\module.\MGLOBALS`, do: +5. For each :ref:`exception ` :math:`\exn_i` in :math:`\module.\MEXNS`, do: + + a. Let :math:`\exntype` be the :ref:`exception type ` :math:`\module.\MTYPES[\exn_i.ETYPE]`. + + b. Let :math:`\exnaddr_i` be the :ref:`exception address ` resulting from :ref:`allocating ` :math:`\exntype`. + +6. For each :ref:`global ` :math:`\global_i` in :math:`\module.\MGLOBALS`, do: a. Let :math:`\globaladdr_i` be the :ref:`global address ` resulting from :ref:`allocating ` :math:`\global_i.\GTYPE` with initializer value :math:`\val^\ast[i]`. -6. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS`, do: +7. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS`, do: - a. Let :math:`\elemaddr_i` be the :ref:`element address ` resulting from :ref:`allocating ` a :ref:`element instance ` of :ref:`reference type ` :math:`\elem_i.\ETYPE` with contents :math:`(\reff^\ast)^\ast[i]`. + a. Let :math:`\elemaddr_i` be the :ref:`element address ` resulting from :ref:`allocating ` a :ref:`element instance ` of :ref:`reference type ` :math:`\elem_i.\EELEMTYPE` with contents :math:`(\reff^\ast)^\ast[i]`. -7. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATAS`, do: +8. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATAS`, do: a. Let :math:`\dataaddr_i` be the :ref:`data address ` resulting from :ref:`allocating ` a :ref:`data instance ` with contents :math:`\data_i.\DINIT`. -8. Let :math:`\funcaddr^\ast` be the the concatenation of the :ref:`function addresses ` :math:`\funcaddr_i` in index order. +9. Let :math:`\funcaddr^\ast` be the concatenation of the :ref:`function addresses ` :math:`\funcaddr_i` in index order. + +10. Let :math:`\tableaddr^\ast` be the concatenation of the :ref:`table addresses ` :math:`\tableaddr_i` in index order. -9. Let :math:`\tableaddr^\ast` be the the concatenation of the :ref:`table addresses ` :math:`\tableaddr_i` in index order. +11. Let :math:`\memaddr^\ast` be the concatenation of the :ref:`memory addresses ` :math:`\memaddr_i` in index order. -10. Let :math:`\memaddr^\ast` be the the concatenation of the :ref:`memory addresses ` :math:`\memaddr_i` in index order. +12. Let :math:`\exnaddr^\ast` be the concatenation of the :ref:`exception addresses ` :math:`\exnaddr_i` in index order. -11. Let :math:`\globaladdr^\ast` be the the concatenation of the :ref:`global addresses ` :math:`\globaladdr_i` in index order. +13. Let :math:`\globaladdr^\ast` be the concatenation of the :ref:`global addresses ` :math:`\globaladdr_i` in index order. -12. Let :math:`\elemaddr^\ast` be the the concatenation of the :ref:`element addresses ` :math:`\elemaddr_i` in index order. +14. Let :math:`\elemaddr^\ast` be the concatenation of the :ref:`element addresses ` :math:`\elemaddr_i` in index order. -13. Let :math:`\dataaddr^\ast` be the the concatenation of the :ref:`data addresses ` :math:`\dataaddr_i` in index order. +15. Let :math:`\dataaddr^\ast` be the concatenation of the :ref:`data addresses ` :math:`\dataaddr_i` in index order. -14. Let :math:`\funcaddr_{\F{mod}}^\ast` be the list of :ref:`function addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\funcaddr^\ast`. +16. Let :math:`\funcaddr_{\F{mod}}^\ast` be the list of :ref:`function addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\funcaddr^\ast`. -15. Let :math:`\tableaddr_{\F{mod}}^\ast` be the list of :ref:`table addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\tableaddr^\ast`. +17. Let :math:`\tableaddr_{\F{mod}}^\ast` be the list of :ref:`table addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\tableaddr^\ast`. -16. Let :math:`\memaddr_{\F{mod}}^\ast` be the list of :ref:`memory addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\memaddr^\ast`. +18. Let :math:`\memaddr_{\F{mod}}^\ast` be the list of :ref:`memory addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\memaddr^\ast`. -17. Let :math:`\globaladdr_{\F{mod}}^\ast` be the list of :ref:`global addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\globaladdr^\ast`. +19. Let :math:`\exnaddr_{\F{mod}}^\ast` be the list of :ref:`exception addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\exnaddr^\ast`. -18. For each :ref:`export ` :math:`\export_i` in :math:`\module.\MEXPORTS`, do: +20. Let :math:`\globaladdr_{\F{mod}}^\ast` be the list of :ref:`global addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\globaladdr^\ast`. + +21. For each :ref:`export ` :math:`\export_i` in :math:`\module.\MEXPORTS`, do: a. If :math:`\export_i` is a function export for :ref:`function index ` :math:`x`, then let :math:`\externval_i` be the :ref:`external value ` :math:`\EVFUNC~(\funcaddr_{\F{mod}}^\ast[x])`. @@ -496,15 +571,17 @@ and list of :ref:`reference ` vectors for the module's :ref:`element c. Else, if :math:`\export_i` is a memory export for :ref:`memory index ` :math:`x`, then let :math:`\externval_i` be the :ref:`external value ` :math:`\EVMEM~(\memaddr_{\F{mod}}^\ast[x])`. - d. Else, if :math:`\export_i` is a global export for :ref:`global index ` :math:`x`, then let :math:`\externval_i` be the :ref:`external value ` :math:`\EVGLOBAL~(\globaladdr_{\F{mod}}^\ast[x])`. + d. Else, if :math:`\export_i` is an exception export for :ref:`exception index ` :math:`x`, then let :math:`\externval_i` be the :ref:`external value ` :math:`\EVEXN~(\exnaddr_{\F{mod}}^\ast[x])`. + + e. Else, if :math:`\export_i` is a global export for :ref:`global index ` :math:`x`, then let :math:`\externval_i` be the :ref:`external value ` :math:`\EVGLOBAL~(\globaladdr_{\F{mod}}^\ast[x])`. - e. Let :math:`\exportinst_i` be the :ref:`export instance ` :math:`\{\EINAME~(\export_i.\ENAME), \EIVALUE~\externval_i\}`. + f. Let :math:`\exportinst_i` be the :ref:`export instance ` :math:`\{\EINAME~(\export_i.\ENAME), \EIVALUE~\externval_i\}`. -19. Let :math:`\exportinst^\ast` be the the concatenation of the :ref:`export instances ` :math:`\exportinst_i` in index order. +22. Let :math:`\exportinst^\ast` be the the concatenation of the :ref:`export instances ` :math:`\exportinst_i` in index order. -20. Let :math:`\moduleinst` be the :ref:`module instance ` :math:`\{\MITYPES~(\module.\MTYPES),` :math:`\MIFUNCS~\funcaddr_{\F{mod}}^\ast,` :math:`\MITABLES~\tableaddr_{\F{mod}}^\ast,` :math:`\MIMEMS~\memaddr_{\F{mod}}^\ast,` :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIEXPORTS~\exportinst^\ast\}`. +23. Let :math:`\moduleinst` be the :ref:`module instance ` :math:`\{\MITYPES~(\module.\MTYPES),` :math:`\MIFUNCS~\funcaddr_{\F{mod}}^\ast,` :math:`\MITABLES~\tableaddr_{\F{mod}}^\ast,` :math:`\MIMEMS~\memaddr_{\F{mod}}^\ast,` :math:`\MIEXNS~\exnaddr_{\F{mod}}^\ast`, :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIEXPORTS~\exportinst^\ast\}`. -21. Return :math:`\moduleinst`. +24. Return :math:`\moduleinst`. .. math:: @@ -523,6 +600,7 @@ where: \MIFUNCS~\evfuncs(\externval_{\F{im}}^\ast)~\funcaddr^\ast, \\ \MITABLES~\evtables(\externval_{\F{im}}^\ast)~\tableaddr^\ast, \\ \MIMEMS~\evmems(\externval_{\F{im}}^\ast)~\memaddr^\ast, \\ + \MIEXNS~\evexns(\externval_{\F{im}}^\ast)~\exnaddr^\ast, \\ \MIGLOBALS~\evglobals(\externval_{\F{im}}^\ast)~\globaladdr^\ast, \\ \MIELEMS~\elemaddr^\ast, \\ \MIDATAS~\dataaddr^\ast, \\ @@ -534,11 +612,13 @@ where: \qquad\qquad\qquad~~ \wedge (\table.\TTYPE)^\ast = (\limits~t)^\ast) \\ S_3, \memaddr^\ast &=& \allocmem^\ast(S_2, (\mem.\MTYPE)^\ast) \qquad\qquad\qquad~ (\where \mem^\ast = \module.\MMEMS) \\ - S_4, \globaladdr^\ast &=& \allocglobal^\ast(S_3, (\global.\GTYPE)^\ast, \val^\ast) + S_4, \exnaddr^\ast &=& \allocexn^\ast(S_3, \exn^\ast, \module) + \qquad\quad~ (\where \exn^\ast = \module.\MEXNS) \\ + S_5, \globaladdr^\ast &=& \allocglobal^\ast(S_4, (\global.\GTYPE)^\ast, \val^\ast) \qquad\quad~ (\where \global^\ast = \module.\MGLOBALS) \\ - S_5, \elemaddr^\ast &=& \allocelem^\ast(S_4, (\elem.\ETYPE)^\ast, (\reff^\ast)^\ast) \\ + S_6, \elemaddr^\ast &=& \allocelem^\ast(S_5, (\elem.\EELEMTYPE)^\ast, (\reff^\ast)^\ast) \\ \qquad\quad~ (\where \elem^\ast = \module.\MELEMS) \\ - S', \dataaddr^\ast &=& \allocdata^\ast(S_5, (\data.\DINIT)^\ast) + S', \dataaddr^\ast &=& \allocdata^\ast(S_6, (\data.\DINIT)^\ast) \qquad\qquad\qquad~ (\where \data^\ast = \module.\MDATAS) \\ \exportinst^\ast &=& \{ \EINAME~(\export.\ENAME), \EIVALUE~\externval_{\F{ex}} \}^\ast \quad (\where \export^\ast = \module.\MEXPORTS) \\[1ex] @@ -548,6 +628,8 @@ where: \qquad (\where x^\ast = \edtables(\module.\MEXPORTS)) \\ \evmems(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIMEMS[x])^\ast \qquad (\where x^\ast = \edmems(\module.\MEXPORTS)) \\ + \evexns(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIEXNS[x])^\ast + \qquad\!\!\! (\where x^\ast = \edexns(\module.\MEXPORTS)) \\ \evglobals(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIGLOBALS[x])^\ast \qquad\!\!\! (\where x^\ast = \edglobals(\module.\MEXPORTS)) \\ \end{array} @@ -731,10 +813,10 @@ where: .. math:: \begin{array}{@{}l} - \F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EPASSIVE\}) \quad=\quad \epsilon \\ - \F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EACTIVE \{\ETABLE~0, \EOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad + \F{runelem}_i(\{\EELEMTYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EPASSIVE\}) \quad=\quad \epsilon \\ + \F{runelem}_i(\{\EELEMTYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EACTIVE \{\ETABLE~0, \EOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad \instr^\ast~(\I32.\CONST~0)~(\I32.\CONST~n)~(\TABLEINIT~i)~(\ELEMDROP~i) \\ - \F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EDECLARATIVE\}) \quad=\\ \qquad + \F{runelem}_i(\{\EELEMTYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EDECLARATIVE\}) \quad=\\ \qquad (\ELEMDROP~i) \\[1ex] \F{rundata}_i(\{\DINIT~b^n, DMODE~\DPASSIVE\}) \quad=\quad \epsilon \\ \F{rundata}_i(\{\DINIT~b^n, DMODE~\DACTIVE \{\DMEM~0, \DOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 43c66efe..80735c23 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -7,7 +7,7 @@ Runtime Structure :ref:`Store `, :ref:`stack `, and other *runtime structure* forming the WebAssembly abstract machine, such as :ref:`values ` or :ref:`module instances `, are made precise in terms of additional auxiliary syntax. -.. index:: ! value, number, reference, constant, number type, reference type, ! host address, value type, integer, floating-point, ! default value +.. index:: ! value, number, reference, constant, number type, reference type, ! host address, ! exception address, value type, integer, floating-point, ! default value, embedder pair: abstract syntax; value .. _syntax-num: .. _syntax-ref: @@ -25,6 +25,7 @@ It is convenient to reuse the same notation as for the |CONST| :ref:`instruction References other than null are represented with additional :ref:`administrative instructions `. They either are *function references*, pointing to a specific :ref:`function address `, +*exception references* representing a caught exception pointing to a specific :ref:`exception address ` and carrying a sequence of :ref:`values `, or *external references* pointing to an uninterpreted form of :ref:`extern address ` that can be defined by the :ref:`embedder ` to represent its own objects. .. math:: @@ -37,7 +38,8 @@ or *external references* pointing to an uninterpreted form of :ref:`extern addre \production{(reference)} & \reff &::=& \REFNULL~t \\&&|& \REFFUNCADDR~\funcaddr \\&&|& - \REFEXTERNADDR~\externaddr \\ + \REFEXTERNADDR~\externaddr \\&&|& + \REFEXNADDR~\exnaddr~\val^\ast \\ \production{(value)} & \val &::=& \num ~|~ \reff \\ \end{array} @@ -84,7 +86,7 @@ It is either a sequence of :ref:`values ` or a :ref:`trap `, :ref:`tables `, :ref:`memories `, and :ref:`globals `, :ref:`element segments `, and :ref:`data segments ` that have been :ref:`allocated ` during the life time of the abstract machine. [#gc]_ +It consists of the runtime representation of all *instances* of :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`exceptions `, and :ref:`globals `, :ref:`element segments `, and :ref:`data segments ` that have been :ref:`allocated ` during the life time of the abstract machine. [#gc]_ It is an invariant of the semantics that no element or data instance is :ref:`addressed ` from anywhere else but the owning module instances. @@ -106,6 +108,7 @@ Syntactically, the store is defined as a :ref:`record ` listing \SFUNCS & \funcinst^\ast, \\ \STABLES & \tableinst^\ast, \\ \SMEMS & \meminst^\ast, \\ + \SEXNS & \exninst^\ast, \\ \SGLOBALS & \globalinst^\ast, \\ \SELEMS & \eleminst^\ast, \\ \SDATAS & \datainst^\ast ~\} \\ @@ -124,10 +127,11 @@ Convention * The meta variable :math:`S` ranges over stores where clear from context. -.. index:: ! address, store, function instance, table instance, memory instance, global instance, element instance, data instance, embedder +.. index:: ! address, store, function instance, table instance, memory instance, exception instance, global instance, element instance, data instance, embedder pair: abstract syntax; function address pair: abstract syntax; table address pair: abstract syntax; memory address + pair: abstract syntax; exception address pair: abstract syntax; global address pair: abstract syntax; element address pair: abstract syntax; data address @@ -135,6 +139,7 @@ Convention pair: function; address pair: table; address pair: memory; address + pair: exception; address pair: global; address pair: element; address pair: data; address @@ -142,6 +147,7 @@ Convention .. _syntax-funcaddr: .. _syntax-tableaddr: .. _syntax-memaddr: +.. _syntax-exnaddr: .. _syntax-globaladdr: .. _syntax-elemaddr: .. _syntax-dataaddr: @@ -151,7 +157,7 @@ Convention Addresses ~~~~~~~~~ -:ref:`Function instances `, :ref:`table instances `, :ref:`memory instances `, and :ref:`global instances `, :ref:`element instances `, and :ref:`data instances ` in the :ref:`store ` are referenced with abstract *addresses*. +:ref:`Function instances `, :ref:`table instances `, :ref:`memory instances `, :ref:`exception instances `, :ref:`global instances `, :ref:`element instances `, and :ref:`data instances ` in the :ref:`store ` are referenced with abstract *addresses*. These are simply indices into the respective store component. In addition, an :ref:`embedder ` may supply an uninterpreted set of *host addresses*. @@ -165,6 +171,8 @@ In addition, an :ref:`embedder ` may supply an uninterpreted set of *h \addr \\ \production{(memory address)} & \memaddr &::=& \addr \\ + \production{(exception address)} & \exnaddr &::=& + \addr \\ \production{(global address)} & \globaladdr &::=& \addr \\ \production{(element address)} & \elemaddr &::=& @@ -190,7 +198,7 @@ even where this identity is not observable from within WebAssembly code itself hence logical addresses can be arbitrarily large natural numbers. -.. index:: ! instance, function type, function instance, table instance, memory instance, global instance, element instance, data instance, export instance, table address, memory address, global address, element address, data address, index, name +.. index:: ! instance, function type, function instance, table instance, memory instance, exception instance, global instance, element instance, data instance, export instance, table address, memory address, exception address, global address, element address, data address, index, name pair: abstract syntax; module instance pair: module; instance .. _syntax-moduleinst: @@ -210,6 +218,7 @@ and collects runtime representations of all entities that are imported, defined, \MIFUNCS & \funcaddr^\ast, \\ \MITABLES & \tableaddr^\ast, \\ \MIMEMS & \memaddr^\ast, \\ + \MIEXNS & \exnaddr^\ast, \\ \MIGLOBALS & \globaladdr^\ast, \\ \MIELEMS & \elemaddr^\ast, \\ \MIDATAS & \dataaddr^\ast, \\ @@ -218,7 +227,7 @@ and collects runtime representations of all entities that are imported, defined, \end{array} Each component references runtime instances corresponding to respective declarations from the original module -- whether imported or defined -- in the order of their static :ref:`indices `. -:ref:`Function instances `, :ref:`table instances `, :ref:`memory instances `, and :ref:`global instances ` are referenced with an indirection through their respective :ref:`addresses ` in the :ref:`store `. +:ref:`Function instances `, :ref:`table instances `, :ref:`memory instances `, :ref:`exception instances `, and :ref:`global instances ` are referenced with an indirection through their respective :ref:`addresses ` in the :ref:`store `. It is an invariant of the semantics that all :ref:`export instances ` in a given module instance have different :ref:`names `. @@ -303,6 +312,27 @@ The bytes can be mutated through :ref:`memory instructions It is an invariant of the semantics that the length of the byte vector, divided by page size, never exceeds the maximum size of :math:`\memtype`, if present. +.. index:: ! exception instance, exception, exception tag, exception type + pair: abstract syntax; exception instance + pair: exception; instance +.. _syntax-exninst: + +Exception Instances +~~~~~~~~~~~~~~~~~~~ + +An *exception instance* is the runtime representation of an :ref:`exception ` definition. +It records the :ref:`type ` of the exception. + +.. math:: + \begin{array}{llll} + \production{(exception instance)} & \exninst &::=& + \{ \EITYPE~\exntype \} \\ + \end{array} + +.. note:: + The :ref:`exception address ` of an exception instance is also called an *exception tag*. + + .. index:: ! global instance, global, value, mutability, instruction, embedder pair: abstract syntax; global instance pair: global; instance @@ -339,7 +369,7 @@ It holds a vector of references and their common :ref:`type `. .. math:: \begin{array}{llll} \production{(element instance)} & \eleminst &::=& - \{ \EITYPE~\reftype, \EIELEM~\vec(\reff) \} \\ + \{ \EIELEMTYPE~\reftype, \EIELEM~\vec(\reff) \} \\ \end{array} @@ -379,7 +409,7 @@ It defines the export's :ref:`name ` and the associated :ref:`exter \end{array} -.. index:: ! external value, function address, table address, memory address, global address, store, function, table, memory, global +.. index:: ! external value, function address, table address, memory address, exception address, global address, store, function, table, memory, exception, global pair: abstract syntax; external value pair: external; value .. _syntax-externval: @@ -388,7 +418,7 @@ External Values ~~~~~~~~~~~~~~~ An *external value* is the runtime representation of an entity that can be imported or exported. -It is an :ref:`address ` denoting either a :ref:`function instance `, :ref:`table instance `, :ref:`memory instance `, or :ref:`global instances ` in the shared :ref:`store `. +It is an :ref:`address ` denoting either a :ref:`function instance `, :ref:`table instance `, :ref:`memory instance `, :ref:`global instances `, or :ref:`exception instances ` in the shared :ref:`store `. .. math:: \begin{array}{llcl} @@ -396,6 +426,7 @@ It is an :ref:`address ` denoting either a :ref:`function instance \EVFUNC~\funcaddr \\&&|& \EVTABLE~\tableaddr \\&&|& \EVMEM~\memaddr \\&&|& + \EVEXN~\exnaddr \\&&|& \EVGLOBAL~\globaladdr \\ \end{array} @@ -412,16 +443,22 @@ It filters out entries of a specific kind in an order-preserving fashion: * :math:`\evmems(\externval^\ast) = [\memaddr ~|~ (\EVMEM~\memaddr) \in \externval^\ast]` +* :math:`\evexns(\externval^\ast) = [\exnaddr ~|~ (\EVEXN~\exnaddr) \in \externval^\ast]` + * :math:`\evglobals(\externval^\ast) = [\globaladdr ~|~ (\EVGLOBAL~\globaladdr) \in \externval^\ast]` -.. index:: ! stack, ! frame, ! label, instruction, store, activation, function, call, local, module instance + +.. index:: ! stack, ! frame, ! label, ! handler, instruction, store, activation, function, call, local, module instance, exception handler pair: abstract syntax; frame pair: abstract syntax; label + pair: abstract syntax; handler .. _syntax-frame: .. _syntax-label: +.. _syntax-catch: .. _frame: .. _label: +.. _handler: .. _stack: Stack @@ -436,6 +473,8 @@ The stack contains three kinds of entries: * *Activations*: the *call frames* of active :ref:`function ` calls. +* *Handlers*: active exception handlers. + These entries can occur on the stack in any order during the execution of a program. Stack entries are described by abstract syntax as follows. @@ -493,6 +532,21 @@ and a reference to the function's own :ref:`module instance ` The values of the locals are mutated by respective :ref:`variable instructions `. +Exception handlers +.................. + +Like labels, exception handlers carry the return arity :math:`n` of the +respective |TRY| block, and their associated branch *target*, which is +expressed syntactically as an :ref:`instruction ` sequence: + +.. math:: + \begin{array}{llll} + \production{(handler)} & \X{handler} &::=& + \CATCH_n\{\instr^\ast\}\\ + \end{array} + +Intuitively, :math:`\instr^\ast` is the *continuation* to execute +when the handler catches a thrown exception. Conventions ........... @@ -510,11 +564,14 @@ Conventions \end{array} -.. index:: ! administrative instructions, function, function instance, function address, label, frame, instruction, trap, call, memory, memory instance, table, table instance, element, data, segment +.. index:: ! administrative instructions, function, function instance, function address, label, frame, instruction, trap, call, memory, memory instance, table, table instance, element, data, segment, exception, exception instance, exception address, exception, reftype pair:: abstract syntax; administrative instruction .. _syntax-trap: .. _syntax-reffuncaddr: .. _syntax-invoke: +.. _syntax-refexnaddr: +.. _syntax-throwaddr: +.. _syntax-catchn: .. _syntax-instr-admin: Administrative Instructions @@ -523,7 +580,7 @@ Administrative Instructions .. note:: This section is only relevant for the :ref:`formal notation `. -In order to express the reduction of :ref:`traps `, :ref:`calls `, and :ref:`control instructions `, the syntax of instructions is extended to include the following *administrative instructions*: +In order to express the reduction of :ref:`traps `, :ref:`calls `, :ref:`exception handling `, and :ref:`control instructions `, the syntax of instructions is extended to include the following *administrative instructions*: .. math:: \begin{array}{llcl} @@ -533,19 +590,27 @@ In order to express the reduction of :ref:`traps `, :ref:`calls `. Similarly, |REFEXTERNADDR| represents :ref:`external references `. +The |REFFUNCADDR| instruction represents :ref:`function reference values `. Similarly, |REFEXTERNADDR| represents :ref:`external references `, +and |REFEXNADDR| represents :ref:`exception reference values ` of caught exceptions. The |INVOKE| instruction represents the imminent invocation of a :ref:`function instance `, identified by its :ref:`address `. It unifies the handling of different forms of calls. -The |LABEL| and |FRAME| instructions model :ref:`labels ` and :ref:`frames ` :ref:`"on the stack" `. +The |THROWADDR| instruction represents the imminent throw of an :ref:`exception reference value ` based on an :ref:`exception instance `, identified by its :ref:`address `. +The values it will consume to create the exception depend on its :ref:`exception type `. +It unifies the throwing of different forms of exceptions. + +The |LABEL|, |FRAME|, and |CATCHN| instructions model :ref:`labels `, :ref:`frames `, and active :ref:`exception handlers `, respectively, :ref:`"on the stack" `. Moreover, the administrative syntax maintains the nesting structure of the original :ref:`structured control instruction ` or :ref:`function body ` and their :ref:`instruction sequences ` with an |END| marker. That way, the end of the inner instruction sequence is known when part of an outer sequence. @@ -608,6 +673,53 @@ This definition allows to index active labels surrounding a :ref:`branch ` :math:`l`, which corresponds to the number of surrounding |LABEL| instructions that must be hopped over -- which is exactly the count encoded in the index of a block context. +.. index:: ! throw context, exception, throw address, catch block +.. _syntax-ctxt-throw: + +Throw Contexts +.............. + +In order to specify the reduction of |TRY| blocks +with the help of the administrative instructions |THROWADDR|, |REFEXNADDR|, and |CATCHN|, +the following syntax of *throw contexts* is defined, as well as associated structural rules: + +.. math:: + \begin{array}{llll} + \production{(throw contexts)} & \XT &::=& + \val^\ast~[\_]~\instr^\ast \\ &&|& + \LABEL_n\{\instr^\ast\}~\XT~\END \\ &&|& + \CATCHN_n\{\instr^\ast\}~\XT~\END \\ &&|& + \FRAME_n\{F\}~\XT~\END \\ + \end{array} + +Throw contexts allow matching the program context around a throw instruction up to the nearest enclosing :math:`\CATCHN` handler, thereby selecting the exception handler responsible for an exception. + +.. note:: + For example, catching a simple :ref:`throw ` in a :ref:`try block ` would be as follows. + + .. math:: + \begin{array}{ll} + & \hspace{-5ex} S;~F;~\val^n~(\TRY~\X{bt}~\THROW~x~\CATCH~\RETURN~\END) \\ + \stepto & S;~F;~\CATCHN_1\{\RETURN\}~(\LABEL_1 \{\}~\val^n~\THROWADDR~a~\END)~\END \\ + \end{array} + + :ref:`Handling ` the thrown exception address :math:`a` in the throw context + :math:`T=\LABEL_1 \{\}[\_]~\END`, with the exception handler :math:`\CATCHN_1\{\RETURN\}` gives: + + .. math:: + \begin{array}{lll} + \stepto & S;~F;~\LABEL_1~\{\}~(\REFEXNADDR~a~\val^n)~\RETURN~\END & \hspace{9ex}\ \\ + \stepto & (\REFEXNADDR~a~\val^n) & \\ + \end{array} + + When a throw occurs, execution halts until that throw is the continuation of a throw context in a catching try block. + + In this particular case, the exception reference is returned normally, as opposed to being thrown as the result of a plain + :math:`\THROW~x` without a catching |TRY| block. + + *(TODO: add administrative values to describe unresolved throws).* + + .. index:: ! configuration, ! thread, store, frame, instruction, module instruction .. _syntax-thread: .. _syntax-config: @@ -663,6 +775,8 @@ Finally, the following definition of *evaluation context* and associated structu Reduction terminates when a thread's instruction sequence has been reduced to a :ref:`result `, that is, either a sequence of :ref:`values ` or to a |TRAP|. +*(TODO: add rules to deal with unresolved* :math:`\THROWADDR~\exnaddr`, *and extend results to include such situations.)* + .. note:: The restriction on evaluation contexts rules out contexts like :math:`[\_]` and :math:`\epsilon~[\_]~\epsilon` for which :math:`E[\TRAP] = \TRAP`. diff --git a/document/core/index.rst b/document/core/index.rst index 139a05b0..9d4d71af 100644 --- a/document/core/index.rst +++ b/document/core/index.rst @@ -3,7 +3,7 @@ WebAssembly Specification .. only:: html - | Release |release| + bulk instructions + reference types (Draft, |today|) + | Release |release| + bulk instructions + reference types + exception handling (Draft, |today|) | Editor: Andreas Rossberg diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 85c641f0..d019feea 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -350,7 +350,7 @@ The |DATADROP| instruction prevents further use of a passive data segment. This This restriction may be lifted in future versions. -.. index:: ! control instruction, ! structured control, ! label, ! block, ! block type, ! branch, ! unwinding, result type, label index, function index, type index, vector, trap, function, table, function type, value type, type index +.. index:: ! control instruction, ! structured control, ! label, ! block, ! block type, ! branch, ! unwinding, result type, label index, function index, type index, exception index, vector, trap, function, table, exception, function type, value type, type index, exception index pair: abstract syntax; instruction pair: abstract syntax; block type pair: block; type @@ -360,6 +360,10 @@ The |DATADROP| instruction prevents further use of a passive data segment. This .. _syntax-block: .. _syntax-loop: .. _syntax-if: +.. _syntax-try: +.. _syntax-throw: +.. _syntax-rethrow: +.. _syntax-br_on_exn: .. _syntax-br: .. _syntax-br_if: .. _syntax-br_table: @@ -385,6 +389,10 @@ Instructions in this group affect the flow of control. \BLOCK~\blocktype~\instr^\ast~\END \\&&|& \LOOP~\blocktype~\instr^\ast~\END \\&&|& \IF~\blocktype~\instr^\ast~\ELSE~\instr^\ast~\END \\&&|& + \TRY~\blocktype~instr^\ast~\CATCH~\instr^\ast~\END \\&&|& + \THROW~\exnidx \\&&|& + \RETHROW \\&&|& + \BRONEXN~\labelidx~\exnidx \\&&|& \BR~\labelidx \\&&|& \BRIF~\labelidx \\&&|& \BRTABLE~\vec(\labelidx)~\labelidx \\&&|& @@ -397,10 +405,13 @@ The |NOP| instruction does nothing. The |UNREACHABLE| instruction causes an unconditional :ref:`trap `. -The |BLOCK|, |LOOP| and |IF| instructions are *structured* instructions. -They bracket nested sequences of instructions, called *blocks*, terminated with, or separated by, |END| or |ELSE| pseudo-instructions. +The |BLOCK|, |LOOP|, |IF|, and |TRY| instructions are *structured* instructions. +They bracket nested sequences of instructions, called *blocks*, terminated with, or separated by, either |END|, |ELSE|, or |CATCH| pseudo-instructions. As the grammar prescribes, they must be well-nested. +The instructions |TRY|, |THROW|, |RETHROW|, and |BRONEXN| are concerned with handling exceptions. +The |THROW| and |RETHROW| instructions alter control flow by searching for the catching-try block, if any. + A structured instruction can consume *input* and produce *output* on the operand stack according to its annotated *block type*. It is given either as a :ref:`type index ` that refers to a suitable :ref:`function type `, or as an optional :ref:`value type ` inline, which is a shorthand for the function type :math:`[] \to [\valtype^?]`. @@ -425,6 +436,7 @@ In case of |LOOP| it is a *backward jump* to the beginning of the loop. Branch instructions come in several flavors: |BR| performs an unconditional branch, |BRIF| performs a conditional branch, +|BRONEXN| performs a branch if the exception on the stack matches the specified exception index, and |BRTABLE| performs an indirect branch through an operand indexing into the label vector that is an immediate to the instruction, or to a default target if the operand is out of bounds. The |RETURN| instruction is a shortcut for an unconditional branch to the outermost block, which implicitly is the body of the current function. Taking a branch *unwinds* the operand stack up to the height where the targeted structured control instruction was entered. diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst index f0973d81..8e76240b 100644 --- a/document/core/syntax/modules.rst +++ b/document/core/syntax/modules.rst @@ -1,4 +1,4 @@ -.. index:: ! module, type definition, function type, function, table, memory, global, element, data, start function, import, export +.. index:: ! module, type definition, function type, exception type, function, table, memory, exception, global, element, data, start function, import, export pair: abstract syntax; module .. _syntax-module: @@ -7,7 +7,7 @@ Modules WebAssembly programs are organized into *modules*, which are the unit of deployment, loading, and compilation. -A module collects definitions for :ref:`types `, :ref:`functions `, :ref:`tables `, :ref:`memories `, and :ref:`globals `. +A module collects definitions for :ref:`types `, :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`exceptions `, and :ref:`globals `. In addition, it can declare :ref:`imports ` and :ref:`exports ` and provide initialization in the form of :ref:`data ` and :ref:`element ` segments, or a :ref:`start function `. @@ -18,6 +18,7 @@ and provide initialization in the form of :ref:`data ` and :ref:`el \MFUNCS~\vec(\func), \\&&&& \MTABLES~\vec(\table), \\&&&& \MMEMS~\vec(\mem), \\&&&& + \MEXNS~\vec(\exn), \\&&&& \MGLOBALS~\vec(\global), \\&&&& \MELEMS~\vec(\elem), \\&&&& \MDATAS~\vec(\data), \\&&&& @@ -29,11 +30,12 @@ and provide initialization in the form of :ref:`data ` and :ref:`el Each of the vectors -- and thus the entire module -- may be empty. -.. index:: ! index, ! index space, ! type index, ! function index, ! table index, ! memory index, ! global index, ! local index, ! label index, ! element index, ! data index, function, global, table, memory, element, data, local, parameter, import +.. index:: ! index, ! index space, ! type index, ! function index, ! table index, ! memory index, ! exception index, ! global index, ! local index, ! label index, ! element index, ! data index, function, global, table, memory, exception, element, data, local, parameter, import pair: abstract syntax; type index pair: abstract syntax; function index pair: abstract syntax; table index pair: abstract syntax; memory index + pair: abstract syntax; exception index pair: abstract syntax; global index pair: abstract syntax; element index pair: abstract syntax; data index @@ -43,6 +45,7 @@ Each of the vectors -- and thus the entire module -- may be empty. pair: function; index pair: table; index pair: memory; index + pair: exception; index pair: global; index pair: element; index pair: data; index @@ -52,6 +55,7 @@ Each of the vectors -- and thus the entire module -- may be empty. .. _syntax-funcidx: .. _syntax-tableidx: .. _syntax-memidx: +.. _syntax-exnidx: .. _syntax-globalidx: .. _syntax-elemidx: .. _syntax-dataidx: @@ -71,6 +75,7 @@ Each class of definition has its own *index space*, as distinguished by the foll \production{function index} & \funcidx &::=& \u32 \\ \production{table index} & \tableidx &::=& \u32 \\ \production{memory index} & \memidx &::=& \u32 \\ + \production{exception index} & \exnidx &::=& \u32 \\ \production{global index} & \globalidx &::=& \u32 \\ \production{element index} & \elemidx &::=& \u32 \\ \production{data index} & \dataidx &::=& \u32 \\ @@ -78,7 +83,7 @@ Each class of definition has its own *index space*, as distinguished by the foll \production{label index} & \labelidx &::=& \u32 \\ \end{array} -The index space for :ref:`functions `, :ref:`tables `, :ref:`memories ` and :ref:`globals ` includes respective :ref:`imports ` declared in the same module. +The index space for :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`exceptions `, and :ref:`globals ` includes respective :ref:`imports ` declared in the same module. The indices of these imports precede the indices of other definitions in the same index space. Element indices reference :ref:`element segments ` and data indices reference :ref:`data segments `. @@ -92,6 +97,7 @@ Label indices reference :ref:`structured control instructions `, +starting with the smallest index not referencing an exception :ref:`import `. + + .. index:: ! global, global index, global type, mutability, expression, constant, value, import pair: abstract syntax; global .. _syntax-global: @@ -267,7 +294,7 @@ A declarative element segment is not available at runtime but merely serves to f .. math:: \begin{array}{llll} \production{element segment} & \elem &::=& - \{ \ETYPE~\reftype, \EINIT~\vec(\expr), \EMODE~\elemmode \} \\ + \{ \EELEMTYPE~\reftype, \EINIT~\vec(\expr), \EMODE~\elemmode \} \\ \production{element segment mode} & \elemmode &::=& \EPASSIVE \\&&|& \EACTIVE~\{ \ETABLE~\tableidx, \EOFFSET~\expr \} \\&&|& @@ -337,7 +364,7 @@ The |MSTART| component of a module declares the :ref:`function index `. -Exportable definitions are :ref:`functions `, :ref:`tables `, :ref:`memories `, and :ref:`globals `, +Exportable definitions are :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`exceptions `, and :ref:`globals `, which are referenced through a respective descriptor. @@ -378,15 +406,18 @@ The following auxiliary notation is defined for sequences of exports, filtering * :math:`\edmems(\export^\ast) = [\memidx ~|~ \EDMEM~\memidx \in (\export.\EDESC)^\ast]` +* :math:`\edexns(\export^\ast) = [\exnidx ~|~ \EDEXN~\exnidx \in (\export.\EDESC)^\ast]` + * :math:`\edglobals(\export^\ast) = [\globalidx ~|~ \EDGLOBAL~\globalidx \in (\export.\EDESC)^\ast]` -.. index:: ! import, name, function type, table type, memory type, global type, index, index space, type index, function index, table index, memory index, global index, function, table, memory, global, instantiation +.. index:: ! import, name, function type, table type, memory type, global type, exception type, index space, type index, function index, table index, memory index, global index, exception index, function, table, memory, exception, global, instantiation pair: abstract syntax; import single: function; import single: table; import single: memory; import single: global; import + single: exception; import .. _syntax-importdesc: .. _syntax-import: @@ -403,11 +434,12 @@ The |MIMPORTS| component of a module defines a set of *imports* that are require \IDFUNC~\typeidx \\&&|& \IDTABLE~\tabletype \\&&|& \IDMEM~\memtype \\&&|& + \IDEXN~\exntype \\&&|& \IDGLOBAL~\globaltype \\ \end{array} Each import is labeled by a two-level :ref:`name ` space, consisting of a |IMODULE| name and a |INAME| for an entity within that module. -Importable definitions are :ref:`functions `, :ref:`tables `, :ref:`memories `, and :ref:`globals `. +Importable definitions are :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`exceptions `, and :ref:`globals `. Each import is specified by a descriptor with a respective type that a definition provided during instantiation is required to match. Every import defines an index in the respective :ref:`index space `. diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 5a6c3d92..9de2b556 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -41,7 +41,7 @@ Conventions That is, :math:`|\I32| = |\F32| = 32` and :math:`|\I64| = |\F64| = 64`. -.. index:: ! reference type, reference, table, function, function type, null +.. index:: ! reference type, reference, table, function, function type, exception, exception type, null pair: abstract syntax; reference type pair: reference; type .. _syntax-reftype: @@ -54,11 +54,13 @@ Reference Types .. math:: \begin{array}{llll} \production{reference type} & \reftype &::=& - \FUNCREF ~|~ \EXTERNREF \\ + \FUNCREF ~|~ \EXNREF ~|~ \EXTERNREF \\ \end{array} The type |FUNCREF| denotes the infinite union of all references to :ref:`functions `, regardless of their :ref:`function types `. +The type |EXNREF| denotes a caught :ref:`exception `. + The type |EXTERNREF| denotes the infinite union of all references to objects owned by the :ref:`embedder ` and that can be passed into WebAssembly under this type. Reference types are *opaque*, meaning that neither their size nor their bit pattern can be observed. @@ -190,6 +192,28 @@ The limits are given in numbers of entries. In future versions of WebAssembly, additional element types may be introduced. +.. index:: ! exception, exception type, function type + pair: abstract syntax; exception + single: exception; type +.. _syntax-exntype: + +Exception Types +~~~~~~~~~~~~~~~ + +*Exception types* classify the signature of :ref:`exceptions ` with a function type. + +.. math:: + \begin{array}{llll} + \production{exception type} &\exntype &::=& \functype \\ + \end{array} + +The parameters of |functype| define the list of values associated with the exception. +Furthermore, it is an invariant of the semantics that every |functype| in a :ref:`valid ` exception type has an empty result type. + +.. note:: + Future versions of WebAssembly may allow non-empty result types in exceptions. + + .. index:: ! global type, ! mutability, value type, global, mutability pair: abstract syntax; global type pair: abstract syntax; mutability @@ -213,7 +237,7 @@ Global Types \end{array} -.. index:: ! external type, function type, table type, memory type, global type, import, external value +.. index:: ! external type, function type, table type, memory type, exception type, global type, import, external value pair: abstract syntax; external type pair: external; type .. _syntax-externtype: @@ -229,6 +253,7 @@ External Types \ETFUNC~\functype ~|~ \ETTABLE~\tabletype ~|~ \ETMEM~\memtype ~|~ + \ETEXN~\exntype ~|~ \ETGLOBAL~\globaltype \\ \end{array} @@ -245,4 +270,6 @@ It filters out entries of a specific kind in an order-preserving fashion: * :math:`\etmems(\externtype^\ast) = [\memtype ~|~ (\ETMEM~\memtype) \in \externtype^\ast]` +* :math:`\etexns(\externtype^\ast) = [\exntype ~|~ (\ETEXN~\exntype) \in \externtype^\ast]` + * :math:`\etglobals(\externtype^\ast) = [\globaltype ~|~ (\ETGLOBAL~\globaltype) \in \externtype^\ast]` diff --git a/document/core/text/conventions.rst b/document/core/text/conventions.rst index ea62cc4b..03dfe43f 100644 --- a/document/core/text/conventions.rst +++ b/document/core/text/conventions.rst @@ -123,6 +123,7 @@ It is convenient to define identifier contexts as :ref:`records ` can bind an optional symbolic :ref:`label identifier `. -The same label identifier may optionally be repeated after the corresponding :math:`\T{end}` and :math:`\T{else}` pseudo instructions, to indicate the matching delimiters. +The same label identifier may optionally be repeated after the corresponding :math:`\T{end}`, :math:`\T{else}`, and :math:`\T{catch}` +pseudo instructions, to indicate the matching delimiters. Their :ref:`block type ` is given as a :ref:`type use `, analogous to the type of :ref:`functions `. However, the special case of a type use that is syntactically empty or consists of only a single :ref:`result ` is not regarded as an :ref:`abbreviation ` for an inline :ref:`function type `, but is parsed directly into an optional :ref:`value type `. @@ -83,7 +85,11 @@ However, the special case of a type use that is syntactically empty or consists \text{if}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}_1{:}\Tinstr_{I'})^\ast~~ \text{else}~~\Tid_1^?~~(\X{in}_2{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid_2^? \\ &&&\qquad \Rightarrow\quad \IF~\X{bt}~\X{in}_1^\ast~\ELSE~\X{in}_2^\ast~\END - \qquad (\iff \Tid_1^? = \epsilon \vee \Tid_1^? = \Tlabel, \Tid_2^? = \epsilon \vee \Tid_2^? = \Tlabel) \\ + \qquad (\iff \Tid_1^? = \epsilon \vee \Tid_1^? = \Tlabel, \Tid_2^? = \epsilon \vee \Tid_2^? = \Tlabel) \\ &&|& + \text{try}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}_1{:}\Tinstr_{I'})^\ast~~ + \text{catch}~~\Tid_1^?~~(\X{in}_2{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid_2^? + \\ &&&\qquad \Rightarrow\quad \TRY~\X{rt}~\X{in}_1^\ast~\CATCH~\X{in}_2^\ast~\END + \quad (\iff \Tid_1^? = \epsilon \vee \Tid_1^? = \Tlabel, \Tid_2^? = \epsilon \vee \Tid_2^? = \Tlabel) \\ \end{array} .. note:: @@ -92,6 +98,9 @@ However, the special case of a type use that is syntactically empty or consists .. _text-nop: .. _text-unreachable: +.. _text-throw: +.. _text-rethrow: +.. _text-br_on_exn: .. _text-br: .. _text-br_if: .. _text-br_table: @@ -106,6 +115,9 @@ All other control instruction are represented verbatim. \production{plain instruction} & \Tplaininstr_I &::=& \text{unreachable} &\Rightarrow& \UNREACHABLE \\ &&|& \text{nop} &\Rightarrow& \NOP \\ &&|& + \text{throw}~~\text{(}\text{exception}~x{:}\Texnidx_I\text{)} &\Rightarrow& \THROW~x \\ &&|& + \text{rethrow} &\Rightarrow& \RETHROW \\ &&|& + \text{br\_on\_exn}~~l{:}\Tlabelidx_I~~\text{(}\text{exception}~x{:}\Texnidx_I~\text{)} &\Rightarrow& \BRONEXN~l~x \\ &&|& \text{br}~~l{:}\Tlabelidx_I &\Rightarrow& \BR~l \\ &&|& \text{br\_if}~~l{:}\Tlabelidx_I &\Rightarrow& \BRIF~l \\ &&|& \text{br\_table}~~l^\ast{:}\Tvec(\Tlabelidx_I)~~l_N{:}\Tlabelidx_I @@ -561,7 +573,10 @@ Such a folded instruction can appear anywhere a regular instruction can. \text{(}~\text{if}~~\Tlabel~~\Tblocktype~~\Tfoldedinstr^\ast &\hspace{-3ex} \text{(}~\text{then}~~\Tinstr_1^\ast~\text{)}~~\text{(}~\text{else}~~\Tinstr_2^\ast~\text{)}^?~~\text{)} \quad\equiv \\ &\qquad - \Tfoldedinstr^\ast~~\text{if}~~\Tlabel~~\Tblocktype &\hspace{-1ex} \Tinstr_1^\ast~~\text{else}~~(\Tinstr_2^\ast)^?~\text{end} \\ + \Tfoldedinstr^\ast~~\text{if}~~\Tlabel~~\Tblocktype &\hspace{-1ex} \Tinstr_1^\ast~~\text{else}~~(\Tinstr_2^\ast)^?~\text{end} \\ & + \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do}~~\Tinstr_1^\ast~~\text{)} + &\hspace{-8ex} \text{(}~\text{catch}~~\Tinstr_2^\ast~\text{)}~\text{)} \quad\equiv \\ &\qquad + \text{try}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast & \hspace{-6ex} \text{catch}~~\Tinstr_2^\ast~\text{end} & \\ \end{array} .. note:: diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index 9ae3b2d1..5a877eab 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -2,11 +2,12 @@ Modules ------- -.. index:: index, type index, function index, table index, memory index, global index, element index, data index, local index, label index +.. index:: index, type index, function index, table index, memory index, exception index, global index, element index, data index, local index, label index pair: text format; type index pair: text format; function index pair: text format; table index pair: text format; memory index + pair: text format; exception index pair: text format; global index pair: text format; element index pair: text format; data index @@ -16,6 +17,7 @@ Modules .. _text-funcidx: .. _text-tableidx: .. _text-memidx: +.. _text-exnidx: .. _text-globalidx: .. _text-localidx: .. _text-labelidx: @@ -41,6 +43,9 @@ Such identifiers are looked up in the suitable space of the :ref:`identifier con \production{memory index} & \Tmemidx_I &::=& x{:}\Tu32 &\Rightarrow& x \\&&|& v{:}\Tid &\Rightarrow& x & (\iff I.\IMEMS[x] = v) \\ + \production{exception index} & \Texnidx_I &::=& + x{:}\Tu32 &\Rightarrow& x \\&&|& + v{:}\Tid &\Rightarrow& x & (\iff I.\IEXNS[x] = v) \\ \production{global index} & \Tglobalidx_I &::=& x{:}\Tu32 &\Rightarrow& x \\&&|& v{:}\Tid &\Rightarrow& x & (\iff I.\IGLOBALS[x] = v) \\ @@ -147,7 +152,7 @@ is inserted at the end of the module. Abbreviations are expanded in the order they appear, such that previously inserted type definitions are reused by consecutive expansions. -.. index:: import, name, function type, table type, memory type, global type +.. index:: import, name, function type, table type, memory type, exception type, global type pair: text format; import .. _text-importdesc: .. _text-import: @@ -155,7 +160,7 @@ Abbreviations are expanded in the order they appear, such that previously insert Imports ~~~~~~~ -The descriptors in imports can bind a symbolic function, table, memory, or global :ref:`identifier `. +The descriptors in imports can bind a symbolic function, table, memory, exception, or global :ref:`identifier `. .. math:: \begin{array}{llclll} @@ -169,6 +174,8 @@ The descriptors in imports can bind a symbolic function, table, memory, or globa &\Rightarrow& \IDTABLE~\X{tt} \\ &&|& \text{(}~\text{memory}~~\Tid^?~~\X{mt}{:}\Tmemtype~\text{)} &\Rightarrow& \IDMEM~~\X{mt} \\ &&|& + \text{(}~\text{exception}~~\Tid^?~~\X{et}{:}\Texn~\text{)} + &\Rightarrow& \IDEXN~\X{et} \\ &&|& \text{(}~\text{global}~~\Tid^?~~\X{gt}{:}\Tglobaltype~\text{)} &\Rightarrow& \IDGLOBAL~\X{gt} \\ \end{array} @@ -177,7 +184,7 @@ The descriptors in imports can bind a symbolic function, table, memory, or globa Abbreviations ............. -As an abbreviation, imports may also be specified inline with :ref:`function `, :ref:`table `, :ref:`memory `, or :ref:`global ` definitions; see the respective sections. +As an abbreviation, imports may also be specified inline with :ref:`function `, :ref:`table `, :ref:`memory `, :ref:`exception ` or :ref:`global ` definitions; see the respective sections. @@ -380,6 +387,51 @@ Memories can be defined as :ref:`imports ` or :ref:`exports `. + +.. math:: + \begin{array}{llcl} + \production{exception} & \Texn_I &::=& + \text{(}~\text{exception}~~\Tid^?~~x,I'{:}\Ttypeuse_I~\text{)} \\ &&& \qquad + \Rightarrow\quad \{ \ETYPE~x \} \\ + \end{array} + + +.. index:: import, name + pair: text format; import +.. index:: export, name, index, exception index + pair: text format; export +.. index:: exception +.. _text-exn-abbrev: + +Abbreviations +............. + +Exceptions can be defined as :ref:`imports ` or :ref:`exports ` inline: + +.. math:: + \begin{array}{llclll} + \production{module field} & + \text{(}~\text{exception}~~\Tid^?~~\text{(}~\text{import}~~\Tname_1~~\Tname_2~\text{)}~~\Ttypeuse~\text{)} \quad\equiv \\ & \qquad + \text{(}~\text{import}~~\Tname_1~~\Tname_2~~\text{(}~\text{exception}~~\Tid^?~~\Ttypeuse~\text{)}~\text{)} + \\[1ex] & + \text{(}~\text{exception}~~\Tid^?~~\text{(}~\text{export}~~\Tname~\text{)}~~\dots~\text{)} \quad\equiv \\ & \qquad + \text{(}~\text{export}~~\Tname~~\text{(}~\text{exception}~~\Tid'~\text{)}~\text{)}~~ + \text{(}~\text{exception}~~\Tid'~~\dots~\text{)} + \\ & \qquad\qquad + (\iff \Tid' = \Tid^? \neq \epsilon \vee \Tid' \idfresh) \\ + \end{array} + +The latter abbreviation can be applied repeatedly, with ":math:`\dots`" containing another import or export. + + .. index:: global, global type, identifier, expression pair: text format; global .. _text-global: @@ -424,7 +476,7 @@ Globals can be defined as :ref:`imports ` or :ref:`exports ` dire &\Rightarrow& \EDTABLE~x \\ &&|& \text{(}~\text{memory}~~x{:}\Tmemidx_I~\text{)} &\Rightarrow& \EDMEM~x \\ &&|& + \text{(}~\text{exception}~~x{:}\Texnidx_I~\text{)} + &\Rightarrow& \EDEXN~x \\&&|& \text{(}~\text{global}~~x{:}\Tglobalidx_I~\text{)} &\Rightarrow& \EDGLOBAL~x \\ \end{array} @@ -454,7 +508,7 @@ The syntax for exports mirrors their :ref:`abstract syntax ` dire Abbreviations ............. -As an abbreviation, exports may also be specified inline with :ref:`function `, :ref:`table `, :ref:`memory `, or :ref:`global ` definitions; see the respective sections. +As an abbreviation, exports may also be specified inline with :ref:`function `, :ref:`table `, :ref:`memory `, :ref:`exception ` definitions, or :ref:`global ` definitions; see the respective sections. .. index:: start function, function index @@ -497,13 +551,13 @@ Element segments allow for an optional :ref:`table index ` to ide \begin{array}{llclll} \production{element segment} & \Telem_I &::=& \text{(}~\text{elem}~~\Tid^?~~(et, y^\ast){:}\Telemlist~\text{)} \\ &&& \qquad - \Rightarrow\quad \{ \ETYPE~et, \EINIT~y^\ast, \EMODE~\EPASSIVE \} \\ &&|& + \Rightarrow\quad \{ \EELEMTYPE~et, \EINIT~y^\ast, \EMODE~\EPASSIVE \} \\ &&|& \text{(}~\text{elem}~~\Tid^?~~x{:}\Ttableuse_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~(et, y^\ast){:}\Telemlist~\text{)} \\ &&& \qquad - \Rightarrow\quad \{ \ETYPE~et, \EINIT~y^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&& + \Rightarrow\quad \{ \EELEMTYPE~et, \EINIT~y^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&& \text{(}~\text{elem}~~\Tid^?~~\text{declare}~~(et, y^\ast){:}\Telemlist~\text{)} \\ &&& \qquad - \Rightarrow\quad \{ \ETYPE~et, \EINIT~y^\ast, \EMODE~\EDECLARATIVE \} \\ + \Rightarrow\quad \{ \EELEMTYPE~et, \EINIT~y^\ast, \EMODE~\EDECLARATIVE \} \\ \production{element list} & \Telemlist &::=& - t{:}\Treftype~~y^\ast{:}\Tvec(\Telemexpr_I) \qquad\Rightarrow\quad ( \ETYPE~t, \EINIT~y^\ast ) \\ + t{:}\Treftype~~y^\ast{:}\Tvec(\Telemexpr_I) \qquad\Rightarrow\quad ( \EELEMTYPE~t, \EINIT~y^\ast ) \\ \production{element expression} & \Telemexpr &::=& \text{(}~\text{item}~~e{:}\Texpr~\text{)} \quad\Rightarrow\quad e \\ @@ -609,7 +663,7 @@ Also, a memory use can be omitted, defaulting to :math:`\T{0}`. As another abbreviation, data segments may also be specified inline with :ref:`memory ` definitions; see the respective section. -.. index:: module, type definition, function type, function, table, memory, global, element, data, start function, import, export, identifier context, identifier, name section +.. index:: module, type definition, function type, function, table, memory, exception, global, element, data, start function, import, export, identifier context, identifier, name section pair: text format; module single: section; name .. _text-modulefield: @@ -644,6 +698,7 @@ The name serves a documentary role only. \X{fn}{:}\Tfunc_I &\Rightarrow& \{\MFUNCS~\X{fn}\} \\ |& \X{ta}{:}\Ttable_I &\Rightarrow& \{\MTABLES~\X{ta}\} \\ |& \X{me}{:}\Tmem_I &\Rightarrow& \{\MMEMS~\X{me}\} \\ |& + \X{et}{:}\Texn_I &\Rightarrow& \{\MEXNS~\X{et}\} \\ |& \X{gl}{:}\Tglobal_I &\Rightarrow& \{\MGLOBALS~\X{gl}\} \\ |& \X{ex}{:}\Texport_I &\Rightarrow& \{\MEXPORTS~\X{ex}\} \\ |& \X{st}{:}\Tstart_I &\Rightarrow& \{\MSTART~\X{st}\} \\ |& @@ -656,11 +711,11 @@ The following restrictions are imposed on the composition of :ref:`modules ` must occur before any regular definition of a :ref:`function `, :ref:`table `, :ref:`memory `, or :ref:`global `, + The second condition enforces that all :ref:`imports ` must occur before any regular definition of a :ref:`function `, :ref:`table `, :ref:`memory `, :ref:`exception `, or :ref:`global `, thereby maintaining the ordering of the respective :ref:`index spaces `. The :ref:`well-formedness ` condition on :math:`I` in the grammar for |Tmodule| ensures that no namespace contains duplicate identifiers. @@ -677,6 +732,8 @@ The definition of the initial :ref:`identifier context ` :math:`I` \{\ITABLES~(\Tid^?)\} \\ \F{idc}(\text{(}~\text{memory}~\Tid^?~\dots~\text{)}) &=& \{\IMEMS~(\Tid^?)\} \\ + \F{idc}(\text{(}~\text{exception}~\Tid^?~\dots~\text{)}) &=& + \{\IEXNS~(\Tid^?)\} \\ \F{idc}(\text{(}~\text{global}~\Tid^?~\dots~\text{)}) &=& \{\IGLOBALS~(\Tid^?)\} \\ \F{idc}(\text{(}~\text{elem}~\Tid^?~\dots~\text{)}) &=& @@ -689,6 +746,8 @@ The definition of the initial :ref:`identifier context ` :math:`I` \{\ITABLES~(\Tid^?)\} \\ \F{idc}(\text{(}~\text{import}~\dots~\text{(}~\text{memory}~\Tid^?~\dots~\text{)}~\text{)}) &=& \{\IMEMS~(\Tid^?)\} \\ + \F{idc}(\text{(}~\text{import}~\dots~\text{(}~\text{exception}~\Tid^?~\dots~\text{)}~\text{)}) &=& + \{\IEXNS~(\Tid^?)\} \\ \F{idc}(\text{(}~\text{import}~\dots~\text{(}~\text{global}~\Tid^?~\dots~\text{)}~\text{)}) &=& \{\IGLOBALS~(\Tid^?)\} \\ \F{idc}(\text{(}~\dots~\text{)}) &=& diff --git a/document/core/text/types.rst b/document/core/text/types.rst index bfeb2b82..6c655efe 100644 --- a/document/core/text/types.rst +++ b/document/core/text/types.rst @@ -34,9 +34,11 @@ Reference Types \begin{array}{llcll@{\qquad\qquad}l} \production{reference type} & \Treftype &::=& \text{funcref} &\Rightarrow& \FUNCREF \\ &&|& + \text{exnref} &\Rightarrow& \EXNREF \\ &&|& \text{externref} &\Rightarrow& \EXTERNREF \\ \production{referenced type} & \Trefedtype &::=& \text{func} &\Rightarrow& \FUNCREF \\ &&|& + \text{exn} &\Rightarrow& \EXNREF \\ &&|& \text{extern} &\Rightarrow& \EXTERNREF \\ \end{array} diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 360b9d84..cefab579 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -3,11 +3,11 @@ .. External Standards .. ------------------ -.. |WasmDraft| replace:: https://webassembly.github.io/reference-types/core/ -.. _WasmDraft: https://webassembly.github.io/reference-types/core/ +.. |WasmDraft| replace:: http://webassembly.github.io/exception-handling/core/ +.. _WasmDraft: http://webassembly.github.io/exception-handling/core/ -.. |WasmIssues| replace:: https://github.com/webassembly/reference-types/issues/ -.. _WasmIssues: https://github.com/webassembly/reference-types/issues/ +.. |WasmIssues| replace:: http://github.com/webassembly/exception-handling/issues/ +.. _WasmIssues: http://github.com/webassembly/exception-handling/issues/ .. |IEEE754| replace:: IEEE 754-2019 .. _IEEE754: https://ieeexplore.ieee.org/document/8766229 @@ -179,6 +179,7 @@ .. |FUNCREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{funcref}} .. |EXTERNREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{externref}} +.. |EXNREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{exnref}} .. |MVAR| mathdef:: \xref{syntax/types}{syntax-mut}{\K{var}} .. |MCONST| mathdef:: \xref{syntax/types}{syntax-mut}{\K{const}} @@ -190,6 +191,7 @@ .. |ETTABLE| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{table}} .. |ETMEM| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{mem}} .. |ETGLOBAL| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{global}} +.. |ETEXN| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{exception}} .. Types, non-terminals @@ -199,6 +201,7 @@ .. |valtype| mathdef:: \xref{syntax/types}{syntax-valtype}{\X{valtype}} .. |resulttype| mathdef:: \xref{syntax/types}{syntax-resulttype}{\X{resulttype}} .. |functype| mathdef:: \xref{syntax/types}{syntax-functype}{\X{functype}} +.. |exntype| mathdef:: \xref{syntax/types}{syntax-exntype}{\X{exntype}} .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}} .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}} @@ -216,6 +219,7 @@ .. |ettables| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}} .. |etmems| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{mems}} .. |etglobals| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{globals}} +.. |etexns| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{exceptions}} .. Indices, non-terminals @@ -229,6 +233,7 @@ .. |dataidx| mathdef:: \xref{syntax/modules}{syntax-dataidx}{\X{dataidx}} .. |localidx| mathdef:: \xref{syntax/modules}{syntax-localidx}{\X{localidx}} .. |labelidx| mathdef:: \xref{syntax/modules}{syntax-labelidx}{\X{labelidx}} +.. |exnidx| mathdef:: \xref{syntax/modules}{syntax-exnidx}{\X{exnidx}} .. Indices, meta functions @@ -251,6 +256,7 @@ .. |MTABLES| mathdef:: \xref{syntax/modules}{syntax-module}{\K{tables}} .. |MMEMS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{mems}} .. |MGLOBALS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{globals}} +.. |MEXNS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{exceptions}} .. |MIMPORTS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{imports}} .. |MEXPORTS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{exports}} .. |MDATAS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{datas}} @@ -265,10 +271,12 @@ .. |MTYPE| mathdef:: \xref{syntax/modules}{syntax-mem}{\K{type}} +.. |ETYPE| mathdef:: \xref{syntax/modules}{syntax-exn}{\K{type}} + .. |GTYPE| mathdef:: \xref{syntax/modules}{syntax-global}{\K{type}} .. |GINIT| mathdef:: \xref{syntax/modules}{syntax-global}{\K{init}} -.. |ETYPE| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{type}} +.. |EELEMTYPE| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{type}} .. |EINIT| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{init}} .. |EMODE| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{mode}} .. |EPASSIVE| mathdef:: \xref{syntax/modules}{syntax-elemmode}{\K{passive}} @@ -292,6 +300,7 @@ .. |EDTABLE| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{table}} .. |EDMEM| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{mem}} .. |EDGLOBAL| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{global}} +.. |EDEXN| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{exception}} .. |IMODULE| mathdef:: \xref{syntax/modules}{syntax-import}{\K{module}} .. |INAME| mathdef:: \xref{syntax/modules}{syntax-import}{\K{name}} @@ -299,6 +308,7 @@ .. |IDFUNC| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{func}} .. |IDTABLE| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{table}} .. |IDMEM| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{mem}} +.. |IDEXN| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{exception}} .. |IDGLOBAL| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{global}} @@ -309,6 +319,7 @@ .. |func| mathdef:: \xref{syntax/modules}{syntax-func}{\X{func}} .. |table| mathdef:: \xref{syntax/modules}{syntax-table}{\X{table}} .. |mem| mathdef:: \xref{syntax/modules}{syntax-mem}{\X{mem}} +.. |exn| mathdef:: \xref{syntax/modules}{syntax-exn}{\X{exn}} .. |global| mathdef:: \xref{syntax/modules}{syntax-global}{\X{global}} .. |import| mathdef:: \xref{syntax/modules}{syntax-import}{\X{import}} .. |export| mathdef:: \xref{syntax/modules}{syntax-export}{\X{export}} @@ -326,6 +337,7 @@ .. |edfuncs| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{funcs}} .. |edtables| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{tables}} .. |edmems| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{mems}} +.. |edexns| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{exceptions}} .. |edglobals| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{globals}} @@ -347,6 +359,11 @@ .. |RETURN| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return}} .. |CALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call}} .. |CALLINDIRECT| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_indirect}} +.. |TRY| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{try}} +.. |CATCH| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{catch}} +.. |THROW| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{throw}} +.. |RETHROW| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{rethrow}} +.. |BRONEXN| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_exn}} .. |DROP| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{drop}} .. |SELECT| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{select}} @@ -503,6 +520,7 @@ .. |Bresulttype| mathdef:: \xref{binary/types}{binary-resulttype}{\B{resulttype}} .. |Bfunctype| mathdef:: \xref{binary/types}{binary-functype}{\B{functype}} .. |Bglobaltype| mathdef:: \xref{binary/types}{binary-globaltype}{\B{globaltype}} +.. |Bexntype| mathdef:: \xref{binary/types}{binary-exntype}{\B{exntype}} .. |Btabletype| mathdef:: \xref{binary/types}{binary-tabletype}{\B{tabletype}} .. |Bmemtype| mathdef:: \xref{binary/types}{binary-memtype}{\B{memtype}} .. |Blimits| mathdef:: \xref{binary/types}{binary-limits}{\B{limits}} @@ -516,6 +534,7 @@ .. |Bfuncidx| mathdef:: \xref{binary/modules}{binary-funcidx}{\B{funcidx}} .. |Btableidx| mathdef:: \xref{binary/modules}{binary-tableidx}{\B{tableidx}} .. |Bmemidx| mathdef:: \xref{binary/modules}{binary-memidx}{\B{memidx}} +.. |Bexnidx| mathdef:: \xref{binary/modules}{binary-exnidx}{\B{exnidx}} .. |Bglobalidx| mathdef:: \xref{binary/modules}{binary-globalidx}{\B{globalidx}} .. |Belemidx| mathdef:: \xref{binary/modules}{binary-elemidx}{\B{elemidx}} .. |Bdataidx| mathdef:: \xref{binary/modules}{binary-dataidx}{\B{dataidx}} @@ -536,6 +555,7 @@ .. |Bcodesec| mathdef:: \xref{binary/modules}{binary-codesec}{\B{codesec}} .. |Btablesec| mathdef:: \xref{binary/modules}{binary-tablesec}{\B{tablesec}} .. |Bmemsec| mathdef:: \xref{binary/modules}{binary-memsec}{\B{memsec}} +.. |Bexnsec| mathdef:: \xref{binary/modules}{binary-exnsec}{\B{exnsec}} .. |Bglobalsec| mathdef:: \xref{binary/modules}{binary-globalsec}{\B{globalsec}} .. |Bimportsec| mathdef:: \xref{binary/modules}{binary-importsec}{\B{importsec}} .. |Bexportsec| mathdef:: \xref{binary/modules}{binary-exportsec}{\B{exportsec}} @@ -549,6 +569,7 @@ .. |Bfunc| mathdef:: \xref{binary/modules}{binary-func}{\B{func}} .. |Btable| mathdef:: \xref{binary/modules}{binary-table}{\B{table}} .. |Bmem| mathdef:: \xref{binary/modules}{binary-mem}{\B{mem}} +.. |Bexn| mathdef:: \xref{binary/modules}{binary-exn}{\B{exn}} .. |Bglobal| mathdef:: \xref{binary/modules}{binary-global}{\B{global}} .. |Bimport| mathdef:: \xref{binary/modules}{binary-import}{\B{import}} .. |Bexport| mathdef:: \xref{binary/modules}{binary-export}{\B{export}} @@ -679,6 +700,7 @@ .. |Tfuncidx| mathdef:: \xref{text/modules}{text-funcidx}{\T{funcidx}} .. |Ttableidx| mathdef:: \xref{text/modules}{text-tableidx}{\T{tableidx}} .. |Tmemidx| mathdef:: \xref{text/modules}{text-memidx}{\T{memidx}} +.. |Texnidx| mathdef:: \xref{text/modules}{text-exnidx}{\T{exnidx}} .. |Tglobalidx| mathdef:: \xref{text/modules}{text-globalidx}{\T{globalidx}} .. |Telemidx| mathdef:: \xref{text/modules}{text-elemidx}{\T{elemidx}} .. |Tdataidx| mathdef:: \xref{text/modules}{text-dataidx}{\T{dataidx}} @@ -704,6 +726,7 @@ .. |Tfunc| mathdef:: \xref{text/modules}{text-func}{\T{func}} .. |Ttable| mathdef:: \xref{text/modules}{text-table}{\T{table}} .. |Tmem| mathdef:: \xref{text/modules}{text-mem}{\T{mem}} +.. |Texn| mathdef:: \xref{text/modules}{text-exn}{\T{exception}} .. |Tglobal| mathdef:: \xref{text/modules}{text-global}{\T{global}} .. |Timport| mathdef:: \xref{text/modules}{text-import}{\T{import}} .. |Texport| mathdef:: \xref{text/modules}{text-export}{\T{export}} @@ -749,6 +772,7 @@ .. |IFUNCS| mathdef:: \xref{text/conventions}{text-context}{\K{funcs}} .. |ITABLES| mathdef:: \xref{text/conventions}{text-context}{\K{tables}} .. |IMEMS| mathdef:: \xref{text/conventions}{text-context}{\K{mems}} +.. |IEXNS| mathdef:: \xref{text/conventions}{text-context}{\K{exceptions}} .. |IGLOBALS| mathdef:: \xref{text/conventions}{text-context}{\K{globals}} .. |IELEM| mathdef:: \xref{text/conventions}{text-context}{\K{elem}} .. |IDATA| mathdef:: \xref{text/conventions}{text-context}{\K{data}} @@ -779,6 +803,7 @@ .. |CFUNCS| mathdef:: \xref{valid/conventions}{context}{\K{funcs}} .. |CTABLES| mathdef:: \xref{valid/conventions}{context}{\K{tables}} .. |CMEMS| mathdef:: \xref{valid/conventions}{context}{\K{mems}} +.. |CEXNS| mathdef:: \xref{valid/conventions}{context}{\K{exceptions}} .. |CGLOBALS| mathdef:: \xref{valid/conventions}{context}{\K{globals}} .. |CELEMS| mathdef:: \xref{valid/conventions}{context}{\K{elems}} .. |CDATAS| mathdef:: \xref{valid/conventions}{context}{\K{datas}} @@ -795,6 +820,7 @@ .. |vdashfunctype| mathdef:: \xref{valid/types}{valid-functype}{\vdash} .. |vdashtabletype| mathdef:: \xref{valid/types}{valid-tabletype}{\vdash} .. |vdashmemtype| mathdef:: \xref{valid/types}{valid-memtype}{\vdash} +.. |vdashexntype| mathdef:: \xref{valid/types}{valid-exntype}{\vdash} .. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash} .. |vdashexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\vdash} @@ -807,6 +833,7 @@ .. |vdashfunc| mathdef:: \xref{valid/modules}{valid-func}{\vdash} .. |vdashtable| mathdef:: \xref{valid/modules}{valid-table}{\vdash} .. |vdashmem| mathdef:: \xref{valid/modules}{valid-mem}{\vdash} +.. |vdashexn| mathdef:: \xref{valid/modules}{valid-exn}{\vdash} .. |vdashglobal| mathdef:: \xref{valid/modules}{valid-global}{\vdash} .. |vdashelem| mathdef:: \xref{valid/modules}{valid-elem}{\vdash} .. |vdashelemmode| mathdef:: \xref{valid/modules}{valid-elemmode}{\vdash} @@ -837,6 +864,7 @@ .. |allochostfunc| mathdef:: \xref{exec/modules}{alloc-hostfunc}{\F{allochostfunc}} .. |alloctable| mathdef:: \xref{exec/modules}{alloc-table}{\F{alloctable}} .. |allocmem| mathdef:: \xref{exec/modules}{alloc-mem}{\F{allocmem}} +.. |allocexn| mathdef:: \xref{exec/modules}{alloc-exn}{\F{allocexn}} .. |allocglobal| mathdef:: \xref{exec/modules}{alloc-global}{\F{allocglobal}} .. |allocelem| mathdef:: \xref{exec/modules}{alloc-elem}{\F{allocelem}} .. |allocdata| mathdef:: \xref{exec/modules}{alloc-data}{\F{allocdata}} @@ -852,6 +880,7 @@ .. |funcaddr| mathdef:: \xref{exec/runtime}{syntax-funcaddr}{\X{funcaddr}} .. |tableaddr| mathdef:: \xref{exec/runtime}{syntax-tableaddr}{\X{tableaddr}} .. |memaddr| mathdef:: \xref{exec/runtime}{syntax-memaddr}{\X{memaddr}} +.. |exnaddr| mathdef:: \xref{exec/runtime}{syntax-exnaddr}{\X{exnaddr}} .. |globaladdr| mathdef:: \xref{exec/runtime}{syntax-globaladdr}{\X{globaladdr}} .. |elemaddr| mathdef:: \xref{exec/runtime}{syntax-elemaddr}{\X{elemaddr}} .. |dataaddr| mathdef:: \xref{exec/runtime}{syntax-dataaddr}{\X{dataaddr}} @@ -870,10 +899,12 @@ .. |MITYPE| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{type}} .. |MIDATA| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{data}} +.. |EITYPE| mathdef:: \xref{exec/runtime}{syntax-exninst}{\K{type}} + .. |GITYPE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{type}} .. |GIVALUE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{value}} -.. |EITYPE| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{type}} +.. |EIELEMTYPE| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{type}} .. |EIELEM| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{elem}} .. |DIDATA| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{data}} @@ -884,12 +915,14 @@ .. |EVFUNC| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{func}} .. |EVTABLE| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{table}} .. |EVMEM| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{mem}} +.. |EVEXN| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{exception}} .. |EVGLOBAL| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{global}} .. |MITYPES| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{types}} .. |MIFUNCS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{funcaddrs}} .. |MITABLES| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{tableaddrs}} .. |MIMEMS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{memaddrs}} +.. |MIEXNS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{exnaddrs}} .. |MIGLOBALS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{globaladdrs}} .. |MIELEMS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{elemaddrs}} .. |MIDATAS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{dataaddrs}} @@ -904,6 +937,7 @@ .. |funcinst| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\X{funcinst}} .. |tableinst| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\X{tableinst}} .. |meminst| mathdef:: \xref{exec/runtime}{syntax-meminst}{\X{meminst}} +.. |exninst| mathdef:: \xref{exec/runtime}{syntax-exninst}{\X{exninst}} .. |globalinst| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\X{globalinst}} .. |eleminst| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\X{eleminst}} .. |datainst| mathdef:: \xref{exec/runtime}{syntax-datainst}{\X{datainst}} @@ -917,6 +951,7 @@ .. |evfuncs| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{funcs}} .. |evtables| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{tables}} .. |evmems| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{mems}} +.. |evexns| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{exceptions}} .. |evglobals| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{globals}} @@ -925,6 +960,7 @@ .. |SFUNCS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{funcs}} .. |STABLES| mathdef:: \xref{exec/runtime}{syntax-store}{\K{tables}} .. |SMEMS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{mems}} +.. |SEXNS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{exceptions}} .. |SGLOBALS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{globals}} .. |SELEMS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{elems}} .. |SDATAS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{datas}} @@ -960,6 +996,9 @@ .. |REFEXTERNADDR| mathdef:: \xref{exec/runtime}{syntax-ref.extern}{\K{ref{.}extern}} .. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}} .. |INVOKE| mathdef:: \xref{exec/runtime}{syntax-invoke}{\K{invoke}} +.. |REFEXNADDR| mathdef:: \xref{exec/runtime}{syntax-refexnaddr}{\K{ref{.}exn}} +.. |THROWADDR| mathdef:: \xref{exec/runtime}{syntax-throwaddr}{\K{throw}} +.. |CATCHN| mathdef:: \xref{exec/runtime}{syntax-catchn}{\K{catch}} .. Values & Results, non-terminals @@ -978,6 +1017,7 @@ .. Administrative Instructions, non-terminals .. |XB| mathdef:: \xref{exec/runtime}{syntax-ctxt-block}{B} +.. |XT| mathdef:: \xref{exec/runtime}{syntax-ctxt-throw}{T} .. Configurations, non-terminals @@ -1099,6 +1139,7 @@ .. |vdashfuncinst| mathdef:: \xref{appendix/properties}{valid-funcinst}{\vdash} .. |vdashtableinst| mathdef:: \xref{appendix/properties}{valid-tableinst}{\vdash} .. |vdashmeminst| mathdef:: \xref{appendix/properties}{valid-meminst}{\vdash} +.. |vdashexninst| mathdef:: \xref{appendix/properties}{valid-exninst}{\vdash} .. |vdashglobalinst| mathdef:: \xref{appendix/properties}{valid-globalinst}{\vdash} .. |vdasheleminst| mathdef:: \xref{appendix/properties}{valid-eleminst}{\vdash} .. |vdashdatainst| mathdef:: \xref{appendix/properties}{valid-datainst}{\vdash} @@ -1113,6 +1154,7 @@ .. |vdashfuncinstextends| mathdef:: \xref{appendix/properties}{extend-funcinst}{\vdash} .. |vdashtableinstextends| mathdef:: \xref{appendix/properties}{extend-tableinst}{\vdash} .. |vdashmeminstextends| mathdef:: \xref{appendix/properties}{extend-meminst}{\vdash} +.. |vdashexninstextends| mathdef:: \xref{appendix/properties}{extend-exninst}{\vdash} .. |vdashglobalinstextends| mathdef:: \xref{appendix/properties}{extend-globalinst}{\vdash} .. |vdasheleminstextends| mathdef:: \xref{appendix/properties}{extend-eleminst}{\vdash} .. |vdashdatainstextends| mathdef:: \xref{appendix/properties}{extend-datainst}{\vdash} diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index b6a49b0c..027b5938 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -24,7 +24,7 @@ That is, they only formulate the constraints, they do not define an algorithm. The skeleton of a sound and complete algorithm for type-checking instruction sequences according to this specification is provided in the :ref:`appendix `. -.. index:: ! context, function type, table type, memory type, global type, value type, result type, index space, module, function +.. index:: ! context, function type, table type, memory type, exception type, global type, value type, result type, index space, module, function, exception .. _context: Contexts @@ -37,6 +37,7 @@ which collects relevant information about the surrounding :ref:`module ` :math: & \CFUNCS & \functype^\ast, \\ & \CTABLES & \tabletype^\ast, \\ & \CMEMS & \memtype^\ast, \\ + & \CEXNS & \exntype^\ast, \\ & \CGLOBALS & \globaltype^\ast, \\ & \CELEMS & \reftype^\ast, \\ & \CDATAS & {\ok}^\ast, \\ diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 5dbf44f4..523a31fd 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -746,7 +746,7 @@ Memory Instructions } -.. index:: control instructions, structured control, label, block, branch, block type, label index, function index, type index, vector, polymorphism, context +.. index:: control instructions, structured control, label, block, branch, block type, label index, function index, type index, exception index, vector, polymorphism, context pair: validation; instruction single: abstract syntax; instruction .. _valid-label: @@ -872,6 +872,113 @@ Control Instructions The :ref:`notation ` :math:`C,\CLABELS\,[t^\ast]` inserts the new label type at index :math:`0`, shifting all others. + +.. _valid-try: + +:math:`\TRY~\blocktype~\instr_1^\ast~\CATCH~\instr_2^\ast~\END` +............................................................... + + +* The :ref:`block type ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. + +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. + +* Under context :math:`C'`, + the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. + +* Under context :math:`C'`, + the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid ` with type :math:`[\EXNREF] \to [t_2^\ast]`. + +* Then the compound instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`. + +.. math:: + \frac{ + \begin{array}{lll} + C \vdashblocktype \blocktype : [t_1^\ast] \to [t_2^\ast] & \qquad & \\ + C,\CLABELS\,[t_2^\ast] \vdashinstrseq \instr_1^\ast : [t_1^\ast] \to [t_2^\ast] + & \qquad & + C,\CLABELS\,[t_2^\ast] \vdashinstrseq \instr_2^\ast : [\EXNREF] \to [t_2^\ast]\\ + \end{array} + }{ + C \vdashinstr \TRY~\blocktype~\instr_1^\ast~\CATCH~\instr_2^\ast~\END : [t_1^\ast] \to [t_2^\ast] + } + +.. note:: + The :ref:`notation ` :math:`C,\CLABELS\,[t_2^\ast]` inserts the new label type at index :math:`0`, shifting all others. + + +.. _valid-throw: + +:math:`\THROW~x` +................ + +* The exception :math:`C.\CEXNS[x]` must be defined in the context. + +* Let :math:`[t^\ast] \to []` be its :ref:`exception type `. + +* Then the instruction is valid with type :math:`[t_1^\ast t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. + +.. math:: + \frac{ + C.\CEXNS[x] = [t^\ast] \to [] + }{ + C \vdashinstr \THROW~x : [t_1^\ast t^\ast] \to [t_2^\ast] + } + + +.. note:: + The |THROW| instruction is :ref:`stack-polymorphic `. + + +.. _valid-rethrow: + +:math:`\RETHROW` +................ + +* The instruction is valid with type :math:`[t_1^\ast \EXNREF] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. + +.. math:: + \frac{ + }{ + C \vdashinstr \RETHROW : [t_1^\ast \EXNREF] \to [t_2^\ast] + } + + +.. note:: + The |RETHROW| instruction is :ref:`stack-polymorphic `. + + +.. _valid-br_on_exn: + +:math:`\BRONEXN~l~x` +.................... + +* The label :math:`C.\CLABELS[l]` must be defined in the context. + +* The exception :math:`C.\CEXNS[x]` must be defined in the context. + +* Let :math:`[t^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. + +* Assert: the exception :math:`C.\CEXNS[x]` is :math:`[t'^\ast]\to[]`. + +* The type sequence :math:`t'^\ast` must be the same as the type sequence :math:`t^\ast`. + +* Then the instruction is valid with type :math:`[\EXNREF]\to[\EXNREF]` + +.. math:: + \frac{ + C.\CLABELS[l]=[t^\ast] + \qquad + C.\CEXNS[x]=[t^\ast]\to[] + }{ + C \vdashinstr \BRONEXN~l~x : [\EXNREF]\to[\EXNREF] + } + +.. note:: + The :ref:`label index ` space in the :ref:`context ` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected. + + + .. _valid-br: :math:`\BR~l` diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index eeed38f3..15bc170e 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -98,6 +98,36 @@ Memories :math:`\mem` are classified by :ref:`memory types `. } +.. index:: exception, exception type, function type + pair: validation; exception + single: abstract syntax; exception +.. _valid-exn: + +Exceptions +~~~~~~~~~~ + +Exceptions :math:`\exn` are classified by their :ref:`exception type `, +which contains an index to a :ref:`function type ` with empty result. + +:math:`\{ \ETYPE~x \}` +...................... + +* The type :math:`C.\CTYPES[x]` must be defined in the context. + +* Let :math:`[t^\ast] \to [t'^\ast]` be the :ref:`function type ` :math:`C.\CTYPES[x]`. + +* The sequence :math:`t'^\ast` must be empty. + +* Then the exception definition is valid with :ref:`exception type ` :math:`[t^\ast]\to[]`. + +.. math:: + \frac{ + C.\CTYPES[x] = [t^\ast] \to [] + }{ + C \vdashexn \{ \ETYPE~x \} : [t^\ast]\to[] + } + + .. index:: global, global type, expression pair: validation; global single: abstract syntax; global @@ -144,8 +174,8 @@ Element Segments Element segments :math:`\elem` are classified by the :ref:`reference type ` of their elements. -:math:`\{ \ETYPE~t, \EINIT~e^\ast, \EMODE~\elemmode \}` -....................................................... +:math:`\{ \EELEMTYPE~t, \EINIT~e^\ast, \EMODE~\elemmode \}` +........................................................... * For each :math:`e_i` in :math:`e^\ast`, @@ -166,7 +196,7 @@ Element segments :math:`\elem` are classified by the :ref:`reference type ` :math:`\ETEXN~C.\CEXNS[x]`. + +.. math:: + \frac{ + C.\CEXNS[x] = \exntype + }{ + C \vdashexportdesc \EDEXN~x : \ETEXN~\exntype + } + + :math:`\EDGLOBAL~x` ................... @@ -402,7 +447,7 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi } -.. index:: import, name, function type, table type, memory type, global type +.. index:: import, name, function type, table type, memory type, exception type, global type pair: validation; import single: abstract syntax; import .. _valid-importdesc: @@ -476,6 +521,26 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi } +:math:`\IDEXN~\exn` +................... + +* Let :math:`\{ \ETYPE~x \}` be the exception :math:`\exn`. + +* The type :math:`C.\CTYPES[x]` must be defined in the context. + +* The :ref:`exception type ` :math:`C.\CTYPES[x]` must be a :ref:`valid exception type `. + +* Then the import description is valid with type :math:`\ETEXN~C.\CTYPES[x]`. + +.. math:: + \frac{ + \vdashexntype C.\CTYPES[x] \ok + }{ + C \vdashimportdesc \IDEXN~\{ \ETYPE~x \} : \ETEXN~C.\CTYPES[x] + } + + + :math:`\IDGLOBAL~\globaltype` ............................. @@ -491,7 +556,7 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi } -.. index:: module, type definition, function type, function, table, memory, global, element, data, start function, import, export, context +.. index:: module, type definition, function type, function, table, memory, exception, global, element, data, start function, import, export, context pair: validation; module single: abstract syntax; module .. _valid-module: @@ -521,6 +586,9 @@ Instead, the context :math:`C` for validation of the module's content is constru * :math:`C.\CMEMS` is :math:`\etmems(\X{it}^\ast)` concatenated with :math:`\X{mt}^\ast`, with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :ref:`memory types ` :math:`\X{mt}^\ast` as determined below, + * :math:`C.\CEXNS` is :math:`\etexns(\X{it}^\ast)` concatenated with :math:`\X{exnt}^\ast`, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :ref:`exception types ` :math:`\X{exnt}^\ast` as determined below, + * :math:`C.\CGLOBALS` is :math:`\etglobals(\X{it}^\ast)` concatenated with :math:`\X{gt}^\ast`, with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :ref:`global types ` :math:`\X{gt}^\ast` as determined below, @@ -544,6 +612,8 @@ Instead, the context :math:`C` for validation of the module's content is constru * :math:`C'.\CREFS` is the same as :math:`C.\CREFS`, + * :math:`C'.\CEXNS` is the same as :math:`C.\CEXNS`, + * all other fields are empty. * Under the context :math:`C`: @@ -560,6 +630,9 @@ Instead, the context :math:`C` for validation of the module's content is constru * For each :math:`\mem_i` in :math:`\module.\MMEMS`, the definition :math:`\mem_i` must be :ref:`valid ` with a :ref:`memory type ` :math:`\X{mt}_i`. + * For each :math:`\exn_i` in :math:`\module.\MEXNS`, + the definition :math:`\exn_i` must be :ref:`valid ` with an :ref:`exception type ` :math:`\X{exnt}_i`. + * For each :math:`\global_i` in :math:`\module.\MGLOBALS`: * Under the context :math:`C'`, @@ -590,6 +663,8 @@ Instead, the context :math:`C` for validation of the module's content is constru * Let :math:`\X{mt}^\ast` be the concatenation of the internal :ref:`memory types ` :math:`\X{mt}_i`, in index order. +* Let :math:`\X{exnt}^\ast` be the concatenation of the internal :ref:`exception types ` :math:`\X{exnt}_i`, in index order. + * Let :math:`\X{gt}^\ast` be the concatenation of the internal :ref:`global types ` :math:`\X{gt}_i`, in index order. * Let :math:`\X{rt}^\ast` be the concatenation of the :ref:`reference types ` :math:`\X{rt}_i`, in index order. @@ -611,8 +686,10 @@ Instead, the context :math:`C` for validation of the module's content is constru \quad (C \vdashmem \mem : \X{mt})^\ast \quad - (C' \vdashglobal \global : \X{gt})^\ast + (C \vdashexn \exn : \X{exnt})^\ast \\ + (C' \vdashglobal \global : \X{gt})^\ast + \quad (C \vdashelem \elem : \X{rt})^\ast \quad (C \vdashdata \data \ok)^n @@ -620,23 +697,26 @@ Instead, the context :math:`C` for validation of the module's content is constru (C \vdashstart \start \ok)^? \quad (C \vdashimport \import : \X{it})^\ast - \quad - (C \vdashexport \export : \X{et})^\ast \\ + (C \vdashexport \export : \X{et})^\ast + \qquad \X{ift}^\ast = \etfuncs(\X{it}^\ast) \qquad \X{itt}^\ast = \ettables(\X{it}^\ast) \qquad \X{imt}^\ast = \etmems(\X{it}^\ast) + \\ + \X{iet}^\ast = \etexns(\X{it}^\ast) \qquad \X{igt}^\ast = \etglobals(\X{it}^\ast) \\ x^\ast = \freefuncidx(\module \with \MFUNCS = \epsilon \with \MSTART = \epsilon) \\ - C = \{ \CTYPES~\type^\ast, \CFUNCS~\X{ift}^\ast\,\X{ft}^\ast, \CTABLES~\X{itt}^\ast\,\X{tt}^\ast, \CMEMS~\X{imt}^\ast\,\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast\,\X{gt}^\ast, \CELEMS~\X{rt}^\ast, \CDATAS~{\ok}^n, \CREFS~x^\ast \} + C = \{ \CTYPES~\type^\ast, \CFUNCS~\X{ift}^\ast\,\X{ft}^\ast, \CTABLES~\X{itt}^\ast\,\X{tt}^\ast, \CMEMS~\X{imt}^\ast\,\X{mt}^\ast, \CEXNS~\X{iet}^\ast\,\X{exnt}^\ast,\\ + \CGLOBALS~\X{igt}^\ast\,\X{gt}^\ast, \CELEMS~\X{rt}^\ast, \CDATAS~{\ok}^n, \CREFS~x^\ast \} + \\ + C' = \{ \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS), \CEXNS~(C.\CEXNS) \} \qquad \\ - C' = \{ \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \} - \qquad |C.\CMEMS| \leq 1 \qquad (\export.\ENAME)^\ast ~\F{disjoint} @@ -647,6 +727,7 @@ Instead, the context :math:`C` for validation of the module's content is constru \MFUNCS~\func^\ast, \MTABLES~\table^\ast, \MMEMS~\mem^\ast, + \MEXNS~\exn^\ast, \MGLOBALS~\global^\ast, \\ \MELEMS~\elem^\ast, \MDATAS~\data^n, diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 21401456..f6d858a6 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -2,7 +2,7 @@ Types ----- Most :ref:`types ` are universally valid. -However, restrictions apply to :ref:`limits `, which must be checked during validation. +However, restrictions apply to :ref:`exception types ` and to :ref:`limits `, which must be checked during validation. Moreover, :ref:`block types ` are converted to plain :ref:`function types ` for ease of processing. @@ -146,6 +146,31 @@ Memory Types } +.. index:: exception type, function type + pair: validation; exception type + single: abstract syntax; exception type +.. _valid-exntype: + +Exception Types +~~~~~~~~~~~~~~~ + +:math:`[t_1^n] \to [t_2^m]` +........................... + +* The :ref:`function type ` :math:`[t_1^n] \to [t_2^m]` must be :ref:`valid `. + +* The type sequence :math:`t_2^m` must be empty. + +* Then the exception type is valid. + +.. math:: + \frac{ + \vdashfunctype [t^n] \to [] \ok + }{ + \vdashexntype [t^n] \to [] \ok + } + + .. index:: global type, value type, mutability pair: validation; global type single: abstract syntax; global type @@ -216,6 +241,20 @@ External Types \vdashexterntype \ETMEM~\memtype \ok } +:math:`\ETEXN~\exntype` +....................... + +* The :ref:`exception type ` :math:`\exntype` must be :ref:`valid `. + +* Then the external type is valid. + +.. math:: + \frac{ + \vdashexntype \exntype \ok + }{ + \vdashexterntype \ETEXN~\exntype \ok + } + :math:`\ETGLOBAL~\globaltype` ............................. @@ -338,6 +377,23 @@ An :ref:`external type ` :math:`\ETMEM~\limits_1` matches :ma } +.. index:: exception type, value type +.. _match-exntype: + +Exceptions +.......... + +An :ref:`external type ` :math:`\ETEXN~\exntype_1` matches :math:`\ETEXN~\exntype_2` if and only if: + +* Both :math:`\ETEXN~\exntype_1` and :math:`\ETEXN~\exntype_2` are the same. + +.. math:: + \frac{ + }{ + \vdashexterntypematch \ETEXN~\exntype \matchesexterntype \ETEXN~\exntype + } + + .. index:: global type, value type, mutability .. _match-globaltype: diff --git a/proposals/Exceptions.md b/proposals/Exceptions.md index bb6bc512..102f0b39 100644 --- a/proposals/Exceptions.md +++ b/proposals/Exceptions.md @@ -117,21 +117,22 @@ Each event has an `attribute` and a `type`. Currently, the attribute can only specify that the event is an exception. In the future, additional attribute values may be added when other events are added to WebAssembly. -The type of an event is denoted by an index to a function signature defined in -the `type` section. The parameters of the function signature defines the list of -values associated with the exception event. The result type must be 'void'. - -An `event tag` is a value to distinguish different events, while an `event -index` is a numeric name to refer to an (imported or defined) event tag within a -module (see [event index space](#event-index-space) for details). +To allow for such a future extension possibility, we reserve a byte in the binary +format of an exception definition, set to 0 to denote an exception attribute, +but for the moment we won't use the term event in the formal spec. ### Exceptions An `exception` is an internal construct in WebAssembly . WebAssembly exceptions -are defined in the `event` and import sections of a module. Each event (with an -exception attribute) defines an `exception`. The event index is also called the -`exception index`. Similarly, the corresponding event tag is called an -`exception tag`. +are defined in the `exception` and import sections of a module. + +The type of an exception is denoted by an index to a function signature defined in +the `type` section. The parameters of the function signature define the list of +values associated with the exception. The result type must be empty. + +An `exception tag` is a value to distinguish different exceptions, while an `exception +index` is a numeric name to refer to an (imported or defined) exception tag within a +module (see [exception index space](#exception-index-space) for details). Exception indices are used by: @@ -322,9 +323,9 @@ The following rules are added to *instructions*: ``` try blocktype instruction* catch instruction* end | - throw except_index | + throw (exception except_index) | rethrow | - br_on_exn label except_index + br_on_exn label (exception except_index) ``` Like the `block`, `loop`, and `if` instructions, the `try` instruction is @@ -341,18 +342,18 @@ tags. This section describes change in the [Modules document](https://github.com/WebAssembly/design/blob/master/Modules.md). -### Event index space +### Exception index space -The `event index space` indexes all imported and internally-defined events, +The `exception index space` indexes all imported and internally-defined exceptions, assigning monotonically-increasing indices based on the order defined in the -import and event sections. Thus, the index space starts at zero with imported -events, followed by internally-defined events in the [event -section](#event-section). +import and exception sections. Thus, the index space starts at zero with imported +exceptions, followed by internally-defined exceptions in the +[exception section](#exception-section). -The event index space defines the (module) static version of runtime event tags. -For event indices that are not imported/exported, the corresponding event tag is -guaranteed to be unique over all loaded modules. Events that are imported or -exported alias the respective events defined elsewhere, and use the same tag. +The exception index space defines the (module) static version of runtime exception tags. +For exception indices that are not imported/exported, the corresponding exception tag is +guaranteed to be unique over all loaded modules. Exceptions that are imported or +exported alias the respective exceptions defined elsewhere, and use the same tag. ## Changes to the binary model @@ -378,19 +379,19 @@ above. #### Other Types -##### event_type +##### exception_type -The set of event attributes are: +We reserve a bit to denote the exception attribute: | Name | Value | |-----------|-------| | Exception | 0 | -Each event type has the fields: +Each exception type has the fields: | Field | Type | Description | |-------|------|-------------| -| `attribute` | `varuint32` | The attribute of the event. | +| `attribute` | `varuint32` | The attribute of an exception. | | `type` | `varuint32` | The type index for its corresponding type signature | ##### external_kind @@ -406,19 +407,19 @@ or defined: [definition](Modules.md#linear-memory-section) * `3` indicating a `Global` [import](Modules.md#imports) or [definition](Modules.md#global-section) -* `4` indicating an `Event` [import](#import-section) or -[definition](#event-section) +* `4` indicating an `Exception` [import](#import-section) or +[definition](#exception-section) ### Module structure #### High-level structure -A new `event` section is introduced and is named `event`. If included, it must +A new `exception` section is introduced and is named `exception`. If included, it must appear immediately after the memory section. -##### Event section +##### Exception section -The `event` section is the named section 'event'. For ease of validation, this +The `exception` section is the named section 'exception'. For ease of validation, this section comes after the [memory section](https://github.com/WebAssembly/design/blob/master/BinaryEncoding.md#memory-section) and before the [global @@ -432,7 +433,7 @@ So the list of all sections will be: | Function | `3` | Function declarations | | Table | `4` | Indirect function table and other tables | | Memory | `5` | Memory attributes | -| Event | `13` | Event declarations | +| Exception | `13` | Exception declarations | | Global | `6` | Global declarations | | Export | `7` | Exports | | Start | `8` | Start function declaration | @@ -440,34 +441,34 @@ So the list of all sections will be: | Code | `10` | Function bodies (code) | | Data | `11` | Data segments | -The event section declares a list of event types as follows: +The exception section declares a list of exception types as follows: | Field | Type | Description | |-------|------|-------------| -| count | `varuint32` | count of the number of events to follow | -| type | `event_type*` | The definitions of the event types | +| count | `varuint32` | count of the number of exceptions to follow | +| type | `exception_type*` | The definitions of the exception types | ##### Import section -The import section is extended to include event definitions by extending an +The import section is extended to include exception definitions by extending an `import_entry` as follows: -If the `kind` is `Event`: +If the `kind` is `Exception`: | Field | Type | Description | |-------|------|-------------| -| `type` | `event_type` | the event being imported | +| `type` | `exception_type` | the exception being imported | ##### Export section -The export section is extended to reference event types by extending an +The export section is extended to reference exception types by extending an `export_entry` as follows: -If the `kind` is `Event`: +If the `kind` is `Exception`: | Field | Type | Description | |-------|------|-------------| -| `index` | `varuint32` | the index into the corresponding event index space | +| `index` | `varuint32` | the index into the corresponding exception index space | ##### Name section @@ -478,12 +479,12 @@ follows: | --------- | ---- | ----------- | | [Function](#function-names) | `1` | Assigns names to functions | | [Local](#local-names) | `2` | Assigns names to locals in functions | -| [Event](#event-names) | `3` | Assigns names to event types | +| [Exception](#exception-names) | `3` | Assigns names to exception types | -###### Event names +###### Exception names -The event names subsection is a `name_map` which assigns names to a subset of -the event indices (Used for both imports and module-defined). +The exception names subsection is a `name_map` which assigns names to a subset of +the exception indices (Used for both imports and module-defined). ### Control flow operators