Skip to content

Latest commit

 

History

History
617 lines (379 loc) · 20.8 KB

embedding.rst

File metadata and controls

617 lines (379 loc) · 20.8 KB
.. 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-parse-module>` of the :ref:`text format <text>`.

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.

Failure of an interface operation is 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.

.. index:: allocation, store

Store

\F{init\_store}() : \store

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

.. index:: module

Modules

.. index:: binary format

\F{decode\_module}(\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{decode\_module}(b^\ast) &=& m && (\iff \Bmodule \stackrel\ast\Longrightarrow m{:}b^\ast) \\
\F{decode\_module}(b^\ast) &=& \ERROR && (\otherwise) \\
\end{array}

.. index:: text format

\F{parse\_module}(\codepoint^\ast) : \module ~|~ \error

  1. If there exists a derivation for the :ref:`source <text-source>` \codepoint^\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{parse\_module}(c^\ast) &=& m && (\iff \Tmodule \stackrel\ast\Longrightarrow m{:}c^\ast) \\
\F{parse\_module}(c^\ast) &=& \ERROR && (\otherwise) \\
\end{array}

.. index:: validation

\F{validate\_module}(\module) : \error^?

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

.. index:: instantiation, module instance

\F{instantiate\_module}(\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{instantiate\_module}(S, m, \X{ev}^\ast) &=& (S', F.\AMODULE) && (\iff \instantiate(S, m, \X{ev}^\ast) \stepto^\ast S'; F; \epsilon) \\
\F{instantiate\_module}(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. Assert: \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.
~ \\
\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. Assert: \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.
~ \\
\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, store, module instance, export instance

Exports

\F{get\_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{get\_export}(m, \name) &=& m.\MIEXPORTS[i].\EIVALUE && (\iff m.\MEXPORTS[i].\EINAME = \name) \\
\F{get\_export}(m, \name) &=& \ERROR && (\otherwise) \\
\end{array}

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

Functions

\F{alloc\_func}(\store, \functype, \hostfunc) : (\store, \funcaddr)

  1. 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.
  2. Return the new store paired with \funcaddr.
\begin{array}{lclll}
\F{alloc\_func}(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-instantiate-module>`.

\F{type\_func}(\store, \funcaddr) : \functype

  1. Assert: \store.\SFUNCS[\funcaddr] exists.
  2. Assert: the :ref:`external value <syntax-externval>` \EVFUNC~\funcaddr is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` \ETFUNC~\functype.
  3. Return \functype.
\begin{array}{lclll}
\F{type\_func}(S, a) &=& \X{ft} && (\iff S \vdashexternval \EVFUNC~a : \ETFUNC~\X{ft}) \\
\end{array}

.. index:: invocation, value, result

\F{invoke\_func}(\store, \funcaddr, \val^\ast) : (\store, \val^\ast ~|~ \error)`

  1. Assert: \store.\SFUNCS[\funcaddr] exists.
  2. 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 it has trapped, hence let \X{result} be \ERROR.
  1. Return the new store paired with \X{result}.
