Skip to content

Latest commit

 

History

History
705 lines (435 loc) · 24.1 KB

embedding.rst

File metadata and controls

705 lines (435 loc) · 24.1 KB
Raw
.. index:: ! embedding, embedder, implementation, host

Embedding

A WebAssembly implementation will typically be embedded into a host environment. An embedder implements the connection between such a host environment and the WebAssembly semantics as defined in the main body of this specification. An embedder is expected to interact with the semantics in well-defined ways.

This section defines a suitable interface to the WebAssembly semantics in the form of entry points through which an embedder can access it. The interface is intended to be complete, in the sense that an embedder does not need to reference other functional parts of the WebAssembly specification directly.

Note

On the other hand, an embedder does not need to provide the host environment with access to all functionality defined in this interface. For example, an implementation may not support :ref:`parsing <embed-module-parse>` of the :ref:`text format <text>`.

Types

In the description of the embedder interface, syntactic classes from the :ref:`abstract syntax <syntax>` and the :ref:`runtime's abstract machine <syntax-runtime>` are used as names for variables that range over the possible objects from that class. Hence, these syntactic classes can also be interpreted as types.

For numeric parameters, notation like n:\u32 is used to specify a symbolic name in addition to the respective value range.

Exceptions and Errors

Invoking an exported function may throw or propagate exceptions, expressed by an auxiliary syntactic class:

\begin{array}{llll}
\production{exception} & \exception &::=& \ETHROW ~ \exnaddr \\
\end{array}

The exception address exnaddr identifies the exception thrown.

Failure of an interface operation is also indicated by an auxiliary syntactic class:

\begin{array}{llll}
\production{error} & \error &::=& \ERROR \\
\end{array}

In addition to the error conditions specified explicitly in this section, implementations may also return errors when specific :ref:`implementation limitations <impl>` are reached.

Note

Errors are abstract and unspecific with this definition. Implementations can refine it to carry suitable classifications and diagnostic messages.

Pre- and Post-Conditions

Some operations state pre-conditions about their arguments or post-conditions about their results. It is the embedder's responsibility to meet the pre-conditions. If it does, the post conditions are guaranteed by the semantics.

In addition to pre- and post-conditions explicitly stated with each operation, the specification adopts the following conventions for :ref:`runtime objects <syntax-runtime>` (\store, \moduleinst, \externval, :ref:`addresses <syntax-addr>`):

Note

As long as an embedder treats runtime objects as abstract and only creates and manipulates them through the interface defined here, all implicit pre-conditions are automatically met.

.. index:: allocation, store

Store

\F{store\_init}() : \store

  1. Return the empty :ref:`store <syntax-store>`.
\begin{array}{lclll}
\F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon, ~\STAGS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\
\end{array}

.. index:: module

Modules

.. index:: binary format

\F{module\_decode}(\byte^\ast) : \module ~|~ \error

  1. If there exists a derivation for the :ref:`byte <syntax-byte>` sequence \byte^\ast as a \Bmodule according to the :ref:`binary grammar for modules <binary-module>`, yielding a :ref:`module <syntax-module>` m, then return m.
  2. Else, return \ERROR.
\begin{array}{lclll}
\F{module\_decode}(b^\ast) &=& m && (\iff \Bmodule \stackrel\ast\Longrightarrow m{:}b^\ast) \\
\F{module\_decode}(b^\ast) &=& \ERROR && (\otherwise) \\
\end{array}

.. index:: text format

\F{module\_parse}(\char^\ast) : \module ~|~ \error

  1. If there exists a derivation for the :ref:`source <text-source>` \char^\ast as a \Tmodule according to the :ref:`text grammar for modules <text-module>`, yielding a :ref:`module <syntax-module>` m, then return m.
  2. Else, return \ERROR.
\begin{array}{lclll}
\F{module\_parse}(c^\ast) &=& m && (\iff \Tmodule \stackrel\ast\Longrightarrow m{:}c^\ast) \\
\F{module\_parse}(c^\ast) &=& \ERROR && (\otherwise) \\
\end{array}

.. index:: validation

\F{module\_validate}(\module) : \error^?

  1. If \module is :ref:`valid <valid-module>`, then return nothing.
  2. Else, return \ERROR.
