| .. index:: ! embedding, embedder, implementation, host |
| .. _embed: |
| |
| 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 :math:`n:\u32` is used to specify a symbolic name in addition to the respective value range. |
| |
| |
| .. _embed-error: |
| |
| Errors |
| ...... |
| |
| Failure of an interface operation is indicated by an auxiliary syntactic class: |
| |
| .. math:: |
| \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>` (:math:`store`, :math:`\moduleinst`, :math:`\externval`, :ref:`addresses <syntax-addr>`): |
| |
| * Every runtime object passed as a parameter must be :ref:`valid <valid-store>` per an implicit pre-condition. |
| |
| * Every runtime object returned as a result is :ref:`valid <valid-store>` per an implicit post-condition. |
| |
| .. 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 |
| .. _embed-store: |
| |
| Store |
| ~~~~~ |
| |
| .. _embed-store-init: |
| |
| :math:`\F{store\_init}() : \store` |
| .................................. |
| |
| 1. Return the empty :ref:`store <syntax-store>`. |
| |
| .. math:: |
| \begin{array}{lclll} |
| \F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\ |
| \end{array} |
| |
| |
| |
| .. index:: module |
| .. _embed-module: |
| |
| Modules |
| ~~~~~~~ |
| |
| .. index:: binary format |
| .. _embed-module-decode: |
| |
| :math:`\F{module\_decode}(\byte^\ast) : \module ~|~ \error` |
| ........................................................... |
| |
| 1. If there exists a derivation for the :ref:`byte <syntax-byte>` sequence :math:`\byte^\ast` as a :math:`\Bmodule` according to the :ref:`binary grammar for modules <binary-module>`, yielding a :ref:`module <syntax-module>` :math:`m`, then return :math:`m`. |
| |
| 2. Else, return :math:`\ERROR`. |
| |
| .. math:: |
| \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 |
| .. _embed-module-parse: |
| |
| :math:`\F{module\_parse}(\char^\ast) : \module ~|~ \error` |
| .......................................................... |
| |
| 1. If there exists a derivation for the :ref:`source <text-source>` :math:`\char^\ast` as a :math:`\Tmodule` according to the :ref:`text grammar for modules <text-module>`, yielding a :ref:`module <syntax-module>` :math:`m`, then return :math:`m`. |
| |
| 2. Else, return :math:`\ERROR`. |
| |
| .. math:: |
| \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 |
| .. _embed-module-validate: |
| |
| :math:`\F{module\_validate}(\module) : \error^?` |
| ................................................ |
| |
| 1. If :math:`\module` is :ref:`valid <valid-module>`, then return nothing. |
| |
| 2. Else, return :math:`\ERROR`. |
| |
| .. math:: |
| \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 |
| .. _embed-module-instantiate: |
| |
| :math:`\F{module\_instantiate}(\store, \module, \externval^\ast) : (\store, \moduleinst ~|~ \error)` |
| .................................................................................................... |
| |
| 1. Try :ref:`instantiating <exec-instantiation>` :math:`\module` in :math:`\store` with :ref:`external values <syntax-externval>` :math:`\externval^\ast` as imports: |
| |
| a. If it succeeds with a :ref:`module instance <syntax-moduleinst>` :math:`\moduleinst`, then let :math:`\X{result}` be :math:`\moduleinst`. |
| |
| b. Else, let :math:`\X{result}` be :math:`\ERROR`. |
| |
| 2. Return the new store paired with :math:`\X{result}`. |
| |
| .. math:: |
| \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 |
| .. _embed-module-imports: |
| |
| :math:`\F{module\_imports}(\module) : (\name, \name, \externtype)^\ast` |
| ....................................................................... |
| |
| 1. Pre-condition: :math:`\module` is :ref:`valid <valid-module>` with external import types :math:`\externtype^\ast` and external export types :math:`{\externtype'}^\ast`. |
| |
| 2. Let :math:`\import^\ast` be the :ref:`imports <syntax-import>` :math:`\module.\MIMPORTS`. |
| |
| 3. Assert: the length of :math:`\import^\ast` equals the length of :math:`\externtype^\ast`. |
| |
| 4. For each :math:`\import_i` in :math:`\import^\ast` and corresponding :math:`\externtype_i` in :math:`\externtype^\ast`, do: |
| |
| a. Let :math:`\X{result}_i` be the triple :math:`(\import_i.\IMODULE, \import_i.\INAME, \externtype_i)`. |
| |
| 5. Return the concatenation of all :math:`\X{result}_i`, in index order. |
| |
| 6. Post-condition: each :math:`\externtype_i` is :ref:`valid <valid-externtype>`. |
| |
| .. math:: |
| ~ \\ |
| \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 |
| .. _embed-module-exports: |
| |
| :math:`\F{module\_exports}(\module) : (\name, \externtype)^\ast` |
| ................................................................ |
| |
| 1. Pre-condition: :math:`\module` is :ref:`valid <valid-module>` with external import types :math:`\externtype^\ast` and external export types :math:`{\externtype'}^\ast`. |
| |
| 2. Let :math:`\export^\ast` be the :ref:`exports <syntax-export>` :math:`\module.\MEXPORTS`. |
| |
| 3. Assert: the length of :math:`\export^\ast` equals the length of :math:`{\externtype'}^\ast`. |
| |
| 4. For each :math:`\export_i` in :math:`\export^\ast` and corresponding :math:`\externtype'_i` in :math:`{\externtype'}^\ast`, do: |
| |
| a. Let :math:`\X{result}_i` be the pair :math:`(\export_i.\ENAME, \externtype'_i)`. |
| |
| 5. Return the concatenation of all :math:`\X{result}_i`, in index order. |
| |
| 6. Post-condition: each :math:`\externtype'_i` is :ref:`valid <valid-externtype>`. |
| |
| .. math:: |
| ~ \\ |
| \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 |
| .. _embed-instance: |
| |
| Module Instances |
| ~~~~~~~~~~~~~~~~ |
| |
| .. index:: export, export instance |
| |
| .. _embed-instance-export: |
| |
| :math:`\F{instance\_export}(\moduleinst, \name) : \externval ~|~ \error` |
| ........................................................................ |
| |
| 1. Assert: due to :ref:`validity <valid-moduleinst>` of the :ref:`module instance <syntax-moduleinst>` :math:`\moduleinst`, all its :ref:`export names <syntax-exportinst>` are different. |
| |
| 2. If there exists an :math:`\exportinst_i` in :math:`\moduleinst.\MIEXPORTS` such that :ref:`name <syntax-name>` :math:`\exportinst_i.\EINAME` equals :math:`\name`, then: |
| |
| a. Return the :ref:`external value <syntax-externval>` :math:`\exportinst_i.\EIVALUE`. |
| |
| 3. Else, return :math:`\ERROR`. |
| |
| .. math:: |
| ~ \\ |
| \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 |
| .. _embed-func: |
| |
| Functions |
| ~~~~~~~~~ |
| |
| .. _embed-func-alloc: |
| |
| :math:`\F{func\_alloc}(\store, \functype, \hostfunc) : (\store, \funcaddr)` |
| ........................................................................... |
| |
| 1. Pre-condition: :math:`\functype` is :math:`valid <valid-functype>`. |
| |
| 2. Let :math:`\funcaddr` be the result of :ref:`allocating a host function <alloc-func>` in :math:`\store` with :ref:`function type <syntax-functype>` :math:`\functype` and host function code :math:`\hostfunc`. |
| |
| 3. Return the new store paired with :math:`\funcaddr`. |
| |
| .. math:: |
| \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 :math:`\hostfunc` satisfies the :ref:`pre- and post-conditions <exec-invoke-host>` required for a function instance with type :math:`\functype`. |
| |
| Regular (non-host) function instances can only be created indirectly through :ref:`module instantiation <embed-module-instantiate>`. |
| |
| |
| .. _embed-func-type: |
| |
| :math:`\F{func\_type}(\store, \funcaddr) : \functype` |
| ..................................................... |
| |
| 1. Assert: the :ref:`external value <syntax-externval>` :math:`\EVFUNC~\funcaddr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETFUNC~\functype`. |
| |
| 2. Return :math:`\functype`. |
| |
| 3. Post-condition: :math:`\functype` is :ref:`valid <valid-functype>`. |
| |
| .. math:: |
| \begin{array}{lclll} |
| \F{func\_type}(S, a) &=& \X{ft} && (\iff S \vdashexternval \EVFUNC~a : \ETFUNC~\X{ft}) \\ |
| \end{array} |
| |
| |
| .. index:: invocation, value, result |
| .. _embed-func-invoke: |
| |
| :math:`\F{func\_invoke}(\store, \funcaddr, \val^\ast) : (\store, \val^\ast ~|~ \error)` |
| ........................................................................................ |
| |
| 1. Try :ref:`invoking <exec-invocation>` the function :math:`\funcaddr` in :math:`\store` with :ref:`values <syntax-val>` :math:`\val^\ast` as arguments: |
| |
| a. If it succeeds with :ref:`values <syntax-val>` :math:`{\val'}^\ast` as results, then let :math:`\X{result}` be :math:`{\val'}^\ast`. |
| |
| b. Else it has trapped, hence let :math:`\X{result}` be :math:`\ERROR`. |
| |
| 2. Return the new store paired with :math:`\X{result}`. |
| |
| .. math:: |
| ~ \\ |
| \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', \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 |
| .. _embed-table: |
| |
| Tables |
| ~~~~~~ |
| |
| .. _embed-table-alloc: |
| |
| :math:`\F{table\_alloc}(\store, \tabletype) : (\store, \tableaddr)` |
| ................................................................... |
| |
| 1. Pre-condition: :math:`\tabletype` is :math:`valid <valid-tabletype>`. |
| |
| 2. Let :math:`\tableaddr` be the result of :ref:`allocating a table <alloc-table>` in :math:`\store` with :ref:`table type <syntax-tabletype>` :math:`\tabletype`. |
| |
| 3. Return the new store paired with :math:`\tableaddr`. |
| |
| .. math:: |
| \begin{array}{lclll} |
| \F{table\_alloc}(S, \X{tt}) &=& (S', \X{a}) && (\iff \alloctable(S, \X{tt}) = S', \X{a}) \\ |
| \end{array} |
| |
| |
| .. _embed-table-type: |
| |
| :math:`\F{table\_type}(\store, \tableaddr) : \tabletype` |
| ........................................................ |
| |
| 1. Assert: the :ref:`external value <syntax-externval>` :math:`\EVTABLE~\tableaddr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETTABLE~\tabletype`. |
| |
| 2. Return :math:`\tabletype`. |
| |
| 3. Post-condition: :math:`\tabletype` is :math:`valid <valid-tabletype>`. |
| |
| .. math:: |
| \begin{array}{lclll} |
| \F{table\_type}(S, a) &=& \X{tt} && (\iff S \vdashexternval \EVTABLE~a : \ETTABLE~\X{tt}) \\ |
| \end{array} |
| |
| |
| .. _embed-table-read: |
| |
| :math:`\F{table\_read}(\store, \tableaddr, i:\u32) : \funcaddr^? ~|~ \error` |
| ............................................................................ |
| |
| 1. Let :math:`\X{ti}` be the :ref:`table instance <syntax-tableinst>` :math:`\store.\STABLES[\tableaddr]`. |
| |
| 2. If :math:`i` is larger than or equal to the length of :math:`\X{ti}.\TIELEM`, then return :math:`\ERROR`. |
| |
| 3. Else, return :math:`\X{ti}.\TIELEM[i]`. |
| |
| .. math:: |
| \begin{array}{lclll} |
| \F{table\_read}(S, a, i) &=& \X{fa}^? && (\iff S.\STABLES[a].\TIELEM[i] = \X{fa}^?) \\ |
| \F{table\_read}(S, a, i) &=& \ERROR && (\otherwise) \\ |
| \end{array} |
| |
| |
| .. _embed-table-write: |
| |
| :math:`\F{table\_write}(\store, \tableaddr, i:\u32, \funcaddr^?) : \store ~|~ \error` |
| ....................................................................................... |
| |
| 1. Let :math:`\X{ti}` be the :ref:`table instance <syntax-tableinst>` :math:`\store.\STABLES[\tableaddr]`. |
| |
| 2. If :math:`i` is larger than or equal to the length of :math:`\X{ti}.\TIELEM`, then return :math:`\ERROR`. |
| |
| 3. Replace :math:`\X{ti}.\TIELEM[i]` with the optional :ref:`function address <syntax-funcaddr>` :math:`\X{fa}^?`. |
| |
| 4. Return the updated store. |
| |
| .. math:: |
| \begin{array}{lclll} |
| \F{table\_write}(S, a, i, \X{fa}^?) &=& S' && (\iff S' = S \with \STABLES[a].\TIELEM[i] = \X{fa}^?) \\ |
| \F{table\_write}(S, a, i, \X{fa}^?) &=& \ERROR && (\otherwise) \\ |
| \end{array} |
| |
| |
| .. _embed-table-size: |
| |
| :math:`\F{table\_size}(\store, \tableaddr) : \u32` |
| .................................................. |
| |
| 1. Return the length of :math:`\store.\STABLES[\tableaddr].\TIELEM`. |
| |
| .. math:: |
| ~ \\ |
| \begin{array}{lclll} |
| \F{table\_size}(S, a) &=& n && |
| (\iff |S.\STABLES[a].\TIELEM| = n) \\ |
| \end{array} |
| |
| |
| |
| .. _embed-table-grow: |
| |
| :math:`\F{table\_grow}(\store, \tableaddr, n:\u32) : \store ~|~ \error` |
| ....................................................................... |
| |
| 1. Try :ref:`growing <grow-table>` the :ref:`table instance <syntax-tableinst>` :math:`\store.\STABLES[\tableaddr]` by :math:`n` elements: |
| |
| a. If it succeeds, return the updated store. |
| |
| b. Else, return :math:`\ERROR`. |
| |
| .. math:: |
| ~ \\ |
| \begin{array}{lclll} |
| \F{table\_grow}(S, a, n) &=& S' && |
| (\iff S' = S \with \STABLES[a] = \growtable(S.\STABLES[a], n)) \\ |
| \F{table\_grow}(S, a, n) &=& \ERROR && (\otherwise) \\ |
| \end{array} |
| |
| |
| .. index:: memory, memory address, store, memory instance, memory type, byte |
| .. _embed-mem: |
| |
| Memories |
| ~~~~~~~~ |
| |
| .. _embed-mem-alloc: |
| |
| :math:`\F{mem\_alloc}(\store, \memtype) : (\store, \memaddr)` |
| ................................................................ |
| |
| 1. Pre-condition: :math:`\memtype` is :math:`valid <valid-memtype>`. |
| |
| 2. Let :math:`\memaddr` be the result of :ref:`allocating a memory <alloc-mem>` in :math:`\store` with :ref:`memory type <syntax-memtype>` :math:`\memtype`. |
| |
| 3. Return the new store paired with :math:`\memaddr`. |
| |
| .. math:: |
| \begin{array}{lclll} |
| \F{mem\_alloc}(S, \X{mt}) &=& (S', \X{a}) && (\iff \allocmem(S, \X{mt}) = S', \X{a}) \\ |
| \end{array} |
| |
| |
| .. _embed-mem-type: |
| |
| :math:`\F{mem\_type}(\store, \memaddr) : \memtype` |
| .................................................. |
| |
| 1. Assert: the :ref:`external value <syntax-externval>` :math:`\EVMEM~\memaddr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETMEM~\memtype`. |
| |
| 2. Return :math:`\memtype`. |
| |
| 3. Post-condition: :math:`\memtype` is :math:`valid <valid-memtype>`. |
| |
| .. math:: |
| \begin{array}{lclll} |
| \F{mem\_type}(S, a) &=& \X{mt} && (\iff S \vdashexternval \EVMEM~a : \ETMEM~\X{mt}) \\ |
| \end{array} |
| |
| |
| .. _embed-mem-read: |
| |
| :math:`\F{mem\_read}(\store, \memaddr, i:\u32) : \byte ~|~ \error` |
| .................................................................. |
| |
| 1. Let :math:`\X{mi}` be the :ref:`memory instance <syntax-meminst>` :math:`\store.\SMEMS[\memaddr]`. |
| |
| 2. If :math:`i` is larger than or equal to the length of :math:`\X{mi}.\MIDATA`, then return :math:`\ERROR`. |
| |
| 3. Else, return the :ref:`byte <syntax-byte>` :math:`\X{mi}.\MIDATA[i]`. |
| |
| .. math:: |
| \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} |
| |
| |
| .. _embed-mem-write: |
| |
| :math:`\F{mem\_write}(\store, \memaddr, i:\u32, \byte) : \store ~|~ \error` |
| ........................................................................... |
| |
| 1. Let :math:`\X{mi}` be the :ref:`memory instance <syntax-meminst>` :math:`\store.\SMEMS[\memaddr]`. |
| |
| 2. If :math:`\u32` is larger than or equal to the length of :math:`\X{mi}.\MIDATA`, then return :math:`\ERROR`. |
| |
| 3. Replace :math:`\X{mi}.\MIDATA[i]` with :math:`\byte`. |
| |
| 4. Return the updated store. |
| |
| .. math:: |
| \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} |
| |
| |
| .. _embed-mem-size: |
| |
| :math:`\F{mem\_size}(\store, \memaddr) : \u32` |
| .............................................. |
| |
| 1. Return the length of :math:`\store.\SMEMS[\memaddr].\MIDATA` divided by the :ref:`page size <page-size>`. |
| |
| .. math:: |
| ~ \\ |
| \begin{array}{lclll} |
| \F{mem\_size}(S, a) &=& n && |
| (\iff |S.\SMEMS[a].\MIDATA| = n \cdot 64\,\F{Ki}) \\ |
| \end{array} |
| |
| |
| |
| .. _embed-mem-grow: |
| |
| :math:`\F{mem\_grow}(\store, \memaddr, n:\u32) : \store ~|~ \error` |
| ................................................................... |
| |
| 1. Try :ref:`growing <grow-mem>` the :ref:`memory instance <syntax-meminst>` :math:`\store.\SMEMS[\memaddr]` by :math:`n` :ref:`pages <page-size>`: |
| |
| a. If it succeeds, return the updated store. |
| |
| b. Else, return :math:`\ERROR`. |
| |
| .. math:: |
| ~ \\ |
| \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:: global, global address, store, global instance, global type, value |
| .. _embed-global: |
| |
| Globals |
| ~~~~~~~ |
| |
| .. _embed-global-alloc: |
| |
| :math:`\F{global\_alloc}(\store, \globaltype, \val) : (\store, \globaladdr)` |
| ............................................................................ |
| |
| 1. Pre-condition: :math:`\globaltype` is :math:`valid <valid-globaltype>`. |
| |
| 2. Let :math:`\globaladdr` be the result of :ref:`allocating a global <alloc-global>` in :math:`\store` with :ref:`global type <syntax-globaltype>` :math:`\globaltype` and initialization value :math:`\val`. |
| |
| 3. Return the new store paired with :math:`\globaladdr`. |
| |
| .. math:: |
| \begin{array}{lclll} |
| \F{global\_alloc}(S, \X{gt}, v) &=& (S', \X{a}) && (\iff \allocglobal(S, \X{gt}, v) = S', \X{a}) \\ |
| \end{array} |
| |
| |
| .. _embed-global-type: |
| |
| :math:`\F{global\_type}(\store, \globaladdr) : \globaltype` |
| ........................................................... |
| |
| 1. Assert: the :ref:`external value <syntax-externval>` :math:`\EVGLOBAL~\globaladdr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETGLOBAL~\globaltype`. |
| |
| 2. Return :math:`\globaltype`. |
| |
| 3. Post-condition: :math:`\globaltype` is :math:`valid <valid-globaltype>`. |
| |
| .. math:: |
| \begin{array}{lclll} |
| \F{global\_type}(S, a) &=& \X{gt} && (\iff S \vdashexternval \EVGLOBAL~a : \ETGLOBAL~\X{gt}) \\ |
| \end{array} |
| |
| |
| .. _embed-global-read: |
| |
| :math:`\F{global\_read}(\store, \globaladdr) : \val` |
| .................................................... |
| |
| 1. Let :math:`\X{gi}` be the :ref:`global instance <syntax-globalinst>` :math:`\store.\SGLOBALS[\globaladdr]`. |
| |
| 2. Return the :ref:`value <syntax-val>` :math:`\X{gi}.\GIVALUE`. |
| |
| .. math:: |
| \begin{array}{lclll} |
| \F{global\_read}(S, a) &=& v && (\iff S.\SGLOBALS[a].\GIVALUE = v) \\ |
| \end{array} |
| |
| |
| .. _embed-global-write: |
| |
| :math:`\F{global\_write}(\store, \globaladdr, \val) : \store ~|~ \error` |
| ........................................................................ |
| |
| 1. Let :math:`\X{gi}` be the :ref:`global instance <syntax-globalinst>` :math:`\store.\SGLOBALS[\globaladdr]`. |
| |
| 2. If :math:`\X{gi}.\GIMUT` is not :math:`\MVAR`, then return :math:`\ERROR`. |
| |
| 3. Replace :math:`\X{gi}.\GIVALUE` with the :ref:`value <syntax-val>` :math:`\val`. |
| |
| 4. Return the updated store. |
| |
| .. math:: |
| ~ \\ |
| \begin{array}{lclll} |
| \F{global\_write}(S, a, v) &=& S' && (\iff S.\SGLOBALS[a].\GIMUT = \MVAR \wedge S' = S \with \SGLOBALS[a].\GIVALUE = v) \\ |
| \F{global\_write}(S, a, v) &=& \ERROR && (\otherwise) \\ |
| \end{array} |