diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index da9dd112df..0b0c126fb5 100755 --- a/document/core/appendix/index-instructions.py +++ b/document/core/appendix/index-instructions.py @@ -117,10 +117,10 @@ def Instruction(version, name, opcode, type=None, validation=None, execution=Non Instruction(2.0, r'\TABLEGET~x', r'\hex{25}', r'[\X{at}] \to [t]', r'valid-table.get', r'exec-table.get'), Instruction(2.0, r'\TABLESET~x', r'\hex{26}', r'[\X{at}~t] \to []', r'valid-table.set', r'exec-table.set'), Instruction(0.0, None, r'\hex{27}'), - Instruction(1.0, r'\I32.\LOAD~x~\memarg', r'\hex{28}', r'[\X{at}] \to [\I32]', r'valid-load-val', r'exec-load-val'), - Instruction(1.0, r'\I64.\LOAD~x~\memarg', r'\hex{29}', r'[\X{at}] \to [\I64]', r'valid-load-val', r'exec-load-val'), - Instruction(1.0, r'\F32.\LOAD~x~\memarg', r'\hex{2A}', r'[\X{at}] \to [\F32]', r'valid-load-val', r'exec-load-val'), - Instruction(1.0, r'\F64.\LOAD~x~\memarg', r'\hex{2B}', r'[\X{at}] \to [\F64]', r'valid-load-val', r'exec-load-val'), + Instruction(1.0, r'\I32.\LOAD~x~\memarg', r'\hex{28}', r'[\X{at}] \to [\I32]', r'valid-load-num', r'exec-load-num'), + Instruction(1.0, r'\I64.\LOAD~x~\memarg', r'\hex{29}', r'[\X{at}] \to [\I64]', r'valid-load-num', r'exec-load-num'), + Instruction(1.0, r'\F32.\LOAD~x~\memarg', r'\hex{2A}', r'[\X{at}] \to [\F32]', r'valid-load-num', r'exec-load-num'), + Instruction(1.0, r'\F64.\LOAD~x~\memarg', r'\hex{2B}', r'[\X{at}] \to [\F64]', r'valid-load-num', r'exec-load-num'), Instruction(1.0, r'\I32.\LOAD\K{8\_s}~x~\memarg', r'\hex{2C}', r'[\X{at}] \to [\I32]', r'valid-load-pack', r'exec-load-pack'), Instruction(1.0, r'\I32.\LOAD\K{8\_u}~x~\memarg', r'\hex{2D}', r'[\X{at}] \to [\I32]', r'valid-load-pack', r'exec-load-pack'), Instruction(1.0, r'\I32.\LOAD\K{16\_s}~x~\memarg', r'\hex{2E}', r'[\X{at}] \to [\I32]', r'valid-load-pack', r'exec-load-pack'), @@ -131,10 +131,10 @@ def Instruction(version, name, opcode, type=None, validation=None, execution=Non Instruction(1.0, r'\I64.\LOAD\K{16\_u}~x~\memarg', r'\hex{33}', r'[\X{at}] \to [\I64]', r'valid-load-pack', r'exec-load-pack'), Instruction(1.0, r'\I64.\LOAD\K{32\_s}~x~\memarg', r'\hex{34}', r'[\X{at}] \to [\I64]', r'valid-load-pack', r'exec-load-pack'), Instruction(1.0, r'\I64.\LOAD\K{32\_u}~x~\memarg', r'\hex{35}', r'[\X{at}] \to [\I64]', r'valid-load-pack', r'exec-load-pack'), - Instruction(1.0, r'\I32.\STORE~x~\memarg', r'\hex{36}', r'[\X{at}~\I32] \to []', r'valid-store-val', r'exec-store-val'), - Instruction(1.0, r'\I64.\STORE~x~\memarg', r'\hex{37}', r'[\X{at}~\I64] \to []', r'valid-store-val', r'exec-store-val'), - Instruction(1.0, r'\F32.\STORE~x~\memarg', r'\hex{38}', r'[\X{at}~\F32] \to []', r'valid-store-val', r'exec-store-val'), - Instruction(1.0, r'\F64.\STORE~x~\memarg', r'\hex{39}', r'[\X{at}~\F64] \to []', r'valid-store-val', r'exec-store-val'), + Instruction(1.0, r'\I32.\STORE~x~\memarg', r'\hex{36}', r'[\X{at}~\I32] \to []', r'valid-store-num', r'exec-store-num'), + Instruction(1.0, r'\I64.\STORE~x~\memarg', r'\hex{37}', r'[\X{at}~\I64] \to []', r'valid-store-num', r'exec-store-num'), + Instruction(1.0, r'\F32.\STORE~x~\memarg', r'\hex{38}', r'[\X{at}~\F32] \to []', r'valid-store-num', r'exec-store-num'), + Instruction(1.0, r'\F64.\STORE~x~\memarg', r'\hex{39}', r'[\X{at}~\F64] \to []', r'valid-store-num', r'exec-store-num'), Instruction(1.0, r'\I32.\STORE\K{8}~x~\memarg', r'\hex{3A}', r'[\X{at}~\I32] \to []', r'valid-store-pack', r'exec-store-pack'), Instruction(1.0, r'\I32.\STORE\K{16}~x~\memarg', r'\hex{3B}', r'[\X{at}~\I32] \to []', r'valid-store-pack', r'exec-store-pack'), Instruction(1.0, r'\I64.\STORE\K{8}~x~\memarg', r'\hex{3C}', r'[\X{at}~\I64] \to []', r'valid-store-pack', r'exec-store-pack'), @@ -379,7 +379,7 @@ def Instruction(version, name, opcode, type=None, validation=None, execution=Non Instruction(2.0, r'\TABLESIZE~x', r'\hex{FC}~\hex{10}', r'[] \to [\X{at}]', r'valid-table.size', r'exec-table.size'), Instruction(2.0, r'\TABLEFILL~x', r'\hex{FC}~\hex{11}', r'[\X{at}~t~\X{at}] \to []', r'valid-table.fill', r'exec-table.fill'), Instruction(0.0, None, r'\hex{FC}~\hex{12} \dots'), - Instruction(2.0, r'\V128.\VLOAD~x~\memarg', r'\hex{FD}~~\hex{00}', r'[\X{at}] \to [\V128]', r'valid-vload-val', r'exec-vload-val'), + Instruction(2.0, r'\V128.\VLOAD~x~\memarg', r'\hex{FD}~~\hex{00}', r'[\X{at}] \to [\V128]', r'valid-vload-num', r'exec-vload-num'), Instruction(2.0, r'\V128.\VLOAD\K{8x8\_s}~x~\memarg', r'\hex{FD}~~\hex{01}', r'[\X{at}] \to [\V128]', r'valid-vload-pack', r'exec-vload-pack'), Instruction(2.0, r'\V128.\VLOAD\K{8x8\_u}~x~\memarg', r'\hex{FD}~~\hex{02}', r'[\X{at}] \to [\V128]', r'valid-vload-pack', r'exec-vload-pack'), Instruction(2.0, r'\V128.\VLOAD\K{16x4\_s}~x~\memarg', r'\hex{FD}~~\hex{03}', r'[\X{at}] \to [\V128]', r'valid-vload-pack', r'exec-vload-pack'), diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 373edf4576..04c53f82d5 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -551,13 +551,25 @@ Memory Instructions However, it may be substantially slower on some hardware. -.. _exec-load-val: +.. _exec-load-num: + +$${rule-prose: Step_read/load-num-*} + +$${rule: {Step_read/load-num-*}} + + .. _exec-load-pack: -.. _exec-vload-val: -$${rule-prose: Step_read/load} +$${rule-prose: Step_read/load-pack-*} + +$${rule: {Step_read/load-pack-*}} + + +.. _exec-vload-num: -$${rule: {Step_read/load-*}} +$${rule-prose: Step_read/vload-num-*} + +$${rule: {Step_read/vload-num-*}} .. _exec-vload-pack: @@ -588,13 +600,19 @@ $${rule-prose: Step_read/vload_lane} $${rule: {Step_read/vload_lane-*}} -.. _exec-store-val: +.. _exec-store-num: .. _exec-store-pack: -.. _exec-vstore: $${rule-prose: Step/store} -$${rule: {Step/store-* Step/vstore-*}} +$${rule: {Step/store-*}} + + +.. _exec-vstore: + +$${rule-prose: Step/vstore} + +$${rule: {Step/vstore-*}} .. _exec-vstore_lane: diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 52eff5b381..e80b1a3d25 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -569,14 +569,14 @@ $${rule-prose: Memarg_ok} $${rule: Memarg_ok} -.. _valid-load-val: +.. _valid-load-num: :math:`t\K{.}\LOAD~x~\memarg` ............................. -$${rule-prose: Instr_ok/load-val} +$${rule-prose: Instr_ok/load-num} -$${rule: Instr_ok/load-val} +$${rule: Instr_ok/load-num} .. _valid-load-pack: @@ -589,14 +589,14 @@ $${rule-prose: Instr_ok/load-pack} $${rule: Instr_ok/load-pack} -.. _valid-store-val: +.. _valid-store-num: :math:`t\K{.}\STORE~x~\memarg` .............................. -$${rule-prose: Instr_ok/store-val} +$${rule-prose: Instr_ok/store-num} -$${rule: Instr_ok/store-val} +$${rule: Instr_ok/store-num} .. _valid-store-pack: @@ -609,14 +609,14 @@ $${rule-prose: Instr_ok/store-pack} $${rule: Instr_ok/store-pack} -.. _valid-vload-val: +.. _valid-vload-num: :math:`\K{v128.}\LOAD~x~\memarg` -..................................... +................................ -$${rule-prose: Instr_ok/vload-val} +$${rule-prose: Instr_ok/vload-num} -$${rule: Instr_ok/vload-val} +$${rule: Instr_ok/vload-num} .. _valid-vload-pack: diff --git a/specification/wasm-3.0/2.3-validation.instructions.spectec b/specification/wasm-3.0/2.3-validation.instructions.spectec index 62ec9c61db..e9685d1cd8 100644 --- a/specification/wasm-3.0/2.3-validation.instructions.spectec +++ b/specification/wasm-3.0/2.3-validation.instructions.spectec @@ -448,7 +448,7 @@ rule Instr_ok/load: -- if K? = eps \/ nt = Inn ;) -rule Instr_ok/load-val: +rule Instr_ok/load-num: C |- LOAD nt x memarg : at -> nt -- if C.MEMS[x] = at lim PAGE -- Memarg_ok: |- memarg : at -> $size(nt) @@ -467,7 +467,7 @@ rule Instr_ok/store: -- if K? = eps \/ nt = Inn ;) -rule Instr_ok/store-val: +rule Instr_ok/store-num: C |- STORE nt x memarg : at nt -> eps -- if C.MEMS[x] = at lim PAGE -- Memarg_ok: |- memarg : at -> $size(nt) @@ -477,7 +477,7 @@ rule Instr_ok/store-pack: -- if C.MEMS[x] = at lim PAGE -- Memarg_ok: |- memarg : at -> K -rule Instr_ok/vload-val: +rule Instr_ok/vload-num: C |- VLOAD V128 x memarg : at -> V128 -- if C.MEMS[x] = at lim PAGE -- Memarg_ok: |- memarg : at -> $vsize(V128) diff --git a/specification/wasm-3.0/4.3-execution.instructions.spectec b/specification/wasm-3.0/4.3-execution.instructions.spectec index 36fe9daa9d..7df750f7a0 100644 --- a/specification/wasm-3.0/4.3-execution.instructions.spectec +++ b/specification/wasm-3.0/4.3-execution.instructions.spectec @@ -451,11 +451,11 @@ rule Step_read/load-pack-val: ---- -- if $ibytes_(n, c) = $mem(z, x).BYTES[i + ao.OFFSET : n/8] -rule Step_read/vload-oob: +rule Step_read/vload-num-oob: z; (CONST at i) (VLOAD V128 x ao) ~> TRAP -- if $(i + ao.OFFSET + $vsize(V128)/8 > |$mem(z, x).BYTES|) -rule Step_read/vload-val: +rule Step_read/vload-num-val: z; (CONST at i) (VLOAD V128 x ao) ~> (VCONST V128 c) -- if $vbytes_(V128, c) = $mem(z, x).BYTES[i + ao.OFFSET : $vsize(V128)/8] diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index 62ec9c61db..e9685d1cd8 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -448,7 +448,7 @@ rule Instr_ok/load: -- if K? = eps \/ nt = Inn ;) -rule Instr_ok/load-val: +rule Instr_ok/load-num: C |- LOAD nt x memarg : at -> nt -- if C.MEMS[x] = at lim PAGE -- Memarg_ok: |- memarg : at -> $size(nt) @@ -467,7 +467,7 @@ rule Instr_ok/store: -- if K? = eps \/ nt = Inn ;) -rule Instr_ok/store-val: +rule Instr_ok/store-num: C |- STORE nt x memarg : at nt -> eps -- if C.MEMS[x] = at lim PAGE -- Memarg_ok: |- memarg : at -> $size(nt) @@ -477,7 +477,7 @@ rule Instr_ok/store-pack: -- if C.MEMS[x] = at lim PAGE -- Memarg_ok: |- memarg : at -> K -rule Instr_ok/vload-val: +rule Instr_ok/vload-num: C |- VLOAD V128 x memarg : at -> V128 -- if C.MEMS[x] = at lim PAGE -- Memarg_ok: |- memarg : at -> $vsize(V128) diff --git a/specification/wasm-latest/4.3-execution.instructions.spectec b/specification/wasm-latest/4.3-execution.instructions.spectec index 36fe9daa9d..7df750f7a0 100644 --- a/specification/wasm-latest/4.3-execution.instructions.spectec +++ b/specification/wasm-latest/4.3-execution.instructions.spectec @@ -451,11 +451,11 @@ rule Step_read/load-pack-val: ---- -- if $ibytes_(n, c) = $mem(z, x).BYTES[i + ao.OFFSET : n/8] -rule Step_read/vload-oob: +rule Step_read/vload-num-oob: z; (CONST at i) (VLOAD V128 x ao) ~> TRAP -- if $(i + ao.OFFSET + $vsize(V128)/8 > |$mem(z, x).BYTES|) -rule Step_read/vload-val: +rule Step_read/vload-num-val: z; (CONST at i) (VLOAD V128 x ao) ~> (VCONST V128 c) -- if $vbytes_(V128, c) = $mem(z, x).BYTES[i + ao.OFFSET : $vsize(V128)/8] diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 47e8109b40..0b3e20844d 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -4275,7 +4275,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:451.1-454.44 - rule `load-val`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: + rule `load-num`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, LOAD_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)],), [], `%`_resulttype([(nt : numtype <: valtype)],))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $size(nt)) @@ -4287,7 +4287,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Memarg_ok: `|-%:%->%`(memarg, at, K) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:470.1-473.44 - rule `store-val`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: + rule `store-num`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) (nt : numtype <: valtype)],), [], `%`_resulttype([],))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $size(nt)) @@ -4299,7 +4299,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Memarg_ok: `|-%:%->%`(memarg, at, K) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:480.1-483.47 - rule `vload-val`{C : context, x : idx, memarg : memarg, at : addrtype, lim : limits}: + rule `vload-num`{C : context, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)],), [], `%`_resulttype([V128_valtype],))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $vsize(V128_vectype)) @@ -7103,12 +7103,12 @@ relation Step_read: `%~>%`(config, instr*) -- if ($ibytes_(n, c) = $mem(z, x).BYTES_meminst[(i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) : (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec - rule `vload-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg}: + rule `vload-num-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(), x, ao)]), [TRAP_instr]) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec - rule `vload-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg, c : vec_(V128_Vnn)}: + rule `vload-num-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg, c : vec_(V128_Vnn)}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(), x, ao)]), [VCONST_instr(V128_vectype, c)]) -- if ($vbytes_(V128_vectype, c) = $mem(z, x).BYTES_meminst[(i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) : ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 8bf9cc3a7d..6313ef72f7 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -6891,7 +6891,7 @@ C{.}\mathsf{mems}{}[x] = {\mathit{at}}~{\mathit{lim}}~\mathsf{page} {\vdash}\, {\mathit{memarg}} : {\mathit{at}} \rightarrow {|{\mathit{nt}}|} }{ C \vdash {\mathit{nt}}{.}\mathsf{load}~x~{\mathit{memarg}} : {\mathit{at}} \rightarrow {\mathit{nt}} -} \, {[\textsc{\scriptsize T{-}instr{-}load{-}val}]} +} \, {[\textsc{\scriptsize T{-}instr{-}load{-}num}]} \qquad \end{array} $$ @@ -6917,7 +6917,7 @@ C{.}\mathsf{mems}{}[x] = {\mathit{at}}~{\mathit{lim}}~\mathsf{page} {\vdash}\, {\mathit{memarg}} : {\mathit{at}} \rightarrow {|{\mathit{nt}}|} }{ C \vdash {\mathit{nt}}{.}\mathsf{store}~x~{\mathit{memarg}} : {\mathit{at}}~{\mathit{nt}} \rightarrow \epsilon -} \, {[\textsc{\scriptsize T{-}instr{-}store{-}val}]} +} \, {[\textsc{\scriptsize T{-}instr{-}store{-}num}]} \qquad \end{array} $$ @@ -6943,7 +6943,7 @@ C{.}\mathsf{mems}{}[x] = {\mathit{at}}~{\mathit{lim}}~\mathsf{page} {\vdash}\, {\mathit{memarg}} : {\mathit{at}} \rightarrow {|\mathsf{v{\scriptstyle 128}}|} }{ C \vdash \mathsf{v{\scriptstyle 128}}{.}\mathsf{load}~x~{\mathit{memarg}} : {\mathit{at}} \rightarrow \mathsf{v{\scriptstyle 128}} -} \, {[\textsc{\scriptsize T{-}instr{-}vload{-}val}]} +} \, {[\textsc{\scriptsize T{-}instr{-}vload{-}num}]} \qquad \end{array} $$ @@ -10241,8 +10241,8 @@ $$ &&& \multicolumn{2}{@{}l@{}}{\quad \quad \mbox{if}~ {{\mathrm{bytes}}}_{{\mathsf{i}}{n}}(c) = z{.}\mathsf{mems}{}[x]{.}\mathsf{bytes}{}[i + {\mathit{ao}}{.}\mathsf{offset} : n / 8] } \\ -{[\textsc{\scriptsize E{-}vload{-}oob}]} \quad & z ; ({\mathit{at}}{.}\mathsf{const}~i)~(\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}~x~{\mathit{ao}}) & \hookrightarrow & \mathsf{trap} & \quad \mbox{if}~ i + {\mathit{ao}}{.}\mathsf{offset} + {|\mathsf{v{\scriptstyle 128}}|} / 8 > {|z{.}\mathsf{mems}{}[x]{.}\mathsf{bytes}|} \\ -{[\textsc{\scriptsize E{-}vload{-}val}]} \quad & z ; ({\mathit{at}}{.}\mathsf{const}~i)~(\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}~x~{\mathit{ao}}) & \hookrightarrow & (\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c) & \quad \mbox{if}~ {{\mathrm{bytes}}}_{\mathsf{v{\scriptstyle 128}}}(c) = z{.}\mathsf{mems}{}[x]{.}\mathsf{bytes}{}[i + {\mathit{ao}}{.}\mathsf{offset} : {|\mathsf{v{\scriptstyle 128}}|} / 8] \\ +{[\textsc{\scriptsize E{-}vload{-}num{-}oob}]} \quad & z ; ({\mathit{at}}{.}\mathsf{const}~i)~(\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}~x~{\mathit{ao}}) & \hookrightarrow & \mathsf{trap} & \quad \mbox{if}~ i + {\mathit{ao}}{.}\mathsf{offset} + {|\mathsf{v{\scriptstyle 128}}|} / 8 > {|z{.}\mathsf{mems}{}[x]{.}\mathsf{bytes}|} \\ +{[\textsc{\scriptsize E{-}vload{-}num{-}val}]} \quad & z ; ({\mathit{at}}{.}\mathsf{const}~i)~(\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}~x~{\mathit{ao}}) & \hookrightarrow & (\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c) & \quad \mbox{if}~ {{\mathrm{bytes}}}_{\mathsf{v{\scriptstyle 128}}}(c) = z{.}\mathsf{mems}{}[x]{.}\mathsf{bytes}{}[i + {\mathit{ao}}{.}\mathsf{offset} : {|\mathsf{v{\scriptstyle 128}}|} / 8] \\ \end{array} $$ diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 0ffd418d5e..ee68858b29 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -3798,7 +3798,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:451.1-454.44 - rule `load-val`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: + rule `load-num`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, LOAD_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)],), [], `%`_resulttype([(nt : numtype <: valtype)],))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $size(nt)) @@ -3810,7 +3810,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Memarg_ok: `|-%:%->%`(memarg, at, K) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:470.1-473.44 - rule `store-val`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: + rule `store-num`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) (nt : numtype <: valtype)],), [], `%`_resulttype([],))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $size(nt)) @@ -3822,7 +3822,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Memarg_ok: `|-%:%->%`(memarg, at, K) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:480.1-483.47 - rule `vload-val`{C : context, x : idx, memarg : memarg, at : addrtype, lim : limits}: + rule `vload-num`{C : context, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)],), [], `%`_resulttype([V128_valtype],))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $vsize(V128_vectype)) @@ -6626,12 +6626,12 @@ relation Step_read: `%~>%`(config, instr*) -- if ($ibytes_(n, c) = $mem(z, x).BYTES_meminst[(i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) : (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec - rule `vload-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg}: + rule `vload-num-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(), x, ao)]), [TRAP_instr]) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec - rule `vload-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg, c : vec_(V128_Vnn)}: + rule `vload-num-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg, c : vec_(V128_Vnn)}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(), x, ao)]), [VCONST_instr(V128_vectype, c)]) -- if ($vbytes_(V128_vectype, c) = $mem(z, x).BYTES_meminst[(i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) : ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]) @@ -15707,7 +15707,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:451.1-454.44 - rule `load-val`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: + rule `load-num`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, LOAD_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)],), [], `%`_resulttype([(nt : numtype <: valtype)],))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $size(nt)) @@ -15719,7 +15719,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Memarg_ok: `|-%:%->%`(memarg, at, K) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:470.1-473.44 - rule `store-val`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: + rule `store-num`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) (nt : numtype <: valtype)],), [], `%`_resulttype([],))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $size(nt)) @@ -15731,7 +15731,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Memarg_ok: `|-%:%->%`(memarg, at, K) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:480.1-483.47 - rule `vload-val`{C : context, x : idx, memarg : memarg, at : addrtype, lim : limits}: + rule `vload-num`{C : context, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)],), [], `%`_resulttype([V128_valtype],))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $vsize(V128_vectype)) @@ -18537,12 +18537,12 @@ relation Step_read: `%~>%`(config, instr*) -- if ($ibytes_(n, c) = $mem(z, x).BYTES_meminst[(i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) : (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec - rule `vload-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg}: + rule `vload-num-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(), x, ao)]), [TRAP_instr]) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec - rule `vload-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg, c : vec_(V128_Vnn)}: + rule `vload-num-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg, c : vec_(V128_Vnn)}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(), x, ao)]), [VCONST_instr(V128_vectype, c)]) -- if ($vbytes_(V128_vectype, c) = $mem(z, x).BYTES_meminst[(i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) : ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]) @@ -27711,7 +27711,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:451.1-454.44 - rule `load-val`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: + rule `load-num`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, LOAD_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)],), [], `%`_resulttype([(nt : numtype <: valtype)],))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) @@ -27725,7 +27725,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Memarg_ok: `|-%:%->%`(memarg, at, K) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:470.1-473.44 - rule `store-val`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: + rule `store-num`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) (nt : numtype <: valtype)],), [], `%`_resulttype([],))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) @@ -27739,7 +27739,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Memarg_ok: `|-%:%->%`(memarg, at, K) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:480.1-483.47 - rule `vload-val`{C : context, x : idx, memarg : memarg, at : addrtype, lim : limits}: + rule `vload-num`{C : context, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)],), [], `%`_resulttype([V128_valtype],))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) @@ -30605,12 +30605,12 @@ relation Step_read: `%~>%`(config, instr*) -- if ($ibytes_(n, c) = $mem(z, x).BYTES_meminst[(i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) : (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec - rule `vload-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg}: + rule `vload-num-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(), x, ao)]), [TRAP_instr]) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec - rule `vload-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg, c : vec_(V128_Vnn)}: + rule `vload-num-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), x : idx, ao : memarg, c : vec_(V128_Vnn)}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(), x, ao)]), [VCONST_instr(V128_vectype, c)]) -- if ($vbytes_(V128_vectype, c) = $mem(z, x).BYTES_meminst[(i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) : ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]) diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index d231327386..171d1e1a4d 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -18782,6 +18782,25 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i #. Push the value :math:`({\mathsf{i}}{N}{.}\mathsf{const}~{{{{\mathrm{extend}}}_{n, {|{\mathsf{i}}{N}|}}^{{\mathit{sx}}}}}{(c)})` to the stack. +:math:`\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}~x~{\mathit{ao}}` +.................................................................... + + +1. Let :math:`z` be the current state. + +#. Assert: Due to validation, a number value is on the top of the stack. + +#. Pop the value :math:`({\mathit{at}}{.}\mathsf{const}~i)` from the stack. + +#. If :math:`i + {\mathit{ao}}{.}\mathsf{offset} + {|\mathsf{v{\scriptstyle 128}}|} / 8 > {|z{.}\mathsf{mems}{}[x]{.}\mathsf{bytes}|}`, then: + + a. Trap. + +#. Let :math:`c` be the result for which :math:`{{\mathrm{bytes}}}_{\mathsf{v{\scriptstyle 128}}}(c)` :math:`=` :math:`z{.}\mathsf{mems}{}[x]{.}\mathsf{bytes}{}[i + {\mathit{ao}}{.}\mathsf{offset} : {|\mathsf{v{\scriptstyle 128}}|} / 8]`. + +#. Push the value :math:`(\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c)` to the stack. + + :math:`{\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}}{{K}{\mathsf{x}}{M}{\mathsf{\_}}{{\mathit{sx}}}}~x~{\mathit{ao}}` ...................................................................................................................... @@ -29110,7 +29129,7 @@ Instr_ok/select-impl - t matches the value type t'. - t' is numtype or t' is vectype. -Instr_ok/load-val +Instr_ok/load-num - the instruction (LOAD nt ?() x memarg) is valid with the instruction type [at] -> [nt] if: - the memory C.MEMS[x] exists. - C.MEMS[x] is at lim PAGE. @@ -29122,7 +29141,7 @@ Instr_ok/load-pack - C.MEMS[x] is at lim PAGE. - memarg is valid for at and K. -Instr_ok/store-val +Instr_ok/store-num - the instruction (STORE nt ?() x memarg) is valid with the instruction type [at, nt] -> [] if: - the memory C.MEMS[x] exists. - C.MEMS[x] is at lim PAGE. @@ -29134,7 +29153,7 @@ Instr_ok/store-pack - C.MEMS[x] is at lim PAGE. - memarg is valid for at and K. -Instr_ok/vload-val +Instr_ok/vload-num - the instruction (VLOAD V128 ?() x memarg) is valid with the instruction type [at] -> [V128] if: - the memory C.MEMS[x] exists. - C.MEMS[x] is at lim PAGE. @@ -30314,6 +30333,15 @@ Step_read/load-pack-* Inn ?(n _ sx) x ao 5. Let c be $ibytes__1^-1(n, $mem(z, x).BYTES[(i + ao.OFFSET) : (n / 8)]). 6. Push the value (Inn.CONST $extend__(n, $size(Inn), sx, c)) to the stack. +Step_read/vload-num-* V128 ?() x ao +1. Let z be the current state. +2. Assert: Due to validation, a value of value type num is on the top of the stack. +3. Pop the value (at.CONST i) from the stack. +4. If (((i + ao.OFFSET) + ($vsize(V128) / 8)) > |$mem(z, x).BYTES|), then: + a. Trap. +5. Let c be $vbytes__1^-1(V128, $mem(z, x).BYTES[(i + ao.OFFSET) : ($vsize(V128) / 8)]). +6. Push the value (V128.CONST c) to the stack. + Step_read/vload-pack-* V128 ?((SHAPE K X M _ sx)) x ao 1. Let z be the current state. 2. Assert: Due to validation, a value of value type num is on the top of the stack. diff --git a/spectec/test-prose/doc/valid/instructions-in.rst b/spectec/test-prose/doc/valid/instructions-in.rst index bc1eeff52e..005ed403ab 100644 --- a/spectec/test-prose/doc/valid/instructions-in.rst +++ b/spectec/test-prose/doc/valid/instructions-in.rst @@ -597,7 +597,7 @@ $${rule-prose: Instr_ok/load} \ -$${rule: Instr_ok/load-val} +$${rule: Instr_ok/load-num} $${rule: Instr_ok/load-pack} .. _valid-store: @@ -606,7 +606,7 @@ $${rule-prose: Instr_ok/store} \ -$${rule: Instr_ok/store-val} +$${rule: Instr_ok/store-num} $${rule: Instr_ok/store-pack} .. _valid-vload: @@ -615,7 +615,7 @@ $${rule-prose: Instr_ok/vload} \ -$${rule: Instr_ok/vload-val} +$${rule: Instr_ok/vload-num} $${rule: Instr_ok/vload-pack} $${rule: Instr_ok/vload-splat} $${rule: Instr_ok/vload-zero} diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index 15420bc04d..05fbca79d2 100644 --- a/spectec/test-splice/TEST.md +++ b/spectec/test-splice/TEST.md @@ -1145,11 +1145,11 @@ warning: rule `Instr_ok/memory.fill` was never spliced warning: rule `Instr_ok/memory.copy` was never spliced warning: rule `Instr_ok/memory.init` was never spliced warning: rule `Instr_ok/data.drop` was never spliced -warning: rule `Instr_ok/load-val` was never spliced +warning: rule `Instr_ok/load-num` was never spliced warning: rule `Instr_ok/load-pack` was never spliced -warning: rule `Instr_ok/store-val` was never spliced +warning: rule `Instr_ok/store-num` was never spliced warning: rule `Instr_ok/store-pack` was never spliced -warning: rule `Instr_ok/vload-val` was never spliced +warning: rule `Instr_ok/vload-num` was never spliced warning: rule `Instr_ok/vload-pack` was never spliced warning: rule `Instr_ok/vload-splat` was never spliced warning: rule `Instr_ok/vload-zero` was never spliced @@ -1405,8 +1405,8 @@ warning: rule `Step_read/load-num-oob` was never spliced warning: rule `Step_read/load-num-val` was never spliced warning: rule `Step_read/load-pack-oob` was never spliced warning: rule `Step_read/load-pack-val` was never spliced -warning: rule `Step_read/vload-oob` was never spliced -warning: rule `Step_read/vload-val` was never spliced +warning: rule `Step_read/vload-num-oob` was never spliced +warning: rule `Step_read/vload-num-val` was never spliced warning: rule `Step_read/vload-pack-oob` was never spliced warning: rule `Step_read/vload-pack-val` was never spliced warning: rule `Step_read/vload-splat-oob` was never spliced @@ -2126,8 +2126,8 @@ warning: rule prose `Instr_ok/global.set` was never spliced warning: rule prose `Instr_ok/i31.get` was never spliced warning: rule prose `Instr_ok/if` was never spliced warning: rule prose `Instr_ok/load` was never spliced +warning: rule prose `Instr_ok/load-num` was never spliced warning: rule prose `Instr_ok/load-pack` was never spliced -warning: rule prose `Instr_ok/load-val` was never spliced warning: rule prose `Instr_ok/local.get` was never spliced warning: rule prose `Instr_ok/local.set` was never spliced warning: rule prose `Instr_ok/local.tee` was never spliced @@ -2155,8 +2155,8 @@ warning: rule prose `Instr_ok/select` was never spliced warning: rule prose `Instr_ok/select-expl` was never spliced warning: rule prose `Instr_ok/select-impl` was never spliced warning: rule prose `Instr_ok/store` was never spliced +warning: rule prose `Instr_ok/store-num` was never spliced warning: rule prose `Instr_ok/store-pack` was never spliced -warning: rule prose `Instr_ok/store-val` was never spliced warning: rule prose `Instr_ok/struct.get` was never spliced warning: rule prose `Instr_ok/struct.new` was never spliced warning: rule prose `Instr_ok/struct.new_default` was never spliced @@ -2183,9 +2183,9 @@ warning: rule prose `Instr_ok/vextract_lane` was never spliced warning: rule prose `Instr_ok/vextternop` was never spliced warning: rule prose `Instr_ok/vextunop` was never spliced warning: rule prose `Instr_ok/vload` was never spliced +warning: rule prose `Instr_ok/vload-num` was never spliced warning: rule prose `Instr_ok/vload-pack` was never spliced warning: rule prose `Instr_ok/vload-splat` was never spliced -warning: rule prose `Instr_ok/vload-val` was never spliced warning: rule prose `Instr_ok/vload-zero` was never spliced warning: rule prose `Instr_ok/vload_lane` was never spliced warning: rule prose `Instr_ok/vnarrow` was never spliced @@ -2397,6 +2397,7 @@ warning: rule prose `Step_read/throw_ref-handler-*` was never spliced warning: rule prose `Step_read/throw_ref-instrs-*` was never spliced warning: rule prose `Step_read/try_table` was never spliced warning: rule prose `Step_read/vload` was never spliced +warning: rule prose `Step_read/vload-num-*` was never spliced warning: rule prose `Step_read/vload-pack-*` was never spliced warning: rule prose `Step_read/vload-splat-*` was never spliced warning: rule prose `Step_read/vload-zero-*` was never spliced