\begin{array}{lclll}
\F{module\_validate}(m) &=& \epsilon && (\iff {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast) \\
\F{module\_validate}(m) &=& \ERROR && (\otherwise) \\
\end{array}

.. index:: instantiation, module instance

\F{module\_instantiate}(\store, \module, \externval^\ast) : (\store, \moduleinst ~|~ \error)

  1. Try :ref:`instantiating <exec-instantiation>` \module in \store with :ref:`external values <syntax-externval>` \externval^\ast as imports:
  1. If it succeeds with a :ref:`module instance <syntax-moduleinst>` \moduleinst, then let \X{result} be \moduleinst.
  2. Else, let \X{result} be \ERROR.
  1. Return the new store paired with \X{result}.
\begin{array}{lclll}
\F{module\_instantiate}(S, m, \X{ev}^\ast) &=& (S', F.\AMODULE) && (\iff \instantiate(S, m, \X{ev}^\ast) \stepto^\ast S'; F; \epsilon) \\
\F{module\_instantiate}(S, m, \X{ev}^\ast) &=& (S', \ERROR) && (\iff \instantiate(S, m, \X{ev}^\ast) \stepto^\ast S'; F; \TRAP) \\
\end{array}

Note

The store may be modified even in case of an error.

.. index:: import

\F{module\_imports}(\module) : (\name, \name, \externtype)^\ast

  1. Pre-condition: \module is :ref:`valid <valid-module>` with external import types \externtype^\ast and external export types {\externtype'}^\ast.
  2. Let \import^\ast be the :ref:`imports <syntax-import>` \module.\MIMPORTS.
  3. Assert: the length of \import^\ast equals the length of \externtype^\ast.
  4. For each \import_i in \import^\ast and corresponding \externtype_i in \externtype^\ast, do:
  1. Let \X{result}_i be the triple (\import_i.\IMODULE, \import_i.\INAME, \externtype_i).
  1. Return the concatenation of all \X{result}_i, in index order.
  2. Post-condition: each \externtype_i is :ref:`valid <valid-externtype>`.
~ \\
\begin{array}{lclll}
\F{module\_imports}(m) &=& (\X{im}.\IMODULE, \X{im}.\INAME, \externtype)^\ast \\
  && \qquad (\iff \X{im}^\ast = m.\MIMPORTS \wedge {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast) \\
\end{array}

.. index:: export

\F{module\_exports}(\module) : (\name, \externtype)^\ast

  1. Pre-condition: \module is :ref:`valid <valid-module>` with external import types \externtype^\ast and external export types {\externtype'}^\ast.
  2. Let \export^\ast be the :ref:`exports <syntax-export>` \module.\MEXPORTS.
  3. Assert: the length of \export^\ast equals the length of {\externtype'}^\ast.
  4. For each \export_i in \export^\ast and corresponding \externtype'_i in {\externtype'}^\ast, do:
  1. Let \X{result}_i be the pair (\export_i.\ENAME, \externtype'_i).
  1. Return the concatenation of all \X{result}_i, in index order.
  2. Post-condition: each \externtype'_i is :ref:`valid <valid-externtype>`.
~ \\
\begin{array}{lclll}
\F{module\_exports}(m) &=& (\X{ex}.\ENAME, \externtype')^\ast \\
  && \qquad (\iff \X{ex}^\ast = m.\MEXPORTS \wedge {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast) \\
\end{array}

.. index:: module, module instance

Module Instances

.. index:: export, export instance

\F{instance\_export}(\moduleinst, \name) : \externval ~|~ \error

  1. Assert: due to :ref:`validity <valid-moduleinst>` of the :ref:`module instance <syntax-moduleinst>` \moduleinst, all its :ref:`export names <syntax-exportinst>` are different.
  2. If there exists an \exportinst_i in \moduleinst.\MIEXPORTS such that :ref:`name <syntax-name>` \exportinst_i.\EINAME equals \name, then:
    1. Return the :ref:`external value <syntax-externval>` \exportinst_i.\EIVALUE.
  3. Else, return \ERROR.
~ \\
\begin{array}{lclll}
\F{instance\_export}(m, \name) &=& m.\MIEXPORTS[i].\EIVALUE && (\iff m.\MEXPORTS[i].\EINAME = \name) \\
\F{instance\_export}(m, \name) &=& \ERROR && (\otherwise) \\
\end{array}

.. index:: function, host function, function address, function instance, function type, store

Functions

\F{func\_alloc}(\store, \functype, \hostfunc) : (\store, \funcaddr)

  1. Pre-condition: \functype is :ref:`valid <valid-functype>`.
  2. Let \funcaddr be the result of :ref:`allocating a host function <alloc-func>` in \store with :ref:`function type <syntax-functype>` \functype and host function code \hostfunc.
  3. Return the new store paired with \funcaddr.
\begin{array}{lclll}
\F{func\_alloc}(S, \X{ft}, \X{code}) &=& (S', \X{a}) && (\iff \allochostfunc(S, \X{ft}, \X{code}) = S', \X{a}) \\
\end{array}

Note

This operation assumes that \hostfunc satisfies the :ref:`pre- and post-conditions <exec-invoke-host>` required for a function instance with type \functype.

Regular (non-host) function instances can only be created indirectly through :ref:`module instantiation <embed-module-instantiate>`.

\F{func\_type}(\store, \funcaddr) : \functype

  1. Return S.\SFUNCS[a].\FITYPE.
  2. Post-condition: the returned :ref:`function type <syntax-functype>` is :ref:`valid <valid-functype>`.
\begin{array}{lclll}
\F{func\_type}(S, a) &=& S.\SFUNCS[a].\FITYPE \\
\end{array}

.. index:: invocation, value, result

\F{func\_invoke}(\store, \funcaddr, \val^\ast) : (\store, \val^\ast ~|~ \exception ~|~ \error)

  1. Try :ref:`invoking <exec-invocation>` the function \funcaddr in \store with :ref:`values <syntax-val>` \val^\ast as arguments:
  1. If it succeeds with :ref:`values <syntax-val>` {\val'}^\ast as results, then let \X{result} be {\val'}^\ast.
  2. Else if the outcome is an exception with a thrown :ref:`exception <exec-throw_ref>` \REFEXNADDR~\exnaddr as the result, then let \X{result} be \ETHROW~\exnaddr
  3. Else it has trapped, hence let \X{result} be \ERROR.
  1. Return the new store paired with \X{result}.
~ \\
\begin{array}{lclll}
\F{func\_invoke}(S, a, v^\ast) &=& (S', {v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; {v'}^\ast) \\
\F{func\_invoke}(S, a, v^\ast) &=& (S', \ETHROW~a') && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \XT[(\REFEXNADDR~a')~\THROWREF] \\
\F{func\_invoke}(S, a, v^\ast) &=& (S', \ERROR) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \TRAP) \\
\end{array}

Note

The store may be modified even in case of an error.

.. index:: table, table address, store, table instance, table type, element, function address

Tables

\F{table\_alloc}(\store, \tabletype, \reff) : (\store, \tableaddr)

  1. Pre-condition: \tabletype is :ref:`valid <valid-tabletype>`.
  2. Let \tableaddr be the result of :ref:`allocating a table <alloc-table>` in \store with :ref:`table type <syntax-tabletype>` \tabletype and initialization value \reff.
  3. Return the new store paired with \tableaddr.
\begin{array}{lclll}
\F{table\_alloc}(S, \X{tt}, r) &=& (S', \X{a}) && (\iff \alloctable(S, \X{tt}, r) = S', \X{a}) \\
\end{array}

\F{table\_type}(\store, \tableaddr) : \tabletype

  1. Return S.\STABLES[a].\TITYPE.
  2. Post-condition: the returned :ref:`table type <syntax-tabletype>` is :ref:`valid <valid-tabletype>`.
\begin{array}{lclll}
\F{table\_type}(S, a) &=& S.\STABLES[a].\TITYPE \\
\end{array}

\F{table\_read}(\store, \tableaddr, i:\u32) : \reff ~|~ \error

  1. Let \X{ti} be the :ref:`table instance <syntax-tableinst>` \store.\STABLES[\tableaddr].
  2. If i is larger than or equal to the length of \X{ti}.\TIELEM, then return \ERROR.
  3. Else, return the :ref:`reference value <syntax-ref>` \X{ti}.\TIELEM[i].
\begin{array}{lclll}
\F{table\_read}(S, a, i) &=& r && (\iff S.\STABLES[a].\TIELEM[i] = r) \\
\F{table\_read}(S, a, i) &=& \ERROR && (\otherwise) \\
\end{array}

\F{table\_write}(\store, \tableaddr, i:\u32, \reff) : \store ~|~ \error

  1. Let \X{ti} be the :ref:`table instance <syntax-tableinst>` \store.\STABLES[\tableaddr].
  2. If i is larger than or equal to the length of \X{ti}.\TIELEM, then return \ERROR.
  3. Replace \X{ti}.\TIELEM[i] with the :ref:`reference value <syntax-ref>` \reff.
  4. Return the updated store.
\begin{array}{lclll}
\F{table\_write}(S, a, i, r) &=& S' && (\iff S' = S \with \STABLES[a].\TIELEM[i] = r) \\
\F{table\_write}(S, a, i, r) &=& \ERROR && (\otherwise) \\
\end{array}

\F{table\_size}(\store, \tableaddr) : \u32

  1. Return the length of \store.\STABLES[\tableaddr].\TIELEM.
~ \\
\begin{array}{lclll}
\F{table\_size}(S, a) &=& n &&
  (\iff |S.\STABLES[a].\TIELEM| = n) \\
\end{array}

\F{table\_grow}(\store, \tableaddr, n:\u32, \reff) : \store ~|~ \error

  1. Try :ref:`growing <grow-table>` the :ref:`table instance <syntax-tableinst>` \store.\STABLES[\tableaddr] by n elements with initialization value \reff:
    1. If it succeeds, return the updated store.
    2. Else, return \ERROR.
~ \\
\begin{array}{lclll}
\F{table\_grow}(S, a, n, r) &=& S' &&
  (\iff S' = S \with \STABLES[a] = \growtable(S.\STABLES[a], n, r)) \\
\F{table\_grow}(S, a, n, r) &=& \ERROR && (\otherwise) \\
\end{array}

.. index:: memory, memory address, store, memory instance, memory type, byte

Memories

\F{mem\_alloc}(\store, \memtype) : (\store, \memaddr)

  1. Pre-condition: \memtype is :ref:`valid <valid-memtype>`.
  2. Let \memaddr be the result of :ref:`allocating a memory <alloc-mem>` in \store with :ref:`memory type <syntax-memtype>` \memtype.
  3. Return the new store paired with \memaddr.
\begin{array}{lclll}
\F{mem\_alloc}(S, \X{mt}) &=& (S', \X{a}) && (\iff \allocmem(S, \X{mt}) = S', \X{a}) \\
\end{array}

\F{mem\_type}(\store, \memaddr) : \memtype

  1. Return S.\SMEMS[a].\MITYPE.
  2. Post-condition: the returned :ref:`memory type <syntax-memtype>` is :ref:`valid <valid-memtype>`.
\begin{array}{lclll}
\F{mem\_type}(S, a) &=& S.\SMEMS[a].\MITYPE \\
\end{array}

\F{mem\_read}(\store, \memaddr, i:\u32) : \byte ~|~ \error

  1. Let \X{mi} be the :ref:`memory instance <syntax-meminst>` \store.\SMEMS[\memaddr].
  2. If i is larger than or equal to the length of \X{mi}.\MIDATA, then return \ERROR.
  3. Else, return the :ref:`byte <syntax-byte>` \X{mi}.\MIDATA[i].
\begin{array}{lclll}
\F{mem\_read}(S, a, i) &=& b && (\iff S.\SMEMS[a].\MIDATA[i] = b) \\
\F{mem\_read}(S, a, i) &=& \ERROR && (\otherwise) \\
\end{array}

\F{mem\_write}(\store, \memaddr, i:\u32, \byte) : \store ~|~ \error

  1. Let \X{mi} be the :ref:`memory instance <syntax-meminst>` \store.\SMEMS[\memaddr].
  2. If \u32 is larger than or equal to the length of \X{mi}.\MIDATA, then return \ERROR.
  3. Replace \X{mi}.\MIDATA[i] with \byte.
  4. Return the updated store.
\begin{array}{lclll}
\F{mem\_write}(S, a, i, b) &=& S' && (\iff S' = S \with \SMEMS[a].\MIDATA[i] = b) \\
\F{mem\_write}(S, a, i, b) &=& \ERROR && (\otherwise) \\
\end{array}

\F{mem\_size}(\store, \memaddr) : \u32

  1. Return the length of \store.\SMEMS[\memaddr].\MIDATA divided by the :ref:`page size <page-size>`.
~ \\
\begin{array}{lclll}
\F{mem\_size}(S, a) &=& n &&
  (\iff |S.\SMEMS[a].\MIDATA| = n \cdot 64\,\F{Ki}) \\
\end{array}

\F{mem\_grow}(\store, \memaddr, n:\u32) : \store ~|~ \error

  1. Try :ref:`growing <grow-mem>` the :ref:`memory instance <syntax-meminst>` \store.\SMEMS[\memaddr] by n :ref:`pages <page-size>`:
    1. If it succeeds, return the updated store.
    2. Else, return \ERROR.
~ \\
\begin{array}{lclll}
\F{mem\_grow}(S, a, n) &=& S' &&
  (\iff S' = S \with \SMEMS[a] = \growmem(S.\SMEMS[a], n)) \\
\F{mem\_grow}(S, a, n) &=& \ERROR && (\otherwise) \\
\end{array}

.. index:: tag, tag address, store, tag instance, tag type, function type

Tags

\F{tag\_alloc}(\store, \tagtype) : (\store, \tagaddr)

  1. Pre-condition: tagtype is :ref:`valid <valid-tagtype>`.
  2. Let \tagaddr be the result of :ref:`allocating a tag <alloc-tag>` in \store with :ref:`tag type <syntax-tagtype>` \tagtype.
  3. Return the new store paired with \tagaddr.
\begin{array}{lclll}
\F{tag\_alloc}(S, \X{tt}) &=& (S', \X{a}) && (\iff \alloctag(S, \X{tt}) = S', \X{a}) \\
\end{array}

\F{tag\_type}(\store, \tagaddr) : \tagtype

  1. Return S.\STAGS[a].\TAGITYPE.
  2. Post-condition: the returned :ref:`tag type <syntax-tagtype>` is :ref:`valid <valid-tagtype>`.
\begin{array}{lclll}
\F{tag\_type}(S, a) &=& S.\STAGS[a].\TAGITYPE \\
\end{array}

.. index:: exception, exception address, store, exception instance, exception type

Exceptions

\F{exn\_alloc}(\store, \tagaddr, \val^\ast) : (\store, \exnaddr)

  1. Pre-condition: \tagaddr is an allocated :ref:`tag address <syntax-tagaddr>`.
  2. Let \exnaddr be the result of :ref:`allocating an exception <alloc-exception>` in \store with :ref:`tag address <syntax-tagaddr>` \tagaddr and initialization values \val^\ast.
  3. Return the new store paired with \exnaddr.
\begin{array}{lclll}
\F{exn\_alloc}(S, \tagaddr, \val^\ast) &=& (S', a) && (\iff \allocexn(S, \tagaddr, \val^\ast) = S', a) \\
\end{array}

\F{exn\_read}(\store, \exnaddr) : (\tagaddr, \val^\ast)

  1. Let \X{ei} be the :ref:`exception instance <syntax-exninst>` \store.\SEXNS[\exnaddr].
  2. Return the :ref:`tag address <syntax-tagaddr>` \X{ei}.\EITAG~\tagaddr paired with :ref:`values <syntax-val>` \X{ei}.\EIFIELDS~\val^\ast.
\begin{array}{lcll}
\F{exn\_read}(S, a) &=& (a', v^\ast) \\
\end{array}

.. index:: global, global address, store, global instance, global type, value

Globals

\F{global\_alloc}(\store, \globaltype, \val) : (\store, \globaladdr)

  1. Pre-condition: \globaltype is :ref:`valid <valid-globaltype>`.
  2. Let \globaladdr be the result of :ref:`allocating a global <alloc-global>` in \store with :ref:`global type <syntax-globaltype>` \globaltype and initialization value \val.
  3. Return the new store paired with \globaladdr.
\begin{array}{lclll}
\F{global\_alloc}(S, \X{gt}, v) &=& (S', \X{a}) && (\iff \allocglobal(S, \X{gt}, v) = S', \X{a}) \\
\end{array}

\F{global\_type}(\store, \globaladdr) : \globaltype

  1. Return S.\SGLOBALS[a].\GITYPE.
  2. Post-condition: the returned :ref:`global type <syntax-globaltype>` is :ref:`valid <valid-globaltype>`.
\begin{array}{lclll}
\F{global\_type}(S, a) &=& S.\SGLOBALS[a].\GITYPE \\
\end{array}

\F{global\_read}(\store, \globaladdr) : \val

  1. Let \X{gi} be the :ref:`global instance <syntax-globalinst>` \store.\SGLOBALS[\globaladdr].
  2. Return the :ref:`value <syntax-val>` \X{gi}.\GIVALUE.
\begin{array}{lclll}
\F{global\_read}(S, a) &=& v && (\iff S.\SGLOBALS[a].\GIVALUE = v) \\
\end{array}

\F{global\_write}(\store, \globaladdr, \val) : \store ~|~ \error

  1. Let \X{gi} be the :ref:`global instance <syntax-globalinst>` \store.\SGLOBALS[\globaladdr].
  2. Let \mut~t be the structure of the :ref:`global type <syntax-globaltype>` \X{gi}.\GITYPE.
  3. If \mut is not \MVAR, then return \ERROR.
  4. Replace \X{gi}.\GIVALUE with the :ref:`value <syntax-val>` \val.
  5. Return the updated store.
~ \\
\begin{array}{lclll}
\F{global\_write}(S, a, v) &=& S' && (\iff S.\SGLOBALS[a].\GITYPE = \MVAR~t \wedge S' = S \with \SGLOBALS[a].\GIVALUE = v) \\
\F{global\_write}(S, a, v) &=& \ERROR && (\otherwise) \\
\end{array}