Add uncaught exceptions to the core formal spec. (#238)

I found several places that needed change by grepping for 'trap'.

Also applied suggestions from code review

Co-authored-by: Andreas Rossberg <[email protected]>

Author: ioannad

document/core/appendix/properties.rst

@@ -7,7 +7,7 @@ Soundness
 The :ref:`type system <type-system>` of WebAssembly is *sound*, implying both *type safety* and *memory safety* with respect to the WebAssembly semantics. For example:
 
 * All types declared and derived during validation are respected at run time;
-  e.g., every :ref:`local <syntax-local>` or :ref:`global <syntax-global>` variable will only contain type-correct values, every :ref:`instruction <syntax-instr>` will only be applied to operands of the expected type, and every :ref:`function <syntax-func>` :ref:`invocation <exec-invocation>` always evaluates to a result of the right type (if it does not :ref:`trap <trap>` or diverge).
+  e.g., every :ref:`local <syntax-local>` or :ref:`global <syntax-global>` variable will only contain type-correct values, every :ref:`instruction <syntax-instr>` will only be applied to operands of the expected type, and every :ref:`function <syntax-func>` :ref:`invocation <exec-invocation>` always evaluates to a result of the right type (if it does not :ref:`trap <trap>`, throw an exception, or diverge).
 
 * No memory location will be read or written except those explicitly defined by the program, i.e., as a :ref:`local <syntax-local>`, a :ref:`global <syntax-global>`, an element in a :ref:`table <syntax-table>`, or a location within a linear :ref:`memory <syntax-mem>`.
 
@@ -20,7 +20,7 @@ The typing rules defining WebAssembly :ref:`validation <valid>` only cover the *
 In order to state and prove soundness precisely, the typing rules must be extended to the *dynamic* components of the abstract :ref:`runtime <syntax-runtime>`, that is, the :ref:`store <syntax-store>`, :ref:`configurations <syntax-config>`, and :ref:`administrative instructions <syntax-instr-admin>`. [#cite-pldi2017]_
 
 
-.. index:: value, value type, result, result type, trap
+.. index:: value, value type, result, result type, trap, exception, throw
 .. _valid-result:
 
 Results
@@ -58,6 +58,9 @@ Results
      S \vdashresult \TRAP : [t^\ast]
    }
 
+.. todo::
+   Add validation for exception results.
+
 
 .. _module-context:
 .. _valid-store:
@@ -979,7 +982,7 @@ If a :ref:`configuration <syntax-config>` :math:`S;T` is :ref:`valid <valid-conf
 then it either diverges or takes a finite number of steps to reach a terminal configuration :math:`S';T'` (i.e., :math:`S;T \stepto^\ast S';T'`) that is valid with the same result type (i.e., :math:`\vdashconfig S';T' : [t^\ast]`)
 and where :math:`S'` is an :ref:`extension <extend-store>` of :math:`S` (i.e., :math:`\vdashstoreextends S \extendsto S'`).
 
-In other words, every thread in a valid configuration either runs forever, traps, or terminates with a result that has the expected type.
+In other words, every thread in a valid configuration either runs forever, traps, throws an exception, or terminates with a result that has the expected type.
 Consequently, given a :ref:`valid store <valid-store>`, no computation defined by :ref:`instantiation <exec-instantiation>` or :ref:`invocation <exec-invocation>` of a valid module can "crash" or otherwise (mis)behave in ways not covered by the :ref:`execution <exec>` semantics given in this specification.
 
 

document/core/exec/conventions.rst

@@ -49,7 +49,7 @@ The following conventions are adopted in stating these rules.
 
 * Execution can *enter* and *exit* :ref:`instruction sequences <syntax-instr-seq>` that form :ref:`blocks <syntax-instr-control>`.
 
-* :ref:`Instruction sequences <syntax-instr-seq>` are implicitly executed in order, unless a trap or jump occurs.
+* :ref:`Instruction sequences <syntax-instr-seq>` are implicitly executed in order, unless a trap or jump occurs, or an exception is thrown.
 
 * In various places the rules contain *assertions* expressing crucial invariants about the program state.
 
@@ -105,7 +105,7 @@ The order of reduction is determined by the definition of an appropriate :ref:`e
 
 Reduction *terminates* when no more reduction rules are applicable.
 :ref:`Soundness <soundness>` of the WebAssembly :ref:`type system <type-system>` guarantees that this is only the case when the original instruction sequence has either been reduced to a sequence of |CONST| instructions, which can be interpreted as the :ref:`values <syntax-val>` of the resulting operand stack,
-or if a :ref:`trap <syntax-trap>` occurred.
+or if a :ref:`trap <syntax-trap>` or an uncaught exception occurred.
 
 .. note::
    For example, the following instruction sequence,

document/core/exec/instructions.rst

@@ -3171,7 +3171,7 @@ Host Functions
 ..............
 
 Invoking a :ref:`host function <syntax-hostfunc>` has non-deterministic behavior.
-It may either terminate with a :ref:`trap <trap>` or return regularly.
+It may either terminate with a :ref:`trap <trap>`, an exception, or return regularly.
 However, in the latter case, it must consume and produce the right number and types of WebAssembly :ref:`values <syntax-val>` on the stack,
 according to its :ref:`function type <syntax-functype>`.
 

document/core/exec/modules.rst

@@ -648,7 +648,7 @@ Moreover, if the dots :math:`\dots` are a sequence :math:`A^n` (as for globals o
    In an implementation, this recursion is easily unraveled by mutating one or the other in a secondary step.
 
 
-.. index:: ! instantiation, module, instance, store, trap
+.. index:: ! instantiation, module, instance, store, trap, exception
 .. _exec-module:
 .. _exec-instantiation:
 
@@ -659,7 +659,7 @@ Given a :ref:`store <syntax-store>` :math:`S`, a :ref:`module <syntax-module>` :
 
 Instantiation checks that the module is :ref:`valid <valid>` and the provided imports :ref:`match <match-externtype>` the declared types,
 and may *fail* with an error otherwise.
-Instantiation can also result in a :ref:`trap <trap>` from executing the start function.
+Instantiation can also result in a :ref:`trap <trap>` or an exception from executing the start function.
 It is up to the :ref:`embedder <embedder>` to define how such conditions are reported.
 
 1. If :math:`\module` is not :ref:`valid <valid-module>`, then:
@@ -816,7 +816,7 @@ where:
    :ref:`Evaluation <exec-expr>` of :ref:`constant expressions <valid-constant>` does not affect the store.
 
 
-.. index:: ! invocation, module, module instance, function, export, function address, function instance, function type, value, stack, trap, store
+.. index:: ! invocation, module, module instance, function, export, function address, function instance, function type, value, stack, trap, exception, store
 .. _exec-invocation:
 
 Invocation
@@ -825,11 +825,11 @@ Invocation
 Once a :ref:`module <syntax-module>` has been :ref:`instantiated <exec-instantiation>`, any exported function can be *invoked* externally via its :ref:`function address <syntax-funcaddr>` :math:`\funcaddr` in the :ref:`store <syntax-store>` :math:`S` and an appropriate list :math:`\val^\ast` of argument :ref:`values <syntax-val>`.
 
 Invocation may *fail* with an error if the arguments do not fit the :ref:`function type <syntax-functype>`.
-Invocation can also result in a :ref:`trap <trap>`.
+Invocation can also result in a :ref:`trap <trap>` or an exception.
 It is up to the :ref:`embedder <embedder>` to define how such conditions are reported.
 
 .. note::
-   If the :ref:`embedder <embedder>` API performs type checks itself, either statically or dynamically, before performing an invocation, then no failure other than traps can occur.
+   If the :ref:`embedder <embedder>` API performs type checks itself, either statically or dynamically, before performing an invocation, then no failure other than traps or exceptions can occur.
 
 The following steps are performed:
 

document/core/exec/runtime.rst

@@ -66,26 +66,24 @@ Convention
 * The meta variable :math:`r` ranges over reference values where clear from context.
 
 
-.. index:: ! result, value, trap
+.. index:: ! result, value, trap, exception
    pair: abstract syntax; result
 .. _syntax-result:
 
 Results
 ~~~~~~~
 
 A *result* is the outcome of a computation.
-It is either a sequence of :ref:`values <syntax-val>` or a :ref:`trap <syntax-trap>`.
+It is either a sequence of :ref:`values <syntax-val>`, a :ref:`trap <syntax-trap>`, or an uncaught exception wrapped in its throw context.
 
 .. math::
    \begin{array}{llcl}
    \production{(result)} & \result &::=&
      \val^\ast \\&&|&
-     \TRAP
+     \TRAP  \\&&|&
+     \XT[\val^\ast~(\THROWadm~\tagaddr)]
    \end{array}
 
-.. todo::
-   Add a result value for an unhandled exception.
-
 .. note::
    In the current version of WebAssembly, a result can consist of at most one value.
 
@@ -714,13 +712,14 @@ the following syntax of *throw contexts* is defined, as well as associated struc
 .. math::
    \begin{array}{llll}
    \production{(throw contexts)} & \XT &::=&
-     \val^\ast~[\_]~\instr^\ast \\ &&|&
+     [\_] | \val^\ast~\XT~\instr^\ast \\ &&|&
      \LABEL_n\{\instr^\ast\}~\XT~\END \\ &&|&
      \CAUGHTadm\{\tagaddr~\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 innermost enclosing |CATCHadm| or |DELEGATEadm|, thereby selecting the exception |handler| responsible for an exception, if one exists.
+If no exception :ref:`handler that catches the exception <syntax-handler>` is found, the computation :ref:`results <syntax-result>` in an uncaught exception result value, which contains the exception's entire throw context.
 
 .. note::
    Contrary to block contexts, throw contexts don't skip over handlers.
@@ -763,8 +762,6 @@ 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.
 
 
 .. index:: ! configuration, ! thread, store, frame, instruction, module instruction
@@ -820,10 +817,7 @@ Finally, the following definition of *evaluation context* and associated structu
    \end{array}
 
 Reduction terminates when a thread's instruction sequence has been reduced to a :ref:`result <syntax-result>`,
-that is, either a sequence of :ref:`values <syntax-val>` or to a |TRAP|.
-
-.. todo::
-   Add rules to deal with unresolved :math:`\THROWadm~\tagaddr`, and extend results to include such situations.
+that is, either a sequence of :ref:`values <syntax-val>`, to an uncaught exception, or to a |TRAP|.
 
 .. note::
    The restriction on evaluation contexts rules out contexts like :math:`[\_]` and :math:`\epsilon~[\_]~\epsilon` for which :math:`E[\TRAP] = \TRAP`.