Skip to content
This repository was archived by the owner on Nov 3, 2021. It is now read-only.

table.fill: Bounds check before mutating the table #106

Merged
merged 1 commit into from
Jul 21, 2020
Merged

table.fill: Bounds check before mutating the table #106

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 30 additions & 23 deletions document/core/exec/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The formal notation needs to be fixed too -- this will still partially fill.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps someone else could fix that part? I'm not super familiar with latex / our conventions for the formal notation.

\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}

Expand Down