From b108440070907c485841745ac33331012de9caae Mon Sep 17 00:00:00 2001 From: Wonho Date: Fri, 3 Nov 2023 17:24:28 +0900 Subject: [PATCH 1/4] Fix OOB cases for `array.get/set` --- document/core/exec/instructions.rst | 40 +++++++++++++++++------------ 1 file changed, 24 insertions(+), 16 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 802d0c69c8..ec36a56467 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -894,16 +894,20 @@ Reference Instructions 16. Push the value :math:`\val` to the stack. .. math:: + ~\\[-1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) &\stepto& \val - & + S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) \stepto \TRAP + \\ \qquad + (\iff |\SARRAYS[a].\AIFIELDS| \leq i) + \\[1ex] + S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) \stepto \val + \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ - \land & \val = \unpackval^{\sx^?}_{\X{ft}}(S.\SARRAYS[a].\AIFIELDS[i])) - \end{array} \\ - S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) &\stepto& \TRAP - & (\otherwise) \\ - S; F; (\REFNULL~t)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) &\stepto& \TRAP + (\otherwise, \iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ + \land & \val = \unpackval^{\sx^?}_{\X{ft}}(S.\SARRAYS[a].\AIFIELDS[i])) \\ + \end{array} + \\[1ex] + S; F; (\REFNULL~t)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) \stepto \TRAP \end{array} @@ -951,16 +955,20 @@ Reference Instructions 17. Replace the :ref:`field value ` :math:`S.\SARRAYS[a].\AIFIELDS[i]` with :math:`\fieldval`. .. math:: + ~\\[-1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) &\stepto& S'; \epsilon - & + S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) \stepto \TRAP + \\ \qquad + (\iff |\SARRAYS[a].\AIFIELDS| \leq i) + \\[1ex] + S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) \stepto S'; \epsilon + \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ - \land & S' = S \with \SARRAYS[a].\AIFIELDS[i] = \packval_{\X{ft}}(\val)) - \end{array} \\ - S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) &\stepto& \TRAP - & (\otherwise) \\ - S; F; (\REFNULL~t)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) &\stepto& \TRAP + (\otherwise, \iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ + \land & S' = S \with \SARRAYS[a].\AIFIELDS[i] = \packval_{\X{ft}}(\val)) \\ + \end{array} + \\[1ex] + S; F; (\REFNULL~t)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) \stepto \TRAP \end{array} From 3c6f6ea9a30457ac98deefb87d1931e731e717ef Mon Sep 17 00:00:00 2001 From: ShinWonho <50018375+ShinWonho@users.noreply.github.com> Date: Fri, 3 Nov 2023 19:31:05 +0900 Subject: [PATCH 2/4] Update document/core/exec/instructions.rst Co-authored-by: Andreas Rossberg --- document/core/exec/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ec36a56467..ef92e20e98 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -898,7 +898,7 @@ Reference Instructions \begin{array}{lcl@{\qquad}l} S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) \stepto \TRAP \\ \qquad - (\iff |\SARRAYS[a].\AIFIELDS| \leq i) + (\iff i \geq |\SARRAYS[a].\AIFIELDS|) \\[1ex] S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) \stepto \val \\ \qquad From 6a9736a79c16fb55b7c9ef215258705c99849a56 Mon Sep 17 00:00:00 2001 From: ShinWonho <50018375+ShinWonho@users.noreply.github.com> Date: Fri, 3 Nov 2023 19:31:13 +0900 Subject: [PATCH 3/4] Update document/core/exec/instructions.rst Co-authored-by: Andreas Rossberg --- document/core/exec/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ef92e20e98..970ebffb14 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -959,7 +959,7 @@ Reference Instructions \begin{array}{lcl@{\qquad}l} S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) \stepto \TRAP \\ \qquad - (\iff |\SARRAYS[a].\AIFIELDS| \leq i) + (\iff i \geq |\SARRAYS[a].\AIFIELDS|) \\[1ex] S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) \stepto S'; \epsilon \\ \qquad From 26ba9e298cb2e55b1dee2d00b8e3a0dc6b651f38 Mon Sep 17 00:00:00 2001 From: Wonho Date: Fri, 3 Nov 2023 19:42:15 +0900 Subject: [PATCH 4/4] Remove otherwise --- document/core/exec/instructions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 970ebffb14..ef10d61468 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -903,7 +903,7 @@ Reference Instructions S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) \stepto \val \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\otherwise, \iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ + (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ \land & \val = \unpackval^{\sx^?}_{\X{ft}}(S.\SARRAYS[a].\AIFIELDS[i])) \\ \end{array} \\[1ex] @@ -964,7 +964,7 @@ Reference Instructions S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) \stepto S'; \epsilon \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\otherwise, \iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ + (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ \land & S' = S \with \SARRAYS[a].\AIFIELDS[i] = \packval_{\X{ft}}(\val)) \\ \end{array} \\[1ex]