diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 3672e42d..42e47e94 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -618,6 +618,377 @@ 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]` is :math:`\epsilon`, 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~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:`dsz` be the length of :math:`\X{data}.\DIINIT`. + +16. If :math:`i + n > dsz`, then: + + a. Trap. + +17. If :math:`j + n > msz`, then: + + a. Trap. + +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`. + +.. math:: + ~\\[-1ex] + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + 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}[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]) \\ + \end{array} + \\[1ex] + \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\MEMORYINIT~x) &\stepto& S; F; \TRAP + \end{array} + \\ \qquad + (\otherwise) + \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.\MIDATAS[x]` exists. + +3. Let :math:`da` be the :ref:`data segment address ` :math:`F.\AMODULE.\MIDATAS[x]`. + +4. 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.\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) &\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) &\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: + +: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 +~~~~~~~~~~~~~~~~~~ + +.. _exec-table.init: + +:math:`\TABLEINIT~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. Let :math:`tsz` be the length of :math:`\X{table}.\TIELEM`. + +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]` is :math:`\epsilon`, 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].\TIELEM|) \\ + \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.\MIELEMS[x]` exists. + +3. Let :math:`ea` be the :ref:`element segment address ` :math:`F.\AMODULE.\MIELEMS[x]`. + +4. 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.\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}.\TIELEM`. + +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}.\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`. + +.. math:: + ~\\[-1ex] + \begin{array}{l} + \begin{array}{lcl@{\qquad}l} + 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@{}} + (\iff & F.\AMODULE.\MITABLES[0] = ta \\ + \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} + S; F; (\I32.\CONST~n)~(\I32.\CONST~j)~(\I32.\CONST~i)~(\TABLECOPY) &\stepto& S; F; \TRAP + \end{array} + \\ \qquad + (\otherwise) + \end{array} + + +.. index:: table, table instance, table address, initialize table +.. _initelem: + +: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:`a^\ast`: + + a. Replace :math:`S.\STABLES[\tableaddr].\TIELEM[o + i]` with :math:`x_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~(a_0~a^\ast) &\stepto& S'; F; \INITELEM~\tableaddr~(o+1)~a^\ast + \end{array} + \\ \qquad + (\iff S' = S \with \STABLES[\tableaddr].\TIELEM[o] = a_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 bc772ddc..344f938b 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -371,6 +371,67 @@ New instances of :ref:`functions `, :ref:`tables ` +......................................... + +1. Let :math:`e` be the :ref:`element segment ` to allocate. + +2. 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: + + 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`. + +5. Let :math:`\eleminst` be the :ref:`element instance ` :math:`\{ \EIINIT~\funcaddr^\ast \}`. + +6. Append :math:`\eleminst` to the |SELEM| of :math:`S`. + +7. Return :math:`a`. + +.. math:: + \begin{array}{rlll} + \allocelem(S, e, \moduleinst) &=& S', \elemaddr \\[1ex] + \mbox{where:} \hfill \\ + \x^\ast &=& e.\EINIT \\ + \elemaddr &=& |S.\SELEM| \\ + \eleminst &=& \{ \EIINIT~(\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. Let :math:`a` be the first free :ref:`data address ` in :math:`S`. + +3. Let :math:`\datainst` be the :ref:`data instance ` :math:`\{ \DIINIT~d.\DINIT \}`. + +4. Append :math:`\datainst` to the |SDATA| of :math:`S`. + +5. Return :math:`a`. + +.. math:: + \begin{array}{rlll} + \allocdata(S, d, \moduleinst) &=& S', \dataaddr \\[1ex] + \mbox{where:} \hfill \\ + \dataaddr &=& |S.\SDATA| \\ + \datainst &=& \{ \DIINIT~d.\DINIT \} \\ + S' &=& S \compose \{\SDATA~\datainst\} \\ + \end{array} + + .. index:: table, table instance, table address, grow, limits .. _grow-table: @@ -411,7 +472,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 +500,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. Let :math:`\tableaddr^\ast` be the the concatenation of the :ref:`table addresses ` :math:`\tableaddr_i` in index order. +7. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA`, do: -8. Let :math:`\memaddr^\ast` be the the concatenation of the :ref:`memory addresses ` :math:`\memaddr_i` in index order. + a. Let :math:`\dataaddr_i` be the :ref:`data address ` resulting from :ref:`allocating ` :math:`\data_i`. -9. Let :math:`\globaladdr^\ast` be the the concatenation of the :ref:`global addresses ` :math:`\globaladdr_i` in index order. +8. Let :math:`\funcaddr^\ast` be the the concatenation of the :ref:`function addresses ` :math:`\funcaddr_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`. +9. Let :math:`\tableaddr^\ast` be the the concatenation of the :ref:`table addresses ` :math:`\tableaddr_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`. +10. Let :math:`\memaddr^\ast` be the the concatenation of the :ref:`memory addresses ` :math:`\memaddr_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`. +11. Let :math:`\globaladdr^\ast` be the the concatenation of the :ref:`global addresses ` :math:`\globaladdr_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`. +12. Let :math:`\elemaddr^\ast` be the the concatenation of the :ref:`element addresses ` :math:`\elemaddr_i` in index order. -14. For each :ref:`export ` :math:`\export_i` in :math:`\module.\MEXPORTS`, do: +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`. + +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 +540,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 +563,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 +572,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 @@ -597,47 +674,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. @@ -645,19 +726,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. 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. + a. If :math:`\elem_i` is :ref:`active `, then: - 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}`. + 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. For each :ref:`byte ` :math:`b_{ij}` in :math:`\data_i.\DINIT` (starting with :math:`j = 0`), do: + a. If :math:`\data_i` :ref:`active `, then: - i. Replace :math:`\meminst_i.\MIDATA[\X{do}_i + j]` with :math:`b_{ij}`. + 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: @@ -682,8 +759,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] @@ -696,18 +773,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..215d515d 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 &::=& + \{ \EIINIT~\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 &::=& + \{ \DIINIT~\vec(\byte) \} \\ + \end{array} + + .. index:: ! export instance, export, name, external value pair: abstract syntax; export instance pair: export; instance 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 657ec4ce..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}} @@ -781,6 +785,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 +800,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 +820,10 @@ .. |GIVALUE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{value}} .. |GIMUT| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{mut}} +.. |EIINIT| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\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}} @@ -825,6 +837,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 +852,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 +873,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