diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 20822a28..ab3ef5b0 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -651,42 +651,49 @@ Table Instructions 11. Pop the value :math:`\I32.\CONST~i` from the stack. -12. If :math:`n` is :math:`0`, then: +12. If :math:`i + n` is larger than the length of :math:`\X{tab}.\TIELEM`, then: - a. If :math:`i` is larger than the length of :math:`\X{tab}.\TIELEM`, then: + a. Trap. - i. Trap. +12. If :math:`n` is :math:`0`, then: -12. Else: + a. Return. - a. Push the value :math:`\I32.CONST~i` to the stack. +13. Push the value :math:`\I32.CONST~i` to the stack. - b. Push the value :math:`\val` to the stack. +14. Push the value :math:`\val` to the stack. - c. Execute the instruction :math:`\TABLESET~x`. +15. Execute the instruction :math:`\TABLESET~x`. - d. Push the value :math:`\I32.CONST~(i+1)` to the stack. +16. Push the value :math:`\I32.CONST~(i+1)` to the stack. - e. Push the value :math:`\val` to the stack. +17. Push the value :math:`\val` to the stack. - f. Push the value :math:`\I32.CONST~(n-1)` to the stack. +18. Push the value :math:`\I32.CONST~(n-1)` to the stack. - c. Execute the instruction :math:`\TABLEFILL~x`. +19. Execute the instruction :math:`\TABLEFILL~x`. .. math:: \begin{array}{l} - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~(n+1))~(\TABLEFILL~x) &\stepto& S'; F; (\I32.\CONST~i)~\val~(\TABLESET~x)~(\I32.\CONST~(i+1))~\val~(\I32.\CONST~n)~(\TABLEFILL~x) - \end{array} \\ - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~0)~(\TABLEFILL~x) &\stepto& S'; F; \epsilon - \end{array} - \\ \qquad - (\iff i \leq |\STABLES[F.\AMODULE.\MITABLES[x]]|) \\ - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~0)~(\TABLEFILL~x) &\stepto& S; F; \TRAP - \end{array} - \\ \qquad + S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~n)~(\TABLEFILL~x) + \quad\stepto\quad S; F; \TRAP + \\ \qquad + \begin{array}[t]{@{}r@{~}l@{}} + (\iff & i + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\ + \end{array} + \\[1ex] + S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~0)~(\TABLEFILL~x) + \quad\stepto\quad S; F; \epsilon + \\ \qquad + (\otherwise) + \\[1ex] + S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~n+1)~(\TABLEFILL~x) + \quad\stepto\quad S; F; + \begin{array}[t]{@{}l@{}} + (\I32.\CONST~i)~\val~(\TABLESET~x) \\ + (\I32.\CONST~i+1)~\val~(\I32.\CONST~n)~(\TABLEFILL~x) \\ + \end{array} + \\ \qquad (\otherwise) \\ \end{array}