diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst index ef862d80f2..a647295698 100644 --- a/document/core/appendix/index-rules.rst +++ b/document/core/appendix/index-rules.rst @@ -44,6 +44,9 @@ Typing of Runtime Constructs =============================================== =============================================================================== Construct Judgement =============================================== =============================================================================== +:ref:`Value ` :math:`\vdashval \val : \valtype` +:ref:`Result ` :math:`\vdashresult \result : \resulttype` +:ref:`External value ` :math:`S \vdashexternval \externval : \externtype` :ref:`Module instruction ` :math:`S \vdashmoduleinstr \moduleinstr \ok` :ref:`Function instance ` :math:`S \vdashfuncinst \funcinst : \resulttype` :ref:`Table instance ` :math:`S \vdashtableinst \tableinst : \tabletype` @@ -55,8 +58,6 @@ Construct Judgement :ref:`Configuration ` :math:`\vdashconfig \config \ok` :ref:`Thread ` :math:`S;\resulttype^? \vdashthread \thread : \resulttype^?` :ref:`Frame ` :math:`S \vdashframe \frame : C` -:ref:`Value ` :math:`\vdashval \val : \valtype` -:ref:`External value ` :math:`S \vdashexternval \externval : \externtype` =============================================== =============================================================================== diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 2473df9d0c..2ade29dfad 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -20,6 +20,58 @@ The typing rules defining WebAssembly :ref:`validation ` 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 `, that is, the :ref:`store `, :ref:`configurations `, and :ref:`administrative instructions ` as well as :ref:`module instructions `. [#pldi2017]_ +.. index:: value, value type, result, result type, trap +.. _valid-val: +.. _valid-result: + +Values and Results +~~~~~~~~~~~~~~~~~~ + +:ref:`Values ` and :ref:`results ` can be classified by :ref:`value types ` and :ref:`result types ` as follows. + +:ref:`Values ` :math:`t.\CONST~c` +............................................. + +* The value is valid with :ref:`value type ` :math:`t`. + +.. math:: + \frac{ + }{ + \vdashval t.\CONST~c : t + } + + +:ref:`Results ` :math:`\val^\ast` +................................................ + +* For each :ref:`value ` :math:`\val_i` in :math:`\val^\ast`: + + * The value :math:`\val_i` is :ref:`valid ` with some :ref:`value type ` :math:`t_i`. + +* Let :math:`t^\ast` be the concatenation of all :math:`t_i`. + +* Then the result is valid with :ref:`result type ` :math:`[t^\ast]`. + +.. math:: + \frac{ + (\vdashval \val : t)^\ast + }{ + \vdashresult \val^\ast : [t^\ast] + } + + +:ref:`Results ` :math:`\TRAP` +............................................ + +* The result is valid with :ref:`result type ` :math:`[t^\ast]`, for any sequence :math:`t^\ast` of :ref:`value types `. + +.. math:: + \frac{ + }{ + \vdashresult \TRAP : [t^\ast] + } + + .. _module-context: .. _valid-store: @@ -76,8 +128,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co .. index:: function type, function instance .. _valid-funcinst: -:ref:`Function Instance ` :math:`\{\FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func\}` -...................................................................................................................... +:ref:`Function Instances ` :math:`\{\FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func\}` +....................................................................................................................... * The :ref:`function type ` :math:`\functype` must be :ref:`valid `. @@ -99,11 +151,59 @@ Module instances are classified by *module contexts*, which are regular :ref:`co } +.. index:: function type, function instance, host function +.. _valid-hostfuncinst: + +:ref:`Host Function Instances ` :math:`\{\FITYPE~\functype, \FIHOSTCODE~\X{hf}\}` +.................................................................................................. + +* The :ref:`function type ` :math:`\functype` must be :ref:`valid `. + +* Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type ` :math:`\functype`. + +* For every possible :ref:`valid ` :ref:`store ` :math:`S_1` :ref:`extending ` :math:`S` and every sequence :math:`\val^\ast` of :ref:`values ` whose :ref:`types ` coincide with :math:`t_1^\ast`: + + * There must exist a :ref:`valid ` :ref:`store ` :math:`S_2` :ref:`extending ` :math:`S_1` and a :ref:`result ` :math:`\result` whose :ref:`type ` coincides with :math:`[t_2^\ast]` such that: + + * :ref:`Executing ` :math:`\X{hf}` in store :math:`S_1` with arguments :math:`\val^\ast` produces :math:`\result` and store :math:`S_2`. + +* Then the function instance is valid with :ref:`function type ` :math:`\functype`. + +.. math:: + \frac{ + \begin{array}[b]{@{}l@{}} + \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok \\ + \end{array} + \quad + \begin{array}[b]{@{}l@{}} + \forall S_1, \val^\ast,~ + {\vdashstore S_1 \ok} \wedge + {\vdashstoreextends S \extendsto S_1} \wedge + {\vdashresult \val^\ast : [t_1^\ast]} + \Longrightarrow {} \\ \qquad + \exists S_2, \result,~ + {\vdashstore S_2 \ok} \wedge + {\vdashstoreextends S_1 \extendsto S_2} \wedge + {\vdashresult \result : [t_2^\ast]} \wedge + \X{hf}(S_1; \val^\ast) = S_2; \result + \end{array} + }{ + S \vdashfuncinst \{\FITYPE~[t_1^\ast] \to [t_2^\ast], \FIHOSTCODE~\X{hf}\} : [t_1^\ast] \to [t_2^\ast] + } + +.. note:: + This rule states that, if appropriate pre-conditions about store and arguments are satisfied, then executing the host function must satisfy appropriate post-conditions about store and results. + The post-conditions match the ones in the :ref:`execution rule ` for invoking host functions. + + Any store under which the function is invoked is assumed to be an extension of the current store. + That way, the function itself is able to make sufficient assumptions about future stores. + + .. index:: table type, table instance, limits, function address .. _valid-tableinst: -:ref:`Table Instance ` :math:`\{ \TIELEM~(\X{fa}^?)^n, \TIMAX~m^? \}` -............................................................................................. +:ref:`Table Instances ` :math:`\{ \TIELEM~(\X{fa}^?)^n, \TIMAX~m^? \}` +.............................................................................................. * For each optional :ref:`function address ` :math:`\X{fa}^?_i` in the table elements :math:`(\X{fa}^?)^n`: @@ -128,8 +228,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co .. index:: memory type, memory instance, limits, byte .. _valid-meminst: -:ref:`Memory Instance ` :math:`\{ \MIDATA~b^n, \MIMAX~m^? \}` -............................................................................. +:ref:`Memory Instances ` :math:`\{ \MIDATA~b^n, \MIMAX~m^? \}` +.............................................................................. * The :ref:`limits ` :math:`\{\LMIN~n, \LMAX~m^?\}` must be :ref:`valid `. @@ -146,8 +246,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co .. index:: global type, global instance, value, mutability .. _valid-globalinst: -:ref:`Global Instance ` :math:`\{ \GIVALUE~(t.\CONST~c), \GIMUT~\mut \}` -........................................................................................... +:ref:`Global Instances ` :math:`\{ \GIVALUE~(t.\CONST~c), \GIMUT~\mut \}` +............................................................................................ * The global instance is valid with :ref:`global type ` :math:`\mut~t`. @@ -161,8 +261,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co .. index:: external type, export instance, name, external value .. _valid-exportinst: -:ref:`Export Instance ` :math:`\{ \EINAME~\name, \EIVALUE~\externval \}` -...................................................................................................... +:ref:`Export Instances ` :math:`\{ \EINAME~\name, \EIVALUE~\externval \}` +....................................................................................................... * The :ref:`external value ` :math:`\externval` must be :ref:`valid ` with some :ref:`external type ` :math:`\externtype`. @@ -179,8 +279,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co .. index:: module instance, context .. _valid-moduleinst: -:ref:`Module Instance ` :math:`\moduleinst` -.............................................................. +:ref:`Module Instances ` :math:`\moduleinst` +............................................................... * Each :ref:`function type ` :math:`\functype_i` in :math:`\moduleinst.\MITYPES` must be :ref:`valid `. @@ -254,7 +354,7 @@ Configuration Validity To relate the WebAssembly :ref:`type system ` to its :ref:`execution semantics `, the :ref:`typing rules for instructions ` must be extended to :ref:`configurations ` :math:`S;T`, which relates the :ref:`store ` to execution :ref:`threads `. -Threads may either be regular threads executing sequences of :ref:`instructions `, or module threads executing :ref:`module instructions ` that represent an ongoing module instantiation. +Threads may either be regular threads executing sequences of :ref:`instructions `, or module threads executing :ref:`module instructions ` that represent an ongoing module instantiation. Regular threads are classified by their :ref:`result type `. Module threads on the other hand have no result, not even an empty one. Consequently, threads and configurations are cumutavily classified by an *optional* result type, where :math:`\epsilon` classifies the thread as a module computation. @@ -339,7 +439,7 @@ Finally, :ref:`frames ` are classified with *frame contexts*, whic :ref:`Frames ` :math:`\{\ALOCALS~\val^\ast, \AMODULE~\moduleinst\}` ................................................................................. -* The :ref:`module instance ` :math:`\moduleinst` must be :ref:`valid ` with some :ref:`module context ` :math:`C`. +* The :ref:`module instance ` :math:`\moduleinst` must be :ref:`valid ` with some :ref:`module context ` :math:`C`. * Each :ref:`value ` :math:`\val_i` in :math:`\val^\ast` must be :ref:`valid ` with some :ref:`value type ` :math:`t_i`. @@ -359,21 +459,6 @@ Finally, :ref:`frames ` are classified with *frame contexts*, whic } -.. index:: value, value type -.. _valid-val: - -:ref:`Values ` :math:`t.\CONST~c` -............................................. - -* The value is valid with :ref:`value type ` :math:`t`. - -.. math:: - \frac{ - }{ - \vdashval t.\CONST~c : t - } - - .. index:: administrative instruction, value type, context, store .. _valid-instr-admin: @@ -381,7 +466,7 @@ Administrative Instructions ~~~~~~~~~~~~~~~~~~~~~~~~~~~ Typing rules for :ref:`administrative instructions ` are specified as follows. -In addition to the :ref:`context ` :math:`C`, typing of these instructions is defined under a given :ref:`store ` :math:`S`. +In addition to the :ref:`context ` :math:`C`, typing of these instructions is defined under a given :ref:`store ` :math:`S`. To that end, all previous typing judgements :math:`C \vdash \X{prop}` are generalized to include the store, as in :math:`S; C \vdash \X{prop}`, by implicitly adding :math:`S` to all rules -- :math:`S` is never modified by the pre-existing rules, but it is accessed in the new rules for :ref:`administrative instructions ` and :ref:`module instructions ` given below. diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 7f33fc9624..4ae83dc5d6 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1095,31 +1095,24 @@ Furthermore, the resulting store must be :ref:`valid `, i.e., all d ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; \val_1^n~(\INVOKE~a) &\stepto& S'; \val_2^m + S; \val^n~(\INVOKE~a) &\stepto& S'; \result \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\mbox{if} & S.\SFUNCS[a] = \{ \FITYPE~[t_1^n] \to [t_2^m], \FIHOSTCODE~\dots \} \\ - \wedge & \val_1^n = (t_1.\CONST~c_1)^n \\ - \wedge & \val_2^m = (t_2.\CONST~c_2)^m \\ - \wedge & \vdashstoreextends S \extendsto S' \\ - \wedge & \vdashstore S' \ok) \\ - \end{array} - \\[1ex] - \begin{array}{lcl@{\qquad}l} - S; \val^n~(\INVOKE~a) &\stepto& S'; \TRAP - \end{array} - \\ \qquad - \begin{array}[t]{@{}r@{~}l@{}} - (\mbox{if} & S.\SFUNCS[a] = \{ \FITYPE~\X{ft}, \FIHOSTCODE~\dots \} \\ - \wedge & \vdashstoreextends S \extendsto S' \\ - \wedge & \vdashstore S' \ok) \\ + (\mbox{if} & S.\SFUNCS[a] = \{ \FITYPE~[t_1^n] \to [t_2^m], \FIHOSTCODE~\X{hf} \} \\ + \wedge & \X{hf}(S; \val^n) = S'; \result) \\ \end{array} \\ \end{array} -Here, :math:`S \extendsto S'` expresses that the new store :math:`S'` is an :ref:`extension ` of :math:`S`. -Moreover, :math:`\vdashstore S' \ok` restricts :math:`S'` to be a :ref:`valid ` store. -Both notions are defined in the :ref:`Appendix `. +Here, :math:`\X{hf}(S; \val^n)` denotes the implementation-defined execution of host function :math:`\X{hf}` in current store :math:`S` with arguments :math:`\val^n`. +The outcome is a pair of a modified store :math:`S'` and a :ref:`result `. + +For a WebAssembly implementation to be :ref:`sound ` in the presence of host functions, +every :ref:`host function instance ` must be :ref:`valid `, +which means that it adheres to suitable pre- and post-conditions: +under a :ref:`valid store ` :math:`S`, and given arguments :math:`\val^n` matching the ascribed parameter types :math:`t_1^n`, +executing the host function must produce a valid store :math:`S'` that is an :ref:`extension ` of :math:`S` and a result matching the ascribed return types :math:`t_2^m`. +All these notions are made precise in the :ref:`Appendix `. .. note:: A host function can call back into WebAssembly by :ref:`invoking ` a function :ref:`exported ` from a :ref:`module `. diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 3548a4dd18..6a3dc2b464 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -729,8 +729,8 @@ The values :math:`\val_{\F{res}}^m` are returned as the results of the invocatio .. math:: ~\\[-1ex] \begin{array}{@{}lcl} - \invoke(S, \funcaddr, \val^n) &=& \val_{\F{res}}^m / \TRAP \\ + \invoke(S, \funcaddr, \val^n) &=& \result \\ &(\iff & S.\SFUNCS[\funcaddr].\FITYPE = [t_1^n] \to [t_2^m] \\ &\wedge& \val^n = (t_1.\CONST~c)^n \\ - &\wedge& S; \val^n~(\INVOKE~\funcaddr) \stepto^\ast S'; \val_{\F{res}}^m / \TRAP) \\ + &\wedge& S; \val^n~(\INVOKE~\funcaddr) \stepto^\ast S'; \result) \\ \end{array} diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 5d81db128c..03a1de0be2 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -30,6 +30,27 @@ It is convenient to reuse the same notation as for the |CONST| :ref:`instruction \end{array} +.. index:: ! result, value, trap + pair: abstract syntax; result +.. _syntax-result: + +Results +~~~~~~~ + +A *result* is the outcome of a computation. +It is either a sequence of :ref:`values ` or a :ref:`trap `. + +.. math:: + \begin{array}{llcl} + \production{(result)} & \result &::=& + \val^\ast \\&&|& + \TRAP + \end{array} + +.. note:: + In the current version of WebAssembly, a result can consist of at most one value. + + .. index:: ! store, function instance, table instance, memory instance, global instance, module, allocation pair: abstract syntax; store .. _syntax-store: @@ -171,7 +192,8 @@ The module instance is used to resolve references to other definitions during ex A *host function* is a function expressed outside WebAssembly but passed to a :ref:`module ` as an :ref:`import `. The definition and behavior of host functions are outside the scope of this specification. For the purpose of this specification, it is assumed that when :ref:`invoked `, -a host function behaves non-deterministically. +a host function behaves non-deterministically, +but within certain :ref:`constraints ` that ensure the integrity of the runtime. .. note:: Function instances are immutable, and their identity is not observable by WebAssembly code. diff --git a/document/core/util/math.def b/document/core/util/math.def index ed2d48ff03..3002aa6460 100644 --- a/document/core/util/math.def +++ b/document/core/util/math.def @@ -819,9 +819,13 @@ .. |DO| mathdef:: \xref{exec/runtime}{syntax-do}{\K{do}} -.. Values & Administrative Instructions, non-terminals +.. Values & Results, non-terminals .. |val| mathdef:: \xref{exec/runtime}{syntax-val}{\X{val}} +.. |result| mathdef:: \xref{exec/runtime}{syntax-result}{\X{result}} + + +.. Administrative Instructions, non-terminals .. |moduleinstr| mathdef:: \xref{exec/runtime}{syntax-moduleinstr}{\X{moduleinstr}} @@ -938,6 +942,9 @@ .. |vdashadmininstr| mathdef:: \xref{appendix/properties}{valid-instr-admin}{\vdash} .. |vdashmoduleinstr| mathdef:: \xref{appendix/properties}{valid-moduleinstr}{\vdash} +.. |vdashval| mathdef:: \xref{appendix/properties}{valid-val}{\vdash} +.. |vdashresult| mathdef:: \xref{appendix/properties}{valid-result}{\vdash} + .. |vdashfuncinst| mathdef:: \xref{appendix/properties}{valid-funcinst}{\vdash} .. |vdashtableinst| mathdef:: \xref{appendix/properties}{valid-tableinst}{\vdash} .. |vdashmeminst| mathdef:: \xref{appendix/properties}{valid-meminst}{\vdash} @@ -949,7 +956,6 @@ .. |vdashconfig| mathdef:: \xref{appendix/properties}{valid-config}{\vdash} .. |vdashthread| mathdef:: \xref{appendix/properties}{valid-thread}{\vdash} .. |vdashframe| mathdef:: \xref{appendix/properties}{valid-frame}{\vdash} -.. |vdashval| mathdef:: \xref{appendix/properties}{valid-val}{\vdash} .. |vdashfuncinstextends| mathdef:: \xref{appendix/properties}{extend-funcinst}{\vdash} .. |vdashtableinstextends| mathdef:: \xref{appendix/properties}{extend-tableinst}{\vdash}