From 6f5ce24e5b200bb0d9058a237b17939b8959fd34 Mon Sep 17 00:00:00 2001 From: Ben Smith Date: Thu, 27 Jun 2019 17:52:20 -0700 Subject: [PATCH 1/2] [spec] Update text for zero-byte OOB case Also fix some typos from previous CL (see macros.def) --- document/core/exec/instructions.rst | 53 +++-------------------------- document/core/util/macros.def | 4 +-- 2 files changed, 7 insertions(+), 50 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 71d15d30..26023ab8 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -645,13 +645,7 @@ Memory Instructions 11. Pop the value :math:`\I32.\CONST~i` from the stack. -12. If :math:`n` is :math:`0`, then: - - a. If :math:`i` is larger than the length of :math:`\X{mem}.\MIDATA`, then: - - i. Trap. - -13. Else: +12. Else: a. Push the value :math:`\I32.\CONST~i` to the stack. @@ -678,14 +672,7 @@ Memory Instructions \end{array} \\ \begin{array}{lcl@{\qquad}l} S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~0)~(\MEMORYFILL) &\stepto& S; F; \epsilon - \end{array} - \\ \qquad - (\iff i \leq |\SMEMS[F.\AMODULE.\MIMEMS[0]]|) \\ - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~0)~(\MEMORYFILL) &\stepto& S; F; \TRAP - \end{array} - \\ \qquad - (\otherwise) \\ + \end{array} \\ \end{array} @@ -728,17 +715,7 @@ Memory Instructions 16. Pop the value :math:`\I32.\CONST~d` from the stack. -17. If :math:`n` is :math:`0`, then: - - a. If :math:`d` is larger than the length of :math:`\X{mem}.\MIDATA`, then: - - i. Trap. - - b. If :math:`s` is larger than the length of :math:`\X{data}.\DIINIT`, then: - - i. Trap. - -18. Else: +17. Else: a. Push the value :math:`\I32.\CONST~d` to the stack. @@ -773,13 +750,8 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~d)~(\I32.\CONST~(s)~(\I32.\CONST~0)~(\MEMORYINIT~x) &\stepto& S; F; \epsilon + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\MEMORYINIT~x) &\stepto& S; F; \epsilon \end{array} - \\ \qquad - \begin{array}[t]{@{}r@{~}l@{}} - (\iff & d \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\ - \wedge & s \leq |S.\SDATA[F.\AMODULE.\MIDATAS[x]].\DIINIT|) \\ - \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\MEMORYINIT~x) &\stepto& S; F; \TRAP @@ -877,17 +849,7 @@ Table Instructions 16. Pop the value :math:`\I32.\CONST~d` from the stack. -17. If :math:`n` is :math:`0`, then: - - a. If :math:`d` is larger than the length of :math:`\X{table}.\TIELEM`, then: - - i. Trap. - - b. If :math:`s` is larger than the length of :math:`\X{elem}.\EIINIT`, then: - - i. Trap. - -18. Else: +17. Else: a. Push the value :math:`\I32.\CONST~d` to the stack. @@ -922,11 +884,6 @@ Table Instructions \begin{array}{lcl@{\qquad}l} S; F; (\I32.\CONST~d)~(\I32.\CONST~(s)~(\I32.\CONST~0)~(\TABLEINIT~x) &\stepto& S; F; \epsilon \end{array} - \\ \qquad - \begin{array}[t]{@{}r@{~}l@{}} - (\iff & d \leq |S.\STABLES[F.\AMODULE.\MITABLES[0]].\TIELEM| \\ - \wedge & s \leq |S.\SELEM[F.\AMODULE.\MIELEMS[x]].\EIINIT|) \\ - \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLEINIT~x) &\stepto& S; F; \TRAP diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 50160af9..be0829cf 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -922,8 +922,8 @@ .. |INVOKE| mathdef:: \xref{exec/runtime}{syntax-invoke}{\K{invoke}} .. |INITELEM| mathdef:: \xref{exec/runtime}{syntax-init_elem}{\K{init\_elem}} .. |INITDATA| mathdef:: \xref{exec/runtime}{syntax-init_data}{\K{init\_data}} -.. |TABLEGET| mathdef:: \xref{exec/runtime}{syntax-table_get}{\K{table.get} -.. |TABLESET| mathdef:: \xref{exec/runtime}{syntax-table_set}{\K{table.set} +.. |TABLEGET| mathdef:: \xref{exec/runtime}{syntax-table_get}{\K{table.get}} +.. |TABLESET| mathdef:: \xref{exec/runtime}{syntax-table_set}{\K{table.set}} .. Values & Results, non-terminals From c7773437b5d86c78e4ba6b7b302e5326a7c141e6 Mon Sep 17 00:00:00 2001 From: Ben Smith Date: Fri, 28 Jun 2019 11:35:02 -0700 Subject: [PATCH 2/2] Move zero case first --- document/core/exec/instructions.rst | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 26023ab8..5706ab54 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -737,6 +737,10 @@ Memory Instructions ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\MEMORYINIT~x) &\stepto& S; F; \epsilon + \end{array} + \\[1ex] + \begin{array}{lcl@{\qquad}l} S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~(n+1))~(\MEMORYINIT~x) &\stepto& S; F; \begin{array}[t]{@{}l@{}} (\I32.\CONST~d)~(\I32.\CONST~b)~(\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\ @@ -750,10 +754,6 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\MEMORYINIT~x) &\stepto& S; F; \epsilon - \end{array} - \\[1ex] - \begin{array}{lcl@{\qquad}l} S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\MEMORYINIT~x) &\stepto& S; F; \TRAP \end{array} \\ \qquad @@ -869,6 +869,10 @@ Table Instructions ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} + S; F; (\I32.\CONST~d)~(\I32.\CONST~(s)~(\I32.\CONST~0)~(\TABLEINIT~x) &\stepto& S; F; \epsilon + \end{array} + \\[1ex] + \begin{array}{lcl@{\qquad}l} S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~(n+1))~(\TABLEINIT~x) &\stepto& S; F; \begin{array}[t]{@{}l@{}} (\I32.\CONST~d)~\funcelem~\TABLESET \\ @@ -882,10 +886,6 @@ Table Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~d)~(\I32.\CONST~(s)~(\I32.\CONST~0)~(\TABLEINIT~x) &\stepto& S; F; \epsilon - \end{array} - \\[1ex] - \begin{array}{lcl@{\qquad}l} S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLEINIT~x) &\stepto& S; F; \TRAP \end{array} \\ \qquad