diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 63e17be482..4042c34994 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2000,9 +2000,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:`\tobool(\bigwedge(i_1 \neq 0)^\ast)`. @@ -2012,7 +2012,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@{}} @@ -2029,7 +2029,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)`. @@ -2039,14 +2039,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} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index f3a57bd836..746189e549 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1972,17 +1972,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:`value types `, such that: - * The result type :math:`[t^\ast]` :ref:`matches ` :math:`C.\CLABELS[l_N]`. + * The length of the sequence :math:`t^\ast` is the same as the length of the sequence :math:`C.\CLABELS[l_N]`. - * For all :math:`l_i` in :math:`l^\ast`, - the result type :math:`[t^\ast]` :ref:`matches ` :math:`C.\CLABELS[l_i]`. + * 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 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 any :ref:`valid ` type of the form :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`. diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index dc755f332c..9bb1459412 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -889,7 +889,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/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/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 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))