From 66ad44a1efe3895a8063c837ada1136311ac1809 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 17 Jun 2020 18:30:20 +0200 Subject: [PATCH] Current core formal spec for the WebAssembly Exception Handling Proposal. This adds the [informal formal core spec](https://github.com/WebAssembly/exception-handling/issues/87#issuecomment-517216137) laid out by Andreas Rossberg, and the core spec outlined in the [proposal overview](https://github.com/WebAssembly/exception-handling/blob/master/proposals/Exceptions.md). I have aimed for this to be as complete as possible for the above "informal formal spec" and proposal overview, meaning I added prose for all the relevant parts in syntax, validation, execution, binary format, text format, and the appendix, as well as an example for throw contexts. --- document/core/appendix/algorithm.rst | 13 +- document/core/appendix/embedding.rst | 24 ++- document/core/appendix/implementation.rst | 2 + document/core/appendix/index-instructions.rst | 10 +- document/core/appendix/index-rules.rst | 4 + document/core/appendix/index-types.rst | 4 +- document/core/appendix/properties.rst | 150 +++++++++++++++--- document/core/binary/instructions.rst | 14 +- document/core/binary/modules.rst | 44 ++++- document/core/binary/types.rst | 28 +++- document/core/exec/instructions.rst | 115 ++++++++++++++ document/core/exec/modules.rst | 130 ++++++++++++--- document/core/exec/runtime.rst | 135 ++++++++++++++-- document/core/index.rst | 2 +- document/core/syntax/instructions.rst | 18 ++- document/core/syntax/modules.rst | 62 ++++++-- document/core/syntax/types.rst | 36 ++++- document/core/text/conventions.rst | 1 + document/core/text/instructions.rst | 23 ++- document/core/text/modules.rst | 80 +++++++++- document/core/text/types.rst | 21 ++- document/core/util/macros.def | 56 ++++++- document/core/valid/conventions.rst | 4 +- document/core/valid/instructions.rst | 107 ++++++++++++- document/core/valid/modules.rst | 95 ++++++++++- document/core/valid/types.rst | 58 ++++++- 26 files changed, 1113 insertions(+), 123 deletions(-) diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index be20a5358..615b24688 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 | Externref | Exnref 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 = Externref || t = Exnref 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 db83ae26b..1f9853e71 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, ~\SEVENTS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\ \end{array} @@ -539,6 +539,28 @@ Memories \end{array} +.. index: event, event address, store, event instance, event type, exception attribute, function type +.. _embed-event: + +Events +~~~~~~ + +.. _embedd-event-alloc: + +:math:`\F{event\_alloc}(\store, \eventtype) : (\store, \eventaddr)` +................................................................... + +1. Pre-condition: :math:`eventtype` is :ref:`valid `. + +2. Let :math:`\eventaddr` be the result of :ref:`allocating an event ` in :math:`\store` with :ref:`event type ` :math:`\eventtype`. + +3. Return the new store paired with :math:`\eventaddr`. + +.. math:: + \begin{array}{lclll} + \F{event\_alloc}(S, \X{et}) &=& (S', \X{a}) && (\iff \allocevent(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 d5e53920f..556643c0b 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:`events ` 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:`event 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 694b47d02..a12a2d5ed 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 dde34900e..249566057 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:`Event type ` :math:`\vdasheventtype \eventtype \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:`Event ` :math:`C \vdashevent \event : \eventtype` :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:`Event instance ` :math:`S \vdasheventinst \eventinst : \eventtype` :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:`Event instance ` :math:`\vdasheventinstextends \eventinst_1 \extendsto \eventinst_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 413e6f0b0..0b05b3c14 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{6E}` (-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:`Event type ` :math:`\EXCEPTION~\functype` (none) :ref:`Global type ` :math:`\mut~\valtype` (none) ======================================== =========================================== =============================================================================== diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 30cb620c9..0dfe8e0f2 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:`event `, :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:`event `, 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, event instance, global instance, function type, table type, memory type, event 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:`event instance ` :math:`\eventinst_i` in :math:`S.\SEVENTS` must be :ref:`valid ` with some :ref:`event type ` :math:`\eventtype_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 \vdasheventinst \eventinst : \eventtype)^\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, + \SEVENTS~\eventinst^\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:: event type, event instance, exception tag, function type +.. _valid-eventinst: + +:ref:`Event Instances ` :math:`\{ \EVIATTRIBUTE~\EXCEPTION, \EVITYPE~\functype \}` +.................................................................................................... + +* The :ref:`event type ` :math:`\EXCEPTION~\functype` must be :ref:`valid `. + +* Then the event instance is valid with :ref:`event type ` :math:`\EXCEPTION~\functype`. + +.. math:: + \frac{ + \vdasheventtype \EXCEPTION~\functype \ok + }{ + S \vdasheventinst \{ \EVIATTRIBUTE~\EXCEPTION, \EVITYPE~\functype \} : \EXCEPTION~\functype + } + + .. index:: global type, global instance, value, mutability .. _valid-globalinst: @@ -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:`event address ` :math:`\eventaddr_i` in :math:`\moduleinst.\MIEVENTS`, the :ref:`external value ` :math:`\EVEVENT~\eventaddr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETEVENT~\eventtype_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:`\eventtype^\ast` be the concatenation of all :math:`\eventtype_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,` :math:`\CTABLES~\tabletype^\ast, \CMEMS~\memtype^\ast, \CEVENTS~\eventtype^\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 \EVEVENT~\eventaddr : \ETEVENT~\eventtype)^\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, \\ + \MIEVENTS & \eventaddr^\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, \\ + \CEVENTS & \eventtype^\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:: event address, event type, function type, value type, exception attribute, exception tag + +:math:`\EXNREFADDR~\eventaddr~\val^\ast` +........................................ + +* The :ref:`external event value ` :math:`\EVEVENT~\eventaddr` must be :ref:`valid ` with :ref:`external event type ` :math:`\ETEVENT~\EXCEPTION~[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 \EVEVENT~\eventaddr : \ETEVENT~\EXCEPTION~[t^\ast]\to[] + \qquad + (S \vdashval \val : t)^\ast + }{ + S; C \vdashadmininstr \EXNREFADDR~\eventaddr~\val^\ast : [] \to [\EXNREF] + } + + +.. index:: throw, throw context, event address, exception tag + +:math:`\THROWADDR~\eventaddr` +............................. + +* The :ref:`external event value ` :math:`\EVEVENT~\eventaddr` must be :ref:`valid ` with :ref:`external event type ` :math:`\ETEVENT~\EXCEPTION~[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 \EVEVENT~\eventaddr : \ETEVENT~\EXCEPTION~[t^\ast]\to[] + }{ + S; C \vdashadmininstr \THROWADDR~\eventaddr : [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 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:`[\EXNREF]` 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\,[\EXNREF] \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.\SEVENTS` 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:`event instance ` :math:`\eventinst_i` in the original :math:`S.\SEVENTS`, the new event 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.\SEVENTS = \eventinst_1^\ast & + S_2.\SEVENTS = {\eventinst'_1}^\ast~\eventinst_2^\ast & + (\vdasheventinstextends \eventinst_1 \extendsto \eventinst'_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:: event instance +.. _extend-eventinst: + +:ref:`Event Instance ` :math:`\eventinst` +........................................................... + +* An event instance must remain unchanged. + +.. math:: + \frac{ + }{ + \vdasheventinstextends \eventinst \extendsto \eventinst + } + + .. index:: global instance, value, mutability .. _extend-globalinst: diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 23ee48897..39347e19a 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}~~ev{:}\Beventidx &\Rightarrow& \THROW~ev \\ &&|& + \hex{09} &\Rightarrow& \RETHROW \\ &&|& + \hex{0A}~~l{:}\Blabelidx~~ev{:}\Beventidx &\Rightarrow& \BRONEXN~l~ev \\ &&|& \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 8ff6e9d8b..62ed9d495 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, event 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; event 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-eventidx: .. _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{event index} & \Beventidx &::=& 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:`event 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, event 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{ev}{:}\Bevent &\Rightarrow& \IDEVENT~\X{ev} \\ \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, event 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{:}\Beventidx &\Rightarrow& \EDEVENT~x \\ \end{array} @@ -476,7 +482,30 @@ 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:: ! event section, event, event type, attribute, function type index + pair: binary format; event + pair: section; event +.. _binary-event: +.. _binary-eventsec: + +Event Section +~~~~~~~~~~~~~~ + +The *event section* has the id 13. +It decodes into a vector of :ref:`events ` that represent the |MEVENTS| +component of a :ref:`module `. + +.. math:: + \begin{array}{llclll} + \production{event section} & \Beventsec &::=& + \X{event}^\ast{:}\Bsection_{13}(\Bvec(\Bevent)) &\Rightarrow& \X{event}^\ast \\ + \production{event} & \Bevent &::=& + \X{a}{:}\Battribute~~\X{x}{:}\Btypeidx + &\Rightarrow& \{ \EVATTRIBUTE~\X{a}, \EVTYPE~\X{x} \} \\ + \end{array} + + +.. index:: module, section, type definition, function type, function, table, memory, event, global, element, data, start function, import, export, context, version pair: binary format; module .. _binary-magic: .. _binary-version: @@ -518,6 +547,8 @@ Furthermore, it must be present if any :math:`data index ` occur \Bcustomsec^\ast \\ &&& \mem^\ast{:\,}\Bmemsec \\ &&& \Bcustomsec^\ast \\ &&& + \event^\ast{:\,}\Beventsec \\ &&& + \Bcustomsec^\ast \\ &&& \global^\ast{:\,}\Bglobalsec \\ &&& \Bcustomsec^\ast \\ &&& \export^\ast{:\,}\Bexportsec \\ &&& @@ -538,6 +569,7 @@ Furthermore, it must be present if any :math:`data index ` occur \MFUNCS~\func^n, \\ \MTABLES~\table^\ast, \\ \MMEMS~\mem^\ast, \\ + \MEVENTS~\event^\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 7c462e029..6ffe1927b 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -42,7 +42,8 @@ Reference Types \begin{array}{llclll@{\qquad\qquad}l} \production{reference type} & \Breftype &::=& \hex{70} &\Rightarrow& \FUNCREF \\ &&|& - \hex{6F} &\Rightarrow& \EXTERNREF \\ + \hex{6F} &\Rightarrow& \EXTERNREF \\ &&|& + \hex{68} &\Rightarrow& \EXNREF \\ \end{array} @@ -168,3 +169,28 @@ Global Types \hex{00} &\Rightarrow& \MCONST \\ &&|& \hex{01} &\Rightarrow& \MVAR \\ \end{array} + + +.. index:: event type, exception attribute, function type + pair: binary format; event type + pair: binary format; attribute +.. _binary-attribute: +.. _binary-eventtype: + +Event Types +~~~~~~~~~~~ + +:ref:`Event types ` are encoded as function types with a preceding flag indicating their :ref:`attribute `. + +.. math:: + \begin{array}{llclll} + \production{event type} & \Beventtype &::=& + a{:}\Battribute~~ft{:}\Bfunctype &\Rightarrow& a~ft \\ + \production{attribute} & \Battribute &::=& + \hex{00} &\Rightarrow& \EXCEPTION \\ + \end{array} + +|EXCEPTION| is the |attribute| of an exception, whose function type must have void result. + +.. note:: + Currently events can only be exceptions. diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 20822a28a..23eff1bc2 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. + +4. Execute the :math:`\CATCHN_m` administrative instruction, depending on the outcome of + :ref:`entering ` the block :math:`\instr_1^\ast` with label :math:`L`, + using the :ref:`throw context ` rules. + +.. 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_1 \{\}~\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.\MIEVENTS[x]` exists. + +3. Let :math:`a` be the :ref:`event address ` :math:`F.\AMODULE.\MIEVENTS[x]`. + +4. :ref:`Throw ` the :ref:`event address ` :math:`a`. + +.. math:: + ~\\[-1ex] + \begin{array}{lclr@{\qquad}l} + \THROW~x &\stepto& \THROWADDR~a & (\iff F.\AMODULE.\MIEVENTS[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. Else the :math:`\EXNREF` value is of the form :math:`(\EXNREFADDR~a~\val^\ast)`. + +5. Put the values :math:`\val^\ast` on the stack. + +6. :ref:`Throw ` the :ref:`event address ` :math:`a`. + +.. math:: + ~\\[-1ex] + \begin{array}{lclr@{\qquad}} + (\REFNULL~\EXNREF)~\RETHROW &\stepto& \TRAP \\ + (\EXNREFADDR~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. Else the :math:`\EXNREF` value is of the form :math:`(\EXNREFADDR~a~\val^\ast)`. + +5. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIEVENTS[x]` exists. + +7. If :math:`F.\AMODULE.\MIEVENTS[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:`(\EXNREFADDR~a~\val^\ast)` back on the stack. + +.. math:: + ~\\[-1ex] + \begin{array}{lclr@{\qquad}l} + F; (\REFNULL~\EXNREF)~\BRONEXN~l~x &\stepto& F; \TRAP \\ + F; (\EXNREFADDR~a~\val^\ast)~\BRONEXN~l~x &\stepto& F; \val^\ast~(\BR~l) & (\iff F.\AMODULE.\MIEVENTS[x] = a) \\ + F; (\EXNREFADDR~a~\val^\ast)~\BRONEXN~l~x &\stepto& F; (\EXNREFADDR~a~\val^\ast) & (\iff F.\AMODULE.\MIEVENTS[x] \neq a) \\ + \end{array} + + .. _exec-br: :math:`\BR~l` diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 35df503de..698ed8bad 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:: event type, event address, exception tag, function type, event attribute +.. _valid-externval-event: + +:math:`\EVEVENT~a` +................... + +* The store entry :math:`S.\SEVENTS[a]` must exist. + +* Let :math:`\functype` be the function type :math:`S.\SEVENTS[a].\EVITYPE`. + +* Then :math:`\EVEVENT~a` is valid with :ref:`external type ` :math:`\ETEVENT~S.\SEVENTS[a].\EVIATTRIBUTE~\functype`. + +.. math:: + \frac{ + }{ + S \vdashexternval \EVEVENT~a : \ETEVENT~(S.\SEVENTS[a].\EVIATTRIBUTE)~(S.\SEVENTS[a].\EVITYPE) + } + + + .. 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:`\EXNREFADDR~a~\val^n` +............................................................................ + +* The external value :math:`\EVEVENT~a` must be valid with :ref:`event type ` :math:`\EXCEPTION~[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 \EVEVENT~a : \EXCEPTION~[t^n]\to[] + \qquad + (S \vdashval \val : t)^n + }{ + S \vdashval \EXNREFADDR~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:`events `, 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,34 @@ New instances of :ref:`functions `, :ref:`tables ` +................................ + +1. Let :math:`\event` be the :ref:`event ` to allocate for the module :math:`\module`. + +2. Let :math:`a` be the first free :ref:`event address ` in :math:`S`. + +3. Let :math:`\functype` be the :ref:`function type ` :math:`\module.\MTYPES[\event.\EVTYPE]`. + +4. Let :math:`\eventinst` be the :ref:`event instance ` :math:`\{ \EVIATTRIBUTE~\event.\EVATTRIBUTE, \EVITYPE~\functype \}`. + +5. Append :math:`\eventinst` to the |SEVENTS| of :math:`S`. + +5. Return :math:`a`. + +.. math:: + \begin{array}{rlll} + \allocevent(S, \event, \module) &=& S', \eventaddr \\[1ex] + \mbox{where:} \hfill \\ + \eventaddr &=& |S.\SEVENTS| \\ + \eventinst &=& \{ \EVIATTRIBUTE~\event.\EVATTRIBUTE, \EVITYPE~\functype \} \\ + S' &=& S \compose \{\SEVENTS~\eventinst\} \\ + \end{array} + + .. index:: global, global instance, global address, global type, value type, mutability, value .. _alloc-global: @@ -429,7 +496,7 @@ Growing :ref:`memories ` \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, event instance, global instance, export instance, function address, table address, memory address, event address, global address, function index, table index, memory index, event index, global index, type, function, table, memory, event, global, import, export, external value, external type, matching .. _alloc-module: :ref:`Modules ` @@ -456,39 +523,47 @@ 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:`event ` :math:`\event_i` in :math:`\module.\MEVENTS`, do: + + a. Let :math:`\eventaddr_i` be the :ref:`event address ` resulting from :ref:`allocating ` :math:`\event_i` for the module :math:`\module`. + +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]`. -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:`\eventaddr^\ast` be the concatenation of the :ref:`event addresses ` :math:`\eventaddr_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:`\eventaddr_{\F{mod}}^\ast` be the list of :ref:`event addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\eventaddr^\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 event export for :ref:`event index ` :math:`x`, then let :math:`\externval_i` be the :ref:`external value ` :math:`\EVEVENT~(\eventaddr_{\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:`\MIEVENTS~\eventaddr_{\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, \\ + \MIEVENTS~\evevents(\externval_{\F{im}}^\ast)~\eventaddr^\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, \eventaddr^\ast &=& \allocevent^\ast(S_3, \event^\ast, \module) + \qquad\quad~ (\where \event^\ast = \module.\MEVENTS) \\ + 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.\ETYPE)^\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)) \\ + \evevents(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIEVENTS[x])^\ast + \qquad\!\!\! (\where x^\ast = \edevents(\module.\MEXPORTS)) \\ \evglobals(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIGLOBALS[x])^\ast \qquad\!\!\! (\where x^\ast = \edglobals(\module.\MEXPORTS)) \\ \end{array} diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 43c66efe2..9a937e378 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, ! event 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* pointing to a specific :ref:`event address ` (sometimes referred to as the exception tag) 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,11 +38,15 @@ or *external references* pointing to an uninterpreted form of :ref:`extern addre \production{(reference)} & \reff &::=& \REFNULL~t \\&&|& \REFFUNCADDR~\funcaddr \\&&|& - \REFEXTERNADDR~\externaddr \\ + \REFEXTERNADDR~\externaddr \\&&|& + \EXNREFADDR~\eventaddr~\val^\ast \\ \production{(value)} & \val &::=& \num ~|~ \reff \\ \end{array} +The administrative value |EXNREFADDR| is an exception reference of type |EXNREF|, representing a thrown exception on the stack, identified by the exception's :ref:`event address `, and carrying the exception event's arguments. +If it is uncaught by a |CATCHN| block, then the embedder defines how to handle it. It is an abstract value, and it is an implementation detail how and where its argument values are stored. It is separate from any linear memory. + .. note:: Future versions of WebAssembly may add additional forms of reference. @@ -84,7 +89,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:`events `, 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 +111,7 @@ Syntactically, the store is defined as a :ref:`record ` listing \SFUNCS & \funcinst^\ast, \\ \STABLES & \tableinst^\ast, \\ \SMEMS & \meminst^\ast, \\ + \SEVENTS & \eventinst^\ast, \\ \SGLOBALS & \globalinst^\ast, \\ \SELEMS & \eleminst^\ast, \\ \SDATAS & \datainst^\ast ~\} \\ @@ -124,10 +130,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, event 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; event address pair: abstract syntax; global address pair: abstract syntax; element address pair: abstract syntax; data address @@ -135,6 +142,7 @@ Convention pair: function; address pair: table; address pair: memory; address + pair: event; address pair: global; address pair: element; address pair: data; address @@ -142,6 +150,7 @@ Convention .. _syntax-funcaddr: .. _syntax-tableaddr: .. _syntax-memaddr: +.. _syntax-eventaddr: .. _syntax-globaladdr: .. _syntax-elemaddr: .. _syntax-dataaddr: @@ -151,7 +160,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:`event 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 +174,8 @@ In addition, an :ref:`embedder ` may supply an uninterpreted set of *h \addr \\ \production{(memory address)} & \memaddr &::=& \addr \\ + \production{(event address)} & \eventaddr &::=& + \addr \\ \production{(global address)} & \globaladdr &::=& \addr \\ \production{(element address)} & \elemaddr &::=& @@ -190,7 +201,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, event, instance, global instance, element instance, data instance, export instance, table address, memory address, event address, global address, element address, data address, index, name pair: abstract syntax; module instance pair: module; instance .. _syntax-moduleinst: @@ -210,6 +221,7 @@ and collects runtime representations of all entities that are imported, defined, \MIFUNCS & \funcaddr^\ast, \\ \MITABLES & \tableaddr^\ast, \\ \MIMEMS & \memaddr^\ast, \\ + \MIEVENTS & \eventaddr^\ast, \\ \MIGLOBALS & \globaladdr^\ast, \\ \MIELEMS & \elemaddr^\ast, \\ \MIDATAS & \dataaddr^\ast, \\ @@ -218,7 +230,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:`event 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 +315,31 @@ 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:: ! event instance, event, exception attribute, exception tag + pair: abstract syntax; event instance + pair: event; instance +.. _syntax-eventinst: + +Event Instances +~~~~~~~~~~~~~~~ + +An *event instance* is the runtime representation of an :ref:`event `. +It records the :ref:`attribute ` and :ref:`function type ` of its :ref:`type `. + +.. math:: + \begin{array}{llll} + \production{(event instance)} & \eventinst &::=& + \{ \EVIATTRIBUTE~\EXCEPTION, \EVITYPE~\functype \} \\ + \end{array} + +Because :ref:`events ` :ref:`have type ` |eventtype|, it is an invariant of the semantics that the function type :math:`\functype` has void result type. + +.. note:: + In the current version of WebAssembly, events may only be exceptions. This may change in future versions. + + The event address of an event instance is also called an exception tag. + + .. index:: ! global instance, global, value, mutability, instruction, embedder pair: abstract syntax; global instance pair: global; instance @@ -379,7 +416,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, event address, global address, store, function, table, memory, event, global pair: abstract syntax; external value pair: external; value .. _syntax-externval: @@ -388,7 +425,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:`event instances ` in the shared :ref:`store `. .. math:: \begin{array}{llcl} @@ -396,6 +433,7 @@ It is an :ref:`address ` denoting either a :ref:`function instance \EVFUNC~\funcaddr \\&&|& \EVTABLE~\tableaddr \\&&|& \EVMEM~\memaddr \\&&|& + \EVEVENT~\eventaddr \\&&|& \EVGLOBAL~\globaladdr \\ \end{array} @@ -412,9 +450,12 @@ It filters out entries of a specific kind in an order-preserving fashion: * :math:`\evmems(\externval^\ast) = [\memaddr ~|~ (\EVMEM~\memaddr) \in \externval^\ast]` +* :math:`\evevents(\externval^\ast) = [\eventaddr ~|~ (\EVEVENT~\eventaddr) \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 pair: abstract syntax; frame pair: abstract syntax; label @@ -510,11 +551,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, event, event instance, event address, exception, reftype pair:: abstract syntax; administrative instruction .. _syntax-trap: .. _syntax-reffuncaddr: .. _syntax-invoke: +.. _syntax-exnrefaddr: +.. _syntax-throwaddr: +.. _syntax-catchn: .. _syntax-instr-admin: Administrative Instructions @@ -523,7 +567,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 events `, and :ref:`control instructions `, the syntax of instructions is extended to include the following *administrative instructions*: .. math:: \begin{array}{llcl} @@ -533,6 +577,9 @@ In order to express the reduction of :ref:`traps `, :ref:`calls `, :ref:`calls `. Similarly, |REFEXTERNADDR| represents :ref:`external references `. +The |REFFUNCADDR| instruction represents :ref:`function reference values `. Similarly, |REFEXTERNADDR| represents :ref:`external references `, +, and |EXNREFADDR| represents :ref:`exception reference values ` of thrown exception events. 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:`event instance `, identified by its :ref:`address `. +The values it will consume to create the exception depend on the event's :ref:`event type `. +It unifies the throwing of different forms of events. + +The |LABEL|, |FRAME|, and |CATCHN| instructions model :ref:`labels `, :ref:`frames `, and :ref:`try-catch blocks ` 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 +660,59 @@ 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, event, exception, throw address, catch block +.. _syntax-ctxt-throw: + +Throw Contexts +.............. + +In order to specify the reduction of :ref:`try-catch blocks ` +with the help of the administrative instructions |THROWADDR|, |EXNREFADDR|, 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} + +.. math:: + \begin{array}{rcl} + S;~F;~\CATCHN_m~\{\instr^\ast\}~\val^m~\END &\stepto& S;~F;~\val^m \\ + S;~F;~\CATCHN_m~\{\instr^\ast\}~\XT[\val^n~[\_]~(\THROWADDR~a)]~\END &\stepto& + S;~F;~\LABEL_m~\{\}~(\EXNREFADDR~a~\val^n)~{\instr}^\ast~\END \\ + && \hspace{-12ex} (\iff S.\SEVENTS[a]=\{\EVATTRIBUTE~\EXCEPTION, \EVTYPE~[t^n]\to[]\}) \\ + \end{array} + +This definition allows to potentially capture the throw of an exception from surrounding catch blocks in the body of +a calling function. + +.. note:: + For example, catching a simple :ref:`throw ` in a :ref:`try-catch block ` would be as follows. + + Let :math:`x` be the :ref:`event index ` of an event with :ref:`event instance ` \ :math:`\{ \EVIATTRIBUTE~\EXCEPTION, \EVITYPE~[t^n]\to[]\}`, + let :math:`\expand_F(\X{bt}) = [t^n] \to [\EXNREF]`, and consider arbitrary :ref:`values ` :math:`(val : t)^n`. + + .. 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} + + Reducing :math:`\CATCHN` for the throw context :math:`T[\val^n~\THROWADDR~a]`, where :math:`T=\LABEL_1 \{\}[\_]~\END` gives: + + .. math:: + \begin{array}{lll} + \stepto & S;~F;~\LABEL_1~\{\}~(\EXNREFADDR~a~\val^n)~\RETURN~\END & \hspace{9ex}\ \\ + \stepto & (\EXNREFADDR~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. + + .. index:: ! configuration, ! thread, store, frame, instruction, module instruction .. _syntax-thread: .. _syntax-config: @@ -663,6 +768,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~\eventaddr`, 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 139a05b04..9d4d71afd 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 85c641f01..2769ba4e7 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, event index, vector, trap, function, table, event, function type, value type, type index, event 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~\eventidx \\&&|& + \RETHROW \\&&|& + \BRONEXN~\labelidx~\eventidx \\&&|& \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 events, and in particular with handling exception events. +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 event 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 f0973d814..f8f48add8 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, event type, function, table, memory, event, 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:`events `, 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), \\&&&& + \MEVENTS~\vec(\event), \\&&&& \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, ! event index, ! global index, ! local index, ! label index, ! element index, ! data index, function, global, table, memory, event, 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; event 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: event; 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-eventidx: .. _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{event index} & \eventidx &::=& \u32 \\ \production{global index} & \globalidx &::=& \u32 \\ \production{element index} & \elemidx &::=& \u32 \\ \production{data index} & \dataidx &::=& \u32 \\ @@ -78,9 +83,11 @@ 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:`events `, 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. +Event indices are at the moment only indices for exception :ref:`events `. + Element indices reference :ref:`element segments ` and data indices reference :ref:`data segments `. The index space for :ref:`locals ` is only accessible inside a :ref:`function ` and includes the parameters of that function, which precede the local variables. @@ -92,6 +99,7 @@ Label indices reference :ref:`structured control instructions `. +The |MTYPES| component of a module defines a vector of :ref:`function types `, +which may also be part of an :ref:`event type `. -All function types used in a module must be defined in this component. +All function types and all event function types used in a module must be defined in this component. They are referenced by :ref:`type indices `. .. note:: @@ -219,6 +228,32 @@ Most constructs implicitly reference memory index :math:`0`. This restriction may be lifted in future versions. + +.. index:: ! event, exception, table index, function index, event type + pair: abstract syntax; event + pair: abstract syntax; exception +.. _syntax-event: + +Events +~~~~~~ + +The |MEVENTS| component of a module defines a vector of *events* with the following structure. + +.. math:: + \begin{array}{llll} + \production{event} & \event &::=& \{ \EVATTRIBUTE~\EXCEPTION, \EVTYPE~\typeidx \} \\ + \end{array} + +The event's :ref:`attribute ` may only specify the attribute |EXCEPTION|, meaning that the event is an exception. +In this case, the result type of the function signature with type index :math:`\typeidx` must be void. + +Events are referenced through :ref:`event indices `, +starting with the smallest index not referencing an event :ref:`import `. + +.. note:: + In the current version of WebAssembly, events may only be exceptions. In future versions additional events may be added. + + .. index:: ! global, global index, global type, mutability, expression, constant, value, import pair: abstract syntax; global .. _syntax-global: @@ -337,7 +372,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:`events `, and :ref:`globals `, which are referenced through a respective descriptor. @@ -378,15 +414,18 @@ The following auxiliary notation is defined for sequences of exports, filtering * :math:`\edmems(\export^\ast) = [\memidx ~|~ \EDMEM~\memidx \in (\export.\EDESC)^\ast]` +* :math:`\edevents(\export^\ast) = [\eventidx ~|~ \EDEVENT~\eventidx \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, event, index, index space, type index, function index, table index, memory index, global index, event index, function, table, memory, event, global, instantiation pair: abstract syntax; import single: function; import single: table; import single: memory; import single: global; import + single: event; import .. _syntax-importdesc: .. _syntax-import: @@ -403,11 +442,12 @@ The |MIMPORTS| component of a module defines a set of *imports* that are require \IDFUNC~\typeidx \\&&|& \IDTABLE~\tabletype \\&&|& \IDMEM~\memtype \\&&|& + \IDEVENT~\event \\&&|& \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:`events `, 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 5a6c3d92b..904533c6a 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,13 +54,15 @@ Reference Types .. math:: \begin{array}{llll} \production{reference type} & \reftype &::=& - \FUNCREF ~|~ \EXTERNREF \\ + \FUNCREF ~|~ \EXTERNREF ~|~ \EXNREF \\ \end{array} The type |FUNCREF| denotes the infinite union of all references to :ref:`functions `, regardless of their :ref:`function types `. 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. +The type |EXNREF| denotes the infinite union of all references to exception :ref:`events `, regardless of their :ref:`event types `. + Reference types are *opaque*, meaning that neither their size nor their bit pattern can be observed. Values of reference type can be stored in :ref:`tables `. @@ -190,6 +192,33 @@ The limits are given in numbers of entries. In future versions of WebAssembly, additional element types may be introduced. +.. index:: ! event, exception, event type, attribute + pair: abstract syntax; event + pair: abstract syntax; exception + single: event; type + single: event; attribute +.. _syntax-attribute: +.. _syntax-eventtype: + +Event Types +~~~~~~~~~~~ + +*Event types* classify the signature of :ref:`events `, +with an attribute and a function type. + +.. math:: + \begin{array}{llll} + \production{event type} &\eventtype &::=& \attribute~~\functype \\ + \production{attribute} &\attribute &::=& \EXCEPTION \\ + \end{array} + +The |attribute| |EXCEPTION| specifies that the event is an exception, in which case the result type of its function type |functype| must be void. +The parameters of |functype| define the list of values associated with the exception event. + + +.. note:: In the current version of WebAssembly, events may only be exceptions. In future versions additional events may be added. + + .. index:: ! global type, ! mutability, value type, global, mutability pair: abstract syntax; global type pair: abstract syntax; mutability @@ -229,6 +258,7 @@ External Types \ETFUNC~\functype ~|~ \ETTABLE~\tabletype ~|~ \ETMEM~\memtype ~|~ + \ETEVENT~\eventtype ~|~ \ETGLOBAL~\globaltype \\ \end{array} @@ -245,4 +275,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:`\etevents(\externtype^\ast) = [\eventtype ~|~ (\ETEVENT~\eventtype) \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 ea62cc4b7..63515f0f3 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}~~x{:}\Teventidx_I &\Rightarrow& \THROW~x \\ &&|& + \text{rethrow} &\Rightarrow& \RETHROW \\ &&|& + \text{br\_on\_exn}~~l{:}\Tlabelidx_I~~x{:}\Teventidx_I &\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~~\Tinstr_1^\ast + &\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 9ae3b2d11..73870fdf1 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, event 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; event 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-eventidx: .. _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{event index} & \Teventidx_I &::=& + x{:}\Tu32 &\Rightarrow& x \\&&|& + v{:}\Tid &\Rightarrow& x & (\iff I.\IEVENTS[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, event 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, event, 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{event}~~\Tid^?~~\X{ev}{:}\Tevent~\text{)} + &\Rightarrow& \IDEVENT~\X{ev} \\ &&|& \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:`event ` or :ref:`global ` definitions; see the respective sections. @@ -380,6 +387,56 @@ Memories can be defined as :ref:`imports ` or :ref:`exports `. + +.. math:: + \begin{array}{llcl} + \production{event} & \Tevent_I &::=& + \text{(}~\text{exception}~~\Tid^?~~x,I'{:}\Ttypeuse_I~\text{)} \\ &&& \qquad + \Rightarrow\quad \{ \EVATTRIBUTE~\EXCEPTION, \EVTYPE~x \} \\ + \end{array} + +.. note:: + The syntax for events just covers the only possible event attribute, that of an exception. + In future versions of WebAssembly, more events may be added, and the above syntax + may become an abbreviation. + + +.. index:: import, name + pair: text format; import +.. index:: export, name, index, event index + pair: text format; export +.. index:: exception +.. _text-event-abbrev: + +Abbreviations +............. + +Events 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{)}~~\Teventtype~\text{)} \quad\equiv \\ & \qquad + \text{(}~\text{import}~~\Tname_1~~\Tname_2~~\text{(}~\text{exception}~~\Tid^?~~\Teventtype~\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 +481,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{event}~~x{:}\Teventidx_I~\text{)} + &\Rightarrow& \EDEVENT~x \\&&|& \text{(}~\text{global}~~x{:}\Tglobalidx_I~\text{)} &\Rightarrow& \EDGLOBAL~x \\ \end{array} @@ -454,7 +513,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:`event ` definitions, or :ref:`global ` definitions; see the respective sections. .. index:: start function, function index @@ -644,6 +703,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{ev}{:}\Tevent_I &\Rightarrow& \{\MEVENTS~\X{ev}\} \\ |& \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 +716,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:`event `, 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 +737,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{event}~\Tid^?~\dots~\text{)}) &=& + \{\IEVENTS~(\Tid^?)\} \\ \F{idc}(\text{(}~\text{global}~\Tid^?~\dots~\text{)}) &=& \{\IGLOBALS~(\Tid^?)\} \\ \F{idc}(\text{(}~\text{elem}~\Tid^?~\dots~\text{)}) &=& @@ -689,6 +751,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{event}~\Tid^?~\dots~\text{)}~\text{)}) &=& + \{\IEVENTS~(\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 bfeb2b82b..d7fa19033 100644 --- a/document/core/text/types.rst +++ b/document/core/text/types.rst @@ -34,10 +34,12 @@ Reference Types \begin{array}{llcll@{\qquad\qquad}l} \production{reference type} & \Treftype &::=& \text{funcref} &\Rightarrow& \FUNCREF \\ &&|& - \text{externref} &\Rightarrow& \EXTERNREF \\ + \text{externref} &\Rightarrow& \EXTERNREF \\ &&|& + \text{exnref} &\Rightarrow& \EXNREF \\ \production{referenced type} & \Trefedtype &::=& \text{func} &\Rightarrow& \FUNCREF \\ &&|& - \text{extern} &\Rightarrow& \EXTERNREF \\ + \text{extern} &\Rightarrow& \EXTERNREF \\ &&|& + \text{event} &\Rightarrow& \EXNREF \\ \end{array} @@ -138,6 +140,21 @@ Table Types \end{array} +.. index:: event type, exception attribute, exception, function type + pair: text format; event type + pair: text format; exception attribute +.. _text-eventtype: + +Event Types +~~~~~~~~~~~ + +.. math:: + \begin{array}{llclll} + \production{event type} & \Teventtype &::=& + \text{(}~\text{exception}~~t^\ast{:}\Tvec(\Tparam)~\text{)} &\Rightarrow& \EXCEPTION~~[t^\ast] \to [] \\ + \end{array} + + .. index:: global type, mutability, value type pair: text format; global type pair: text format; mutability diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 360b9d84c..3a57a0f53 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,7 +191,9 @@ .. |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}} +.. |ETEVENT| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{event}} +.. |EXCEPTION| mathdef:: \xref{syntax/types}{syntax-eventtype}{\K{exception}} .. Types, non-terminals @@ -199,6 +202,8 @@ .. |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}} +.. |eventtype| mathdef:: \xref{syntax/types}{syntax-eventtype}{\X{eventtype}} +.. |attribute| mathdef:: \xref{syntax/types}{syntax-eventtype}{\X{attribute}} .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}} .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}} @@ -216,6 +221,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}} +.. |etevents| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{events}} .. Indices, non-terminals @@ -229,6 +235,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}} +.. |eventidx| mathdef:: \xref{syntax/modules}{syntax-eventidx}{\X{eventidx}} .. Indices, meta functions @@ -251,6 +258,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}} +.. |MEVENTS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{events}} .. |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,6 +273,9 @@ .. |MTYPE| mathdef:: \xref{syntax/modules}{syntax-mem}{\K{type}} +.. |EVATTRIBUTE| mathdef:: \xref{syntax/modules}{syntax-event}{\K{attribute}} +.. |EVTYPE| mathdef:: \xref{syntax/modules}{syntax-event}{\K{type}} + .. |GTYPE| mathdef:: \xref{syntax/modules}{syntax-global}{\K{type}} .. |GINIT| mathdef:: \xref{syntax/modules}{syntax-global}{\K{init}} @@ -292,6 +303,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}} +.. |EDEVENT| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{event}} .. |IMODULE| mathdef:: \xref{syntax/modules}{syntax-import}{\K{module}} .. |INAME| mathdef:: \xref{syntax/modules}{syntax-import}{\K{name}} @@ -299,6 +311,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}} +.. |IDEVENT| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{event}} .. |IDGLOBAL| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{global}} @@ -309,6 +322,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}} +.. |event| mathdef:: \xref{syntax/modules}{syntax-event}{\X{event}} .. |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 +340,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}} +.. |edevents| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{events}} .. |edglobals| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{globals}} @@ -347,6 +362,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,10 +523,12 @@ .. |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}} +.. |Beventtype| mathdef:: \xref{binary/types}{binary-eventtype}{\B{eventtype}} .. |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}} .. |Bmut| mathdef:: \xref{binary/types}{binary-mut}{\B{mut}} +.. |Battribute| mathdef:: \xref{binary/types}{binary-attribute}{\B{attribute}} .. Indices, non-terminals @@ -516,6 +538,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}} +.. |Beventidx| mathdef:: \xref{binary/modules}{binary-eventidx}{\B{eventidx}} .. |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 +559,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}} +.. |Beventsec| mathdef:: \xref{binary/modules}{binary-eventsec}{\B{eventsec}} .. |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 +573,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}} +.. |Bevent| mathdef:: \xref{binary/modules}{binary-event}{\B{event}} .. |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}} @@ -663,6 +688,7 @@ .. |Trefedtype| mathdef:: \xref{text/types}{text-refedtype}{\T{refedtype}} .. |Tvaltype| mathdef:: \xref{text/types}{text-valtype}{\T{valtype}} .. |Tfunctype| mathdef:: \xref{text/types}{text-functype}{\T{functype}} +.. |Teventtype| mathdef:: \xref{text/types}{text-eventtype}{\T{eventtype}} .. |Tglobaltype| mathdef:: \xref{text/types}{text-globaltype}{\T{globaltype}} .. |Ttabletype| mathdef:: \xref{text/types}{text-tabletype}{\T{tabletype}} @@ -679,6 +705,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}} +.. |Teventidx| mathdef:: \xref{text/modules}{text-eventidx}{\T{eventidx}} .. |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 +731,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}} +.. |Tevent| mathdef:: \xref{text/modules}{text-event}{\T{event}} .. |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 +777,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}} +.. |IEVENTS| mathdef:: \xref{text/conventions}{text-context}{\K{events}} .. |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 +808,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}} +.. |CEVENTS| mathdef:: \xref{valid/conventions}{context}{\K{events}} .. |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 +825,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} +.. |vdasheventtype| mathdef:: \xref{valid/types}{valid-eventtype}{\vdash} .. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash} .. |vdashexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\vdash} @@ -807,6 +838,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} +.. |vdashevent| mathdef:: \xref{valid/modules}{valid-event}{\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 +869,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}} +.. |allocevent| mathdef:: \xref{exec/modules}{alloc-event}{\F{allocevent}} .. |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 +885,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}} +.. |eventaddr| mathdef:: \xref{exec/runtime}{syntax-eventaddr}{\X{eventaddr}} .. |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,6 +904,9 @@ .. |MITYPE| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{type}} .. |MIDATA| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{data}} +.. |EVIATTRIBUTE| mathdef:: \xref{exec/runtime}{syntax-eventinst}{\K{attribute}} +.. |EVITYPE| mathdef:: \xref{exec/runtime}{syntax-eventinst}{\K{type}} + .. |GITYPE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{type}} .. |GIVALUE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{value}} @@ -884,12 +921,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}} +.. |EVEVENT| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{event}} .. |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}} +.. |MIEVENTS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{eventaddrs}} .. |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 +943,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}} +.. |eventinst| mathdef:: \xref{exec/runtime}{syntax-eventinst}{\X{eventinst}} .. |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 +957,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}} +.. |evevents| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{events}} .. |evglobals| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{globals}} @@ -925,6 +966,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}} +.. |SEVENTS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{events}} .. |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 +1002,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}} +.. |EXNREFADDR| mathdef:: \xref{exec/runtime}{syntax-exnrefaddr}{\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 +1023,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 +1145,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} +.. |vdasheventinst| mathdef:: \xref{appendix/properties}{valid-eventinst}{\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 +1160,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} +.. |vdasheventinstextends| mathdef:: \xref{appendix/properties}{extend-eventinst}{\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 b6a49b0cd..624874a24 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, event type, global type, value type, result type, index space, module, function, event .. _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, \\ + & \CEVENTS & \eventtype^\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 5dbf44f4e..93be2c3d2 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, event index, vector, polymorphism, context pair: validation; instruction single: abstract syntax; instruction .. _valid-label: @@ -872,6 +872,111 @@ 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 event :math:`C.\CEVENTS[x]` must be defined in the context. + +* Let :math:`\EXCEPTION [t^\ast] \to []` be its :ref:`event 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.\CEVENTS[x] = \EXCEPTION [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 event :math:`C.\CEVENTS[x]` must be defined in the context. + +* Let :math:`[t^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. + +* The event :math:`C.\CEVENTS[x]` must be :math:`\EXCEPTION~[t^\ast]\to[]`. + +* Then the instruction is valid with type :math:`[\EXNREF]\to[\EXNREF]` + +.. math:: + \frac{ + C.\CLABELS[l]=[t^\ast] + \qquad + C.\CEVENTS[x]=\EXCEPTION~[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 eeed38f3a..105689894 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:: event, event type, exception attribute + pair: validation; event + single: abstract syntax; event +.. _valid-event: + +Events +~~~~~~ + +Events :math:`\event` are classified by the contents of their :ref:`event types `. +Currently the only allowed events are exceptions, i.e., events with type of the form :math:`\EXCEPTION~[t^\ast]\to[]`. + +:math:`\{ \EVATTRIBUTE~\EXCEPTION, \EVTYPE~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 event definition is valid with :ref:`event type ` :math:`\EXCEPTION~[t^\ast]\to[]`. + +.. math:: + \frac{ + C.\CTYPES[x] = [t^\ast] \to [] + }{ + C \vdashevent \{ \EVATTRIBUTE~\EXCEPTION, \EVTYPE~x \} : \EXCEPTION~[t^\ast]\to[] + } + + .. index:: global, global type, expression pair: validation; global single: abstract syntax; global @@ -387,6 +417,21 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi } +:math:`\EDEVENT~x` +.................. + +* The global :math:`C.\CEVENTS[x]` must be defined in the context. + +* Then the export description is valid with :ref:`external type ` :math:`\ETEVENT~C.\CEVENTS[x]`. + +.. math:: + \frac{ + C.\CEVENTS[x] = \eventtype + }{ + C \vdashexportdesc \EDEVENT~x : \ETEVENT~\eventtype + } + + :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, event 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:`\IDEVENT~\event` +....................... + +* Let :math:`\{ \EVATTRIBUTE~\EXCEPTION, \EVTYPE~x \}` be the :math:`\event`. + +* The type :math:`C.\CTYPES[x]` must be defined in the context. + +* The :ref:`event type ` :math:`\EXCEPTION~C.\CTYPES[x]` must be a :ref:`valid event type `. + +* Then the import description is valid with type :math:`\ETEVENT~\EXCEPTION~C.\CTYPES[x]`. + +.. math:: + \frac{ + \vdasheventtype \EXCEPTION~C.\CTYPES[x] \ok + }{ + C \vdashimportdesc \IDEVENT~\{ \EVATTRIBUTE~\EXCEPTION, \EVTYPE~x \}: \ETEVENT~\EXCEPTION~C.\CTYPES[x] + } + + + :math:`\IDGLOBAL~\globaltype` ............................. @@ -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.\CEVENTS` is :math:`\etevents(\X{it}^\ast)` concatenated with :math:`\X{ev}^\ast`, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :ref:`event types ` :math:`\X{ev}^\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'.\CEVENTS` is the same as :math:`C.\CEVENTS`, + * 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:`\event_i` in :math:`\module.\MEVENTS`, + the definition :math:`\event_i` must be :ref:`valid ` with a :ref:`event type ` :math:`\X{ev}_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{ev}^\ast` be the concatenation of the internal :ref:`event types ` :math:`\X{ev}_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 \vdashevent \event : \X{ev})^\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{iev}^\ast = \etevents(\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, \CEVENTS~\X{iev}^\ast\,\X{ev}^\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), \CEVENTS~(C.\CEVENTS) \} \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, + \MEVENTS~\event^\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 214014564..786179953 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:`event 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:: event type, exception attribute, result type + pair: validation; event type + single: abstract syntax; event type +.. _valid-eventtype: + +Event Types +~~~~~~~~~~~ + +:math:`\EXCEPTION~~[t^n] \to []` +................................. + +* The :ref:`attribute ` must be |EXCEPTION|. + +* The :ref:`function type ` :math:`[t^n] \to []` must be :ref:`valid `. + +* Then the event type is valid. + +.. math:: + \frac{ + \vdashfunctype [t^n] \to [] \ok + }{ + \vdasheventtype \EXCEPTION~[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:`\ETEVENT~\eventtype` +........................... + +* The :ref:`event type ` :math:`\eventtype` must be :ref:`valid `. + +* Then the external type is valid. + +.. math:: + \frac{ + \vdasheventtype \eventtype \ok + }{ + \vdashexterntype \ETEVENT~\eventtype \ok + } + :math:`\ETGLOBAL~\globaltype` ............................. @@ -338,6 +377,23 @@ An :ref:`external type ` :math:`\ETMEM~\limits_1` matches :ma } +.. index:: event type, value type +.. _match-eventtype: + +Events +...... + +An :ref:`external type ` :math:`\ETEVENT~\eventtype_1` matches :math:`\ETEVENT~\eventtype_2` if and only if: + +* Both :math:`\ETEVENT~\eventtype_1` and :math:`\ETEVENT~\eventtype_2` are the same. + +.. math:: + \frac{ + }{ + \vdashexterntypematch \ETEVENT~\eventtype \matchesexterntype \ETEVENT~\eventtype + } + + .. index:: global type, value type, mutability .. _match-globaltype: