From d63d22b613bd1d97673ef3ee6923e5ad91530d59 Mon Sep 17 00:00:00 2001 From: Zilin Chen Date: Fri, 30 Jan 2026 21:10:37 +0800 Subject: [PATCH] [spec] add missing rules for HANDLER --- .../4.3-execution.instructions.spectec | 7 + spectec/test-frontend/TEST.md | 63 +++--- spectec/test-latex/TEST.md | 2 + spectec/test-middlend/TEST.md | 189 ++++++++++-------- spectec/test-splice/TEST.md | 2 + 5 files changed, 155 insertions(+), 108 deletions(-) diff --git a/specification/wasm-3.0/4.3-execution.instructions.spectec b/specification/wasm-3.0/4.3-execution.instructions.spectec index bde165a665..8ed03426ac 100644 --- a/specification/wasm-3.0/4.3-execution.instructions.spectec +++ b/specification/wasm-3.0/4.3-execution.instructions.spectec @@ -38,6 +38,10 @@ rule Step/ctxt-label: z; (LABEL_ n `{instr_0*} instr*) ~> z'; (LABEL_ n `{instr_0*} instr'*) -- Step: z; instr* ~> z'; instr'* +rule Step/ctxt-handler: + z; (HANDLER_ n `{catch*} instr*) ~> z'; (HANDLER_ n `{catch*} instr'*) + -- Step: z; instr* ~> z'; instr'* + rule Step/ctxt-frame: s; f; (FRAME_ n `{f'} instr*) ~> s'; f; (FRAME_ n `{f''} instr'*) -- Step: s; f'; instr* ~> s'; f''; instr'* @@ -289,6 +293,9 @@ rule Step_pure/trap-instrs: rule Step_pure/trap-label: (LABEL_ n `{instr'*} TRAP) ~> TRAP +rule Step_pure/trap-handler: + (HANDLER_ n `{catch*} TRAP) ~> TRAP + rule Step_pure/trap-frame: (FRAME_ n `{f} TRAP) ~> TRAP diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index e1fee92447..fbc99ad21e 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -6079,6 +6079,10 @@ relation Step_pure: `%~>%`(instr*, instr*) rule `trap-label`{n : n, `instr'*` : instr*}: `%~>%`([`LABEL_%{%}%`_instr(n, instr'*{instr' <- `instr'*`}, [TRAP_instr])], [TRAP_instr]) + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec + rule `trap-handler`{n : n, `catch*` : catch*}: + `%~>%`([`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, [TRAP_instr])], [TRAP_instr]) + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule `trap-frame`{n : n, f : frame}: `%~>%`([`FRAME_%{%}%`_instr(n, f, [TRAP_instr])], [TRAP_instr]) @@ -6904,136 +6908,141 @@ relation Step: `%~>%`(config, config) `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_instr(n, instr_0*{instr_0 <- `instr_0*`}, instr*{instr <- `instr*`})]), `%;%`_config(z', [`LABEL_%{%}%`_instr(n, instr_0*{instr_0 <- `instr_0*`}, instr'*{instr' <- `instr'*`})])) -- Step: `%~>%`(`%;%`_config(z, instr*{instr <- `instr*`}), `%;%`_config(z', instr'*{instr' <- `instr'*`})) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:41.1-43.45 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:41.1-43.36 + rule `ctxt-handler`{z : state, n : n, `catch*` : catch*, `instr*` : instr*, z' : state, `instr'*` : instr*}: + `%~>%`(`%;%`_config(z, [`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`})]), `%;%`_config(z', [`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr'*{instr' <- `instr'*`})])) + -- Step: `%~>%`(`%;%`_config(z, instr*{instr <- `instr*`}), `%;%`_config(z', instr'*{instr' <- `instr'*`})) + + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:45.1-47.45 rule `ctxt-frame`{s : store, f : frame, n : n, f' : frame, `instr*` : instr*, s' : store, f'' : frame, `instr'*` : instr*}: `%~>%`(`%;%`_config(`%;%`_state(s, f), [`FRAME_%{%}%`_instr(n, f', instr*{instr <- `instr*`})]), `%;%`_config(`%;%`_state(s', f), [`FRAME_%{%}%`_instr(n, f'', instr'*{instr' <- `instr'*`})])) -- Step: `%~>%`(`%;%`_config(`%;%`_state(s, f'), instr*{instr <- `instr*`}), `%;%`_config(`%;%`_state(s', f''), instr'*{instr' <- `instr'*`})) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:227.1-231.49 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:231.1-235.49 rule throw{z : state, `val*` : val*, n : n, x : idx, exn : exninst, a : addr, `t*` : valtype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [THROW_instr(x)]), `%;%`_config($add_exninst(z, [exn]), [REF.EXN_ADDR_instr(a) THROW_REF_instr])) -- Expand: `%~~%`($as_deftype($tag(z, x).TYPE_taginst), `FUNC%->%`_comptype(`%`_resulttype(t^n{t <- `t*`}), `%`_resulttype([]))) -- if (a = |$exninst(z)|) -- if (exn = {TAG $tagaddr(z)[x!`%`_idx.0], FIELDS val^n{val <- `val*`}}) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:302.1-303.56 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:309.1-310.56 rule local.set{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) LOCAL.SET_instr(x)]), `%;%`_config($with_local(z, x, val), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:315.1-316.58 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:322.1-323.58 rule global.set{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) GLOBAL.SET_instr(x)]), `%;%`_config($with_global(z, x, val), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:329.1-331.33 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:336.1-338.33 rule `table.set-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) TABLE.SET_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:333.1-335.32 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:340.1-342.32 rule `table.set-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) TABLE.SET_instr(x)]), `%;%`_config($with_table(z, x, i!`%`_num_.0, ref), [])) -- if (i!`%`_num_.0 < |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:344.1-347.46 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:351.1-354.46 rule `table.grow-succeed`{z : state, ref : ref, at : addrtype, n : n, x : idx, ti : tableinst}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n)) TABLE.GROW_instr(x)]), `%;%`_config($with_tableinst(z, x, ti), [CONST_instr((at : addrtype <: numtype), `%`_num_(|$table(z, x).REFS_tableinst|))])) -- if (ti = $growtable($table(z, x), n, ref)) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:349.1-350.87 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:356.1-357.87 rule `table.grow-fail`{z : state, ref : ref, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n)) TABLE.GROW_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int))))])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:410.1-411.51 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:417.1-418.51 rule elem.drop{z : state, x : idx}: `%~>%`(`%;%`_config(z, [ELEM.DROP_instr(x)]), `%;%`_config($with_elem(z, x, []), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:494.1-497.60 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:501.1-504.60 rule `store-num-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:499.1-503.29 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:506.1-510.29 rule `store-num-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $nbytes_(nt, c)) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:505.1-508.52 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:512.1-515.52 rule `store-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n))), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:510.1-514.52 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:517.1-521.52 rule `store-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n))), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $ibytes_(n, $wrap__($size((Inn : Inn <: numtype)), n, c))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:516.1-519.63 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:523.1-526.63 rule `vstore-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config(z, [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-3.0/4.3-execution.instructions.spectec:521.1-524.31 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:528.1-531.31 rule `vstore-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $vbytes_(V128_vectype, c)) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:527.1-530.50 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:534.1-537.50 rule `vstore_lane-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, ao, j)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + N) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:532.1-537.49 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:539.1-544.49 rule `vstore_lane-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx, `b*` : byte*, Jnn : Jnn, M : M}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, ao, j)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((N : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (N = $jsize(Jnn)) -- if ((M : nat <:> rat) = ((128 : nat <:> rat) / (N : nat <:> rat))) -- if (b*{b <- `b*`} = $ibytes_(N, `%`_iN($lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c)[j!`%`_laneidx.0]!`%`_lane_.0))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:546.1-549.37 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:553.1-556.37 rule `memory.grow-succeed`{z : state, at : addrtype, n : n, x : idx, mi : meminst}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n)) MEMORY.GROW_instr(x)]), `%;%`_config($with_meminst(z, x, mi), [CONST_instr((at : addrtype <: numtype), `%`_num_((((|$mem(z, x).BYTES_meminst| : nat <:> rat) / ((64 * $Ki) : nat <:> rat)) : rat <:> nat)))])) -- if (mi = $growmem($mem(z, x), n)) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:551.1-552.84 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:558.1-559.84 rule `memory.grow-fail`{z : state, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n)) MEMORY.GROW_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int))))])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:612.1-613.51 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:619.1-620.51 rule data.drop{z : state, x : idx}: `%~>%`(`%;%`_config(z, [DATA.DROP_instr(x)]), `%;%`_config($with_data(z, x, []), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:693.1-697.65 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:700.1-704.65 rule struct.new{z : state, `val*` : val*, n : n, x : idx, si : structinst, a : addr, `mut?*` : mut?*, `zt*` : storagetype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [STRUCT.NEW_instr(x)]), `%;%`_config($add_structinst(z, [si]), [REF.STRUCT_ADDR_instr(a)])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)^n{`mut?` <- `mut?*`, zt <- `zt*`}))) -- if (a = |$structinst(z)|) -- if (si = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`, zt <- `zt*`}}) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:714.1-715.53 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:721.1-722.53 rule `struct.set-null`{z : state, ht : heaptype, val : val, x : idx, i : u32}: `%~>%`(`%;%`_config(z, [REF.NULL_instr(ht) (val : val <: instr) STRUCT.SET_instr(x, i)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:717.1-720.46 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:724.1-727.46 rule `struct.set-struct`{z : state, a : addr, val : val, x : idx, i : u32, `zt*` : storagetype*, `mut?*` : mut?*}: `%~>%`(`%;%`_config(z, [REF.STRUCT_ADDR_instr(a) (val : val <: instr) STRUCT.SET_instr(x, i)]), `%;%`_config($with_struct(z, a, i!`%`_u32.0, $packfield_(zt*{zt <- `zt*`}[i!`%`_u32.0], val)), [])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`}))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:733.1-738.65 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:740.1-745.65 rule array.new_fixed{z : state, `val*` : val*, n : n, x : idx, ai : arrayinst, a : addr, `mut?` : mut?, zt : storagetype}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [ARRAY.NEW_FIXED_instr(x, `%`_u32(n))]), `%;%`_config($add_arrayinst(z, [ai]), [REF.ARRAY_ADDR_instr(a)])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if ((a = |$arrayinst(z)|) /\ (ai = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`}})) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:778.1-779.64 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:785.1-786.64 rule `array.set-null`{z : state, ht : heaptype, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [REF.NULL_instr(ht) CONST_instr(I32_numtype, i) (val : val <: instr) ARRAY.SET_instr(x)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:781.1-783.39 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:788.1-790.39 rule `array.set-oob`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [REF.ARRAY_ADDR_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) ARRAY.SET_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$arrayinst(z)[a].FIELDS_arrayinst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:785.1-788.44 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:792.1-795.44 rule `array.set-array`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx, zt : storagetype, `mut?` : mut?}: `%~>%`(`%;%`_config(z, [REF.ARRAY_ADDR_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) ARRAY.SET_instr(x)]), `%;%`_config($with_array(z, a, i!`%`_num_.0, $packfield_(zt, val)), [])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 5e4e6345c5..e13cfb488d 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -9643,6 +9643,7 @@ $$ {\land}~ {{\mathit{val}}^\ast} \neq \epsilon \lor {{\mathit{instr}}_1^\ast} \neq \epsilon \\ \end{array} \\ {[\textsc{\scriptsize E{-}ctxt{-}label}]} \quad & z ; ({{\mathsf{label}}_{n}}{\{ {{\mathit{instr}}_0^\ast} \}}~{{\mathit{instr}}^\ast}) & \hookrightarrow & {z'} ; ({{\mathsf{label}}_{n}}{\{ {{\mathit{instr}}_0^\ast} \}}~{{\mathit{instr}'}^\ast}) & \quad \mbox{if}~ z ; {{\mathit{instr}}^\ast} \hookrightarrow {z'} ; {{\mathit{instr}'}^\ast} \\ +{[\textsc{\scriptsize E{-}ctxt{-}handler}]} \quad & z ; ({{\mathsf{handler}}_{n}}{\{ {{\mathit{catch}}^\ast} \}}~{{\mathit{instr}}^\ast}) & \hookrightarrow & {z'} ; ({{\mathsf{handler}}_{n}}{\{ {{\mathit{catch}}^\ast} \}}~{{\mathit{instr}'}^\ast}) & \quad \mbox{if}~ z ; {{\mathit{instr}}^\ast} \hookrightarrow {z'} ; {{\mathit{instr}'}^\ast} \\ {[\textsc{\scriptsize E{-}ctxt{-}frame}]} \quad & s ; f ; ({{\mathsf{frame}}_{n}}{\{ {f'} \}}~{{\mathit{instr}}^\ast}) & \hookrightarrow & {s'} ; f ; ({{\mathsf{frame}}_{n}}{\{ {f''} \}}~{{\mathit{instr}'}^\ast}) & \quad \mbox{if}~ s ; {f'} ; {{\mathit{instr}}^\ast} \hookrightarrow {s'} ; {f''} ; {{\mathit{instr}'}^\ast} \\ \end{array} $$ @@ -9896,6 +9897,7 @@ $$ \begin{array}[t]{@{}lrcl@{}l@{}} {[\textsc{\scriptsize E{-}trap{-}instrs}]} \quad & {{\mathit{val}}^\ast}~\mathsf{trap}~{{\mathit{instr}}^\ast} & \hookrightarrow & \mathsf{trap} & \quad \mbox{if}~ {{\mathit{val}}^\ast} \neq \epsilon \lor {{\mathit{instr}}^\ast} \neq \epsilon \\ {[\textsc{\scriptsize E{-}trap{-}label}]} \quad & ({{\mathsf{label}}_{n}}{\{ {{\mathit{instr}'}^\ast} \}}~\mathsf{trap}) & \hookrightarrow & \mathsf{trap} \\ +{[\textsc{\scriptsize E{-}trap{-}handler}]} \quad & ({{\mathsf{handler}}_{n}}{\{ {{\mathit{catch}}^\ast} \}}~\mathsf{trap}) & \hookrightarrow & \mathsf{trap} \\ {[\textsc{\scriptsize E{-}trap{-}frame}]} \quad & ({{\mathsf{frame}}_{n}}{\{ f \}}~\mathsf{trap}) & \hookrightarrow & \mathsf{trap} \\ \end{array} $$ diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 98e1801b30..a4b3506adc 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -6069,6 +6069,10 @@ relation Step_pure: `%~>%`(instr*, instr*) rule `trap-label`{n : n, `instr'*` : instr*}: `%~>%`([`LABEL_%{%}%`_instr(n, instr'*{instr' <- `instr'*`}, [TRAP_instr])], [TRAP_instr]) + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec + rule `trap-handler`{n : n, `catch*` : catch*}: + `%~>%`([`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, [TRAP_instr])], [TRAP_instr]) + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule `trap-frame`{n : n, f : frame}: `%~>%`([`FRAME_%{%}%`_instr(n, f, [TRAP_instr])], [TRAP_instr]) @@ -6894,136 +6898,141 @@ relation Step: `%~>%`(config, config) `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_instr(n, instr_0*{instr_0 <- `instr_0*`}, instr*{instr <- `instr*`})]), `%;%`_config(z', [`LABEL_%{%}%`_instr(n, instr_0*{instr_0 <- `instr_0*`}, instr'*{instr' <- `instr'*`})])) -- Step: `%~>%`(`%;%`_config(z, instr*{instr <- `instr*`}), `%;%`_config(z', instr'*{instr' <- `instr'*`})) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:41.1-43.45 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:41.1-43.36 + rule `ctxt-handler`{z : state, n : n, `catch*` : catch*, `instr*` : instr*, z' : state, `instr'*` : instr*}: + `%~>%`(`%;%`_config(z, [`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`})]), `%;%`_config(z', [`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr'*{instr' <- `instr'*`})])) + -- Step: `%~>%`(`%;%`_config(z, instr*{instr <- `instr*`}), `%;%`_config(z', instr'*{instr' <- `instr'*`})) + + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:45.1-47.45 rule `ctxt-frame`{s : store, f : frame, n : n, f' : frame, `instr*` : instr*, s' : store, f'' : frame, `instr'*` : instr*}: `%~>%`(`%;%`_config(`%;%`_state(s, f), [`FRAME_%{%}%`_instr(n, f', instr*{instr <- `instr*`})]), `%;%`_config(`%;%`_state(s', f), [`FRAME_%{%}%`_instr(n, f'', instr'*{instr' <- `instr'*`})])) -- Step: `%~>%`(`%;%`_config(`%;%`_state(s, f'), instr*{instr <- `instr*`}), `%;%`_config(`%;%`_state(s', f''), instr'*{instr' <- `instr'*`})) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:227.1-231.49 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:231.1-235.49 rule throw{z : state, `val*` : val*, n : n, x : idx, exn : exninst, a : addr, `t*` : valtype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [THROW_instr(x)]), `%;%`_config($add_exninst(z, [exn]), [REF.EXN_ADDR_instr(a) THROW_REF_instr])) -- Expand: `%~~%`($as_deftype($tag(z, x).TYPE_taginst), `FUNC%->%`_comptype(`%`_resulttype(t^n{t <- `t*`}), `%`_resulttype([]))) -- if (a = |$exninst(z)|) -- if (exn = {TAG $tagaddr(z)[x!`%`_idx.0], FIELDS val^n{val <- `val*`}}) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:302.1-303.56 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:309.1-310.56 rule local.set{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) LOCAL.SET_instr(x)]), `%;%`_config($with_local(z, x, val), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:315.1-316.58 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:322.1-323.58 rule global.set{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) GLOBAL.SET_instr(x)]), `%;%`_config($with_global(z, x, val), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:329.1-331.33 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:336.1-338.33 rule `table.set-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) TABLE.SET_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:333.1-335.32 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:340.1-342.32 rule `table.set-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) TABLE.SET_instr(x)]), `%;%`_config($with_table(z, x, i!`%`_num_.0, ref), [])) -- if (i!`%`_num_.0 < |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:344.1-347.46 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:351.1-354.46 rule `table.grow-succeed`{z : state, ref : ref, at : addrtype, n : n, x : idx, ti : tableinst}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n)) TABLE.GROW_instr(x)]), `%;%`_config($with_tableinst(z, x, ti), [CONST_instr((at : addrtype <: numtype), `%`_num_(|$table(z, x).REFS_tableinst|))])) -- if (ti = $growtable($table(z, x), n, ref)) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:349.1-350.87 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:356.1-357.87 rule `table.grow-fail`{z : state, ref : ref, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n)) TABLE.GROW_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int))))])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:410.1-411.51 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:417.1-418.51 rule elem.drop{z : state, x : idx}: `%~>%`(`%;%`_config(z, [ELEM.DROP_instr(x)]), `%;%`_config($with_elem(z, x, []), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:494.1-497.60 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:501.1-504.60 rule `store-num-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:499.1-503.29 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:506.1-510.29 rule `store-num-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $nbytes_(nt, c)) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:505.1-508.52 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:512.1-515.52 rule `store-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n))), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:510.1-514.52 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:517.1-521.52 rule `store-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n))), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $ibytes_(n, $wrap__($size((Inn : Inn <: numtype)), n, c))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:516.1-519.63 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:523.1-526.63 rule `vstore-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config(z, [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-3.0/4.3-execution.instructions.spectec:521.1-524.31 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:528.1-531.31 rule `vstore-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $vbytes_(V128_vectype, c)) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:527.1-530.50 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:534.1-537.50 rule `vstore_lane-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, ao, j)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + N) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:532.1-537.49 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:539.1-544.49 rule `vstore_lane-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx, `b*` : byte*, Jnn : Jnn, M : M}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, ao, j)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((N : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (N = $jsize(Jnn)) -- if ((M : nat <:> rat) = ((128 : nat <:> rat) / (N : nat <:> rat))) -- if (b*{b <- `b*`} = $ibytes_(N, `%`_iN($lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c)[j!`%`_laneidx.0]!`%`_lane_.0))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:546.1-549.37 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:553.1-556.37 rule `memory.grow-succeed`{z : state, at : addrtype, n : n, x : idx, mi : meminst}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n)) MEMORY.GROW_instr(x)]), `%;%`_config($with_meminst(z, x, mi), [CONST_instr((at : addrtype <: numtype), `%`_num_((((|$mem(z, x).BYTES_meminst| : nat <:> rat) / ((64 * $Ki) : nat <:> rat)) : rat <:> nat)))])) -- if (mi = $growmem($mem(z, x), n)) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:551.1-552.84 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:558.1-559.84 rule `memory.grow-fail`{z : state, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n)) MEMORY.GROW_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int))))])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:612.1-613.51 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:619.1-620.51 rule data.drop{z : state, x : idx}: `%~>%`(`%;%`_config(z, [DATA.DROP_instr(x)]), `%;%`_config($with_data(z, x, []), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:693.1-697.65 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:700.1-704.65 rule struct.new{z : state, `val*` : val*, n : n, x : idx, si : structinst, a : addr, `mut?*` : mut?*, `zt*` : storagetype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [STRUCT.NEW_instr(x)]), `%;%`_config($add_structinst(z, [si]), [REF.STRUCT_ADDR_instr(a)])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)^n{`mut?` <- `mut?*`, zt <- `zt*`}))) -- if (a = |$structinst(z)|) -- if (si = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`, zt <- `zt*`}}) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:714.1-715.53 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:721.1-722.53 rule `struct.set-null`{z : state, ht : heaptype, val : val, x : idx, i : u32}: `%~>%`(`%;%`_config(z, [REF.NULL_instr(ht) (val : val <: instr) STRUCT.SET_instr(x, i)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:717.1-720.46 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:724.1-727.46 rule `struct.set-struct`{z : state, a : addr, val : val, x : idx, i : u32, `zt*` : storagetype*, `mut?*` : mut?*}: `%~>%`(`%;%`_config(z, [REF.STRUCT_ADDR_instr(a) (val : val <: instr) STRUCT.SET_instr(x, i)]), `%;%`_config($with_struct(z, a, i!`%`_u32.0, $packfield_(zt*{zt <- `zt*`}[i!`%`_u32.0], val)), [])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`}))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:733.1-738.65 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:740.1-745.65 rule array.new_fixed{z : state, `val*` : val*, n : n, x : idx, ai : arrayinst, a : addr, `mut?` : mut?, zt : storagetype}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [ARRAY.NEW_FIXED_instr(x, `%`_u32(n))]), `%;%`_config($add_arrayinst(z, [ai]), [REF.ARRAY_ADDR_instr(a)])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if ((a = |$arrayinst(z)|) /\ (ai = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`}})) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:778.1-779.64 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:785.1-786.64 rule `array.set-null`{z : state, ht : heaptype, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [REF.NULL_instr(ht) CONST_instr(I32_numtype, i) (val : val <: instr) ARRAY.SET_instr(x)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:781.1-783.39 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:788.1-790.39 rule `array.set-oob`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [REF.ARRAY_ADDR_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) ARRAY.SET_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$arrayinst(z)[a].FIELDS_arrayinst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:785.1-788.44 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:792.1-795.44 rule `array.set-array`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx, zt : storagetype, `mut?` : mut?}: `%~>%`(`%;%`_config(z, [REF.ARRAY_ADDR_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) ARRAY.SET_instr(x)]), `%;%`_config($with_array(z, a, i!`%`_num_.0, $packfield_(zt, val)), [])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) @@ -17425,6 +17434,10 @@ relation Step_pure: `%~>%`(instr*, instr*) rule `trap-label`{n : n, `instr'*` : instr*}: `%~>%`([`LABEL_%{%}%`_instr(n, instr'*{instr' <- `instr'*`}, [TRAP_instr])], [TRAP_instr]) + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec + rule `trap-handler`{n : n, `catch*` : catch*}: + `%~>%`([`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, [TRAP_instr])], [TRAP_instr]) + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule `trap-frame`{n : n, f : frame}: `%~>%`([`FRAME_%{%}%`_instr(n, f, [TRAP_instr])], [TRAP_instr]) @@ -18250,136 +18263,141 @@ relation Step: `%~>%`(config, config) `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_instr(n, instr_0*{instr_0 <- `instr_0*`}, instr*{instr <- `instr*`})]), `%;%`_config(z', [`LABEL_%{%}%`_instr(n, instr_0*{instr_0 <- `instr_0*`}, instr'*{instr' <- `instr'*`})])) -- Step: `%~>%`(`%;%`_config(z, instr*{instr <- `instr*`}), `%;%`_config(z', instr'*{instr' <- `instr'*`})) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:41.1-43.45 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:41.1-43.36 + rule `ctxt-handler`{z : state, n : n, `catch*` : catch*, `instr*` : instr*, z' : state, `instr'*` : instr*}: + `%~>%`(`%;%`_config(z, [`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`})]), `%;%`_config(z', [`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr'*{instr' <- `instr'*`})])) + -- Step: `%~>%`(`%;%`_config(z, instr*{instr <- `instr*`}), `%;%`_config(z', instr'*{instr' <- `instr'*`})) + + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:45.1-47.45 rule `ctxt-frame`{s : store, f : frame, n : n, f' : frame, `instr*` : instr*, s' : store, f'' : frame, `instr'*` : instr*}: `%~>%`(`%;%`_config(`%;%`_state(s, f), [`FRAME_%{%}%`_instr(n, f', instr*{instr <- `instr*`})]), `%;%`_config(`%;%`_state(s', f), [`FRAME_%{%}%`_instr(n, f'', instr'*{instr' <- `instr'*`})])) -- Step: `%~>%`(`%;%`_config(`%;%`_state(s, f'), instr*{instr <- `instr*`}), `%;%`_config(`%;%`_state(s', f''), instr'*{instr' <- `instr'*`})) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:227.1-231.49 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:231.1-235.49 rule throw{z : state, `val*` : val*, n : n, x : idx, exn : exninst, a : addr, `t*` : valtype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [THROW_instr(x)]), `%;%`_config($add_exninst(z, [exn]), [REF.EXN_ADDR_instr(a) THROW_REF_instr])) -- Expand: `%~~%`($as_deftype($tag(z, x).TYPE_taginst), `FUNC%->%`_comptype(`%`_resulttype(t^n{t <- `t*`}), `%`_resulttype([]))) -- if (a = |$exninst(z)|) -- if (exn = {TAG $tagaddr(z)[x!`%`_idx.0], FIELDS val^n{val <- `val*`}}) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:302.1-303.56 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:309.1-310.56 rule local.set{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) LOCAL.SET_instr(x)]), `%;%`_config($with_local(z, x, val), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:315.1-316.58 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:322.1-323.58 rule global.set{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) GLOBAL.SET_instr(x)]), `%;%`_config($with_global(z, x, val), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:329.1-331.33 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:336.1-338.33 rule `table.set-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) TABLE.SET_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:333.1-335.32 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:340.1-342.32 rule `table.set-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) TABLE.SET_instr(x)]), `%;%`_config($with_table(z, x, i!`%`_num_.0, ref), [])) -- if (i!`%`_num_.0 < |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:344.1-347.46 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:351.1-354.46 rule `table.grow-succeed`{z : state, ref : ref, at : addrtype, n : n, x : idx, ti : tableinst}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n)) TABLE.GROW_instr(x)]), `%;%`_config($with_tableinst(z, x, ti), [CONST_instr((at : addrtype <: numtype), `%`_num_(|$table(z, x).REFS_tableinst|))])) -- if (ti = !($growtable($table(z, x), n, ref))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:349.1-350.87 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:356.1-357.87 rule `table.grow-fail`{z : state, ref : ref, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n)) TABLE.GROW_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int))))])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:410.1-411.51 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:417.1-418.51 rule elem.drop{z : state, x : idx}: `%~>%`(`%;%`_config(z, [ELEM.DROP_instr(x)]), `%;%`_config($with_elem(z, x, []), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:494.1-497.60 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:501.1-504.60 rule `store-num-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:499.1-503.29 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:506.1-510.29 rule `store-num-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $nbytes_(nt, c)) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:505.1-508.52 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:512.1-515.52 rule `store-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n))), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:510.1-514.52 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:517.1-521.52 rule `store-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n))), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $ibytes_(n, $wrap__($size((Inn : Inn <: numtype)), n, c))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:516.1-519.63 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:523.1-526.63 rule `vstore-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config(z, [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-3.0/4.3-execution.instructions.spectec:521.1-524.31 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:528.1-531.31 rule `vstore-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $vbytes_(V128_vectype, c)) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:527.1-530.50 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:534.1-537.50 rule `vstore_lane-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, ao, j)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + N) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:532.1-537.49 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:539.1-544.49 rule `vstore_lane-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx, `b*` : byte*, Jnn : Jnn, M : M}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, ao, j)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((N : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (N = $jsize(Jnn)) -- if ((M : nat <:> rat) = ((128 : nat <:> rat) / (N : nat <:> rat))) -- if (b*{b <- `b*`} = $ibytes_(N, `%`_iN($lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c)[j!`%`_laneidx.0]!`%`_lane_.0))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:546.1-549.37 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:553.1-556.37 rule `memory.grow-succeed`{z : state, at : addrtype, n : n, x : idx, mi : meminst}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n)) MEMORY.GROW_instr(x)]), `%;%`_config($with_meminst(z, x, mi), [CONST_instr((at : addrtype <: numtype), `%`_num_((((|$mem(z, x).BYTES_meminst| : nat <:> rat) / ((64 * $Ki) : nat <:> rat)) : rat <:> nat)))])) -- if (mi = !($growmem($mem(z, x), n))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:551.1-552.84 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:558.1-559.84 rule `memory.grow-fail`{z : state, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n)) MEMORY.GROW_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int))))])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:612.1-613.51 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:619.1-620.51 rule data.drop{z : state, x : idx}: `%~>%`(`%;%`_config(z, [DATA.DROP_instr(x)]), `%;%`_config($with_data(z, x, []), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:693.1-697.65 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:700.1-704.65 rule struct.new{z : state, `val*` : val*, n : n, x : idx, si : structinst, a : addr, `mut?*` : mut?*, `zt*` : storagetype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [STRUCT.NEW_instr(x)]), `%;%`_config($add_structinst(z, [si]), [REF.STRUCT_ADDR_instr(a)])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)^n{`mut?` <- `mut?*`, zt <- `zt*`}))) -- if (a = |$structinst(z)|) -- if (si = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`, zt <- `zt*`}}) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:714.1-715.53 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:721.1-722.53 rule `struct.set-null`{z : state, ht : heaptype, val : val, x : idx, i : u32}: `%~>%`(`%;%`_config(z, [REF.NULL_instr(ht) (val : val <: instr) STRUCT.SET_instr(x, i)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:717.1-720.46 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:724.1-727.46 rule `struct.set-struct`{z : state, a : addr, val : val, x : idx, i : u32, `zt*` : storagetype*, `mut?*` : mut?*}: `%~>%`(`%;%`_config(z, [REF.STRUCT_ADDR_instr(a) (val : val <: instr) STRUCT.SET_instr(x, i)]), `%;%`_config($with_struct(z, a, i!`%`_u32.0, $packfield_(zt*{zt <- `zt*`}[i!`%`_u32.0], val)), [])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`}))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:733.1-738.65 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:740.1-745.65 rule array.new_fixed{z : state, `val*` : val*, n : n, x : idx, ai : arrayinst, a : addr, `mut?` : mut?, zt : storagetype}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [ARRAY.NEW_FIXED_instr(x, `%`_u32(n))]), `%;%`_config($add_arrayinst(z, [ai]), [REF.ARRAY_ADDR_instr(a)])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if ((a = |$arrayinst(z)|) /\ (ai = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`}})) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:778.1-779.64 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:785.1-786.64 rule `array.set-null`{z : state, ht : heaptype, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [REF.NULL_instr(ht) CONST_instr(I32_numtype, i) (val : val <: instr) ARRAY.SET_instr(x)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:781.1-783.39 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:788.1-790.39 rule `array.set-oob`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [REF.ARRAY_ADDR_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) ARRAY.SET_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$arrayinst(z)[a].FIELDS_arrayinst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:785.1-788.44 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:792.1-795.44 rule `array.set-array`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx, zt : storagetype, `mut?` : mut?}: `%~>%`(`%;%`_config(z, [REF.ARRAY_ADDR_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) ARRAY.SET_instr(x)]), `%;%`_config($with_array(z, a, i!`%`_num_.0, $packfield_(zt, val)), [])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) @@ -28914,6 +28932,10 @@ relation Step_pure: `%~>%`(instr*, instr*) rule `trap-label`{n : n, `instr'*` : instr*}: `%~>%`([`LABEL_%{%}%`_instr(n, instr'*{instr' <- `instr'*`}, [TRAP_instr])], [TRAP_instr]) + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec + rule `trap-handler`{n : n, `catch*` : catch*}: + `%~>%`([`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, [TRAP_instr])], [TRAP_instr]) + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec rule `trap-frame`{n : n, f : frame}: `%~>%`([`FRAME_%{%}%`_instr(n, f, [TRAP_instr])], [TRAP_instr]) @@ -29779,12 +29801,17 @@ relation Step: `%~>%`(config, config) `%~>%`(`%;%`_config(z, [`LABEL_%{%}%`_instr(n, instr_0*{instr_0 <- `instr_0*`}, instr*{instr <- `instr*`})]), `%;%`_config(z', [`LABEL_%{%}%`_instr(n, instr_0*{instr_0 <- `instr_0*`}, instr'*{instr' <- `instr'*`})])) -- Step: `%~>%`(`%;%`_config(z, instr*{instr <- `instr*`}), `%;%`_config(z', instr'*{instr' <- `instr'*`})) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:41.1-43.45 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:41.1-43.36 + rule `ctxt-handler`{z : state, n : n, `catch*` : catch*, `instr*` : instr*, z' : state, `instr'*` : instr*}: + `%~>%`(`%;%`_config(z, [`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`})]), `%;%`_config(z', [`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr'*{instr' <- `instr'*`})])) + -- Step: `%~>%`(`%;%`_config(z, instr*{instr <- `instr*`}), `%;%`_config(z', instr'*{instr' <- `instr'*`})) + + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:45.1-47.45 rule `ctxt-frame`{s : store, f : frame, n : n, f' : frame, `instr*` : instr*, s' : store, f'' : frame, `instr'*` : instr*}: `%~>%`(`%;%`_config(`%;%`_state(s, f), [`FRAME_%{%}%`_instr(n, f', instr*{instr <- `instr*`})]), `%;%`_config(`%;%`_state(s', f), [`FRAME_%{%}%`_instr(n, f'', instr'*{instr' <- `instr'*`})])) -- Step: `%~>%`(`%;%`_config(`%;%`_state(s, f'), instr*{instr <- `instr*`}), `%;%`_config(`%;%`_state(s', f''), instr'*{instr' <- `instr'*`})) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:227.1-231.49 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:231.1-235.49 rule throw{z : state, `val*` : val*, n : n, x : idx, exn : exninst, a : addr, `t*` : valtype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [THROW_instr(x)]), `%;%`_config($add_exninst(z, [exn]), [REF.EXN_ADDR_instr(a) THROW_REF_instr])) -- Expand: `%~~%`($as_deftype($tag(z, x).TYPE_taginst), `FUNC%->%`_comptype(`%`_resulttype(t^n{t <- `t*`}), `%`_resulttype([]))) @@ -29792,74 +29819,74 @@ relation Step: `%~>%`(config, config) -- if (x!`%`_idx.0 < |$tagaddr(z)|) -- if (exn = {TAG $tagaddr(z)[x!`%`_idx.0], FIELDS val^n{val <- `val*`}}) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:302.1-303.56 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:309.1-310.56 rule local.set{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) LOCAL.SET_instr(x)]), `%;%`_config($with_local(z, x, val), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:315.1-316.58 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:322.1-323.58 rule global.set{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) GLOBAL.SET_instr(x)]), `%;%`_config($with_global(z, x, val), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:329.1-331.33 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:336.1-338.33 rule `table.set-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) TABLE.SET_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:333.1-335.32 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:340.1-342.32 rule `table.set-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) TABLE.SET_instr(x)]), `%;%`_config($with_table(z, x, i!`%`_num_.0, ref), [])) -- if (i!`%`_num_.0 < |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:344.1-347.46 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:351.1-354.46 rule `table.grow-succeed`{z : state, ref : ref, at : addrtype, n : n, x : idx, ti : tableinst}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n)) TABLE.GROW_instr(x)]), `%;%`_config($with_tableinst(z, x, ti), [CONST_instr((at : addrtype <: numtype), `%`_num_(|$table(z, x).REFS_tableinst|))])) -- if ($growtable($table(z, x), n, ref) =/= ?()) -- if (ti = !($growtable($table(z, x), n, ref))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:349.1-350.87 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:356.1-357.87 rule `table.grow-fail`{z : state, ref : ref, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n)) TABLE.GROW_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int))))])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:410.1-411.51 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:417.1-418.51 rule elem.drop{z : state, x : idx}: `%~>%`(`%;%`_config(z, [ELEM.DROP_instr(x)]), `%;%`_config($with_elem(z, x, []), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:494.1-497.60 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:501.1-504.60 rule `store-num-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:499.1-503.29 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:506.1-510.29 rule `store-num-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $nbytes_(nt, c)) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:505.1-508.52 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:512.1-515.52 rule `store-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n))), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:510.1-514.52 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:517.1-521.52 rule `store-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n))), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $ibytes_(n, $wrap__($size((Inn : Inn <: numtype)), n, c))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:516.1-519.63 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:523.1-526.63 rule `vstore-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config(z, [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-3.0/4.3-execution.instructions.spectec:521.1-524.31 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:528.1-531.31 rule `vstore-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $vbytes_(V128_vectype, c)) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:527.1-530.50 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:534.1-537.50 rule `vstore_lane-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, ao, j)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + N) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:532.1-537.49 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:539.1-544.49 rule `vstore_lane-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx, `b*` : byte*, Jnn : Jnn, M : M}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, ao, j)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((N : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (N = $jsize(Jnn)) @@ -29867,54 +29894,54 @@ relation Step: `%~>%`(config, config) -- if (j!`%`_laneidx.0 < |$lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c)|) -- if (b*{b <- `b*`} = $ibytes_(N, `%`_iN($lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c)[j!`%`_laneidx.0]!`%`_lane_.0))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:546.1-549.37 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:553.1-556.37 rule `memory.grow-succeed`{z : state, at : addrtype, n : n, x : idx, mi : meminst}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n)) MEMORY.GROW_instr(x)]), `%;%`_config($with_meminst(z, x, mi), [CONST_instr((at : addrtype <: numtype), `%`_num_((((|$mem(z, x).BYTES_meminst| : nat <:> rat) / ((64 * $Ki) : nat <:> rat)) : rat <:> nat)))])) -- if ($growmem($mem(z, x), n) =/= ?()) -- if (mi = !($growmem($mem(z, x), n))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:551.1-552.84 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:558.1-559.84 rule `memory.grow-fail`{z : state, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n)) MEMORY.GROW_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int))))])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:612.1-613.51 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:619.1-620.51 rule data.drop{z : state, x : idx}: `%~>%`(`%;%`_config(z, [DATA.DROP_instr(x)]), `%;%`_config($with_data(z, x, []), [])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:693.1-697.65 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:700.1-704.65 rule struct.new{z : state, `val*` : val*, n : n, x : idx, si : structinst, a : addr, `mut?*` : mut?*, `zt*` : storagetype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [STRUCT.NEW_instr(x)]), `%;%`_config($add_structinst(z, [si]), [REF.STRUCT_ADDR_instr(a)])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)^n{`mut?` <- `mut?*`, zt <- `zt*`}))) -- if (a = |$structinst(z)|) -- if (si = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`, zt <- `zt*`}}) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:714.1-715.53 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:721.1-722.53 rule `struct.set-null`{z : state, ht : heaptype, val : val, x : idx, i : u32}: `%~>%`(`%;%`_config(z, [REF.NULL_instr(ht) (val : val <: instr) STRUCT.SET_instr(x, i)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:717.1-720.46 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:724.1-727.46 rule `struct.set-struct`{z : state, a : addr, val : val, x : idx, i : u32, `zt*` : storagetype*, `mut?*` : mut?*}: `%~>%`(`%;%`_config(z, [REF.STRUCT_ADDR_instr(a) (val : val <: instr) STRUCT.SET_instr(x, i)]), `%;%`_config($with_struct(z, a, i!`%`_u32.0, $packfield_(zt*{zt <- `zt*`}[i!`%`_u32.0], val)), [])) -- if (i!`%`_u32.0 < |zt*{zt <- `zt*`}|) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`}))) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:733.1-738.65 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:740.1-745.65 rule array.new_fixed{z : state, `val*` : val*, n : n, x : idx, ai : arrayinst, a : addr, `mut?` : mut?, zt : storagetype}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [ARRAY.NEW_FIXED_instr(x, `%`_u32(n))]), `%;%`_config($add_arrayinst(z, [ai]), [REF.ARRAY_ADDR_instr(a)])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if ((a = |$arrayinst(z)|) /\ (ai = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`}})) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:778.1-779.64 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:785.1-786.64 rule `array.set-null`{z : state, ht : heaptype, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [REF.NULL_instr(ht) CONST_instr(I32_numtype, i) (val : val <: instr) ARRAY.SET_instr(x)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:781.1-783.39 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:788.1-790.39 rule `array.set-oob`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [REF.ARRAY_ADDR_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) ARRAY.SET_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (a < |$arrayinst(z)|) -- if (i!`%`_num_.0 >= |$arrayinst(z)[a].FIELDS_arrayinst|) - ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:785.1-788.44 + ;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:792.1-795.44 rule `array.set-array`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx, zt : storagetype, `mut?` : mut?}: `%~>%`(`%;%`_config(z, [REF.ARRAY_ADDR_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) ARRAY.SET_instr(x)]), `%;%`_config($with_array(z, a, i!`%`_num_.0, $packfield_(zt, val)), [])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index f72afe47ee..ffcdfe35d2 100644 --- a/spectec/test-splice/TEST.md +++ b/spectec/test-splice/TEST.md @@ -1196,6 +1196,7 @@ warning: rule `Resulttype_sub` was never spliced warning: rule `Start_ok` was never spliced warning: rule `Step/ctxt-instrs` was never spliced warning: rule `Step/ctxt-label` was never spliced +warning: rule `Step/ctxt-handler` was never spliced warning: rule `Step/ctxt-frame` was never spliced warning: rule `Step/throw` was never spliced warning: rule `Step/local.set` was never spliced @@ -1251,6 +1252,7 @@ warning: rule `Step_pure/return-handler` was never spliced warning: rule `Step_pure/handler-vals` was never spliced warning: rule `Step_pure/trap-instrs` was never spliced warning: rule `Step_pure/trap-label` was never spliced +warning: rule `Step_pure/trap-handler` was never spliced warning: rule `Step_pure/trap-frame` was never spliced warning: rule `Step_pure/local.tee` was never spliced warning: rule `Step_pure/ref.i31` was never spliced