From 9acb6e2c82edcc6873b8fdb7d36c7fdd8e8e403a Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 31 Jul 2023 17:59:02 +0200 Subject: [PATCH 01/20] Final opcodes (#372) Co-authored-by: Thomas Lively --- document/core/appendix/index-instructions.py | 85 ++++++++----- document/core/appendix/index-types.rst | 22 ++-- document/core/binary/instructions.rst | 60 ++++----- document/core/binary/types.rst | 22 ++-- interpreter/binary/decode.ml | 112 +++++++++-------- interpreter/binary/encode.ml | 101 ++++++++------- proposals/gc/MVP.md | 124 ++++++++++--------- 7 files changed, 282 insertions(+), 244 deletions(-) diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index 8d33768ab..f779a6b66 100755 --- a/document/core/appendix/index-instructions.py +++ b/document/core/appendix/index-instructions.py @@ -320,37 +320,38 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(None, r'\hex{F8}'), Instruction(None, r'\hex{F9}'), Instruction(None, r'\hex{FA}'), - Instruction(r'\STRUCTNEW~x', r'\hex{FB}~\hex{01}', r'[t^\ast] \to [(\REF~x)]', r'valid-struct.new', r'exec-struct.new'), - Instruction(r'\STRUCTNEWDEFAULT~x', r'\hex{FB}~\hex{02}', r'[] \to [(\REF~x)]', r'valid-struct.new_default', r'exec-struct.new_default'), - Instruction(r'\STRUCTGET~x~i', r'\hex{FB}~\hex{03}', r'[(\REF~\NULL~x)] \to [t]', r'valid-struct.get', r'exec-struct.get'), - Instruction(r'\STRUCTGETS~x~i', r'\hex{FB}~\hex{04}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'), - Instruction(r'\STRUCTGETU~x~i', r'\hex{FB}~\hex{05}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'), - Instruction(r'\STRUCTSET~x~i', r'\hex{FB}~\hex{06}', r'[(\REF~\NULL~x)~t] \to []', r'valid-struct.set', r'exec-struct.set'), - Instruction(r'\ARRAYFILL~x', r'\hex{FB}~\hex{0F}', r'[(\REF~\NULL~x)~\I32~t~\I32] \to []', r'valid-array.fill', r'exec-array.fill'), - Instruction(r'\ARRAYNEW~x', r'\hex{FB}~\hex{11}', r'[t] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'), - Instruction(r'\ARRAYNEWDEFAULT~x', r'\hex{FB}~\hex{12}', r'[] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'), - Instruction(r'\ARRAYGET~x', r'\hex{FB}~\hex{13}', r'[(\REF~\NULL~x)~\I32] \to [t]', r'valid-array.get', r'exec-array.get'), - Instruction(r'\ARRAYGETS~x', r'\hex{FB}~\hex{14}', r'[(\REF~\NULL~x)~\I32] \to [\I32]', r'valid-array.get', r'exec-array.get'), - Instruction(r'\ARRAYGETU~x', r'\hex{FB}~\hex{15}', r'[(\REF~\NULL~x)~\I32] \to [\I32]', r'valid-array.get', r'exec-array.get'), - Instruction(r'\ARRAYSET~x', r'\hex{FB}~\hex{16}', r'[(\REF~\NULL~x)~\I32~t] \to []', r'valid-array.set', r'exec-array.set'), - Instruction(r'\ARRAYLEN', r'\hex{FB}~\hex{17}', r'[\ARRAYREF] \to []', r'valid-array.len', r'exec-array.len'), - Instruction(r'\ARRAYCOPY~x~y', r'\hex{FB}~\hex{18}', r'[(\REF~\NULL~x)~\I32~(\REF~\NULL~y)~\I32~\I32] \to []', r'valid-array.copy', r'exec-array.copy'), - Instruction(r'\ARRAYNEWFIXED~x~n', r'\hex{FB}~\hex{19}', r'[t^n] \to [(\REF~x)]', r'valid-array.new_fixed', r'exec-array.new_fixed'), - Instruction(r'\ARRAYNEWDATA~x~y', r'\hex{FB}~\hex{1B}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_data', r'exec-array.new_data'), - Instruction(r'\ARRAYNEWELEM~x~y', r'\hex{FB}~\hex{1C}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_elem', r'exec-array.new_elem'), - Instruction(r'\I31NEW', r'\hex{FB}~\hex{20}', r'[\I32] \to [\I31REF]', r'valid-i31.new', r'exec-i31.new'), - Instruction(r'\I31GETS', r'\hex{FB}~\hex{21}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'), - Instruction(r'\I31GETU', r'\hex{FB}~\hex{22}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'), - Instruction(r'\REFTEST~(\REF~t)', r'\hex{FB}~\hex{40}', r"[(\REF~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'), - Instruction(r'\REFCAST~(\REF~t)', r'\hex{FB}~\hex{41}', r"[(\REF~t')] \to [(\REF~t)]", r'valid-ref.test', r'exec-ref.test'), - Instruction(r'\REFTEST~(\REF~\NULL~t)', r'\hex{FB}~\hex{48}', r"[(REF~\NULL~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'), - Instruction(r'\REFCAST~(\REF~\NULL~t)', r'\hex{FB}~\hex{49}', r"[(\REF~\NULL~t')] \to [(\REF~\NULL~t)]", r'valid-ref.cast', r'exec-ref.cast'), - Instruction(r'\BRONCAST~t_1~t_2', r'\hex{FB}~\hex{4E}', r'[t_1] \to [t_1\reftypediff t_2]', r'valid-br_on_cast', r'exec-br_on_cast'), - Instruction(r'\BRONCASTFAIL~t_1~t_2', r'\hex{FB}~\hex{4F}', r'[t_1] \to [t_2]', r'valid-br_on_cast_fail', r'exec-br_on_cast_fail'), - Instruction(r'\ARRAYINITDATA~x~y', r'\hex{FB}~\hex{54}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_data', r'exec-array.init_data'), - Instruction(r'\ARRAYINITELEM~x~y', r'\hex{FB}~\hex{55}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_elem', r'exec-array.init_elem'), - Instruction(r'\EXTERNINTERNALIZE', r'\hex{FB}~\hex{70}', r'[\EXTERNREF] \to [\ANYREF]', r'valid-extern.internalize', r'exec-extern.internalize'), - Instruction(r'\EXTERNEXTERNALIZE', r'\hex{FB}~\hex{71}', r'[\ANYREF] \to [\EXTERNREF]', r'valid-extern.externalize', r'exec-extern.externalize'), + Instruction(r'\STRUCTNEW~x', r'\hex{FB}~\hex{00}', r'[t^\ast] \to [(\REF~x)]', r'valid-struct.new', r'exec-struct.new'), + Instruction(r'\STRUCTNEWDEFAULT~x', r'\hex{FB}~\hex{01}', r'[] \to [(\REF~x)]', r'valid-struct.new_default', r'exec-struct.new_default'), + Instruction(r'\STRUCTGET~x~i', r'\hex{FB}~\hex{02}', r'[(\REF~\NULL~x)] \to [t]', r'valid-struct.get', r'exec-struct.get'), + Instruction(r'\STRUCTGETS~x~i', r'\hex{FB}~\hex{03}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'), + Instruction(r'\STRUCTGETU~x~i', r'\hex{FB}~\hex{04}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'), + Instruction(r'\STRUCTSET~x~i', r'\hex{FB}~\hex{05}', r'[(\REF~\NULL~x)~t] \to []', r'valid-struct.set', r'exec-struct.set'), + Instruction(r'\ARRAYNEW~x', r'\hex{FB}~\hex{06}', r'[t] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'), + Instruction(r'\ARRAYNEWDEFAULT~x', r'\hex{FB}~\hex{07}', r'[] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'), + Instruction(r'\ARRAYNEWFIXED~x~n', r'\hex{FB}~\hex{08}', r'[t^n] \to [(\REF~x)]', r'valid-array.new_fixed', r'exec-array.new_fixed'), + Instruction(r'\ARRAYNEWDATA~x~y', r'\hex{FB}~\hex{09}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_data', r'exec-array.new_data'), + Instruction(r'\ARRAYNEWELEM~x~y', r'\hex{FB}~\hex{0A}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_elem', r'exec-array.new_elem'), + Instruction(r'\ARRAYGET~x', r'\hex{FB}~\hex{0B}', r'[(\REF~\NULL~x)~\I32] \to [t]', r'valid-array.get', r'exec-array.get'), + Instruction(r'\ARRAYGETS~x', r'\hex{FB}~\hex{0C}', r'[(\REF~\NULL~x)~\I32] \to [\I32]', r'valid-array.get', r'exec-array.get'), + Instruction(r'\ARRAYGETU~x', r'\hex{FB}~\hex{0D}', r'[(\REF~\NULL~x)~\I32] \to [\I32]', r'valid-array.get', r'exec-array.get'), + Instruction(r'\ARRAYSET~x', r'\hex{FB}~\hex{0E}', r'[(\REF~\NULL~x)~\I32~t] \to []', r'valid-array.set', r'exec-array.set'), + Instruction(r'\ARRAYLEN', r'\hex{FB}~\hex{0F}', r'[\ARRAYREF] \to []', r'valid-array.len', r'exec-array.len'), + Instruction(r'\ARRAYFILL~x', r'\hex{FB}~\hex{10}', r'[(\REF~\NULL~x)~\I32~t~\I32] \to []', r'valid-array.fill', r'exec-array.fill'), + Instruction(r'\ARRAYCOPY~x~y', r'\hex{FB}~\hex{11}', r'[(\REF~\NULL~x)~\I32~(\REF~\NULL~y)~\I32~\I32] \to []', r'valid-array.copy', r'exec-array.copy'), + Instruction(r'\ARRAYINITDATA~x~y', r'\hex{FB}~\hex{12}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_data', r'exec-array.init_data'), + Instruction(r'\ARRAYINITELEM~x~y', r'\hex{FB}~\hex{13}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_elem', r'exec-array.init_elem'), + Instruction(r'\REFTEST~(\REF~t)', r'\hex{FB}~\hex{14}', r"[(\REF~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'), + Instruction(r'\REFTEST~(\REF~\NULL~t)', r'\hex{FB}~\hex{15}', r"[(REF~\NULL~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'), + Instruction(r'\REFCAST~(\REF~t)', r'\hex{FB}~\hex{16}', r"[(\REF~t')] \to [(\REF~t)]", r'valid-ref.test', r'exec-ref.test'), + Instruction(r'\REFCAST~(\REF~\NULL~t)', r'\hex{FB}~\hex{17}', r"[(\REF~\NULL~t')] \to [(\REF~\NULL~t)]", r'valid-ref.cast', r'exec-ref.cast'), + Instruction(r'\BRONCAST~t_1~t_2', r'\hex{FB}~\hex{18}', r'[t_1] \to [t_1\reftypediff t_2]', r'valid-br_on_cast', r'exec-br_on_cast'), + Instruction(r'\BRONCASTFAIL~t_1~t_2', r'\hex{FB}~\hex{19}', r'[t_1] \to [t_2]', r'valid-br_on_cast_fail', r'exec-br_on_cast_fail'), + Instruction(r'\EXTERNINTERNALIZE', r'\hex{FB}~\hex{1A}', r'[\EXTERNREF] \to [\ANYREF]', r'valid-extern.internalize', r'exec-extern.internalize'), + Instruction(r'\EXTERNEXTERNALIZE', r'\hex{FB}~\hex{1B}', r'[\ANYREF] \to [\EXTERNREF]', r'valid-extern.externalize', r'exec-extern.externalize'), + Instruction(r'\I31NEW', r'\hex{FB}~\hex{1C}', r'[\I32] \to [\I31REF]', r'valid-i31.new', r'exec-i31.new'), + Instruction(r'\I31GETS', r'\hex{FB}~\hex{1D}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'), + Instruction(r'\I31GETU', r'\hex{FB}~\hex{1E}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'), + Instruction(None, r'\hex{FB}~\hex{1E} \dots'), Instruction(r'\I32.\TRUNC\K{\_sat\_}\F32\K{\_s}', r'\hex{FC}~\hex{00}', r'[\F32] \to [\I32]', r'valid-cvtop', r'exec-cvtop', r'op-trunc_sat_s'), Instruction(r'\I32.\TRUNC\K{\_sat\_}\F32\K{\_u}', r'\hex{FC}~\hex{01}', r'[\F32] \to [\I32]', r'valid-cvtop', r'exec-cvtop', r'op-trunc_sat_u'), Instruction(r'\I32.\TRUNC\K{\_sat\_}\F64\K{\_s}', r'\hex{FC}~\hex{02}', r'[\F64] \to [\I32]', r'valid-cvtop', r'exec-cvtop', r'op-trunc_sat_s'), @@ -369,6 +370,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\TABLEGROW~x', r'\hex{FC}~\hex{0F}', r'[t~\I32] \to [\I32]', r'valid-table.grow', r'exec-table.grow'), Instruction(r'\TABLESIZE~x', r'\hex{FC}~\hex{10}', r'[] \to [\I32]', r'valid-table.size', r'exec-table.size'), Instruction(r'\TABLEFILL~x', r'\hex{FC}~\hex{11}', r'[\I32~t~\I32] \to []', r'valid-table.fill', r'exec-table.fill'), + Instruction(None, r'\hex{FC}~\hex{1E} \dots'), Instruction(r'\V128.\LOAD~\memarg', r'\hex{FD}~~\hex{00}', r'[\I32] \to [\V128]', r'valid-load', r'exec-load'), Instruction(r'\V128.\LOAD\K{8x8\_s}~\memarg', r'\hex{FD}~~\hex{01}', r'[\I32] \to [\V128]', r'valid-load-extend', r'exec-load-extend'), Instruction(r'\V128.\LOAD\K{8x8\_u}~\memarg', r'\hex{FD}~~\hex{02}', r'[\I32] \to [\V128]', r'valid-load-extend', r'exec-load-extend'), @@ -523,6 +525,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\I16X8.\VMIN\K{\_u}', r'\hex{FD}~~\hex{97}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-imin_u'), Instruction(r'\I16X8.\VMAX\K{\_s}', r'\hex{FD}~~\hex{98}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-imax_s'), Instruction(r'\I16X8.\VMAX\K{\_u}', r'\hex{FD}~~\hex{99}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-imax_u'), + Instruction(None, r'\hex{FD}~\hex{9A}~\hex{01}'), Instruction(r'\I16X8.\AVGR\K{\_u}', r'\hex{FD}~~\hex{9B}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-iavgr_u'), Instruction(r'\I16X8.\EXTMUL\K{\_low\_i8x16\_s}', r'\hex{FD}~~\hex{9C}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vec-extmul', r'exec-vec-extmul'), Instruction(r'\I16X8.\EXTMUL\K{\_high\_i8x16\_s}', r'\hex{FD}~~\hex{9D}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vec-extmul', r'exec-vec-extmul'), @@ -530,8 +533,11 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\I16X8.\EXTMUL\K{\_high\_i8x16\_u}', r'\hex{FD}~~\hex{9F}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vec-extmul', r'exec-vec-extmul'), Instruction(r'\I32X4.\VABS', r'\hex{FD}~~\hex{A0}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-iabs'), Instruction(r'\I32X4.\VNEG', r'\hex{FD}~~\hex{A1}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-ineg'), + Instruction(None, r'\hex{FD}~\hex{A2}~\hex{01}'), Instruction(r'\I32X4.\ALLTRUE', r'\hex{FD}~~\hex{A3}~~\hex{01}', r'[\V128] \to [\I32]', r'valid-vtestop', r'exec-vtestop'), Instruction(r'\I32X4.\BITMASK', r'\hex{FD}~~\hex{A4}~~\hex{01}', r'[\V128] \to [\I32]', r'valid-vec-bitmask', r'exec-vec-bitmask'), + Instruction(None, r'\hex{FD}~\hex{A5}~\hex{01}'), + Instruction(None, r'\hex{FD}~\hex{A6}~\hex{01}'), Instruction(r'\I32X4.\VEXTEND\K{\_low\_i16x8\_s}', r'\hex{FD}~~\hex{A7}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vcvtop'), Instruction(r'\I32X4.\VEXTEND\K{\_high\_i16x8\_s}', r'\hex{FD}~~\hex{A8}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vcvtop'), Instruction(r'\I32X4.\VEXTEND\K{\_low\_i16x8\_u}', r'\hex{FD}~~\hex{A9}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vcvtop'), @@ -540,7 +546,12 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\I32X4.\VSHR\K{\_s}', r'\hex{FD}~~\hex{AC}~~\hex{01}', r'[\V128~\I32] \to [\V128]', r'valid-vishiftop', r'exec-vishiftop', r'op-ishr_s'), Instruction(r'\I32X4.\VSHR\K{\_u}', r'\hex{FD}~~\hex{AD}~~\hex{01}', r'[\V128~\I32] \to [\V128]', r'valid-vishiftop', r'exec-vishiftop', r'op-ishr_u'), Instruction(r'\I32X4.\VADD', r'\hex{FD}~~\hex{AE}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-iadd'), + Instruction(None, r'\hex{FD}~\hex{AF}~\hex{01}'), + Instruction(None, r'\hex{FD}~\hex{B0}~\hex{01}'), Instruction(r'\I32X4.\VSUB', r'\hex{FD}~~\hex{B1}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-isub'), + Instruction(None, r'\hex{FD}~\hex{B2}~\hex{01}'), + Instruction(None, r'\hex{FD}~\hex{B3}~\hex{01}'), + Instruction(None, r'\hex{FD}~\hex{B4}~\hex{01}'), Instruction(r'\I32X4.\VMUL', r'\hex{FD}~~\hex{B5}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-imul'), Instruction(r'\I32X4.\VMIN\K{\_s}', r'\hex{FD}~~\hex{B6}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-imin_s'), Instruction(r'\I32X4.\VMIN\K{\_u}', r'\hex{FD}~~\hex{B7}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-imin_u'), @@ -553,8 +564,11 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\I32X4.\EXTMUL\K{\_high\_i16x8\_u}', r'\hex{FD}~~\hex{BF}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vec-extmul', r'exec-vec-extmul'), Instruction(r'\I64X2.\VABS', r'\hex{FD}~~\hex{C0}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-iabs'), Instruction(r'\I64X2.\VNEG', r'\hex{FD}~~\hex{C1}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-ineg'), + Instruction(None, r'\hex{FD}~\hex{C2}~\hex{01}'), Instruction(r'\I64X2.\ALLTRUE', r'\hex{FD}~~\hex{C3}~~\hex{01}', r'[\V128] \to [\I32]', r'valid-vtestop', r'exec-vtestop'), Instruction(r'\I64X2.\BITMASK', r'\hex{FD}~~\hex{C4}~~\hex{01}', r'[\V128] \to [\I32]', r'valid-vec-bitmask', r'exec-vec-bitmask'), + Instruction(None, r'\hex{FD}~\hex{C5}~\hex{01}'), + Instruction(None, r'\hex{FD}~\hex{C6}~\hex{01}'), Instruction(r'\I64X2.\VEXTEND\K{\_low\_i32x4\_s}', r'\hex{FD}~~\hex{C7}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vcvtop'), Instruction(r'\I64X2.\VEXTEND\K{\_high\_i32x4\_s}', r'\hex{FD}~~\hex{C8}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vcvtop'), Instruction(r'\I64X2.\VEXTEND\K{\_low\_i32x4\_u}', r'\hex{FD}~~\hex{C9}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vcvtop'), @@ -563,7 +577,12 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\I64X2.\VSHR\K{\_s}', r'\hex{FD}~~\hex{CC}~~\hex{01}', r'[\V128~\I32] \to [\V128]', r'valid-vishiftop', r'exec-vishiftop', r'op-ishr_s'), Instruction(r'\I64X2.\VSHR\K{\_u}', r'\hex{FD}~~\hex{CD}~~\hex{01}', r'[\V128~\I32] \to [\V128]', r'valid-vishiftop', r'exec-vishiftop', r'op-ishr_u'), Instruction(r'\I64X2.\VADD', r'\hex{FD}~~\hex{CE}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-iadd'), + Instruction(None, r'\hex{FD}~\hex{CF}~\hex{01}'), + Instruction(None, r'\hex{FD}~\hex{D0}~\hex{01}'), Instruction(r'\I64X2.\VSUB', r'\hex{FD}~~\hex{D1}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-isub'), + Instruction(None, r'\hex{FD}~\hex{D2}~\hex{01}'), + Instruction(None, r'\hex{FD}~\hex{D3}~\hex{01}'), + Instruction(None, r'\hex{FD}~\hex{D4}~\hex{01}'), Instruction(r'\I64X2.\VMUL', r'\hex{FD}~~\hex{D5}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-imul'), Instruction(r'\I64X2.\VEQ', r'\hex{FD}~~\hex{D6}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ieq'), Instruction(r'\I64X2.\VNE', r'\hex{FD}~~\hex{D7}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ine'), @@ -577,6 +596,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\I64X2.\EXTMUL\K{\_high\_i32x4\_u}', r'\hex{FD}~~\hex{DF}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vec-extmul', r'exec-vec-extmul'), Instruction(r'\F32X4.\VABS', r'\hex{FD}~~\hex{E0}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-fabs'), Instruction(r'\F32X4.\VNEG', r'\hex{FD}~~\hex{E1}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-fneg'), + Instruction(None, r'\hex{FD}~\hex{E2}~\hex{01}'), Instruction(r'\F32X4.\VSQRT', r'\hex{FD}~~\hex{E3}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-fsqrt'), Instruction(r'\F32X4.\VADD', r'\hex{FD}~~\hex{E4}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fadd'), Instruction(r'\F32X4.\VSUB', r'\hex{FD}~~\hex{E5}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fsub'), @@ -605,6 +625,9 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\I32X4.\VTRUNC\K{\_sat\_f64x2\_u\_zero}', r'\hex{FD}~~\hex{FD}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-trunc_sat_u'), Instruction(r'\F64X2.\VCONVERT\K{\_low\_i32x4\_s}', r'\hex{FD}~~\hex{FE}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-convert_s'), Instruction(r'\F64X2.\VCONVERT\K{\_low\_i32x4\_u}', r'\hex{FD}~~\hex{FF}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-convert_u'), + Instruction(None, r'\hex{FD}~\hex{00}~\hex{02} \dots'), + Instruction(None, r'\hex{FE}'), + Instruction(None, r'\hex{FF}'), ] diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst index f2de63204..5d31e71c0 100644 --- a/document/core/appendix/index-types.rst +++ b/document/core/appendix/index-types.rst @@ -15,27 +15,27 @@ Category Constructor :ref:`Vector type ` |V128| :math:`\hex{7B}` (-5 as |Bs7|) :ref:`Packed type ` |I8| :math:`\hex{7A}` (-6 as |Bs7|) :ref:`Packed type ` |I16| :math:`\hex{79}` (-7 as |Bs7|) -(reserved) :math:`\hex{78}` .. :math:`\hex{71}` +(reserved) :math:`\hex{78}` .. :math:`\hex{74}` +:ref:`Heap type ` |NOFUNC| :math:`\hex{73}` (-13 as |Bs7|) +:ref:`Heap type ` |NOEXTERN| :math:`\hex{72}` (-14 as |Bs7|) +:ref:`Heap type ` |NONE| :math:`\hex{71}` (-15 as |Bs7|) :ref:`Heap type ` |FUNC| :math:`\hex{70}` (-16 as |Bs7|) :ref:`Heap type ` |EXTERN| :math:`\hex{6F}` (-17 as |Bs7|) :ref:`Heap type ` |ANY| :math:`\hex{6E}` (-18 as |Bs7|) :ref:`Heap type ` |EQT| :math:`\hex{6D}` (-19 as |Bs7|) -:ref:`Reference type ` |REF| |NULL| :math:`\hex{6C}` (-20 as |Bs7|) -:ref:`Reference type ` |REF| :math:`\hex{6B}` (-21 as |Bs7|) -:ref:`Heap type ` |I31| :math:`\hex{6A}` (-22 as |Bs7|) -:ref:`Heap type ` |NOFUNC| :math:`\hex{69}` (-23 as |Bs7|) -:ref:`Heap type ` |NOEXTERN| :math:`\hex{68}` (-24 as |Bs7|) -:ref:`Heap type ` |STRUCT| :math:`\hex{67}` (-25 as |Bs7|) -:ref:`Heap type ` |ARRAY| :math:`\hex{66}` (-26 as |Bs7|) -:ref:`Heap type ` |NONE| :math:`\hex{65}` (-27 as |Bs7|) +:ref:`Heap type ` |I31| :math:`\hex{6C}` (-20 as |Bs7|) +:ref:`Heap type ` |STRUCT| :math:`\hex{6B}` (-21 as |Bs7|) +:ref:`Heap type ` |ARRAY| :math:`\hex{6A}` (-22 as |Bs7|) +:ref:`Reference type ` |REF| :math:`\hex{64}` (-28 as |Bs7|) +:ref:`Reference type ` |REF| |NULL| :math:`\hex{63}` (-29 as |Bs7|) (reserved) :math:`\hex{64}` .. :math:`\hex{61}` :ref:`Composite type ` :math:`\TFUNC~[\valtype^\ast] \toF[\valtype^\ast]` :math:`\hex{60}` (-32 as |Bs7|) :ref:`Composite type ` :math:`\TSTRUCT~\fieldtype^\ast` :math:`\hex{5F}` (-33 as |Bs7|) :ref:`Composite type ` :math:`\TARRAY~\fieldtype` :math:`\hex{5E}` (-34 as |Bs7|) (reserved) :math:`\hex{5D}` .. :math:`\hex{51}` :ref:`Sub type ` :math:`\TSUB~\typeidx^\ast~\comptype` :math:`\hex{50}` (-48 as |Bs7|) -:ref:`Recursive type ` :math:`\TREC~\subtype^\ast` :math:`\hex{4F}` (-49 as |Bs7|) -:ref:`Sub type ` :math:`\TSUB~\TFINAL~\typeidx^\ast~\comptype` :math:`\hex{4E}` (-50 as |Bs7|) +:ref:`Sub type ` :math:`\TSUB~\TFINAL~\typeidx^\ast~\comptype` :math:`\hex{4F}` (-49 as |Bs7|) +:ref:`Recursive type ` :math:`\TREC~\subtype^\ast` :math:`\hex{4E}` (-50 as |Bs7|) (reserved) :math:`\hex{4D}` .. :math:`\hex{41}` :ref:`Result type ` :math:`[\epsilon]` :math:`\hex{40}` (-64 as |Bs7|) :ref:`Table type ` :math:`\limits~\reftype` (none) diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 4e69cdbcb..a23c02cf0 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -77,8 +77,8 @@ Control Instructions \hex{15}~~x{:}\Btypeidx &\Rightarrow& \RETURNCALLREF~x \\ &&|& \hex{D4}~~l{:}\Blabelidx &\Rightarrow& \BRONNULL~l \\ &&|& \hex{D6}~~l{:}\Blabelidx &\Rightarrow& \BRONNONNULL~l \\ &&|& - \hex{FB}~~78{:}\Bu32~~(\NULL_1^?,\NULL_2^?){:}\Bcastflags\\&&&~~~~l{:}\Blabelidx~~\X{ht}_1{:}\Bheaptype~~\X{ht}_2{:}\Bheaptype &\Rightarrow& \BRONCAST~l~(\REF~\NULL_1^?~\X{ht}_1)~(\REF~\NULL_2^?~\X{ht}_2) \\ &&|& - \hex{FB}~~79{:}\Bu32~~(\NULL_1^?,\NULL_2^?){:}\Bcastflags\\&&&~~~~l{:}\Blabelidx~~\X{ht}_1{:}\Bheaptype~~\X{ht}_2{:}\Bheaptype &\Rightarrow& \BRONCASTFAIL~l~(\REF~\NULL_1^?~\X{ht}_1)~(\REF~\NULL_2^?~\X{ht}_2) \\ + \hex{FB}~~24{:}\Bu32~~(\NULL_1^?,\NULL_2^?){:}\Bcastflags\\&&&~~~~l{:}\Blabelidx~~\X{ht}_1{:}\Bheaptype~~\X{ht}_2{:}\Bheaptype &\Rightarrow& \BRONCAST~l~(\REF~\NULL_1^?~\X{ht}_1)~(\REF~\NULL_2^?~\X{ht}_2) \\ &&|& + \hex{FB}~~25{:}\Bu32~~(\NULL_1^?,\NULL_2^?){:}\Bcastflags\\&&&~~~~l{:}\Blabelidx~~\X{ht}_1{:}\Bheaptype~~\X{ht}_2{:}\Bheaptype &\Rightarrow& \BRONCASTFAIL~l~(\REF~\NULL_1^?~\X{ht}_1)~(\REF~\NULL_2^?~\X{ht}_2) \\ \production{cast flags} & \Bcastflags &::=& 0{:}\Bu8 &\Rightarrow& (\epsilon, \epsilon) \\ &&|& 1{:}\Bu8 &\Rightarrow& (\NULL, \epsilon) \\ &&|& @@ -142,35 +142,35 @@ Generic :ref:`reference instructions ` are represented by sing \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\ &&|& \hex{D3} &\Rightarrow& \REFASNONNULL \\ &&|& \hex{D5} &\Rightarrow& \REFEQ \\ &&|& - \hex{FB}~~1{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \STRUCTNEW~x \\ &&|& - \hex{FB}~~2{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \STRUCTNEWDEFAULT~x \\ &&|& - \hex{FB}~~3{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTGET~x~i \\ &&|& - \hex{FB}~~4{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTGETS~x~i \\ &&|& - \hex{FB}~~5{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTGETU~x~i \\ &&|& - \hex{FB}~~6{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTSET~x~i \\ &&|& + \hex{FB}~~0{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \STRUCTNEW~x \\ &&|& + \hex{FB}~~1{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \STRUCTNEWDEFAULT~x \\ &&|& + \hex{FB}~~2{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTGET~x~i \\ &&|& + \hex{FB}~~3{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTGETS~x~i \\ &&|& + \hex{FB}~~4{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTGETU~x~i \\ &&|& + \hex{FB}~~5{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTSET~x~i \\ &&|& + \hex{FB}~~6{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYNEW~x \\ &&|& + \hex{FB}~~7{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYNEWDEFAULT~x \\ &&|& + \hex{FB}~~8{:}\Bu32~~x{:}\Btypeidx~~n{:}\Bu32 &\Rightarrow& \ARRAYNEWFIXED~x~n \\ &&|& + \hex{FB}~~9{:}\Bu32~~x{:}\Btypeidx~~y{:}\Bdataidx &\Rightarrow& \ARRAYNEWDATA~x~y \\ &&|& + \hex{FB}~~10{:}\Bu32~~x{:}\Btypeidx~~y{:}\Belemidx &\Rightarrow& \ARRAYNEWELEM~x~y \\ &&|& + \hex{FB}~~11{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYGET~x \\ &&|& + \hex{FB}~~12{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYGETS~x \\ &&|& + \hex{FB}~~13{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYGETU~x \\ &&|& + \hex{FB}~~14{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYSET~x \\ &&|& + \hex{FB}~~15{:}\Bu32 &\Rightarrow& \ARRAYLEN \\ &&|& \hex{FB}~~16{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYFILL~x \\ &&|& - \hex{FB}~~17{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYNEW~x \\ &&|& - \hex{FB}~~18{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYNEWDEFAULT~x \\ &&|& - \hex{FB}~~19{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYGET~x \\ &&|& - \hex{FB}~~20{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYGETS~x \\ &&|& - \hex{FB}~~21{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYGETU~x \\ &&|& - \hex{FB}~~22{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYSET~x \\ &&|& - \hex{FB}~~23{:}\Bu32 &\Rightarrow& \ARRAYLEN \\ &&|& - \hex{FB}~~24{:}\Bu32~~x{:}\Btypeidx~~y{:}\Btypeidx &\Rightarrow& \ARRAYCOPY~x~y \\ &&|& - \hex{FB}~~25{:}\Bu32~~x{:}\Btypeidx~~n{:}\Bu32 &\Rightarrow& \ARRAYNEWFIXED~x~n \\ &&|& - \hex{FB}~~27{:}\Bu32~~x{:}\Btypeidx~~y{:}\Bdataidx &\Rightarrow& \ARRAYNEWDATA~x~y \\ &&|& - \hex{FB}~~28{:}\Bu32~~x{:}\Btypeidx~~y{:}\Belemidx &\Rightarrow& \ARRAYNEWELEM~x~y \\ &&|& - \hex{FB}~~32{:}\Bu32 &\Rightarrow& \I31NEW \\ &&|& - \hex{FB}~~33{:}\Bu32 &\Rightarrow& \I31GETS \\ &&|& - \hex{FB}~~34{:}\Bu32 &\Rightarrow& \I31GETU \\ &&|& - \hex{FB}~~64{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFTEST~(\REF~\X{ht}) \\ &&|& - \hex{FB}~~65{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFCAST~(\REF~\X{ht}) \\ &&|& - \hex{FB}~~72{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFTEST~(\REF~\NULL~\X{ht}) \\ &&|& - \hex{FB}~~73{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFCAST~(\REF~\NULL~\X{ht}) \\ &&|& - \hex{FB}~~84{:}\Bu32~~x{:}\Btypeidx~~y{:}\Bdataidx &\Rightarrow& \ARRAYINITDATA~x~y \\ &&|& - \hex{FB}~~85{:}\Bu32~~x{:}\Btypeidx~~y{:}\Belemidx &\Rightarrow& \ARRAYINITELEM~x~y \\ &&|& - \hex{FB}~~112{:}\Bu32 &\Rightarrow& \EXTERNINTERNALIZE \\ &&|& - \hex{FB}~~113{:}\Bu32 &\Rightarrow& \EXTERNEXTERNALIZE \\ + \hex{FB}~~17{:}\Bu32~~x{:}\Btypeidx~~y{:}\Btypeidx &\Rightarrow& \ARRAYCOPY~x~y \\ &&|& + \hex{FB}~~18{:}\Bu32~~x{:}\Btypeidx~~y{:}\Bdataidx &\Rightarrow& \ARRAYINITDATA~x~y \\ &&|& + \hex{FB}~~19{:}\Bu32~~x{:}\Btypeidx~~y{:}\Belemidx &\Rightarrow& \ARRAYINITELEM~x~y \\ &&|& + \hex{FB}~~20{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFTEST~(\REF~\X{ht}) \\ &&|& + \hex{FB}~~21{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFTEST~(\REF~\NULL~\X{ht}) \\ &&|& + \hex{FB}~~22{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFCAST~(\REF~\X{ht}) \\ &&|& + \hex{FB}~~23{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFCAST~(\REF~\NULL~\X{ht}) \\ &&|& + \hex{FB}~~26{:}\Bu32 &\Rightarrow& \EXTERNINTERNALIZE \\ &&|& + \hex{FB}~~27{:}\Bu32 &\Rightarrow& \EXTERNEXTERNALIZE \\ &&|& + \hex{FB}~~28{:}\Bu32 &\Rightarrow& \I31NEW \\ &&|& + \hex{FB}~~29{:}\Bu32 &\Rightarrow& \I31GETS \\ &&|& + \hex{FB}~~30{:}\Bu32 &\Rightarrow& \I31GETU \\ \end{array} diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index 64c98a268..39af72feb 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -58,16 +58,16 @@ Heap Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} \production{abstract heap type} & \Babsheaptype &::=& - \hex{65} &\Rightarrow& \NONE \\ &&|& - \hex{66} &\Rightarrow& \ARRAY \\ &&|& - \hex{67} &\Rightarrow& \STRUCT \\ &&|& - \hex{68} &\Rightarrow& \NOEXTERN \\ &&|& - \hex{69} &\Rightarrow& \NOFUNC \\ &&|& - \hex{6A} &\Rightarrow& \I31 \\ &&|& - \hex{6D} &\Rightarrow& \EQT \\ &&|& - \hex{6E} &\Rightarrow& \ANY \\ &&|& + \hex{73} &\Rightarrow& \NOFUNC \\ &&|& + \hex{72} &\Rightarrow& \NOEXTERN \\ &&|& + \hex{71} &\Rightarrow& \NONE \\ &&|& + \hex{70} &\Rightarrow& \FUNC \\ &&|& \hex{6F} &\Rightarrow& \EXTERN \\ &&|& - \hex{70} &\Rightarrow& \FUNC \\ + \hex{6E} &\Rightarrow& \ANY \\ &&|& + \hex{6D} &\Rightarrow& \EQT \\ &&|& + \hex{6C} &\Rightarrow& \I31 \\ &&|& + \hex{6B} &\Rightarrow& \STRUCT \\ &&|& + \hex{6A} &\Rightarrow& \ARRAY \\ \production{heap type} & \Bheaptype &::=& \X{ht}{:}\Babsheaptype &\Rightarrow& \X{ht} \\ &&|& x{:}\Bs33 &\Rightarrow& x & (\iff x \geq 0) \\ @@ -86,8 +86,8 @@ Reference Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} \production{reference type} & \Breftype &::=& - \hex{6B}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\X{ht} \\ &&|& - \hex{6C}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\NULL~\X{ht} \\ &&|& + \hex{64}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\X{ht} \\ &&|& + \hex{63}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\NULL~\X{ht} \\ &&|& \X{ht}{:}\Babsheaptype &\Rightarrow& \REF~\NULL~\X{ht} \\ \end{array} diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index af59368c2..cbff7fb2b 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -177,16 +177,16 @@ let heap_type s = (fun s -> VarHT (var_type s33 s)); (fun s -> match s7 s with + | -0x0d -> NoFuncHT + | -0x0e -> NoExternHT + | -0x0f -> NoneHT | -0x10 -> FuncHT | -0x11 -> ExternHT | -0x12 -> AnyHT | -0x13 -> EqHT - | -0x16 -> I31HT - | -0x17 -> NoFuncHT - | -0x18 -> NoExternHT - | -0x19 -> StructHT - | -0x1a -> ArrayHT - | -0x1b -> NoneHT + | -0x14 -> I31HT + | -0x15 -> StructHT + | -0x16 -> ArrayHT | _ -> error s pos "malformed heap type" ) ] s @@ -194,18 +194,18 @@ let heap_type s = let ref_type s = let pos = pos s in match s7 s with + | -0x0d -> (Null, NoFuncHT) + | -0x0e -> (Null, NoExternHT) + | -0x0f -> (Null, NoneHT) | -0x10 -> (Null, FuncHT) | -0x11 -> (Null, ExternHT) | -0x12 -> (Null, AnyHT) | -0x13 -> (Null, EqHT) - | -0x14 -> (Null, heap_type s) - | -0x15 -> (NoNull, heap_type s) - | -0x16 -> (Null, I31HT) - | -0x17 -> (Null, NoFuncHT) - | -0x18 -> (Null, NoExternHT) - | -0x19 -> (Null, StructHT) - | -0x1a -> (Null, ArrayHT) - | -0x1b -> (Null, NoneHT) + | -0x14 -> (Null, I31HT) + | -0x15 -> (Null, StructHT) + | -0x16 -> (Null, ArrayHT) + | -0x1c -> (NoNull, heap_type s) + | -0x1d -> (Null, heap_type s) | _ -> error s pos "malformed reference type" let val_type s = @@ -259,7 +259,7 @@ let sub_type s = skip 1 s; let xs = vec (var_type u32) s in SubT (NoFinal, List.map (fun x -> VarHT x) xs, str_type s) - | Some i when i = -0x32 land 0x7f -> + | Some i when i = -0x31 land 0x7f -> skip 1 s; let xs = vec (var_type u32) s in SubT (Final, List.map (fun x -> VarHT x) xs, str_type s) @@ -267,7 +267,7 @@ let sub_type s = let rec_type s = match peek s with - | Some i when i = -0x31 land 0x7f -> skip 1 s; RecT (vec sub_type s) + | Some i when i = -0x32 land 0x7f -> skip 1 s; RecT (vec sub_type s) | _ -> RecT [sub_type s] @@ -588,48 +588,46 @@ let rec instr s = | 0xfb as b -> (match u32 s with - | 0x01l -> struct_new (at var s) - | 0x02l -> struct_new_default (at var s) - | 0x03l -> let x = at var s in let y = at var s in struct_get x y - | 0x04l -> let x = at var s in let y = at var s in struct_get_s x y - | 0x05l -> let x = at var s in let y = at var s in struct_get_u x y - | 0x06l -> let x = at var s in let y = at var s in struct_set x y - - | 0x11l -> array_new (at var s) - | 0x12l -> array_new_default (at var s) - | 0x13l -> array_get (at var s) - | 0x14l -> array_get_s (at var s) - | 0x15l -> array_get_u (at var s) - | 0x16l -> array_set (at var s) - | 0x17l -> array_len - - | 0x18l -> let x = at var s in let y = at var s in array_copy x y - | 0x0fl -> array_fill (at var s) - | 0x54l -> let x = at var s in let y = at var s in array_init_data x y - | 0x55l -> let x = at var s in let y = at var s in array_init_elem x y - - | 0x19l -> let x = at var s in let n = u32 s in array_new_fixed x n - | 0x1bl -> let x = at var s in let y = at var s in array_new_data x y - | 0x1cl -> let x = at var s in let y = at var s in array_new_elem x y - - | 0x20l -> i31_new - | 0x21l -> i31_get_s - | 0x22l -> i31_get_u - - | 0x40l -> ref_test (NoNull, heap_type s) - | 0x41l -> ref_cast (NoNull, heap_type s) - | 0x48l -> ref_test (Null, heap_type s) - | 0x49l -> ref_cast (Null, heap_type s) - | 0x4el | 0x4fl as opcode -> + | 0x00l -> struct_new (at var s) + | 0x01l -> struct_new_default (at var s) + | 0x02l -> let x = at var s in let y = at var s in struct_get x y + | 0x03l -> let x = at var s in let y = at var s in struct_get_s x y + | 0x04l -> let x = at var s in let y = at var s in struct_get_u x y + | 0x05l -> let x = at var s in let y = at var s in struct_set x y + + | 0x06l -> array_new (at var s) + | 0x07l -> array_new_default (at var s) + | 0x08l -> let x = at var s in let n = u32 s in array_new_fixed x n + | 0x09l -> let x = at var s in let y = at var s in array_new_data x y + | 0x0al -> let x = at var s in let y = at var s in array_new_elem x y + | 0x0bl -> array_get (at var s) + | 0x0cl -> array_get_s (at var s) + | 0x0dl -> array_get_u (at var s) + | 0x0el -> array_set (at var s) + | 0x0fl -> array_len + | 0x10l -> array_fill (at var s) + | 0x11l -> let x = at var s in let y = at var s in array_copy x y + | 0x12l -> let x = at var s in let y = at var s in array_init_data x y + | 0x13l -> let x = at var s in let y = at var s in array_init_elem x y + + | 0x14l -> ref_test (NoNull, heap_type s) + | 0x15l -> ref_test (Null, heap_type s) + | 0x16l -> ref_cast (NoNull, heap_type s) + | 0x17l -> ref_cast (Null, heap_type s) + | 0x18l | 0x19l as opcode -> let flags = byte s in require (flags land 0xfc = 0) s (pos + 2) "malformed br_on_cast flags"; let x = at var s in let rt1 = ((if bit 0 flags then Null else NoNull), heap_type s) in let rt2 = ((if bit 1 flags then Null else NoNull), heap_type s) in - (if opcode = 0x4el then br_on_cast else br_on_cast_fail) x rt1 rt2 + (if opcode = 0x18l then br_on_cast else br_on_cast_fail) x rt1 rt2 - | 0x70l -> extern_internalize - | 0x71l -> extern_externalize + | 0x1al -> extern_internalize + | 0x1bl -> extern_externalize + + | 0x1cl -> i31_new + | 0x1dl -> i31_get_s + | 0x1el -> i31_get_u | n -> illegal2 s pos b n ) @@ -848,6 +846,7 @@ let rec instr s = | 0x97l -> i16x8_min_u | 0x98l -> i16x8_max_s | 0x99l -> i16x8_max_u + | 0x9al as n -> illegal s pos (I32.to_int_u n) | 0x9bl -> i16x8_avgr_u | 0x9cl -> i16x8_extmul_low_i8x16_s | 0x9dl -> i16x8_extmul_high_i8x16_s @@ -855,8 +854,10 @@ let rec instr s = | 0x9fl -> i16x8_extmul_high_i8x16_u | 0xa0l -> i32x4_abs | 0xa1l -> i32x4_neg + | 0xa2l as n -> illegal s pos (I32.to_int_u n) | 0xa3l -> i32x4_all_true | 0xa4l -> i32x4_bitmask + | 0xa5l | 0xa6l as n -> illegal s pos (I32.to_int_u n) | 0xa7l -> i32x4_extend_low_i16x8_s | 0xa8l -> i32x4_extend_high_i16x8_s | 0xa9l -> i32x4_extend_low_i16x8_u @@ -865,7 +866,9 @@ let rec instr s = | 0xacl -> i32x4_shr_s | 0xadl -> i32x4_shr_u | 0xael -> i32x4_add + | 0xafl | 0xb0l as n -> illegal s pos (I32.to_int_u n) | 0xb1l -> i32x4_sub + | 0xb2l | 0xb3l | 0xb4l as n -> illegal s pos (I32.to_int_u n) | 0xb5l -> i32x4_mul | 0xb6l -> i32x4_min_s | 0xb7l -> i32x4_min_u @@ -878,8 +881,10 @@ let rec instr s = | 0xbfl -> i32x4_extmul_high_i16x8_u | 0xc0l -> i64x2_abs | 0xc1l -> i64x2_neg + | 0xc2l as n -> illegal s pos (I32.to_int_u n) | 0xc3l -> i64x2_all_true | 0xc4l -> i64x2_bitmask + | 0xc5l | 0xc6l as n -> illegal s pos (I32.to_int_u n) | 0xc7l -> i64x2_extend_low_i32x4_s | 0xc8l -> i64x2_extend_high_i32x4_s | 0xc9l -> i64x2_extend_low_i32x4_u @@ -888,7 +893,9 @@ let rec instr s = | 0xccl -> i64x2_shr_s | 0xcdl -> i64x2_shr_u | 0xcel -> i64x2_add + | 0xcfl | 0xd0l as n -> illegal s pos (I32.to_int_u n) | 0xd1l -> i64x2_sub + | 0xd2l | 0xd3l | 0xd4l as n -> illegal s pos (I32.to_int_u n) | 0xd5l -> i64x2_mul | 0xd6l -> i64x2_eq | 0xd7l -> i64x2_ne @@ -902,6 +909,7 @@ let rec instr s = | 0xdfl -> i64x2_extmul_high_i32x4_u | 0xe0l -> f32x4_abs | 0xe1l -> f32x4_neg + | 0xe2l as n -> illegal s pos (I32.to_int_u n) | 0xe3l -> f32x4_sqrt | 0xe4l -> f32x4_add | 0xe5l -> f32x4_sub diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 71615e415..fe7be0db6 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -116,15 +116,15 @@ struct let heap_type = function | AnyHT -> s7 (-0x12) - | NoneHT -> s7 (-0x1b) | EqHT -> s7 (-0x13) - | I31HT -> s7 (-0x16) - | StructHT -> s7 (-0x19) - | ArrayHT -> s7 (-0x1a) + | I31HT -> s7 (-0x14) + | StructHT -> s7 (-0x15) + | ArrayHT -> s7 (-0x16) + | NoneHT -> s7 (-0x0f) | FuncHT -> s7 (-0x10) - | NoFuncHT -> s7 (-0x17) + | NoFuncHT -> s7 (-0x0d) | ExternHT -> s7 (-0x11) - | NoExternHT -> s7 (-0x18) + | NoExternHT -> s7 (-0x0e) | VarHT x -> var_type s33 x | DefHT _ | BotHT -> assert false @@ -134,17 +134,17 @@ struct let ref_type = function | (Null, AnyHT) -> s7 (-0x12) - | (Null, NoneHT) -> s7 (-0x1b) | (Null, EqHT) -> s7 (-0x13) - | (Null, I31HT) -> s7 (-0x16) - | (Null, StructHT) -> s7 (-0x19) - | (Null, ArrayHT) -> s7 (-0x1a) + | (Null, I31HT) -> s7 (-0x14) + | (Null, StructHT) -> s7 (-0x15) + | (Null, ArrayHT) -> s7 (-0x16) + | (Null, NoneHT) -> s7 (-0x0f) | (Null, FuncHT) -> s7 (-0x10) - | (Null, NoFuncHT) -> s7 (-0x17) + | (Null, NoFuncHT) -> s7 (-0x0d) | (Null, ExternHT) -> s7 (-0x11) - | (Null, NoExternHT) -> s7 (-0x18) - | (Null, t) -> s7 (-0x14); heap_type t - | (NoNull, t) -> s7 (-0x15); heap_type t + | (Null, NoExternHT) -> s7 (-0x0e) + | (Null, t) -> s7 (-0x1d); heap_type t + | (NoNull, t) -> s7 (-0x1c); heap_type t let val_type = function | NumT t -> num_type t @@ -180,12 +180,12 @@ struct let sub_type = function | SubT (Final, [], st) -> str_type st - | SubT (Final, hts, st) -> s7 (-0x32); vec var_heap_type hts; str_type st + | SubT (Final, hts, st) -> s7 (-0x31); vec var_heap_type hts; str_type st | SubT (NoFinal, hts, st) -> s7 (-0x30); vec var_heap_type hts; str_type st let rec_type = function | RecT [st] -> sub_type st - | RecT sts -> s7 (-0x31); vec sub_type sts + | RecT sts -> s7 (-0x32); vec sub_type sts let limits uN {min; max} = bool (max <> None); uN min; opt uN max @@ -249,10 +249,10 @@ struct | BrOnNonNull x -> op 0xd6; var x | BrOnCast (x, (nul1, t1), (nul2, t2)) -> let flags = bit 0 (nul1 = Null) + bit 1 (nul2 = Null) in - op 0xfb; op 0x4e; byte flags; var x; heap_type t1; heap_type t2 + op 0xfb; op 0x18; byte flags; var x; heap_type t1; heap_type t2 | BrOnCastFail (x, (nul1, t1), (nul2, t2)) -> let flags = bit 0 (nul1 = Null) + bit 1 (nul2 = Null) in - op 0xfb; op 0x4f; byte flags; var x; heap_type t1; heap_type t2 + op 0xfb; op 0x19; byte flags; var x; heap_type t1; heap_type t2 | Return -> op 0x0f | Call x -> op 0x10; var x | CallRef x -> op 0x14; var x @@ -378,42 +378,41 @@ struct | RefIsNull -> op 0xd1 | RefAsNonNull -> op 0xd3 - | RefTest (NoNull, t) -> op 0xfb; op 0x40; heap_type t - | RefTest (Null, t) -> op 0xfb; op 0x48; heap_type t - | RefCast (NoNull, t) -> op 0xfb; op 0x41; heap_type t - | RefCast (Null, t) -> op 0xfb; op 0x49; heap_type t + | RefTest (NoNull, t) -> op 0xfb; op 0x14; heap_type t + | RefTest (Null, t) -> op 0xfb; op 0x15; heap_type t + | RefCast (NoNull, t) -> op 0xfb; op 0x16; heap_type t + | RefCast (Null, t) -> op 0xfb; op 0x17; heap_type t | RefEq -> op 0xd5 - | I31New -> op 0xfb; op 0x20 - | I31Get SX -> op 0xfb; op 0x21 - | I31Get ZX -> op 0xfb; op 0x22 - - | StructNew (x, Explicit) -> op 0xfb; op 0x01; var x - | StructNew (x, Implicit) -> op 0xfb; op 0x02; var x - | StructGet (x, y, None) -> op 0xfb; op 0x03; var x; var y - | StructGet (x, y, Some SX) -> op 0xfb; op 0x04; var x; var y - | StructGet (x, y, Some ZX) -> op 0xfb; op 0x05; var x; var y - | StructSet (x, y) -> op 0xfb; op 0x06; var x; var y - - | ArrayNew (x, Explicit) -> op 0xfb; op 0x11; var x - | ArrayNew (x, Implicit) -> op 0xfb; op 0x12; var x - | ArrayNewFixed (x, n) -> op 0xfb; op 0x19; var x; u32 n - | ArrayNewElem (x, y) -> op 0xfb; op 0x1c; var x; var y - | ArrayNewData (x, y) -> op 0xfb; op 0x1b; var x; var y - | ArrayGet (x, None) -> op 0xfb; op 0x13; var x - | ArrayGet (x, Some SX) -> op 0xfb; op 0x14; var x - | ArrayGet (x, Some ZX) -> op 0xfb; op 0x15; var x - | ArraySet x -> op 0xfb; op 0x16; var x - | ArrayLen -> op 0xfb; op 0x17 - - | ArrayCopy (x, y) -> op 0xfb; op 0x18; var x; var y - | ArrayFill x -> op 0xfb; op 0x0f; var x - | ArrayInitData (x, y) -> op 0xfb; op 0x54; var x; var y - | ArrayInitElem (x, y) -> op 0xfb; op 0x55; var x; var y - - | ExternConvert Internalize -> op 0xfb; op 0x70 - | ExternConvert Externalize -> op 0xfb; op 0x71 + | I31New -> op 0xfb; op 0x1c + | I31Get SX -> op 0xfb; op 0x1d + | I31Get ZX -> op 0xfb; op 0x1e + + | StructNew (x, Explicit) -> op 0xfb; op 0x00; var x + | StructNew (x, Implicit) -> op 0xfb; op 0x01; var x + | StructGet (x, y, None) -> op 0xfb; op 0x02; var x; var y + | StructGet (x, y, Some SX) -> op 0xfb; op 0x03; var x; var y + | StructGet (x, y, Some ZX) -> op 0xfb; op 0x04; var x; var y + | StructSet (x, y) -> op 0xfb; op 0x05; var x; var y + + | ArrayNew (x, Explicit) -> op 0xfb; op 0x06; var x + | ArrayNew (x, Implicit) -> op 0xfb; op 0x07; var x + | ArrayNewFixed (x, n) -> op 0xfb; op 0x08; var x; u32 n + | ArrayNewElem (x, y) -> op 0xfb; op 0x0a; var x; var y + | ArrayNewData (x, y) -> op 0xfb; op 0x09; var x; var y + | ArrayGet (x, None) -> op 0xfb; op 0x0b; var x + | ArrayGet (x, Some SX) -> op 0xfb; op 0x0c; var x + | ArrayGet (x, Some ZX) -> op 0xfb; op 0x0d; var x + | ArraySet x -> op 0xfb; op 0x0e; var x + | ArrayLen -> op 0xfb; op 0x0f + | ArrayFill x -> op 0xfb; op 0x10; var x + | ArrayCopy (x, y) -> op 0xfb; op 0x11; var x; var y + | ArrayInitData (x, y) -> op 0xfb; op 0x12; var x; var y + | ArrayInitElem (x, y) -> op 0xfb; op 0x13; var x; var y + + | ExternConvert Internalize -> op 0xfb; op 0x1a + | ExternConvert Externalize -> op 0xfb; op 0x1b | Const {it = I32 c; _} -> op 0x41; s32 c | Const {it = I64 c; _} -> op 0x42; s64 c diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index efda212c7..6382005df 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -721,25 +721,25 @@ This extends the [encodings](https://github.com/WebAssembly/function-references/ | Opcode | Type | | ------ | --------------- | -| -0x06 | `i8` | -| -0x07 | `i16` | +| -0x08 | `i8` | +| -0x09 | `i16` | #### Reference Types | Opcode | Type | Parameters | Note | | ------ | --------------- | ---------- | ---- | +| -0x0d | `nullfuncref` | | shorthand | +| -0x0e | `nullexternref` | | shorthand | +| -0x0f | `nullref` | | shorthand | | -0x10 | `funcref` | | shorthand, from reftype proposal | | -0x11 | `externref` | | shorthand, from reftype proposal | | -0x12 | `anyref` | | shorthand | | -0x13 | `eqref` | | shorthand | -| -0x14 | `(ref null ht)` | `ht : heaptype (s33)` | from funcref proposal | -| -0x15 | `(ref ht)` | `ht : heaptype (s33)` | from funcref proposal | -| -0x16 | `i31ref` | | shorthand | -| -0x17 | `nullfuncref` | | shorthand | -| -0x18 | `nullexternref` | | shorthand | -| -0x19 | `structref` | | shorthand | -| -0x1a | `arrayref` | | shorthand | -| -0x1b | `nullref` | | shorthand | +| -0x14 | `i31ref` | | shorthand | +| -0x15 | `structref` | | shorthand | +| -0x16 | `arrayref` | | shorthand | +| -0x1c | `(ref ht)` | `ht : heaptype (s33)` | from funcref proposal | +| -0x1d | `(ref null ht)` | `ht : heaptype (s33)` | from funcref proposal | #### Heap Types @@ -748,42 +748,45 @@ The opcode for heap types is encoded as an `s33`. | Opcode | Type | Parameters | Note | | ------ | --------------- | ---------- | ---- | | i >= 0 | `(type i)` | | from funcref proposal | +| -0x0d | `nofunc` | | | +| -0x0e | `noextern` | | | +| -0x0f | `none` | | | | -0x10 | `func` | | from funcref proposal | | -0x11 | `extern` | | from funcref proposal | | -0x12 | `any` | | | | -0x13 | `eq` | | | -| -0x16 | `i31` | | | -| -0x17 | `nofunc` | | | -| -0x18 | `noextern` | | | -| -0x19 | `struct` | | | -| -0x1a | `array` | | | -| -0x1b | `none` | | | +| -0x14 | `i31` | | | +| -0x15 | `struct` | | | +| -0x16 | `array` | | | #### Composite Types -| Opcode | Type | Parameters | -| ------ | --------------- | ---------- | -| -0x21 | `struct ft*` | `ft* : vec(fieldtype)` | -| -0x22 | `array ft` | `ft : fieldtype` | +| Opcode | Type | Parameters | Note | +| ------ | --------------- | ---------- | ---- | +| -0x20 | `func t1* t2*` | `t1* : vec(valtype)`, `t2* : vec(valtype)` | from Wasm 1.0 | +| -0x21 | `struct ft*` | `ft* : vec(fieldtype)` | | +| -0x22 | `array ft` | `ft : fieldtype` | | #### Subtypes | Opcode | Type | Parameters | Note | | ------ | --------------- | ---------- | ---- | +| -0x20 | `func t1* t2*` | `t1* : vec(valtype)`, `t2* : vec(valtype)` | shorthand | | -0x21 | `struct ft*` | `ft* : vec(fieldtype)` | shorthand | | -0x22 | `array ft` | `ft : fieldtype` | shorthand | | -0x30 | `sub $t* st` | `$t* : vec(typeidx)`, `st : comptype` | | -| -0x32 | `sub final $t* st` | `$t* : vec(typeidx)`, `st : comptype` | | +| -0x31 | `sub final $t* st` | `$t* : vec(typeidx)`, `st : comptype` | | #### Defined Types | Opcode | Type | Parameters | Note | | ------ | --------------- | ---------- | ---- | +| -0x20 | `func t1* t2*` | `t1* : vec(valtype)`, `t2* : vec(valtype)` | shorthand | | -0x21 | `struct ft*` | `ft* : vec(fieldtype)` | shorthand | | -0x22 | `array ft` | `ft : fieldtype` | shorthand | | -0x30 | `sub $t* st` | `$t* : vec(typeidx)`, `st : comptype` | shorthand | -| -0x31 | `rec dt*` | `dt* : vec(subtype)` | | -| -0x32 | `sub final $t* st` | `$t* : vec(typeidx)`, `st : comptype` | shorthand | +| -0x31 | `sub final $t* st` | `$t* : vec(typeidx)`, `st : comptype` | shorthand | +| -0x32 | `rec dt*` | `dt* : vec(subtype)` | | #### Field Types @@ -794,41 +797,46 @@ The opcode for heap types is encoded as an `s33`. ### Instructions -| Opcode | Type | Parameters | -| ------ | --------------- | ---------- | -| 0xd5 | `ref.eq` | | -| 0xd6 | `br_on_non_null $l` | `$l : labelidx` | -| 0xfb01 | `struct.new $t` | `$t : typeidx` | -| 0xfb02 | `struct.new_default $t` | `$t : typeidx` | -| 0xfb03 | `struct.get $t i` | `$t : typeidx`, `i : fieldidx` | -| 0xfb04 | `struct.get_s $t i` | `$t : typeidx`, `i : fieldidx` | -| 0xfb05 | `struct.get_u $t i` | `$t : typeidx`, `i : fieldidx` | -| 0xfb06 | `struct.set $t i` | `$t : typeidx`, `i : fieldidx` | -| 0xfb0f | `array.fill $t` | `$t : typeidx` | -| 0xfb11 | `array.new $t` | `$t : typeidx` | -| 0xfb12 | `array.new_default $t` | `$t : typeidx` | -| 0xfb13 | `array.get $t` | `$t : typeidx` | -| 0xfb14 | `array.get_s $t` | `$t : typeidx` | -| 0xfb15 | `array.get_u $t` | `$t : typeidx` | -| 0xfb16 | `array.set $t` | `$t : typeidx` | -| 0xfb17 | `array.len` | | -| 0xfb18 | `array.copy $t1 $t2` | `$t1 : typeidx`, `$t2 : typeidx` | -| 0xfb19 | `array.new_fixed $t N` | `$t : typeidx`, `N : u32` | -| 0xfb1b | `array.new_data $t $d` | `$t : typeidx`, `$d : dataidx` | -| 0xfb1c | `array.new_elem $t $e` | `$t : typeidx`, `$e : elemidx` | -| 0xfb20 | `i31.new` | | -| 0xfb21 | `i31.get_s` | | -| 0xfb22 | `i31.get_u` | | -| 0xfb40 | `ref.test (ref ht)` | `ht : heaptype` | -| 0xfb41 | `ref.cast (ref ht)` | `ht : heaptype` | -| 0xfb48 | `ref.test (ref null ht)` | `ht : heaptype` | -| 0xfb49 | `ref.cast (ref null ht)` | `ht : heaptype` | -| 0xfb4e | `br_on_cast $l (ref null1? ht1) (ref null2? ht2)` | `flags : u8`, $l : labelidx`, `ht1 : heaptype`, `ht2 : heaptype` | -| 0xfb4f | `br_on_cast_fail $l (ref null1? ht1) (ref null2? ht2)` | `flags : u8`, $l : labelidx`, `ht1 : heaptype`, `ht2 : heaptype` | -| 0xfb54 | `array.init_data $t $d` | `$t : typeidx`, `$d: dataidx` | -| 0xfb55 | `array.init_elem $t $e` | `$t : typeidx`, `$d: elemidx` | -| 0xfb70 | `extern.internalize` | | -| 0xfb71 | `extern.externalize` | | +| Opcode | Type | Parameters | Note | +| ------ | --------------- | ---------- | ---- | +| 0xd0 | `ref.null ht` | `ht : heap_type` | from Wasm 2.0 | +| 0xd1 | `ref.is_null` | | from Wasm 2.0 | +| 0xd2 | `ref.func $f` | `$f : funcidx` | from Wasm 2.0 | +| 0xd3 | `ref.eq` | | +| 0xd4 | `ref.as_non_null` | | from funcref proposal | +| 0xd5 | `br_on_null $l` | `$l : u32` | from funcref proposal | +| 0xd6 | `br_on_non_null $l` | `$l : u32` | from funcref proposal | +| 0xfb00 | `struct.new $t` | `$t : typeidx` | +| 0xfb01 | `struct.new_default $t` | `$t : typeidx` | +| 0xfb02 | `struct.get $t i` | `$t : typeidx`, `i : fieldidx` | +| 0xfb03 | `struct.get_s $t i` | `$t : typeidx`, `i : fieldidx` | +| 0xfb04 | `struct.get_u $t i` | `$t : typeidx`, `i : fieldidx` | +| 0xfb05 | `struct.set $t i` | `$t : typeidx`, `i : fieldidx` | +| 0xfb06 | `array.new $t` | `$t : typeidx` | +| 0xfb07 | `array.new_default $t` | `$t : typeidx` | +| 0xfb08 | `array.new_fixed $t N` | `$t : typeidx`, `N : u32` | +| 0xfb09 | `array.new_data $t $d` | `$t : typeidx`, `$d : dataidx` | +| 0xfb0a | `array.new_elem $t $e` | `$t : typeidx`, `$e : elemidx` | +| 0xfb0b | `array.get $t` | `$t : typeidx` | +| 0xfb0c | `array.get_s $t` | `$t : typeidx` | +| 0xfb0d | `array.get_u $t` | `$t : typeidx` | +| 0xfb0e | `array.set $t` | `$t : typeidx` | +| 0xfb0f | `array.len` | +| 0xfb10 | `array.fill $t` | +| 0xfb11 | `array.copy $t1 $t2` | +| 0xfb12 | `array.init_data $t $d` | +| 0xfb13 | `array.init_elem $t $e` | +| 0xfb14 | `ref.test (ref ht)` | `ht : heaptype` | +| 0xfb15 | `ref.test (ref null ht)` | `ht : heaptype` | +| 0xfb16 | `ref.cast (ref ht)` | `ht : heaptype` | +| 0xfb17 | `ref.cast (ref null ht)` | `ht : heaptype` | +| 0xfb18 | `br_on_cast $l (ref null1? ht1) (ref null2? ht2)` | `flags : u8`, $l : labelidx`, `ht1 : heaptype`, `ht2 : heaptype` | +| 0xfb19 | `br_on_cast_fail $l (ref null1? ht1) (ref null2? ht2)` | `flags : u8`, $l : labelidx`, `ht1 : heaptype`, `ht2 : heaptype` | +| 0xfb1a | `extern.internalize` | +| 0xfb1b | `extern.externalize` | +| 0xfb1c | `i31.new` | +| 0xfb1d | `i31.get_s` | +| 0xfb1e | `i31.get_u` | Flag byte encoding for `br_on_cast(_fail)?`: From 07970345efd9d3fb2817e62232394ed59584e73b Mon Sep 17 00:00:00 2001 From: YiYing He Date: Fri, 4 Aug 2023 11:11:28 +0800 Subject: [PATCH 02/20] Use another name for registering a new module in test. Signed-off-by: YiYing He --- test/core/type-equivalence.wast | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/test/core/type-equivalence.wast b/test/core/type-equivalence.wast index 4e295061f..4d6288b1f 100644 --- a/test/core/type-equivalence.wast +++ b/test/core/type-equivalence.wast @@ -118,15 +118,15 @@ (func (export "f1") (param (ref $t1))) (func (export "f2") (param (ref $t1))) ) -(register "M") +(register "N") (module (type $s0 (func (param i32) (result f32))) (type $s1 (func (param i32 (ref $s0)) (result (ref $s0)))) (type $s2 (func (param i32 (ref $s0)) (result (ref $s0)))) (type $t1 (func (param (ref $s1)) (result (ref $s2)))) (type $t2 (func (param (ref $s2)) (result (ref $s1)))) - (func (import "M" "f1") (param (ref $t1))) - (func (import "M" "f1") (param (ref $t2))) - (func (import "M" "f2") (param (ref $t1))) - (func (import "M" "f2") (param (ref $t1))) + (func (import "N" "f1") (param (ref $t1))) + (func (import "N" "f1") (param (ref $t2))) + (func (import "N" "f2") (param (ref $t1))) + (func (import "N" "f2") (param (ref $t1))) ) From 3a4e5a06c1f4d93e664494e871f3f64b8e66c479 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Sun, 6 Aug 2023 11:03:15 -0700 Subject: [PATCH 03/20] Update binary encodings Update the encodings for ref.as_non_null, br_on_null, (ref ht), and (ref null ht) for consistency with the final encodings chosen in https://github.com/WebAssembly/gc/pull/372. Fixes #103. --- document/core/appendix/index-instructions.py | 6 +++--- document/core/appendix/index-types.rst | 8 ++++---- document/core/binary/instructions.rst | 4 ++-- document/core/binary/types.rst | 4 ++-- interpreter/binary/decode.ml | 10 +++++----- interpreter/binary/encode.ml | 8 ++++---- 6 files changed, 20 insertions(+), 20 deletions(-) diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index 00cb5800d..955ec2c48 100755 --- a/document/core/appendix/index-instructions.py +++ b/document/core/appendix/index-instructions.py @@ -280,9 +280,9 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\REFNULL~\X{ht}', r'\hex{D0}', r'[] \to [(\REF~\NULL~\X{ht})]', r'valid-ref.null', r'exec-ref.null'), Instruction(r'\REFISNULL', r'\hex{D1}', r'[(\REF~\NULL~\X{ht})] \to [\I32]', r'valid-ref.is_null', r'exec-ref.is_null'), Instruction(r'\REFFUNC~x', r'\hex{D2}', r'[] \to [\FUNCREF]', r'valid-ref.func', r'exec-ref.func'), - Instruction(r'\REFASNONNULL', r'\hex{D3}', r'[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]', r'valid-ref.as_non_null', r'exec-ref.as_non_null'), - Instruction(r'\BRONNULL~l', r'\hex{D4}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]', r'valid-br_on_null', r'exec-br_on_null'), - Instruction(None, r'\hex{D5}'), + Instruction(None, r'\hex{D3}'), + Instruction(r'\REFASNONNULL', r'\hex{D4}', r'[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]', r'valid-ref.as_non_null', r'exec-ref.as_non_null'), + Instruction(r'\BRONNULL~l', r'\hex{D5}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]', r'valid-br_on_null', r'exec-br_on_null'), Instruction(r'\BRONNONNULL~l', r'\hex{D6}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast]', r'valid-br_on_non_null', r'exec-br_on_non_null'), Instruction(None, r'\hex{D7}'), Instruction(None, r'\hex{D8}'), diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst index 9db74d3b3..c1f459495 100644 --- a/document/core/appendix/index-types.rst +++ b/document/core/appendix/index-types.rst @@ -16,10 +16,10 @@ Category Constructor (reserved) :math:`\hex{7A}` .. :math:`\hex{71}` :ref:`Heap type ` |FUNC| :math:`\hex{70}` (-16 as |Bs7|) :ref:`Heap type ` |EXTERN| :math:`\hex{6F}` (-17 as |Bs7|) -(reserved) :math:`\hex{6E}` .. :math:`\hex{6D}` -:ref:`Reference type ` |REF| |NULL| :math:`\hex{6C}` (-20 as |Bs7|) -:ref:`Reference type ` |REF| :math:`\hex{6B}` (-21 as |Bs7|) -(reserved) :math:`\hex{6A}` .. :math:`\hex{61}` +(reserved) :math:`\hex{6E}` .. :math:`\hex{65}` +:ref:`Reference type ` |REF| :math:`\hex{64}` (-28 as |Bs7|) +:ref:`Reference type ` |REF| |NULL| :math:`\hex{63}` (-29 as |Bs7|) +(reserved) :math:`\hex{62}` .. :math:`\hex{61}` :ref:`Function type ` :math:`[\valtype^\ast] \toF[\valtype^\ast]` :math:`\hex{60}` (-32 as |Bs7|) (reserved) :math:`\hex{5F}` .. :math:`\hex{41}` :ref:`Result type ` :math:`[\epsilon]` :math:`\hex{40}` (-64 as |Bs7|) diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 175526bb8..80ac806cf 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -72,7 +72,7 @@ Control Instructions \hex{13}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \RETURNCALLINDIRECT~x~y \\ &&|& \hex{14}~~x{:}\Btypeidx &\Rightarrow& \CALLREF~x \\ &&|& \hex{15}~~x{:}\Btypeidx &\Rightarrow& \RETURNCALLREF~x \\ &&|& - \hex{D4}~~l{:}\Blabelidx &\Rightarrow& \BRONNULL~l \\ &&|& + \hex{D5}~~l{:}\Blabelidx &\Rightarrow& \BRONNULL~l \\ &&|& \hex{D6}~~l{:}\Blabelidx &\Rightarrow& \BRONNONNULL~l \\ \end{array} @@ -103,7 +103,7 @@ Reference Instructions \hex{D0}~~t{:}\Bheaptype &\Rightarrow& \REFNULL~t \\ &&|& \hex{D1} &\Rightarrow& \REFISNULL \\ &&|& \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\ &&|& - \hex{D3} &\Rightarrow& \REFASNONNULL \\ + \hex{D4} &\Rightarrow& \REFASNONNULL \\ \end{array} diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index 08a30d521..9c05d7840 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -75,8 +75,8 @@ Reference Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} \production{reference type} & \Breftype &::=& - \hex{6B}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\X{ht} \\ &&|& - \hex{6C}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\NULL~\X{ht} \\ &&|& + \hex{63}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\NULL~\X{ht} \\ &&|& + \hex{64}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\X{ht} \\ &&|& \hex{6F} &\Rightarrow& \EXTERNREF \\ &&|& \hex{70} &\Rightarrow& \FUNCREF \\ \end{array} diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 8fa6db0b1..887da409b 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -180,8 +180,8 @@ let ref_type s = match s7 s with | -0x10 -> (Null, FuncHT) | -0x11 -> (Null, ExternHT) - | -0x14 -> (Null, heap_type s) - | -0x15 -> (NoNull, heap_type s) + | -0x1c -> (NoNull, heap_type s) + | -0x1d -> (Null, heap_type s) | _ -> error s pos "malformed reference type" let val_type s = @@ -522,9 +522,9 @@ let rec instr s = | 0xd0 -> ref_null (heap_type s) | 0xd1 -> ref_is_null | 0xd2 -> ref_func (at var s) - | 0xd3 -> ref_as_non_null - | 0xd4 -> br_on_null (at var s) - | 0xd5 as b -> illegal s pos b + | 0xd3 as b -> illegal s pos b + | 0xd4 -> ref_as_non_null + | 0xd5 -> br_on_null (at var s) | 0xd6 -> br_on_non_null (at var s) | 0xfc as b -> diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 621103513..7f9bb347f 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -116,8 +116,8 @@ struct let ref_type = function | (Null, FuncHT) -> s7 (-0x10) | (Null, ExternHT) -> s7 (-0x11) - | (Null, t) -> s7 (-0x14); heap_type t - | (NoNull, t) -> s7 (-0x15); heap_type t + | (NoNull, t) -> s7 (-0x1c); heap_type t + | (Null, t) -> s7 (-0x1d); heap_type t let val_type = function | NumT t -> num_type t @@ -193,7 +193,7 @@ struct | Br x -> op 0x0c; var x | BrIf x -> op 0x0d; var x | BrTable (xs, x) -> op 0x0e; vec var xs; var x - | BrOnNull x -> op 0xd4; var x + | BrOnNull x -> op 0xd5; var x | BrOnNonNull x -> op 0xd6; var x | Return -> op 0x0f | Call x -> op 0x10; var x @@ -318,7 +318,7 @@ struct | RefNull t -> op 0xd0; heap_type t | RefFunc x -> op 0xd2; var x | RefIsNull -> op 0xd1 - | RefAsNonNull -> op 0xd3 + | RefAsNonNull -> op 0xd4 | Const {it = I32 c; _} -> op 0x41; s32 c | Const {it = I64 c; _} -> op 0x42; s64 c From 1d9585f29845a1bfbc7d6f17b51aeb272b6e28fd Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 9 Aug 2023 17:42:19 +0200 Subject: [PATCH 04/20] Fix JS integer conversion (#411) Fix #399 and a couple of other small bugs with conversion to/from JS numbers. --- document/js-api/index.bs | 29 +++++++++++++++++++---------- 1 file changed, 19 insertions(+), 10 deletions(-) diff --git a/document/js-api/index.bs b/document/js-api/index.bs index 5ac847fab..0e17977a0 100644 --- a/document/js-api/index.bs +++ b/document/js-api/index.bs @@ -168,6 +168,7 @@ urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: df text: var text: const text: address; url: exec/runtime.html#addresses + text: signed_31; url: exec/numerics.html#aux-signed text: signed_32; url: exec/numerics.html#aux-signed text: memory.grow; url: exec/instructions.html#exec-memory-grow text: current frame; url: exec/conventions.html#exec-notation-textual @@ -1079,10 +1080,12 @@ Note: Exported Functions do not have a \[[Construct]] method and thus it is not The algorithm ToJSValue(|w|) coerces a [=WebAssembly value=] to a JavaScript value by performing the following steps: 1. Assert: |w| is not of the form [=v128.const=] v128. -1. If |w| is of the form [=i64.const=] |i64|, - 1. Let |v| be [=signed_64=](|i64|). - 1. Return [=ℤ=](|v| interpreted as a mathematical value). -1. If |w| is of the form [=i32.const=] |i32|, return [=𝔽=]([=signed_32=](|i32| interpreted as a mathematical value)). +1. If |w| is of the form [=i64.const=] |u64|, + 1. Let |i64| be [=signed_64=](|u64|). + 1. Return [=ℤ=](|i64| interpreted as a mathematical value). +1. If |w| is of the form [=i32.const=] |u32|, + 1. Let |i32| be [=signed_32=](|i32|). + 2. Return [=𝔽=](|i32| interpreted as a mathematical value). 1. If |w| is of the form [=f32.const=] |f32|, 1. If |f32| is [=+∞=] or [=−∞=], return **+∞**𝔽 or **-∞**𝔽, respectively. 1. If |f32| is [=nan=], return **NaN**. @@ -1091,8 +1094,10 @@ The algorithm ToJSValue(|w|) coerces a [=WebAssembly value=] to a Jav 1. If |f64| is [=+∞=] or [=−∞=], return **+∞**𝔽 or **-∞**𝔽, respectively. 1. If |f64| is [=nan=], return **NaN**. 1. Return [=𝔽=](|f64| interpreted as a mathematical value). -1. If |w| is of the form [=ref.null=] t, return null. -1. If |w| is of the form [=ref.i31=] i, return [=ℤ=](|i|). +1. If |w| is of the form [=ref.null=] |t|, return null. +1. If |w| is of the form [=ref.i31=] |u31|, + 1. Let |i31| be [=signed_31=](|u31|). + 1. Let return [=𝔽=](|i31|). 1. If |w| is of the form [=ref.struct=] |structaddr|, return the result of creating [=a new Exported GC Object=] from |structaddr| and "struct". 1. If |w| is of the form [=ref.array=] |arrayaddr|, return the result of creating [=a new Exported GC Object=] from |arrayaddr| and "array". 1. If |w| is of the form [=ref.func=] |funcaddr|, return the result of creating [=a new Exported Function=] from |funcaddr|. @@ -1119,10 +1124,12 @@ The algorithm ToWebAssemblyValue(|v|, |type|) coerces a JavaScript va 1. Assert: |type| is not [=v128=]. 1. If |type| is [=i64=], 1. Let |i64| be [=?=] [$ToBigInt64$](|v|). - 1. Return [=i64.const=] |i64|. + 1. Let |u64| be the unsigned integer such that |i64| is [=signed_64=](|u64|). + 1. Return [=i64.const=] |u64|. 1. If |type| is [=i32=], 1. Let |i32| be [=?=] [$ToInt32$](|v|). - 1. Return [=i32.const=] |i32|. + 1. Let |u32| be the unsigned integer such that |i32| is [=signed_32=](|u32|). + 1. Return [=i32.const=] |u32|. 1. If |type| is [=f32=], 1. Let |number| be [=?=] [$ToNumber$](|v|). 1. If |number| is **NaN**, @@ -1145,8 +1152,10 @@ The algorithm ToWebAssemblyValue(|v|, |type|) coerces a JavaScript va 1. Return [=ref.extern=] |r|. 1. If |v| is null, 1. Let |r| be [=ref.null=] |heaptype|. - 1. Else if |v| [=is a Number=] and |v| is equal to ? [$ToInt32$](|v|) and [=ℝ=](|v|) < 230 and [=ℝ=](|v|) ⩾ -230, - 1. Let |r| be [=ref.i31=] |v|. + 1. Else if |v| [=is a Number=] and |v| is equal to [=?=] [$ToInt32$](|v|) and [=ℝ=](|v|) < 230 and [=ℝ=](|v|) ⩾ -230, + 1. Let |i31| [=?=] [$ToInt32$](|v|). + 1. Let |u31| be the unsigned integer such that |i31| is [=signed_31=](|i31|). + 1. Let |r| be [=ref.i31=] |u31|. 1. Else if |v| is an [=Exported Function=], 1. Let |funcaddr| be the value of |v|'s \[[FunctionAddress]] internal slot. 1. Let |r| be [=ref.func=] |funcaddr|. From 89d13db959222c0e22be6cfc047a83c477daa26a Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Thu, 17 Aug 2023 12:54:44 -0700 Subject: [PATCH 05/20] update Overview.md as well --- proposals/function-references/Overview.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md index eb32bc371..6aa48b1d9 100644 --- a/proposals/function-references/Overview.md +++ b/proposals/function-references/Overview.md @@ -272,7 +272,7 @@ Typing of instruction sequences is updated to account for initialization of loca - `epsilon : [] -> [] epsilon` Note: These typing rules do not try to eliminate duplicate indices, but an implementation could. - + A subsumption rule allows to go to a supertype for any instruction: * `instr` @@ -302,8 +302,8 @@ Table definitions have an initialiser value: | ------ | --------------- | ---------- | | -0x10 | `funcref` | | | -0x11 | `externref` | | -| -0x14 | `(ref null ht)` | `$t : heaptype` | -| -0x15 | `(ref ht)` | `$t : heaptype` | +| -0x1c | `(ref ht)` | `$t : heaptype` | +| -0x1d | `(ref null ht)` | `$t : heaptype` | #### Heap Types @@ -321,8 +321,8 @@ The opcode for heap types is encoded as an `s33`. | ------ | ------------------------ | ---------- | | 0x14 | `call_ref $t` | `$t : u32` | | 0x15 | `return_call_ref $t` | `$t : u32` | -| 0xd3 | `ref.as_non_null` | | -| 0xd4 | `br_on_null $l` | `$l : u32` | +| 0xd4 | `ref.as_non_null` | | +| 0xd5 | `br_on_null $l` | `$l : u32` | | 0xd6 | `br_on_non_null $l` | `$l : u32` | ### Tables From 028daa2f5ecb84cc118574cd6fca798ca0b1322a Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Thu, 24 Aug 2023 12:16:39 -0700 Subject: [PATCH 06/20] Update array.copy semantics to handle packed types Previously the array.copy semantics were defined in terms of executing array.get on the source array, which is not correct if the source array contains a packed type. Update the semantics prose and formalism to choose between array.get and array.get_u depending on whether the array contents are packed. The interpreter does not need updating because it already handled the difference correctly. --- document/core/exec/instructions.rst | 84 ++++++++++++++++++----------- 1 file changed, 53 insertions(+), 31 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index a3e4d7691..3d6e0770a 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1120,61 +1120,75 @@ Reference Instructions :math:`\ARRAYCOPY~x~y` ...................... -.. todo:: Handle packed fields correctly via array.get_u instead of array.get +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]` exists. -1. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]`. -2. Pop the value :math:`n` from the stack. +3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. -3. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +4. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. -4. Pop the value :math:`s` from the stack. +5. If :math:`\X{ft} = \mut~\packedtype`, then: -5. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~y)` is on the top of the stack. + a. Let :math:`\X{get}` be the instruction :math:`\ARRAYGETU~y`. + +6. Else: -6. Pop the value :math:`\reff_2` from the stack. + a. Let :math:`\X{get}` be the instruction :math:`\ARRAYGET~y`. 7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -8. Pop the value :math:`d` from the stack. +8. Pop the value :math:`n` from the stack. + +9. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. + +10. Pop the value :math:`s` from the stack. + +11. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~y)` is on the top of the stack. + +12. Pop the value :math:`\reff_2` from the stack. -9. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. +13. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -10. Pop the value :math:`\reff_1` from the stack. +14. Pop the value :math:`d` from the stack. -11. If :math:`\reff_1` is :math:`\REFNULL~t`, then: +15. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. + +16. Pop the value :math:`\reff_1` from the stack. + +17. If :math:`\reff_1` is :math:`\REFNULL~t`, then: a. Trap. -12. Assert: due to :ref:`validation `, :math:`\reff_1` is an :ref:`array reference `. +18. Assert: due to :ref:`validation `, :math:`\reff_1` is an :ref:`array reference `. -13. Let :math:`\REFARRAYADDR~a_1` be the reference value :math:`\reff_1`. +19. Let :math:`\REFARRAYADDR~a_1` be the reference value :math:`\reff_1`. -14. If :math:`\reff_2` is :math:`\REFNULL~t`, then: +20. If :math:`\reff_2` is :math:`\REFNULL~t`, then: a. Trap. -15. Assert: due to :ref:`validation `, :math:`\reff_2` is an :ref:`array reference `. +21. Assert: due to :ref:`validation `, :math:`\reff_2` is an :ref:`array reference `. -16. Let :math:`\REFARRAYADDR~a_2` be the reference value :math:`\reff_2`. +22. Let :math:`\REFARRAYADDR~a_2` be the reference value :math:`\reff_2`. -17. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_1]` exists. +23. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_1]` exists. -18. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_2]` exists. +24. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_2]` exists. -19. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then: +25. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then: a. Trap. -20. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then: +26. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then: a. Trap. -21. If :math:`n = 0`, then: +27. If :math:`n = 0`, then: a. Return. -22. If :math:`d \leq s`, then: +28. If :math:`d \leq s`, then: a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. @@ -1184,7 +1198,7 @@ Reference Instructions d. Push the value :math:`\I32.\CONST~s` to the stack. - e. Execute the instruction :math:`\ARRAYGET~y`. + e. Execute :math:`\X{get}`. f. Execute the instruction :math:`\ARRAYSET~x`. @@ -1200,7 +1214,7 @@ Reference Instructions l. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -23. Else: +29. Else: a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. @@ -1214,7 +1228,7 @@ Reference Instructions f. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack. - g. Execute the instruction :math:`\ARRAYGET~y`. + g. Execute :math:`\X{get}`. h. Execute the instruction :math:`\ARRAYSET~x`. @@ -1226,9 +1240,9 @@ Reference Instructions l. Push the value :math:`\I32.\CONST~s` to the stack. -24. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +30. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -25. Execute the instruction :math:`\ARRAYCOPY~x~y`. +31. Execute the instruction :math:`\ARRAYCOPY~x~y`. .. math:: ~\\[-1ex] @@ -1248,24 +1262,32 @@ Reference Instructions \\ \quad S; \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\ARRAYGET~y) \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~\X{get} \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d+1)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad - (\otherwise, \iff d \leq s) + \begin{array}[t]{@{}r@{~}l@{}} + (\otherwise, \iff & d \leq s \\ + \land & (\X{get} = \ARRAYGET~y \vee \X{get} = \ARRAYGETU~y) \\ + \land & (F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\packedtype \Longleftrightarrow \X{get} = \ARRAYGETU~y)) + \end{array} \\[1ex] S; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYCOPY~x~y) \quad\stepto \\ \quad S; \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d+n) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~(\ARRAYGET~y) \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~\X{get} \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad - (\otherwise, \iff d > s) + \begin{array}[t]{@{}r@{~}l@{}} + (\otherwise, \iff & d > s \\ + \land & (\X{get} = \ARRAYGET~y \vee \X{get} = \ARRAYGETU~y) \\ + \land & (F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\packedtype \Longleftrightarrow \X{get} = \ARRAYGETU~y)) + \end{array} \\[1ex] S; (\REFNULL~t)~(\I32.\CONST~d)~\val~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \quad\stepto\quad \TRAP \\[1ex] From 95ae953cc313746879bea5b61cb7aeda333f4835 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Mon, 28 Aug 2023 09:54:46 -0500 Subject: [PATCH 07/20] Fix encoding inconsistencies (#414) Fix various places in the spec text and interpreter where binary encodings were inconsistent with those we decided on in #372. --- document/core/appendix/index-instructions.py | 6 +++--- document/core/appendix/index-types.rst | 3 ++- document/core/binary/instructions.rst | 6 +++--- interpreter/binary/decode.ml | 6 +++--- interpreter/binary/encode.ml | 8 ++++---- 5 files changed, 15 insertions(+), 14 deletions(-) diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index f779a6b66..0169d91b6 100755 --- a/document/core/appendix/index-instructions.py +++ b/document/core/appendix/index-instructions.py @@ -280,9 +280,9 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\REFNULL~\X{ht}', r'\hex{D0}', r'[] \to [(\REF~\NULL~\X{ht})]', r'valid-ref.null', r'exec-ref.null'), Instruction(r'\REFISNULL', r'\hex{D1}', r'[(\REF~\NULL~\X{ht})] \to [\I32]', r'valid-ref.is_null', r'exec-ref.is_null'), Instruction(r'\REFFUNC~x', r'\hex{D2}', r'[] \to [\FUNCREF]', r'valid-ref.func', r'exec-ref.func'), - Instruction(r'\REFASNONNULL', r'\hex{D3}', r'[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]', r'valid-ref.as_non_null', r'exec-ref.as_non_null'), - Instruction(r'\BRONNULL~l', r'\hex{D4}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]', r'valid-br_on_null', r'exec-br_on_null'), - Instruction(r'\REFEQ', r'\hex{D5}', r'[\EQREF~\EQREF] \to [\I32]', r'valid-ref.eq', r'exec-ref.eq'), + Instruction(r'\REFEQ', r'\hex{D3}', r'[\EQREF~\EQREF] \to [\I32]', r'valid-ref.eq', r'exec-ref.eq'), + Instruction(r'\REFASNONNULL', r'\hex{D4}', r'[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]', r'valid-ref.as_non_null', r'exec-ref.as_non_null'), + Instruction(r'\BRONNULL~l', r'\hex{D5}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]', r'valid-br_on_null', r'exec-br_on_null'), Instruction(r'\BRONNONNULL~l', r'\hex{D6}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast]', r'valid-br_on_non_null', r'exec-br_on_non_null'), Instruction(None, r'\hex{D7}'), Instruction(None, r'\hex{D8}'), diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst index 5d31e71c0..854eb4e17 100644 --- a/document/core/appendix/index-types.rst +++ b/document/core/appendix/index-types.rst @@ -26,9 +26,10 @@ Category Constructor :ref:`Heap type ` |I31| :math:`\hex{6C}` (-20 as |Bs7|) :ref:`Heap type ` |STRUCT| :math:`\hex{6B}` (-21 as |Bs7|) :ref:`Heap type ` |ARRAY| :math:`\hex{6A}` (-22 as |Bs7|) +(reserved) :math:`\hex{69}` .. :math:`\hex{65}` :ref:`Reference type ` |REF| :math:`\hex{64}` (-28 as |Bs7|) :ref:`Reference type ` |REF| |NULL| :math:`\hex{63}` (-29 as |Bs7|) -(reserved) :math:`\hex{64}` .. :math:`\hex{61}` +(reserved) :math:`\hex{62}` .. :math:`\hex{61}` :ref:`Composite type ` :math:`\TFUNC~[\valtype^\ast] \toF[\valtype^\ast]` :math:`\hex{60}` (-32 as |Bs7|) :ref:`Composite type ` :math:`\TSTRUCT~\fieldtype^\ast` :math:`\hex{5F}` (-33 as |Bs7|) :ref:`Composite type ` :math:`\TARRAY~\fieldtype` :math:`\hex{5E}` (-34 as |Bs7|) diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index a23c02cf0..8e9277019 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -75,7 +75,7 @@ Control Instructions \hex{13}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \RETURNCALLINDIRECT~x~y \\ &&|& \hex{14}~~x{:}\Btypeidx &\Rightarrow& \CALLREF~x \\ &&|& \hex{15}~~x{:}\Btypeidx &\Rightarrow& \RETURNCALLREF~x \\ &&|& - \hex{D4}~~l{:}\Blabelidx &\Rightarrow& \BRONNULL~l \\ &&|& + \hex{D5}~~l{:}\Blabelidx &\Rightarrow& \BRONNULL~l \\ &&|& \hex{D6}~~l{:}\Blabelidx &\Rightarrow& \BRONNONNULL~l \\ &&|& \hex{FB}~~24{:}\Bu32~~(\NULL_1^?,\NULL_2^?){:}\Bcastflags\\&&&~~~~l{:}\Blabelidx~~\X{ht}_1{:}\Bheaptype~~\X{ht}_2{:}\Bheaptype &\Rightarrow& \BRONCAST~l~(\REF~\NULL_1^?~\X{ht}_1)~(\REF~\NULL_2^?~\X{ht}_2) \\ &&|& \hex{FB}~~25{:}\Bu32~~(\NULL_1^?,\NULL_2^?){:}\Bcastflags\\&&&~~~~l{:}\Blabelidx~~\X{ht}_1{:}\Bheaptype~~\X{ht}_2{:}\Bheaptype &\Rightarrow& \BRONCASTFAIL~l~(\REF~\NULL_1^?~\X{ht}_1)~(\REF~\NULL_2^?~\X{ht}_2) \\ @@ -140,8 +140,8 @@ Generic :ref:`reference instructions ` are represented by sing \hex{D0}~~t{:}\Bheaptype &\Rightarrow& \REFNULL~t \\ &&|& \hex{D1} &\Rightarrow& \REFISNULL \\ &&|& \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\ &&|& - \hex{D3} &\Rightarrow& \REFASNONNULL \\ &&|& - \hex{D5} &\Rightarrow& \REFEQ \\ &&|& + \hex{D3} &\Rightarrow& \REFEQ \\ &&|& + \hex{D4} &\Rightarrow& \REFASNONNULL \\ &&|& \hex{FB}~~0{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \STRUCTNEW~x \\ &&|& \hex{FB}~~1{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \STRUCTNEWDEFAULT~x \\ &&|& \hex{FB}~~2{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTGET~x~i \\ &&|& diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index cbff7fb2b..10dcceabc 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -581,9 +581,9 @@ let rec instr s = | 0xd0 -> ref_null (heap_type s) | 0xd1 -> ref_is_null | 0xd2 -> ref_func (at var s) - | 0xd3 -> ref_as_non_null - | 0xd4 -> br_on_null (at var s) - | 0xd5 -> ref_eq + | 0xd3 -> ref_eq + | 0xd4 -> ref_as_non_null + | 0xd5 -> br_on_null (at var s) | 0xd6 -> br_on_non_null (at var s) | 0xfb as b -> diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index fe7be0db6..de5047446 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -245,7 +245,7 @@ struct | Br x -> op 0x0c; var x | BrIf x -> op 0x0d; var x | BrTable (xs, x) -> op 0x0e; vec var xs; var x - | BrOnNull x -> op 0xd4; var x + | BrOnNull x -> op 0xd5; var x | BrOnNonNull x -> op 0xd6; var x | BrOnCast (x, (nul1, t1), (nul2, t2)) -> let flags = bit 0 (nul1 = Null) + bit 1 (nul2 = Null) in @@ -376,15 +376,15 @@ struct | RefNull t -> op 0xd0; heap_type t | RefFunc x -> op 0xd2; var x + | RefEq -> op 0xd3 + | RefIsNull -> op 0xd1 - | RefAsNonNull -> op 0xd3 + | RefAsNonNull -> op 0xd4 | RefTest (NoNull, t) -> op 0xfb; op 0x14; heap_type t | RefTest (Null, t) -> op 0xfb; op 0x15; heap_type t | RefCast (NoNull, t) -> op 0xfb; op 0x16; heap_type t | RefCast (Null, t) -> op 0xfb; op 0x17; heap_type t - | RefEq -> op 0xd5 - | I31New -> op 0xfb; op 0x1c | I31Get SX -> op 0xfb; op 0x1d | I31Get ZX -> op 0xfb; op 0x1e From e80576e347ccd5ef80431cbd9276e54d36a4afe7 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Mon, 28 Aug 2023 13:31:46 -0500 Subject: [PATCH 08/20] Updated packed type encodings in the spec and interpreter (#417) This was missed in #372. --- document/core/appendix/index-types.rst | 5 +++-- document/core/binary/types.rst | 4 ++-- interpreter/binary/decode.ml | 4 ++-- interpreter/binary/encode.ml | 4 ++-- test/core/gc/binary-gc.wast | 2 +- 5 files changed, 10 insertions(+), 9 deletions(-) diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst index 854eb4e17..30cf30523 100644 --- a/document/core/appendix/index-types.rst +++ b/document/core/appendix/index-types.rst @@ -13,8 +13,9 @@ Category Constructor :ref:`Number type ` |F32| :math:`\hex{7D}` (-3 as |Bs7|) :ref:`Number type ` |F64| :math:`\hex{7C}` (-4 as |Bs7|) :ref:`Vector type ` |V128| :math:`\hex{7B}` (-5 as |Bs7|) -:ref:`Packed type ` |I8| :math:`\hex{7A}` (-6 as |Bs7|) -:ref:`Packed type ` |I16| :math:`\hex{79}` (-7 as |Bs7|) +(reserved) :math:`\hex{7a}` .. :math:`\hex{79}` +:ref:`Packed type ` |I8| :math:`\hex{78}` (-8 as |Bs7|) +:ref:`Packed type ` |I16| :math:`\hex{77}` (-9 as |Bs7|) (reserved) :math:`\hex{78}` .. :math:`\hex{74}` :ref:`Heap type ` |NOFUNC| :math:`\hex{73}` (-13 as |Bs7|) :ref:`Heap type ` |NOEXTERN| :math:`\hex{72}` (-14 as |Bs7|) diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index 39af72feb..e0267d00e 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -185,9 +185,9 @@ Aggregate Types t{:}\Bpackedtype &\Rightarrow& t \\ \production{packed type} & \Bpackedtype &::=& - \hex{7A} + \hex{78} &\Rightarrow& \I8 \\ &&|& - \hex{79} + \hex{77} &\Rightarrow& \I16 \\ \end{array} diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 10dcceabc..baaae3e72 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -220,8 +220,8 @@ let result_type s = vec val_type s let pack_type s = let pos = pos s in match s7 s with - | -0x06 -> Pack.Pack8 - | -0x07 -> Pack.Pack16 + | -0x08 -> Pack.Pack8 + | -0x09 -> Pack.Pack16 | _ -> error s pos "malformed storage type" let storage_type s = diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index de5047446..c1d8b47c7 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -153,8 +153,8 @@ struct | BotT -> assert false let pack_type = function - | Pack.Pack8 -> s7 (-0x06) - | Pack.Pack16 -> s7 (-0x07) + | Pack.Pack8 -> s7 (-0x08) + | Pack.Pack16 -> s7 (-0x09) | Pack.Pack32 | Pack.Pack64 -> assert false let storage_type = function diff --git a/test/core/gc/binary-gc.wast b/test/core/gc/binary-gc.wast index 3adb38200..52cf02ace 100644 --- a/test/core/gc/binary-gc.wast +++ b/test/core/gc/binary-gc.wast @@ -5,7 +5,7 @@ "\05" ;; Type section length "\01" ;; Types vector length "\5e" ;; Array type, -0x22 - "\7a" ;; Storage type: i8 or -0x06 + "\78" ;; Storage type: i8 or -0x08 "\02" ;; Mutability, should be 0 or 1, but isn't ) "malformed mutability" From ede9c0b4b2e91fb1c3d6ece69ccf493b53b02cbd Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 6 Sep 2023 07:08:47 -0700 Subject: [PATCH 09/20] Disable xref on toX because MathJax --- document/core/util/macros.def | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 010a061e9..ba3561c53 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -178,7 +178,10 @@ .. |toF| mathdef:: \xref{syntax/types}{syntax-functype}{\rightarrow} .. |to| mathdef:: \xref{syntax/types}{syntax-instrtype}{\rightarrow} -.. |toX#1| mathdef:: \xref{syntax/types}{syntax-instrtype}{\rightarrow_{#1}} +.. Unfortunately, MathJax somehow barfs on the use of xref in the expansion + of a macro with parameters, so we cannot hyperlink the arrow + .. |toX#1| mathdef:: \xref{syntax/types}{syntax-instrtype}{\rightarrow_{#1}} +.. |toX#1| mathdef:: \rightarrow_{#1} .. |BOT| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{bot}} From abae97d6019f0a0a7da6b54182f06ac2118abbf2 Mon Sep 17 00:00:00 2001 From: Ashley Nelson Date: Fri, 8 Sep 2023 12:55:16 -0700 Subject: [PATCH 10/20] Extends Name Section w/ Type & Field (#415) This PR updates the spec to add additional subsections for type and field within the custom name section. struct.get and struct.set are also updated to indicate that their field indices are of type fieldidx, instead of u32. As a result, the metavariable representation was updated from i (integers) to y (indices). Closes #193 --- document/core/appendix/changes.rst | 2 +- document/core/appendix/custom.rst | 34 ++++++++++++++++++ document/core/appendix/index-instructions.py | 8 ++--- document/core/binary/instructions.rst | 8 ++--- document/core/binary/modules.rst | 5 ++- document/core/exec/instructions.rst | 36 ++++++++++---------- document/core/syntax/instructions.rst | 6 ++-- document/core/syntax/modules.rst | 9 ++++- document/core/text/instructions.rst | 8 ++--- document/core/util/macros.def | 4 +++ document/core/valid/instructions.rst | 16 ++++----- 11 files changed, 92 insertions(+), 44 deletions(-) diff --git a/document/core/appendix/changes.rst b/document/core/appendix/changes.rst index 9dbf0cd43..e0bb708f0 100644 --- a/document/core/appendix/changes.rst +++ b/document/core/appendix/changes.rst @@ -165,7 +165,7 @@ Added more precise types for references [#proposal-typedref]_. * Extended :ref:`table definitions ` with optional initializer expression -.. index:: reference, reference type, heap type, field type, storage type, structure type, array type, composite type, sub type, recrusive type +.. index:: reference, reference type, heap type, field type, storage type, structure type, array type, composite type, sub type, recursive type Garbage Collection ~~~~~~~~~~~~~~~~~~ diff --git a/document/core/appendix/custom.rst b/document/core/appendix/custom.rst index c12ebf183..ee9b39c90 100644 --- a/document/core/appendix/custom.rst +++ b/document/core/appendix/custom.rst @@ -60,6 +60,8 @@ Id Subsection 0 :ref:`module name ` 1 :ref:`function names ` 2 :ref:`local names ` + 4 :ref:`type names ` +10 :ref:`field names ` == =========================================== Each subsection may occur at most once, and in order of increasing id. @@ -143,3 +145,35 @@ It consists of an :ref:`indirect name map ` assigning lo \production{local name subsection} & \Blocalnamesubsec &::=& \Bnamesubsection_2(\Bindirectnamemap) \\ \end{array} + + +.. index:: type, type index +.. _binary-typenamesec: + +Type Names +.............. + +The *type name subsection* has the id 4. +It consists of a :ref:`name map ` assigning type names to :ref:`type indices `. + +.. math:: + \begin{array}{llclll} + \production{type name subsection} & \Btypenamesubsec &::=& + \Bnamesubsection_1(\Bnamemap) \\ + \end{array} + + +.. index:: type, field, type index, field index +.. _binary-fieldnamesec: + +Field Names +........... + +The *field name subsection* has the id 10. +It consists of an :ref:`indirect name map ` assigning field names to :ref:`field indices ` grouped by :ref:`type indices `. + +.. math:: + \begin{array}{llclll} + \production{field name subsection} & \Bfieldnamesubsec &::=& + \Bnamesubsection_2(\Bindirectnamemap) \\ + \end{array} diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index 0169d91b6..80c8e8b03 100755 --- a/document/core/appendix/index-instructions.py +++ b/document/core/appendix/index-instructions.py @@ -322,10 +322,10 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(None, r'\hex{FA}'), Instruction(r'\STRUCTNEW~x', r'\hex{FB}~\hex{00}', r'[t^\ast] \to [(\REF~x)]', r'valid-struct.new', r'exec-struct.new'), Instruction(r'\STRUCTNEWDEFAULT~x', r'\hex{FB}~\hex{01}', r'[] \to [(\REF~x)]', r'valid-struct.new_default', r'exec-struct.new_default'), - Instruction(r'\STRUCTGET~x~i', r'\hex{FB}~\hex{02}', r'[(\REF~\NULL~x)] \to [t]', r'valid-struct.get', r'exec-struct.get'), - Instruction(r'\STRUCTGETS~x~i', r'\hex{FB}~\hex{03}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'), - Instruction(r'\STRUCTGETU~x~i', r'\hex{FB}~\hex{04}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'), - Instruction(r'\STRUCTSET~x~i', r'\hex{FB}~\hex{05}', r'[(\REF~\NULL~x)~t] \to []', r'valid-struct.set', r'exec-struct.set'), + Instruction(r'\STRUCTGET~x~y', r'\hex{FB}~\hex{02}', r'[(\REF~\NULL~x)] \to [t]', r'valid-struct.get', r'exec-struct.get'), + Instruction(r'\STRUCTGETS~x~y', r'\hex{FB}~\hex{03}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'), + Instruction(r'\STRUCTGETU~x~y', r'\hex{FB}~\hex{04}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'), + Instruction(r'\STRUCTSET~x~y', r'\hex{FB}~\hex{05}', r'[(\REF~\NULL~x)~t] \to []', r'valid-struct.set', r'exec-struct.set'), Instruction(r'\ARRAYNEW~x', r'\hex{FB}~\hex{06}', r'[t] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'), Instruction(r'\ARRAYNEWDEFAULT~x', r'\hex{FB}~\hex{07}', r'[] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'), Instruction(r'\ARRAYNEWFIXED~x~n', r'\hex{FB}~\hex{08}', r'[t^n] \to [(\REF~x)]', r'valid-array.new_fixed', r'exec-array.new_fixed'), diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 8e9277019..2aebc124d 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -144,10 +144,10 @@ Generic :ref:`reference instructions ` are represented by sing \hex{D4} &\Rightarrow& \REFASNONNULL \\ &&|& \hex{FB}~~0{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \STRUCTNEW~x \\ &&|& \hex{FB}~~1{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \STRUCTNEWDEFAULT~x \\ &&|& - \hex{FB}~~2{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTGET~x~i \\ &&|& - \hex{FB}~~3{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTGETS~x~i \\ &&|& - \hex{FB}~~4{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTGETU~x~i \\ &&|& - \hex{FB}~~5{:}\Bu32~~x{:}\Btypeidx~~i{:}\Bu32 &\Rightarrow& \STRUCTSET~x~i \\ &&|& + \hex{FB}~~2{:}\Bu32~~x{:}\Btypeidx~~y{:}\Bfieldidx &\Rightarrow& \STRUCTGET~x~y \\ &&|& + \hex{FB}~~3{:}\Bu32~~x{:}\Btypeidx~~y{:}\Bfieldidx &\Rightarrow& \STRUCTGETS~x~y \\ &&|& + \hex{FB}~~4{:}\Bu32~~x{:}\Btypeidx~~y{:}\Bfieldidx &\Rightarrow& \STRUCTGETU~x~y \\ &&|& + \hex{FB}~~5{:}\Bu32~~x{:}\Btypeidx~~y{:}\Bfieldidx &\Rightarrow& \STRUCTSET~x~y \\ &&|& \hex{FB}~~6{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYNEW~x \\ &&|& \hex{FB}~~7{:}\Bu32~~x{:}\Btypeidx &\Rightarrow& \ARRAYNEWDEFAULT~x \\ &&|& \hex{FB}~~8{:}\Bu32~~x{:}\Btypeidx~~n{:}\Bu32 &\Rightarrow& \ARRAYNEWFIXED~x~n \\ &&|& diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst index ef924249b..0361e4e9e 100644 --- a/document/core/binary/modules.rst +++ b/document/core/binary/modules.rst @@ -9,7 +9,7 @@ except that :ref:`function definitions ` are split into two section This separation enables *parallel* and *streaming* compilation of the functions in a module. -.. index:: index, type index, function index, table index, memory index, global index, element index, data index, local index, label index +.. index:: index, type index, function index, table index, memory index, global index, element index, data index, local index, label index, field index pair: binary format; type index pair: binary format; function index pair: binary format; table index @@ -19,6 +19,7 @@ except that :ref:`function definitions ` are split into two section pair: binary format; data index pair: binary format; local index pair: binary format; label index + pair: binary format; field index .. _binary-typeidx: .. _binary-funcidx: .. _binary-tableidx: @@ -28,6 +29,7 @@ except that :ref:`function definitions ` are split into two section .. _binary-dataidx: .. _binary-localidx: .. _binary-labelidx: +.. _binary-fieldidx: .. _binary-index: Indices @@ -46,6 +48,7 @@ All :ref:`indices ` are encoded with their respective value. \production{data index} & \Bdataidx &::=& x{:}\Bu32 &\Rightarrow& x \\ \production{local index} & \Blocalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ \production{label index} & \Blabelidx &::=& l{:}\Bu32 &\Rightarrow& l \\ + \production{field index} & \Bfieldidx &::=& x{:}\Bu32 &\Rightarrow& x \\ \end{array} diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index a3e4d7691..2ce0123b6 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -521,7 +521,7 @@ Reference Instructions .. _exec-struct.get: .. _exec-struct.get_sx: -:math:`\STRUCTGET\K{\_}\sx^?~x~i` +:math:`\STRUCTGET\K{\_}\sx^?~x~y` ................................. .. todo:: unroll type @@ -530,11 +530,11 @@ Reference Instructions 2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -3. Assert: due to :ref:`validation `, :math:`\deftype` is a :ref:`structure type ` with at least :math:`i + 1` fields. +3. Assert: due to :ref:`validation `, :math:`\deftype` is a :ref:`structure type ` with at least :math:`y + 1` fields. 4. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`structure type ` :math:`\deftype`. (todo: unroll) -5. Let :math:`\X{ft}_i` be the :math:`i`-th :ref:`field type ` of :math:`\X{ft}^\ast`. +5. Let :math:`\X{ft}_y` be the :math:`y`-th :ref:`field type ` of :math:`\X{ft}^\ast`. 6. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. @@ -548,29 +548,29 @@ Reference Instructions 10. Let :math:`\REFSTRUCTADDR~a` be the reference value :math:`\reff`. -11. Assert: due to :ref:`validation `, the :ref:`structure instance ` :math:`S.\SSTRUCTS[a]` exists and has at least :math:`i + 1` fields. +11. Assert: due to :ref:`validation `, the :ref:`structure instance ` :math:`S.\SSTRUCTS[a]` exists and has at least :math:`y + 1` fields. -12. Let :math:`\fieldval` be the :ref:`field value ` :math:`S.\SSTRUCTS[a].\SIFIELDS[i]`. +12. Let :math:`\fieldval` be the :ref:`field value ` :math:`S.\SSTRUCTS[a].\SIFIELDS[y]`. -13. Let :math:`\val` be the result of computing :math:`\unpackval^{\sx^?}_{\X{ft}_i}(\fieldval))`. +13. Let :math:`\val` be the result of computing :math:`\unpackval^{\sx^?}_{\X{ft}_y}(\fieldval))`. 14. Push the value :math:`\val` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} - S; F; (\REFSTRUCTADDR~a)~(\STRUCTGET\K{\_}\sx^?~x~i) &\stepto& \val + S; F; (\REFSTRUCTADDR~a)~(\STRUCTGET\K{\_}\sx^?~x~y) &\stepto& \val & \begin{array}[t]{@{}r@{~}l@{}} (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ - \land & \val = \unpackval^{\sx^?}_{\X{ft}^n[i]}(S.\SSTRUCTS[a].\SIFIELDS[i])) + \land & \val = \unpackval^{\sx^?}_{\X{ft}^n[y]}(S.\SSTRUCTS[a].\SIFIELDS[y])) \end{array} \\ - S; F; (\REFNULL~t)~(\STRUCTGET\K{\_}\sx^?~x~i) &\stepto& \TRAP + S; F; (\REFNULL~t)~(\STRUCTGET\K{\_}\sx^?~x~y) &\stepto& \TRAP \end{array} .. _exec-struct.set: -:math:`\STRUCTSET~x~i` +:math:`\STRUCTSET~x~y` ...................... .. todo:: unroll type @@ -579,11 +579,11 @@ Reference Instructions 2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -3. Assert: due to :ref:`validation `, :math:`\deftype` is a :ref:`structure type ` with at least :math:`i + 1` fields. +3. Assert: due to :ref:`validation `, :math:`\deftype` is a :ref:`structure type ` with at least :math:`y + 1` fields. 4. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`structure type ` :math:`\deftype`. (todo: unroll) -5. Let :math:`\X{ft}_i` be the :math:`i`-th :ref:`field type ` of :math:`\X{ft}^\ast`. +5. Let :math:`\X{ft}_y` be the :math:`y`-th :ref:`field type ` of :math:`\X{ft}^\ast`. 6. Assert: due to :ref:`validation `, a :ref:`value ` is on the top of the stack. @@ -601,21 +601,21 @@ Reference Instructions 12. Let :math:`\REFSTRUCTADDR~a` be the reference value :math:`\reff`. -13. Assert: due to :ref:`validation `, the :ref:`structure instance ` :math:`S.\SSTRUCTS[a]` exists and has at least :math:`i + 1` fields. +13. Assert: due to :ref:`validation `, the :ref:`structure instance ` :math:`S.\SSTRUCTS[a]` exists and has at least :math:`y + 1` fields. -14. Let :math:`\fieldval` be the result of computing :math:`\packval_{\X{ft}_i}(\val))`. +14. Let :math:`\fieldval` be the result of computing :math:`\packval_{\X{ft}_y}(\val))`. -15. Replace the :ref:`field value ` :math:`S.\SSTRUCTS[a].\SIFIELDS[i]` with :math:`\fieldval`. +15. Replace the :ref:`field value ` :math:`S.\SSTRUCTS[a].\SIFIELDS[y]` with :math:`\fieldval`. .. math:: \begin{array}{lcl@{\qquad}l} - S; F; (\REFSTRUCTADDR~a)~\val~(\STRUCTSET~x~i) &\stepto& S'; \epsilon + S; F; (\REFSTRUCTADDR~a)~\val~(\STRUCTSET~x~y) &\stepto& S'; \epsilon & \begin{array}[t]{@{}r@{~}l@{}} (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ - \land & S' = S \with \SSTRUCTS[a].\SIFIELDS[i] = \packval_{\X{ft}^n[i]}(\val)) + \land & S' = S \with \SSTRUCTS[a].\SIFIELDS[y] = \packval_{\X{ft}^n[y]}(\val)) \end{array} \\ - S; F; (\REFNULL~t)~\val~(\STRUCTSET~x~i) &\stepto& \TRAP + S; F; (\REFNULL~t)~\val~(\STRUCTSET~x~y) &\stepto& \TRAP \end{array} diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 8d4efe959..215d6ffcd 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -503,9 +503,9 @@ Instructions in this group are concerned with creating and accessing :ref:`refer \dots \\&&|& \STRUCTNEW~\typeidx \\&&|& \STRUCTNEWDEFAULT~\typeidx \\&&|& - \STRUCTGET~\typeidx~\u32 \\&&|& - \STRUCTGET\K{\_}\sx~\typeidx~\u32 \\&&|& - \STRUCTSET~\typeidx~\u32 \\&&|& + \STRUCTGET~\typeidx~\fieldidx \\&&|& + \STRUCTGET\K{\_}\sx~\typeidx~\fieldidx \\&&|& + \STRUCTSET~\typeidx~\fieldidx \\&&|& \ARRAYNEW~\typeidx \\&&|& \ARRAYNEWFIXED~\typeidx~\u32 \\&&|& \ARRAYNEWDEFAULT~\typeidx \\&&|& diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst index d8b0f5ae9..ff935ccc2 100644 --- a/document/core/syntax/modules.rst +++ b/document/core/syntax/modules.rst @@ -29,7 +29,7 @@ and provide initialization in the form of :ref:`data ` and :ref:`el Each of the vectors -- and thus the entire module -- may be empty. -.. index:: ! index, ! index space, ! type index, ! function index, ! table index, ! memory index, ! global index, ! local index, ! label index, ! element index, ! data index, function, global, table, memory, element, data, local, parameter, import +.. index:: ! index, ! index space, ! type index, ! function index, ! table index, ! memory index, ! global index, ! local index, ! label index, ! element index, ! data index, ! field index, function, global, table, memory, element, data, local, parameter, import, field pair: abstract syntax; type index pair: abstract syntax; function index pair: abstract syntax; table index @@ -39,6 +39,7 @@ Each of the vectors -- and thus the entire module -- may be empty. pair: abstract syntax; data index pair: abstract syntax; local index pair: abstract syntax; label index + pair: abstract syntax; field index pair: type; index pair: function; index pair: table; index @@ -48,6 +49,7 @@ Each of the vectors -- and thus the entire module -- may be empty. pair: data; index pair: local; index pair: label; index + pair: field; index .. _syntax-typeidx: .. _syntax-funcidx: .. _syntax-tableidx: @@ -57,6 +59,7 @@ Each of the vectors -- and thus the entire module -- may be empty. .. _syntax-dataidx: .. _syntax-localidx: .. _syntax-labelidx: +.. _syntax-fieldidx: .. _syntax-index: Indices @@ -76,6 +79,7 @@ Each class of definition has its own *index space*, as distinguished by the foll \production{data index} & \dataidx &::=& \u32 \\ \production{local index} & \localidx &::=& \u32 \\ \production{label index} & \labelidx &::=& \u32 \\ + \production{field index} & \fieldidx &::=& \u32 \\ \end{array} The index space for :ref:`functions `, :ref:`tables `, :ref:`memories ` and :ref:`globals ` includes respective :ref:`imports ` declared in the same module. @@ -87,6 +91,8 @@ The index space for :ref:`locals ` is only accessible inside a :re Label indices reference :ref:`structured control instructions ` inside an instruction sequence. +Each :ref:`aggregate type ` provides an index space for its :ref:`fields `. + .. _free-typeidx: .. _free-funcidx: @@ -97,6 +103,7 @@ Label indices reference :ref:`structured control instructions ` :math:`C.\CTYPES[x]` must exist. * The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be a :ref:`structure type ` :math:`\TSTRUCT~\fieldtype^\ast`. -* Let the :ref:`field type ` :math:`\mut~\storagetype` be :math:`\fieldtype^\ast[i]`. +* Let the :ref:`field type ` :math:`\mut~\storagetype` be :math:`\fieldtype^\ast[y]`. * Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\storagetype)`. @@ -366,23 +366,23 @@ Aggregate Reference Instructions \frac{ \expanddt(C.\CTYPES[x]) = \TSTRUCT~\X{ft}^\ast \qquad - \X{ft}^\ast[i] = \mut~\X{st} + \X{ft}^\ast[y] = \mut~\X{st} \qquad \sx = \epsilon \Leftrightarrow \X{st} = \unpacktype(\X{st}) }{ - C \vdashinstr \STRUCTGET\K{\_}\sx^?~x~i : [(\REF~\NULL~x)] \to [\unpacktype(\X{st})] + C \vdashinstr \STRUCTGET\K{\_}\sx^?~x~y : [(\REF~\NULL~x)] \to [\unpacktype(\X{st})] } .. _valid-struct.set: -:math:`\STRUCTSET~x~i` +:math:`\STRUCTSET~x~y` ...................... * The :ref:`defined type ` :math:`C.\CTYPES[x]` must exist. * The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be a :ref:`structure type ` :math:`\TSTRUCT~\fieldtype^\ast`. -* Let the :ref:`field type ` :math:`\mut~\storagetype` be :math:`\fieldtype^\ast[i]`. +* Let the :ref:`field type ` :math:`\mut~\storagetype` be :math:`\fieldtype^\ast[y]`. * The prefix :math:`\mut` must be :math:`\MVAR`. @@ -394,9 +394,9 @@ Aggregate Reference Instructions \frac{ \expanddt(C.\CTYPES[x]) = \TSTRUCT~\X{ft}^\ast \qquad - \X{ft}^\ast[i] = \MVAR~\X{st} + \X{ft}^\ast[y] = \MVAR~\X{st} }{ - C \vdashinstr \STRUCTSET~x~i : [(\REF~\NULL~x)~\unpacktype(\X{st})] \to [] + C \vdashinstr \STRUCTSET~x~y : [(\REF~\NULL~x)~\unpacktype(\X{st})] \to [] } From 8e3581d5142eaf4aaec6e551dd28cfdb11d11065 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Fri, 8 Sep 2023 16:38:49 -0700 Subject: [PATCH 11/20] getfield meta function --- document/core/exec/instructions.rst | 76 ++++++++++++--------------- document/core/syntax/instructions.rst | 9 ++++ document/core/util/macros.def | 5 ++ 3 files changed, 47 insertions(+), 43 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 3d6e0770a..c7e492ec7 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1120,75 +1120,67 @@ Reference Instructions :math:`\ARRAYCOPY~x~y` ...................... -1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]` exists. +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]` exists. 2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]`. -3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. - -4. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. - -5. If :math:`\X{ft} = \mut~\packedtype`, then: +3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. - a. Let :math:`\X{get}` be the instruction :math:`\ARRAYGETU~y`. +4. Let :math:`\TARRAY~\mut~\X{st}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. -6. Else: +5. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. - a. Let :math:`\X{get}` be the instruction :math:`\ARRAYGET~y`. +6. Pop the value :math:`n` from the stack. 7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -8. Pop the value :math:`n` from the stack. - -9. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +8. Pop the value :math:`s` from the stack. -10. Pop the value :math:`s` from the stack. +9. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~y)` is on the top of the stack. -11. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~y)` is on the top of the stack. +10. Pop the value :math:`\reff_2` from the stack. -12. Pop the value :math:`\reff_2` from the stack. +11. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -13. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. +12. Pop the value :math:`d` from the stack. -14. Pop the value :math:`d` from the stack. +13. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. -15. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. +14. Pop the value :math:`\reff_1` from the stack. -16. Pop the value :math:`\reff_1` from the stack. - -17. If :math:`\reff_1` is :math:`\REFNULL~t`, then: +15. If :math:`\reff_1` is :math:`\REFNULL~t`, then: a. Trap. -18. Assert: due to :ref:`validation `, :math:`\reff_1` is an :ref:`array reference `. +16. Assert: due to :ref:`validation `, :math:`\reff_1` is an :ref:`array reference `. -19. Let :math:`\REFARRAYADDR~a_1` be the reference value :math:`\reff_1`. +17. Let :math:`\REFARRAYADDR~a_1` be the reference value :math:`\reff_1`. -20. If :math:`\reff_2` is :math:`\REFNULL~t`, then: +18. If :math:`\reff_2` is :math:`\REFNULL~t`, then: a. Trap. -21. Assert: due to :ref:`validation `, :math:`\reff_2` is an :ref:`array reference `. +19. Assert: due to :ref:`validation `, :math:`\reff_2` is an :ref:`array reference `. -22. Let :math:`\REFARRAYADDR~a_2` be the reference value :math:`\reff_2`. +20. Let :math:`\REFARRAYADDR~a_2` be the reference value :math:`\reff_2`. -23. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_1]` exists. +21. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_1]` exists. -24. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_2]` exists. +22. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_2]` exists. -25. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then: +23. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then: a. Trap. -26. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then: +24. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then: a. Trap. -27. If :math:`n = 0`, then: +25. If :math:`n = 0`, then: a. Return. -28. If :math:`d \leq s`, then: +26. If :math:`d \leq s`, then: a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. @@ -1198,7 +1190,7 @@ Reference Instructions d. Push the value :math:`\I32.\CONST~s` to the stack. - e. Execute :math:`\X{get}`. + e. Execute :math:`\getfield(\X{st})`. f. Execute the instruction :math:`\ARRAYSET~x`. @@ -1214,7 +1206,7 @@ Reference Instructions l. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -29. Else: +27. Else: a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. @@ -1228,7 +1220,7 @@ Reference Instructions f. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack. - g. Execute :math:`\X{get}`. + g. Execute :math:`\getfield(\X{st})`. h. Execute the instruction :math:`\ARRAYSET~x`. @@ -1240,9 +1232,9 @@ Reference Instructions l. Push the value :math:`\I32.\CONST~s` to the stack. -30. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +28. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -31. Execute the instruction :math:`\ARRAYCOPY~x~y`. +29. Execute the instruction :math:`\ARRAYCOPY~x~y`. .. math:: ~\\[-1ex] @@ -1262,15 +1254,14 @@ Reference Instructions \\ \quad S; \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~\X{get} \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~\getfield(\X{st}) \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d+1)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\otherwise, \iff & d \leq s \\ - \land & (\X{get} = \ARRAYGET~y \vee \X{get} = \ARRAYGETU~y) \\ - \land & (F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\packedtype \Longleftrightarrow \X{get} = \ARRAYGETU~y)) + \land & F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\X{st}) \end{array} \\[1ex] S; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYCOPY~x~y) @@ -1278,15 +1269,14 @@ Reference Instructions \\ \quad S; \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d+n) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~\X{get} \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~\getfield(\X{st}) \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\otherwise, \iff & d > s \\ - \land & (\X{get} = \ARRAYGET~y \vee \X{get} = \ARRAYGETU~y) \\ - \land & (F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\packedtype \Longleftrightarrow \X{get} = \ARRAYGETU~y)) + \land & F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\X{st}) \end{array} \\[1ex] S; (\REFNULL~t)~(\I32.\CONST~d)~\val~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \quad\stepto\quad \TRAP diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 8d4efe959..e6ff0221e 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -541,6 +541,15 @@ The instructions |I31NEW| and :math:`\I31GET\K{\_}\sx` convert between type |I31 The instructions |EXTERNINTERNALIZE| and |EXTERNEXTERNALIZE| allow lossless conversion between references represented as type :math:`(\REF~\NULL~\EXTERN)`| and as :math:`(\REF~\NULL~\ANY)`. +The following auxiliary function produces an instruction that accesses an array slot for a given :ref:`storage type `. + +.. _aux-getfield: + +.. math:: + \begin{array}{lll} + \getfield(\valtype) &=& \ARRAYGET \\ + \getfield(\packedtype) &=& \ARRAYGETU \\ + \end{array} .. index:: ! parametric instruction, value type pair: abstract syntax; instruction diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 1833fdc98..79ef43076 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -656,6 +656,11 @@ .. |expr| mathdef:: \xref{syntax/instructions}{syntax-expr}{\X{expr}} +.. Instructions, meta functions + +.. |getfield| mathdef:: \xref{syntax/instructions}{aux-getfield}{\F{getfield}} + + .. Binary Format .. ------------- From e04ecbdc592bbd2af19bccce7f508d036fe130ac Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Fri, 8 Sep 2023 17:35:15 -0700 Subject: [PATCH 12/20] move auxiliary function --- document/core/exec/instructions.rst | 10 ++++++++++ document/core/syntax/instructions.rst | 10 ---------- document/core/util/macros.def | 2 +- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index c7e492ec7..66ddd4f12 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1284,6 +1284,16 @@ Reference Instructions S; \val~(\I32.\CONST~d)~(\REFNULL~t)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \quad\stepto\quad \TRAP \end{array} +Where: + +.. _aux-getfield: + +.. math:: + \begin{array}{lll} + \getfield(\valtype) &=& \ARRAYGET \\ + \getfield(\packedtype) &=& \ARRAYGETU \\ + \end{array} + .. _exec-array.init_data: diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index e6ff0221e..57fafe27e 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -541,16 +541,6 @@ The instructions |I31NEW| and :math:`\I31GET\K{\_}\sx` convert between type |I31 The instructions |EXTERNINTERNALIZE| and |EXTERNEXTERNALIZE| allow lossless conversion between references represented as type :math:`(\REF~\NULL~\EXTERN)`| and as :math:`(\REF~\NULL~\ANY)`. -The following auxiliary function produces an instruction that accesses an array slot for a given :ref:`storage type `. - -.. _aux-getfield: - -.. math:: - \begin{array}{lll} - \getfield(\valtype) &=& \ARRAYGET \\ - \getfield(\packedtype) &=& \ARRAYGETU \\ - \end{array} - .. index:: ! parametric instruction, value type pair: abstract syntax; instruction .. _syntax-instr-parametric: diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 79ef43076..78ded3620 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -658,7 +658,7 @@ .. Instructions, meta functions -.. |getfield| mathdef:: \xref{syntax/instructions}{aux-getfield}{\F{getfield}} +.. |getfield| mathdef:: \xref{exec/instructions}{aux-getfield}{\F{getfield}} From 31444ad90c38008a377b2e4c4db55b446d7d1c27 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Fri, 8 Sep 2023 17:42:48 -0700 Subject: [PATCH 13/20] pop i32.const fixes --- document/core/exec/instructions.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 66ddd4f12..b75b38e97 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1130,11 +1130,11 @@ Reference Instructions 5. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -6. Pop the value :math:`n` from the stack. +6. Pop the value :math:`\I32.\CONST~n` from the stack. 7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -8. Pop the value :math:`s` from the stack. +8. Pop the value :math:`\I32.\CONST~s` from the stack. 9. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~y)` is on the top of the stack. @@ -1142,7 +1142,7 @@ Reference Instructions 11. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -12. Pop the value :math:`d` from the stack. +12. Pop the value :math:`\I32.\CONST~d` from the stack. 13. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. From aa173f6ca4d0b9c35871200ac0edbafd6d09d705 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Fri, 8 Sep 2023 17:47:09 -0700 Subject: [PATCH 14/20] format conditions on single line --- document/core/exec/instructions.rst | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index b75b38e97..82be56270 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1259,10 +1259,7 @@ Reference Instructions (\REFARRAYADDR~a_1)~(\I32.\CONST~d+1)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad - \begin{array}[t]{@{}r@{~}l@{}} - (\otherwise, \iff & d \leq s \\ - \land & F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\X{st}) - \end{array} + (\otherwise, \iff d \leq s \land F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\X{st}) \\ \\[1ex] S; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYCOPY~x~y) \quad\stepto @@ -1274,10 +1271,7 @@ Reference Instructions (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} \\ \qquad - \begin{array}[t]{@{}r@{~}l@{}} - (\otherwise, \iff & d > s \\ - \land & F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\X{st}) - \end{array} + (\otherwise, \iff d > s \land F.\AMODULE.\MITYPES[x] = \TARRAY~\mut~\X{st}) \\ \\[1ex] S; (\REFNULL~t)~(\I32.\CONST~d)~\val~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \quad\stepto\quad \TRAP \\[1ex] From b5f57596a75079f4f9527e8fff85f62303207e2d Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sat, 9 Sep 2023 10:10:08 -0700 Subject: [PATCH 15/20] Relax validation of global order --- document/core/util/macros.def | 1 + document/core/valid/modules.rst | 80 +++++++++++++++++++++---------- test/core/global.wast | 83 ++++++++++++++++++++++++++++----- 3 files changed, 128 insertions(+), 36 deletions(-) diff --git a/document/core/util/macros.def b/document/core/util/macros.def index b027b9033..85ce64e0d 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -1120,6 +1120,7 @@ .. |vdashtable| mathdef:: \xref{valid/modules}{valid-table}{\vdash} .. |vdashmem| mathdef:: \xref{valid/modules}{valid-mem}{\vdash} .. |vdashglobal| mathdef:: \xref{valid/modules}{valid-global}{\vdash} +.. |vdashglobalseq| mathdef:: \xref{valid/modules}{valid-globalseq}{\vdash} .. |vdashelem| mathdef:: \xref{valid/modules}{valid-elem}{\vdash} .. |vdashelemmode| mathdef:: \xref{valid/modules}{valid-elemmode}{\vdash} .. |vdashdata| mathdef:: \xref{valid/modules}{valid-data}{\vdash} diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 89d1c54d3..d8fd6c45e 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -221,12 +221,15 @@ Memories :math:`\mem` are classified by :ref:`memory types `. pair: validation; global single: abstract syntax; global .. _valid-global: +.. _valid-globalseq: Globals ~~~~~~~ Globals :math:`\global` are classified by :ref:`global types ` of the form :math:`\mut~t`. +Sequences of globals are handled incrementally, such that each definition has access to previous definitions. + :math:`\{ \GTYPE~\mut~t, \GINIT~\expr \}` ......................................... @@ -251,6 +254,38 @@ Globals :math:`\global` are classified by :ref:`global types } +:math:`\global^\ast` +.................... + +* If the sequence is empty, then it is valid with the empty sequence of :ref:`global types `. + +* Else: + + * The first global definition must be :ref:`valid ` with some type :ref:`global type ` :math:`\X{gt}_1`. + + * Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`global type ` :math:`\X{gt}_1` apppended to the |CGLOBALS| vector. + + * Under context :math:`C'`, the remainder of the sequence must be valid with some sequence :math:`\X{gt}^\ast` of :ref:`global types `. + + * Then the sequence is valid with the sequence of :ref:`global types ` consisting of :math:`\X{gt}_1` prepended to :math:`\X{gt}^\ast`. + +.. math:: + ~\\ + \frac{ + }{ + C \vdashglobalseq \epsilon : \epsilon + } + \qquad + \frac{ + C \vdashglobal \global_1 : \X{gt}_1 + \qquad + C, \CGLOBALS~\X{gt}_1 \vdashglobalseq \global^\ast : \X{gt}^\ast + }{ + C \vdashglobalseq \global_1~\global^\ast : \X{gt}_1~\X{gt}^\ast + } + + + .. index:: element, table, table index, expression, constant, function index pair: validation; element single: abstract syntax; element @@ -684,20 +719,6 @@ The :ref:`external types ` classifying a module may contain f * all other fields are empty. -* Under the context :math:`C`: - - * For each :math:`\func_i` in :math:`\module.\MFUNCS`, - the definition :math:`\func_i` must be :ref:`valid ` with a :ref:`function type ` :math:`\X{ft}_i`. - - * If :math:`\module.\MSTART` is non-empty, - then :math:`\module.\MSTART` must be :ref:`valid `. - - * For each :math:`\import_i` in :math:`\module.\MIMPORTS`, - the segment :math:`\import_i` must be :ref:`valid ` with an :ref:`external type ` :math:`\X{it}_i`. - - * For each :math:`\export_i` in :math:`\module.\MEXPORTS`, - the segment :math:`\export_i` must be :ref:`valid ` with :ref:`external type ` :math:`\X{et}_i`. - * Under the context :math:`C'`: * For each :math:`\table_i` in :math:`\module.\MTABLES`, @@ -706,8 +727,12 @@ The :ref:`external types ` classifying a module may contain f * For each :math:`\mem_i` in :math:`\module.\MMEMS`, the definition :math:`\mem_i` must be :ref:`valid ` with a :ref:`memory type ` :math:`\X{mt}_i`. - * For each :math:`\global_i` in :math:`\module.\MGLOBALS`, - the definition :math:`\global_i` must be :ref:`valid ` with a :ref:`global type ` :math:`\X{gt}_i`. + * The sequence :math:`\module.\MGLOBALS` of :ref:`globals ` must be :ref:`valid ` with a sequence :math:`\X{gt}^\ast` of :ref:`global types `. + +* Under the context :math:`C`: + + * For each :math:`\func_i` in :math:`\module.\MFUNCS`, + the definition :math:`\func_i` must be :ref:`valid ` with a :ref:`function type ` :math:`\X{ft}_i`. * For each :math:`\elem_i` in :math:`\module.\MELEMS`, the segment :math:`\elem_i` must be :ref:`valid ` with :ref:`reference type ` :math:`\X{rt}_i`. @@ -715,6 +740,15 @@ The :ref:`external types ` classifying a module may contain f * For each :math:`\data_i` in :math:`\module.\MDATAS`, the segment :math:`\data_i` must be :ref:`valid `. + * If :math:`\module.\MSTART` is non-empty, + then :math:`\module.\MSTART` must be :ref:`valid `. + + * For each :math:`\import_i` in :math:`\module.\MIMPORTS`, + the segment :math:`\import_i` must be :ref:`valid ` with an :ref:`external type ` :math:`\X{it}_i`. + + * For each :math:`\export_i` in :math:`\module.\MEXPORTS`, + the segment :math:`\export_i` must be :ref:`valid ` with :ref:`external type ` :math:`\X{et}_i`. + * The length of :math:`C.\CMEMS` must not be larger than :math:`1`. * All export names :math:`\export_i.\ENAME` must be different. @@ -725,8 +759,6 @@ The :ref:`external types ` classifying a module may contain f * Let :math:`\X{mt}^\ast` be the concatenation of the internal :ref:`memory types ` :math:`\X{mt}_i`, in index order. -* Let :math:`\X{gt}^\ast` be the concatenation of the internal :ref:`global types ` :math:`\X{gt}_i`, in index order. - * Let :math:`\X{rt}^\ast` be the concatenation of the :ref:`reference types ` :math:`\X{rt}_i`, in index order. * Let :math:`\X{it}^\ast` be the concatenation of :ref:`external types ` :math:`\X{it}_i` of the imports, in index order. @@ -740,17 +772,17 @@ The :ref:`external types ` classifying a module may contain f \begin{array}{@{}c@{}} C_0 \vdashtypes \type^\ast \ok \quad - (C \vdashfunc \func : \X{ft})^\ast - \quad (C' \vdashtable \table : \X{tt})^\ast \quad (C' \vdashmem \mem : \X{mt})^\ast \quad - (C' \vdashglobal \global : \X{gt})^\ast + C' \vdashglobalseq \global^\ast : \X{gt}^\ast \\ - (C' \vdashelem \elem : \X{rt})^\ast + (C \vdashfunc \func : \X{ft})^\ast + \quad + (C \vdashelem \elem : \X{rt})^\ast \quad - (C' \vdashdata \data \ok)^n + (C \vdashdata \data \ok)^n \quad (C \vdashstart \start \ok)^? \quad @@ -802,7 +834,7 @@ The :ref:`external types ` classifying a module may contain f However, this recursion is just a specification device. All types needed to construct :math:`C` can easily be determined from a simple pre-pass over the module that does not perform any actual validation. - Globals, however, are not recursive and not accessible within :ref:`constant expressions ` when they are defined locally. + Globals, however, are not recursive but eveluated sequentially, such that each :ref:`constant expressions ` only has access to imported or priviously defined globals. The effect of defining the limited context :math:`C'` for validating certain definitions is that they can only access functions and imported globals and nothing else. .. note:: diff --git a/test/core/global.wast b/test/core/global.wast index 0816b6a3b..3ec4cb727 100644 --- a/test/core/global.wast +++ b/test/core/global.wast @@ -611,17 +611,76 @@ "type mismatch" ) + +;; Definition order + +(module + (global (export "g") i32 (i32.const 4)) +) +(register "G") + +(module + (global $g0 (import "G" "g") i32) + (global $g1 i32 (i32.const 8)) + (global $g2 i32 (global.get $g0)) + (global $g3 i32 (global.get $g1)) + + (global $gn funcref (ref.null func)) + (global $gf funcref (ref.func $f)) + (func $f) + + (table $t 10 funcref (global.get $gn)) + (elem (table $t) (global.get $g2) funcref (ref.func $f)) + (elem (table $t) (global.get $g3) funcref (global.get $gf)) + + (memory $m 1) + (data (global.get $g2) "\44\44\44\44") + (data (global.get $g3) "\88\88\88\88") + + (func (export "get-elem") (param $i i32) (result funcref) + (table.get $t (local.get $i)) + ) + (func (export "get-data") (param $i i32) (result i32) + (i32.load (local.get $i)) + ) +) + +(assert_return (invoke "get-elem" (i32.const 0)) (ref.null)) +(assert_return (invoke "get-elem" (i32.const 4)) (ref.func)) +(assert_return (invoke "get-elem" (i32.const 8)) (ref.func)) + +(assert_return (invoke "get-data" (i32.const 4)) (i32.const 0x44444444)) +(assert_return (invoke "get-data" (i32.const 8)) (i32.const 0x88888888)) + +(assert_invalid + (module + (global $g1 i32 (global.get $g2)) + (global $g2 i32 (i32.const 0)) + ) + "unknown global" +) + + ;; Duplicate identifier errors -(assert_malformed (module quote - "(global $foo i32 (i32.const 0))" - "(global $foo i32 (i32.const 0))") - "duplicate global") -(assert_malformed (module quote - "(import \"\" \"\" (global $foo i32))" - "(global $foo i32 (i32.const 0))") - "duplicate global") -(assert_malformed (module quote - "(import \"\" \"\" (global $foo i32))" - "(import \"\" \"\" (global $foo i32))") - "duplicate global") +(assert_malformed + (module quote + "(global $foo i32 (i32.const 0))" + "(global $foo i32 (i32.const 0))" + ) + "duplicate global" +) +(assert_malformed + (module quote + "(import \"\" \"\" (global $foo i32))" + "(global $foo i32 (i32.const 0))" + ) + "duplicate global" +) +(assert_malformed + (module quote + "(import \"\" \"\" (global $foo i32))" + "(import \"\" \"\" (global $foo i32))" + ) + "duplicate global" +) From 654e02b7b94d43c04c8b27899a4f731439b02a40 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sat, 9 Sep 2023 10:20:53 -0700 Subject: [PATCH 16/20] Cleanup --- document/core/exec/modules.rst | 5 +---- document/core/valid/modules.rst | 30 ++++++++++++++---------------- 2 files changed, 15 insertions(+), 20 deletions(-) diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index fd7a3dddb..792888954 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -291,7 +291,6 @@ Growing :ref:`memories ` .................................. .. todo:: update prose for types -.. todo:: change semantics for globals The allocation function for :ref:`modules ` requires a suitable list of :ref:`external values ` that are assumed to :ref:`match ` the :ref:`import ` vector of the module, a list of initialization :ref:`values ` for the module's :ref:`globals `, @@ -461,8 +460,6 @@ For types, however, allocation is defined in terms of :ref:`rolling ` and the :ref:`evaluation ` of :ref:`global ` and :ref:`table ` initializers as well as :ref:`element segments ` are mutually recursive because the global initialization :ref:`values ` :math:`\val_{\F{g}}^\ast`, :math:`\reff_{\F{t}}`, and element segment contents :math:`(\reff^\ast)^\ast` are passed to the module allocator while depending on the module instance :math:`\moduleinst` and store :math:`S'` returned by allocation. Again, this recursion is just a specification device. - In practice, the initialization values can :ref:`be determined ` beforehand by staging module allocation further such that first, the module's own :math:`function instances ` are pre-allocated in the store, then the initializer expressions are evaluated, then the rest of the module instance is allocated, and finally the new function instances' :math:`\AMODULE` fields are set to that module instance. + In practice, the initialization values can :ref:`be determined ` beforehand by staging module allocation further such that first, the module's own :ref:`function instances ` are pre-allocated in the store, then the initializer expressions are evaluated in order, allocating globals on the way, then the rest of the module instance is allocated, and finally the new function instances' :math:`\AMODULE` fields are set to that module instance. This is possible because :ref:`validation ` ensures that initialization expressions cannot actually call a function, only take their reference. All failure conditions are checked before any observable mutation of the store takes place. diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index d8fd6c45e..6b9bf4c88 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -719,7 +719,10 @@ The :ref:`external types ` classifying a module may contain f * all other fields are empty. -* Under the context :math:`C'`: +* Under the context :math:`C'`, + the sequence :math:`\module.\MGLOBALS` of :ref:`globals ` must be :ref:`valid ` with a sequence :math:`\X{gt}^\ast` of :ref:`global types `. + +* Under the context :math:`C`: * For each :math:`\table_i` in :math:`\module.\MTABLES`, the definition :math:`\table_i` must be :ref:`valid ` with a :ref:`table type ` :math:`\X{tt}_i`. @@ -727,10 +730,6 @@ The :ref:`external types ` classifying a module may contain f * For each :math:`\mem_i` in :math:`\module.\MMEMS`, the definition :math:`\mem_i` must be :ref:`valid ` with a :ref:`memory type ` :math:`\X{mt}_i`. - * The sequence :math:`\module.\MGLOBALS` of :ref:`globals ` must be :ref:`valid ` with a sequence :math:`\X{gt}^\ast` of :ref:`global types `. - -* Under the context :math:`C`: - * For each :math:`\func_i` in :math:`\module.\MFUNCS`, the definition :math:`\func_i` must be :ref:`valid ` with a :ref:`function type ` :math:`\X{ft}_i`. @@ -749,10 +748,6 @@ The :ref:`external types ` classifying a module may contain f * For each :math:`\export_i` in :math:`\module.\MEXPORTS`, the segment :math:`\export_i` must be :ref:`valid ` with :ref:`external type ` :math:`\X{et}_i`. -* The length of :math:`C.\CMEMS` must not be larger than :math:`1`. - -* All export names :math:`\export_i.\ENAME` must be different. - * Let :math:`\X{ft}^\ast` be the concatenation of the internal :ref:`function types ` :math:`\X{ft}_i`, in index order. * Let :math:`\X{tt}^\ast` be the concatenation of the internal :ref:`table types ` :math:`\X{tt}_i`, in index order. @@ -765,6 +760,10 @@ The :ref:`external types ` classifying a module may contain f * Let :math:`\X{et}^\ast` be the concatenation of :ref:`external types ` :math:`\X{et}_i` of the exports, in index order. +* The length of :math:`C.\CMEMS` must not be larger than :math:`1`. + +* All export names :math:`\export_i.\ENAME` must be different. + * Then the module is valid with :ref:`external types ` :math:`\X{it}^\ast \to \X{et}^\ast`. .. math:: @@ -772,14 +771,14 @@ The :ref:`external types ` classifying a module may contain f \begin{array}{@{}c@{}} C_0 \vdashtypes \type^\ast \ok \quad - (C' \vdashtable \table : \X{tt})^\ast + C' \vdashglobalseq \global^\ast : \X{gt}^\ast + \quad + (C \vdashtable \table : \X{tt})^\ast \quad - (C' \vdashmem \mem : \X{mt})^\ast + (C \vdashmem \mem : \X{mt})^\ast \quad - C' \vdashglobalseq \global^\ast : \X{gt}^\ast - \\ (C \vdashfunc \func : \X{ft})^\ast - \quad + \\ (C \vdashelem \elem : \X{rt})^\ast \quad (C \vdashdata \data \ok)^n @@ -802,7 +801,7 @@ The :ref:`external types ` classifying a module may contain f \\ C = \{ \CTYPES~C_0.\CTYPES, \CFUNCS~\X{ift}^\ast\,\X{ft}^\ast, \CTABLES~\X{itt}^\ast\,\X{tt}^\ast, \CMEMS~\X{imt}^\ast\,\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast\,\X{gt}^\ast, \CELEMS~\X{rt}^\ast, \CDATAS~{\ok}^n, \CREFS~x^\ast \} \\ - C' = \{ \CTYPES~\type^\ast, \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \} + C' = \{ \CTYPES~C_0.\CTYPES, \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \} \qquad |C.\CMEMS| \leq 1 \qquad @@ -835,7 +834,6 @@ The :ref:`external types ` classifying a module may contain f All types needed to construct :math:`C` can easily be determined from a simple pre-pass over the module that does not perform any actual validation. Globals, however, are not recursive but eveluated sequentially, such that each :ref:`constant expressions ` only has access to imported or priviously defined globals. - The effect of defining the limited context :math:`C'` for validating certain definitions is that they can only access functions and imported globals and nothing else. .. note:: The restriction on the number of memories may be lifted in future versions of WebAssembly. From 1a2de44b9ec095fb622c0f29e58473f9b9fb6455 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Sat, 9 Sep 2023 11:41:08 -0700 Subject: [PATCH 17/20] [test] Add tests for packed struct fields --- test/core/gc/struct.wast | 73 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 73 insertions(+) diff --git a/test/core/gc/struct.wast b/test/core/gc/struct.wast index 971ad2ccf..7a3ce4fc8 100644 --- a/test/core/gc/struct.wast +++ b/test/core/gc/struct.wast @@ -154,3 +154,76 @@ (assert_trap (invoke "struct.get-null") "null structure") (assert_trap (invoke "struct.set-null") "null structure") + +;; Packed field instructions + +(module + (type $s (struct (field i8) (field (mut i8)) (field i16) (field (mut i16)))) + + (global (export "g0") (ref $s) (struct.new $s (i32.const 0) (i32.const 1) (i32.const 2) (i32.const 3))) + (global (export "g1") (ref $s) (struct.new $s (i32.const 254) (i32.const 255) (i32.const 65534) (i32.const 65535))) + + (func (export "get_packed_g0_0") (result i32 i32) + (struct.get_s 0 0 (global.get 0)) + (struct.get_u 0 0 (global.get 0)) + ) + + (func (export "get_packed_g1_0") (result i32 i32) + (struct.get_s 0 0 (global.get 1)) + (struct.get_u 0 0 (global.get 1)) + ) + + (func (export "get_packed_g0_1") (result i32 i32) + (struct.get_s 0 1 (global.get 0)) + (struct.get_u 0 1 (global.get 0)) + ) + + (func (export "get_packed_g1_1") (result i32 i32) + (struct.get_s 0 1 (global.get 1)) + (struct.get_u 0 1 (global.get 1)) + ) + + (func (export "get_packed_g0_2") (result i32 i32) + (struct.get_s 0 2 (global.get 0)) + (struct.get_u 0 2 (global.get 0)) + ) + + (func (export "get_packed_g1_2") (result i32 i32) + (struct.get_s 0 2 (global.get 1)) + (struct.get_u 0 2 (global.get 1)) + ) + + (func (export "get_packed_g0_3") (result i32 i32) + (struct.get_s 0 3 (global.get 0)) + (struct.get_u 0 3 (global.get 0)) + ) + + (func (export "get_packed_g1_3") (result i32 i32) + (struct.get_s 0 3 (global.get 1)) + (struct.get_u 0 3 (global.get 1)) + ) + + (func (export "set_get_packed_g0_1") (param i32) (result i32 i32) + (struct.set 0 1 (global.get 0) (local.get 0)) + (struct.get_s 0 1 (global.get 0)) + (struct.get_u 0 1 (global.get 0)) + ) + + (func (export "set_get_packed_g0_3") (param i32) (result i32 i32) + (struct.set 0 3 (global.get 0) (local.get 0)) + (struct.get_s 0 3 (global.get 0)) + (struct.get_u 0 3 (global.get 0)) + ) +) + +(assert_return (invoke "get_packed_g0_0") (i32.const 0) (i32.const 0)) +(assert_return (invoke "get_packed_g1_0") (i32.const -2) (i32.const 254)) +(assert_return (invoke "get_packed_g0_1") (i32.const 1) (i32.const 1)) +(assert_return (invoke "get_packed_g1_1") (i32.const -1) (i32.const 255)) +(assert_return (invoke "get_packed_g0_2") (i32.const 2) (i32.const 2)) +(assert_return (invoke "get_packed_g1_2") (i32.const -2) (i32.const 65534)) +(assert_return (invoke "get_packed_g0_3") (i32.const 3) (i32.const 3)) +(assert_return (invoke "get_packed_g1_3") (i32.const -1) (i32.const 65535)) + +(assert_return (invoke "set_get_packed_g0_1" (i32.const 257)) (i32.const 1) (i32.const 1)) +(assert_return (invoke "set_get_packed_g0_3" (i32.const 257)) (i32.const 257) (i32.const 257)) From 9c1b8f65a9d8a579516229e6c4dd5dcfcc903160 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sat, 9 Sep 2023 15:14:21 -0700 Subject: [PATCH 18/20] Comments --- document/core/valid/modules.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 6b9bf4c88..d982ca34e 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -279,7 +279,7 @@ Sequences of globals are handled incrementally, such that each definition has ac \frac{ C \vdashglobal \global_1 : \X{gt}_1 \qquad - C, \CGLOBALS~\X{gt}_1 \vdashglobalseq \global^\ast : \X{gt}^\ast + C \compose \{\CGLOBALS~\X{gt}_1\} \vdashglobalseq \global^\ast : \X{gt}^\ast }{ C \vdashglobalseq \global_1~\global^\ast : \X{gt}_1~\X{gt}^\ast } @@ -833,7 +833,7 @@ The :ref:`external types ` classifying a module may contain f However, this recursion is just a specification device. All types needed to construct :math:`C` can easily be determined from a simple pre-pass over the module that does not perform any actual validation. - Globals, however, are not recursive but eveluated sequentially, such that each :ref:`constant expressions ` only has access to imported or priviously defined globals. + Globals, however, are not recursive but evaluated sequentially, such that each :ref:`constant expressions ` only has access to imported or previously defined globals. .. note:: The restriction on the number of memories may be lifted in future versions of WebAssembly. From 0f4dba993aadc6401b1dac54f73d7c6f836e7ddd Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sun, 10 Sep 2023 07:27:30 -0700 Subject: [PATCH 19/20] Rename i31.new mnemonic to ref.i31 --- document/core/appendix/changes.rst | 4 ++-- document/core/appendix/index-instructions.py | 2 +- document/core/binary/instructions.rst | 4 ++-- document/core/exec/instructions.rst | 16 ++++++++-------- document/core/exec/runtime.rst | 8 ++++---- document/core/exec/values.rst | 8 ++++---- document/core/syntax/instructions.rst | 6 +++--- document/core/text/instructions.rst | 4 ++-- document/core/util/macros.def | 4 ++-- document/core/valid/instructions.rst | 6 +++--- interpreter/binary/decode.ml | 2 +- interpreter/binary/encode.ml | 2 +- interpreter/exec/eval.ml | 2 +- interpreter/syntax/ast.ml | 2 +- interpreter/syntax/free.ml | 2 +- interpreter/syntax/operators.ml | 2 +- interpreter/text/arrange.ml | 2 +- interpreter/text/lexer.mll | 3 +-- interpreter/text/parser.mly | 4 ++-- interpreter/valid/valid.ml | 4 ++-- proposals/gc/MVP.md | 8 ++++---- proposals/gc/Overview.md | 4 ++-- test/core/gc/br_on_cast.wast | 2 +- test/core/gc/br_on_cast_fail.wast | 2 +- test/core/gc/extern.wast | 2 +- test/core/gc/i31.wast | 10 +++++----- test/core/gc/ref_cast.wast | 2 +- test/core/gc/ref_eq.wast | 6 +++--- test/core/gc/ref_test.wast | 4 ++-- 29 files changed, 63 insertions(+), 64 deletions(-) diff --git a/document/core/appendix/changes.rst b/document/core/appendix/changes.rst index e0bb708f0..2817d5a5d 100644 --- a/document/core/appendix/changes.rst +++ b/document/core/appendix/changes.rst @@ -182,7 +182,7 @@ Added managed reference types [#proposal-gc]_. * New generic :ref:`reference instructions `: |REFEQ|, |REFTEST|, |REFCAST|, |BRONCAST|, |BRONCASTFAIL| -* New :ref:`reference instructions ` for :ref:`unboxed scalars `: |I31NEW|, :math:`\I31GET\K{\_}\sx` +* New :ref:`reference instructions ` for :ref:`unboxed scalars `: |REFI31|, :math:`\I31GET\K{\_}\sx` * New :ref:`reference instructions ` for :ref:`structure types `: |STRUCTNEW|, |STRUCTNEWDEFAULT|, :math:`\STRUCTGET\K{\_}\sx^?`, |STRUCTSET| @@ -190,7 +190,7 @@ Added managed reference types [#proposal-gc]_. * New :ref:`reference instructions ` for converting :ref:`host types `: |EXTERNINTERNALIZE|, |EXTERNEXTERNALIZE| -* Extended set of :ref:`constant instructions ` with |I31NEW|, |STRUCTNEW|, |STRUCTNEWDEFAULT|, |ARRAYNEW|, |ARRAYNEWDEFAULT|, |ARRAYNEWFIXED|, |EXTERNINTERNALIZE|, |EXTERNEXTERNALIZE|, and |GLOBALGET| for any previously declared immutable :ref:`global ` +* Extended set of :ref:`constant instructions ` with |REFI31|, |STRUCTNEW|, |STRUCTNEWDEFAULT|, |ARRAYNEW|, |ARRAYNEWDEFAULT|, |ARRAYNEWFIXED|, |EXTERNINTERNALIZE|, |EXTERNEXTERNALIZE|, and |GLOBALGET| for any previously declared immutable :ref:`global ` .. [#proposal-signext] diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index 80c8e8b03..edcddb6fa 100755 --- a/document/core/appendix/index-instructions.py +++ b/document/core/appendix/index-instructions.py @@ -348,7 +348,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\BRONCASTFAIL~t_1~t_2', r'\hex{FB}~\hex{19}', r'[t_1] \to [t_2]', r'valid-br_on_cast_fail', r'exec-br_on_cast_fail'), Instruction(r'\EXTERNINTERNALIZE', r'\hex{FB}~\hex{1A}', r'[\EXTERNREF] \to [\ANYREF]', r'valid-extern.internalize', r'exec-extern.internalize'), Instruction(r'\EXTERNEXTERNALIZE', r'\hex{FB}~\hex{1B}', r'[\ANYREF] \to [\EXTERNREF]', r'valid-extern.externalize', r'exec-extern.externalize'), - Instruction(r'\I31NEW', r'\hex{FB}~\hex{1C}', r'[\I32] \to [\I31REF]', r'valid-i31.new', r'exec-i31.new'), + Instruction(r'\REFI31', r'\hex{FB}~\hex{1C}', r'[\I32] \to [\I31REF]', r'valid-ref.i31', r'exec-ref.i31'), Instruction(r'\I31GETS', r'\hex{FB}~\hex{1D}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'), Instruction(r'\I31GETU', r'\hex{FB}~\hex{1E}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'), Instruction(None, r'\hex{FB}~\hex{1E} \dots'), diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 2aebc124d..53e32a3cd 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -126,7 +126,7 @@ Generic :ref:`reference instructions ` are represented by sing .. _binary-array.copy: .. _binary-array.init_data: .. _binary-array.init_elem: -.. _binary-i31.new: +.. _binary-ref.i31: .. _binary-i31.get_s: .. _binary-i31.get_u: .. _binary-ref.test: @@ -168,7 +168,7 @@ Generic :ref:`reference instructions ` are represented by sing \hex{FB}~~23{:}\Bu32~~\X{ht}{:}\Bheaptype &\Rightarrow& \REFCAST~(\REF~\NULL~\X{ht}) \\ &&|& \hex{FB}~~26{:}\Bu32 &\Rightarrow& \EXTERNINTERNALIZE \\ &&|& \hex{FB}~~27{:}\Bu32 &\Rightarrow& \EXTERNEXTERNALIZE \\ &&|& - \hex{FB}~~28{:}\Bu32 &\Rightarrow& \I31NEW \\ &&|& + \hex{FB}~~28{:}\Bu32 &\Rightarrow& \REFI31 \\ &&|& \hex{FB}~~29{:}\Bu32 &\Rightarrow& \I31GETS \\ &&|& \hex{FB}~~30{:}\Bu32 &\Rightarrow& \I31GETU \\ \end{array} diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 5768ca375..4dee649e6 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -375,22 +375,22 @@ Reference Instructions -.. _exec-i31.new: +.. _exec-ref.i31: -:math:`\I31NEW` +:math:`\REFI31` ............... -1. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` |I32| is on the top of the stack. +1. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` |I32| is on the top of the stack. 2. Pop the value :math:`\I32.\CONST~i` from the stack. 3. Let :math:`j` be the result of computing :math:`\wrap_{32,31}(i)`. -4. Push the reference value :math:`(\REFI31~j)` to the stack. +4. Push the reference value :math:`(\REFI31NUM~j)` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} - (\I32.\CONST~i)~\I31NEW &\stepto& (\REFI31~\wrap_{32,31}(i)) + (\I32.\CONST~i)~\REFI31 &\stepto& (\REFI31NUM~\wrap_{32,31}(i)) \end{array} @@ -409,7 +409,7 @@ Reference Instructions 4. Assert: due to :ref:`validation `, a :math:`\reff` is a :ref:`scalar reference `. -5. Let :math:`\REFI31~i` be the reference value :math:`\reff`. +5. Let :math:`\REFI31NUM~i` be the reference value :math:`\reff`. 6. Let :math:`j` be the result of computing :math:`\extend^{\sx}_{31,32}(i)`. @@ -417,8 +417,8 @@ Reference Instructions .. math:: \begin{array}{lcl@{\qquad}l} - (\REFI31~i)~\I31NEW &\stepto& (\I32.\CONST~\extend^{\sx}_{31,32}(i)) \\ - (\REFNULL~t)~\I31NEW &\stepto& \TRAP + (\REFI31NUM~i)~\I31GET\K{\_}\sx &\stepto& (\I32.\CONST~\extend^{\sx}_{31,32}(i)) \\ + (\REFNULL~t)~\I31GET\K{\_}\sx &\stepto& \TRAP \end{array} diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index bf3b4ef69..3a613aa5d 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -12,7 +12,7 @@ Runtime Structure .. _syntax-num: .. _syntax-vecc: .. _syntax-ref: -.. _syntax-ref.i31: +.. _syntax-ref.i31num: .. _syntax-ref.struct: .. _syntax-ref.array: .. _syntax-ref.host: @@ -48,7 +48,7 @@ Any of the aformentioned references can furthermore be wrapped up as an *externa \V128.\CONST~\i128 \\ \production{reference} & \reff &::=& \REFNULL~t \\&&|& - \REFI31~\u31 \\&&|& + \REFI31NUM~\u31 \\&&|& \REFSTRUCTADDR~\structaddr \\&&|& \REFARRAYADDR~\arrayaddr \\&&|& \REFFUNCADDR~\funcaddr \\&&|& @@ -634,7 +634,7 @@ In order to express the reduction of :ref:`traps `, :ref:`calls `, :ref:`calls ` reference values, +The |REFI31NUM| instruction represents :ref:`unboxed scalar ` reference values, |REFSTRUCTADDR| and |REFARRAYADDR| represent :ref:`structure ` and :ref:`array ` reference values, respectively, and |REFFUNCADDR| instruction represents :ref:`function reference ` values. Similarly, |REFHOSTADDR| represents :ref:`host references ` diff --git a/document/core/exec/values.rst b/document/core/exec/values.rst index d7a7de952..7ec439cdd 100644 --- a/document/core/exec/values.rst +++ b/document/core/exec/values.rst @@ -66,17 +66,17 @@ The following auxiliary typing rules specify this typing relation relative to a That ensures that it is compatible with any nullable type in that hierarchy. -.. _valid-ref.i31: +.. _valid-ref.i31num: -:ref:`Scalar References ` :math:`\REFI31~i` -....................................................... +:ref:`Scalar References ` :math:`\REFI31NUM~i` +.......................................................... * The value is valid with :ref:`reference type ` :math:`(\REF~\I31)`. .. math:: \frac{ }{ - S \vdashval \REFI31~i : \REF~\I31 + S \vdashval \REFI31NUM~i : \REF~\I31 } diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 67b985885..1d6a61b71 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -482,7 +482,7 @@ while the latter performs a downcast and :ref:`traps ` if the operand's ty .. _syntax-array.copy: .. _syntax-array.init_data: .. _syntax-array.init_elem: -.. _syntax-i31.new: +.. _syntax-ref.i31: .. _syntax-i31.get_s: .. _syntax-i31.get_u: .. _syntax-extern.internalize: @@ -519,7 +519,7 @@ Instructions in this group are concerned with creating and accessing :ref:`refer \ARRAYCOPY~\typeidx~\typeidx \\&&|& \ARRAYINITDATA~\typeidx~\dataidx \\&&|& \ARRAYINITELEM~\typeidx~\elemidx \\&&|& - \I31NEW \\&&|& + \REFI31 \\&&|& \I31GET\K{\_}\sx \\&&|& \EXTERNINTERNALIZE \\&&|& \EXTERNEXTERNALIZE \\ @@ -537,7 +537,7 @@ again allowing for different sign extension modes in the case of a :ref:`packed |ARRAYLEN| produces the length of an array. |ARRAYFILL| fills a specified slice of an array with a given value and |ARRAYCOPY|, |ARRAYINITDATA|, and |ARRAYINITELEM| copy elements to a specified slice of an array from a given array, data segment, or element segment, respectively. -The instructions |I31NEW| and :math:`\I31GET\K{\_}\sx` convert between type |I31| and an unboxed :ref:`scalar `. +The instructions |REFI31| and :math:`\I31GET\K{\_}\sx` convert between type |I31| and an unboxed :ref:`scalar `. The instructions |EXTERNINTERNALIZE| and |EXTERNEXTERNALIZE| allow lossless conversion between references represented as type :math:`(\REF~\NULL~\EXTERN)`| and as :math:`(\REF~\NULL~\ANY)`. diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 1b076c383..ad1c3e3e1 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -199,7 +199,7 @@ Reference Instructions .. _text-array.copy: .. _text-array.init_data: .. _text-array.init_elem: -.. _text-i31.new: +.. _text-ref.i31: .. _text-i31.get_s: .. _text-i31.get_u: .. _text-ref.test: @@ -237,7 +237,7 @@ Reference Instructions \text{array.copy}~~x{:}\Ttypeidx_I~~y{:}\Ttypeidx_I &\Rightarrow& \ARRAYCOPY~x~y \\ &&|& \text{array.init\_data}~~x{:}\Ttypeidx_I~~y{:}\Tdataidx_I &\Rightarrow& \ARRAYINITDATA~x~y \\ &&|& \text{array.init\_elem}~~x{:}\Ttypeidx_I~~y{:}\Telemidx_I &\Rightarrow& \ARRAYINITELEM~x~y \\ &&|& - \text{i31.new} &\Rightarrow& \I31NEW \\ &&|& + \text{ref.i31} &\Rightarrow& \REFI31 \\ &&|& \text{i31.get\_u} &\Rightarrow& \I31GETU \\ &&|& \text{i31.get\_s} &\Rightarrow& \I31GETS \\ &&|& \text{extern.internalize} &\Rightarrow& \EXTERNINTERNALIZE \\ &&|& diff --git a/document/core/util/macros.def b/document/core/util/macros.def index b027b9033..8489531a7 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -504,7 +504,7 @@ .. |ARRAYINITDATA| mathdef:: \xref{syntax/instructions}{syntax-instr-aray}{\K{array.init\_data}} .. |ARRAYINITELEM| mathdef:: \xref{syntax/instructions}{syntax-instr-aray}{\K{array.init\_elem}} -.. |I31NEW| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{i31.new}} +.. |REFI31| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{ref.i31}} .. |I31GET| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{i31.get}} .. |I31GETS| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{i31.get\_s}} .. |I31GETU| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{i31.get\_u}} @@ -1301,7 +1301,7 @@ .. Administrative Instructions, terminals -.. |REFI31| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}i31}} +.. |REFI31NUM| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}i31}} .. |REFFUNCADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}func}} .. |REFSTRUCTADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}struct}} .. |REFARRAYADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}array}} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 0509bd591..c7fdafedf 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -729,9 +729,9 @@ Aggregate Reference Instructions Scalar Reference Instructions ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. _valid-i31.new: +.. _valid-ref.i31: -:math:`\I31NEW` +:math:`\REFI31` ............... * The instruction is valid with type :math:`[\I32] \to [(\REF~\I31)]`. @@ -739,7 +739,7 @@ Scalar Reference Instructions .. math:: \frac{ }{ - C \vdashinstr \I31NEW : [\I32] \to [(\REF~\I31)] + C \vdashinstr \REFI31 : [\I32] \to [(\REF~\I31)] } .. _valid-i31.get_sx: diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index baaae3e72..f3ebce676 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -625,7 +625,7 @@ let rec instr s = | 0x1al -> extern_internalize | 0x1bl -> extern_externalize - | 0x1cl -> i31_new + | 0x1cl -> ref_i31 | 0x1dl -> i31_get_s | 0x1el -> i31_get_u diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index c1d8b47c7..0319f5c06 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -385,7 +385,7 @@ struct | RefCast (NoNull, t) -> op 0xfb; op 0x16; heap_type t | RefCast (Null, t) -> op 0xfb; op 0x17; heap_type t - | I31New -> op 0xfb; op 0x1c + | RefI31 -> op 0xfb; op 0x1c | I31Get SX -> op 0xfb; op 0x1d | I31Get ZX -> op 0xfb; op 0x1e diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 2ca39e395..b4a0062de 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -609,7 +609,7 @@ let rec step (c : config) : config = | RefEq, Ref r1 :: Ref r2 :: vs' -> value_of_bool (eq_ref r1 r2) :: vs', [] - | I31New, Num (I32 i) :: vs' -> + | RefI31, Num (I32 i) :: vs' -> Ref (I31.I31Ref (I31.of_i32 i)) :: vs', [] | I31Get ext, Ref (NullRef _) :: vs' -> diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml index 437e3a10c..d7535374c 100644 --- a/interpreter/syntax/ast.ml +++ b/interpreter/syntax/ast.ml @@ -201,7 +201,7 @@ and instr' = | RefTest of ref_type (* type test *) | RefCast of ref_type (* type cast *) | RefEq (* reference equality *) - | I31New (* allocate scalar *) + | RefI31 (* scalar reference *) | I31Get of extension (* read scalar *) | StructNew of idx * initop (* allocate structure *) | StructGet of idx * idx * extension option (* read structure field *) diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml index a43b72f31..85858d432 100644 --- a/interpreter/syntax/free.ml +++ b/interpreter/syntax/free.ml @@ -139,7 +139,7 @@ let rec instr (e : instr) = | RefEq -> empty | RefNull t -> heap_type t | RefFunc x -> funcs (idx x) - | I31New | I31Get _ -> empty + | RefI31 | I31Get _ -> empty | StructNew (x, _) | ArrayNew (x, _) | ArrayNewFixed (x, _) -> types (idx x) | ArrayNewElem (x, y) -> types (idx x) ++ elems (idx y) | ArrayNewData (x, y) -> types (idx x) ++ datas (idx y) diff --git a/interpreter/syntax/operators.ml b/interpreter/syntax/operators.ml index 168265898..cc3d09b69 100644 --- a/interpreter/syntax/operators.ml +++ b/interpreter/syntax/operators.ml @@ -108,7 +108,7 @@ let ref_test t = RefTest t let ref_cast t = RefCast t let ref_eq = RefEq -let i31_new = I31New +let ref_i31 = RefI31 let i31_get_u = I31Get ZX let i31_get_s = I31Get SX let struct_new x = StructNew (x, Explicit) diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index 0124b27f5..71590ef8a 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -545,7 +545,7 @@ let rec instr e = | RefTest t -> "ref.test", [Atom (ref_type t)] | RefCast t -> "ref.cast", [Atom (ref_type t)] | RefEq -> "ref.eq", [] - | I31New -> "i31.new", [] + | RefI31 -> "ref.i31", [] | I31Get ext -> "i31.get" ^ extension ext, [] | StructNew (x, op) -> "struct.new" ^ initop op ^ " " ^ var x, [] | StructGet (x, y, exto) -> diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll index 3435dd3d0..44c22423c 100644 --- a/interpreter/text/lexer.mll +++ b/interpreter/text/lexer.mll @@ -308,7 +308,6 @@ rule token = parse | "ref.null" -> REF_NULL | "ref.func" -> REF_FUNC - | "ref.i31" -> REF_I31 | "ref.struct" -> REF_STRUCT | "ref.array" -> REF_ARRAY | "ref.extern" -> REF_EXTERN @@ -320,7 +319,7 @@ rule token = parse | "ref.cast" -> REF_CAST | "ref.eq" -> REF_EQ - | "i31.new" -> I31_NEW + | "ref.i31" -> REF_I31 | "i31.get_u" -> I31_GET i31_get_u | "i31.get_s" -> I31_GET i31_get_s diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 4c16da85e..8e74493f8 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -275,7 +275,7 @@ let inline_func_type_explicit (c : context) x ft at = %token UNARY BINARY TEST COMPARE CONVERT %token REF_NULL REF_FUNC REF_I31 REF_STRUCT REF_ARRAY REF_EXTERN REF_HOST %token REF_EQ REF_IS_NULL REF_AS_NON_NULL REF_TEST REF_CAST -%token I31_NEW +%token REF_I31 %token I31_GET %token Ast.instr'> STRUCT_NEW ARRAY_NEW ARRAY_GET %token STRUCT_SET @@ -565,7 +565,7 @@ plain_instr : | REF_TEST ref_type { fun c -> ref_test ($2 c) } | REF_CAST ref_type { fun c -> ref_cast ($2 c) } | REF_EQ { fun c -> ref_eq } - | I31_NEW { fun c -> i31_new } + | REF_I31 { fun c -> ref_i31 } | I31_GET { fun c -> $1 } | STRUCT_NEW var { fun c -> $1 ($2 c type_) } | STRUCT_GET var var { fun c -> let x = $2 c type_ in $1 x ($3 c (field x.it)) } diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 53d0cb976..5a28beb63 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -676,7 +676,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in | RefEq -> [RefT (Null, EqHT); RefT (Null, EqHT)] --> [NumT I32T], [] - | I31New -> + | RefI31 -> [NumT I32T] --> [RefT (NoNull, I31HT)], [] | I31Get ext -> @@ -944,7 +944,7 @@ let is_const (c : context) (e : instr) = match e.it with | Const _ | VecConst _ | RefNull _ | RefFunc _ - | I31New | StructNew _ | ArrayNew _ | ArrayNewFixed _ -> true + | RefI31 | StructNew _ | ArrayNew _ | ArrayNewFixed _ -> true | GlobalGet x -> let GlobalT (mut, _t) = global c x in mut = Cons | _ -> false diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index 6382005df..69d72a6f0 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -630,8 +630,8 @@ In particular, `ref.null` is typed as before, despite the introduction of `none` #### Unboxed Scalars -* `i31.new` creates an `i31ref` from a 32 bit value, truncating high bit - - `i31.new : [i32] -> [(ref i31)]` +* `ref.i31` creates an `i31ref` from a 32 bit value, truncating high bit + - `ref.i31 : [i32] -> [(ref i31)]` - this is a *constant instruction* * `i31.get_` extracts the value, zero- or sign-extending @@ -703,7 +703,7 @@ Note: The [reference types](https://github.com/WebAssembly/reference-types) and In order to allow RTTs to be initialised as globals, the following extensions are made to the definition of *constant expressions*: -* `i31.new` is a constant instruction +* `ref.i31` is a constant instruction * `struct.new` and `struct.new_default` are constant instructions * `array.new`, `array.new_default`, and `array.new_fixed` are constant instructions - Note: `array.new_data` and `array.new_elem` are not for the time being, see above @@ -834,7 +834,7 @@ The opcode for heap types is encoded as an `s33`. | 0xfb19 | `br_on_cast_fail $l (ref null1? ht1) (ref null2? ht2)` | `flags : u8`, $l : labelidx`, `ht1 : heaptype`, `ht2 : heaptype` | | 0xfb1a | `extern.internalize` | | 0xfb1b | `extern.externalize` | -| 0xfb1c | `i31.new` | +| 0xfb1c | `ref.i31` | | 0xfb1d | `i31.get_s` | | 0xfb1e | `i31.get_u` | diff --git a/proposals/gc/Overview.md b/proposals/gc/Overview.md index f215b0c94..7655c206e 100644 --- a/proposals/gc/Overview.md +++ b/proposals/gc/Overview.md @@ -350,7 +350,7 @@ However, compilation with a uniform representation can still be achieved in this (func $new_C (result (ref $C)) ...) (func $f ... - (call $make_pair (i31.new 1) (i31.new 0)) + (call $make_pair (ref.i31 1) (ref.i31 0)) ... (call $make_pair (call $new_C) (call $new_C)) ... @@ -607,7 +607,7 @@ To implement any such language efficiently, Wasm needs to provide such a mechani There are only three instructions for converting from and to this reference type: ``` -i31.new : [i32] -> [i31ref] +ref.i31 : [i32] -> [i31ref] i31.get_u : [i31ref] -> [i32] i31.get_s : [i31ref] -> [i32] ``` diff --git a/test/core/gc/br_on_cast.wast b/test/core/gc/br_on_cast.wast index a7b35949a..5b0605545 100644 --- a/test/core/gc/br_on_cast.wast +++ b/test/core/gc/br_on_cast.wast @@ -12,7 +12,7 @@ (func (export "init") (param $x externref) (table.set (i32.const 0) (ref.null any)) - (table.set (i32.const 1) (i31.new (i32.const 7))) + (table.set (i32.const 1) (ref.i31 (i32.const 7))) (table.set (i32.const 2) (struct.new $st (i32.const 6))) (table.set (i32.const 3) (array.new $at (i32.const 5) (i32.const 3))) (table.set (i32.const 4) (extern.internalize (local.get $x))) diff --git a/test/core/gc/br_on_cast_fail.wast b/test/core/gc/br_on_cast_fail.wast index 601de88af..ac5086407 100644 --- a/test/core/gc/br_on_cast_fail.wast +++ b/test/core/gc/br_on_cast_fail.wast @@ -12,7 +12,7 @@ (func (export "init") (param $x externref) (table.set (i32.const 0) (ref.null any)) - (table.set (i32.const 1) (i31.new (i32.const 7))) + (table.set (i32.const 1) (ref.i31 (i32.const 7))) (table.set (i32.const 2) (struct.new $st (i32.const 6))) (table.set (i32.const 3) (array.new $at (i32.const 5) (i32.const 3))) (table.set (i32.const 4) (extern.internalize (local.get $x))) diff --git a/test/core/gc/extern.wast b/test/core/gc/extern.wast index f9b01f11e..0f2fa8ec6 100644 --- a/test/core/gc/extern.wast +++ b/test/core/gc/extern.wast @@ -10,7 +10,7 @@ (func (export "init") (param $x externref) (table.set (i32.const 0) (ref.null any)) - (table.set (i32.const 1) (i31.new (i32.const 7))) + (table.set (i32.const 1) (ref.i31 (i32.const 7))) (table.set (i32.const 2) (struct.new_default $st)) (table.set (i32.const 3) (array.new_default $at (i32.const 0))) (table.set (i32.const 4) (extern.internalize (local.get $x))) diff --git a/test/core/gc/i31.wast b/test/core/gc/i31.wast index 284b5d244..3b6c32fba 100644 --- a/test/core/gc/i31.wast +++ b/test/core/gc/i31.wast @@ -1,13 +1,13 @@ (module (func (export "new") (param $i i32) (result (ref i31)) - (i31.new (local.get $i)) + (ref.i31 (local.get $i)) ) (func (export "get_u") (param $i i32) (result i32) - (i31.get_u (i31.new (local.get $i))) + (i31.get_u (ref.i31 (local.get $i))) ) (func (export "get_s") (param $i i32) (result i32) - (i31.get_s (i31.new (local.get $i))) + (i31.get_s (ref.i31 (local.get $i))) ) (func (export "get_u-null") (result i32) @@ -17,8 +17,8 @@ (i31.get_u (ref.null i31)) ) - (global $i (ref i31) (i31.new (i32.const 2))) - (global $m (mut (ref i31)) (i31.new (i32.const 3))) + (global $i (ref i31) (ref.i31 (i32.const 2))) + (global $m (mut (ref i31)) (ref.i31 (i32.const 3))) (func (export "get_globals") (result i32 i32) (i31.get_u (global.get $i)) (i31.get_u (global.get $m)) diff --git a/test/core/gc/ref_cast.wast b/test/core/gc/ref_cast.wast index 0a1a0edea..43a9587d8 100644 --- a/test/core/gc/ref_cast.wast +++ b/test/core/gc/ref_cast.wast @@ -12,7 +12,7 @@ (func (export "init") (param $x externref) (table.set (i32.const 0) (ref.null any)) - (table.set (i32.const 1) (i31.new (i32.const 7))) + (table.set (i32.const 1) (ref.i31 (i32.const 7))) (table.set (i32.const 2) (struct.new_default $st)) (table.set (i32.const 3) (array.new_default $at (i32.const 0))) (table.set (i32.const 4) (extern.internalize (local.get $x))) diff --git a/test/core/gc/ref_eq.wast b/test/core/gc/ref_eq.wast index c30d7a5c1..001efd69f 100644 --- a/test/core/gc/ref_eq.wast +++ b/test/core/gc/ref_eq.wast @@ -12,9 +12,9 @@ (func (export "init") (table.set (i32.const 0) (ref.null eq)) (table.set (i32.const 1) (ref.null i31)) - (table.set (i32.const 2) (i31.new (i32.const 7))) - (table.set (i32.const 3) (i31.new (i32.const 7))) - (table.set (i32.const 4) (i31.new (i32.const 8))) + (table.set (i32.const 2) (ref.i31 (i32.const 7))) + (table.set (i32.const 3) (ref.i31 (i32.const 7))) + (table.set (i32.const 4) (ref.i31 (i32.const 8))) (table.set (i32.const 5) (struct.new_default $st)) (table.set (i32.const 6) (struct.new_default $st)) (table.set (i32.const 7) (array.new_default $at (i32.const 0))) diff --git a/test/core/gc/ref_test.wast b/test/core/gc/ref_test.wast index 31cf62897..9a34c8468 100644 --- a/test/core/gc/ref_test.wast +++ b/test/core/gc/ref_test.wast @@ -16,7 +16,7 @@ (table.set $ta (i32.const 0) (ref.null any)) (table.set $ta (i32.const 1) (ref.null struct)) (table.set $ta (i32.const 2) (ref.null none)) - (table.set $ta (i32.const 3) (i31.new (i32.const 7))) + (table.set $ta (i32.const 3) (ref.i31 (i32.const 7))) (table.set $ta (i32.const 4) (struct.new_default $st)) (table.set $ta (i32.const 5) (array.new_default $at (i32.const 0))) (table.set $ta (i32.const 6) (extern.internalize (local.get $x))) @@ -29,7 +29,7 @@ (table.set $te (i32.const 0) (ref.null noextern)) (table.set $te (i32.const 1) (ref.null extern)) (table.set $te (i32.const 2) (local.get $x)) - (table.set $te (i32.const 3) (extern.externalize (i31.new (i32.const 8)))) + (table.set $te (i32.const 3) (extern.externalize (ref.i31 (i32.const 8)))) (table.set $te (i32.const 4) (extern.externalize (struct.new_default $st))) (table.set $te (i32.const 5) (extern.externalize (ref.null any))) ) From c27610d09200c19e553318918eaad4db224a1691 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Mon, 11 Sep 2023 18:07:15 -0700 Subject: [PATCH 20/20] Test that br_on_cast{_fail} must do a down cast Add tests checking for validation failures if the output type of br_on_cast or br_on_cast_fail is not a subtype of the input type. --- test/core/gc/br_on_cast.wast | 8 ++++++++ test/core/gc/br_on_cast_fail.wast | 8 ++++++++ 2 files changed, 16 insertions(+) diff --git a/test/core/gc/br_on_cast.wast b/test/core/gc/br_on_cast.wast index a7b35949a..ec925cfdc 100644 --- a/test/core/gc/br_on_cast.wast +++ b/test/core/gc/br_on_cast.wast @@ -249,3 +249,11 @@ ) "type mismatch" ) +(assert_invalid + (module + (func (result anyref) + (br_on_cast 0 eqref anyref (unreachable)) + ) + ) + "type mismatch" +) diff --git a/test/core/gc/br_on_cast_fail.wast b/test/core/gc/br_on_cast_fail.wast index 601de88af..c422d1ba1 100644 --- a/test/core/gc/br_on_cast_fail.wast +++ b/test/core/gc/br_on_cast_fail.wast @@ -264,3 +264,11 @@ ) "type mismatch" ) +(assert_invalid + (module + (func (result anyref) + (br_on_cast_fail 0 eqref anyref (unreachable)) + ) + ) + "type mismatch" +)