From f83a375df438067de1eafc25a2b5e249b7115a92 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 21 Nov 2023 09:03:52 +0100 Subject: [PATCH 1/4] [spec] Add missing length condition to br_table prose (#1709) --- document/core/valid/instructions.rst | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index afcda69c01..43dfe9abfb 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1412,17 +1412,22 @@ Control Instructions ........................... -* The label :math:`C.\CLABELS[l_N]` must be defined in the context. +* The :ref:`label ` :math:`C.\CLABELS[l_N]` must be defined in the context. -* For all :math:`l_i` in :math:`l^\ast`, +* For each :ref:`label ` :math:`l_i` in :math:`l^\ast`, the label :math:`C.\CLABELS[l_i]` must be defined in the context. * There must be a sequence :math:`t^\ast` of :ref:`operand types `, such that: + * The length of the sequence :math:`t^\ast` is the same as the length of the sequence :math:`C.\CLABELS[l_N]`. + * For each :ref:`operand type ` :math:`t_j` in :math:`t^\ast` and corresponding type :math:`t'_{Nj}` in :math:`C.\CLABELS[l_N]`, :math:`t_j` :ref:`matches ` :math:`t'_{Nj}`. - * For all :math:`l_i` in :math:`l^\ast`, - and for each :ref:`operand type ` :math:`t_j` in :math:`t^\ast` and corresponding type :math:`t'_{ij}` in :math:`C.\CLABELS[l_i]`, :math:`t_j` :ref:`matches ` :math:`t'_{ij}`. + * For each :ref:`label ` :math:`l_i` in :math:`l^\ast`: + + * The length of the sequence :math:`t^\ast` is the same as the length of the sequence :math:`C.\CLABELS[l_i]`. + + * For each :ref:`operand type ` :math:`t_j` in :math:`t^\ast` and corresponding type :math:`t'_{ij}` in :math:`C.\CLABELS[l_i]`, :math:`t_j` :ref:`matches ` :math:`t'_{ij}`. * Then the instruction is valid with type :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`, for any sequences of :ref:`operand types ` :math:`t_1^\ast` and :math:`t_2^\ast`. From c7eef192b77125b88a4ab3ae7a944d10c0860f55 Mon Sep 17 00:00:00 2001 From: Hoseong Lee <101983402+HoseongLee@users.noreply.github.com> Date: Fri, 1 Dec 2023 16:17:23 +0900 Subject: [PATCH 2/4] [spec] Fix typo in shape.all_true and txN.bitmask instruction execution (#1710) --- 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 74802d6deb..dac2b7390a 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -669,9 +669,9 @@ Most other vector instructions are defined in terms of numeric operators that ar 1. Assert: due to :ref:`validation `, a value of :ref:`value type ` |V128| is on the top of the stack. -2. Pop the value :math:`\V128.\VCONST~c_1` from the stack. +2. Pop the value :math:`\V128.\VCONST~c` from the stack. -3. Let :math:`i_1^\ast` be the result of computing :math:`\lanes_{\shape}(c_1)`. +3. Let :math:`i_1^\ast` be the result of computing :math:`\lanes_{\shape}(c)`. 4. Let :math:`i` be the result of computing :math:`\bool(\bigwedge(i_1 \neq 0)^\ast)`. @@ -681,7 +681,7 @@ Most other vector instructions are defined in terms of numeric operators that ar .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - (\V128\K{.}\VCONST~c_1)~\shape\K{.}\ALLTRUE &\stepto& (\I32\K{.}\CONST~i) + (\V128\K{.}\VCONST~c)~\shape\K{.}\ALLTRUE &\stepto& (\I32\K{.}\CONST~i) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -698,7 +698,7 @@ Most other vector instructions are defined in terms of numeric operators that ar 1. Assert: due to :ref:`validation `, a value of :ref:`value type ` |V128| is on the top of the stack. -2. Pop the value :math:`\V128.\VCONST~c_1` from the stack. +2. Pop the value :math:`\V128.\VCONST~c` from the stack. 3. Let :math:`i_1^N` be the result of computing :math:`\lanes_{t\K{x}N}(c)`. @@ -708,14 +708,14 @@ Most other vector instructions are defined in terms of numeric operators that ar 6. Let :math:`j^\ast` be the concatenation of the two sequences :math:`i_2^N` and :math:`0^{32-N}`. -7. Let :math:`c` be the result of computing :math:`\ibits_{32}^{-1}(j^\ast)`. +7. Let :math:`i` be the result of computing :math:`\ibits_{32}^{-1}(j^\ast)`. -8. Push the value :math:`\I32.\CONST~c` onto the stack. +8. Push the value :math:`\I32.\CONST~i` onto the stack. .. math:: \begin{array}{lcl@{\qquad}l} - (\V128\K{.}\VCONST~c_1)~t\K{x}N\K{.}\BITMASK &\stepto& (\I32\K{.}\CONST~c) - & (\iff c = \ibits_{32}^{-1}(\ilts_{|t|}(\lanes_{t\K{x}N}(c), 0^N))) + (\V128\K{.}\VCONST~c)~t\K{x}N\K{.}\BITMASK &\stepto& (\I32\K{.}\CONST~i) + & (\iff i = \ibits_{32}^{-1}(\ilts_{|t|}(\lanes_{t\K{x}N}(c), 0^N))) \\ \end{array} From 2f351f3a84037902740f05085584ad60e388c24b Mon Sep 17 00:00:00 2001 From: YiYing He Date: Sat, 2 Dec 2023 01:37:00 +0800 Subject: [PATCH 3/4] [test] Unify the error message. 1. "array is immutable" for trying to assign values into an immutable array in validation. 2. "out of bounds array access" for trying to access out of bounds array in execution. Signed-off-by: YiYing He --- interpreter/valid/valid.ml | 2 +- test/core/gc/array.wast | 16 ++++++++-------- test/core/gc/array_copy.wast | 2 +- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index e14fc6d36b..f076e42b4f 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -758,7 +758,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in | ArrayCopy (x, y) -> let ArrayT (FieldT (mutd, std)) = array_type c x in let ArrayT (FieldT (_muts, sts)) = array_type c y in - require (mutd = Var) e.at "destination array is immutable"; + require (mutd = Var) e.at "array is immutable"; require (match_storage_type c.types sts std) e.at "array types do not match"; [RefT (Null, DefHT (type_ c x)); NumT I32T; RefT (Null, DefHT (type_ c y)); NumT I32T; NumT I32T] --> [], [] diff --git a/test/core/gc/array.wast b/test/core/gc/array.wast index 0da7e84320..f5888cb2d9 100644 --- a/test/core/gc/array.wast +++ b/test/core/gc/array.wast @@ -100,8 +100,8 @@ (assert_return (invoke "set_get" (i32.const 1) (f32.const 7)) (f32.const 7)) (assert_return (invoke "len") (i32.const 3)) -(assert_trap (invoke "get" (i32.const 10)) "out of bounds") -(assert_trap (invoke "set_get" (i32.const 10) (f32.const 7)) "out of bounds") +(assert_trap (invoke "get" (i32.const 10)) "out of bounds array access") +(assert_trap (invoke "set_get" (i32.const 10) (f32.const 7)) "out of bounds array access") (module (type $vec (array f32)) @@ -145,8 +145,8 @@ (assert_return (invoke "set_get" (i32.const 1) (f32.const 7)) (f32.const 7)) (assert_return (invoke "len") (i32.const 2)) -(assert_trap (invoke "get" (i32.const 10)) "out of bounds") -(assert_trap (invoke "set_get" (i32.const 10) (f32.const 7)) "out of bounds") +(assert_trap (invoke "get" (i32.const 10)) "out of bounds array access") +(assert_trap (invoke "set_get" (i32.const 10) (f32.const 7)) "out of bounds array access") (module (type $vec (array i8)) @@ -190,8 +190,8 @@ (assert_return (invoke "set_get" (i32.const 1) (i32.const 7)) (i32.const 7)) (assert_return (invoke "len") (i32.const 3)) -(assert_trap (invoke "get" (i32.const 10)) "out of bounds") -(assert_trap (invoke "set_get" (i32.const 10) (i32.const 7)) "out of bounds") +(assert_trap (invoke "get" (i32.const 10)) "out of bounds array access") +(assert_trap (invoke "set_get" (i32.const 10) (i32.const 7)) "out of bounds array access") (module (type $bvec (array i8)) @@ -249,8 +249,8 @@ (assert_return (invoke "set_get" (i32.const 0) (i32.const 1) (i32.const 1)) (i32.const 2)) (assert_return (invoke "len") (i32.const 2)) -(assert_trap (invoke "get" (i32.const 10) (i32.const 0)) "out of bounds") -(assert_trap (invoke "set_get" (i32.const 10) (i32.const 0) (i32.const 0)) "out of bounds") +(assert_trap (invoke "get" (i32.const 10) (i32.const 0)) "out of bounds array access") +(assert_trap (invoke "set_get" (i32.const 10) (i32.const 0) (i32.const 0)) "out of bounds array access") (assert_invalid (module diff --git a/test/core/gc/array_copy.wast b/test/core/gc/array_copy.wast index 06090cb53a..d1caf12647 100644 --- a/test/core/gc/array_copy.wast +++ b/test/core/gc/array_copy.wast @@ -11,7 +11,7 @@ (array.copy $a $b (local.get $1) (i32.const 0) (local.get $2) (i32.const 0) (i32.const 0)) ) ) - "destination array is immutable" + "array is immutable" ) (assert_invalid From 30362a2a3345c4a8f2d63331c1dc15f328c8ccea Mon Sep 17 00:00:00 2001 From: YiYing He Date: Sat, 2 Dec 2023 20:20:49 +0800 Subject: [PATCH 4/4] [test] Unify the trap message of "null function reference". Signed-off-by: YiYing He --- test/core/call_ref.wast | 2 +- test/core/return_call_ref.wast | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/test/core/call_ref.wast b/test/core/call_ref.wast index 425339593e..da480a7f23 100644 --- a/test/core/call_ref.wast +++ b/test/core/call_ref.wast @@ -94,7 +94,7 @@ (assert_return (invoke "run" (i32.const 0)) (i32.const 0)) (assert_return (invoke "run" (i32.const 3)) (i32.const -9)) -(assert_trap (invoke "null") "null function") +(assert_trap (invoke "null") "null function reference") (assert_return (invoke "fac" (i64.const 0)) (i64.const 1)) (assert_return (invoke "fac" (i64.const 1)) (i64.const 1)) diff --git a/test/core/return_call_ref.wast b/test/core/return_call_ref.wast index 353811f038..2b495f46e9 100644 --- a/test/core/return_call_ref.wast +++ b/test/core/return_call_ref.wast @@ -180,7 +180,7 @@ (assert_return (invoke "type-second-f32") (f32.const 32)) (assert_return (invoke "type-second-f64") (f64.const 64.1)) -(assert_trap (invoke "null") "null function") +(assert_trap (invoke "null") "null function reference") (assert_return (invoke "fac-acc" (i64.const 0) (i64.const 1)) (i64.const 1)) (assert_return (invoke "fac-acc" (i64.const 1) (i64.const 1)) (i64.const 1))