From 1f65aa116ab7f2a44edf251c151cc7bffee334ff Mon Sep 17 00:00:00 2001 From: Ben Smith Date: Mon, 21 May 2018 17:51:11 -0700 Subject: [PATCH 1/8] [spec] Document execution --- document/core/exec/instructions.rst | 70 +++++++++++ document/core/exec/modules.rst | 176 ++++++++++++++++++++++------ document/core/exec/runtime.rst | 60 +++++++++- document/core/util/macros.def | 14 +++ 4 files changed, 279 insertions(+), 41 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 3672e42d..54934233 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -618,6 +618,76 @@ Memory Instructions In practice, the choice depends on the :ref:`resources ` available to the :ref:`embedder `. +.. _exec-memory.init: + +:math:`\MEMORYINIT~x` +..................... + +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIMEMS[0]` exists. + +3. Let :math:`ma` be the :ref:`memory address ` :math:`F.\AMODULE.\MIMEMS[0]`. + +4. Assert: due to :ref:`validation `, :math:`S.\SMEMS[ma]` exists. + +5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[ma]`. + +6. Let :math:`msz` be the length of :math:`\X{mem}.\MIDATA`. + +7. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIDATAS[x]` exists. + +8. Let :math:`da` be the :ref:`data segment address ` :math:`F.\AMODULE.\MIDATAS[x]`. + +9. If :math:`S.\SDATA[da]` does not exist, then: + + a. Trap. + +10. Let :math:`\X{data}` be the :ref:`data segment instance ` :math:`S.\SDATA[da]`. + +11. Assert: due to :ref:`validation `, three values of :ref:`value type ` |I32| are on the top of the stack. + +12. Pop the value :math:`\I32.\CONST~s` from the stack. + +13. Pop the value :math:`\I32.\CONST~t` from the stack. + +14. Pop the value :math:`\I32.\CONST~n` from the stack. + +15. Let :math:`dsz` be the length of :math:`\X{data}.\DSIINIT`. + +16. If :math:`s + n > dsz`, then: + + a. Trap. + +17. If :math:`t + n > msz`, then: + + a. Trap. + +18. Let :math:`y` be the byte sequence :math:`\X{mem}.\DSIINIT[s \slice n]`. + +19. :ref:`Initialize ` the memory instance at address :math:`ma` starting from offset :math:`t` with the byte sequence :math:`y`. + +.. math:: + ~\\[-1ex] + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~n)~(\I32.\CONST~t)~(\I32.\CONST~s)~(\MEMORYINIT~x) &\stepto& S; F; (\INITDATA~ma~t~y) + \end{array} + \\ \qquad + \begin{array}[t]{@{}r@{~}l@{}} + (\iff & F.\AMODULE.\MIMEMS[0] = ma \\ + \wedge & F.\AMODULE.\MIDATAS[x] = da \\ + \wedge & (s + n \leq |S.\SDATA[da].\DSIINIT|) \\ + \wedge & (t + n \leq |S.\SMEMS[ma].\MIDATA|) \\ + \wedge & y = S.\SDATA[da].\DSIINIT[s \slice n]) \\ + \end{array} + \\[1ex] + \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~n)~(\I32.\CONST~t)~(\I32.\CONST~s)~(\MEMORYINIT~x) &\stepto& S; F; \TRAP + \end{array} + \end{array} + + .. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, address, table address, table instance, store, frame pair: execution; instruction single: abstract syntax; instruction diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index bc772ddc..997967db 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -371,6 +371,66 @@ New instances of :ref:`functions `, :ref:`tables ` +......................................... + +1. Let :math:`e` be the :ref:`element segment ` to allocate. + +2. If :math:`e` is of the form :math:`\{ \EINIT~x^\ast \}`, then: + + a. Let :math:`a` be the first free :ref:`element address ` in :math:`S`. + + b. For each :ref:`function index ` :math:`x_i` in :math:`e.\EINIT`, do: + + i. Let :math:`\funcaddr_i` be the :ref:`function address ` :math:`\moduleinst.\MIFUNCS[x_i]`. + + c. Let :math:`\funcaddr^\ast` be the concatenation of the function addresses :math:`\funcaddr_i`. + + d. Let :math:`\eleminst` be the :ref:`element instance ` :math:`\{ \ESIINIT~\funcaddr^\ast \}`. + + e. Append :math:`\eleminst` to the |SELEM| of :math:`S`. + +.. math:: + \begin{array}{rlll@{\qquad}l} + \allocelem(S, e, \moduleinst) &=& S', \elemaddr & (\iff e = \{ \EINIT~x^\ast \}) \\[1ex] + \allocelem(S, e, \moduleinst) &=& S & (\otherwise) \\[1ex] + \mbox{where:} \hfill \\ + \elemaddr &=& |S.\SELEM| \\ + \eleminst &=& \{ \ESIINIT~(\moduleinst.\MIFUNCS[x])^\ast \} \\ + S' &=& S \compose \{\SELEM~\eleminst\} \\ + \end{array} + + +.. index:: data, data instance, data address +.. _alloc-data: + +:ref:`Data segments ` +...................................... + +1. Let :math:`d` be the :ref:`data segment ` to allocate. + +2. If :math:`d` is of the form :math:`\{ \DINIT~b^\ast \}`, then: + + a. Let :math:`a` be the first free :ref:`data address ` in :math:`S`. + + b. Let :math:`\datainst` be the :ref:`data instance ` :math:`\{ \ESIINIT~d.\DINIT \}`. + + c. Append :math:`\datainst` to the |SDATA| of :math:`S`. + +.. math:: + \begin{array}{rlll} + \allocdata(S, d, \moduleinst) &=& S', \dataaddr & (\iff d = \{ \DINIT~b^\ast \}) \\[1ex] + \allocdata(S, d, \moduleinst) &=& S & (\otherwise) \\[1ex] + \mbox{where:} \hfill \\ + \dataaddr &=& |S.\SDATA| \\ + \datainst &=& \{ \DSIINIT~d.\DINIT \} \\ + S' &=& S \compose \{\SDATA~\datainst\} \\ + \end{array} + + .. index:: table, table instance, table address, grow, limits .. _grow-table: @@ -411,7 +471,7 @@ Growing :ref:`memories ` \end{array} -.. index:: module, module instance, function instance, table instance, memory instance, global instance, export instance, function address, table address, memory address, global address, function index, table index, memory index, global index, type, function, table, memory, global, import, export, external value, external type, matching +.. index:: module, module instance, function instance, table instance, memory instance, global instance, export instance, function address, table address, memory address, global address, element address, data addresss, function index, table index, memory index, global index, element index, data index, type, function, table, memory, global, element, data, import, export, external value, external type, matching .. _alloc-module: :ref:`Modules ` @@ -439,23 +499,35 @@ and :math:`\val^\ast` the initialization :ref:`values ` of the modul a. Let :math:`\globaladdr_i` be the :ref:`global address ` resulting from :ref:`allocating ` :math:`\global_i.\GTYPE` with initializer value :math:`\val^\ast[i]`. -6. Let :math:`\funcaddr^\ast` be the the concatenation of the :ref:`function addresses ` :math:`\funcaddr_i` in index order. +6. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEM`, do: + + a. Let :math:`\elemaddr_i` be the :ref:`element address ` resulting from :ref:`allocating ` :math:`\elem_i` for the :ref:`\module instance ` :math:`\moduleinst` defined below. + +7. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA`, do: + + a. Let :math:`\dataaddr_i` be the :ref:`data address ` resulting from :ref:`allocating ` :math:`\data_i`. -7. Let :math:`\tableaddr^\ast` be the the concatenation of the :ref:`table addresses ` :math:`\tableaddr_i` in index order. +8. Let :math:`\funcaddr^\ast` be the the concatenation of the :ref:`function addresses ` :math:`\funcaddr_i` in index order. -8. Let :math:`\memaddr^\ast` be the the concatenation of the :ref:`memory addresses ` :math:`\memaddr_i` in index order. +9. Let :math:`\tableaddr^\ast` be the the concatenation of the :ref:`table addresses ` :math:`\tableaddr_i` in index order. -9. Let :math:`\globaladdr^\ast` be the the concatenation of the :ref:`global addresses ` :math:`\globaladdr_i` in index order. +10. Let :math:`\memaddr^\ast` be the the concatenation of the :ref:`memory addresses ` :math:`\memaddr_i` in index order. -10. Let :math:`\funcaddr_{\F{mod}}^\ast` be the list of :ref:`function addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\funcaddr^\ast`. +11. Let :math:`\globaladdr^\ast` be the the concatenation of the :ref:`global addresses ` :math:`\globaladdr_i` in index order. -11. Let :math:`\tableaddr_{\F{mod}}^\ast` be the list of :ref:`table addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\tableaddr^\ast`. +12. Let :math:`\elemaddr^\ast` be the the concatenation of the :ref:`element addresses ` :math:`\elemaddr_i` in index order. -12. Let :math:`\memaddr_{\F{mod}}^\ast` be the list of :ref:`memory addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\memaddr^\ast`. +13. Let :math:`\dataaddr^\ast` be the the concatenation of the :ref:`data addresses ` :math:`\dataaddr_i` in index order. -13. Let :math:`\globaladdr_{\F{mod}}^\ast` be the list of :ref:`global addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\globaladdr^\ast`. +14. Let :math:`\funcaddr_{\F{mod}}^\ast` be the list of :ref:`function addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\funcaddr^\ast`. -14. For each :ref:`export ` :math:`\export_i` in :math:`\module.\MEXPORTS`, do: +15. Let :math:`\tableaddr_{\F{mod}}^\ast` be the list of :ref:`table addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\tableaddr^\ast`. + +16. Let :math:`\memaddr_{\F{mod}}^\ast` be the list of :ref:`memory addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\memaddr^\ast`. + +17. Let :math:`\globaladdr_{\F{mod}}^\ast` be the list of :ref:`global addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\globaladdr^\ast`. + +18. For each :ref:`export ` :math:`\export_i` in :math:`\module.\MEXPORTS`, do: a. If :math:`\export_i` is a function export for :ref:`function index ` :math:`x`, then let :math:`\externval_i` be the :ref:`external value ` :math:`\EVFUNC~(\funcaddr_{\F{mod}}^\ast[x])`. @@ -467,11 +539,11 @@ and :math:`\val^\ast` the initialization :ref:`values ` of the modul e. Let :math:`\exportinst_i` be the :ref:`export instance ` :math:`\{\EINAME~(\export_i.\ENAME), \EIVALUE~\externval_i\}`. -15. Let :math:`\exportinst^\ast` be the the concatenation of the :ref:`export instances ` :math:`\exportinst_i` in index order. +19. Let :math:`\exportinst^\ast` be the the concatenation of the :ref:`export instances ` :math:`\exportinst_i` in index order. -16. Let :math:`\moduleinst` be the :ref:`module instance ` :math:`\{\MITYPES~(\module.\MTYPES),` :math:`\MIFUNCS~\funcaddr_{\F{mod}}^\ast,` :math:`\MITABLES~\tableaddr_{\F{mod}}^\ast,` :math:`\MIMEMS~\memaddr_{\F{mod}}^\ast,` :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIEXPORTS~\exportinst^\ast\}`. +20. Let :math:`\moduleinst` be the :ref:`module instance ` :math:`\{\MITYPES~(\module.\MTYPES),` :math:`\MIFUNCS~\funcaddr_{\F{mod}}^\ast,` :math:`\MITABLES~\tableaddr_{\F{mod}}^\ast,` :math:`\MIMEMS~\memaddr_{\F{mod}}^\ast,` :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIELEMS~\elemaddr^\ast`, :math:`\MIDATAS~\dataaddr^\ast`, :math:`\MIEXPORTS~\exportinst^\ast\}`. -17. Return :math:`\moduleinst`. +21. Return :math:`\moduleinst`. .. math:: @@ -490,6 +562,8 @@ where: \MITABLES~\evtables(\externval_{\F{im}}^\ast)~\tableaddr^\ast, \\ \MIMEMS~\evmems(\externval_{\F{im}}^\ast)~\memaddr^\ast, \\ \MIGLOBALS~\evglobals(\externval_{\F{im}}^\ast)~\globaladdr^\ast, \\ + \MIELEMS~\elemaddr^\ast, \\ + \MIDATAS~\dataaddr^\ast, \\ \MIEXPORTS~\exportinst^\ast ~\} \end{array} \\[1ex] S_1, \funcaddr^\ast &=& \allocfunc^\ast(S, \module.\MFUNCS, \moduleinst) \\ @@ -497,8 +571,10 @@ where: \qquad\qquad\qquad~ (\where \table^\ast = \module.\MTABLES) \\ S_3, \memaddr^\ast &=& \allocmem^\ast(S_2, (\mem.\MTYPE)^\ast) \qquad\qquad\qquad~ (\where \mem^\ast = \module.\MMEMS) \\ - S', \globaladdr^\ast &=& \allocglobal^\ast(S_3, (\global.\GTYPE)^\ast, \val^\ast) + S_4, \globaladdr^\ast &=& \allocglobal^\ast(S_3, (\global.\GTYPE)^\ast, \val^\ast) \qquad\quad~ (\where \global^\ast = \module.\MGLOBALS) \\ + S_5, \elemaddr^\ast &=& \allocelem^\ast(S_4, \module.\MELEM, \moduleinst) \\ + S', \dataaddr^\ast &=& \allocdata^\ast(S_5, \module.\MDATA) \\ \exportinst^\ast &=& \{ \EINAME~(\export.\ENAME), \EIVALUE~\externval_{\F{ex}} \}^\ast \quad (\where \export^\ast = \module.\MEXPORTS) \\[1ex] \evfuncs(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIFUNCS[x])^\ast @@ -537,6 +613,54 @@ Moreover, if the dots :math:`\dots` are a sequence :math:`A^n` (as for globals), In an implementation, this recursion is easily unraveled by mutating one or the other in a secondary step. +.. index:: table, table instance, table address, initialize table +.. _initelem: + +:math:`\INITELEM~\tableaddr~o~x^\ast` +..................................... + +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. For each :ref:`function index ` :math:`x_i` of :math:`x^\ast`: + + a. Let :math:`\funcaddr_i` be the :ref:`function address ` :math:`F.\AMODULE.\MIFUNCS[x_i]`. + + b. Replace :math:`S.\STABLES[\tableaddr].\TIELEM[o + i]` with :math:`\funcaddr_i`. + +.. math:: + ~\\[-1ex] + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + S; F; \INITELEM~\tableaddr~o~\epsilon &\stepto& S; F; \epsilon & \\ + S; F; \INITELEM~\tableaddr~o~(x_0~x^\ast) &\stepto& S'; F; \INITELEM~\tableaddr~(o+1)~x^\ast + \end{array} + \\ \qquad + (\iff S' = S \with \STABLES[\tableaddr].\TIELEM[o] = F.\AMODULE.\MIFUNCS[x_0]) \\ + \end{array} + + +.. index:: memory, memory instance, memory address, initialize memory +.. _initdata: + +:math:`\INITDATA~\memaddr~o~b^\ast` +................................... + +1. For each byte :math:`b_i` of :math:`b^\ast`: + + a. Replace :math:`S.\SMEMS[\memaddr].\MIDATA[o + i]` with :math:`b_i`. + +.. math:: + ~\\[-1ex] + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + S; F; \INITDATA~\memaddr~o~\epsilon &\stepto& S; F; \epsilon \\ + S; F; \INITDATA~\memaddr~o~(b_0~b^\ast) &\stepto& S'; F; \INITDATA~\memaddr~(o+1)~b^\ast + \end{array} + \\ \qquad + (\iff S' = S \with \SMEMS[\memaddr].\MIDATA[o] = b_0) \\ + \end{array} + + .. index:: ! instantiation, module, instance, store, trap .. _exec-module: .. _exec-instantiation: @@ -645,19 +769,11 @@ It is up to the :ref:`embedder ` to define how such conditions are rep 13. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEM`, do: - a. For each :ref:`function index ` :math:`\funcidx_{ij}` in :math:`\elem_i.\EINIT` (starting with :math:`j = 0`), do: - - i. Assert: due to :ref:`validation `, :math:`\moduleinst.\MIFUNCS[\funcidx_{ij}]` exists. - - ii. Let :math:`\funcaddr_{ij}` be the :ref:`function address ` :math:`\moduleinst.\MIFUNCS[\funcidx_{ij}]`. - - iii. Replace :math:`\tableinst_i.\TIELEM[\X{eo}_i + j]` with :math:`\funcaddr_{ij}`. + a. :ref:`Intialize ` the table instance at :math:`\tableaddr_i` starting from offset :math:`\X{eo}_i` with the :ref:`function index ` sequence :math:`\elem_i.\EINIT`. 14. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA`, do: - a. For each :ref:`byte ` :math:`b_{ij}` in :math:`\data_i.\DINIT` (starting with :math:`j = 0`), do: - - i. Replace :math:`\meminst_i.\MIDATA[\X{do}_i + j]` with :math:`b_{ij}`. + a. :ref:`Initialize ` the memory instance at :math:`\memaddr_i` starting from offset :math:`\X{do}_i` with the :ref:`byte ` sequence :math:`\data_i.\DINIT`. 15. If the :ref:`start function ` :math:`\module.\MSTART` is not empty, then: @@ -696,18 +812,6 @@ It is up to the :ref:`embedder ` to define how such conditions are rep &\wedge& (\tableaddr = \moduleinst.\MITABLES[\elem.\ETABLE])^\ast \\ &\wedge& (\memaddr = \moduleinst.\MIMEMS[\data.\DMEM])^\ast \\ &\wedge& (\funcaddr = \moduleinst.\MIFUNCS[\start.\SFUNC])^?) - \\[2ex] - S; F; \INITELEM~a~i~\epsilon &\stepto& - S; F; \epsilon \\ - S; F; \INITELEM~a~i~(x_0~x^\ast) &\stepto& - S'; F; \INITELEM~a~(i+1)~x^\ast \\ && - (\iff S' = S \with \STABLES[a].\TIELEM[i] = F.\AMODULE.\MIFUNCS[x_0]) - \\[1ex] - S; F; \INITDATA~a~i~\epsilon &\stepto& - S; F; \epsilon \\ - S; F; \INITDATA~a~i~(b_0~b^\ast) &\stepto& - S'; F; \INITDATA~a~(i+1)~b^\ast \\ && - (\iff S' = S \with \SMEMS[a].\MIDATA[i] = b_0) \end{array} .. note:: diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index c1375fe1..6a40bc42 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -60,7 +60,7 @@ Store ~~~~~ The *store* represents all global state that can be manipulated by WebAssembly programs. -It consists of the runtime representation of all *instances* of :ref:`functions `, :ref:`tables `, :ref:`memories `, and :ref:`globals ` that have been :ref:`allocated ` during the life time of the abstract machine. [#gc]_ +It consists of the runtime representation of all *instances* of :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`globals `, :ref:`element segments `, and :ref:`data segments ` that have been :ref:`allocated ` during the life time of the abstract machine. [#gc]_ Syntactically, the store is defined as a :ref:`record ` listing the existing instances of each category: @@ -71,7 +71,9 @@ Syntactically, the store is defined as a :ref:`record ` listing \SFUNCS & \funcinst^\ast, \\ \STABLES & \tableinst^\ast, \\ \SMEMS & \meminst^\ast, \\ - \SGLOBALS & \globalinst^\ast ~\} \\ + \SGLOBALS & \globalinst^\ast, \\ + \SELEM & \eleminst^\ast, \\ + \SDATA & \datainst^\ast ~\} \\ \end{array} \end{array} @@ -87,25 +89,31 @@ Convention * The meta variable :math:`S` ranges over stores where clear from context. -.. index:: ! address, store, function instance, table instance, memory instance, global instance, embedder +.. index:: ! address, store, function instance, table instance, memory instance, global instance, element instance, data instance, embedder pair: abstract syntax; function address pair: abstract syntax; table address pair: abstract syntax; memory address pair: abstract syntax; global address + pair: abstract syntax; element address + pair: abstract syntax; data address pair: function; address pair: table; address pair: memory; address pair: global; address + pair: element; address + pair: data; address .. _syntax-funcaddr: .. _syntax-tableaddr: .. _syntax-memaddr: .. _syntax-globaladdr: +.. _syntax-elemaddr: +.. _syntax-dataaddr: .. _syntax-addr: Addresses ~~~~~~~~~ -:ref:`Function instances `, :ref:`table instances `, :ref:`memory instances `, and :ref:`global instances ` in the :ref:`store ` are referenced with abstract *addresses*. +:ref:`Function instances `, :ref:`table instances `, :ref:`memory instances `, :ref:`global instances `, :ref:`element instances `, and :ref:`data instances ` in the :ref:`store ` are referenced with abstract *addresses*. These are simply indices into the respective store component. .. math:: @@ -120,6 +128,10 @@ These are simply indices into the respective store component. \addr \\ \production{(global address)} & \globaladdr &::=& \addr \\ + \production{(element address)} & \elemaddr &::=& + \addr \\ + \production{(data address)} & \dataaddr &::=& + \addr \\ \end{array} An :ref:`embedder ` may assign identity to :ref:`exported ` store objects corresponding to their addresses, @@ -137,7 +149,7 @@ even where this identity is not observable from within WebAssembly code itself hence logical addresses can be arbitrarily large natural numbers. -.. index:: ! instance, function type, function instance, table instance, memory instance, global instance, export instance, table address, memory address, global address, index, name +.. index:: ! instance, function type, function instance, table instance, memory instance, global instance, element instance, data instance, export instance, table address, memory address, global address, element address, data address, index, name pair: abstract syntax; module instance pair: module; instance .. _syntax-moduleinst: @@ -158,6 +170,8 @@ and collects runtime representations of all entities that are imported, defined, \MITABLES & \tableaddr^\ast, \\ \MIMEMS & \memaddr^\ast, \\ \MIGLOBALS & \globaladdr^\ast, \\ + \MIELEMS & \elemaddr^\ast, \\ + \MIDATAS & \dataaddr^\ast, \\ \MIEXPORTS & \exportinst^\ast ~\} \\ \end{array} \end{array} @@ -275,6 +289,42 @@ It holds an individual :ref:`value ` and a flag indicating whether i The value of mutable globals can be mutated through :ref:`variable instructions ` or by external means provided by the :ref:`embedder `. +.. index:: ! element instance, element segment, embedder, function address + pair: abstract syntax; element instance + pair: element; instance +.. _syntax-eleminst: + +element instances +~~~~~~~~~~~~~~~~~ + +An *element instance* is the runtime representation of a :ref:`passive element segment `. +It holds a vector of :ref:`function addresses `. + +.. math:: + \begin{array}{llll} + \production{(element instance)} & \eleminst &::=& + \{ \ESIINIT~\vec(\funcaddr) \} \\ + \end{array} + + +.. index:: ! data instance, data segment, embedder, byte + pair: abstract syntax; data instance + pair: data; instance +.. _syntax-datainst: + +data instances +~~~~~~~~~~~~~~ + +An *data instance* is the runtime representation of a :ref:`passive data segment `. +It holds a vector of :ref:`bytes `. + +.. math:: + \begin{array}{llll} + \production{(data instance)} & \datainst &::=& + \{ \DSIINIT~\vec(\byte) \} \\ + \end{array} + + .. index:: ! export instance, export, name, external value pair: abstract syntax; export instance pair: export; instance diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 657ec4ce..4fd63698 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -781,6 +781,8 @@ .. |alloctable| mathdef:: \xref{exec/modules}{alloc-table}{\F{alloctable}} .. |allocmem| mathdef:: \xref{exec/modules}{alloc-mem}{\F{allocmem}} .. |allocglobal| mathdef:: \xref{exec/modules}{alloc-global}{\F{allocglobal}} +.. |allocelem| mathdef:: \xref{exec/modules}{alloc-elem}{\F{allocelem}} +.. |allocdata| mathdef:: \xref{exec/modules}{alloc-data}{\F{allocdata}} .. |allocmodule| mathdef:: \xref{exec/modules}{alloc-module}{\F{allocmodule}} .. |growtable| mathdef:: \xref{exec/modules}{grow-table}{\F{growtable}} @@ -794,6 +796,8 @@ .. |tableaddr| mathdef:: \xref{exec/runtime}{syntax-tableaddr}{\X{tableaddr}} .. |memaddr| mathdef:: \xref{exec/runtime}{syntax-memaddr}{\X{memaddr}} .. |globaladdr| mathdef:: \xref{exec/runtime}{syntax-globaladdr}{\X{globaladdr}} +.. |elemaddr| mathdef:: \xref{exec/runtime}{syntax-elemaddr}{\X{elemaddr}} +.. |dataaddr| mathdef:: \xref{exec/runtime}{syntax-dataaddr}{\X{dataaddr}} .. Instances, terminals @@ -812,6 +816,10 @@ .. |GIVALUE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{value}} .. |GIMUT| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{mut}} +.. |ESIINIT| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{init}} + +.. |DSIINIT| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{init}} + .. |EINAME| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{name}} .. |EIVALUE| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{value}} @@ -825,6 +833,8 @@ .. |MITABLES| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{tableaddrs}} .. |MIMEMS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{memaddrs}} .. |MIGLOBALS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{globaladdrs}} +.. |MIELEMS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{elemaddrs}} +.. |MIDATAS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{dataaddrs}} .. |MIEXPORTS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{exports}} @@ -838,6 +848,8 @@ .. |funcelem| mathdef:: \xref{exec/runtime}{syntax-funcelem}{\X{funcelem}} .. |meminst| mathdef:: \xref{exec/runtime}{syntax-meminst}{\X{meminst}} .. |globalinst| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\X{globalinst}} +.. |eleminst| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\X{eleminst}} +.. |datainst| mathdef:: \xref{exec/runtime}{syntax-datainst}{\X{datainst}} .. |exportinst| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\X{exportinst}} .. |hostfunc| mathdef:: \xref{exec/runtime}{syntax-hostfunc}{\X{hostfunc}} @@ -857,6 +869,8 @@ .. |STABLES| mathdef:: \xref{exec/runtime}{syntax-store}{\K{tables}} .. |SMEMS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{mems}} .. |SGLOBALS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{globals}} +.. |SELEM| mathdef:: \xref{exec/runtime}{syntax-store}{\K{elem}} +.. |SDATA| mathdef:: \xref{exec/runtime}{syntax-store}{\K{data}} .. Store, non-terminals From 6c73ce1d0a6c1cc31b7adcea36c2ded5c3fdf386 Mon Sep 17 00:00:00 2001 From: Ben Smith Date: Mon, 21 May 2018 17:56:58 -0700 Subject: [PATCH 2/8] Capitalize some headings --- document/core/exec/runtime.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 6a40bc42..6076ecd5 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -294,7 +294,7 @@ The value of mutable globals can be mutated through :ref:`variable instructions pair: element; instance .. _syntax-eleminst: -element instances +Element Instances ~~~~~~~~~~~~~~~~~ An *element instance* is the runtime representation of a :ref:`passive element segment `. @@ -312,7 +312,7 @@ It holds a vector of :ref:`function addresses `. pair: data; instance .. _syntax-datainst: -data instances +Data Instances ~~~~~~~~~~~~~~ An *data instance* is the runtime representation of a :ref:`passive data segment `. From 94e91c4448bbdcc3aff771b8dded255a2e433ae8 Mon Sep 17 00:00:00 2001 From: Ben Smith Date: Thu, 7 Jun 2018 16:40:58 -0700 Subject: [PATCH 3/8] Address some comments --- document/core/exec/instructions.rst | 28 ++++---- document/core/exec/modules.rst | 100 ++++++++++++++++------------ document/core/exec/runtime.rst | 8 +-- document/core/syntax/modules.rst | 20 ++++++ document/core/util/macros.def | 8 ++- 5 files changed, 103 insertions(+), 61 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 54934233..937a6153 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -647,44 +647,46 @@ Memory Instructions 11. Assert: due to :ref:`validation `, three values of :ref:`value type ` |I32| are on the top of the stack. -12. Pop the value :math:`\I32.\CONST~s` from the stack. +12. Pop the value :math:`\I32.\CONST~i` from the stack. -13. Pop the value :math:`\I32.\CONST~t` from the stack. +13. Pop the value :math:`\I32.\CONST~j` from the stack. 14. Pop the value :math:`\I32.\CONST~n` from the stack. -15. Let :math:`dsz` be the length of :math:`\X{data}.\DSIINIT`. +15. Let :math:`dsz` be the length of :math:`\X{data}.\DIINIT`. -16. If :math:`s + n > dsz`, then: +16. If :math:`i + n > dsz`, then: a. Trap. -17. If :math:`t + n > msz`, then: +17. If :math:`j + n > msz`, then: a. Trap. -18. Let :math:`y` be the byte sequence :math:`\X{mem}.\DSIINIT[s \slice n]`. +18. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\DIINIT[i \slice n]`. -19. :ref:`Initialize ` the memory instance at address :math:`ma` starting from offset :math:`t` with the byte sequence :math:`y`. +19. :ref:`Initialize ` the memory instance at address :math:`ma` starting from offset :math:`j` with the byte sequence :math:`b^\ast`. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~n)~(\I32.\CONST~t)~(\I32.\CONST~s)~(\MEMORYINIT~x) &\stepto& S; F; (\INITDATA~ma~t~y) + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYINIT~x) &\stepto& S; F; (\INITDATA~ma~j~b^\ast) \end{array} \\ \qquad - \begin{array}[t]{@{}r@{~}l@{}} + \begin{array}[j]{@{}r@{~}l@{}} (\iff & F.\AMODULE.\MIMEMS[0] = ma \\ \wedge & F.\AMODULE.\MIDATAS[x] = da \\ - \wedge & (s + n \leq |S.\SDATA[da].\DSIINIT|) \\ - \wedge & (t + n \leq |S.\SMEMS[ma].\MIDATA|) \\ - \wedge & y = S.\SDATA[da].\DSIINIT[s \slice n]) \\ + \wedge & (i + n \leq |S.\SDATA[da].\DIINIT|) \\ + \wedge & (j + n \leq |S.\SMEMS[ma].\MIDATA|) \\ + \wedge & b^\ast = S.\SDATA[da].\DIINIT[i \slice n]) \\ \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~n)~(\I32.\CONST~t)~(\I32.\CONST~s)~(\MEMORYINIT~x) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYINIT~x) &\stepto& S; F; \TRAP \end{array} + \\ \qquad + (\otherwise) \end{array} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 997967db..f2f7c520 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -389,18 +389,22 @@ New instances of :ref:`functions `, :ref:`tables ` :math:`\{ \ESIINIT~\funcaddr^\ast \}`. + d. Let :math:`\eleminst` be the :ref:`element instance ` :math:`\{ \EIINIT~\funcaddr^\ast \}`. e. Append :math:`\eleminst` to the |SELEM| of :math:`S`. + f. Return :math:`a`. + +3. Else, return :math:`\epsilon`. + .. math:: - \begin{array}{rlll@{\qquad}l} - \allocelem(S, e, \moduleinst) &=& S', \elemaddr & (\iff e = \{ \EINIT~x^\ast \}) \\[1ex] - \allocelem(S, e, \moduleinst) &=& S & (\otherwise) \\[1ex] + \begin{array}{rlll} + \allocelem(S, e, \moduleinst) &=& S', \elemaddr \\[1ex] \mbox{where:} \hfill \\ \elemaddr &=& |S.\SELEM| \\ - \eleminst &=& \{ \ESIINIT~(\moduleinst.\MIFUNCS[x])^\ast \} \\ + \eleminst &=& \{ \EIINIT~(\moduleinst.\MIFUNCS[x])^\ast \} \\ S' &=& S \compose \{\SELEM~\eleminst\} \\ + \allocelem(S, e, \moduleinst) &=& S, \epsilon & (\otherwise) \\[1ex] \end{array} @@ -416,18 +420,22 @@ New instances of :ref:`functions `, :ref:`tables ` in :math:`S`. - b. Let :math:`\datainst` be the :ref:`data instance ` :math:`\{ \ESIINIT~d.\DINIT \}`. + b. Let :math:`\datainst` be the :ref:`data instance ` :math:`\{ \DIINIT~d.\DINIT \}`. c. Append :math:`\datainst` to the |SDATA| of :math:`S`. + d. Return :math:`a`. + +3. Else, return :math:`\epsilon`. + .. math:: \begin{array}{rlll} - \allocdata(S, d, \moduleinst) &=& S', \dataaddr & (\iff d = \{ \DINIT~b^\ast \}) \\[1ex] - \allocdata(S, d, \moduleinst) &=& S & (\otherwise) \\[1ex] + \allocdata(S, d, \moduleinst) &=& S', \dataaddr \\[1ex] \mbox{where:} \hfill \\ \dataaddr &=& |S.\SDATA| \\ - \datainst &=& \{ \DSIINIT~d.\DINIT \} \\ + \datainst &=& \{ \DIINIT~d.\DINIT \} \\ S' &=& S \compose \{\SDATA~\datainst\} \\ + \allocdata(S, d, \moduleinst) &=& S, \epsilon & (\otherwise) \\[1ex] \end{array} @@ -501,11 +509,11 @@ and :math:`\val^\ast` the initialization :ref:`values ` of the modul 6. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEM`, do: - a. Let :math:`\elemaddr_i` be the :ref:`element address ` resulting from :ref:`allocating ` :math:`\elem_i` for the :ref:`\module instance ` :math:`\moduleinst` defined below. + a. Let :math:`\elemaddr_i^?` be the optional :ref:`element address ` resulting from :ref:`allocating ` :math:`\elem_i` for the :ref:`\module instance ` :math:`\moduleinst` defined below. 7. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA`, do: - a. Let :math:`\dataaddr_i` be the :ref:`data address ` resulting from :ref:`allocating ` :math:`\data_i`. + a. Let :math:`\dataaddr_i^?` be the optional :ref:`data address ` resulting from :ref:`allocating ` :math:`\data_i`. 8. Let :math:`\funcaddr^\ast` be the the concatenation of the :ref:`function addresses ` :math:`\funcaddr_i` in index order. @@ -515,9 +523,9 @@ and :math:`\val^\ast` the initialization :ref:`values ` of the modul 11. Let :math:`\globaladdr^\ast` be the the concatenation of the :ref:`global addresses ` :math:`\globaladdr_i` in index order. -12. Let :math:`\elemaddr^\ast` be the the concatenation of the :ref:`element addresses ` :math:`\elemaddr_i` in index order. +12. Let :math:`(\elemaddr^?)^\ast` be the the concatenation of the optional :ref:`element addresses ` :math:`\elemaddr_i^?` in index order. -13. Let :math:`\dataaddr^\ast` be the the concatenation of the :ref:`data addresses ` :math:`\dataaddr_i` in index order. +13. Let :math:`(\dataaddr^?)^\ast` be the the concatenation of the optional :ref:`data addresses ` :math:`\dataaddr_i^?` in index order. 14. Let :math:`\funcaddr_{\F{mod}}^\ast` be the list of :ref:`function addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\funcaddr^\ast`. @@ -541,7 +549,7 @@ and :math:`\val^\ast` the initialization :ref:`values ` of the modul 19. Let :math:`\exportinst^\ast` be the the concatenation of the :ref:`export instances ` :math:`\exportinst_i` in index order. -20. Let :math:`\moduleinst` be the :ref:`module instance ` :math:`\{\MITYPES~(\module.\MTYPES),` :math:`\MIFUNCS~\funcaddr_{\F{mod}}^\ast,` :math:`\MITABLES~\tableaddr_{\F{mod}}^\ast,` :math:`\MIMEMS~\memaddr_{\F{mod}}^\ast,` :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIELEMS~\elemaddr^\ast`, :math:`\MIDATAS~\dataaddr^\ast`, :math:`\MIEXPORTS~\exportinst^\ast\}`. +20. Let :math:`\moduleinst` be the :ref:`module instance ` :math:`\{\MITYPES~(\module.\MTYPES),` :math:`\MIFUNCS~\funcaddr_{\F{mod}}^\ast,` :math:`\MITABLES~\tableaddr_{\F{mod}}^\ast,` :math:`\MIMEMS~\memaddr_{\F{mod}}^\ast,` :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIELEMS~(\elemaddr^?)^\ast`, :math:`\MIDATAS~(\dataaddr^?)^\ast`, :math:`\MIEXPORTS~\exportinst^\ast\}`. 21. Return :math:`\moduleinst`. @@ -562,8 +570,8 @@ where: \MITABLES~\evtables(\externval_{\F{im}}^\ast)~\tableaddr^\ast, \\ \MIMEMS~\evmems(\externval_{\F{im}}^\ast)~\memaddr^\ast, \\ \MIGLOBALS~\evglobals(\externval_{\F{im}}^\ast)~\globaladdr^\ast, \\ - \MIELEMS~\elemaddr^\ast, \\ - \MIDATAS~\dataaddr^\ast, \\ + \MIELEMS~(\elemaddr^?)^\ast, \\ + \MIDATAS~(\dataaddr^?)^\ast, \\ \MIEXPORTS~\exportinst^\ast ~\} \end{array} \\[1ex] S_1, \funcaddr^\ast &=& \allocfunc^\ast(S, \module.\MFUNCS, \moduleinst) \\ @@ -573,8 +581,8 @@ where: \qquad\qquad\qquad~ (\where \mem^\ast = \module.\MMEMS) \\ S_4, \globaladdr^\ast &=& \allocglobal^\ast(S_3, (\global.\GTYPE)^\ast, \val^\ast) \qquad\quad~ (\where \global^\ast = \module.\MGLOBALS) \\ - S_5, \elemaddr^\ast &=& \allocelem^\ast(S_4, \module.\MELEM, \moduleinst) \\ - S', \dataaddr^\ast &=& \allocdata^\ast(S_5, \module.\MDATA) \\ + S_5, (\elemaddr^?)^\ast &=& \allocelem^\ast(S_4, \module.\MELEM, \moduleinst) \\ + S', (\dataaddr^?)^\ast &=& \allocdata^\ast(S_5, \module.\MDATA) \\ \exportinst^\ast &=& \{ \EINAME~(\export.\ENAME), \EIVALUE~\externval_{\F{ex}} \}^\ast \quad (\where \export^\ast = \module.\MEXPORTS) \\[1ex] \evfuncs(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIFUNCS[x])^\ast @@ -721,47 +729,51 @@ It is up to the :ref:`embedder ` to define how such conditions are rep 9. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEM`, do: - a. Let :math:`\X{eoval}_i` be the result of :ref:`evaluating ` the expression :math:`\elem_i.\EOFFSET`. + a. If :math:`\elem_i` is :ref:`active `, then: - b. Assert: due to :ref:`validation `, :math:`\X{eoval}_i` is of the form :math:`\I32.\CONST~\X{eo}_i`. + i. Let :math:`\X{eoval}_i` be the result of :ref:`evaluating ` the expression :math:`\elem_i.\EOFFSET`. - c. Let :math:`\tableidx_i` be the :ref:`table index ` :math:`\elem_i.\ETABLE`. + ii. Assert: due to :ref:`validation `, :math:`\X{eoval}_i` is of the form :math:`\I32.\CONST~\X{eo}_i`. - d. Assert: due to :ref:`validation `, :math:`\moduleinst.\MITABLES[\tableidx_i]` exists. + iii. Let :math:`\tableidx_i` be the :ref:`table index ` :math:`\elem_i.\ETABLE`. - e. Let :math:`\tableaddr_i` be the :ref:`table address ` :math:`\moduleinst.\MITABLES[\tableidx_i]`. + iv. Assert: due to :ref:`validation `, :math:`\moduleinst.\MITABLES[\tableidx_i]` exists. - f. Assert: due to :ref:`validation `, :math:`S'.\STABLES[\tableaddr_i]` exists. + v. Let :math:`\tableaddr_i` be the :ref:`table address ` :math:`\moduleinst.\MITABLES[\tableidx_i]`. - g. Let :math:`\tableinst_i` be the :ref:`table instance ` :math:`S'.\STABLES[\tableaddr_i]`. + vi. Assert: due to :ref:`validation `, :math:`S'.\STABLES[\tableaddr_i]` exists. - h. Let :math:`\X{eend}_i` be :math:`\X{eo}_i` plus the length of :math:`\elem_i.\EINIT`. + vii. Let :math:`\tableinst_i` be the :ref:`table instance ` :math:`S'.\STABLES[\tableaddr_i]`. - i. If :math:`\X{eend}_i` is larger than the length of :math:`\tableinst_i.\TIELEM`, then: + viii. Let :math:`\X{eend}_i` be :math:`\X{eo}_i` plus the length of :math:`\elem_i.\EINIT`. - i. Fail. + ix. If :math:`\X{eend}_i` is larger than the length of :math:`\tableinst_i.\TIELEM`, then: + + 1. Fail. 10. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA`, do: - a. Let :math:`\X{doval}_i` be the result of :ref:`evaluating ` the expression :math:`\data_i.\DOFFSET`. + a. If :math:`\data_i` is :ref:`active `, then: + + i. Let :math:`\X{doval}_i` be the result of :ref:`evaluating ` the expression :math:`\data_i.\DOFFSET`. - b. Assert: due to :ref:`validation `, :math:`\X{doval}_i` is of the form :math:`\I32.\CONST~\X{do}_i`. + ii. Assert: due to :ref:`validation `, :math:`\X{doval}_i` is of the form :math:`\I32.\CONST~\X{do}_i`. - c. Let :math:`\memidx_i` be the :ref:`memory index ` :math:`\data_i.\DMEM`. + iii. Let :math:`\memidx_i` be the :ref:`memory index ` :math:`\data_i.\DMEM`. - d. Assert: due to :ref:`validation `, :math:`\moduleinst.\MIMEMS[\memidx_i]` exists. + iv. Assert: due to :ref:`validation `, :math:`\moduleinst.\MIMEMS[\memidx_i]` exists. - e. Let :math:`\memaddr_i` be the :ref:`memory address ` :math:`\moduleinst.\MIMEMS[\memidx_i]`. + v. Let :math:`\memaddr_i` be the :ref:`memory address ` :math:`\moduleinst.\MIMEMS[\memidx_i]`. - f. Assert: due to :ref:`validation `, :math:`S'.\SMEMS[\memaddr_i]` exists. + vi. Assert: due to :ref:`validation `, :math:`S'.\SMEMS[\memaddr_i]` exists. - g. Let :math:`\meminst_i` be the :ref:`memory instance ` :math:`S'.\SMEMS[\memaddr_i]`. + vii. Let :math:`\meminst_i` be the :ref:`memory instance ` :math:`S'.\SMEMS[\memaddr_i]`. - h. Let :math:`\X{dend}_i` be :math:`\X{do}_i` plus the length of :math:`\data_i.\DINIT`. + viii. Let :math:`\X{dend}_i` be :math:`\X{do}_i` plus the length of :math:`\data_i.\DINIT`. - i. If :math:`\X{dend}_i` is larger than the length of :math:`\meminst_i.\MIDATA`, then: + ix. If :math:`\X{dend}_i` is larger than the length of :math:`\meminst_i.\MIDATA`, then: - i. Fail. + 1. Fail. 11. Assert: due to :ref:`validation `, the frame :math:`F` is now on the top of the stack. @@ -769,11 +781,15 @@ It is up to the :ref:`embedder ` to define how such conditions are rep 13. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEM`, do: - a. :ref:`Intialize ` the table instance at :math:`\tableaddr_i` starting from offset :math:`\X{eo}_i` with the :ref:`function index ` sequence :math:`\elem_i.\EINIT`. + a. If :math:`\elem_i` is :ref:`active `, then: + + i. :ref:`Intialize ` the table instance at :math:`\tableaddr_i` starting from offset :math:`\X{eo}_i` with the :ref:`function index ` sequence :math:`\elem_i.\EINIT`. 14. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA`, do: - a. :ref:`Initialize ` the memory instance at :math:`\memaddr_i` starting from offset :math:`\X{do}_i` with the :ref:`byte ` sequence :math:`\data_i.\DINIT`. + a. If :math:`\data_i` :ref:`active `, then: + + i. :ref:`Initialize ` the memory instance at :math:`\memaddr_i` starting from offset :math:`\X{do}_i` with the :ref:`byte ` sequence :math:`\data_i.\DINIT`. 15. If the :ref:`start function ` :math:`\module.\MSTART` is not empty, then: @@ -798,8 +814,8 @@ It is up to the :ref:`embedder ` to define how such conditions are rep &\wedge& (S \vdashexternval \externval : \externtype)^n \\ &\wedge& (\vdashexterntypematch \externtype \matches \externtype_{\F{im}})^n \\[1ex] &\wedge& \module.\MGLOBALS = \global^\ast \\ - &\wedge& \module.\MELEM = \elem^\ast \\ - &\wedge& \module.\MDATA = \data^\ast \\ + &\wedge& \eactive(\module.\MELEM) = \elem^\ast \\ + &\wedge& \dactive(\module.\MDATA) = \data^\ast \\ &\wedge& \module.\MSTART = \start^? \\[1ex] &\wedge& S', \moduleinst = \allocmodule(S, \module, \externval^n, \val^\ast) \\ &\wedge& F = \{ \AMODULE~\moduleinst, \ALOCALS~\epsilon \} \\[1ex] diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 6076ecd5..ed49b1b6 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -170,8 +170,8 @@ and collects runtime representations of all entities that are imported, defined, \MITABLES & \tableaddr^\ast, \\ \MIMEMS & \memaddr^\ast, \\ \MIGLOBALS & \globaladdr^\ast, \\ - \MIELEMS & \elemaddr^\ast, \\ - \MIDATAS & \dataaddr^\ast, \\ + \MIELEMS & (\elemaddr^?)^\ast, \\ + \MIDATAS & (\dataaddr^?)^\ast, \\ \MIEXPORTS & \exportinst^\ast ~\} \\ \end{array} \end{array} @@ -303,7 +303,7 @@ It holds a vector of :ref:`function addresses `. .. math:: \begin{array}{llll} \production{(element instance)} & \eleminst &::=& - \{ \ESIINIT~\vec(\funcaddr) \} \\ + \{ \EIINIT~\vec(\funcaddr) \} \\ \end{array} @@ -321,7 +321,7 @@ It holds a vector of :ref:`bytes `. .. math:: \begin{array}{llll} \production{(data instance)} & \datainst &::=& - \{ \DSIINIT~\vec(\byte) \} \\ + \{ \DIINIT~\vec(\byte) \} \\ \end{array} diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst index fad27960..80fe2523 100644 --- a/document/core/syntax/modules.rst +++ b/document/core/syntax/modules.rst @@ -259,6 +259,16 @@ Element segments are referenced through :ref:`element indices `. Consequently, the only valid |tableidx| is :math:`0`. +Conventions +........... + +The following auxiliary notation is defined for sequences of element segments, filtering out items of a specific kind in an order-preserving fashion: + +* :math:`\eactive(\elem^\ast) = [\elem ~|~ \{ \ETABLE~\tableidx, \EOFFSET~\expr, \EINIT~\vec(\funcidx) \} \in \elem^\ast]` + +* :math:`\epassive(\elem^\ast) = [\elem ~|~ \{ \EINIT~\vec(\funcidx) \} \in \elem^\ast]` + + .. index:: ! data, active, passive, data index, memory, memory index, expression, constant, byte, vector pair: abstract syntax; data single: memory; data @@ -290,6 +300,16 @@ Data segments are referenced through :ref:`data indices `. Consequently, the only valid |memidx| is :math:`0`. +Conventions +........... + +The following auxiliary notation is defined for sequences of data segments, filtering out items of a specific kind in an order-preserving fashion: + +* :math:`\dactive(\data^\ast) = [\data ~|~ \{ \DMEM~\memidx, \DOFFSET~\expr, \DINIT~\vec(\byte) \} \in \data^\ast]` + +* :math:`\dpassive(\data^\ast) = [\data ~|~ \{ \DINIT~\vec(\byte) \} \in \data^\ast]` + + .. index:: ! start function, function, function index, table, memory, instantiation pair: abstract syntax; start function .. _syntax-start: diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 4fd63698..45c8d5fd 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -295,6 +295,10 @@ .. Modules, meta functions +.. |eactive| mathdef:: \xref{syntax/modules}{syntax-elem}{\F{active}} +.. |epassive| mathdef:: \xref{syntax/modules}{syntax-elem}{\F{passive}} +.. |dactive| mathdef:: \xref{syntax/modules}{syntax-data}{\F{active}} +.. |dpassive| mathdef:: \xref{syntax/modules}{syntax-data}{\F{passive}} .. |edfuncs| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{funcs}} .. |edtables| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{tables}} .. |edmems| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{mems}} @@ -816,9 +820,9 @@ .. |GIVALUE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{value}} .. |GIMUT| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{mut}} -.. |ESIINIT| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{init}} +.. |EIINIT| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{init}} -.. |DSIINIT| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{init}} +.. |DIINIT| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{init}} .. |EINAME| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{name}} .. |EIVALUE| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{value}} From 9bbfe24743077fc5767a1f360bdcf70b82ba11f1 Mon Sep 17 00:00:00 2001 From: Ben Smith Date: Tue, 12 Jun 2018 17:14:55 -0700 Subject: [PATCH 4/8] Add memory.{drop,copy} exec --- document/core/exec/instructions.rst | 98 ++++++++++++++++++++++++++++- 1 file changed, 97 insertions(+), 1 deletion(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 937a6153..8c576a02 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -663,7 +663,7 @@ Memory Instructions a. Trap. -18. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\DIINIT[i \slice n]`. +18. Let :math:`b^\ast` be the byte sequence :math:`\X{data}.\DIINIT[i \slice n]`. 19. :ref:`Initialize ` the memory instance at address :math:`ma` starting from offset :math:`j` with the byte sequence :math:`b^\ast`. @@ -677,6 +677,7 @@ Memory Instructions \begin{array}[j]{@{}r@{~}l@{}} (\iff & F.\AMODULE.\MIMEMS[0] = ma \\ \wedge & F.\AMODULE.\MIDATAS[x] = da \\ + \wedge & S.\SDATA[da] \neq \epsilon \\ \wedge & (i + n \leq |S.\SDATA[da].\DIINIT|) \\ \wedge & (j + n \leq |S.\SMEMS[ma].\MIDATA|) \\ \wedge & b^\ast = S.\SDATA[da].\DIINIT[i \slice n]) \\ @@ -690,6 +691,101 @@ Memory Instructions \end{array} +.. _exec-memory.drop: + +:math:`\MEMORYDROP~x` +..................... + +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIMEMS[0]` exists. + +3. Let :math:`ma` be the :ref:`memory address ` :math:`F.\AMODULE.\MIMEMS[0]`. + +4. Assert: due to :ref:`validation `, :math:`S.\SMEMS[ma]` exists. + +5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[ma]`. + +6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIDATAS[x]` exists. + +7. Let :math:`da` be the :ref:`data segment address ` :math:`F.\AMODULE.\MIDATAS[x]`. + +8. Replace :math:`S.\SDATA[da]` with :math:`\epsilon`. + +.. math:: + ~\\[-1ex] + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + S; F; (\MEMORYDROP~x) &\stepto& S'; F; \epsilon + \end{array} + \\ \qquad + \begin{array}[j]{@{}r@{~}l@{}} + (\iff & F.\AMODULE.\MIMEMS[0] = ma \\ + \wedge & F.\AMODULE.\MIDATAS[x] = da \\ + \wedge & S' = S \with \SDATA[da] = \epsilon) \\ + \end{array} + \end{array} + + +.. _exec-memory.copy: + +:math:`\MEMORYCOPY` +................... + +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIMEMS[0]` exists. + +3. Let :math:`ma` be the :ref:`memory address ` :math:`F.\AMODULE.\MIMEMS[0]`. + +4. Assert: due to :ref:`validation `, :math:`S.\SMEMS[ma]` exists. + +5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[ma]`. + +6. Let :math:`sz` be the length of :math:`\X{mem}.\MIDATA`. + +7. Assert: due to :ref:`validation `, three values of :ref:`value type ` |I32| are on the top of the stack. + +8. Pop the value :math:`\I32.\CONST~i` from the stack. + +9. Pop the value :math:`\I32.\CONST~j` from the stack. + +10. Pop the value :math:`\I32.\CONST~n` from the stack. + +11. If :math:`i + n > sz`, then: + + a. Trap. + +12. If :math:`j + n > sz`, then: + + a. Trap. + +13. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[i \slice n]`. + +14. :ref:`Initialize ` the memory instance at address :math:`ma` starting from offset :math:`j` with the byte sequence :math:`b^\ast`. + +.. math:: + ~\\[-1ex] + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYCOPY~x) &\stepto& S; F; (\INITDATA~ma~j~b^\ast) + \end{array} + \\ \qquad + \begin{array}[j]{@{}r@{~}l@{}} + (\iff & F.\AMODULE.\MIMEMS[0] = ma \\ + \wedge & (i + n \leq |S.\SMEMS[ma].\MIDATA|) \\ + \wedge & (j + n \leq |S.\SMEMS[ma].\MIDATA|) \\ + \wedge & b^\ast = S.\SMEMS[ma].\MIDATA[i \slice n]) \\ + \end{array} + \\[1ex] + \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYCOPY~x) &\stepto& S; F; \TRAP + \end{array} + \\ \qquad + (\otherwise) + \end{array} + + .. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, address, table address, table instance, store, frame pair: execution; instruction single: abstract syntax; instruction From af0622b4f9567308be84016cd53ba7ce22fcd5d3 Mon Sep 17 00:00:00 2001 From: Ben Smith Date: Tue, 19 Jun 2018 17:02:04 -0700 Subject: [PATCH 5/8] Add Table instructions --- document/core/exec/instructions.rst | 171 ++++++++++++++++++++++++++++ 1 file changed, 171 insertions(+) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 8c576a02..8d38e238 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -786,6 +786,177 @@ Memory Instructions \end{array} +Table Instructions +~~~~~~~~~~~~~~~~~~ + +.. _exec-table.init: + +:math:`\TABLEINIT` +.................. + +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[0]` exists. + +3. Let :math:`ta` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[0]`. + +4. Assert: due to :ref:`validation `, :math:`S.\STABLES[ta]` exists. + +5. Let :math:`\X{table}` be the :ref:`table instance ` :math:`S.\STABLES[ta]`. + +6. Let :math:`tsz` be the length of :math:`\X{table}.\MIELEMS`. + +7. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[x]` exists. + +8. Let :math:`ea` be the :ref:`element segment address ` :math:`F.\AMODULE.\MIELEMS[x]`. + +9. If :math:`S.\SELEM[ea]` does not exist, then: + + a. Trap. + +10. Let :math:`\X{elem}` be the :ref:`element segment instance ` :math:`S.\SELEM[ea]`. + +11. Assert: due to :ref:`validation `, three values of :ref:`value type ` |I32| are on the top of the stack. + +12. Pop the value :math:`\I32.\CONST~i` from the stack. + +13. Pop the value :math:`\I32.\CONST~j` from the stack. + +14. Pop the value :math:`\I32.\CONST~n` from the stack. + +15. Let :math:`esz` be the length of :math:`\X{elem}.\EIINIT`. + +16. If :math:`i + n > esz`, then: + + a. Trap. + +17. If :math:`j + n > tsz`, then: + + a. Trap. + +18. Let :math:`y^\ast` be the function address sequence :math:`\X{elem}.\EIINIT[i \slice n]`. + +19. :ref:`Initialize ` the table instance at address :math:`ta` starting from offset :math:`j` with the function address sequence :math:`y^\ast`. + +.. math:: + ~\\[-1ex] + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLEINIT~x) &\stepto& S; F; (\INITELEM~ta~j~y^\ast) + \end{array} + \\ \qquad + \begin{array}[j]{@{}r@{~}l@{}} + (\iff & F.\AMODULE.\MITABLES[0] = ta \\ + \wedge & F.\AMODULE.\MIELEMS[x] = ea \\ + \wedge & S.\SELEM[ea] \neq \epsilon \\ + \wedge & (i + n \leq |S.\SELEM[ea].\EIINIT|) \\ + \wedge & (j + n \leq |S.\STABLES[ta].\MIELEMS|) \\ + \wedge & y^\ast = S.\SELEM[ea].\EIINIT[i \slice n]) \\ + \end{array} + \\[1ex] + \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLEINIT~x) &\stepto& S; F; \TRAP + \end{array} + \\ \qquad + (\otherwise) + \end{array} + + +.. _exec-table.drop: + +:math:`\TABLEDROP~x` +..................... + +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[0]` exists. + +3. Let :math:`ta` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[0]`. + +4. Assert: due to :ref:`validation `, :math:`S.\STABLES[ta]` exists. + +5. Let :math:`\X{table}` be the :ref:`table instance ` :math:`S.\STABLES[ta]`. + +6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[x]` exists. + +7. Let :math:`ea` be the :ref:`element segment address ` :math:`F.\AMODULE.\MIELEMS[x]`. + +8. Replace :math:`S.\SELEM[ea]` with :math:`\epsilon`. + +.. math:: + ~\\[-1ex] + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + S; F; (\TABLEDROP~x) &\stepto& S'; F; \epsilon + \end{array} + \\ \qquad + \begin{array}[j]{@{}r@{~}l@{}} + (\iff & F.\AMODULE.\MITABLES[0] = ta \\ + \wedge & F.\AMODULE.\MIELEMS[x] = ea \\ + \wedge & S' = S \with \SELEM[ea] = \epsilon) \\ + \end{array} + \end{array} + + +.. _exec-table.copy: + +:math:`\TABLECOPY` +................... + +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[0]` exists. + +3. Let :math:`ta` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[0]`. + +4. Assert: due to :ref:`validation `, :math:`S.\STABLES[ta]` exists. + +5. Let :math:`\X{table}` be the :ref:`table instance ` :math:`S.\STABLES[ta]`. + +6. Let :math:`sz` be the length of :math:`\X{table}.\MIELEMS`. + +7. Assert: due to :ref:`validation `, three values of :ref:`value type ` |I32| are on the top of the stack. + +8. Pop the value :math:`\I32.\CONST~i` from the stack. + +9. Pop the value :math:`\I32.\CONST~j` from the stack. + +10. Pop the value :math:`\I32.\CONST~n` from the stack. + +11. If :math:`i + n > sz`, then: + + a. Trap. + +12. If :math:`j + n > sz`, then: + + a. Trap. + +13. Let :math:`y^\ast` be the function address sequence :math:`\X{table}.\MIELEMS[i \slice n]`. + +14. :ref:`Initialize ` the table instance at address :math:`ta` starting from offset :math:`j` with the function address sequence :math:`y^\ast`. + +.. math:: + ~\\[-1ex] + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLECOPY~x) &\stepto& S; F; (\INITELEM~ta~j~y^\ast) + \end{array} + \\ \qquad + \begin{array}[j]{@{}r@{~}l@{}} + (\iff & F.\AMODULE.\MITABLES[0] = ta \\ + \wedge & (i + n \leq |S.\STABLES[ta].\MIELEMS|) \\ + \wedge & (j + n \leq |S.\STABLES[ta].\MIELEMS|) \\ + \wedge & y^\ast = S.\STABLES[ta].\MIELEMS[i \slice n]) \\ + \end{array} + \\[1ex] + \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLECOPY~x) &\stepto& S; F; \TRAP + \end{array} + \\ \qquad + (\otherwise) + \end{array} + + .. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, address, table address, table instance, store, frame pair: execution; instruction single: abstract syntax; instruction From 4fd2b5b8aa3e00adafcd82b2de6d184da43d68c3 Mon Sep 17 00:00:00 2001 From: Ben Smith Date: Tue, 19 Jun 2018 17:19:50 -0700 Subject: [PATCH 6/8] Init all segments, move initdata/initelem into instructions section --- document/core/exec/instructions.rst | 48 ++++++++++++++ document/core/exec/modules.rst | 98 ++++++----------------------- 2 files changed, 68 insertions(+), 78 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 8d38e238..ecf58ccc 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -786,6 +786,28 @@ Memory Instructions \end{array} +.. index:: memory, memory instance, memory address, initialize memory +.. _initdata: + +:math:`\INITDATA~\memaddr~o~b^\ast` +................................... + +1. For each byte :math:`b_i` of :math:`b^\ast`: + + a. Replace :math:`S.\SMEMS[\memaddr].\MIDATA[o + i]` with :math:`b_i`. + +.. math:: + ~\\[-1ex] + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + S; F; \INITDATA~\memaddr~o~\epsilon &\stepto& S; F; \epsilon \\ + S; F; \INITDATA~\memaddr~o~(b_0~b^\ast) &\stepto& S'; F; \INITDATA~\memaddr~(o+1)~b^\ast + \end{array} + \\ \qquad + (\iff S' = S \with \SMEMS[\memaddr].\MIDATA[o] = b_0) \\ + \end{array} + + Table Instructions ~~~~~~~~~~~~~~~~~~ @@ -957,6 +979,32 @@ Table Instructions \end{array} +.. index:: table, table instance, table address, initialize table +.. _initelem: + +:math:`\INITELEM~\tableaddr~o~x^\ast` +..................................... + +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. For each :ref:`function index ` :math:`x_i` of :math:`x^\ast`: + + a. Let :math:`\funcaddr_i` be the :ref:`function address ` :math:`F.\AMODULE.\MIFUNCS[x_i]`. + + b. Replace :math:`S.\STABLES[\tableaddr].\TIELEM[o + i]` with :math:`\funcaddr_i`. + +.. math:: + ~\\[-1ex] + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + S; F; \INITELEM~\tableaddr~o~\epsilon &\stepto& S; F; \epsilon & \\ + S; F; \INITELEM~\tableaddr~o~(x_0~x^\ast) &\stepto& S'; F; \INITELEM~\tableaddr~(o+1)~x^\ast + \end{array} + \\ \qquad + (\iff S' = S \with \STABLES[\tableaddr].\TIELEM[o] = F.\AMODULE.\MIFUNCS[x_0]) \\ + \end{array} + + .. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, address, table address, table instance, store, frame pair: execution; instruction single: abstract syntax; instruction diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index f2f7c520..ca75becf 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -379,23 +379,19 @@ New instances of :ref:`functions `, :ref:`tables ` to allocate. -2. If :math:`e` is of the form :math:`\{ \EINIT~x^\ast \}`, then: +2. Let :math:`a` be the first free :ref:`element address ` in :math:`S`. - a. Let :math:`a` be the first free :ref:`element address ` in :math:`S`. +3. For each :ref:`function index ` :math:`x_i` in :math:`e.\EINIT`, do: - b. For each :ref:`function index ` :math:`x_i` in :math:`e.\EINIT`, do: + a. Let :math:`\funcaddr_i` be the :ref:`function address ` :math:`\moduleinst.\MIFUNCS[x_i]`. - i. Let :math:`\funcaddr_i` be the :ref:`function address ` :math:`\moduleinst.\MIFUNCS[x_i]`. +4. Let :math:`\funcaddr^\ast` be the concatenation of the function addresses :math:`\funcaddr_i`. - c. Let :math:`\funcaddr^\ast` be the concatenation of the function addresses :math:`\funcaddr_i`. +5. Let :math:`\eleminst` be the :ref:`element instance ` :math:`\{ \EIINIT~\funcaddr^\ast \}`. - d. Let :math:`\eleminst` be the :ref:`element instance ` :math:`\{ \EIINIT~\funcaddr^\ast \}`. +6. Append :math:`\eleminst` to the |SELEM| of :math:`S`. - e. Append :math:`\eleminst` to the |SELEM| of :math:`S`. - - f. Return :math:`a`. - -3. Else, return :math:`\epsilon`. +7. Return :math:`a`. .. math:: \begin{array}{rlll} @@ -404,7 +400,6 @@ New instances of :ref:`functions `, :ref:`tables `, :ref:`tables ` to allocate. -2. If :math:`d` is of the form :math:`\{ \DINIT~b^\ast \}`, then: - - a. Let :math:`a` be the first free :ref:`data address ` in :math:`S`. - - b. Let :math:`\datainst` be the :ref:`data instance ` :math:`\{ \DIINIT~d.\DINIT \}`. +2. Let :math:`a` be the first free :ref:`data address ` in :math:`S`. - c. Append :math:`\datainst` to the |SDATA| of :math:`S`. +3. Let :math:`\datainst` be the :ref:`data instance ` :math:`\{ \DIINIT~d.\DINIT \}`. - d. Return :math:`a`. +4. Append :math:`\datainst` to the |SDATA| of :math:`S`. -3. Else, return :math:`\epsilon`. +5. Return :math:`a`. .. math:: \begin{array}{rlll} @@ -435,7 +426,6 @@ New instances of :ref:`functions `, :ref:`tables ` of the modul 6. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEM`, do: - a. Let :math:`\elemaddr_i^?` be the optional :ref:`element address ` resulting from :ref:`allocating ` :math:`\elem_i` for the :ref:`\module instance ` :math:`\moduleinst` defined below. + a. Let :math:`\elemaddr_i` be the :ref:`element address ` resulting from :ref:`allocating ` :math:`\elem_i` for the :ref:`\module instance ` :math:`\moduleinst` defined below. 7. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA`, do: - a. Let :math:`\dataaddr_i^?` be the optional :ref:`data address ` resulting from :ref:`allocating ` :math:`\data_i`. + a. Let :math:`\dataaddr_i` be the :ref:`data address ` resulting from :ref:`allocating ` :math:`\data_i`. 8. Let :math:`\funcaddr^\ast` be the the concatenation of the :ref:`function addresses ` :math:`\funcaddr_i` in index order. @@ -523,9 +513,9 @@ and :math:`\val^\ast` the initialization :ref:`values ` of the modul 11. Let :math:`\globaladdr^\ast` be the the concatenation of the :ref:`global addresses ` :math:`\globaladdr_i` in index order. -12. Let :math:`(\elemaddr^?)^\ast` be the the concatenation of the optional :ref:`element addresses ` :math:`\elemaddr_i^?` in index order. +12. Let :math:`\elemaddr^\ast` be the the concatenation of the :ref:`element addresses ` :math:`\elemaddr_i` in index order. -13. Let :math:`(\dataaddr^?)^\ast` be the the concatenation of the optional :ref:`data addresses ` :math:`\dataaddr_i^?` in index order. +13. Let :math:`\dataaddr^\ast` be the the concatenation of the :ref:`data addresses ` :math:`\dataaddr_i` in index order. 14. Let :math:`\funcaddr_{\F{mod}}^\ast` be the list of :ref:`function addresses ` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\funcaddr^\ast`. @@ -549,7 +539,7 @@ and :math:`\val^\ast` the initialization :ref:`values ` of the modul 19. Let :math:`\exportinst^\ast` be the the concatenation of the :ref:`export instances ` :math:`\exportinst_i` in index order. -20. Let :math:`\moduleinst` be the :ref:`module instance ` :math:`\{\MITYPES~(\module.\MTYPES),` :math:`\MIFUNCS~\funcaddr_{\F{mod}}^\ast,` :math:`\MITABLES~\tableaddr_{\F{mod}}^\ast,` :math:`\MIMEMS~\memaddr_{\F{mod}}^\ast,` :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIELEMS~(\elemaddr^?)^\ast`, :math:`\MIDATAS~(\dataaddr^?)^\ast`, :math:`\MIEXPORTS~\exportinst^\ast\}`. +20. Let :math:`\moduleinst` be the :ref:`module instance ` :math:`\{\MITYPES~(\module.\MTYPES),` :math:`\MIFUNCS~\funcaddr_{\F{mod}}^\ast,` :math:`\MITABLES~\tableaddr_{\F{mod}}^\ast,` :math:`\MIMEMS~\memaddr_{\F{mod}}^\ast,` :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIELEMS~\elemaddr^\ast`, :math:`\MIDATAS~\dataaddr^\ast`, :math:`\MIEXPORTS~\exportinst^\ast\}`. 21. Return :math:`\moduleinst`. @@ -570,8 +560,8 @@ where: \MITABLES~\evtables(\externval_{\F{im}}^\ast)~\tableaddr^\ast, \\ \MIMEMS~\evmems(\externval_{\F{im}}^\ast)~\memaddr^\ast, \\ \MIGLOBALS~\evglobals(\externval_{\F{im}}^\ast)~\globaladdr^\ast, \\ - \MIELEMS~(\elemaddr^?)^\ast, \\ - \MIDATAS~(\dataaddr^?)^\ast, \\ + \MIELEMS~\elemaddr^\ast, \\ + \MIDATAS~\dataaddr^\ast, \\ \MIEXPORTS~\exportinst^\ast ~\} \end{array} \\[1ex] S_1, \funcaddr^\ast &=& \allocfunc^\ast(S, \module.\MFUNCS, \moduleinst) \\ @@ -581,8 +571,8 @@ where: \qquad\qquad\qquad~ (\where \mem^\ast = \module.\MMEMS) \\ S_4, \globaladdr^\ast &=& \allocglobal^\ast(S_3, (\global.\GTYPE)^\ast, \val^\ast) \qquad\quad~ (\where \global^\ast = \module.\MGLOBALS) \\ - S_5, (\elemaddr^?)^\ast &=& \allocelem^\ast(S_4, \module.\MELEM, \moduleinst) \\ - S', (\dataaddr^?)^\ast &=& \allocdata^\ast(S_5, \module.\MDATA) \\ + S_5, \elemaddr^\ast &=& \allocelem^\ast(S_4, \module.\MELEM, \moduleinst) \\ + S', \dataaddr^\ast &=& \allocdata^\ast(S_5, \module.\MDATA) \\ \exportinst^\ast &=& \{ \EINAME~(\export.\ENAME), \EIVALUE~\externval_{\F{ex}} \}^\ast \quad (\where \export^\ast = \module.\MEXPORTS) \\[1ex] \evfuncs(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIFUNCS[x])^\ast @@ -621,54 +611,6 @@ Moreover, if the dots :math:`\dots` are a sequence :math:`A^n` (as for globals), In an implementation, this recursion is easily unraveled by mutating one or the other in a secondary step. -.. index:: table, table instance, table address, initialize table -.. _initelem: - -:math:`\INITELEM~\tableaddr~o~x^\ast` -..................................... - -1. Let :math:`F` be the :ref:`current ` :ref:`frame `. - -2. For each :ref:`function index ` :math:`x_i` of :math:`x^\ast`: - - a. Let :math:`\funcaddr_i` be the :ref:`function address ` :math:`F.\AMODULE.\MIFUNCS[x_i]`. - - b. Replace :math:`S.\STABLES[\tableaddr].\TIELEM[o + i]` with :math:`\funcaddr_i`. - -.. math:: - ~\\[-1ex] - \begin{array}{l} - \begin{array}{lcl@{\qquad}l} - S; F; \INITELEM~\tableaddr~o~\epsilon &\stepto& S; F; \epsilon & \\ - S; F; \INITELEM~\tableaddr~o~(x_0~x^\ast) &\stepto& S'; F; \INITELEM~\tableaddr~(o+1)~x^\ast - \end{array} - \\ \qquad - (\iff S' = S \with \STABLES[\tableaddr].\TIELEM[o] = F.\AMODULE.\MIFUNCS[x_0]) \\ - \end{array} - - -.. index:: memory, memory instance, memory address, initialize memory -.. _initdata: - -:math:`\INITDATA~\memaddr~o~b^\ast` -................................... - -1. For each byte :math:`b_i` of :math:`b^\ast`: - - a. Replace :math:`S.\SMEMS[\memaddr].\MIDATA[o + i]` with :math:`b_i`. - -.. math:: - ~\\[-1ex] - \begin{array}{l} - \begin{array}{lcl@{\qquad}l} - S; F; \INITDATA~\memaddr~o~\epsilon &\stepto& S; F; \epsilon \\ - S; F; \INITDATA~\memaddr~o~(b_0~b^\ast) &\stepto& S'; F; \INITDATA~\memaddr~(o+1)~b^\ast - \end{array} - \\ \qquad - (\iff S' = S \with \SMEMS[\memaddr].\MIDATA[o] = b_0) \\ - \end{array} - - .. index:: ! instantiation, module, instance, store, trap .. _exec-module: .. _exec-instantiation: From 526575e9a94b98279050b5687c1f6c72d7333ff8 Mon Sep 17 00:00:00 2001 From: Ben Smith Date: Tue, 19 Jun 2018 17:48:37 -0700 Subject: [PATCH 7/8] Some instruction fixes --- document/core/exec/instructions.rst | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ecf58ccc..5d7542ea 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -813,7 +813,7 @@ Table Instructions .. _exec-table.init: -:math:`\TABLEINIT` +:math:`\TABLEINIT~x` .................. 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. @@ -826,7 +826,7 @@ Table Instructions 5. Let :math:`\X{table}` be the :ref:`table instance ` :math:`S.\STABLES[ta]`. -6. Let :math:`tsz` be the length of :math:`\X{table}.\MIELEMS`. +6. Let :math:`tsz` be the length of :math:`\X{table}.\TIELEM`. 7. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[x]` exists. @@ -872,7 +872,7 @@ Table Instructions \wedge & F.\AMODULE.\MIELEMS[x] = ea \\ \wedge & S.\SELEM[ea] \neq \epsilon \\ \wedge & (i + n \leq |S.\SELEM[ea].\EIINIT|) \\ - \wedge & (j + n \leq |S.\STABLES[ta].\MIELEMS|) \\ + \wedge & (j + n \leq |S.\STABLES[ta].\TIELEM|) \\ \wedge & y^\ast = S.\SELEM[ea].\EIINIT[i \slice n]) \\ \end{array} \\[1ex] @@ -935,7 +935,7 @@ Table Instructions 5. Let :math:`\X{table}` be the :ref:`table instance ` :math:`S.\STABLES[ta]`. -6. Let :math:`sz` be the length of :math:`\X{table}.\MIELEMS`. +6. Let :math:`sz` be the length of :math:`\X{table}.\TIELEM`. 7. Assert: due to :ref:`validation `, three values of :ref:`value type ` |I32| are on the top of the stack. @@ -953,7 +953,7 @@ Table Instructions a. Trap. -13. Let :math:`y^\ast` be the function address sequence :math:`\X{table}.\MIELEMS[i \slice n]`. +13. Let :math:`y^\ast` be the function address sequence :math:`\X{table}.\TIELEM[i \slice n]`. 14. :ref:`Initialize ` the table instance at address :math:`ta` starting from offset :math:`j` with the function address sequence :math:`y^\ast`. @@ -966,9 +966,9 @@ Table Instructions \\ \qquad \begin{array}[j]{@{}r@{~}l@{}} (\iff & F.\AMODULE.\MITABLES[0] = ta \\ - \wedge & (i + n \leq |S.\STABLES[ta].\MIELEMS|) \\ - \wedge & (j + n \leq |S.\STABLES[ta].\MIELEMS|) \\ - \wedge & y^\ast = S.\STABLES[ta].\MIELEMS[i \slice n]) \\ + \wedge & (i + n \leq |S.\STABLES[ta].\TIELEM|) \\ + \wedge & (j + n \leq |S.\STABLES[ta].\TIELEM|) \\ + \wedge & y^\ast = S.\STABLES[ta].\TIELEM[i \slice n]) \\ \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} @@ -987,11 +987,9 @@ Table Instructions 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. For each :ref:`function index ` :math:`x_i` of :math:`x^\ast`: +2. For each :ref:`function address ` :math:`x_i` of :math:`x^\ast`: - a. Let :math:`\funcaddr_i` be the :ref:`function address ` :math:`F.\AMODULE.\MIFUNCS[x_i]`. - - b. Replace :math:`S.\STABLES[\tableaddr].\TIELEM[o + i]` with :math:`\funcaddr_i`. + a. Replace :math:`S.\STABLES[\tableaddr].\TIELEM[o + i]` with :math:`x_i`. .. math:: ~\\[-1ex] @@ -1001,7 +999,7 @@ Table Instructions S; F; \INITELEM~\tableaddr~o~(x_0~x^\ast) &\stepto& S'; F; \INITELEM~\tableaddr~(o+1)~x^\ast \end{array} \\ \qquad - (\iff S' = S \with \STABLES[\tableaddr].\TIELEM[o] = F.\AMODULE.\MIFUNCS[x_0]) \\ + (\iff S' = S \with \STABLES[\tableaddr].\TIELEM[o] = x_0) \\ \end{array} From d058cd02839f4ae301ff36b1d45c32a9b01534bf Mon Sep 17 00:00:00 2001 From: Ben Smith Date: Mon, 9 Jul 2018 11:49:24 -0700 Subject: [PATCH 8/8] Address some comments --- document/core/exec/instructions.rst | 58 +++++++++++------------------ document/core/exec/modules.rst | 5 ++- document/core/exec/runtime.rst | 4 +- 3 files changed, 28 insertions(+), 39 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 5d7542ea..42e47e94 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -639,7 +639,7 @@ Memory Instructions 8. Let :math:`da` be the :ref:`data segment address ` :math:`F.\AMODULE.\MIDATAS[x]`. -9. If :math:`S.\SDATA[da]` does not exist, then: +9. If :math:`S.\SDATA[da]` is :math:`\epsilon`, then: a. Trap. @@ -698,19 +698,11 @@ Memory Instructions 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIMEMS[0]` exists. +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIDATAS[x]` exists. -3. Let :math:`ma` be the :ref:`memory address ` :math:`F.\AMODULE.\MIMEMS[0]`. - -4. Assert: due to :ref:`validation `, :math:`S.\SMEMS[ma]` exists. - -5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[ma]`. - -6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIDATAS[x]` exists. +3. Let :math:`da` be the :ref:`data segment address ` :math:`F.\AMODULE.\MIDATAS[x]`. -7. Let :math:`da` be the :ref:`data segment address ` :math:`F.\AMODULE.\MIDATAS[x]`. - -8. Replace :math:`S.\SDATA[da]` with :math:`\epsilon`. +4. Replace :math:`S.\SDATA[da]` with :math:`\epsilon`. .. math:: ~\\[-1ex] @@ -720,8 +712,7 @@ Memory Instructions \end{array} \\ \qquad \begin{array}[j]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MIMEMS[0] = ma \\ - \wedge & F.\AMODULE.\MIDATAS[x] = da \\ + (\iff & F.\AMODULE.\MIDATAS[x] = da \\ \wedge & S' = S \with \SDATA[da] = \epsilon) \\ \end{array} \end{array} @@ -768,7 +759,7 @@ Memory Instructions ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYCOPY~x) &\stepto& S; F; (\INITDATA~ma~j~b^\ast) + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYCOPY) &\stepto& S; F; (\INITDATA~ma~j~b^\ast) \end{array} \\ \qquad \begin{array}[j]{@{}r@{~}l@{}} @@ -779,12 +770,16 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYCOPY~x) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYCOPY) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \end{array} +.. TODO: The semantics here describe making a copy of the source memory before + the writing begins. This is probably OK for now but will need to be updated + when threads are added. + .. index:: memory, memory instance, memory address, initialize memory .. _initdata: @@ -832,7 +827,7 @@ Table Instructions 8. Let :math:`ea` be the :ref:`element segment address ` :math:`F.\AMODULE.\MIELEMS[x]`. -9. If :math:`S.\SELEM[ea]` does not exist, then: +9. If :math:`S.\SELEM[ea]` is :math:`\epsilon`, then: a. Trap. @@ -891,19 +886,11 @@ Table Instructions 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[0]` exists. +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[x]` exists. -3. Let :math:`ta` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[0]`. - -4. Assert: due to :ref:`validation `, :math:`S.\STABLES[ta]` exists. - -5. Let :math:`\X{table}` be the :ref:`table instance ` :math:`S.\STABLES[ta]`. +3. Let :math:`ea` be the :ref:`element segment address ` :math:`F.\AMODULE.\MIELEMS[x]`. -6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[x]` exists. - -7. Let :math:`ea` be the :ref:`element segment address ` :math:`F.\AMODULE.\MIELEMS[x]`. - -8. Replace :math:`S.\SELEM[ea]` with :math:`\epsilon`. +4. Replace :math:`S.\SELEM[ea]` with :math:`\epsilon`. .. math:: ~\\[-1ex] @@ -913,8 +900,7 @@ Table Instructions \end{array} \\ \qquad \begin{array}[j]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITABLES[0] = ta \\ - \wedge & F.\AMODULE.\MIELEMS[x] = ea \\ + (\iff & F.\AMODULE.\MIELEMS[x] = ea \\ \wedge & S' = S \with \SELEM[ea] = \epsilon) \\ \end{array} \end{array} @@ -961,7 +947,7 @@ Table Instructions ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLECOPY~x) &\stepto& S; F; (\INITELEM~ta~j~y^\ast) + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLECOPY) &\stepto& S; F; (\INITELEM~ta~j~y^\ast) \end{array} \\ \qquad \begin{array}[j]{@{}r@{~}l@{}} @@ -972,7 +958,7 @@ Table Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLECOPY~x) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLECOPY) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) @@ -982,12 +968,12 @@ Table Instructions .. index:: table, table instance, table address, initialize table .. _initelem: -:math:`\INITELEM~\tableaddr~o~x^\ast` +:math:`\INITELEM~\tableaddr~o~a^\ast` ..................................... 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. For each :ref:`function address ` :math:`x_i` of :math:`x^\ast`: +2. For each :ref:`function address ` :math:`x_i` of :math:`a^\ast`: a. Replace :math:`S.\STABLES[\tableaddr].\TIELEM[o + i]` with :math:`x_i`. @@ -996,10 +982,10 @@ Table Instructions \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; \INITELEM~\tableaddr~o~\epsilon &\stepto& S; F; \epsilon & \\ - S; F; \INITELEM~\tableaddr~o~(x_0~x^\ast) &\stepto& S'; F; \INITELEM~\tableaddr~(o+1)~x^\ast + S; F; \INITELEM~\tableaddr~o~(a_0~a^\ast) &\stepto& S'; F; \INITELEM~\tableaddr~(o+1)~a^\ast \end{array} \\ \qquad - (\iff S' = S \with \STABLES[\tableaddr].\TIELEM[o] = x_0) \\ + (\iff S' = S \with \STABLES[\tableaddr].\TIELEM[o] = a_0) \\ \end{array} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index ca75becf..344f938b 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -383,7 +383,9 @@ New instances of :ref:`functions `, :ref:`tables ` :math:`x_i` in :math:`e.\EINIT`, do: - a. Let :math:`\funcaddr_i` be the :ref:`function address ` :math:`\moduleinst.\MIFUNCS[x_i]`. + a. Assert: due to :ref:`validation `, the :ref:`function address ` :math:`\moduleinst.\MIFUNCS[x_i]` exists. + + b. Let :math:`\funcaddr_i` be the function address :math:`\moduleinst.\MIFUNCS[x_i]`. 4. Let :math:`\funcaddr^\ast` be the concatenation of the function addresses :math:`\funcaddr_i`. @@ -397,6 +399,7 @@ New instances of :ref:`functions `, :ref:`tables ` listing \STABLES & \tableinst^\ast, \\ \SMEMS & \meminst^\ast, \\ \SGLOBALS & \globalinst^\ast, \\ - \SELEM & \eleminst^\ast, \\ - \SDATA & \datainst^\ast ~\} \\ + \SELEM & (\eleminst^?)^\ast, \\ + \SDATA & (\datainst^?)^\ast ~\} \\ \end{array} \end{array}