~ \\
\begin{array}{lclll}
\F{invoke\_func}(S, a, v^\ast) &=& (S', {v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; {v'}^\ast) \\
\F{invoke\_func}(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{alloc\_table}(\store, \tabletype) : (\store, \tableaddr)

  1. Let \tableaddr be the result of :ref:`allocating a table <alloc-table>` in \store with :ref:`table type <syntax-tabletype>` \tabletype.
  2. Return the new store paired with \tableaddr.
\begin{array}{lclll}
\F{alloc\_table}(S, \X{tt}) &=& (S', \X{a}) && (\iff \alloctable(S, \X{tt}) = S', \X{a}) \\
\end{array}

\F{type\_table}(\store, \tableaddr) : \tabletype

  1. Assert: \store.\STABLES[\tableaddr] exists.
  2. Assert: the :ref:`external value <syntax-externval>` \EVTABLE~\tableaddr is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` \ETTABLE~\tabletype.
  3. Return \tabletype.
\begin{array}{lclll}
\F{type\_table}(S, a) &=& \X{tt} && (\iff S \vdashexternval \EVTABLE~a : \ETTABLE~\X{tt}) \\
\end{array}

\F{read\_table}(\store, \tableaddr, i) : \funcaddr ~|~ \error

  1. Assert: \store.\STABLES[\tableaddr] exists.
  2. Assert: i is a non-negative integer.
  3. Let \X{ti} be the :ref:`table instance <syntax-tableinst>` \store.\STABLES[\tableaddr].
  4. If i is larger than or equal to the length if \X{ti}.\TIELEM, then return \ERROR.
  5. Else, return \X{ti}.\TIELEM[i].
\begin{array}{lclll}
\F{read\_table}(S, a, i) &=& \X{fa}^? && (\iff S.\STABLES[a].\TIELEM[i] = \X{fa}^?) \\
\F{read\_table}(S, a, i) &=& \ERROR && (\otherwise) \\
\end{array}

\F{write\_table}(\store, \tableaddr, i, \funcaddr^?) : \store ~|~ \error

  1. Assert: \store.\STABLES[\tableaddr] exists.
  2. Assert: i is a non-negative integer.
  3. Let \X{ti} be the :ref:`table instance <syntax-tableinst>` \store.\STABLES[\tableaddr].
  4. If i is larger than or equal to the length if \X{ti}.\TIELEM, then return \ERROR.
  5. Replace \X{ti}.\TIELEM[i] with the optional :ref:`function address <syntax-funcaddr>` \X{fa}^?.
  6. Return the updated store.
\begin{array}{lclll}
\F{write\_table}(S, a, i, \X{fa}^?) &=& S' && (\iff S' = S \with \STABLES[a].\TIELEM[i] = \X{fa}^?) \\
\F{write\_table}(S, a, i, \X{fa}^?) &=& \ERROR && (\otherwise) \\
\end{array}

\F{size\_table}(\store, \tableaddr) : \i32

  1. Assert: \store.\STABLES[\tableaddr] exists.
  2. Return the length of \store.\STABLES[\tableaddr].\TIELEM.
~ \\
\begin{array}{lclll}
\F{size\_table}(S, a) &=& n &&
  (\iff |S.\STABLES[a].\TIELEM| = n) \\
\end{array}

\F{grow\_table}(\store, \tableaddr, n) : \store ~|~ \error

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

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

Memories

\F{alloc\_mem}(\store, \memtype) : (\store, \memaddr)

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

\F{type\_mem}(\store, \memaddr) : \memtype

  1. Assert: \store.\SMEMS[\memaddr] exists.
  2. Assert: the :ref:`external value <syntax-externval>` \EVMEM~\memaddr is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` \ETMEM~\memtype.
  3. Return \memtype.
\begin{array}{lclll}
\F{type\_mem}(S, a) &=& \X{mt} && (\iff S \vdashexternval \EVMEM~a : \ETMEM~\X{mt}) \\
\end{array}

\F{read\_mem}(\store, \memaddr, i) : \byte ~|~ \error

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

\F{write\_mem}(\store, \memaddr, i, \byte) : \store ~|~ \error

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

\F{size\_mem}(\store, \memaddr) : \i32

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

\F{grow\_mem}(\store, \memaddr, n) : \store ~|~ \error

  1. Assert: \store.\SMEMS[\memaddr] exists.
  2. Assert: n is a non-negative integer.
  3. 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{grow\_mem}(S, a, n) &=& S' &&
  (\iff S' = S \with \SMEMS[a] = \growmem(S.\SMEMS[a], n)) \\
\F{grow\_mem}(S, a, n) &=& \ERROR && (\otherwise) \\
\end{array}

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

Globals

\F{alloc\_global}(\store, \globaltype, \val) : (\store, \globaladdr)

  1. 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.
  2. Return the new store paired with \globaladdr.
\begin{array}{lclll}
\F{alloc\_global}(S, \X{gt}, v) &=& (S', \X{a}) && (\iff \allocglobal(S, \X{gt}, v) = S', \X{a}) \\
\end{array}

\F{type\_global}(\store, \globaladdr) : \globaltype

  1. Assert: \store.\SGLOBALS[\globaladdr] exists.
  2. Assert: the :ref:`external value <syntax-externval>` \EVGLOBAL~\globaladdr is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` \ETGLOBAL~\globaltype.
  3. Return \globaltype.
\begin{array}{lclll}
\F{type\_global}(S, a) &=& \X{gt} && (\iff S \vdashexternval \EVGLOBAL~a : \ETGLOBAL~\X{gt}) \\
\end{array}

\F{read\_global}(\store, \globaladdr) : \val

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

\F{write\_global}(\store, \globaladdr, \val) : \store ~|~ \error

  1. Assert: \store.\SGLOBALS[a] exists.
  2. Let \X{gi} be the :ref:`global instance <syntax-globalinst>` \store.\SGLOBALS[\globaladdr].
  3. If \X{gi}.\GIMUT 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{write\_global}(S, a, v) &=& S' && (\iff S.\SGLOBALS[a].\GIMUT = \MVAR \wedge S' = S \with \SGLOBALS[a].\GIVALUE = v) \\
\F{write\_global}(S, a, v) &=& \ERROR && (\otherwise) \\
\end{array}