From 4bd749a8895434c14b3bf3dda23463e3962192c4 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Tue, 7 Sep 2021 20:11:43 +0200 Subject: [PATCH 01/13] Update core formal spec to the current (3rd) EH proposal As described in `proposals/exceptions/Exceptions.md` and in `proposals/exceptions/Exceptions-formal-overview.md`. * Detailed changes from the previous (2nd proposal) formal spec: - Removed: + the reference type "exnref" is removed, + the administrative instruction "REFEXNADDR" is removed, + Release dependencies "bulk instructions" and "reference types" are removed. - Renamed: + "exn" and (most occurrences of) "exception" renamed to "tag", + "EITYPE" renamed to "TAGITYPE", + "ETYPE" renamed to "TAGTYPE", + variable names for tags changed from "et" to "tt" or "tagt" and "iet" to "itagt", + "CATCHN" is renamed to "CATCHadm". + "THROWADDR" is renamed to "THROWadm". - Adjusted: + syntax and rules for "TRY-CATCH", "RETHROW", and "CATCHadm", + folded text format for "TRY-CATCH", + validation example of control frame with opcode catch. - Added: + validation example of control frame with opcode catch_all, + administrative instructions "CAUGHTadm" and "DELEGATEadm" with rules, + syntax and rules for "TRY-DELEGATE". - Most prose that is changing in the 3rd spec is removed and a temporary "**TODO: add prose**" is added. + This will be updated in a followup PR to include the new prose instead. iIn several places added or adjusted prose or added TODO items to add prose in a followup PR. - Several similar **TODO**s are added for uncaught exceptions. --- document/core/appendix/algorithm.rst | 14 +- document/core/appendix/embedding.rst | 22 +-- document/core/appendix/implementation.rst | 6 +- document/core/appendix/index-rules.rst | 8 +- document/core/appendix/index-types.rst | 3 +- document/core/appendix/properties.rst | 130 ++++++++-------- document/core/binary/instructions.rst | 18 ++- document/core/binary/modules.rst | 50 +++--- document/core/binary/types.rst | 20 +-- document/core/exec/instructions.rst | 180 ++++++++-------------- document/core/exec/modules.rst | 85 ++++------ document/core/exec/runtime.rst | 162 ++++++++++--------- document/core/syntax/instructions.rst | 26 ++-- document/core/syntax/modules.rst | 55 +++---- document/core/syntax/types.rst | 36 ++--- document/core/text/conventions.rst | 2 +- document/core/text/instructions.rst | 39 +++-- document/core/text/modules.rst | 80 +++++----- document/core/text/types.rst | 2 - document/core/util/macros.def | 78 +++++----- document/core/valid/conventions.rst | 12 +- document/core/valid/instructions.rst | 97 +++++------- document/core/valid/modules.rst | 74 ++++----- document/core/valid/types.rst | 40 ++--- 24 files changed, 604 insertions(+), 635 deletions(-) diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index 4ed6963c..8a35bcef 100644 --- a/document/core/appendix/algorithm.rst +++ b/document/core/appendix/algorithm.rst @@ -25,7 +25,7 @@ Types are representable as an enumeration. .. code-block:: pseudo - type val_type = I32 | I64 | F32 | F64 | V128 | Funcref | Exnref | Externref + type val_type = I32 | I64 | F32 | F64 | V128 | Funcref | Externref func is_num(t : val_type | Unknown) : bool = return t = I32 || t = I64 || t = F32 || t = F64 || t = Unknown @@ -34,7 +34,7 @@ Types are representable as an enumeration. return t = V128 || t = Unknown func is_ref(t : val_type | Unknown) : bool = - return t = Funcref || t = Exnref || t = Externref || t = Unknown + return t = Funcref || t = Externref || t = Unknown 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 `, @@ -216,8 +216,14 @@ Other instructions are checked in a similar manner. case (catch) let frame = pop_ctrl() - error_if(frame.opcode =/= try) - push_ctrl(catch, [exnref], frame.end_types) + error_if(frame.opcode =/= try || frame.opcode =/= catch) + let tagparams = tags.[x].type.params + push_ctrl(catch, tagparams , frame.end_types) + + case (catch_all) + let frame = pop_ctrl() + error_if(frame.opcode =/= try || frame.opcode =/= catch) + push_ctrl(catch_all, [] , frame.end_types) case (br n) error_if(ctrls.size() < n) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index 4f3e532b..a66edd24 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, ~\SEXNS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\ + \F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon, ~\STAGS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\ \end{array} @@ -539,26 +539,26 @@ Memories \end{array} -.. index:: exception, exception address, store, exception instance, exception type, function type -.. _embed-exn: +.. index:: tag, tag address, store, tag instance, tag type, function type +.. _embed-tag: -Exceptions -~~~~~~~~~~ +Tags +~~~~ -.. _embedd-exn-alloc: +.. _embedd-tag-alloc: -:math:`\F{exn\_alloc}(\store, \exntype) : (\store, \exnaddr)` +:math:`\F{tag\_alloc}(\store, \tagtype) : (\store, \tagaddr)` ............................................................. -1. Pre-condition: :math:`exntype` is :ref:`valid `. +1. Pre-condition: :math:`tagtype` is :ref:`valid `. -2. Let :math:`\exnaddr` be the result of :ref:`allocating an exception ` in :math:`\store` with :ref:`exception type ` :math:`\exntype`. +2. Let :math:`\tagaddr` be the result of :ref:`allocating a tag ` in :math:`\store` with :ref:`tag type ` :math:`\tagtype`. -3. Return the new store paired with :math:`\exnaddr`. +3. Return the new store paired with :math:`\tagaddr`. .. math:: \begin{array}{lclll} - \F{exn\_alloc}(S, \X{et}) &=& (S', \X{a}) && (\iff \allocexn(S, \X{et}) = S', \X{a}) \\ + \F{tag\_alloc}(S, \X{tt}) &=& (S', \X{a}) && (\iff \alloctag(S, \X{tt}) = S', \X{a}) \\ \end{array} diff --git a/document/core/appendix/implementation.rst b/document/core/appendix/implementation.rst index c51315b0..4ffbe0e7 100644 --- a/document/core/appendix/implementation.rst +++ b/document/core/appendix/implementation.rst @@ -24,7 +24,7 @@ However, it is expected that all implementations have "reasonably" large limits Syntactic Limits ~~~~~~~~~~~~~~~~ -.. index:: abstract syntax, module, type, function, table, memory, global, element, data, import, export, parameter, result, local, structured control instruction, instruction, name, Unicode, character +.. index:: abstract syntax, module, type, function, table, memory, tag, global, element, data, import, export, parameter, result, local, structured control instruction, instruction, name, Unicode, character .. _impl-syntax: Structure @@ -36,7 +36,7 @@ An implementation may impose restrictions on the following dimensions of a modul * the number of :ref:`functions ` in a :ref:`module `, including imports * the number of :ref:`tables ` in a :ref:`module `, including imports * the number of :ref:`memories ` in a :ref:`module `, including imports -* the number of :ref:`exceptions ` in a :ref:`module `, including imports +* the number of :ref:`tags ` 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 ` @@ -124,7 +124,7 @@ Restrictions on the following dimensions may be imposed during :ref:`execution < * the number of allocated :ref:`function instances ` * the number of allocated :ref:`table instances ` * the number of allocated :ref:`memory instances ` -* the number of allocated :ref:`exception instances ` +* the number of allocated :ref:`tag 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-rules.rst b/document/core/appendix/index-rules.rst index 2d40276a..bda9a407 100644 --- a/document/core/appendix/index-rules.rst +++ b/document/core/appendix/index-rules.rst @@ -18,7 +18,7 @@ Construct Judgement :ref:`Block type ` :math:`\vdashblocktype \blocktype \ok` :ref:`Table type ` :math:`\vdashtabletype \tabletype \ok` :ref:`Memory type ` :math:`\vdashmemtype \memtype \ok` -:ref:`Exception type ` :math:`\vdashexntype \exntype \ok` +:ref:`Tag type ` :math:`\vdashtagtype \tagtype \ok` :ref:`Global type ` :math:`\vdashglobaltype \globaltype \ok` :ref:`External type ` :math:`\vdashexterntype \externtype \ok` :ref:`Instruction ` :math:`S;C \vdashinstr \instr : \stacktype` @@ -27,7 +27,7 @@ Construct Judgement :ref:`Function ` :math:`C \vdashfunc \func : \functype` :ref:`Table ` :math:`C \vdashtable \table : \tabletype` :ref:`Memory ` :math:`C \vdashmem \mem : \memtype` -:ref:`Exception ` :math:`C \vdashexn \exn : \exntype` +:ref:`Tag ` :math:`C \vdashtag \tag : \tagtype` :ref:`Global ` :math:`C \vdashglobal \global : \globaltype` :ref:`Element segment ` :math:`C \vdashelem \elem : \reftype` :ref:`Element mode ` :math:`C \vdashelemmode \elemmode : \reftype` @@ -56,7 +56,7 @@ Construct Judgement :ref:`Function instance ` :math:`S \vdashfuncinst \funcinst : \functype` :ref:`Table instance ` :math:`S \vdashtableinst \tableinst : \tabletype` :ref:`Memory instance ` :math:`S \vdashmeminst \meminst : \memtype` -:ref:`Exception instance ` :math:`S \vdashexninst \exninst : \exntype` +:ref:`Tag instance ` :math:`S \vdashtaginst \taginst : \tagtype` :ref:`Global instance ` :math:`S \vdashglobalinst \globalinst : \globaltype` :ref:`Element instance ` :math:`S \vdasheleminst \eleminst \ok` :ref:`Data instance ` :math:`S \vdashdatainst \datainst \ok` @@ -100,7 +100,7 @@ Construct Judgement :ref:`Function instance ` :math:`\vdashfuncinstextends \funcinst_1 \extendsto \funcinst_2` :ref:`Table instance ` :math:`\vdashtableinstextends \tableinst_1 \extendsto \tableinst_2` :ref:`Memory instance ` :math:`\vdashmeminstextends \meminst_1 \extendsto \meminst_2` -:ref:`Exception instance ` :math:`\vdashexninstextends \exninst_1 \extendsto \exninst_2` +:ref:`Tag instance ` :math:`\vdashtaginstextends \taginst_1 \extendsto \taginst_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 bd8f08d2..185a034e 100644 --- a/document/core/appendix/index-types.rst +++ b/document/core/appendix/index-types.rst @@ -16,13 +16,12 @@ Category Constructor (reserved) :math:`\hex{7A}` .. :math:`\hex{71}` :ref:`Reference type ` |FUNCREF| :math:`\hex{70}` (-16 as |Bs7|) :ref:`Reference type ` |EXTERNREF| :math:`\hex{6F}` (-17 as |Bs7|) -: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:`Exception type ` :math:`\functype` (none) +:ref:`Tag type ` :math:`\functype` (none) :ref:`Global type ` :math:`\mut~\valtype` (none) ======================================== =========================================== =============================================================================== diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index cb32d3cd..7438e9ec 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:`exception `, :ref:`global `, and :ref:`module ` instances that are themselves valid, relative to :math:`S`. +:ref:`function `, :ref:`table `, :ref:`memory `, :ref:`tag `, :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 `, :ref:`exception `, or :ref:`global ` type. +To that end, each kind of instance is classified by a respective :ref:`function `, :ref:`table `, :ref:`memory `, :ref:`tag `, 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, exception instance, global instance, function type, table type, memory type, exception type, global type +.. index:: store, function instance, table instance, memory instance, tag instance, global instance, function type, table type, memory type, tag type, global type :ref:`Store ` :math:`S` ..................................... @@ -85,7 +85,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co * Each :ref:`memory instance ` :math:`\meminst_i` in :math:`S.\SMEMS` must be :ref:`valid ` with some :ref:`memory type ` :math:`\memtype_i`. -* Each :ref:`exception instance ` :math:`\exninst_i` in :math:`S.\SEXNS` must be :ref:`valid ` with some :ref:`exception type ` :math:`\exntype_i`. +* Each :ref:`tag instance ` :math:`\taginst_i` in :math:`S.\STAGS` must be :ref:`valid ` with some :ref:`tag type ` :math:`\tagtype_i`. * Each :ref:`global instance ` :math:`\globalinst_i` in :math:`S.\SGLOBALS` must be :ref:`valid ` with some :ref:`global type ` :math:`\globaltype_i`. @@ -105,7 +105,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \\ (S \vdashmeminst \meminst : \memtype)^\ast \qquad - (S \vdashexninst \exninst : \exntype)^\ast + (S \vdashtaginst \taginst : \tagtype)^\ast \\ (S \vdashglobalinst \globalinst : \globaltype)^\ast \\ @@ -117,7 +117,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \SFUNCS~\funcinst^\ast, \STABLES~\tableinst^\ast, \SMEMS~\meminst^\ast, - \SEXNS~\exninst^\ast, + \STAGS~\taginst^\ast, \\ \SGLOBALS~\globalinst^\ast, \SELEMS~\eleminst^\ast, @@ -259,21 +259,21 @@ Module instances are classified by *module contexts*, which are regular :ref:`co } -.. index:: exception type, exception instance, exception tag, function type -.. _valid-exninst: +.. index:: tag type, tag instance, function type +.. _valid-taginst: -:ref:`Exception Instances ` :math:`\{ \EITYPE~\exntype \}` -........................................................................... +:ref:`Tag Instances ` :math:`\{ \TAGITYPE~\tagtype \}` +...................................................................... -* The :ref:`exception type ` :math:`\exntype` must be :ref:`valid `. +* The :ref:`tag type ` :math:`\tagtype` must be :ref:`valid `. -* Then the exception instance is valid with :ref:`exception type ` :math:`\exntype`. +* Then the tag instance is valid with :ref:`tag type ` :math:`\tagtype`. .. math:: \frac{ - \vdashexntype \exntype \ok + \vdashtagtype \tagtype \ok }{ - S \vdashexninst \{ \EITYPE~\exntype \} : \exntype + S \vdashtaginst \{ \TAGITYPE~\tagtype \} : \tagtype } @@ -365,7 +365,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co * For each :ref:`memory address ` :math:`\memaddr_i` in :math:`\moduleinst.\MIMEMS`, the :ref:`external value ` :math:`\EVMEM~\memaddr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETMEM~\memtype_i`. -* For each :ref:`exception address ` :math:`\exnaddr_i` in :math:`\moduleinst.\MIEXNS`, the :ref:`external value ` :math:`\EVEXN~\exnaddr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETEXN~\exntype_i`. +* For each :ref:`tag address ` :math:`\tagaddr_i` in :math:`\moduleinst.\MITAGS`, the :ref:`external value ` :math:`\EVTAG~\tagaddr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETTAG~\tagtype_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`. @@ -383,12 +383,12 @@ Module instances are classified by *module contexts*, which are regular :ref:`co * Let :math:`\memtype^\ast` be the concatenation of all :math:`\memtype_i` in order. -* Let :math:`\exntype^\ast` be the concatenation of all :math:`\exntype_i` in order. +* Let :math:`\tagtype^\ast` be the concatenation of all :math:`\tagtype_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, \CEXNS~\exntype^\ast, \CGLOBALS~\globaltype^\ast\}`. + | :math:`\{\CTYPES~\functype^\ast, \CFUNCS~{\functype'}^\ast, \CTABLES~\tabletype^\ast, \CMEMS~\memtype^\ast, \CTAGS~\tagtype^\ast, \CGLOBALS~\globaltype^\ast\}`. .. math:: ~\\[-1ex] @@ -402,7 +402,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \\ (S \vdashexternval \EVMEM~\memaddr : \ETMEM~\memtype)^\ast \qquad - (S \vdashexternval \EVEXN~\exnaddr : \ETEXN~\exntype)^\ast + (S \vdashexternval \EVTAG~\tagaddr : \ETTAG~\tagtype)^\ast \\ (S \vdashexternval \EVGLOBAL~\globaladdr : \ETGLOBAL~\globaltype)^\ast \\ @@ -421,7 +421,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \MIFUNCS & \funcaddr^\ast, \\ \MITABLES & \tableaddr^\ast, \\ \MIMEMS & \memaddr^\ast, \\ - \MIEXNS & \exnaddr^\ast, \\ + \MITAGS & \tagaddr^\ast, \\ \MIGLOBALS & \globaladdr^\ast, \\ \MIELEMS & \elemaddr^\ast, \\ \MIDATAS & \dataaddr^\ast, \\ @@ -431,7 +431,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \CFUNCS & {\functype'}^\ast, \\ \CTABLES & \tabletype^\ast, \\ \CMEMS & \memtype^\ast, \\ - \CEXNS & \exntype^\ast \\ + \CTAGS & \tagtype^\ast \\ \CGLOBALS & \globaltype^\ast ~\} \end{array} \end{array} @@ -586,65 +586,75 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera } -.. index:: exception address, exception type, function type, value type, exception tag +.. index:: throw, throw context, tag address -:math:`\REFEXNADDR~\exnaddr~\val^\ast` -...................................... +:math:`\THROWadm~\tagaddr` +.......................... -* The :ref:`external exception value ` :math:`\EVEXN~\exnaddr` must be :ref:`valid ` with :ref:`external exception type ` :math:`\ETEXN~[t^\ast]\to[]`. +* The :ref:`external tag value ` :math:`\EVTAG~\tagaddr` must be :ref:`valid ` with :ref:`external tag type ` :math:`\ETTAG~[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]`. +* 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{ - S \vdashexternval \EVEXN~\exnaddr : \ETEXN~[t^\ast]\to[] - \qquad - (S \vdashval \val : t)^\ast + S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t^\ast]\to[] }{ - S; C \vdashadmininstr \REFEXNADDR~\exnaddr~\val^\ast : [] \to [\EXNREF] + S; C \vdashadmininstr \THROWadm~\tagaddr : [t_1^\ast t^\ast] \to [t_2^\ast] } -.. index:: throw, throw context, exception address, exception tag +.. index:: catch, throw context -:math:`\THROWADDR~\exnaddr` -........................... +:math:`\CATCHadm\{\tagaddr^?~\instr'^\ast\}^\ast~\instr^\ast~\END` +.................................................................. -* The :ref:`external exception value ` :math:`\EVEXN~\exnaddr` must be :ref:`valid ` with :ref:`external exception type ` :math:`\ETEXN~[t^\ast]\to[]`. +**TODO: add prose** -* Then the instruction is valid with type :math:`[t_1^\ast t^\ast] -> [t_2^\ast]` for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ - S \vdashexternval \EVEXN~\exnaddr : \ETEXN~[t^\ast]\to[] + \begin{array}{c} + ((S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t'^\ast]\to[])^?~~\land~~S; C,\CLABELS\,(\catch~[t^\ast]) \vdashinstrseq \instr'^\ast : [(t'^\ast)^?] \to [t^\ast])^\ast \\ + S; C,\CLABELS\,[t^\ast] \vdashinstrseq \instr^\ast : [] \to [t^\ast] \\ + \end{array} }{ - S; C \vdashadmininstr \THROWADDR~\exnaddr : [t_1^\ast t^\ast] \to [t_2^\ast] + S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CATCHadm\{\tagaddr^?~\instr'^\ast\}^\ast~\instr^\ast~\END : [] \to [t^\ast] } -.. index:: catch, throw context +.. index:: delegate, throw context -:math:`\CATCH_n\{ \instr_0^\ast \} \instr^\ast \END` -.................................................... +:math:`\DELEGATEadm\{l\}~\instr^\ast~\END` +.......................................... -* The instruction sequence :math:`\instr_0^\ast` must be :ref:`valid ` with a type of the form :math:`[\EXNREF] \to [t^n]`. +**TODO: add prose** -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t^n]` prepended to the |CLABELS| vector. +.. math:: + \frac{ + S; C,\CLABELS\,[t^\ast] \vdashinstrseq \instr^\ast : [] \to [t^\ast] + \qquad + |C.\CLABELS| \ge l + }{ + S; C,\CLABELS\,[t^\ast] \vdashadmininstr \DELEGATEadm\{l\}~\instr^\ast~\END : [] \to [t^\ast] + } -* 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]`. +.. index:: caught, throw context + +:math:`\CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END` +......................................................... + +**TODO: add prose** .. math:: \frac{ - S; C \vdashinstrseq \instr_0^\ast : [\EXNREF] \to [t^n] + S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t'^\ast]\to[] \qquad - S; C,\CLABELS\,[t^n] \vdashinstrseq \instr^\ast : [] \to [t^n] + (val:t')^\ast + \qquad + S; C,\CLABELS\,(\catch~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] }{ - S; C \vdashadmininstr \CATCH_n\{\instr_0^\ast\}~\instr^\ast~\END : [] \to [t^n] + S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] } @@ -738,7 +748,7 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S' * The length of :math:`S.\SMEMS` must not shrink. -* The length of :math:`S.\SEXNS` must not shrink. +* The length of :math:`S.\STAGS` must not shrink. * The length of :math:`S.\SGLOBALS` must not shrink. @@ -752,7 +762,7 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S' * For each :ref:`memory instance ` :math:`\meminst_i` in the original :math:`S.\SMEMS`, the new memory instance must be an :ref:`extension ` of the old. -* For each :ref:`exception instance ` :math:`\exninst_i` in the original :math:`S.\SEXNS`, the new exception instance must be an :ref:`extension ` of the old. +* For each :ref:`tag instance ` :math:`\taginst_i` in the original :math:`S.\STAGS`, the new tag 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. @@ -772,9 +782,9 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S' S_1.\SMEMS = \meminst_1^\ast & S_2.\SMEMS = {\meminst'_1}^\ast~\meminst_2^\ast & (\vdashmeminstextends \meminst_1 \extendsto \meminst'_1)^\ast \\ - S_1.\SEXNS = \exninst_1^\ast & - S_2.\SEXNS = {\exninst'_1}^\ast~\exninst_2^\ast & - (\vdashexninstextends \exninst_1 \extendsto \exninst'_1)^\ast \\ + S_1.\STAGS = \taginst_1^\ast & + S_2.\STAGS = {\taginst'_1}^\ast~\taginst_2^\ast & + (\vdashtaginstextends \taginst_1 \extendsto \taginst'_1)^\ast \\ S_1.\SGLOBALS = \globalinst_1^\ast & S_2.\SGLOBALS = {\globalinst'_1}^\ast~\globalinst_2^\ast & (\vdashglobalinstextends \globalinst_1 \extendsto \globalinst'_1)^\ast \\ @@ -841,18 +851,18 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S' } -.. index:: exception instance -.. _extend-exninst: +.. index:: tag instance +.. _extend-taginst: -:ref:`Exception Instance ` :math:`\exninst` -........................................................... +:ref:`Tag Instance ` :math:`\taginst` +..................................................... -* An exception instance must remain unchanged. +* A tag instance must remain unchanged. .. math:: \frac{ }{ - \vdashexninstextends \exninst \extendsto \exninst + \vdashtaginstextends \taginst \extendsto \taginst } diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 1bdab57e..1bd5744a 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|, |ELSE|, and |CATCH|. +:ref:`Control instructions ` have varying encodings. For structured instructions, the instruction sequences forming nested blocks are separated or terminated with explicit opcodes for |END|, |ELSE|, |CATCH|, |CATCHALL|, and |DELEGATE|. :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 `. @@ -34,7 +34,6 @@ Control Instructions .. _binary-try: .. _binary-throw: .. _binary-rethrow: -.. _binary-br_on_exn: .. _binary-br: .. _binary-br_if: .. _binary-br_table: @@ -61,11 +60,14 @@ Control Instructions \hex{05}~~(\X{in}_2{:}\Binstr)^\ast~~\hex{0B} &\Rightarrow& \IF~\X{bt}~\X{in}_1^\ast~\ELSE~\X{in}_2^\ast~\END \\ &&|& \hex{06}~~\X{bt}{:}\Bblocktype~~(\X{in}_1{:}\Binstr)^\ast~~ - \hex{07}~~(\X{in}_2{:}\Binstr)^\ast~~\hex{0B} - &\Rightarrow& \TRY~\X{bt}~\X{in}_1^\ast~\CATCH~\X{in}_2^\ast~\END \\ &&|& - \hex{08}~~x{:}\Bexnidx &\Rightarrow& \THROW~x \\ &&|& - \hex{09} &\Rightarrow& \RETHROW \\ &&|& - \hex{0A}~~l{:}\Blabelidx~~x{:}\Bexnidx &\Rightarrow& \BRONEXN~l~x \\ &&|& + (\hex{07}~~x{:}\Btagidx~~(\X{in}_2{:}\Binstr)^\ast)^\ast~~ + (\hex{19}~~(\X{in}_3{:}\Binstr)^\ast)^?~~\hex{0B} + &\Rightarrow& \TRY~\X{bt}~\X{in}_1^\ast~(\CATCH~x~\X{in}_2^\ast)^\ast~ + (\CATCHALL~\X{in}_3^\ast)^?\END \\ &&|& + \hex{06}~~\X{bt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{18}~~l{:}\Blabelidx + &\Rightarrow& \TRY~\X{bt}~\X{in}^\ast~\DELEGATE~l \\ &&|& + \hex{08}~~x{:}\Btagidx &\Rightarrow& \THROW~x \\ &&|& + \hex{09}~~l{:}\Blabelidx &\Rightarrow& \RETHROW~l \\ &&|& \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 2c90c7cf..3dcebf39 100644 --- a/document/core/binary/modules.rst +++ b/document/core/binary/modules.rst @@ -9,12 +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, exception index, global index, element index, data index, local index, label index +.. index:: index, type index, function index, table index, memory index, tag index, global index, element index, data index, local index, label index pair: binary format; type index pair: binary format; function index pair: binary format; table index pair: binary format; memory index - pair: binary format; exception index + pair: binary format; tag index pair: binary format; global index pair: binary format; element index pair: binary format; data index @@ -24,7 +24,7 @@ except that :ref:`function definitions ` are split into two section .. _binary-funcidx: .. _binary-tableidx: .. _binary-memidx: -.. _binary-exnidx: +.. _binary-tagidx: .. _binary-globalidx: .. _binary-elemidx: .. _binary-dataidx: @@ -43,7 +43,7 @@ All :ref:`indices ` are encoded with their respective value. \production{function index} & \Bfuncidx &::=& x{:}\Bu32 &\Rightarrow& x \\ \production{table index} & \Btableidx &::=& x{:}\Bu32 &\Rightarrow& x \\ \production{memory index} & \Bmemidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{exception index} & \Bexnidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{tag index} & \Btagidx &::=& 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 \\ @@ -103,7 +103,7 @@ Id Section 10 :ref:`code section ` 11 :ref:`data section ` 12 :ref:`data count section ` -13 :ref:`exception section ` +13 :ref:`tag section ` == =============================================== @@ -150,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, exception type +.. index:: ! import section, import, name, function type, table type, memory type, global type, tag type pair: binary format; import pair: section; import .. _binary-import: @@ -175,7 +175,7 @@ It decodes into a vector of :ref:`imports ` that represent the |M \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{04}~~\X{et}{:}\Bexn &\Rightarrow& \IDEXN~\X{et} \\ + \hex{04}~~\X{tt}{:}\Btag &\Rightarrow& \IDTAG~\X{tt} \\ \end{array} @@ -262,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, exception index, global index +.. index:: ! export section, export, name, index, function index, table index, memory index, tag index, global index pair: binary format; export pair: section; export .. _binary-export: @@ -287,7 +287,7 @@ It decodes into a vector of :ref:`exports ` that represent the |M \hex{01}~~x{:}\Btableidx &\Rightarrow& \EDTABLE~x \\ &&|& \hex{02}~~x{:}\Bmemidx &\Rightarrow& \EDMEM~x \\ &&|& \hex{03}~~x{:}\Bglobalidx &\Rightarrow& \EDGLOBAL~x \\ &&|& - \hex{04}~~x{:}\Bexnidx &\Rightarrow& \EDEXN~x \\ + \hex{04}~~x{:}\Btagidx &\Rightarrow& \EDTAG~x \\ \end{array} @@ -490,29 +490,29 @@ It decodes into an optional :ref:`u32 ` that represents the number instead of deferring validation. -.. index:: ! exception section, exception, exception type, function type index - pair: binary format; exception - pair: section; exception -.. _binary-exn: -.. _binary-exnsec: +.. index:: ! tag section, tag, tag type, function type index, exception tag + pair: binary format; tag + pair: section; tag +.. _binary-tag: +.. _binary-tagsec: -Exception Section -~~~~~~~~~~~~~~~~~ +Tag Section +~~~~~~~~~~~ -The *exception section* has the id 13. -It decodes into a vector of :ref:`exceptions ` that represent the |MEXNS| +The *tag section* has the id 13. +It decodes into a vector of :ref:`tags ` that represent the |MTAGS| component of a :ref:`module `. .. math:: \begin{array}{llclll} - \production{exception section} & \Bexnsec &::=& - \X{exception}^\ast{:}\Bsection_{13}(\Bvec(\Bexn)) &\Rightarrow& \X{exception}^\ast \\ - \production{exception} & \Bexn &::=& - \hex{00}~~\X{x}{:}\Btypeidx &\Rightarrow& \{ \ETYPE~\X{x} \} \\ + \production{tag section} & \Btagsec &::=& + \X{tag}^\ast{:}\Bsection_{13}(\Bvec(\Btag)) &\Rightarrow& \X{tag}^\ast \\ + \production{tag} & \Btag &::=& + \hex{00}~~\X{x}{:}\Btypeidx &\Rightarrow& \{ \TAGTYPE~\X{x} \} \\ \end{array} -.. index:: module, section, type definition, function type, function, table, memory, exception, global, element, data, start function, import, export, context, version +.. index:: module, section, type definition, function type, function, table, memory, tag, global, element, data, start function, import, export, context, version pair: binary format; module .. _binary-magic: .. _binary-version: @@ -554,7 +554,7 @@ Furthermore, it must be present if any :math:`data index ` occur \Bcustomsec^\ast \\ &&& \mem^\ast{:\,}\Bmemsec \\ &&& \Bcustomsec^\ast \\ &&& - \exn^\ast{:\,}\Bexnsec \\ &&& + \tag^\ast{:\,}\Btagsec \\ &&& \Bcustomsec^\ast \\ &&& \global^\ast{:\,}\Bglobalsec \\ &&& \Bcustomsec^\ast \\ &&& @@ -576,7 +576,7 @@ Furthermore, it must be present if any :math:`data index ` occur \MFUNCS~\func^n, \\ \MTABLES~\table^\ast, \\ \MMEMS~\mem^\ast, \\ - \MEXNS~\exn^\ast, \\ + \MTAGS~\tag^\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 87f04b9b..c44a04a1 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -58,8 +58,7 @@ Reference Types \begin{array}{llclll@{\qquad\qquad}l} \production{reference type} & \Breftype &::=& \hex{70} &\Rightarrow& \FUNCREF \\ &&|& - \hex{6F} &\Rightarrow& \EXTERNREF \\ &&|& - \hex{6E} &\Rightarrow& \EXNREF \\ + \hex{6F} &\Rightarrow& \EXTERNREF \\ \end{array} @@ -187,22 +186,23 @@ Global Types \end{array} -.. index:: exception type, function type - pair: binary format; exception type -.. _binary-exntype: +.. index:: tag type, function type, exception tag + pair: binary format; tag type +.. _binary-tagtype: -Exception Types -~~~~~~~~~~~~~~~ +Tag Types +~~~~~~~~~ -:ref:`Exception types ` are encoded by their function type. +:ref:`Tag types ` are encoded by their function type. .. math:: \begin{array}{llclll} - \production{exception type} & \Bexntype &::=& + \production{tag type} & \Btagtype &::=& \hex{00}~~ft{:}\Bfunctype &\Rightarrow& ft \\ \end{array} -The |Bfunctype| of an exception must have an empty result. +The |Bfunctype| of a tag must have an empty result, and it is used to characterise exceptions. +The :math:`\hex{00}` bit signifies an exception and is currently the only allowed value. .. note:: In future versions of WebAssembly, diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ffb72a40..b227ebfe 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2620,35 +2620,42 @@ Control Instructions \end{array} -.. _exec-try: +.. _exec-try-catch: -: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)`. +:math:`\TRY~\blocktype~\instr_1^\ast~(\CATCH~x~\instr_2^\ast)^\ast~(\CATCHALL~\instr_3^\ast)^?~\END` +.................................................................................................... -3. Assert: due to :ref:`validation `, there are at least :math:`n` values on the top of the stack. +**TODO: Add prose** -4. Pop the values :math:`\val^n` from the stack. +.. math:: + ~\\[-1ex] + \begin{array}{l} + F; \val^n~(\TRY~\X{bt}~\instr_1^\ast~(\CATCH~x~\instr_2^\ast)^\ast~(\CATCHALL~\instr_3^\ast)^?~\END + \quad \stepto \\ + \qquad F; \LABEL_m\{\}~(\CATCHadm\{a~\instr_2^\ast\}^\ast\{\epsilon~\instr_3\}^?~\val^n~\instr_1^\ast~\END)~\END \\ + (\iff \expand_F(\X{bt}) = [t_1^n] \to [t_2^m] \land (F.\AMODULE.\MITAGS[x]=a)^\ast) + \end{array} -5. Let :math:`L` be the label whose arity is :math:`m` and whose continuation is the end of the |TRY| instruction. -6. Let :math:`H` be the exception handler whose arity is :math:`m` and whose continuation is the beginning of :math:`\instr_2^\ast`. +.. _exec-try-delegate: -7. :ref:`Enter ` the exception handler `H`. +:math:`\TRY~\blocktype~\instr^\ast~\DELEGATE~l` +............................................... -8. :ref:`Enter ` the block :math:`\val^n~\instr_1^\ast` with label :math:`L`. +**TODO: Add prose** .. math:: ~\\[-1ex] - \begin{array}{lcl@{\qquad}} - F; \val^n~(\TRY~\X{bt}~\instr_1^\ast~\CATCH~\instr_2^\ast~\END &\stepto& - \CATCHN_m\{\instr_2\}~(\LABEL_m \{\}~\val^n~\instr_1^\ast~\END)~\END \\ - \hspace{5ex}(\iff \expand_F(\X{bt}) = [t_1^n] \to [t_2^m]) &&\\ + \begin{array}{lcl} + F; \val^n~(\TRY~\X{bt}~\instr^\ast~\DELEGATE~l) &\stepto& + F; \LABEL_m\{\}~(\DELEGATEadm\{l\}~\val^n~\instr^\ast~\END)~\END \\ + && (\iff \expand_F(\X{bt}) = [t_1^n] \to [t_2^m]) \end{array} +.. note:: + Note that the last reduction step above is similar to the :ref:`reduction ` of :math:`\BR~l`, but also doing a throw after it breaks. + + There is a subtle difference though. The instruction :math:`\BR~l` searches for the :math:`l+1` surrounding block and breaks out after that block. Because :math:`\DELEGATEadm\{l\}` is always wrapped in its own label, with the :ref:`same lookup ` as for :math:`\BR~l` we end up breaking inside the :math:`l+1` surrounding block and throwing there. So if that :math:`l+1` surrounding block is a try, we end up throwing in its "try code", and thus correctly getting delegated to that try's handlers. .. _exec-throw: @@ -2657,81 +2664,31 @@ Control Instructions 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIEXNS[x]` exists. +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITAGS[x]` exists. -3. Let :math:`a` be the :ref:`exception address ` :math:`F.\AMODULE.\MIEXNS[x]`. +3. Let :math:`a` be the :ref:`tag address ` :math:`F.\AMODULE.\MITAGS[x]`. -4. :ref:`Throw ` an exception with :ref:`exception address ` :math:`a`. +4. :ref:`Throw ` an exception with :ref:`tag address ` :math:`a`. .. math:: ~\\[-1ex] \begin{array}{lclr@{\qquad}l} - \THROW~x &\stepto& \THROWADDR~a & (\iff F.\AMODULE.\MIEXNS[x] = a) \\ + \THROW~x &\stepto& \THROWadm~a & (\iff F.\AMODULE.\MITAGS[x] = a) \\ \end{array} .. _exec-rethrow: -:math:`\RETHROW` -................ - -1. Assert: due to :ref:`validation `, there is a value with :ref:`reference type ` :math:`\EXNREF` on top of the stack. - -2. Pop the :math:`\EXNREF` value from the stack. - -3. If the :math:`\EXNREF` value is :math:`\REFNULL~\EXNREF` then: - - a. Trap. - -4. Assert: :math:`\EXNREF` is of the form :math:`(\REFEXNADDR~a~\val^\ast)`. - -5. Put the values :math:`\val^\ast` on the stack. +:math:`\RETHROW~l` +.................. -6. :ref:`Throw ` an exception with :ref:`exception address ` :math:`a`. +**TODO: Add prose** .. math:: ~\\[-1ex] \begin{array}{lclr@{\qquad}} - (\REFNULL~\EXNREF)~\RETHROW &\stepto& \TRAP \\ - (\REFEXNADDR~a~\val^\ast)~\RETHROW &\stepto& \val^\ast~(\THROWADDR~a) \\ - \end{array} - - -.. _exec-br_on_exn: - -:math:`\BRONEXN~l~x` -.................... - -1. Assert: due to :ref:`validation `, there is a value with :ref:`reference type ` :math:`\EXNREF` on top of the stack. - -2. Pop the :math:`\EXNREF` value from the stack. - -3. If the :math:`\EXNREF` value is :math:`\REFNULL~\EXNREF` then: - - a. Trap. - -4. Assert: :math:`\EXNREF` is of the form :math:`(\REFEXNADDR~a~\val^\ast)`. - -5. Let :math:`F` be the :ref:`current ` :ref:`frame `. - -6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIEXNS[x]` exists. - -7. If :math:`F.\AMODULE.\MIEXNS[x]=a`, then: - - a. Put the values :math:`\val^\ast` on the stack. - - b. :ref:`Execute ` the instruction :math:`(\BR~l)`. - -8. Else: - - a. Put the value :math:`(\REFEXNADDR~a~\val^\ast)` back on the stack. - -.. math:: - ~\\[-1ex] - \begin{array}{lclr@{\qquad}l} - F; (\REFNULL~\EXNREF)~\BRONEXN~l~x &\stepto& F; \TRAP \\ - F; (\REFEXNADDR~a~\val^\ast)~\BRONEXN~l~x &\stepto& F; \val^\ast~(\BR~l) & (\iff F.\AMODULE.\MIEXNS[x] = a) \\ - F; (\REFEXNADDR~a~\val^\ast)~\BRONEXN~l~x &\stepto& F; (\REFEXNADDR~a~\val^\ast) & (\iff F.\AMODULE.\MIEXNS[x] \neq a) \\ + \CAUGHTadm\{a~\val^n\}~\XB^l[\RETHROW~l]~\END &\stepto& + \CAUGHTadm\{a~\val^n\}~\XB^l[\val^n~(\THROWadm~a)]~\END \\ \end{array} @@ -3005,15 +2962,16 @@ When the end of a block is reached without a jump, exception, or trap aborting i Therefore, execution of a loop falls off the end, unless a backwards branch is performed explicitly. -.. index:: exception handling, throw context +.. index:: exception handling, throw context, tag, exception tag pair: handling; exception -.. _exec-catch: +.. _exec-catchadm: +.. _exec-delegateadm: Exception Handling ~~~~~~~~~~~~~~~~~~ -The following auxiliary rules define the semantics of entering and exiting exception handlers through :ref:`try ` instructions and handling thrown exceptions. +The following auxiliary rules define the semantics of entering and exiting :ref:`exception handlers ` through :ref:`try ` instructions, and handling thrown exceptions. .. _exec-handler-enter: @@ -3023,10 +2981,11 @@ Entering an exception handler :math:`H` 1. Push :math:`H` onto the stack. .. note:: - No formal reduction rule is needed for installing an exception handler + No formal reduction rule is needed for installing an exception :ref:`handler ` because it is an :ref:`administrative instruction ` that the :ref:`try ` instruction reduced to directly. + .. _exec-handler-exit: Exiting an exception handler @@ -3044,60 +3003,47 @@ When the end of a :ref:`try ` instruction is reached without a jump, 5. Push :math:`\val^m` back to the stack. -6. Jump to the position after the |END| of the originating |TRY| instruction associated with the handler :math:`H`. +6. Jump to the position after the |END| of the administrative instruction associated with the handler :math:`H`. .. math:: ~\\[-1ex] \begin{array}{lcl@{\qquad}l} - \CATCHN_m\{instr^\ast\}~\val^m~\END &\stepto& \val^m + \CATCHadm\{a^?~\instr^\ast\}^\ast~\val^m~\END &\stepto& \val^m \\ + \DELEGATEadm\{l\}~\val^m~\END &\stepto& \val^m \end{array} -.. _exec-throwaddr: - -Throwing an exception with :ref:`exception address ` :math:`a` -.............................................................................. +.. _exec-throwadm: -When a throw or a rethrow occurs, labels and call frames are popped if necessary, -until an exception handler is found on the top of the stack. +Throwing an exception with :ref:`tag address ` :math:`a` +........................................................................ -1. Assert: due to validation, :math:`S.\SEXNS[a]` exists. +**TODO: add prose** -2. Let :math:`[t^n] \to [t'^m]` be the :ref:`exception type ` :math:`S.\SEXNS[a].\EITYPE`. -3. Assert: due to :ref:`validation `, there are :math:`n` values on the top of the stack. - -4. Pop the :math:`n` values :math:`\val^n` from the stack. - -5. While the stack is not empty and the top of the stack is not an exception handler, do: - - a. Pop the top element from the stack. - -6. Assert: The stack is now either empty or there is an exception handler on the top. - - -7. If there is an exception handler :math:`\CATCHN_m\{\instr^\ast\}` on the top of the stack, then: - - a. Pop the exception handler from the stack. - - b. Let :math:`L` be the label whose arity is :math:`m` and whose continuation is the end of the |TRY| instruction associated with the handler. - - c. Push the label :math:`L` on the stack. - - d. Enter the block :math:`\instr^\ast` with label :math:`L`. +.. math:: + \begin{array}{rcl} + \CATCHadm\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast~\XT[\val^n~(\THROWadm~a)]~\END &\stepto& + \CATCHadm\{a'^?~\instr'^\ast\}^\ast~\XT[\val^n~(\THROWadm~a)]~\END \\ + && (\iff a_1^? \neq \epsilon \land a_1^? \neq a) \\ + S;~\CATCHadm\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast~\XT[\val^n~(\THROWadm~a)]~\END &\stepto& + S;~\CAUGHTadm\{a~\val^n\}~(\val^n)?~\instr^\ast~\END \\ + && (\iff~(a_1^? = \epsilon \lor a_1^? = a)~\land\\ + && \ S.\STAGS[a].\TAGITYPE = [t^n]\to[]) \\ + \LABEL_n\{\}~\XB^l[\DELEGATEadm\{l\}~\XT[\val^n~(\THROWadm~a)]~\END]~\END &\stepto& + \val^n~(\THROWadm~a) \\ + \end{array} - e. Push the :ref:`exception reference ` :math:`(\REFEXNADDR~a~\val^n)` to the stack. -8. Else the stack is empty. +.. _exec-caughtadm: -9. *TODO: return TBA administrative instruction for the unresolved throw.* +Holding a caught exception with |CAUGHTadm| +........................................... +**TODO: add prose describing the administrative** |CAUGHTadm| .. math:: \begin{array}{rcl} - S;~F;~\CATCHN_m\{\instr^\ast\}~\XT[\val^n~(\THROWADDR~a)]~\END &\stepto& - S;~F;~\LABEL_m\{\}~(\REFEXNADDR~a~\val^n)~{\instr}^\ast~\END \\ - && \hspace{-12ex} (\iff S.\SEXNS[a]=\{\ETYPE~[t^n]\to[]\}) \\ - % S;\val^n~(\THROWADDR~a) & \stepto & TBA \\ + \CAUGHTadm\{a~\val^n\}~\val^m~\END &\stepto& \val^m \end{array} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index bfcb370a..2819bb80 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -68,22 +68,22 @@ The following auxiliary typing rules specify this typing relation relative to a } -.. index:: exception type, exception address, exception tag, function type -.. _valid-externval-exn: +.. index:: tag type, tag address, exception tag, function type +.. _valid-externval-tag: -:math:`\EVEXN~a` +:math:`\EVTAG~a` ................ -* The store entry :math:`S.\SEXNS[a]` must exist. +* The store entry :math:`S.\STAGS[a]` must exist. -* Let :math:`\exntype` be the function type :math:`S.\SEXNS[a].\EITYPE`. +* Let :math:`\tagtype` be the function type :math:`S.\STAGS[a].\TAGITYPE`. -* Then :math:`\EVEXN~a` is valid with :ref:`external type ` :math:`\ETEXN~\exntype`. +* Then :math:`\EVTAG~a` is valid with :ref:`external type ` :math:`\ETTAG~\tagtype`. .. math:: \frac{ }{ - S \vdashexternval \EVEXN~a : \ETEXN~(S.\SEXNS[a].\EITYPE) + S \vdashexternval \EVTAG~a : \ETTAG~(S.\STAGS[a].\TAGITYPE) } @@ -169,32 +169,13 @@ The following auxiliary typing rules specify this typing relation relative to a } -:ref:`Exception References ` :math:`\REFEXNADDR~a~\val^n` -............................................................................ - -* The external value :math:`\EVEXN~a` must be valid with :ref:`exception type ` :math:`[t^n]\to[]`. - -* Each value :math:`val_i` in :math:`\val^n` must have type :math:`t_i` in :math:`t^n`. - -* The value is valid with :ref:`reference type ` :math:`\EXNREF`. - -.. math:: - \frac{ - S \vdashexternval \EVEXN~a : [t^n]\to[] - \qquad - (S \vdashval \val : t)^n - }{ - S \vdashval \REFEXNADDR~a~\val^n : \EXNREF - } - - .. index:: ! allocation, store, address .. _alloc: Allocation ~~~~~~~~~~ -New instances of :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`exceptions `, 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:`tags `, 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 @@ -316,29 +297,29 @@ New instances of :ref:`functions `, :ref:`tables ` -.................................. +:ref:`Tags ` +............................ -1. Let :math:`\exntype` be the :ref:`exception type ` to allocate. +1. Let :math:`\tagtype` be the :ref:`tag type ` to allocate. -2. Let :math:`a` be the first free :ref:`exception address ` in :math:`S`. +2. Let :math:`a` be the first free :ref:`tag address ` in :math:`S`. -3. Let :math:`\exninst` be the :ref:`exception instance ` :math:`\{ \EITYPE~\exntype \}`. +3. Let :math:`\taginst` be the :ref:`tag instance ` :math:`\{ \TAGITYPE~\tagtype \}`. -4. Append :math:`\exninst` to the |SEXNS| of :math:`S`. +4. Append :math:`\taginst` to the |STAGS| of :math:`S`. 5. Return :math:`a`. .. math:: \begin{array}{rlll} - \allocexn(S, \exntype) &=& S', \exnaddr \\[1ex] + \alloctag(S, \tagtype) &=& S', \tagaddr \\[1ex] \mbox{where:} \hfill \\ - \exnaddr &=& |S.\SEXNS| \\ - \exninst &=& \{ \EITYPE~\exntype \} \\ - S' &=& S \compose \{\SEXNS~\exninst\} \\ + \tagaddr &=& |S.\STAGS| \\ + \taginst &=& \{ \TAGITYPE~\tagtype \} \\ + S' &=& S \compose \{\STAGS~\taginst\} \\ \end{array} @@ -494,7 +475,7 @@ Growing :ref:`memories ` \end{array} -.. index:: module, module instance, function instance, table instance, memory instance, exception instance, global instance, export instance, function address, table address, memory address, exception address, global address, function index, table index, memory index, exception index, global index, type, function, table, memory, exception, global, import, export, external value, external type, matching +.. index:: module, module instance, function instance, table instance, memory instance, tag instance, global instance, export instance, function address, table address, memory address, tag address, global address, function index, table index, memory index, tag index, global index, type, function, table, memory, tag, global, import, export, external value, external type, matching .. _alloc-module: :ref:`Modules ` @@ -521,11 +502,11 @@ 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:`exception ` :math:`\exn_i` in :math:`\module.\MEXNS`, do: +5. For each :ref:`tag ` :math:`\tag_i` in :math:`\module.\MTAGS`, do: - a. Let :math:`\exntype` be the :ref:`exception type ` :math:`\module.\MTYPES[\exn_i.ETYPE]`. + a. Let :math:`\tagtype` be the :ref:`tag type ` :math:`\module.\MTYPES[\tag_i.\TAGTYPE]`. - b. Let :math:`\exnaddr_i` be the :ref:`exception address ` resulting from :ref:`allocating ` :math:`\exntype`. + b. Let :math:`\tagaddr_i` be the :ref:`tag address ` resulting from :ref:`allocating ` :math:`\tagtype`. 6. For each :ref:`global ` :math:`\global_i` in :math:`\module.\MGLOBALS`, do: @@ -545,7 +526,7 @@ and list of :ref:`reference ` vectors for the module's :ref:`element 11. Let :math:`\memaddr^\ast` be the concatenation of the :ref:`memory addresses ` :math:`\memaddr_i` in index order. -12. Let :math:`\exnaddr^\ast` be the concatenation of the :ref:`exception addresses ` :math:`\exnaddr_i` in index order. +12. Let :math:`\tagaddr^\ast` be the concatenation of the :ref:`tag addresses ` :math:`\tagaddr_i` in index order. 13. Let :math:`\globaladdr^\ast` be the concatenation of the :ref:`global addresses ` :math:`\globaladdr_i` in index order. @@ -559,7 +540,7 @@ and list of :ref:`reference ` vectors for the module's :ref:`element 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`. -19. Let :math:`\exnaddr_{\F{mod}}^\ast` be the list of :ref:`exception addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\exnaddr^\ast`. +19. Let :math:`\tagaddr_{\F{mod}}^\ast` be the list of :ref:`tag addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\tagaddr^\ast`. 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`. @@ -571,7 +552,7 @@ 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 an exception export for :ref:`exception index ` :math:`x`, then let :math:`\externval_i` be the :ref:`external value ` :math:`\EVEXN~(\exnaddr_{\F{mod}}^\ast[x])`. + d. Else, if :math:`\export_i` is a tag export for :ref:`tag index ` :math:`x`, then let :math:`\externval_i` be the :ref:`external value ` :math:`\EVTAG~(\tagaddr_{\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])`. @@ -579,7 +560,7 @@ and list of :ref:`reference ` vectors for the module's :ref:`element 22. Let :math:`\exportinst^\ast` be the concatenation of the :ref:`export instances ` :math:`\exportinst_i` in index order. -23. Let :math:`\moduleinst` be the :ref:`module instance ` :math:`\{\MITYPES~(\module.\MTYPES),` :math:`\MIFUNCS~\funcaddr_{\F{mod}}^\ast,` :math:`\MITABLES~\tableaddr_{\F{mod}}^\ast,` :math:`\MIMEMS~\memaddr_{\F{mod}}^\ast,` :math:`\MIEXNS~\exnaddr_{\F{mod}}^\ast`, :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIEXPORTS~\exportinst^\ast\}`. +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:`\MITAGS~\tagaddr_{\F{mod}}^\ast`, :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIEXPORTS~\exportinst^\ast\}`. 24. Return :math:`\moduleinst`. @@ -606,7 +587,7 @@ where: \MIFUNCS~\evfuncs(\externval_{\F{im}}^\ast)~\funcaddr^\ast, \\ \MITABLES~\evtables(\externval_{\F{im}}^\ast)~\tableaddr^\ast, \\ \MIMEMS~\evmems(\externval_{\F{im}}^\ast)~\memaddr^\ast, \\ - \MIEXNS~\evexns(\externval_{\F{im}}^\ast)~\exnaddr^\ast, \\ + \MITAGS~\evtags(\externval_{\F{im}}^\ast)~\tagaddr^\ast, \\ \MIGLOBALS~\evglobals(\externval_{\F{im}}^\ast)~\globaladdr^\ast, \\ \MIELEMS~\elemaddr^\ast, \\ \MIDATAS~\dataaddr^\ast, \\ @@ -619,8 +600,8 @@ where: \quad (\where (\table.\TTYPE)^\ast = (\limits~t)^\ast) \\ S_3, \memaddr^\ast &=& \allocmem^\ast(S_2, (\mem.\MTYPE)^\ast) \\ - S_4, \exnaddr^\ast &=& \allocexn^\ast(S_3, \exn^\ast, \module) - \quad (\where \exn^\ast = \module.\MEXNS) \\ + S_4, \tagaddr^\ast &=& \alloctag^\ast(S_3, \tag^\ast, \module) + \quad (\where \tag^\ast = \module.\MTAGS) \\ S_5, \globaladdr^\ast &=& \allocglobal^\ast(S_4, (\global.\GTYPE)^\ast, \val^\ast) \\ S_6, \elemaddr^\ast &=& @@ -635,8 +616,8 @@ where: \qquad (\where x^\ast = \edtables(\export^\ast)) \\ \evmems(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIMEMS[x])^\ast \qquad (\where x^\ast = \edmems(\export^\ast)) \\ - \evexns(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIEXNS[x])^\ast - \qquad\!\!\! (\where x^\ast = \edexns(\export^\ast)) \\ + \evtags(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MITAGS[x])^\ast + \qquad\!\!\! (\where x^\ast = \edtags(\export^\ast)) \\ \evglobals(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIGLOBALS[x])^\ast \qquad\!\!\! (\where x^\ast = \edglobals(\export^\ast)) \\ \end{array} diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index f09471b0..422da4d9 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, vector type, reference type, ! host address, ! exception address, value type, integer, floating-point, vector number, ! default value, embedder +.. index:: ! value, number, reference, constant, number type, vector type, reference type, ! host address, ! value type, integer, floating-point, vector number, ! default value, embedder pair: abstract syntax; value .. _syntax-num: .. _syntax-vecc: @@ -26,7 +26,6 @@ It is convenient to reuse the same notation as for the |CONST| :ref:`instruction References other than null are represented with additional :ref:`administrative instructions `. They either are *function references*, pointing to a specific :ref:`function address `, -*exception references* representing a caught exception pointing to a specific :ref:`exception address ` and carrying a sequence of :ref:`values `, or *external references* pointing to an uninterpreted form of :ref:`extern address ` that can be defined by the :ref:`embedder ` to represent its own objects. .. math:: @@ -41,8 +40,7 @@ or *external references* pointing to an uninterpreted form of :ref:`extern addre \production{(reference)} & \reff &::=& \REFNULL~t \\&&|& \REFFUNCADDR~\funcaddr \\&&|& - \REFEXTERNADDR~\externaddr \\&&|& - \REFEXNADDR~\exnaddr~\val^\ast \\ + \REFEXTERNADDR~\externaddr \\ \production{(value)} & \val &::=& \num ~|~ \vecc ~|~ \reff \\ \end{array} @@ -85,11 +83,13 @@ It is either a sequence of :ref:`values ` or a :ref:`trap `, :ref:`tables `, :ref:`memories `, :ref:`exceptions `, and :ref:`globals `, :ref:`element segments `, and :ref:`data segments ` that have been :ref:`allocated ` during the life time of the abstract machine. [#gc]_ +It consists of the runtime representation of all *instances* of :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`tags `, 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. @@ -111,7 +111,7 @@ Syntactically, the store is defined as a :ref:`record ` listing \SFUNCS & \funcinst^\ast, \\ \STABLES & \tableinst^\ast, \\ \SMEMS & \meminst^\ast, \\ - \SEXNS & \exninst^\ast, \\ + \STAGS & \taginst^\ast, \\ \SGLOBALS & \globalinst^\ast, \\ \SELEMS & \eleminst^\ast, \\ \SDATAS & \datainst^\ast ~\} \\ @@ -130,11 +130,11 @@ Convention * The meta variable :math:`S` ranges over stores where clear from context. -.. index:: ! address, store, function instance, table instance, memory instance, exception instance, global instance, element instance, data instance, embedder +.. index:: ! address, store, function instance, table instance, memory instance, tag instance, global instance, element instance, data instance, embedder pair: abstract syntax; function address pair: abstract syntax; table address pair: abstract syntax; memory address - pair: abstract syntax; exception address + pair: abstract syntax; tag address pair: abstract syntax; global address pair: abstract syntax; element address pair: abstract syntax; data address @@ -142,7 +142,7 @@ Convention pair: function; address pair: table; address pair: memory; address - pair: exception; address + pair: tag; address pair: global; address pair: element; address pair: data; address @@ -150,7 +150,7 @@ Convention .. _syntax-funcaddr: .. _syntax-tableaddr: .. _syntax-memaddr: -.. _syntax-exnaddr: +.. _syntax-tagaddr: .. _syntax-globaladdr: .. _syntax-elemaddr: .. _syntax-dataaddr: @@ -160,7 +160,7 @@ Convention Addresses ~~~~~~~~~ -:ref:`Function instances `, :ref:`table instances `, :ref:`memory instances `, :ref:`exception instances `, :ref:`global instances `, :ref:`element instances `, and :ref:`data instances ` in the :ref:`store ` are referenced with abstract *addresses*. +:ref:`Function instances `, :ref:`table instances `, :ref:`memory instances `, :ref:`tag 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*. @@ -174,7 +174,7 @@ In addition, an :ref:`embedder ` may supply an uninterpreted set of *h \addr \\ \production{(memory address)} & \memaddr &::=& \addr \\ - \production{(exception address)} & \exnaddr &::=& + \production{(tag address)} & \tagaddr &::=& \addr \\ \production{(global address)} & \globaladdr &::=& \addr \\ @@ -201,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, exception instance, global instance, element instance, data instance, export instance, table address, memory address, exception address, global address, element address, data address, index, name +.. index:: ! instance, function type, function instance, table instance, memory instance, tag instance, global instance, element instance, data instance, export instance, table address, memory address, tag address, global address, element address, data address, index, name pair: abstract syntax; module instance pair: module; instance .. _syntax-moduleinst: @@ -221,7 +221,7 @@ and collects runtime representations of all entities that are imported, defined, \MIFUNCS & \funcaddr^\ast, \\ \MITABLES & \tableaddr^\ast, \\ \MIMEMS & \memaddr^\ast, \\ - \MIEXNS & \exnaddr^\ast, \\ + \MITAGS & \tagaddr^\ast, \\ \MIGLOBALS & \globaladdr^\ast, \\ \MIELEMS & \elemaddr^\ast, \\ \MIDATAS & \dataaddr^\ast, \\ @@ -230,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 `, :ref:`exception 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:`tag 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 `. @@ -315,26 +315,23 @@ The bytes can be mutated through :ref:`memory instructions It is an invariant of the semantics that the length of the byte vector, divided by page size, never exceeds the maximum size of :math:`\memtype`, if present. -.. index:: ! exception instance, exception, exception tag, exception type - pair: abstract syntax; exception instance - pair: exception; instance -.. _syntax-exninst: +.. index:: ! tag instance, tag, exception tag, tag type + pair: abstract syntax; tag instance + pair: tag; instance +.. _syntax-taginst: -Exception Instances -~~~~~~~~~~~~~~~~~~~ +Tag Instances +~~~~~~~~~~~~~ -An *exception instance* is the runtime representation of an :ref:`exception ` definition. -It records the :ref:`type ` of the exception. +A *tag instance* is the runtime representation of a :ref:`tag ` definition. +It records the :ref:`type ` of the tag. .. math:: \begin{array}{llll} - \production{(exception instance)} & \exninst &::=& - \{ \EITYPE~\exntype \} \\ + \production{(tag instance)} & \taginst &::=& + \{ \TAGITYPE~\tagtype \} \\ \end{array} -.. note:: - The :ref:`exception address ` of an exception instance is also called an *exception tag*. - .. index:: ! global instance, global, value, mutability, instruction, embedder pair: abstract syntax; global instance @@ -412,7 +409,7 @@ It defines the export's :ref:`name ` and the associated :ref:`exter \end{array} -.. index:: ! external value, function address, table address, memory address, exception address, global address, store, function, table, memory, exception, global +.. index:: ! external value, function address, table address, memory address, tag address, global address, store, function, table, memory, tag, global pair: abstract syntax; external value pair: external; value .. _syntax-externval: @@ -421,7 +418,7 @@ External Values ~~~~~~~~~~~~~~~ An *external value* is the runtime representation of an entity that can be imported or exported. -It is an :ref:`address ` denoting either a :ref:`function instance `, :ref:`table instance `, :ref:`memory instance `, :ref:`global instances `, or :ref:`exception instances ` in the shared :ref:`store `. +It is an :ref:`address ` denoting either a :ref:`function instance `, :ref:`table instance `, :ref:`memory instance `, :ref:`tag instances `, or :ref:`global instances ` in the shared :ref:`store `. .. math:: \begin{array}{llcl} @@ -429,7 +426,7 @@ It is an :ref:`address ` denoting either a :ref:`function instance \EVFUNC~\funcaddr \\&&|& \EVTABLE~\tableaddr \\&&|& \EVMEM~\memaddr \\&&|& - \EVEXN~\exnaddr \\&&|& + \EVTAG~\tagaddr \\&&|& \EVGLOBAL~\globaladdr \\ \end{array} @@ -446,7 +443,7 @@ It filters out entries of a specific kind in an order-preserving fashion: * :math:`\evmems(\externval^\ast) = [\memaddr ~|~ (\EVMEM~\memaddr) \in \externval^\ast]` -* :math:`\evexns(\externval^\ast) = [\exnaddr ~|~ (\EVEXN~\exnaddr) \in \externval^\ast]` +* :math:`\evtags(\externval^\ast) = [\tagaddr ~|~ (\EVTAG~\tagaddr) \in \externval^\ast]` * :math:`\evglobals(\externval^\ast) = [\globaladdr ~|~ (\EVGLOBAL~\globaladdr) \in \externval^\ast]` @@ -458,7 +455,6 @@ It filters out entries of a specific kind in an order-preserving fashion: pair: abstract syntax; handler .. _syntax-frame: .. _syntax-label: -.. _syntax-catch: .. _frame: .. _label: .. _handler: @@ -535,21 +531,31 @@ and a reference to the function's own :ref:`module instance ` The values of the locals are mutated by respective :ref:`variable instructions `. +.. _syntax-handler: + Exception handlers .................. -Like labels, exception handlers carry the return arity :math:`n` of the -respective |TRY| block, and their associated branch *target*, which is -expressed syntactically as an :ref:`instruction ` sequence: +Exception handlers are installed by |TRY| instructions and are either *catching handlers* or *delegating handlers*. + +Catching handlers start with the identifier |CATCHadm| and carry a mapping from :ref:`tag addresses ` +to their associated branch *targets*, each of which is expressed syntactically as a possibly empty sequence of +:ref:`instructions ` possibly following a :ref:`tag address `. +If there is no :ref:`tag address `, the instructions of that target correspond to a |CATCHALL| clause. + +**TODO: add prose** for delegating handlers. .. math:: - \begin{array}{llll} - \production{(handler)} & \X{handler} &::=& - \CATCH_n\{\instr^\ast\}\\ + \begin{array}{llllll} + \production{(handler)} & \X{handler} &::=& \CATCHadm\{a^?~\instr^\ast\}^\ast &|& \DELEGATEadm\{l\} \end{array} -Intuitively, :math:`\instr^\ast` is the *continuation* to execute +Intuitively, :math:`\CATCHadm\{a^?~\instr^\ast\}^\ast` maps exception tag addreses to possible *continuations* to execute when the handler catches a thrown exception. +If this list of targets is empty, or if the tag address of the thrown exception is not in the handler's mapping and there is no |CATCHALL| clause, then the exception will be rethrown. + +**TODO: add prose** with intuition on delegating handlers. + .. _exec-expand: @@ -560,6 +566,8 @@ Conventions * The meta variable :math:`F` ranges over frames where clear from context. +* The meta variable :math:`H` ranges over exception handlers where clear from context. + * The following auxiliary definition takes a :ref:`block type ` and looks up the :ref:`function type ` that it denotes in the current frame: .. math:: @@ -569,14 +577,15 @@ 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, exception, exception instance, exception address, exception, reftype +.. index:: ! administrative instructions, function, function instance, function address, label, frame, instruction, trap, call, memory, memory instance, table, table instance, element, data, segment, tag, tag instance, tag address, exceptions, reftype, catch, delegate, handler, caught pair:: abstract syntax; administrative instruction .. _syntax-trap: .. _syntax-reffuncaddr: .. _syntax-invoke: -.. _syntax-refexnaddr: -.. _syntax-throwaddr: -.. _syntax-catchn: +.. _syntax-throwadm: +.. _syntax-catchadm: +.. _syntax-delegateadm: +.. _syntax-caughtadm: .. _syntax-instr-admin: Administrative Instructions @@ -585,7 +594,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 `, :ref:`exception handling `, and :ref:`control instructions `, the syntax of instructions is extended to include the following *administrative instructions*: +In order to express the reduction of :ref:`traps `, :ref:`calls `, :ref:`exception handling `, and :ref:`control instructions `, the syntax of instructions is extended to include the following *administrative instructions*: .. math:: \begin{array}{llcl} @@ -595,27 +604,27 @@ In order to express the reduction of :ref:`traps `, :ref:`calls `. Similarly, |REFEXTERNADDR| represents :ref:`external references `, -and |REFEXNADDR| represents :ref:`exception reference values ` of caught exceptions. +The |REFFUNCADDR| instruction represents :ref:`function reference values `. Similarly, |REFEXTERNADDR| represents :ref:`external references `. 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 |THROWADDR| instruction represents the imminent throw of an :ref:`exception reference value ` based on an :ref:`exception instance `, identified by its :ref:`address `. -The values it will consume to create the exception depend on its :ref:`exception type `. +The |THROWadm| instruction represents the imminent throw of an exception based on a :ref:`tag instance `, identified by its :ref:`address `. +The values it will consume depend on its :ref:`tag type `. It unifies the throwing of different forms of exceptions. -The |LABEL|, |FRAME|, and |CATCHN| instructions model :ref:`labels `, :ref:`frames `, and active :ref:`exception handlers `, respectively, :ref:`"on the stack" `. +The |LABEL|, |FRAME|, |CATCHadm|, |DELEGATEadm|, and |CAUGHTadm| instructions model :ref:`labels `, :ref:`frames `, active :ref:`catching exception handlers `, active :ref:`delegating exception handlers `, and :ref:`caught exceptions `, 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. @@ -666,6 +675,16 @@ In order to specify the reduction of :ref:`branches `, the This definition allows to index active labels surrounding a :ref:`branch ` or :ref:`return ` instruction. +In order to be able to break jumping over exception handlers and caught exceptions, we must allow for these new structured administrative control instructions to appear after labels in block contexts, by extending block context as follows. + +.. math:: + \begin{array}{llll} + \production{(block contexts)} & \XC^{k} &::=& \handler~\XB^k~\END \\ + & & | & \CAUGHTadm~\{\tagaddr~\val^\ast\}~\XB^k~\END \\ + \production{(block contexts)} & \XB^0 &::=& \dots ~|~ \val^\ast~\XC^0~\instr^\ast\\ + \production{(block contexts)} & \XB^{k+1} &::=& \dots ~|~ \val^\ast~\XC^{k+1}~\instr^\ast \\ + \end{array} + .. note:: For example, the :ref:`reduction ` of a simple branch can be defined as follows: @@ -678,14 +697,14 @@ This definition allows to index active labels surrounding a :ref:`branch ` :math:`l`, which corresponds to the number of surrounding |LABEL| instructions that must be hopped over -- which is exactly the count encoded in the index of a block context. -.. index:: ! throw context, exception, throw address, catch block +.. index:: ! throw context, tag, throw address, catch block, handler, exception .. _syntax-ctxt-throw: Throw Contexts .............. In order to specify the reduction of |TRY| blocks -with the help of the administrative instructions |THROWADDR|, |REFEXNADDR|, and |CATCHN|, +with the help of the administrative instructions |THROWadm|, |CATCHadm|, |DELEGATEadm|, and |CAUGHTadm|, the following syntax of *throw contexts* is defined, as well as associated structural rules: .. math:: @@ -693,36 +712,41 @@ the following syntax of *throw contexts* is defined, as well as associated struc \production{(throw contexts)} & \XT &::=& \val^\ast~[\_]~\instr^\ast \\ &&|& \LABEL_n\{\instr^\ast\}~\XT~\END \\ &&|& - \CATCHN_n\{\instr^\ast\}~\XT~\END \\ &&|& + \CAUGHTadm\{a~\val^\ast\}~\XT~\END \\ &&|& \FRAME_n\{F\}~\XT~\END \\ \end{array} -Throw contexts allow matching the program context around a throw instruction up to the nearest enclosing :math:`\CATCHN` handler, thereby selecting the exception handler responsible for an exception. +Throw contexts allow matching the program context around a throw instruction up to the innermost enclosing |CATCHadm| or |DELEGATEadm|, thereby selecting the exception |handler| responsible for an exception, if one exists. + +.. note:: + Contrary to block contexts, throw contexts don't skip over handlers. + + Since handlers are not included above, there is always a unique maximal throw context to match the reduction rules. + This basically means that :math:`\CAUGHTadm {..} instr^\ast \END` is not a potential catching block for exceptions thrown by :math:`\instr^\ast`, since it is inside a |handler|'s block. .. note:: - For example, catching a simple :ref:`throw ` in a :ref:`try block ` would be as follows. + For example, catching a simple :ref:`throw ` in a :ref:`try block ` would be as follows. .. math:: \begin{array}{ll} - & \hspace{-5ex} S;~F;~\val^n~(\TRY~\X{bt}~\THROW~x~\CATCH~\RETURN~\END) \\ - \stepto & S;~F;~\CATCHN_1\{\RETURN\}~(\LABEL_1 \{\}~\val^n~\THROWADDR~a~\END)~\END \\ + & \hspace{-5ex} S;~F;~\val^n~(\TRY~\X{bt}~\THROW~x~\CATCH~x~\RETURN~\END) \\ + \stepto & S;~F;~\LABEL_n\{\} (\CATCHadm\{a~\RETURN\}~~\val^n~\THROWadm~a~\END)~\END \\ \end{array} - :ref:`Handling ` the thrown exception address :math:`a` in the throw context - :math:`T=\LABEL_1 \{\}[\_]~\END`, with the exception handler :math:`\CATCHN_1\{\RETURN\}` gives: + :ref:`Handling ` the thrown exception with tag address :math:`a` in the throw context + :math:`T=[\_]`, with the exception handler :math:`H=\CATCHadm\{a~\RETURN\}` gives: .. math:: \begin{array}{lll} - \stepto & S;~F;~\LABEL_1~\{\}~(\REFEXNADDR~a~\val^n)~\RETURN~\END & \hspace{9ex}\ \\ - \stepto & (\REFEXNADDR~a~\val^n) & \\ + \stepto & S;~F;~\LABEL_n\{\}~(\CAUGHTadm\{a~\val^n\}~\val^n~\RETURN~\END)~\END & \hspace{9ex}\ \\ + \stepto & \val^n & \\ \end{array} When a throw occurs, execution halts until that throw is the continuation of a throw context in a catching try block. - In this particular case, the exception reference is returned normally, as opposed to being thrown as the result of a plain - :math:`\THROW~x` without a catching |TRY| block. + In this particular case, the exception is caught by the exception handler :math:`H` and its values are returned. - *(TODO: add administrative values to describe unresolved throws).* + **TODO: add administrative values to describe unresolved throws:** e.g., |EXCEPTION| .. index:: ! configuration, ! thread, store, frame, instruction, module instruction @@ -780,7 +804,7 @@ Finally, the following definition of *evaluation context* and associated structu Reduction terminates when a thread's instruction sequence has been reduced to a :ref:`result `, that is, either a sequence of :ref:`values ` or to a |TRAP|. -*(TODO: add rules to deal with unresolved* :math:`\THROWADDR~\exnaddr`, *and extend results to include such situations.)* +**TODO: add rules to deal with unresolved** :math:`\THROWadm~\tagaddr`, **and extend results to include such situations.** (e.g., |EXCEPTION|) .. 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/syntax/instructions.rst b/document/core/syntax/instructions.rst index 35521033..73781223 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -603,7 +603,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, exception index, vector, trap, function, table, exception, function type, value type, type index, exception index +.. index:: ! control instruction, ! structured control, ! exception handling, ! label, ! block, ! block type, ! branch, result type, label index, function index, type index, tag index, vector, trap, function, table, tag, function type, value type, tag type, try block, catching try block pair: abstract syntax; instruction pair: abstract syntax; block type pair: block; type @@ -614,9 +614,10 @@ The |DATADROP| instruction prevents further use of a passive data segment. This .. _syntax-loop: .. _syntax-if: .. _syntax-try: +.. _syntax-try-catch: +.. _syntax-try-delegate: .. _syntax-throw: .. _syntax-rethrow: -.. _syntax-br_on_exn: .. _syntax-br: .. _syntax-br_if: .. _syntax-br_table: @@ -642,10 +643,10 @@ Instructions in this group affect the flow of control. \BLOCK~\blocktype~\instr^\ast~\END \\&&|& \LOOP~\blocktype~\instr^\ast~\END \\&&|& \IF~\blocktype~\instr^\ast~\ELSE~\instr^\ast~\END \\&&|& - \TRY~\blocktype~instr^\ast~\CATCH~\instr^\ast~\END \\&&|& - \THROW~\exnidx \\&&|& - \RETHROW \\&&|& - \BRONEXN~\labelidx~\exnidx \\&&|& + \TRY~\blocktype~instr^\ast~(\CATCH~\tagidx~\instr^\ast)^\ast~(\CATCHALL~\instr^\ast)^?~\END \\ &&|& + \TRY~\blocktype~instr^\ast~\DELEGATE~\labelidx \\ &&|& + \THROW~\tagidx \\&&|& + \RETHROW~\labelidx \\ &&|& \BR~\labelidx \\&&|& \BRIF~\labelidx \\&&|& \BRTABLE~\vec(\labelidx)~\labelidx \\&&|& @@ -659,11 +660,15 @@ The |NOP| instruction does nothing. The |UNREACHABLE| instruction causes an unconditional :ref:`trap `. 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. +They bracket nested sequences of instructions, called *blocks*, +separated by either |ELSE|, |CATCH|, or |CATCHALL| pseudo-instructions, +and terminated with either an |END| or a |DELEGATE| pseudo-instruction. As the grammar prescribes, they must be well-nested. -The instructions |TRY|, |THROW|, |RETHROW|, and |BRONEXN| are concerned with handling exceptions. -The |THROW| and |RETHROW| instructions alter control flow by searching for the catching-try block, if any. +The instructions |TRY|, |THROW|, and |RETHROW|, are concerned with handling exceptions. +The |TRY| instructions create try-blocks, and either may handle or rethrow exceptions in the case of |CATCH| and |CATCHALL|, +or delegate exceptions to an outer potentially catching try-block in the case of |DELEGATE|. +The |THROW| and |RETHROW| instructions alter control flow by searching for a matching handler in an enclosing 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^?]`. @@ -680,6 +685,7 @@ The exact effect depends on that control construct. In case of |BLOCK| or |IF| it is a *forward jump*, resuming execution after the matching |END|. In case of |LOOP| it is a *backward jump* to the beginning of the loop. +**TODO: add prose** - for try-delegate's jump. .. note:: This enforces *structured control flow*. @@ -689,8 +695,8 @@ In case of |LOOP| it is a *backward jump* to the beginning of the loop. Branch instructions come in several flavors: |BR| performs an unconditional branch, |BRIF| performs a conditional branch, -|BRONEXN| performs a branch if the exception on the stack matches the specified exception index, and |BRTABLE| performs an indirect branch through an operand indexing into the label vector that is an immediate to the instruction, or to a default target if the operand is out of bounds. + The |RETURN| instruction is a shortcut for an unconditional branch to the outermost block, which implicitly is the body of the current function. Taking a branch *unwinds* the operand stack up to the height where the targeted structured control instruction was entered. However, branches may additionally consume operands themselves, which they push back on the operand stack after unwinding. diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst index 75140963..9de07a56 100644 --- a/document/core/syntax/modules.rst +++ b/document/core/syntax/modules.rst @@ -1,4 +1,4 @@ -.. index:: ! module, type definition, function type, exception type, function, table, memory, exception, global, element, data, start function, import, export +.. index:: ! module, type definition, function type, tag type, function, table, memory, tag, 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 `, :ref:`exceptions `, and :ref:`globals `. +A module collects definitions for :ref:`types `, :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`tags `, 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,7 +18,7 @@ and provide initialization in the form of :ref:`data ` and :ref:`el \MFUNCS~\vec(\func), \\&&&& \MTABLES~\vec(\table), \\&&&& \MMEMS~\vec(\mem), \\&&&& - \MEXNS~\vec(\exn), \\&&&& + \MTAGS~\vec(\tag), \\&&&& \MGLOBALS~\vec(\global), \\&&&& \MELEMS~\vec(\elem), \\&&&& \MDATAS~\vec(\data), \\&&&& @@ -30,12 +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, ! exception index, ! global index, ! local index, ! label index, ! element index, ! data index, function, global, table, memory, exception, element, data, local, parameter, import +.. index:: ! index, ! index space, ! type index, ! function index, ! table index, ! memory index, ! tag index, ! global index, ! local index, ! label index, ! element index, ! data index, function, global, table, memory, tag, element, data, local, parameter, import pair: abstract syntax; type index pair: abstract syntax; function index pair: abstract syntax; table index pair: abstract syntax; memory index - pair: abstract syntax; exception index + pair: abstract syntax; tag index pair: abstract syntax; global index pair: abstract syntax; element index pair: abstract syntax; data index @@ -45,7 +45,7 @@ Each of the vectors -- and thus the entire module -- may be empty. pair: function; index pair: table; index pair: memory; index - pair: exception; index + pair: tag; index pair: global; index pair: element; index pair: data; index @@ -55,7 +55,7 @@ Each of the vectors -- and thus the entire module -- may be empty. .. _syntax-funcidx: .. _syntax-tableidx: .. _syntax-memidx: -.. _syntax-exnidx: +.. _syntax-tagidx: .. _syntax-globalidx: .. _syntax-elemidx: .. _syntax-dataidx: @@ -75,7 +75,7 @@ Each class of definition has its own *index space*, as distinguished by the foll \production{function index} & \funcidx &::=& \u32 \\ \production{table index} & \tableidx &::=& \u32 \\ \production{memory index} & \memidx &::=& \u32 \\ - \production{exception index} & \exnidx &::=& \u32 \\ + \production{tag index} & \tagidx &::=& \u32 \\ \production{global index} & \globalidx &::=& \u32 \\ \production{element index} & \elemidx &::=& \u32 \\ \production{data index} & \dataidx &::=& \u32 \\ @@ -83,7 +83,7 @@ Each class of definition has its own *index space*, as distinguished by the foll \production{label index} & \labelidx &::=& \u32 \\ \end{array} -The index space for :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`exceptions `, and :ref:`globals ` includes respective :ref:`imports ` declared in the same module. +The index space for :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`tags `, and :ref:`globals ` includes respective :ref:`imports ` declared in the same module. The indices of these imports precede the indices of other definitions in the same index space. Element indices reference :ref:`element segments ` and data indices reference :ref:`data segments `. @@ -97,7 +97,7 @@ Label indices reference :ref:`structured control instructions `, -starting with the smallest index not referencing an exception :ref:`import `. +Tags are referenced through :ref:`tag indices `, +starting with the smallest index not referencing a tag :ref:`import `. .. index:: ! global, global index, global type, mutability, expression, constant, value, import @@ -358,11 +358,12 @@ The |MSTART| component of a module declares the :ref:`function index `. -Exportable definitions are :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`exceptions `, and :ref:`globals `, +Exportable definitions are :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`tags `, and :ref:`globals `, which are referenced through a respective descriptor. @@ -400,18 +401,18 @@ The following auxiliary notation is defined for sequences of exports, filtering * :math:`\edmems(\export^\ast) = [\memidx ~|~ \EDMEM~\memidx \in (\export.\EDESC)^\ast]` -* :math:`\edexns(\export^\ast) = [\exnidx ~|~ \EDEXN~\exnidx \in (\export.\EDESC)^\ast]` +* :math:`\edtags(\export^\ast) = [\tagidx ~|~ \EDTAG~\tagidx \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, exception type, index space, type index, function index, table index, memory index, global index, exception index, function, table, memory, exception, global, instantiation +.. index:: ! import, name, function type, table type, memory type, global type, tag type, index space, type index, function index, table index, memory index, global index, tag index, function, table, memory, tag, global, instantiation pair: abstract syntax; import single: function; import single: table; import single: memory; import single: global; import - single: exception; import + single: tag; import .. _syntax-importdesc: .. _syntax-import: @@ -428,12 +429,12 @@ The |MIMPORTS| component of a module defines a set of *imports* that are require \IDFUNC~\typeidx \\&&|& \IDTABLE~\tabletype \\&&|& \IDMEM~\memtype \\&&|& - \IDEXN~\exntype \\&&|& + \IDTAG~\tagtype \\&&|& \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 `, :ref:`exceptions `, and :ref:`globals `. +Importable definitions are :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`tags `, 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 ab9f1ac5..3723bc67 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -72,7 +72,7 @@ Conventions * The notation :math:`|t|` for :ref:`bit width ` extends to vector types as well, that is, :math:`|\V128| = 128`. -.. index:: ! reference type, reference, table, function, function type, exception, exception type, null +.. index:: ! reference type, reference, table, function, function type, null pair: abstract syntax; reference type pair: reference; type .. _syntax-reftype: @@ -85,13 +85,11 @@ Reference Types .. math:: \begin{array}{llll} \production{reference type} & \reftype &::=& - \FUNCREF ~|~ \EXNREF ~|~ \EXTERNREF \\ + \FUNCREF ~|~ \EXTERNREF \\ \end{array} The type |FUNCREF| denotes the infinite union of all references to :ref:`functions `, regardless of their :ref:`function types `. -The type |EXNREF| denotes a caught :ref:`exception `. - The type |EXTERNREF| denotes the infinite union of all references to objects owned by the :ref:`embedder ` and that can be passed into WebAssembly under this type. Reference types are *opaque*, meaning that neither their size nor their bit pattern can be observed. @@ -223,26 +221,28 @@ The limits are given in numbers of entries. In future versions of WebAssembly, additional element types may be introduced. -.. index:: ! exception, exception type, function type - pair: abstract syntax; exception - single: exception; type -.. _syntax-exntype: +.. index:: ! tag, tag type, function type, exception tag + pair: abstract syntax; tag + pair: tag; exception tag + single: tag; type; exception +.. _syntax-tagtype: -Exception Types -~~~~~~~~~~~~~~~ +Tag Types +~~~~~~~~~ -*Exception types* classify the signature of :ref:`exceptions ` with a function type. +*Tag types* classify the signature of :ref:`tags ` with a function type. .. math:: \begin{array}{llll} - \production{exception type} &\exntype &::=& \functype \\ + \production{tag type} &\tagtype &::=& \functype \\ \end{array} -The parameters of |functype| define the list of values associated with the exception. -Furthermore, it is an invariant of the semantics that every |functype| in a :ref:`valid ` exception type has an empty result type. +Currently tags are only used for categorising exceptions. +The parameters of |functype| define the list of values associated with the exception thrown with this tag. +Furthermore, it is an invariant of the semantics that every |functype| in a :ref:`valid ` tag type for an exception has an empty result type. .. note:: - Future versions of WebAssembly may allow non-empty result types in exceptions. + Future versions of WebAssembly may have additional uses for tags, and may allow non-empty result types in the function types of tags. .. index:: ! global type, ! mutability, value type, global, mutability @@ -268,7 +268,7 @@ Global Types \end{array} -.. index:: ! external type, function type, table type, memory type, exception type, global type, import, external value +.. index:: ! external type, function type, table type, memory type, tag type, global type, import, external value pair: abstract syntax; external type pair: external; type .. _syntax-externtype: @@ -284,7 +284,7 @@ External Types \ETFUNC~\functype ~|~ \ETTABLE~\tabletype ~|~ \ETMEM~\memtype ~|~ - \ETEXN~\exntype ~|~ + \ETTAG~\tagtype ~|~ \ETGLOBAL~\globaltype \\ \end{array} @@ -301,6 +301,6 @@ It filters out entries of a specific kind in an order-preserving fashion: * :math:`\etmems(\externtype^\ast) = [\memtype ~|~ (\ETMEM~\memtype) \in \externtype^\ast]` -* :math:`\etexns(\externtype^\ast) = [\exntype ~|~ (\ETEXN~\exntype) \in \externtype^\ast]` +* :math:`\ettags(\externtype^\ast) = [\tagtype ~|~ (\ETTAG~\tagtype) \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 29ec2cfa..22bad290 100644 --- a/document/core/text/conventions.rst +++ b/document/core/text/conventions.rst @@ -123,7 +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}`, :math:`\T{else}`, and :math:`\T{catch}` +The same label identifier may optionally be repeated after the corresponding :math:`\T{end}`, :math:`\T{else}`, :math:`\T{catch}`, :math:`\T{catch\_all}`, and :math:`\T{delegate}` 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 `. @@ -86,10 +86,15 @@ However, the special case of a type use that is syntactically empty or consists \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) \\ &&|& - \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) \\ + \text{try}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}_1{:}\Tinstr_{I'})^\ast~~ + (\text{catch}~~\Tid_1^?~~x{:}\Ttagidx_I~~(\X{in}_2{:}\Tinstr_{I'})^\ast)^\ast~~ + \\ &&&\qquad\qquad (\text{catch\_all}~~\Tid_1^?~~(\X{in}_3{:}\Tinstr_{I'})^\ast)^?~~\text{end}~~\Tid_2^? + \\ &&&\qquad \Rightarrow\quad \TRY~\X{rt}~\X{in}_1^\ast~(\CATCH~x~\X{in}_2^\ast)^\ast~(\CATCHALL~\X{in}_3^\ast)^?~\END + \\ &&&\qquad\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{delegate}~~l{:}\Tlabelidx_I~~\X{l}{:}\Tlabelidx_I + \\ &&&\qquad \Rightarrow\quad \TRY~\X{rt}~\X{in}_1^\ast~\DELEGATE~l + \qquad\quad~~ (\iff \Tid^? = \epsilon \vee \Tid^? = \Tlabel) \\ \end{array} .. note:: @@ -100,7 +105,6 @@ However, the special case of a type use that is syntactically empty or consists .. _text-unreachable: .. _text-throw: .. _text-rethrow: -.. _text-br_on_exn: .. _text-br: .. _text-br_if: .. _text-br_table: @@ -115,9 +119,8 @@ All other control instruction are represented verbatim. \production{plain instruction} & \Tplaininstr_I &::=& \text{unreachable} &\Rightarrow& \UNREACHABLE \\ &&|& \text{nop} &\Rightarrow& \NOP \\ &&|& - \text{throw}~~\text{(}\text{exception}~x{:}\Texnidx_I\text{)} &\Rightarrow& \THROW~x \\ &&|& - \text{rethrow} &\Rightarrow& \RETHROW \\ &&|& - \text{br\_on\_exn}~~l{:}\Tlabelidx_I~~\text{(}\text{exception}~x{:}\Texnidx_I~\text{)} &\Rightarrow& \BRONEXN~l~x \\ &&|& + \text{throw}~~x{:}\Ttagidx_I &\Rightarrow& \THROW~x \\ &&|& + \text{rethrow}~~l{:}\Tlabelidx_I &\Rightarrow& \RETHROW~l \\ &&|& \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 @@ -926,14 +929,18 @@ Such a folded instruction can appear anywhere a regular instruction can. \text{(}~\text{block}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~\text{)} &\equiv\quad \text{block}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{end} \\ & \text{(}~\text{loop}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~\text{)} - &\equiv\quad \text{loop}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{end} \\ & + &\equiv\quad \text{loop}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{end} \\ + \end{array}\\ + \begin{array}{lr} \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} \\ & + \text{(}~\text{then}~~\Tinstr_1^\ast~\text{)}~~\text{(}~\text{else}~~\Tinstr_2^\ast~\text{)}^?~~\text{)} + & \equiv \\ + \qquad \Tfoldedinstr^\ast~~\text{if}~~\Tlabel~~\Tblocktype \Tinstr_1^\ast~~\text{else}~~(\Tinstr_2^\ast)^?~\text{end} &\\ \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do}~~\Tinstr_1^\ast~~\text{)} - &\hspace{-8ex} \text{(}~\text{catch}~~\Tinstr_2^\ast~\text{)}~\text{)} \quad\equiv \\ &\qquad - \text{try}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast & \hspace{-6ex} \text{catch}~~\Tinstr_2^\ast~\text{end} & \\ + \qquad (\text{(}~\text{catch}~~\Tinstr_2^\ast~\text{)})^\ast &\\ + \qquad\qquad (\text{(}~\text{catch_all}~~\Tinstr_3^\ast~\text{)})^?~\text{)} & \equiv \\ + \text{try}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast (\text{delegate}~~\Tlabelidx & \equiv \\ + \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{delegate}~~l~\text{)} &\\ \end{array} .. note:: diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index ae0fa55e..488f4642 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -2,12 +2,12 @@ Modules ------- -.. index:: index, type index, function index, table index, memory index, exception index, global index, element index, data index, local index, label index +.. index:: index, type index, function index, table index, memory index, tag index, global index, element index, data index, local index, label index pair: text format; type index pair: text format; function index pair: text format; table index pair: text format; memory index - pair: text format; exception index + pair: text format; tag index pair: text format; global index pair: text format; element index pair: text format; data index @@ -17,7 +17,7 @@ Modules .. _text-funcidx: .. _text-tableidx: .. _text-memidx: -.. _text-exnidx: +.. _text-tagidx: .. _text-elemidx: .. _text-dataidx: .. _text-globalidx: @@ -45,9 +45,9 @@ Such identifiers are looked up in the suitable space of the :ref:`identifier con \production{memory index} & \Tmemidx_I &::=& x{:}\Tu32 &\Rightarrow& x \\&&|& v{:}\Tid &\Rightarrow& x & (\iff I.\IMEMS[x] = v) \\ - \production{exception index} & \Texnidx_I &::=& + \production{tag index} & \Ttagidx_I &::=& x{:}\Tu32 &\Rightarrow& x \\&&|& - v{:}\Tid &\Rightarrow& x & (\iff I.\IEXNS[x] = v) \\ + v{:}\Tid &\Rightarrow& x & (\iff I.\ITAGS[x] = v) \\ \production{global index} & \Tglobalidx_I &::=& x{:}\Tu32 &\Rightarrow& x \\&&|& v{:}\Tid &\Rightarrow& x & (\iff I.\IGLOBALS[x] = v) \\ @@ -154,7 +154,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, exception type, global type +.. index:: import, name, function type, table type, memory type, tag type, global type pair: text format; import .. _text-importdesc: .. _text-import: @@ -162,7 +162,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, exception, or global :ref:`identifier `. +The descriptors in imports can bind a symbolic function, table, memory, tag, or global :ref:`identifier `. .. math:: \begin{array}{llclll} @@ -176,8 +176,8 @@ The descriptors in imports can bind a symbolic function, table, memory, exceptio &\Rightarrow& \IDTABLE~\X{tt} \\ &&|& \text{(}~\text{memory}~~\Tid^?~~\X{mt}{:}\Tmemtype~\text{)} &\Rightarrow& \IDMEM~~\X{mt} \\ &&|& - \text{(}~\text{exception}~~\Tid^?~~\X{et}{:}\Texn~\text{)} - &\Rightarrow& \IDEXN~\X{et} \\ &&|& + \text{(}~\text{tag}~~\Tid^?~~\X{tt}{:}\Ttag~\text{)} + &\Rightarrow& \IDTAG~\X{tt} \\ &&|& \text{(}~\text{global}~~\Tid^?~~\X{gt}{:}\Tglobaltype~\text{)} &\Rightarrow& \IDGLOBAL~\X{gt} \\ \end{array} @@ -186,7 +186,7 @@ The descriptors in imports can bind a symbolic function, table, memory, exceptio Abbreviations ............. -As an abbreviation, imports may also be specified inline with :ref:`function `, :ref:`table `, :ref:`memory `, :ref:`exception ` or :ref:`global ` definitions; see the respective sections. +As an abbreviation, imports may also be specified inline with :ref:`function `, :ref:`table `, :ref:`memory `, :ref:`tag ` or :ref:`global ` definitions; see the respective sections. @@ -389,44 +389,44 @@ Memories can be defined as :ref:`imports ` or :ref:`exports `. +An tag definition can bind a symbolic :ref:`tag identifier `. .. math:: \begin{array}{llcl} - \production{exception} & \Texn_I &::=& - \text{(}~\text{exception}~~\Tid^?~~x,I'{:}\Ttypeuse_I~\text{)} \\ &&& \qquad - \Rightarrow\quad \{ \ETYPE~x \} \\ + \production{tag} & \Ttag_I &::=& + \text{(}~\text{tag}~~\Tid^?~~x,I'{:}\Ttypeuse_I~\text{)} \\ &&& \qquad + \Rightarrow\quad \{ \TAGTYPE~x \} \\ \end{array} .. index:: import, name pair: text format; import -.. index:: export, name, index, exception index +.. index:: export, name, index, tag index pair: text format; export -.. index:: exception -.. _text-exn-abbrev: +.. index:: tag +.. _text-tag-abbrev: Abbreviations ............. -Exceptions can be defined as :ref:`imports ` or :ref:`exports ` inline: +Tags can be defined as :ref:`imports ` or :ref:`exports ` inline: .. math:: \begin{array}{llclll} \production{module field} & - \text{(}~\text{exception}~~\Tid^?~~\text{(}~\text{import}~~\Tname_1~~\Tname_2~\text{)}~~\Ttypeuse~\text{)} \quad\equiv \\ & \qquad - \text{(}~\text{import}~~\Tname_1~~\Tname_2~~\text{(}~\text{exception}~~\Tid^?~~\Ttypeuse~\text{)}~\text{)} + \text{(}~\text{tag}~~\Tid^?~~\text{(}~\text{import}~~\Tname_1~~\Tname_2~\text{)}~~\Ttypeuse~\text{)} \quad\equiv \\ & \qquad + \text{(}~\text{import}~~\Tname_1~~\Tname_2~~\text{(}~\text{tag}~~\Tid^?~~\Ttypeuse~\text{)}~\text{)} \\[1ex] & - \text{(}~\text{exception}~~\Tid^?~~\text{(}~\text{export}~~\Tname~\text{)}~~\dots~\text{)} \quad\equiv \\ & \qquad - \text{(}~\text{export}~~\Tname~~\text{(}~\text{exception}~~\Tid'~\text{)}~\text{)}~~ - \text{(}~\text{exception}~~\Tid'~~\dots~\text{)} + \text{(}~\text{tag}~~\Tid^?~~\text{(}~\text{export}~~\Tname~\text{)}~~\dots~\text{)} \quad\equiv \\ & \qquad + \text{(}~\text{export}~~\Tname~~\text{(}~\text{tag}~~\Tid'~\text{)}~\text{)}~~ + \text{(}~\text{tag}~~\Tid'~~\dots~\text{)} \\ & \qquad\qquad (\iff \Tid' = \Tid^? \neq \epsilon \vee \Tid' \idfresh) \\ \end{array} @@ -478,7 +478,7 @@ Globals can be defined as :ref:`imports ` or :ref:`exports ` dire &\Rightarrow& \EDTABLE~x \\ &&|& \text{(}~\text{memory}~~x{:}\Tmemidx_I~\text{)} &\Rightarrow& \EDMEM~x \\ &&|& - \text{(}~\text{exception}~~x{:}\Texnidx_I~\text{)} - &\Rightarrow& \EDEXN~x \\&&|& + \text{(}~\text{tag}~~x{:}\Ttagidx_I~\text{)} + &\Rightarrow& \EDTAG~x \\&&|& \text{(}~\text{global}~~x{:}\Tglobalidx_I~\text{)} &\Rightarrow& \EDGLOBAL~x \\ \end{array} @@ -510,7 +510,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 `, :ref:`exception ` definitions, 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:`tag ` definitions, or :ref:`global ` definitions; see the respective sections. .. index:: start function, function index @@ -665,7 +665,7 @@ Also, a memory use can be omitted, defaulting to :math:`\T{0}`. As another abbreviation, data segments may also be specified inline with :ref:`memory ` definitions; see the respective section. -.. index:: module, type definition, function type, function, table, memory, exception, global, element, data, start function, import, export, identifier context, identifier, name section +.. index:: module, type definition, function type, function, table, memory, tag, global, element, data, start function, import, export, identifier context, identifier, name section pair: text format; module single: section; name .. _text-modulefield: @@ -700,7 +700,7 @@ The name serves a documentary role only. \X{fn}{:}\Tfunc_I &\Rightarrow& \{\MFUNCS~\X{fn}\} \\ |& \X{ta}{:}\Ttable_I &\Rightarrow& \{\MTABLES~\X{ta}\} \\ |& \X{me}{:}\Tmem_I &\Rightarrow& \{\MMEMS~\X{me}\} \\ |& - \X{et}{:}\Texn_I &\Rightarrow& \{\MEXNS~\X{et}\} \\ |& + \X{tt}{:}\Ttag_I &\Rightarrow& \{\MTAGS~\X{tt}\} \\ |& \X{gl}{:}\Tglobal_I &\Rightarrow& \{\MGLOBALS~\X{gl}\} \\ |& \X{ex}{:}\Texport_I &\Rightarrow& \{\MEXPORTS~\X{ex}\} \\ |& \X{st}{:}\Tstart_I &\Rightarrow& \{\MSTART~\X{st}\} \\ |& @@ -713,11 +713,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 `, :ref:`exception `, 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:`tag `, 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. @@ -734,8 +734,8 @@ The definition of the initial :ref:`identifier context ` :math:`I` \{\ITABLES~(\Tid^?)\} \\ \F{idc}(\text{(}~\text{memory}~\Tid^?~\dots~\text{)}) &=& \{\IMEMS~(\Tid^?)\} \\ - \F{idc}(\text{(}~\text{exception}~\Tid^?~\dots~\text{)}) &=& - \{\IEXNS~(\Tid^?)\} \\ + \F{idc}(\text{(}~\text{tag}~\Tid^?~\dots~\text{)}) &=& + \{\ITAGS~(\Tid^?)\} \\ \F{idc}(\text{(}~\text{global}~\Tid^?~\dots~\text{)}) &=& \{\IGLOBALS~(\Tid^?)\} \\ \F{idc}(\text{(}~\text{elem}~\Tid^?~\dots~\text{)}) &=& @@ -748,8 +748,8 @@ The definition of the initial :ref:`identifier context ` :math:`I` \{\ITABLES~(\Tid^?)\} \\ \F{idc}(\text{(}~\text{import}~\dots~\text{(}~\text{memory}~\Tid^?~\dots~\text{)}~\text{)}) &=& \{\IMEMS~(\Tid^?)\} \\ - \F{idc}(\text{(}~\text{import}~\dots~\text{(}~\text{exception}~\Tid^?~\dots~\text{)}~\text{)}) &=& - \{\IEXNS~(\Tid^?)\} \\ + \F{idc}(\text{(}~\text{import}~\dots~\text{(}~\text{tag}~\Tid^?~\dots~\text{)}~\text{)}) &=& + \{\ITAGS~(\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 685a3657..7705cc57 100644 --- a/document/core/text/types.rst +++ b/document/core/text/types.rst @@ -48,11 +48,9 @@ Reference Types \begin{array}{llcll@{\qquad\qquad}l} \production{reference type} & \Treftype &::=& \text{funcref} &\Rightarrow& \FUNCREF \\ &&|& - \text{exnref} &\Rightarrow& \EXNREF \\ &&|& \text{externref} &\Rightarrow& \EXTERNREF \\ \production{heap type} & \Theaptype &::=& \text{func} &\Rightarrow& \FUNCREF \\ &&|& - \text{exn} &\Rightarrow& \EXNREF \\ &&|& \text{extern} &\Rightarrow& \EXTERNREF \\ \end{array} diff --git a/document/core/util/macros.def b/document/core/util/macros.def index c993914a..9a15564c 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -190,7 +190,6 @@ .. |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}} @@ -202,7 +201,7 @@ .. |ETTABLE| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{table}} .. |ETMEM| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{mem}} .. |ETGLOBAL| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{global}} -.. |ETEXN| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{exception}} +.. |ETTAG| mathdef:: \xref{syntax/types}{syntax-tagtype}{\K{tag}} .. Types, non-terminals @@ -213,7 +212,7 @@ .. |valtype| mathdef:: \xref{syntax/types}{syntax-valtype}{\X{valtype}} .. |resulttype| mathdef:: \xref{syntax/types}{syntax-resulttype}{\X{resulttype}} .. |functype| mathdef:: \xref{syntax/types}{syntax-functype}{\X{functype}} -.. |exntype| mathdef:: \xref{syntax/types}{syntax-exntype}{\X{exntype}} +.. |tagtype| mathdef:: \xref{syntax/types}{syntax-tagtype}{\X{tagtype}} .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}} .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}} @@ -234,7 +233,7 @@ .. |ettables| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}} .. |etmems| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{mems}} .. |etglobals| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{globals}} -.. |etexns| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{exceptions}} +.. |ettags| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tags}} .. Indices, non-terminals @@ -248,7 +247,7 @@ .. |dataidx| mathdef:: \xref{syntax/modules}{syntax-dataidx}{\X{dataidx}} .. |localidx| mathdef:: \xref{syntax/modules}{syntax-localidx}{\X{localidx}} .. |labelidx| mathdef:: \xref{syntax/modules}{syntax-labelidx}{\X{labelidx}} -.. |exnidx| mathdef:: \xref{syntax/modules}{syntax-exnidx}{\X{exnidx}} +.. |tagidx| mathdef:: \xref{syntax/modules}{syntax-tagidx}{\X{tagidx}} .. Indices, meta functions @@ -271,7 +270,7 @@ .. |MTABLES| mathdef:: \xref{syntax/modules}{syntax-module}{\K{tables}} .. |MMEMS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{mems}} .. |MGLOBALS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{globals}} -.. |MEXNS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{exceptions}} +.. |MTAGS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{tags}} .. |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}} @@ -286,7 +285,7 @@ .. |MTYPE| mathdef:: \xref{syntax/modules}{syntax-mem}{\K{type}} -.. |ETYPE| mathdef:: \xref{syntax/modules}{syntax-exn}{\K{type}} +.. |TAGTYPE| mathdef:: \xref{syntax/modules}{syntax-tag}{\K{type}} .. |GTYPE| mathdef:: \xref{syntax/modules}{syntax-global}{\K{type}} .. |GINIT| mathdef:: \xref{syntax/modules}{syntax-global}{\K{init}} @@ -315,7 +314,7 @@ .. |EDTABLE| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{table}} .. |EDMEM| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{mem}} .. |EDGLOBAL| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{global}} -.. |EDEXN| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{exception}} +.. |EDTAG| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{tag}} .. |IMODULE| mathdef:: \xref{syntax/modules}{syntax-import}{\K{module}} .. |INAME| mathdef:: \xref{syntax/modules}{syntax-import}{\K{name}} @@ -323,7 +322,7 @@ .. |IDFUNC| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{func}} .. |IDTABLE| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{table}} .. |IDMEM| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{mem}} -.. |IDEXN| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{exception}} +.. |IDTAG| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{tag}} .. |IDGLOBAL| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{global}} @@ -334,7 +333,7 @@ .. |func| mathdef:: \xref{syntax/modules}{syntax-func}{\X{func}} .. |table| mathdef:: \xref{syntax/modules}{syntax-table}{\X{table}} .. |mem| mathdef:: \xref{syntax/modules}{syntax-mem}{\X{mem}} -.. |exn| mathdef:: \xref{syntax/modules}{syntax-exn}{\X{exn}} +.. |tag| mathdef:: \xref{syntax/modules}{syntax-tag}{\X{tag}} .. |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}} @@ -352,7 +351,7 @@ .. |edfuncs| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{funcs}} .. |edtables| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{tables}} .. |edmems| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{mems}} -.. |edexns| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{exceptions}} +.. |edtags| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{tags}} .. |edglobals| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{globals}} @@ -376,9 +375,10 @@ .. |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}} +.. |CATCHALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{catch\_all}} +.. |DELEGATE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{delegate}} .. |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}} @@ -615,7 +615,7 @@ .. |Bresulttype| mathdef:: \xref{binary/types}{binary-resulttype}{\B{resulttype}} .. |Bfunctype| mathdef:: \xref{binary/types}{binary-functype}{\B{functype}} .. |Bglobaltype| mathdef:: \xref{binary/types}{binary-globaltype}{\B{globaltype}} -.. |Bexntype| mathdef:: \xref{binary/types}{binary-exntype}{\B{exntype}} +.. |Btagtype| mathdef:: \xref{binary/types}{binary-tagtype}{\B{tagtype}} .. |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}} @@ -629,7 +629,7 @@ .. |Bfuncidx| mathdef:: \xref{binary/modules}{binary-funcidx}{\B{funcidx}} .. |Btableidx| mathdef:: \xref{binary/modules}{binary-tableidx}{\B{tableidx}} .. |Bmemidx| mathdef:: \xref{binary/modules}{binary-memidx}{\B{memidx}} -.. |Bexnidx| mathdef:: \xref{binary/modules}{binary-exnidx}{\B{exnidx}} +.. |Btagidx| mathdef:: \xref{binary/modules}{binary-tagidx}{\B{tagidx}} .. |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}} @@ -650,7 +650,7 @@ .. |Bcodesec| mathdef:: \xref{binary/modules}{binary-codesec}{\B{codesec}} .. |Btablesec| mathdef:: \xref{binary/modules}{binary-tablesec}{\B{tablesec}} .. |Bmemsec| mathdef:: \xref{binary/modules}{binary-memsec}{\B{memsec}} -.. |Bexnsec| mathdef:: \xref{binary/modules}{binary-exnsec}{\B{exnsec}} +.. |Btagsec| mathdef:: \xref{binary/modules}{binary-tagsec}{\B{tagsec}} .. |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}} @@ -664,7 +664,7 @@ .. |Bfunc| mathdef:: \xref{binary/modules}{binary-func}{\B{func}} .. |Btable| mathdef:: \xref{binary/modules}{binary-table}{\B{table}} .. |Bmem| mathdef:: \xref{binary/modules}{binary-mem}{\B{mem}} -.. |Bexn| mathdef:: \xref{binary/modules}{binary-exn}{\B{exn}} +.. |Btag| mathdef:: \xref{binary/modules}{binary-tag}{\B{tag}} .. |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}} @@ -799,7 +799,7 @@ .. |Tfuncidx| mathdef:: \xref{text/modules}{text-funcidx}{\T{funcidx}} .. |Ttableidx| mathdef:: \xref{text/modules}{text-tableidx}{\T{tableidx}} .. |Tmemidx| mathdef:: \xref{text/modules}{text-memidx}{\T{memidx}} -.. |Texnidx| mathdef:: \xref{text/modules}{text-exnidx}{\T{exnidx}} +.. |Ttagidx| mathdef:: \xref{text/modules}{text-tagidx}{\T{tagidx}} .. |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}} @@ -825,7 +825,7 @@ .. |Tfunc| mathdef:: \xref{text/modules}{text-func}{\T{func}} .. |Ttable| mathdef:: \xref{text/modules}{text-table}{\T{table}} .. |Tmem| mathdef:: \xref{text/modules}{text-mem}{\T{mem}} -.. |Texn| mathdef:: \xref{text/modules}{text-exn}{\T{exception}} +.. |Ttag| mathdef:: \xref{text/modules}{text-tag}{\T{tag}} .. |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}} @@ -871,7 +871,7 @@ .. |IFUNCS| mathdef:: \xref{text/conventions}{text-context}{\K{funcs}} .. |ITABLES| mathdef:: \xref{text/conventions}{text-context}{\K{tables}} .. |IMEMS| mathdef:: \xref{text/conventions}{text-context}{\K{mems}} -.. |IEXNS| mathdef:: \xref{text/conventions}{text-context}{\K{exceptions}} +.. |ITAGS| mathdef:: \xref{text/conventions}{text-context}{\K{tags}} .. |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}} @@ -894,7 +894,9 @@ .. |ok| mathdef:: \mathrel{\mbox{ok}} .. |const| mathdef:: \xref{valid/instructions}{valid-constant}{\mathrel{\mbox{const}}} +.. |catch| mathdef:: \xref{valid/conventions}{valid-labelkind}{\mathrel{\mbox{catch}}} +.. |labelkind| mathdef:: \xref{valid/conventions}{valid-labelkind}{\mathrel{\X{labelkind}}} .. Contexts @@ -902,7 +904,7 @@ .. |CFUNCS| mathdef:: \xref{valid/conventions}{context}{\K{funcs}} .. |CTABLES| mathdef:: \xref{valid/conventions}{context}{\K{tables}} .. |CMEMS| mathdef:: \xref{valid/conventions}{context}{\K{mems}} -.. |CEXNS| mathdef:: \xref{valid/conventions}{context}{\K{exceptions}} +.. |CTAGS| mathdef:: \xref{valid/conventions}{context}{\K{tags}} .. |CGLOBALS| mathdef:: \xref{valid/conventions}{context}{\K{globals}} .. |CELEMS| mathdef:: \xref{valid/conventions}{context}{\K{elems}} .. |CDATAS| mathdef:: \xref{valid/conventions}{context}{\K{datas}} @@ -919,7 +921,7 @@ .. |vdashfunctype| mathdef:: \xref{valid/types}{valid-functype}{\vdash} .. |vdashtabletype| mathdef:: \xref{valid/types}{valid-tabletype}{\vdash} .. |vdashmemtype| mathdef:: \xref{valid/types}{valid-memtype}{\vdash} -.. |vdashexntype| mathdef:: \xref{valid/types}{valid-exntype}{\vdash} +.. |vdashtagtype| mathdef:: \xref{valid/types}{valid-tagtype}{\vdash} .. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash} .. |vdashexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\vdash} @@ -932,7 +934,7 @@ .. |vdashfunc| mathdef:: \xref{valid/modules}{valid-func}{\vdash} .. |vdashtable| mathdef:: \xref{valid/modules}{valid-table}{\vdash} .. |vdashmem| mathdef:: \xref{valid/modules}{valid-mem}{\vdash} -.. |vdashexn| mathdef:: \xref{valid/modules}{valid-exn}{\vdash} +.. |vdashtag| mathdef:: \xref{valid/modules}{valid-tag}{\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} @@ -966,7 +968,7 @@ .. |allochostfunc| mathdef:: \xref{exec/modules}{alloc-hostfunc}{\F{allochostfunc}} .. |alloctable| mathdef:: \xref{exec/modules}{alloc-table}{\F{alloctable}} .. |allocmem| mathdef:: \xref{exec/modules}{alloc-mem}{\F{allocmem}} -.. |allocexn| mathdef:: \xref{exec/modules}{alloc-exn}{\F{allocexn}} +.. |alloctag| mathdef:: \xref{exec/modules}{alloc-tag}{\F{alloctag}} .. |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}} @@ -982,7 +984,7 @@ .. |funcaddr| mathdef:: \xref{exec/runtime}{syntax-funcaddr}{\X{funcaddr}} .. |tableaddr| mathdef:: \xref{exec/runtime}{syntax-tableaddr}{\X{tableaddr}} .. |memaddr| mathdef:: \xref{exec/runtime}{syntax-memaddr}{\X{memaddr}} -.. |exnaddr| mathdef:: \xref{exec/runtime}{syntax-exnaddr}{\X{exnaddr}} +.. |tagaddr| mathdef:: \xref{exec/runtime}{syntax-tagaddr}{\X{tagaddr}} .. |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}} @@ -1001,7 +1003,7 @@ .. |MITYPE| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{type}} .. |MIDATA| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{data}} -.. |EITYPE| mathdef:: \xref{exec/runtime}{syntax-exninst}{\K{type}} +.. |TAGITYPE| mathdef:: \xref{exec/runtime}{syntax-taginst}{\K{type}} .. |GITYPE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{type}} .. |GIVALUE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{value}} @@ -1017,14 +1019,14 @@ .. |EVFUNC| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{func}} .. |EVTABLE| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{table}} .. |EVMEM| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{mem}} -.. |EVEXN| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{exception}} +.. |EVTAG| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{tag}} .. |EVGLOBAL| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{global}} .. |MITYPES| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{types}} .. |MIFUNCS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{funcaddrs}} .. |MITABLES| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{tableaddrs}} .. |MIMEMS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{memaddrs}} -.. |MIEXNS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{exnaddrs}} +.. |MITAGS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{tagaddrs}} .. |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}} @@ -1039,7 +1041,7 @@ .. |funcinst| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\X{funcinst}} .. |tableinst| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\X{tableinst}} .. |meminst| mathdef:: \xref{exec/runtime}{syntax-meminst}{\X{meminst}} -.. |exninst| mathdef:: \xref{exec/runtime}{syntax-exninst}{\X{exninst}} +.. |taginst| mathdef:: \xref{exec/runtime}{syntax-taginst}{\X{taginst}} .. |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}} @@ -1053,7 +1055,7 @@ .. |evfuncs| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{funcs}} .. |evtables| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{tables}} .. |evmems| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{mems}} -.. |evexns| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{exceptions}} +.. |evtags| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{tags}} .. |evglobals| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{globals}} @@ -1062,7 +1064,7 @@ .. |SFUNCS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{funcs}} .. |STABLES| mathdef:: \xref{exec/runtime}{syntax-store}{\K{tables}} .. |SMEMS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{mems}} -.. |SEXNS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{exceptions}} +.. |STAGS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{tags}} .. |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}} @@ -1085,7 +1087,7 @@ .. |label| mathdef:: \xref{exec/runtime}{syntax-label}{\X{label}} .. |frame| mathdef:: \xref{exec/runtime}{syntax-frame}{\X{frame}} - +.. |handler| mathdef:: \xref{exec/runtime}{syntax-handler}{\X{handler}} .. Stack, meta functions @@ -1098,9 +1100,10 @@ .. |REFEXTERNADDR| mathdef:: \xref{exec/runtime}{syntax-ref.extern}{\K{ref{.}extern}} .. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}} .. |INVOKE| mathdef:: \xref{exec/runtime}{syntax-invoke}{\K{invoke}} -.. |REFEXNADDR| mathdef:: \xref{exec/runtime}{syntax-refexnaddr}{\K{ref{.}exn}} -.. |THROWADDR| mathdef:: \xref{exec/runtime}{syntax-throwaddr}{\K{throw}} -.. |CATCHN| mathdef:: \xref{exec/runtime}{syntax-catchn}{\K{catch}} +.. |THROWadm| mathdef:: \xref{exec/runtime}{syntax-throwadm}{\K{throw}} +.. |CATCHadm| mathdef:: \xref{exec/runtime}{syntax-catchadm}{\K{catch}} +.. |DELEGATEadm| mathdef:: \xref{exec/runtime}{syntax-delegateadm}{\K{delegate}} +.. |CAUGHTadm| mathdef:: \xref{exec/runtime}{syntax-caughtadm}{\K{caught}} .. Values & Results, non-terminals @@ -1120,6 +1123,7 @@ .. Administrative Instructions, non-terminals .. |XB| mathdef:: \xref{exec/runtime}{syntax-ctxt-block}{B} +.. |XC| mathdef:: \xref{exec/runtime}{syntax-ctxt-block}{C} .. |XT| mathdef:: \xref{exec/runtime}{syntax-ctxt-throw}{T} @@ -1266,7 +1270,7 @@ .. |vdashfuncinst| mathdef:: \xref{appendix/properties}{valid-funcinst}{\vdash} .. |vdashtableinst| mathdef:: \xref{appendix/properties}{valid-tableinst}{\vdash} .. |vdashmeminst| mathdef:: \xref{appendix/properties}{valid-meminst}{\vdash} -.. |vdashexninst| mathdef:: \xref{appendix/properties}{valid-exninst}{\vdash} +.. |vdashtaginst| mathdef:: \xref{appendix/properties}{valid-taginst}{\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} @@ -1281,7 +1285,7 @@ .. |vdashfuncinstextends| mathdef:: \xref{appendix/properties}{extend-funcinst}{\vdash} .. |vdashtableinstextends| mathdef:: \xref{appendix/properties}{extend-tableinst}{\vdash} .. |vdashmeminstextends| mathdef:: \xref{appendix/properties}{extend-meminst}{\vdash} -.. |vdashexninstextends| mathdef:: \xref{appendix/properties}{extend-exninst}{\vdash} +.. |vdashtaginstextends| mathdef:: \xref{appendix/properties}{extend-taginst}{\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} @@ -1312,3 +1316,5 @@ .. |error| mathdef:: \xref{appendix/embedding}{embed-error}{\X{error}} .. |ERROR| mathdef:: \xref{appendix/embedding}{embed-error}{\K{error}} +.. |exception| mathdef:: \xref{appendix/embedding}{embed-exception}{\X{exception}} +.. |EXCEPTION| mathdef:: \xref{appendix/embedding}{embed-exception}{\K{exception}} \ No newline at end of file diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 027b5938..81e57660 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -24,8 +24,9 @@ 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, exception type, global type, value type, result type, index space, module, function, exception +.. index:: ! context, function type, table type, memory type, tag type, global type, value type, result type, index space, module, function, tag, labelkind .. _context: +.. _labelkind: Contexts ~~~~~~~~ @@ -37,12 +38,12 @@ which collects relevant information about the surrounding :ref:`module ` that occur in the module outside functions and can hence be used to form references inside them. @@ -55,18 +56,19 @@ More concretely, contexts are defined as :ref:`records ` :math: .. math:: \begin{array}{llll} + \production{(labelkind)} & \labelkind & ::= & \catch^?~\resulttype^\ast\\ \production{(context)} & C &::=& \begin{array}[t]{l@{~}ll} \{ & \CTYPES & \functype^\ast, \\ & \CFUNCS & \functype^\ast, \\ & \CTABLES & \tabletype^\ast, \\ & \CMEMS & \memtype^\ast, \\ - & \CEXNS & \exntype^\ast, \\ + & \CTAGS & \tagtype^\ast, \\ & \CGLOBALS & \globaltype^\ast, \\ & \CELEMS & \reftype^\ast, \\ & \CDATAS & {\ok}^\ast, \\ & \CLOCALS & \valtype^\ast, \\ - & \CLABELS & \resulttype^\ast, \\ + & \CLABELS & \labelkind, \\ & \CRETURN & \resulttype^?, \\ & \CREFS & \funcidx^\ast ~\} \\ \end{array} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index ee7f915e..6e9e601b 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1234,7 +1234,7 @@ Memory Instructions } -.. index:: control instructions, structured control, label, block, branch, block type, label index, function index, type index, exception index, vector, polymorphism, context +.. index:: control instructions, structured control, label, block, branch, block type, label index, function index, type index, tag index, vector, polymorphism, context pair: validation; instruction single: abstract syntax; instruction .. _valid-label: @@ -1361,54 +1361,64 @@ Control Instructions -.. _valid-try: +.. _valid-try-catch: -:math:`\TRY~\blocktype~\instr_1^\ast~\CATCH~\instr_2^\ast~\END` -............................................................... +:math:`\TRY~\blocktype~\instr_1^\ast~(\CATCH~x~\instr_2^\ast)^\ast~(\CATCHALL~\instr_3^\ast)^?~\END` +.................................................................................................... +**TODO: add prose** -* The :ref:`block type ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. +.. math:: + \frac{ + \begin{array}{c} + 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] \\ + (C.\CTAGS[x] = [t^\ast]\to[]~\land~C,\CLABELS\,(\catch [t_2^\ast]) \vdashinstrseq \instr_2^\ast : [t^\ast]\to[t_2^\ast])\ast \\ + (C,\CLABELS\,(\catch~[t_2^\ast]) \vdashinstrseq \instr_3^\ast : []\to[t_2^\ast])^? + \end{array} + }{ + C \vdashinstr \TRY~\blocktype~\instr^\ast (\CATCH~x~\instr_2^\ast)^\ast (\CATCHALL~\instr_3^\ast)^? end : [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]`. +.. note:: + The :ref:`notation ` :math:`C,\CLABELS\,(\labelkind^? [t^\ast])` inserts the new label type at index :math:`0`, shifting all others. -* 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]`. +.. _valid-try-delegate: + +:math:`\TRY~\blocktype~\instr^\ast~\DELEGATE~l` +............................................... + +**TODO: add prose** .. 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 \vdashblocktype \blocktype : [t_1^\ast] \to [t_2^\ast] + \qquad + C,\CLABELS\,[t_2^\ast] \vdashinstrseq \instr^\ast : [t_1^\ast]\to[t_2^\ast] + \qquad + |C.\CLABELS| \ge l }{ - C \vdashinstr \TRY~\blocktype~\instr_1^\ast~\CATCH~\instr_2^\ast~\END : [t_1^\ast] \to [t_2^\ast] + C \vdashinstrseq \TRY~\blocktype~\instr^\ast~\DELEGATE~l : [t_1^\ast]\to[t_2^\ast] } -.. note:: - The :ref:`notation ` :math:`C,\CLABELS\,[t_2^\ast]` inserts the new label type at index :math:`0`, shifting all others. - .. _valid-throw: :math:`\THROW~x` ................ -* The exception :math:`C.\CEXNS[x]` must be defined in the context. +* The tag :math:`C.\CTAGS[x]` must be defined in the context. -* Let :math:`[t^\ast] \to []` be its :ref:`exception type `. +* Let :math:`[t^\ast] \to []` be its :ref:`tag type `. * Then the instruction is valid with type :math:`[t_1^\ast t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ - C.\CEXNS[x] = [t^\ast] \to [] + C.\CTAGS[x] = [t^\ast] \to [] }{ C \vdashinstr \THROW~x : [t_1^\ast t^\ast] \to [t_2^\ast] } @@ -1420,15 +1430,16 @@ Control Instructions .. _valid-rethrow: -:math:`\RETHROW` -................ +:math:`\RETHROW~l` +.................. -* 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`. +**TODO: add prose** .. math:: \frac{ + C.\CLABELS[l] = (\catch [t^\ast]) }{ - C \vdashinstr \RETHROW : [t_1^\ast \EXNREF] \to [t_2^\ast] + C \vdashinstr \RETHROW~l : [t_1^\ast] \to [t_2^\ast] } @@ -1436,36 +1447,6 @@ Control Instructions The |RETHROW| instruction is :ref:`stack-polymorphic `. -.. _valid-br_on_exn: - -:math:`\BRONEXN~l~x` -.................... - -* The label :math:`C.\CLABELS[l]` must be defined in the context. - -* The exception :math:`C.\CEXNS[x]` must be defined in the context. - -* Let :math:`[t^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. - -* Assert: the exception :math:`C.\CEXNS[x]` is :math:`[t'^\ast]\to[]`. - -* The type sequence :math:`t'^\ast` must be the same as the type sequence :math:`t^\ast`. - -* Then the instruction is valid with type :math:`[\EXNREF]\to[\EXNREF]` - -.. math:: - \frac{ - C.\CLABELS[l]=[t^\ast] - \qquad - C.\CEXNS[x]=[t^\ast]\to[] - }{ - C \vdashinstr \BRONEXN~l~x : [\EXNREF]\to[\EXNREF] - } - -.. note:: - The :ref:`label index ` space in the :ref:`context ` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected. - - .. _valid-br: diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 58f9edb9..71a8b1ef 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -98,19 +98,19 @@ Memories :math:`\mem` are classified by :ref:`memory types `. } -.. index:: exception, exception type, function type - pair: validation; exception - single: abstract syntax; exception -.. _valid-exn: +.. index:: tag, tag type, function type, exception tag + pair: validation; tag + single: abstract syntax; tag +.. _valid-tag: -Exceptions -~~~~~~~~~~ +Tags +~~~~ -Exceptions :math:`\exn` are classified by their :ref:`exception type `, -which contains an index to a :ref:`function type ` with empty result. +Tags :math:`\tag` are classified by their :ref:`tag type `, +each containing an index to a :ref:`function type ` with empty result. -:math:`\{ \ETYPE~x \}` -...................... +:math:`\{ \TAGTYPE~x \}` +........................ * The type :math:`C.\CTYPES[x]` must be defined in the context. @@ -118,13 +118,13 @@ which contains an index to a :ref:`function type ` with empty r * The sequence :math:`t'^\ast` must be empty. -* Then the exception definition is valid with :ref:`exception type ` :math:`[t^\ast]\to[]`. +* Then the tag definition is valid with :ref:`tag type ` :math:`[t^\ast]\to[]`. .. math:: \frac{ C.\CTYPES[x] = [t^\ast] \to [] }{ - C \vdashexn \{ \ETYPE~x \} : [t^\ast]\to[] + C \vdashtag \{ \TAGTYPE~x \} : [t^\ast]\to[] } @@ -345,7 +345,7 @@ Start function declarations :math:`\start` are not classified by any type. } -.. index:: export, name, index, function index, table index, memory index, exception index, global index +.. index:: export, name, index, function index, table index, memory index, tag index, global index pair: validation; export single: abstract syntax; export .. _valid-exportdesc: @@ -417,18 +417,18 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi } -:math:`\EDEXN~x` +:math:`\EDTAG~x` ................ -* The exception :math:`C.\CEXNS[x]` must be defined in the context. +* The tag :math:`C.\CTAGS[x]` must be defined in the context. -* Then the export description is valid with :ref:`external type ` :math:`\ETEXN~C.\CEXNS[x]`. +* Then the export description is valid with :ref:`external type ` :math:`\ETTAG~C.\CTAGS[x]`. .. math:: \frac{ - C.\CEXNS[x] = \exntype + C.\CTAGS[x] = \tagtype }{ - C \vdashexportdesc \EDEXN~x : \ETEXN~\exntype + C \vdashexportdesc \EDTAG~x : \ETTAG~\tagtype } @@ -447,7 +447,7 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi } -.. index:: import, name, function type, table type, memory type, exception type, global type +.. index:: import, name, function type, table type, memory type, tag type, global type pair: validation; import single: abstract syntax; import .. _valid-importdesc: @@ -521,22 +521,22 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi } -:math:`\IDEXN~\exn` +:math:`\IDTAG~\tag` ................... -* Let :math:`\{ \ETYPE~x \}` be the exception :math:`\exn`. +* Let :math:`\{ \TAGTYPE~x \}` be the tag :math:`\tag`. * The type :math:`C.\CTYPES[x]` must be defined in the context. -* The :ref:`exception type ` :math:`C.\CTYPES[x]` must be a :ref:`valid exception type `. +* The :ref:`tag type ` :math:`C.\CTYPES[x]` must be a :ref:`valid tag type `. -* Then the import description is valid with type :math:`\ETEXN~C.\CTYPES[x]`. +* Then the import description is valid with type :math:`\ETTAG~C.\CTYPES[x]`. .. math:: \frac{ - \vdashexntype C.\CTYPES[x] \ok + \vdashtagtype C.\CTYPES[x] \ok }{ - C \vdashimportdesc \IDEXN~\{ \ETYPE~x \} : \ETEXN~C.\CTYPES[x] + C \vdashimportdesc \IDTAG~\{ \TAGTYPE~x \} : \ETTAG~C.\CTYPES[x] } @@ -556,7 +556,7 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi } -.. index:: module, type definition, function type, function, table, memory, exception, global, element, data, start function, import, export, context +.. index:: module, type definition, function type, function, table, memory, tag, global, element, data, start function, import, export, context pair: validation; module single: abstract syntax; module .. _valid-module: @@ -586,8 +586,8 @@ Instead, the context :math:`C` for validation of the module's content is constru * :math:`C.\CMEMS` is :math:`\etmems(\X{it}^\ast)` concatenated with :math:`\X{mt}^\ast`, with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :ref:`memory types ` :math:`\X{mt}^\ast` as determined below, - * :math:`C.\CEXNS` is :math:`\etexns(\X{it}^\ast)` concatenated with :math:`\X{exnt}^\ast`, - with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :ref:`exception types ` :math:`\X{exnt}^\ast` as determined below, + * :math:`C.\CTAGS` is :math:`\ettags(\X{it}^\ast)` concatenated with :math:`\X{tagt}^\ast`, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :ref:`tag types ` :math:`\X{tagt}^\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, @@ -612,7 +612,7 @@ Instead, the context :math:`C` for validation of the module's content is constru * :math:`C'.\CREFS` is the same as :math:`C.\CREFS`, - * :math:`C'.\CEXNS` is the same as :math:`C.\CEXNS`, + * :math:`C'.\CTAGS` is the same as :math:`C.\CTAGS`, * all other fields are empty. @@ -630,8 +630,8 @@ Instead, the context :math:`C` for validation of the module's content is constru * For each :math:`\mem_i` in :math:`\module.\MMEMS`, the definition :math:`\mem_i` must be :ref:`valid ` with a :ref:`memory type ` :math:`\X{mt}_i`. - * For each :math:`\exn_i` in :math:`\module.\MEXNS`, - the definition :math:`\exn_i` must be :ref:`valid ` with an :ref:`exception type ` :math:`\X{exnt}_i`. + * For each :math:`\tag_i` in :math:`\module.\MTAGS`, + the definition :math:`\tag_i` must be :ref:`valid ` with an :ref:`tag type ` :math:`\X{tagt}_i`. * For each :math:`\global_i` in :math:`\module.\MGLOBALS`: @@ -663,7 +663,7 @@ Instead, the context :math:`C` for validation of the module's content is constru * Let :math:`\X{mt}^\ast` be the concatenation of the internal :ref:`memory types ` :math:`\X{mt}_i`, in index order. -* Let :math:`\X{exnt}^\ast` be the concatenation of the internal :ref:`exception types ` :math:`\X{exnt}_i`, in index order. +* Let :math:`\X{tagt}^\ast` be the concatenation of the internal :ref:`tag types ` :math:`\X{tagt}_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. @@ -686,7 +686,7 @@ Instead, the context :math:`C` for validation of the module's content is constru \quad (C \vdashmem \mem : \X{mt})^\ast \quad - (C \vdashexn \exn : \X{exnt})^\ast + (C \vdashtag \tag : \X{tagt})^\ast \\ (C' \vdashglobal \global : \X{gt})^\ast \\ @@ -706,16 +706,16 @@ Instead, the context :math:`C` for validation of the module's content is constru \qquad \X{imt}^\ast = \etmems(\X{it}^\ast) \\ - \X{iet}^\ast = \etexns(\X{it}^\ast) + \X{itagt}^\ast = \ettags(\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, \CEXNS~\X{iet}^\ast\,\X{exnt}^\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, \CTAGS~\X{itagt}^\ast\,\X{tagt}^\ast,\\ \CGLOBALS~\X{igt}^\ast\,\X{gt}^\ast, \CELEMS~\X{rt}^\ast, \CDATAS~{\ok}^n, \CREFS~x^\ast \} \\ - C' = \{ \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS), \CEXNS~(C.\CEXNS) \} + C' = \{ \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS), \CTAGS~(C.\CTAGS) \} \\ |C.\CMEMS| \leq 1 \qquad @@ -727,7 +727,7 @@ Instead, the context :math:`C` for validation of the module's content is constru \MFUNCS~\func^\ast, \MTABLES~\table^\ast, \MMEMS~\mem^\ast, - \MEXNS~\exn^\ast, + \MTAGS~\tag^\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 f6d858a6..932038eb 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:`exception types ` and to :ref:`limits `, which must be checked during validation. +However, restrictions apply to :ref:`exception tag 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,13 +146,13 @@ Memory Types } -.. index:: exception type, function type - pair: validation; exception type - single: abstract syntax; exception type -.. _valid-exntype: +.. index:: tag type, function type, exception tag + pair: validation; tag type + single: abstract syntax; tag type +.. _valid-tagtype: -Exception Types -~~~~~~~~~~~~~~~ +Tag Types +~~~~~~~~~ :math:`[t_1^n] \to [t_2^m]` ........................... @@ -161,13 +161,13 @@ Exception Types * The type sequence :math:`t_2^m` must be empty. -* Then the exception type is valid. +* Then the tag type is valid. .. math:: \frac{ \vdashfunctype [t^n] \to [] \ok }{ - \vdashexntype [t^n] \to [] \ok + \vdashtagtype [t^n] \to [] \ok } @@ -241,18 +241,18 @@ External Types \vdashexterntype \ETMEM~\memtype \ok } -:math:`\ETEXN~\exntype` +:math:`\ETTAG~\tagtype` ....................... -* The :ref:`exception type ` :math:`\exntype` must be :ref:`valid `. +* The :ref:`tag type ` :math:`\tagtype` must be :ref:`valid `. * Then the external type is valid. .. math:: \frac{ - \vdashexntype \exntype \ok + \vdashtagtype \tagtype \ok }{ - \vdashexterntype \ETEXN~\exntype \ok + \vdashexterntype \ETTAG~\tagtype \ok } :math:`\ETGLOBAL~\globaltype` @@ -377,20 +377,20 @@ An :ref:`external type ` :math:`\ETMEM~\limits_1` matches :ma } -.. index:: exception type, value type -.. _match-exntype: +.. index:: tag type, value type +.. _match-tagtype: -Exceptions -.......... +Tags +.... -An :ref:`external type ` :math:`\ETEXN~\exntype_1` matches :math:`\ETEXN~\exntype_2` if and only if: +An :ref:`external type ` :math:`\ETTAG~\tagtype_1` matches :math:`\ETTAG~\tagtype_2` if and only if: -* Both :math:`\ETEXN~\exntype_1` and :math:`\ETEXN~\exntype_2` are the same. +* Both :math:`\ETTAG~\tagtype_1` and :math:`\ETTAG~\tagtype_2` are the same. .. math:: \frac{ }{ - \vdashexterntypematch \ETEXN~\exntype \matchesexterntype \ETEXN~\exntype + \vdashexterntypematch \ETTAG~\tagtype \matchesexterntype \ETTAG~\tagtype } From a34f14fa855eb5742b4a0dd37e1cbf1a080c8549 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Fri, 27 May 2022 23:34:25 +0200 Subject: [PATCH 02/13] Apply suggestions from code review Co-authored-by: Heejin Ahn Co-authored-by: Andreas Rossberg --- document/core/appendix/algorithm.rst | 4 ++-- document/core/appendix/index-types.rst | 2 +- document/core/appendix/properties.rst | 4 ++-- document/core/binary/instructions.rst | 2 +- document/core/exec/instructions.rst | 13 ++++++------- document/core/exec/modules.rst | 2 +- document/core/exec/runtime.rst | 12 ++++++------ document/core/syntax/instructions.rst | 10 +++++----- document/core/syntax/types.rst | 2 +- document/core/text/instructions.rst | 18 ++++++++++-------- document/core/text/modules.rst | 2 +- document/core/valid/conventions.rst | 2 +- document/core/valid/instructions.rst | 4 ++-- document/core/valid/types.rst | 3 +-- 14 files changed, 40 insertions(+), 40 deletions(-) diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index 8a35bcef..f06d84e0 100644 --- a/document/core/appendix/algorithm.rst +++ b/document/core/appendix/algorithm.rst @@ -217,13 +217,13 @@ Other instructions are checked in a similar manner. case (catch) let frame = pop_ctrl() error_if(frame.opcode =/= try || frame.opcode =/= catch) - let tagparams = tags.[x].type.params + let tagparams = tags[x].type.params push_ctrl(catch, tagparams , frame.end_types) case (catch_all) let frame = pop_ctrl() error_if(frame.opcode =/= try || frame.opcode =/= catch) - push_ctrl(catch_all, [] , frame.end_types) + push_ctrl(catch_all, [], frame.end_types) case (br n) error_if(ctrls.size() < n) diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst index 185a034e..5ec06bf4 100644 --- a/document/core/appendix/index-types.rst +++ b/document/core/appendix/index-types.rst @@ -16,7 +16,7 @@ Category Constructor (reserved) :math:`\hex{7A}` .. :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{6D}` .. :math:`\hex{61}` +(reserved) :math:`\hex{6E}` .. :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|) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 7438e9ec..5f74e8a5 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -618,7 +618,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera S; C,\CLABELS\,[t^\ast] \vdashinstrseq \instr^\ast : [] \to [t^\ast] \\ \end{array} }{ - S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CATCHadm\{\tagaddr^?~\instr'^\ast\}^\ast~\instr^\ast~\END : [] \to [t^\ast] + S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CATCHadm\{\tagaddr^?~{\instr'}^\ast\}^\ast~\instr^\ast~\END : [] \to [t^\ast] } @@ -650,7 +650,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera \frac{ S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t'^\ast]\to[] \qquad - (val:t')^\ast + (val : t')^\ast \qquad S; C,\CLABELS\,(\catch~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] }{ diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 1bd5744a..b67e41d5 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -21,7 +21,7 @@ The only exception are :ref:`structured control instructions ` have varying encodings. For structured instructions, the instruction sequences forming nested blocks are separated or terminated with explicit opcodes for |END|, |ELSE|, |CATCH|, |CATCHALL|, and |DELEGATE|. +:ref:`Control instructions ` have varying encodings. For structured instructions, the instruction sequences forming nested blocks are separated or terminated with explicit opcodes for |END|, |ELSE|, |CATCH|, |CATCHALL|, and |DELEGATE|. :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 `. diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index b227ebfe..87cdd294 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2632,7 +2632,7 @@ Control Instructions \begin{array}{l} F; \val^n~(\TRY~\X{bt}~\instr_1^\ast~(\CATCH~x~\instr_2^\ast)^\ast~(\CATCHALL~\instr_3^\ast)^?~\END \quad \stepto \\ - \qquad F; \LABEL_m\{\}~(\CATCHadm\{a~\instr_2^\ast\}^\ast\{\epsilon~\instr_3\}^?~\val^n~\instr_1^\ast~\END)~\END \\ + \qquad F; \LABEL_m\{\}~(\CATCHadm\{a~\instr_2^\ast\}^\ast\{\epsilon~\instr_3\ast\}^?~\val^n~\instr_1^\ast~\END)~\END \\ (\iff \expand_F(\X{bt}) = [t_1^n] \to [t_2^m] \land (F.\AMODULE.\MITAGS[x]=a)^\ast) \end{array} @@ -2983,8 +2983,7 @@ Entering an exception handler :math:`H` .. note:: No formal reduction rule is needed for installing an exception :ref:`handler ` because it is an :ref:`administrative instruction ` - that the :ref:`try ` instruction reduced to directly. - + that the :ref:`try ` instruction reduces to directly. .. _exec-handler-exit: @@ -3023,15 +3022,15 @@ Throwing an exception with :ref:`tag address ` :math:`a` .. math:: \begin{array}{rcl} - \CATCHadm\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast~\XT[\val^n~(\THROWadm~a)]~\END &\stepto& - \CATCHadm\{a'^?~\instr'^\ast\}^\ast~\XT[\val^n~(\THROWadm~a)]~\END \\ + \CATCHadm\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast~\XT[(\THROWadm~a)]~\END &\stepto& + \CATCHadm\{a'^?~\instr'^\ast\}^\ast~\XT[(\THROWadm~a)]~\END \\ && (\iff a_1^? \neq \epsilon \land a_1^? \neq a) \\ S;~\CATCHadm\{a_1^?~\instr^\ast\}\{a'^?~\instr'^\ast\}^\ast~\XT[\val^n~(\THROWadm~a)]~\END &\stepto& S;~\CAUGHTadm\{a~\val^n\}~(\val^n)?~\instr^\ast~\END \\ && (\iff~(a_1^? = \epsilon \lor a_1^? = a)~\land\\ && \ S.\STAGS[a].\TAGITYPE = [t^n]\to[]) \\ - \LABEL_n\{\}~\XB^l[\DELEGATEadm\{l\}~\XT[\val^n~(\THROWadm~a)]~\END]~\END &\stepto& - \val^n~(\THROWadm~a) \\ + \LABEL_n\{\}~\XB^l[\DELEGATEadm\{l\}~\XT[(\THROWadm~a)]~\END]~\END &\stepto& + \XT[(\THROWadm~a)] \\ \end{array} .. _exec-caughtadm: diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 2819bb80..7bfbb852 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -83,7 +83,7 @@ The following auxiliary typing rules specify this typing relation relative to a .. math:: \frac{ }{ - S \vdashexternval \EVTAG~a : \ETTAG~(S.\STAGS[a].\TAGITYPE) + S \vdashexternval \EVTAG~a : \ETTAG~S.\STAGS[a].\TAGITYPE } diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 422da4d9..8d561ccb 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -594,7 +594,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 `, :ref:`exception handling `, and :ref:`control instructions `, the syntax of instructions is extended to include the following *administrative instructions*: +In order to express the reduction of :ref:`traps `, :ref:`calls `, :ref:`exception handling `, and :ref:`control instructions `, the syntax of instructions is extended to include the following *administrative instructions*: .. math:: \begin{array}{llcl} @@ -606,9 +606,9 @@ In order to express the reduction of :ref:`traps `, :ref:`calls `, identified by its :ref:`address `. The values it will consume depend on its :ref:`tag type `. -It unifies the throwing of different forms of exceptions. +It unifies the different forms of throwing exceptions. The |LABEL|, |FRAME|, |CATCHadm|, |DELEGATEadm|, and |CAUGHTadm| instructions model :ref:`labels `, :ref:`frames `, active :ref:`catching exception handlers `, active :ref:`delegating exception handlers `, and :ref:`caught exceptions `, 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. @@ -712,7 +712,7 @@ the following syntax of *throw contexts* is defined, as well as associated struc \production{(throw contexts)} & \XT &::=& \val^\ast~[\_]~\instr^\ast \\ &&|& \LABEL_n\{\instr^\ast\}~\XT~\END \\ &&|& - \CAUGHTadm\{a~\val^\ast\}~\XT~\END \\ &&|& + \CAUGHTadm\{\tagaddr~\val^\ast\}~\XT~\END \\ &&|& \FRAME_n\{F\}~\XT~\END \\ \end{array} @@ -733,7 +733,7 @@ Throw contexts allow matching the program context around a throw instruction up \stepto & S;~F;~\LABEL_n\{\} (\CATCHadm\{a~\RETURN\}~~\val^n~\THROWadm~a~\END)~\END \\ \end{array} - :ref:`Handling ` the thrown exception with tag address :math:`a` in the throw context + :ref:`Handling ` the thrown exception with tag address :math:`a` in the throw context :math:`T=[\_]`, with the exception handler :math:`H=\CATCHadm\{a~\RETURN\}` gives: .. math:: diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 73781223..a12ab304 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -643,8 +643,8 @@ 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~\tagidx~\instr^\ast)^\ast~(\CATCHALL~\instr^\ast)^?~\END \\ &&|& - \TRY~\blocktype~instr^\ast~\DELEGATE~\labelidx \\ &&|& + \TRY~\blocktype~\instr^\ast~(\CATCH~\tagidx~\instr^\ast)^\ast~(\CATCHALL~\instr^\ast)^?~\END \\ &&|& + \TRY~\blocktype~\instr^\ast~\DELEGATE~\labelidx \\ &&|& \THROW~\tagidx \\&&|& \RETHROW~\labelidx \\ &&|& \BR~\labelidx \\&&|& @@ -666,9 +666,9 @@ and terminated with either an |END| or a |DELEGATE| pseudo-instruction. As the grammar prescribes, they must be well-nested. The instructions |TRY|, |THROW|, and |RETHROW|, are concerned with handling exceptions. -The |TRY| instructions create try-blocks, and either may handle or rethrow exceptions in the case of |CATCH| and |CATCHALL|, -or delegate exceptions to an outer potentially catching try-block in the case of |DELEGATE|. -The |THROW| and |RETHROW| instructions alter control flow by searching for a matching handler in an enclosing catching-try block, if any. +The |TRY| instruction installs an exception handler, and may either handle exceptions in the case of |CATCH| and |CATCHALL|, +or rethrow them in an outer block in the case of |DELEGATE|. +The |THROW| and |RETHROW| instructions alter control flow by searching for a matching handler in one of the enclosing |TRY| blocks, 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^?]`. diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 3723bc67..b1c164cc 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -237,7 +237,7 @@ Tag Types \production{tag type} &\tagtype &::=& \functype \\ \end{array} -Currently tags are only used for categorising exceptions. +Currently tags are only used for categorizing exceptions. The parameters of |functype| define the list of values associated with the exception thrown with this tag. Furthermore, it is an invariant of the semantics that every |functype| in a :ref:`valid ` tag type for an exception has an empty result type. diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 7d1917b5..42a6e23d 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -89,11 +89,11 @@ However, the special case of a type use that is syntactically empty or consists \text{try}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}_1{:}\Tinstr_{I'})^\ast~~ (\text{catch}~~\Tid_1^?~~x{:}\Ttagidx_I~~(\X{in}_2{:}\Tinstr_{I'})^\ast)^\ast~~ \\ &&&\qquad\qquad (\text{catch\_all}~~\Tid_1^?~~(\X{in}_3{:}\Tinstr_{I'})^\ast)^?~~\text{end}~~\Tid_2^? - \\ &&&\qquad \Rightarrow\quad \TRY~\X{rt}~\X{in}_1^\ast~(\CATCH~x~\X{in}_2^\ast)^\ast~(\CATCHALL~\X{in}_3^\ast)^?~\END + \\ &&&\qquad \Rightarrow\quad \TRY~\X{bt}~\X{in}_1^\ast~(\CATCH~x~\X{in}_2^\ast)^\ast~(\CATCHALL~\X{in}_3^\ast)^?~\END \\ &&&\qquad\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{delegate}~~l{:}\Tlabelidx_I~~\X{l}{:}\Tlabelidx_I - \\ &&&\qquad \Rightarrow\quad \TRY~\X{rt}~\X{in}_1^\ast~\DELEGATE~l + \\ &&&\qquad \Rightarrow\quad \TRY~\X{bt}~\X{in}_1^\ast~\DELEGATE~l \qquad\quad~~ (\iff \Tid^? = \epsilon \vee \Tid^? = \Tlabel) \\ \end{array} @@ -932,15 +932,17 @@ Such a folded instruction can appear anywhere a regular instruction can. &\equiv\quad \text{loop}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{end} \\ \end{array}\\ \begin{array}{lr} - \text{(}~\text{if}~~\Tlabel~~\Tblocktype~~\Tfoldedinstr^\ast + \text{(}~\text{if}~~\Tlabel~~\Tblocktype~~\Tfoldedinstr^\ast~~ \text{(}~\text{then}~~\Tinstr_1^\ast~\text{)}~~\text{(}~\text{else}~~\Tinstr_2^\ast~\text{)}^?~~\text{)} & \equiv \\ - \qquad \Tfoldedinstr^\ast~~\text{if}~~\Tlabel~~\Tblocktype \Tinstr_1^\ast~~\text{else}~~(\Tinstr_2^\ast)^?~\text{end} &\\ + \qquad \Tfoldedinstr^\ast~~\text{if}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast~~\text{else}~~(\Tinstr_2^\ast)^?~~\text{end} &\\ \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do}~~\Tinstr_1^\ast~~\text{)} - \qquad (\text{(}~\text{catch}~~\Tinstr_2^\ast~\text{)})^\ast &\\ - \qquad\qquad (\text{(}~\text{catch_all}~~\Tinstr_3^\ast~\text{)})^?~\text{)} & \equiv \\ - \text{try}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast (\text{delegate}~~\Tlabelidx & \equiv \\ - \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{delegate}~~l~\text{)} &\\ ++ \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do}~~\Tinstr_1^\ast~~\text{)}~~ ++ (\text{(}~\text{catch}~~\Tinstr_2^\ast~\text{)})^\ast &\\ ++ \qquad\qquad(\text{(}~\text{catch\_all}~~\Tinstr_3^\ast~\text{)})^?~\text{)} & \equiv \\ ++ \qquad\text{try}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast~~(\text{catch}~~\Tinstr_2^\ast)^\ast~~(\text{catch\_all}~~\Tinstr_3^\ast)^?~~\text{end} &\\ ++ \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{delegate}~~l~\text{)} & \equiv \\ ++ \qquad\text{try}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{delegate}~~\Tlabelidx &\\ \end{array} .. note:: diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index 488f4642..2f1481ca 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -428,7 +428,7 @@ Tags can be defined as :ref:`imports ` or :ref:`exports ` :math: & \CELEMS & \reftype^\ast, \\ & \CDATAS & {\ok}^\ast, \\ & \CLOCALS & \valtype^\ast, \\ - & \CLABELS & \labelkind, \\ + & \CLABELS & \labelkind^\ast, \\ & \CRETURN & \resulttype^?, \\ & \CREFS & \funcidx^\ast ~\} \\ \end{array} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 6e9e601b..f23c4f10 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1378,7 +1378,7 @@ Control Instructions (C,\CLABELS\,(\catch~[t_2^\ast]) \vdashinstrseq \instr_3^\ast : []\to[t_2^\ast])^? \end{array} }{ - C \vdashinstr \TRY~\blocktype~\instr^\ast (\CATCH~x~\instr_2^\ast)^\ast (\CATCHALL~\instr_3^\ast)^? end : [t_1^\ast]\to[t_2^\ast] + C \vdashinstr \TRY~\blocktype~\instr^\ast (\CATCH~x~\instr_2^\ast)^\ast (\CATCHALL~\instr_3^\ast)^? \END : [t_1^\ast]\to[t_2^\ast] } @@ -1437,7 +1437,7 @@ Control Instructions .. math:: \frac{ - C.\CLABELS[l] = (\catch [t^\ast]) + C.\CLABELS[l] = \catch~[t^\ast] }{ C \vdashinstr \RETHROW~l : [t_1^\ast] \to [t_2^\ast] } diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 932038eb..4aebbeae 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -165,9 +165,8 @@ Tag Types .. math:: \frac{ - \vdashfunctype [t^n] \to [] \ok }{ - \vdashtagtype [t^n] \to [] \ok + \vdashtagtype [t^\ast] \to [] \ok } From 7c4f707ec1e86829b0624cdabef1faf3a9ddcc21 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 6 Jul 2022 20:04:20 +0200 Subject: [PATCH 03/13] Addressed some of the review comments. Pending to address the rest. --- document/core/appendix/algorithm.rst | 3 ++- document/core/appendix/properties.rst | 15 +++++++++------ document/core/binary/types.rst | 2 +- document/core/exec/instructions.rst | 23 ++++++++++++++--------- document/core/exec/runtime.rst | 26 +++++++++++++++++--------- document/core/syntax/instructions.rst | 4 +++- document/core/text/instructions.rst | 12 ++++++------ document/core/util/macros.def | 12 ++++++------ document/core/valid/conventions.rst | 10 +++++----- document/core/valid/instructions.rst | 18 +++++++++++------- 10 files changed, 74 insertions(+), 51 deletions(-) diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index f06d84e0..9e8dfacb 100644 --- a/document/core/appendix/algorithm.rst +++ b/document/core/appendix/algorithm.rst @@ -247,7 +247,8 @@ Other instructions are checked in a similar manner. pop_vals(label_types(ctrls[m])) unreachable() - +.. todo:: + Add a case for :code:`throw`. .. note:: It is an invariant under the current WebAssembly instruction set that an operand of :code:`Unknown` type is never duplicated on the stack. diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 5f74e8a5..9649b45a 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -608,13 +608,14 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera :math:`\CATCHadm\{\tagaddr^?~\instr'^\ast\}^\ast~\instr^\ast~\END` .................................................................. -**TODO: add prose** - +.. todo:: + Add prose. .. math:: \frac{ \begin{array}{c} - ((S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t'^\ast]\to[])^?~~\land~~S; C,\CLABELS\,(\catch~[t^\ast]) \vdashinstrseq \instr'^\ast : [(t'^\ast)^?] \to [t^\ast])^\ast \\ + ((S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t'^\ast]\to[])^? \\ + ~~S; C,\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr'^\ast : [(t'^\ast)^?] \to [t^\ast])^\ast \\ S; C,\CLABELS\,[t^\ast] \vdashinstrseq \instr^\ast : [] \to [t^\ast] \\ \end{array} }{ @@ -627,7 +628,8 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera :math:`\DELEGATEadm\{l\}~\instr^\ast~\END` .......................................... -**TODO: add prose** +.. todo:: + Add prose. .. math:: \frac{ @@ -644,7 +646,8 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera :math:`\CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END` ......................................................... -**TODO: add prose** +.. todo:: + Add prose. .. math:: \frac{ @@ -652,7 +655,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera \qquad (val : t')^\ast \qquad - S; C,\CLABELS\,(\catch~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] + S; C,\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] }{ S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] } diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index c44a04a1..4cb91225 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -201,7 +201,7 @@ Tag Types \hex{00}~~ft{:}\Bfunctype &\Rightarrow& ft \\ \end{array} -The |Bfunctype| of a tag must have an empty result, and it is used to characterise exceptions. +The |Bfunctype| of a tag is used to characterise exceptions. The :math:`\hex{00}` bit signifies an exception and is currently the only allowed value. .. note:: diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 87cdd294..c775c937 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2625,7 +2625,8 @@ Control Instructions :math:`\TRY~\blocktype~\instr_1^\ast~(\CATCH~x~\instr_2^\ast)^\ast~(\CATCHALL~\instr_3^\ast)^?~\END` .................................................................................................... -**TODO: Add prose** +.. todo:: + Add prose for the |TRY| - |CATCH| - |CATCHALL| execution step. .. math:: ~\\[-1ex] @@ -2642,7 +2643,8 @@ Control Instructions :math:`\TRY~\blocktype~\instr^\ast~\DELEGATE~l` ............................................... -**TODO: Add prose** +.. todo:: + Add prose for the |TRY| - |DELEGATE| execution step. .. math:: ~\\[-1ex] @@ -2652,10 +2654,6 @@ Control Instructions && (\iff \expand_F(\X{bt}) = [t_1^n] \to [t_2^m]) \end{array} -.. note:: - Note that the last reduction step above is similar to the :ref:`reduction ` of :math:`\BR~l`, but also doing a throw after it breaks. - - There is a subtle difference though. The instruction :math:`\BR~l` searches for the :math:`l+1` surrounding block and breaks out after that block. Because :math:`\DELEGATEadm\{l\}` is always wrapped in its own label, with the :ref:`same lookup ` as for :math:`\BR~l` we end up breaking inside the :math:`l+1` surrounding block and throwing there. So if that :math:`l+1` surrounding block is a try, we end up throwing in its "try code", and thus correctly getting delegated to that try's handlers. .. _exec-throw: @@ -2682,7 +2680,8 @@ Control Instructions :math:`\RETHROW~l` .................. -**TODO: Add prose** +.. todo:: + Add prose for the |RETHROW| execution step. .. math:: ~\\[-1ex] @@ -3017,7 +3016,8 @@ When the end of a :ref:`try ` instruction is reached without a jump, Throwing an exception with :ref:`tag address ` :math:`a` ........................................................................ -**TODO: add prose** +.. todo:: + Add prose for the following execution steps. .. math:: @@ -3033,12 +3033,17 @@ Throwing an exception with :ref:`tag address ` :math:`a` \XT[(\THROWadm~a)] \\ \end{array} + +.. todo:: + Add explainer note. + .. _exec-caughtadm: Holding a caught exception with |CAUGHTadm| ........................................... -**TODO: add prose describing the administrative** |CAUGHTadm| +.. todo:: + Add prose describing the administrative |CAUGHTadm| execution step. .. math:: \begin{array}{rcl} diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 8d561ccb..7b614c24 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -83,7 +83,8 @@ It is either a sequence of :ref:`values ` or a :ref:`trap ` possibly following a :ref:`tag address `. If there is no :ref:`tag address `, the instructions of that target correspond to a |CATCHALL| clause. -**TODO: add prose** for delegating handlers. +.. todo:: + Add prose for delegating handlers. .. math:: \begin{array}{llllll} - \production{(handler)} & \X{handler} &::=& \CATCHadm\{a^?~\instr^\ast\}^\ast &|& \DELEGATEadm\{l\} + \production{(handler)} & \handler &::=& \CATCHadm\{\tagaddr^?~\instr^\ast\}^\ast &|& \DELEGATEadm\{l\} \end{array} -Intuitively, :math:`\CATCHadm\{a^?~\instr^\ast\}^\ast` maps exception tag addreses to possible *continuations* to execute -when the handler catches a thrown exception. +Intuitively, for each target :math:`\{\tagaddr^?~\instr^\ast\}` of a |CATCHadm|, :math:`\instr^\ast` is the *continuation* to execute +when the handler catches a thrown exception with tag |tagaddr|, or for any exception, when a target specifies no tag address. If this list of targets is empty, or if the tag address of the thrown exception is not in the handler's mapping and there is no |CATCHALL| clause, then the exception will be rethrown. -**TODO: add prose** with intuition on delegating handlers. +.. todo:: + Add prose with intuition on delegating handlers. .. _exec-expand: @@ -722,7 +725,7 @@ Throw contexts allow matching the program context around a throw instruction up Contrary to block contexts, throw contexts don't skip over handlers. Since handlers are not included above, there is always a unique maximal throw context to match the reduction rules. - This basically means that :math:`\CAUGHTadm {..} instr^\ast \END` is not a potential catching block for exceptions thrown by :math:`\instr^\ast`, since it is inside a |handler|'s block. + This basically means that :math:`\CAUGHTadm {\dots} instr^\ast \END` is not a potential catching block for exceptions thrown by :math:`\instr^\ast`, since these are instructions in the scope of a |CATCH| or a |CATCHALL|. .. note:: For example, catching a simple :ref:`throw ` in a :ref:`try block ` would be as follows. @@ -746,7 +749,11 @@ Throw contexts allow matching the program context around a throw instruction up In this particular case, the exception is caught by the exception handler :math:`H` and its values are returned. - **TODO: add administrative values to describe unresolved throws:** e.g., |EXCEPTION| +.. todo:: + Include a more complex example using a throw context other then `T=[\_]` + +.. todo:: + Add administrative values to describe unresolved throws. .. index:: ! configuration, ! thread, store, frame, instruction, module instruction @@ -804,7 +811,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:`\THROWadm~\tagaddr`, **and extend results to include such situations.** (e.g., |EXCEPTION|) +.. todo:: + Add rules to deal with unresolved :math:`\THROWadm~\tagaddr`, 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/syntax/instructions.rst b/document/core/syntax/instructions.rst index a12ab304..1fcaf896 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -685,7 +685,9 @@ The exact effect depends on that control construct. In case of |BLOCK| or |IF| it is a *forward jump*, resuming execution after the matching |END|. In case of |LOOP| it is a *backward jump* to the beginning of the loop. -**TODO: add prose** - for try-delegate's jump. + +.. todo:: + Add prose for try-delegate's jump. .. note:: This enforces *structured control flow*. diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 42a6e23d..9c8a2bee 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -937,12 +937,12 @@ Such a folded instruction can appear anywhere a regular instruction can. & \equiv \\ \qquad \Tfoldedinstr^\ast~~\text{if}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast~~\text{else}~~(\Tinstr_2^\ast)^?~~\text{end} &\\ \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do}~~\Tinstr_1^\ast~~\text{)} -+ \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do}~~\Tinstr_1^\ast~~\text{)}~~ -+ (\text{(}~\text{catch}~~\Tinstr_2^\ast~\text{)})^\ast &\\ -+ \qquad\qquad(\text{(}~\text{catch\_all}~~\Tinstr_3^\ast~\text{)})^?~\text{)} & \equiv \\ -+ \qquad\text{try}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast~~(\text{catch}~~\Tinstr_2^\ast)^\ast~~(\text{catch\_all}~~\Tinstr_3^\ast)^?~~\text{end} &\\ -+ \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{delegate}~~l~\text{)} & \equiv \\ -+ \qquad\text{try}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{delegate}~~\Tlabelidx &\\ + \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do}~~\Tinstr_1^\ast~~\text{)}~~ + (\text{(}~\text{catch}~~\Tinstr_2^\ast~\text{)})^\ast &\\ + \qquad\qquad(\text{(}~\text{catch\_all}~~\Tinstr_3^\ast~\text{)})^?~\text{)} & \equiv \\ + \qquad\text{try}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast~~(\text{catch}~~\Tinstr_2^\ast)^\ast~~(\text{catch\_all}~~\Tinstr_3^\ast)^?~~\text{end} &\\ + \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{delegate}~~l~\text{)} & \equiv \\ + \qquad\text{try}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{delegate}~~\Tlabelidx &\\ \end{array} .. note:: diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 9a15564c..032b7128 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -894,11 +894,8 @@ .. |ok| mathdef:: \mathrel{\mbox{ok}} .. |const| mathdef:: \xref{valid/instructions}{valid-constant}{\mathrel{\mbox{const}}} -.. |catch| mathdef:: \xref{valid/conventions}{valid-labelkind}{\mathrel{\mbox{catch}}} -.. |labelkind| mathdef:: \xref{valid/conventions}{valid-labelkind}{\mathrel{\X{labelkind}}} - -.. Contexts +.. Contexts, terminals .. |CTYPES| mathdef:: \xref{valid/conventions}{context}{\K{types}} .. |CFUNCS| mathdef:: \xref{valid/conventions}{context}{\K{funcs}} @@ -912,6 +909,11 @@ .. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}} .. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}} .. |CREFS| mathdef:: \xref{valid/conventions}{context}{\K{refs}} +.. |LCATCH| mathdef:: \xref{valid/conventions}{valid-labeltype}{\mathrel{\K{catch}}} + +.. Contexts, non-terminals + +.. |labeltype| mathdef:: \xref{valid/conventions}{valid-labeltype}{\mathrel{\X{labeltype}}} .. Judgments @@ -1316,5 +1318,3 @@ .. |error| mathdef:: \xref{appendix/embedding}{embed-error}{\X{error}} .. |ERROR| mathdef:: \xref{appendix/embedding}{embed-error}{\K{error}} -.. |exception| mathdef:: \xref{appendix/embedding}{embed-exception}{\X{exception}} -.. |EXCEPTION| mathdef:: \xref{appendix/embedding}{embed-exception}{\K{exception}} \ No newline at end of file diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 57326d30..e7ea5288 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -24,9 +24,9 @@ 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, tag type, global type, value type, result type, index space, module, function, tag, labelkind +.. index:: ! context, function type, table type, memory type, tag type, global type, value type, result type, index space, module, function, tag, labeltype .. _context: -.. _labelkind: +.. _labeltype: Contexts ~~~~~~~~ @@ -43,7 +43,7 @@ which collects relevant information about the surrounding :ref:`module ` that occur in the module outside functions and can hence be used to form references inside them. @@ -56,7 +56,7 @@ More concretely, contexts are defined as :ref:`records ` :math: .. math:: \begin{array}{llll} - \production{(labelkind)} & \labelkind & ::= & \catch^?~\resulttype^\ast\\ + \production{(labeltype)} & \labeltype & ::= & \LCATCH^?~\resulttype\\ \production{(context)} & C &::=& \begin{array}[t]{l@{~}ll} \{ & \CTYPES & \functype^\ast, \\ @@ -68,7 +68,7 @@ More concretely, contexts are defined as :ref:`records ` :math: & \CELEMS & \reftype^\ast, \\ & \CDATAS & {\ok}^\ast, \\ & \CLOCALS & \valtype^\ast, \\ - & \CLABELS & \labelkind^\ast, \\ + & \CLABELS & \labeltype^\ast, \\ & \CRETURN & \resulttype^?, \\ & \CREFS & \funcidx^\ast ~\} \\ \end{array} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index f23c4f10..48dec1e2 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1366,7 +1366,8 @@ Control Instructions :math:`\TRY~\blocktype~\instr_1^\ast~(\CATCH~x~\instr_2^\ast)^\ast~(\CATCHALL~\instr_3^\ast)^?~\END` .................................................................................................... -**TODO: add prose** +.. todo:: + Add prose. .. math:: \frac{ @@ -1374,8 +1375,9 @@ Control Instructions 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] \\ - (C.\CTAGS[x] = [t^\ast]\to[]~\land~C,\CLABELS\,(\catch [t_2^\ast]) \vdashinstrseq \instr_2^\ast : [t^\ast]\to[t_2^\ast])\ast \\ - (C,\CLABELS\,(\catch~[t_2^\ast]) \vdashinstrseq \instr_3^\ast : []\to[t_2^\ast])^? + (C.\CTAGS[x] = [t^\ast]\to[] \\ + C,\CLABELS\,(\LCATCH [t_2^\ast]) \vdashinstrseq \instr_2^\ast : [t^\ast]\to[t_2^\ast])\ast \\ + (C,\CLABELS\,(\LCATCH~[t_2^\ast]) \vdashinstrseq \instr_3^\ast : []\to[t_2^\ast])^? \end{array} }{ C \vdashinstr \TRY~\blocktype~\instr^\ast (\CATCH~x~\instr_2^\ast)^\ast (\CATCHALL~\instr_3^\ast)^? \END : [t_1^\ast]\to[t_2^\ast] @@ -1383,7 +1385,7 @@ Control Instructions .. note:: - The :ref:`notation ` :math:`C,\CLABELS\,(\labelkind^? [t^\ast])` inserts the new label type at index :math:`0`, shifting all others. + The :ref:`notation ` :math:`C,\CLABELS\,(\LCATCH^? [t^\ast])` inserts the new label type at index :math:`0`, shifting all others. .. _valid-try-delegate: @@ -1391,7 +1393,8 @@ Control Instructions :math:`\TRY~\blocktype~\instr^\ast~\DELEGATE~l` ............................................... -**TODO: add prose** +.. todo:: + Add prose. .. math:: \frac{ @@ -1433,11 +1436,12 @@ Control Instructions :math:`\RETHROW~l` .................. -**TODO: add prose** +.. todo:: + Add prose. .. math:: \frac{ - C.\CLABELS[l] = \catch~[t^\ast] + C.\CLABELS[l] = \LCATCH~[t^\ast] }{ C \vdashinstr \RETHROW~l : [t_1^\ast] \to [t_2^\ast] } From d21ac52db54e60af44a674ee02e9fbc39fd4a386 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Thu, 11 Aug 2022 11:57:43 +0200 Subject: [PATCH 04/13] Finished addressing review comments. --- document/core/appendix/properties.rst | 4 ++-- document/core/exec/runtime.rst | 28 +++++++++++++++++---------- document/core/text/instructions.rst | 1 - document/core/valid/instructions.rst | 2 +- 4 files changed, 21 insertions(+), 14 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 9649b45a..c9d831bc 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -613,7 +613,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera .. math:: \frac{ - \begin{array}{c} + \begin{array}{@{}c@{}} ((S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t'^\ast]\to[])^? \\ ~~S; C,\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr'^\ast : [(t'^\ast)^?] \to [t^\ast])^\ast \\ S; C,\CLABELS\,[t^\ast] \vdashinstrseq \instr^\ast : [] \to [t^\ast] \\ @@ -635,7 +635,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera \frac{ S; C,\CLABELS\,[t^\ast] \vdashinstrseq \instr^\ast : [] \to [t^\ast] \qquad - |C.\CLABELS| \ge l + C.\CLABELS[l] = [t_0^\ast] }{ S; C,\CLABELS\,[t^\ast] \vdashadmininstr \DELEGATEadm\{l\}~\instr^\ast~\END : [] \to [t^\ast] } diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 7b614c24..44537db0 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -554,6 +554,7 @@ If there is no :ref:`tag address `, the instructions of that tar Intuitively, for each target :math:`\{\tagaddr^?~\instr^\ast\}` of a |CATCHadm|, :math:`\instr^\ast` is the *continuation* to execute when the handler catches a thrown exception with tag |tagaddr|, or for any exception, when a target specifies no tag address. +In that case, we say that the exception is handled by the exception handler |CATCHadm|. If this list of targets is empty, or if the tag address of the thrown exception is not in the handler's mapping and there is no |CATCHALL| clause, then the exception will be rethrown. .. todo:: @@ -730,27 +731,34 @@ Throw contexts allow matching the program context around a throw instruction up .. note:: For example, catching a simple :ref:`throw ` in a :ref:`try block ` would be as follows. + Assume that :math:`\expand_F(bt) = [t1^n] \to [t2^m]`, for some :math:`n > m` such that :math:`t1^n[(n-m):n] = t2^m`, + and that the tag address `a` of :math:`x` corresponds to the tag type :math:`[t2^m] \to []`. + .. math:: \begin{array}{ll} - & \hspace{-5ex} S;~F;~\val^n~(\TRY~\X{bt}~\THROW~x~\CATCH~x~\RETURN~\END) \\ - \stepto & S;~F;~\LABEL_n\{\} (\CATCHadm\{a~\RETURN\}~~\val^n~\THROWadm~a~\END)~\END \\ + & \hspace{-5ex} S;~F;~\val^n~(\TRY~\X{bt}~(\THROW~x)~\CATCH~x~\RETURN~\END) \\ + \stepto & S;~F;~\LABEL_m\{\} (\CATCHadm\{a~\RETURN\}~\val^n~(\THROW~x)~\END)~\END \\ \end{array} - :ref:`Handling ` the thrown exception with tag address :math:`a` in the throw context - :math:`T=[\_]`, with the exception handler :math:`H=\CATCHadm\{a~\RETURN\}` gives: + Denote :math:`\val^n = \val^{n-m} val^m`. + :ref:`Handling the thrown exception ` with tag address :math:`a` in the throw context + :math:`T=[val^{n-m}\_]`, with the exception handler :math:`H=\CATCHadm\{a~\RETURN\}` gives: .. math:: \begin{array}{lll} - \stepto & S;~F;~\LABEL_n\{\}~(\CAUGHTadm\{a~\val^n\}~\val^n~\RETURN~\END)~\END & \hspace{9ex}\ \\ - \stepto & \val^n & \\ + \stepto & S;~F;~\LABEL_m\{\}~(\CAUGHTadm\{a~\val^m\}~\val^m~\RETURN~\END)~\END & \hspace{9ex}\ \\ + \stepto & \val^m & \\ \end{array} - When a throw occurs, execution halts until that throw is the continuation of a throw context in a catching try block. + When a throw occurs, we pop the values :math:`val^m:[t^m]` and append them to the tag address :math:`a` into + a |CAUGHTadm| instruction. We then search for the maximal surrounding throw context `T`, which means we pop + any other values, labels, frames, and |CAUGHTadm| instructions, until we find an exception handler + (corresponding to a try block) that :ref:`handles the exception `. - In this particular case, the exception is caught by the exception handler :math:`H` and its values are returned. + In other words, when a throw occurs, normal execution halts and exceptional execution begins, until the throw + is the continuation (i.e., in the place of a :math:`\_`) of a throw context in a catching try block. -.. todo:: - Include a more complex example using a throw context other then `T=[\_]` + In this particular case, the exception is caught by the exception handler :math:`H` and its values are returned. .. todo:: Add administrative values to describe unresolved throws. diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 9c8a2bee..f0e0a2f9 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -936,7 +936,6 @@ Such a folded instruction can appear anywhere a regular instruction can. \text{(}~\text{then}~~\Tinstr_1^\ast~\text{)}~~\text{(}~\text{else}~~\Tinstr_2^\ast~\text{)}^?~~\text{)} & \equiv \\ \qquad \Tfoldedinstr^\ast~~\text{if}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast~~\text{else}~~(\Tinstr_2^\ast)^?~~\text{end} &\\ - \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do}~~\Tinstr_1^\ast~~\text{)} \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do}~~\Tinstr_1^\ast~~\text{)}~~ (\text{(}~\text{catch}~~\Tinstr_2^\ast~\text{)})^\ast &\\ \qquad\qquad(\text{(}~\text{catch\_all}~~\Tinstr_3^\ast~\text{)})^?~\text{)} & \equiv \\ diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 48dec1e2..fbfbfc86 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1402,7 +1402,7 @@ Control Instructions \qquad C,\CLABELS\,[t_2^\ast] \vdashinstrseq \instr^\ast : [t_1^\ast]\to[t_2^\ast] \qquad - |C.\CLABELS| \ge l + C.\CLABELS[l] = [t^\ast] }{ C \vdashinstrseq \TRY~\blocktype~\instr^\ast~\DELEGATE~l : [t_1^\ast]\to[t_2^\ast] } From 4e7710728251d9607117405b4afd098c139db712 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Thu, 11 Aug 2022 12:07:24 +0200 Subject: [PATCH 05/13] Remerged two arrays in folded instructions, realigned, added missing idxs --- document/core/text/instructions.rst | 30 ++++++++++++++++------------- 1 file changed, 17 insertions(+), 13 deletions(-) diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index f0e0a2f9..40c79249 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -929,21 +929,25 @@ Such a folded instruction can appear anywhere a regular instruction can. \text{(}~\text{block}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~\text{)} &\equiv\quad \text{block}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{end} \\ & \text{(}~\text{loop}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~\text{)} - &\equiv\quad \text{loop}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{end} \\ - \end{array}\\ - \begin{array}{lr} - \text{(}~\text{if}~~\Tlabel~~\Tblocktype~~\Tfoldedinstr^\ast~~ - \text{(}~\text{then}~~\Tinstr_1^\ast~\text{)}~~\text{(}~\text{else}~~\Tinstr_2^\ast~\text{)}^?~~\text{)} - & \equiv \\ - \qquad \Tfoldedinstr^\ast~~\text{if}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast~~\text{else}~~(\Tinstr_2^\ast)^?~~\text{end} &\\ - \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do}~~\Tinstr_1^\ast~~\text{)}~~ - (\text{(}~\text{catch}~~\Tinstr_2^\ast~\text{)})^\ast &\\ - \qquad\qquad(\text{(}~\text{catch\_all}~~\Tinstr_3^\ast~\text{)})^?~\text{)} & \equiv \\ - \qquad\text{try}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast~~(\text{catch}~~\Tinstr_2^\ast)^\ast~~(\text{catch\_all}~~\Tinstr_3^\ast)^?~~\text{end} &\\ - \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{delegate}~~l~\text{)} & \equiv \\ - \qquad\text{try}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{delegate}~~\Tlabelidx &\\ + &\equiv\quad \text{loop}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{end} \\ & + \text{(}~\text{if}~~\Tlabel~~\Tblocktype~~\Tfoldedinstr^\ast + &\hspace{-1ex} \text{(}~\text{then}~~\Tinstr_1^\ast~\text{)}~~(\text{(}~\text{else}~~\Tinstr_2^\ast~\text{)})^?~~\text{)} + \quad\equiv \\ &\qquad + \Tfoldedinstr^\ast~~\text{if}~~\Tlabel + &\hspace{-12ex} \Tblocktype~~\Tinstr_1^\ast~~\text{else}~~(\Tinstr_2^\ast)^?~\text{end} \\ & + \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do} &\hspace{-8ex} \Tinstr_1^\ast~\text{)}~~ + (\text{(}~\text{catch}~~x{:}\Ttagidx_I~~\Tinstr_2^\ast~\text{)})^\ast \\ &\quad + (\text{(}~\text{catch\_all}~~\Tinstr_3^\ast~\text{)})^?~\text{)} + \quad\equiv \\ &\qquad + \text{try}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast + &\hspace{-5ex} (\text{catch}~~x{:}\Ttagidx_I~~\Tinstr_2^\ast)^\ast~~(\text{catch\_all}~~\Tinstr_3^\ast)^?~~\text{end} \\ & + \text{(}~\text{try}~~\Tlabel~~\Tblocktype + &\hspace{-15ex} \text{(}~\text{delegate}~~l{:}\Tlabelidx~~\Tinstr^\ast~~\text{)}~\text{)} + \quad\equiv \\ &\qquad + \text{try}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast &\hspace{-5ex} \text{delegate}~~l{:}\Tlabelidx \\ \end{array} + .. note:: For example, the instruction sequence From 7e680703c262b0fbd98d2688a1e34c9a4823ed2c Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Thu, 11 Aug 2022 12:31:19 +0200 Subject: [PATCH 06/13] Added forgotten fix by Andreas Rossberg. Review comment was overlooked: https://github.com/WebAssembly/exception-handling/pull/180/files/4bd749a8895434c14b3bf3dda23463e3962192c4#r820732541 --- document/core/appendix/algorithm.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index 9e8dfacb..d03882b9 100644 --- a/document/core/appendix/algorithm.rst +++ b/document/core/appendix/algorithm.rst @@ -217,8 +217,8 @@ Other instructions are checked in a similar manner. case (catch) let frame = pop_ctrl() error_if(frame.opcode =/= try || frame.opcode =/= catch) - let tagparams = tags[x].type.params - push_ctrl(catch, tagparams , frame.end_types) + let params = tags[x].type.params + push_ctrl(catch, params , frame.end_types) case (catch_all) let frame = pop_ctrl() From d6664e39152cde641c22c620e313bdc9c80e0a50 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Wed, 24 Aug 2022 19:03:29 +0200 Subject: [PATCH 07/13] Update document/core/util/macros.def Co-authored-by: Heejin Ahn --- document/core/util/macros.def | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 032b7128..21e1f72b 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -909,11 +909,11 @@ .. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}} .. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}} .. |CREFS| mathdef:: \xref{valid/conventions}{context}{\K{refs}} -.. |LCATCH| mathdef:: \xref{valid/conventions}{valid-labeltype}{\mathrel{\K{catch}}} +.. |LCATCH| mathdef:: \xref{valid/conventions}{context}{\mathrel{\K{catch}}} .. Contexts, non-terminals -.. |labeltype| mathdef:: \xref{valid/conventions}{valid-labeltype}{\mathrel{\X{labeltype}}} +.. |labeltype| mathdef:: \xref{valid/conventions}{context}{\mathrel{\X{labeltype}}} .. Judgments From 1e71e0d9097e378665def2e34805f8d2f5de49c5 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Wed, 24 Aug 2022 19:04:50 +0200 Subject: [PATCH 08/13] Update document/core/text/instructions.rst Co-authored-by: Heejin Ahn --- document/core/text/instructions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 40c79249..edfd2b61 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -941,8 +941,8 @@ Such a folded instruction can appear anywhere a regular instruction can. \quad\equiv \\ &\qquad \text{try}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast &\hspace{-5ex} (\text{catch}~~x{:}\Ttagidx_I~~\Tinstr_2^\ast)^\ast~~(\text{catch\_all}~~\Tinstr_3^\ast)^?~~\text{end} \\ & - \text{(}~\text{try}~~\Tlabel~~\Tblocktype - &\hspace{-15ex} \text{(}~\text{delegate}~~l{:}\Tlabelidx~~\Tinstr^\ast~~\text{)}~\text{)} ++ \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do} &\hspace{-8ex} \Tinstr^\ast~\text{)}~~ ++ \text{(}~\text{delegate}~~l{:}\Tlabelidx~~\text{)} \quad\equiv \\ &\qquad \text{try}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast &\hspace{-5ex} \text{delegate}~~l{:}\Tlabelidx \\ \end{array} From 56c2506862b41019061be6b9dd37b7bc087bed15 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 24 Aug 2022 19:08:35 +0200 Subject: [PATCH 09/13] Addressed two forgotten review comments. In particular: - https://github.com/WebAssembly/exception-handling/pull/180#discussion_r947302113 - https://github.com/WebAssembly/exception-handling/pull/180#discussion_r947346009 --- document/core/exec/runtime.rst | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 44537db0..140797ac 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -683,7 +683,7 @@ In order to be able to break jumping over exception handlers and caught exceptio .. math:: \begin{array}{llll} - \production{(block contexts)} & \XC^{k} &::=& \handler~\XB^k~\END \\ + \production{(control contexts)} & \XC^{k} &::=& \handler~\XB^k~\END \\ & & | & \CAUGHTadm~\{\tagaddr~\val^\ast\}~\XB^k~\END \\ \production{(block contexts)} & \XB^0 &::=& \dots ~|~ \val^\ast~\XC^0~\instr^\ast\\ \production{(block contexts)} & \XB^{k+1} &::=& \dots ~|~ \val^\ast~\XC^{k+1}~\instr^\ast \\ @@ -726,7 +726,8 @@ Throw contexts allow matching the program context around a throw instruction up Contrary to block contexts, throw contexts don't skip over handlers. Since handlers are not included above, there is always a unique maximal throw context to match the reduction rules. - This basically means that :math:`\CAUGHTadm {\dots} instr^\ast \END` is not a potential catching block for exceptions thrown by :math:`\instr^\ast`, since these are instructions in the scope of a |CATCH| or a |CATCHALL|. + + CAUGHTadm blocks do not represent active handlers. Instead, they delimit the continuation of a handler that has already been selected. Their sole purpose is to record the exception that has been caught, such that |RETHROW| can access it inside such a block. .. note:: For example, catching a simple :ref:`throw ` in a :ref:`try block ` would be as follows. From e9de07d136ccd87541d25b4999a13578e4203ef1 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 24 Aug 2022 19:26:59 +0200 Subject: [PATCH 10/13] Addressed currently last review comment and added |-markers forgotten in the previous commit. This comment: https://github.com/WebAssembly/exception-handling/pull/180#discussion_r947573133 --- document/core/exec/runtime.rst | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 140797ac..6e5155e7 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -727,7 +727,7 @@ Throw contexts allow matching the program context around a throw instruction up Since handlers are not included above, there is always a unique maximal throw context to match the reduction rules. - CAUGHTadm blocks do not represent active handlers. Instead, they delimit the continuation of a handler that has already been selected. Their sole purpose is to record the exception that has been caught, such that |RETHROW| can access it inside such a block. + |CAUGHTadm| blocks do not represent active handlers. Instead, they delimit the continuation of a handler that has already been selected. Their sole purpose is to record the exception that has been caught, such that |RETHROW| can access it inside such a block. .. note:: For example, catching a simple :ref:`throw ` in a :ref:`try block ` would be as follows. @@ -751,10 +751,12 @@ Throw contexts allow matching the program context around a throw instruction up \stepto & \val^m & \\ \end{array} - When a throw occurs, we pop the values :math:`val^m:[t^m]` and append them to the tag address :math:`a` into - a |CAUGHTadm| instruction. We then search for the maximal surrounding throw context `T`, which means we pop - any other values, labels, frames, and |CAUGHTadm| instructions, until we find an exception handler - (corresponding to a try block) that :ref:`handles the exception `. + + + When a throw of the form :math:`val^m (throw a)` occurs, we search for the maximal surrounding throw context :math:`T`, + which means we pop any other values, labels, frames, and |CAUGHTadm| instructions surrounding the throw :math:`val^m (throw a)`, + until we find an exception handler (corresponding to a try block) that :ref:`handles the exception `. + We then append the values :math:`val^m:[t^m]` to the tag address :math:`a` into a new |CAUGHTadm| instruction which we push on the stack. In other words, when a throw occurs, normal execution halts and exceptional execution begins, until the throw is the continuation (i.e., in the place of a :math:`\_`) of a throw context in a catching try block. From 53e4e33427e2c8ee3cc07e2734761d03a865d954 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 24 Aug 2022 20:13:45 +0200 Subject: [PATCH 11/13] Fixed stray + signs that were breaking the build, added missing `)`. --- document/core/text/instructions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index edfd2b61..7193acac 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -941,8 +941,8 @@ Such a folded instruction can appear anywhere a regular instruction can. \quad\equiv \\ &\qquad \text{try}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast &\hspace{-5ex} (\text{catch}~~x{:}\Ttagidx_I~~\Tinstr_2^\ast)^\ast~~(\text{catch\_all}~~\Tinstr_3^\ast)^?~~\text{end} \\ & -+ \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do} &\hspace{-8ex} \Tinstr^\ast~\text{)}~~ -+ \text{(}~\text{delegate}~~l{:}\Tlabelidx~~\text{)} + \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do} &\hspace{-8ex} \Tinstr^\ast~\text{)}~~ + \text{(}~\text{delegate}~~l{:}\Tlabelidx~~\text{)}~\text{)} \quad\equiv \\ &\qquad \text{try}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast &\hspace{-5ex} \text{delegate}~~l{:}\Tlabelidx \\ \end{array} From 4d30c9b810f0a107cf21fb9774e388cc0b6c9fd7 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Fri, 26 Aug 2022 11:21:55 +0200 Subject: [PATCH 12/13] Apply suggestions from code review Co-authored-by: Heejin Ahn --- document/core/exec/runtime.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 6e5155e7..6406d333 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -741,7 +741,7 @@ Throw contexts allow matching the program context around a throw instruction up \stepto & S;~F;~\LABEL_m\{\} (\CATCHadm\{a~\RETURN\}~\val^n~(\THROW~x)~\END)~\END \\ \end{array} - Denote :math:`\val^n = \val^{n-m} val^m`. + Denote :math:`\val^n = \val^{n-m} \val^m`. :ref:`Handling the thrown exception ` with tag address :math:`a` in the throw context :math:`T=[val^{n-m}\_]`, with the exception handler :math:`H=\CATCHadm\{a~\RETURN\}` gives: @@ -753,8 +753,8 @@ Throw contexts allow matching the program context around a throw instruction up - When a throw of the form :math:`val^m (throw a)` occurs, we search for the maximal surrounding throw context :math:`T`, - which means we pop any other values, labels, frames, and |CAUGHTadm| instructions surrounding the throw :math:`val^m (throw a)`, + When a throw of the form :math:`val^m (\THROWadm~a)` occurs, we search for the maximal surrounding throw context :math:`T`, + which means we pop any other values, labels, frames, and |CAUGHTadm| instructions surrounding the throw :math:`val^m (\THROWadm~a)`, until we find an exception handler (corresponding to a try block) that :ref:`handles the exception `. We then append the values :math:`val^m:[t^m]` to the tag address :math:`a` into a new |CAUGHTadm| instruction which we push on the stack. From 86126aedb507aed0cf75894cc451381d2ca8e97b Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 26 Aug 2022 11:28:23 +0200 Subject: [PATCH 13/13] Addressed latest two review comments. --- document/core/exec/runtime.rst | 2 +- document/core/util/macros.def | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 6406d333..d3df56ae 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -741,7 +741,7 @@ Throw contexts allow matching the program context around a throw instruction up \stepto & S;~F;~\LABEL_m\{\} (\CATCHadm\{a~\RETURN\}~\val^n~(\THROW~x)~\END)~\END \\ \end{array} - Denote :math:`\val^n = \val^{n-m} \val^m`. + We denote :math:`\val^n = \val^{n-m} \val^m`. :ref:`Handling the thrown exception ` with tag address :math:`a` in the throw context :math:`T=[val^{n-m}\_]`, with the exception handler :math:`H=\CATCHadm\{a~\RETURN\}` gives: diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 21e1f72b..22383051 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -909,11 +909,11 @@ .. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}} .. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}} .. |CREFS| mathdef:: \xref{valid/conventions}{context}{\K{refs}} -.. |LCATCH| mathdef:: \xref{valid/conventions}{context}{\mathrel{\K{catch}}} +.. |LCATCH| mathdef:: \xref{valid/conventions}{context}{\K{catch}} .. Contexts, non-terminals -.. |labeltype| mathdef:: \xref{valid/conventions}{context}{\mathrel{\X{labeltype}}} +.. |labeltype| mathdef:: \xref{valid/conventions}{context}{\X{labeltype}} .. Judgments