From ea1e36c3ea7ffe2fa8b9767722305bc3ab204190 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 25 Jun 2021 08:52:34 +0200 Subject: [PATCH 1/5] [spec] New instructions --- .../core/appendix/gen-index-instructions.py | 12 +- document/core/appendix/index-instructions.rst | 548 +++++++++--------- document/core/binary/instructions.rst | 15 +- document/core/exec/instructions.rst | 125 +++- document/core/syntax/instructions.rst | 14 +- document/core/text/instructions.rst | 12 +- document/core/util/macros.def | 6 +- document/core/valid/instructions.rst | 120 +++- proposals/function-references/Overview.md | 2 +- 9 files changed, 528 insertions(+), 326 deletions(-) diff --git a/document/core/appendix/gen-index-instructions.py b/document/core/appendix/gen-index-instructions.py index 6191a07b..f366ae48 100755 --- a/document/core/appendix/gen-index-instructions.py +++ b/document/core/appendix/gen-index-instructions.py @@ -81,7 +81,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\CALLINDIRECT~x~y', r'\hex{11}', r'[t_1^\ast~\I32] \to [t_2^\ast]', r'valid-call_indirect', r'exec-call_indirect'), Instruction(None, r'\hex{12}'), Instruction(None, r'\hex{13}'), - Instruction(None, r'\hex{14}'), + Instruction(r'\CALLREF', r'\hex{14}', r'[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]', r'valid-call_ref', r'exec-call_ref'), Instruction(None, r'\hex{15}'), Instruction(None, r'\hex{16}'), Instruction(None, r'\hex{17}'), @@ -269,13 +269,13 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(None, r'\hex{CD}'), Instruction(None, r'\hex{CE}'), Instruction(None, r'\hex{CF}'), - Instruction(r'\REFNULL~t', r'\hex{D0}', r'[] \to [t]', r'valid-ref.null', r'exec-ref.null'), - Instruction(r'\REFISNULL', r'\hex{D1}', r'[t] \to [\I32]', r'valid-ref.is_null', r'exec-ref.is_null'), + 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(None, r'\hex{D3}'), - Instruction(None, r'\hex{D4}'), + 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{D6}'), + 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}'), Instruction(None, r'\hex{D9}'), diff --git a/document/core/appendix/index-instructions.rst b/document/core/appendix/index-instructions.rst index 55bf8fb9..545638b6 100644 --- a/document/core/appendix/index-instructions.rst +++ b/document/core/appendix/index-instructions.rst @@ -6,277 +6,277 @@ Index of Instructions --------------------- -========================================= ========================= ============================================= ======================================= =============================================================== -Instruction Binary Opcode Type Validation Execution -========================================= ========================= ============================================= ======================================= =============================================================== -:math:`\UNREACHABLE` :math:`\hex{00}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\NOP` :math:`\hex{01}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` -:math:`\BLOCK~\X{bt}` :math:`\hex{02}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\LOOP~\X{bt}` :math:`\hex{03}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\IF~\X{bt}` :math:`\hex{04}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\ELSE` :math:`\hex{05}` -(reserved) :math:`\hex{06}` -(reserved) :math:`\hex{07}` -(reserved) :math:`\hex{08}` -(reserved) :math:`\hex{09}` -(reserved) :math:`\hex{0A}` -:math:`\END` :math:`\hex{0B}` -:math:`\BR~l` :math:`\hex{0C}` :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\BRIF~l` :math:`\hex{0D}` :math:`[t^\ast~\I32] \to [t^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\BRTABLE~l^\ast~l` :math:`\hex{0E}` :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\RETURN` :math:`\hex{0F}` :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\CALL~x` :math:`\hex{10}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\CALLINDIRECT~x~y` :math:`\hex{11}` :math:`[t_1^\ast~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -(reserved) :math:`\hex{12}` -(reserved) :math:`\hex{13}` -(reserved) :math:`\hex{14}` -(reserved) :math:`\hex{15}` -(reserved) :math:`\hex{16}` -(reserved) :math:`\hex{17}` -(reserved) :math:`\hex{18}` -(reserved) :math:`\hex{19}` -:math:`\DROP` :math:`\hex{1A}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` -:math:`\SELECT` :math:`\hex{1B}` :math:`[t~t~\I32] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\SELECT~t` :math:`\hex{1C}` :math:`[t~t~\I32] \to [t]` :ref:`validation ` :ref:`execution ` -(reserved) :math:`\hex{1D}` -(reserved) :math:`\hex{1E}` -(reserved) :math:`\hex{1F}` -:math:`\LOCALGET~x` :math:`\hex{20}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\LOCALSET~x` :math:`\hex{21}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` -:math:`\LOCALTEE~x` :math:`\hex{22}` :math:`[t] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\GLOBALGET~x` :math:`\hex{23}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\GLOBALSET~x` :math:`\hex{24}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` -:math:`\TABLEGET~x` :math:`\hex{25}` :math:`[\I32] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\TABLESET~x` :math:`\hex{26}` :math:`[\I32~t] \to []` :ref:`validation ` :ref:`execution ` -(reserved) :math:`\hex{27}` -:math:`\I32.\LOAD~\memarg` :math:`\hex{28}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD~\memarg` :math:`\hex{29}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\F32.\LOAD~\memarg` :math:`\hex{2A}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution ` -:math:`\F64.\LOAD~\memarg` :math:`\hex{2B}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\LOAD\K{8\_s}~\memarg` :math:`\hex{2C}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\LOAD\K{8\_u}~\memarg` :math:`\hex{2D}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\LOAD\K{16\_s}~\memarg` :math:`\hex{2E}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\LOAD\K{16\_u}~\memarg` :math:`\hex{2F}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{8\_s}~\memarg` :math:`\hex{30}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{8\_u}~\memarg` :math:`\hex{31}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{16\_s}~\memarg` :math:`\hex{32}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{16\_u}~\memarg` :math:`\hex{33}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{32\_s}~\memarg` :math:`\hex{34}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{32\_u}~\memarg` :math:`\hex{35}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\STORE~\memarg` :math:`\hex{36}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I64.\STORE~\memarg` :math:`\hex{37}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\F32.\STORE~\memarg` :math:`\hex{38}` :math:`[\I32~\F32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\F64.\STORE~\memarg` :math:`\hex{39}` :math:`[\I32~\F64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I32.\STORE\K{8}~\memarg` :math:`\hex{3A}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I32.\STORE\K{16}~\memarg` :math:`\hex{3B}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I64.\STORE\K{8}~\memarg` :math:`\hex{3C}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I64.\STORE\K{16}~\memarg` :math:`\hex{3D}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I64.\STORE\K{32}~\memarg` :math:`\hex{3E}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\MEMORYSIZE` :math:`\hex{3F}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\MEMORYGROW` :math:`\hex{40}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\CONST~\i32` :math:`\hex{41}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\CONST~\i64` :math:`\hex{42}` :math:`[] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\F32.\CONST~\f32` :math:`\hex{43}` :math:`[] \to [\F32]` :ref:`validation ` :ref:`execution ` -:math:`\F64.\CONST~\f64` :math:`\hex{44}` :math:`[] \to [\F64]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\EQZ` :math:`\hex{45}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\EQ` :math:`\hex{46}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\NE` :math:`\hex{47}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\LT\K{\_s}` :math:`\hex{48}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\LT\K{\_u}` :math:`\hex{49}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\GT\K{\_s}` :math:`\hex{4A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\GT\K{\_u}` :math:`\hex{4B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\LE\K{\_s}` :math:`\hex{4C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\LE\K{\_u}` :math:`\hex{4D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\GE\K{\_s}` :math:`\hex{4E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\GE\K{\_u}` :math:`\hex{4F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EQZ` :math:`\hex{50}` :math:`[\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EQ` :math:`\hex{51}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\NE` :math:`\hex{52}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\LT\K{\_s}` :math:`\hex{53}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\LT\K{\_u}` :math:`\hex{54}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\GT\K{\_s}` :math:`\hex{55}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\GT\K{\_u}` :math:`\hex{56}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\LE\K{\_s}` :math:`\hex{57}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\LE\K{\_u}` :math:`\hex{58}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\GE\K{\_s}` :math:`\hex{59}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\GE\K{\_u}` :math:`\hex{5A}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\EQ` :math:`\hex{5B}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\NE` :math:`\hex{5C}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\LT` :math:`\hex{5D}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\GT` :math:`\hex{5E}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\LE` :math:`\hex{5F}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\GE` :math:`\hex{60}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\EQ` :math:`\hex{61}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\NE` :math:`\hex{62}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\LT` :math:`\hex{63}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\GT` :math:`\hex{64}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\LE` :math:`\hex{65}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\GE` :math:`\hex{66}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\CLZ` :math:`\hex{67}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\CTZ` :math:`\hex{68}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\POPCNT` :math:`\hex{69}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\ADD` :math:`\hex{6A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\SUB` :math:`\hex{6B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\MUL` :math:`\hex{6C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\DIV\K{\_s}` :math:`\hex{6D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\DIV\K{\_u}` :math:`\hex{6E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\REM\K{\_s}` :math:`\hex{6F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\REM\K{\_u}` :math:`\hex{70}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\AND` :math:`\hex{71}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\OR` :math:`\hex{72}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\XOR` :math:`\hex{73}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\SHL` :math:`\hex{74}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\SHR\K{\_s}` :math:`\hex{75}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\SHR\K{\_u}` :math:`\hex{76}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\ROTL` :math:`\hex{77}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\ROTR` :math:`\hex{78}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\CLZ` :math:`\hex{79}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\CTZ` :math:`\hex{7A}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\POPCNT` :math:`\hex{7B}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\ADD` :math:`\hex{7C}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\SUB` :math:`\hex{7D}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\MUL` :math:`\hex{7E}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\DIV\K{\_s}` :math:`\hex{7F}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\DIV\K{\_u}` :math:`\hex{80}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\REM\K{\_s}` :math:`\hex{81}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\REM\K{\_u}` :math:`\hex{82}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\AND` :math:`\hex{83}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\OR` :math:`\hex{84}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\XOR` :math:`\hex{85}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\SHL` :math:`\hex{86}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\SHR\K{\_s}` :math:`\hex{87}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\SHR\K{\_u}` :math:`\hex{88}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\ROTL` :math:`\hex{89}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\ROTR` :math:`\hex{8A}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\ABS` :math:`\hex{8B}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\NEG` :math:`\hex{8C}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CEIL` :math:`\hex{8D}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\FLOOR` :math:`\hex{8E}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\TRUNC` :math:`\hex{8F}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\NEAREST` :math:`\hex{90}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\SQRT` :math:`\hex{91}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\ADD` :math:`\hex{92}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\SUB` :math:`\hex{93}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\MUL` :math:`\hex{94}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\DIV` :math:`\hex{95}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\FMIN` :math:`\hex{96}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\FMAX` :math:`\hex{97}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\COPYSIGN` :math:`\hex{98}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\ABS` :math:`\hex{99}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\NEG` :math:`\hex{9A}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CEIL` :math:`\hex{9B}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\FLOOR` :math:`\hex{9C}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\TRUNC` :math:`\hex{9D}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\NEAREST` :math:`\hex{9E}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\SQRT` :math:`\hex{9F}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\ADD` :math:`\hex{A0}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\SUB` :math:`\hex{A1}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\MUL` :math:`\hex{A2}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\DIV` :math:`\hex{A3}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\FMIN` :math:`\hex{A4}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\FMAX` :math:`\hex{A5}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\COPYSIGN` :math:`\hex{A6}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\WRAP\K{\_}\I64` :math:`\hex{A7}` :math:`[\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_}\F32\K{\_s}` :math:`\hex{A8}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_}\F32\K{\_u}` :math:`\hex{A9}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_}\F64\K{\_s}` :math:`\hex{AA}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_}\F64\K{\_u}` :math:`\hex{AB}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{\_}\I32\K{\_s}` :math:`\hex{AC}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{\_}\I32\K{\_u}` :math:`\hex{AD}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_}\F32\K{\_s}` :math:`\hex{AE}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_}\F32\K{\_u}` :math:`\hex{AF}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_}\F64\K{\_s}` :math:`\hex{B0}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_}\F64\K{\_u}` :math:`\hex{B1}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_}\I32\K{\_s}` :math:`\hex{B2}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_}\I32\K{\_u}` :math:`\hex{B3}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_}\I64\K{\_s}` :math:`\hex{B4}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_}\I64\K{\_u}` :math:`\hex{B5}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\DEMOTE\K{\_}\F64` :math:`\hex{B6}` :math:`[\F64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_}\I32\K{\_s}` :math:`\hex{B7}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_}\I32\K{\_u}` :math:`\hex{B8}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_}\I64\K{\_s}` :math:`\hex{B9}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_}\I64\K{\_u}` :math:`\hex{BA}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\PROMOTE\K{\_}\F32` :math:`\hex{BB}` :math:`[\F32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\REINTERPRET\K{\_}\F32` :math:`\hex{BC}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\REINTERPRET\K{\_}\F64` :math:`\hex{BD}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\REINTERPRET\K{\_}\I32` :math:`\hex{BE}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\REINTERPRET\K{\_}\I64` :math:`\hex{BF}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\EXTEND\K{8\_s}` :math:`\hex{C0}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\EXTEND\K{16\_s}` :math:`\hex{C1}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{8\_s}` :math:`\hex{C2}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{16\_s}` :math:`\hex{C3}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{32\_s}` :math:`\hex{C4}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -(reserved) :math:`\hex{C5}` -(reserved) :math:`\hex{C6}` -(reserved) :math:`\hex{C7}` -(reserved) :math:`\hex{C8}` -(reserved) :math:`\hex{C9}` -(reserved) :math:`\hex{CA}` -(reserved) :math:`\hex{CB}` -(reserved) :math:`\hex{CC}` -(reserved) :math:`\hex{CD}` -(reserved) :math:`\hex{CE}` -(reserved) :math:`\hex{CF}` -:math:`\REFNULL~t` :math:`\hex{D0}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\REFISNULL` :math:`\hex{D1}` :math:`[t] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\REFFUNC~x` :math:`\hex{D2}` :math:`[] \to [\FUNCREF]` :ref:`validation ` :ref:`execution ` -(reserved) :math:`\hex{D3}` -(reserved) :math:`\hex{D4}` -(reserved) :math:`\hex{D5}` -(reserved) :math:`\hex{D6}` -(reserved) :math:`\hex{D7}` -(reserved) :math:`\hex{D8}` -(reserved) :math:`\hex{D9}` -(reserved) :math:`\hex{DA}` -(reserved) :math:`\hex{DB}` -(reserved) :math:`\hex{DC}` -(reserved) :math:`\hex{DD}` -(reserved) :math:`\hex{DE}` -(reserved) :math:`\hex{DF}` -(reserved) :math:`\hex{E0}` -(reserved) :math:`\hex{E1}` -(reserved) :math:`\hex{E2}` -(reserved) :math:`\hex{E3}` -(reserved) :math:`\hex{E4}` -(reserved) :math:`\hex{E5}` -(reserved) :math:`\hex{E6}` -(reserved) :math:`\hex{E7}` -(reserved) :math:`\hex{E8}` -(reserved) :math:`\hex{E9}` -(reserved) :math:`\hex{EA}` -(reserved) :math:`\hex{EB}` -(reserved) :math:`\hex{EC}` -(reserved) :math:`\hex{ED}` -(reserved) :math:`\hex{EE}` -(reserved) :math:`\hex{EF}` -(reserved) :math:`\hex{F0}` -(reserved) :math:`\hex{F1}` -(reserved) :math:`\hex{F2}` -(reserved) :math:`\hex{F3}` -(reserved) :math:`\hex{F4}` -(reserved) :math:`\hex{F5}` -(reserved) :math:`\hex{F6}` -(reserved) :math:`\hex{F7}` -(reserved) :math:`\hex{F8}` -(reserved) :math:`\hex{F9}` -(reserved) :math:`\hex{FA}` -(reserved) :math:`\hex{FB}` -:math:`\I32.\TRUNC\K{\_sat\_}\F32\K{\_s}` :math:`\hex{FC}~\hex{00}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_sat\_}\F32\K{\_u}` :math:`\hex{FC}~\hex{01}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_sat\_}\F64\K{\_s}` :math:`\hex{FC}~\hex{02}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_sat\_}\F64\K{\_u}` :math:`\hex{FC}~\hex{03}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_sat\_}\F32\K{\_s}` :math:`\hex{FC}~\hex{04}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_sat\_}\F32\K{\_u}` :math:`\hex{FC}~\hex{05}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_sat\_}\F64\K{\_s}` :math:`\hex{FC}~\hex{06}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_sat\_}\F64\K{\_u}` :math:`\hex{FC}~\hex{07}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\MEMORYINIT~x` :math:`\hex{FC}~\hex{08}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\DATADROP~x` :math:`\hex{FC}~\hex{09}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` -:math:`\MEMORYCOPY` :math:`\hex{FC}~\hex{0A}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\MEMORYFILL` :math:`\hex{FC}~\hex{0B}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\TABLEINIT~x~y` :math:`\hex{FC}~\hex{0C}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\ELEMDROP~x` :math:`\hex{FC}~\hex{0D}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` -:math:`\TABLECOPY~x~y` :math:`\hex{FC}~\hex{0E}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\TABLEGROW~x` :math:`\hex{FC}~\hex{0F}` :math:`[t~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\TABLESIZE~x` :math:`\hex{FC}~\hex{10}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\TABLEFILL~x` :math:`\hex{FC}~\hex{11}` :math:`[\I32~t~\I32] \to []` :ref:`validation ` :ref:`execution ` -========================================= ========================= ============================================= ======================================= =============================================================== +========================================= ========================= =============================================================== ========================================= =============================================================== +Instruction Binary Opcode Type Validation Execution +========================================= ========================= =============================================================== ========================================= =============================================================== +:math:`\UNREACHABLE` :math:`\hex{00}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\NOP` :math:`\hex{01}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` +:math:`\BLOCK~\X{bt}` :math:`\hex{02}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\LOOP~\X{bt}` :math:`\hex{03}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\IF~\X{bt}` :math:`\hex{04}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\ELSE` :math:`\hex{05}` +(reserved) :math:`\hex{06}` +(reserved) :math:`\hex{07}` +(reserved) :math:`\hex{08}` +(reserved) :math:`\hex{09}` +(reserved) :math:`\hex{0A}` +:math:`\END` :math:`\hex{0B}` +:math:`\BR~l` :math:`\hex{0C}` :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\BRIF~l` :math:`\hex{0D}` :math:`[t^\ast~\I32] \to [t^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\BRTABLE~l^\ast~l` :math:`\hex{0E}` :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\RETURN` :math:`\hex{0F}` :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\CALL~x` :math:`\hex{10}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\CALLINDIRECT~x~y` :math:`\hex{11}` :math:`[t_1^\ast~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{12}` +(reserved) :math:`\hex{13}` +:math:`\CALLREF` :math:`\hex{14}` :math:`[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{15}` +(reserved) :math:`\hex{16}` +(reserved) :math:`\hex{17}` +(reserved) :math:`\hex{18}` +(reserved) :math:`\hex{19}` +:math:`\DROP` :math:`\hex{1A}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` +:math:`\SELECT` :math:`\hex{1B}` :math:`[t~t~\I32] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\SELECT~t` :math:`\hex{1C}` :math:`[t~t~\I32] \to [t]` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{1D}` +(reserved) :math:`\hex{1E}` +(reserved) :math:`\hex{1F}` +:math:`\LOCALGET~x` :math:`\hex{20}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\LOCALSET~x` :math:`\hex{21}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` +:math:`\LOCALTEE~x` :math:`\hex{22}` :math:`[t] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\GLOBALGET~x` :math:`\hex{23}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\GLOBALSET~x` :math:`\hex{24}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` +:math:`\TABLEGET~x` :math:`\hex{25}` :math:`[\I32] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\TABLESET~x` :math:`\hex{26}` :math:`[\I32~t] \to []` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{27}` +:math:`\I32.\LOAD~\memarg` :math:`\hex{28}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD~\memarg` :math:`\hex{29}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\F32.\LOAD~\memarg` :math:`\hex{2A}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution ` +:math:`\F64.\LOAD~\memarg` :math:`\hex{2B}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\LOAD\K{8\_s}~\memarg` :math:`\hex{2C}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\LOAD\K{8\_u}~\memarg` :math:`\hex{2D}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\LOAD\K{16\_s}~\memarg` :math:`\hex{2E}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\LOAD\K{16\_u}~\memarg` :math:`\hex{2F}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{8\_s}~\memarg` :math:`\hex{30}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{8\_u}~\memarg` :math:`\hex{31}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{16\_s}~\memarg` :math:`\hex{32}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{16\_u}~\memarg` :math:`\hex{33}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{32\_s}~\memarg` :math:`\hex{34}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{32\_u}~\memarg` :math:`\hex{35}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\STORE~\memarg` :math:`\hex{36}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I64.\STORE~\memarg` :math:`\hex{37}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\F32.\STORE~\memarg` :math:`\hex{38}` :math:`[\I32~\F32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\F64.\STORE~\memarg` :math:`\hex{39}` :math:`[\I32~\F64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I32.\STORE\K{8}~\memarg` :math:`\hex{3A}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I32.\STORE\K{16}~\memarg` :math:`\hex{3B}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I64.\STORE\K{8}~\memarg` :math:`\hex{3C}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I64.\STORE\K{16}~\memarg` :math:`\hex{3D}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I64.\STORE\K{32}~\memarg` :math:`\hex{3E}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\MEMORYSIZE` :math:`\hex{3F}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\MEMORYGROW` :math:`\hex{40}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\CONST~\i32` :math:`\hex{41}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\CONST~\i64` :math:`\hex{42}` :math:`[] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\F32.\CONST~\f32` :math:`\hex{43}` :math:`[] \to [\F32]` :ref:`validation ` :ref:`execution ` +:math:`\F64.\CONST~\f64` :math:`\hex{44}` :math:`[] \to [\F64]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\EQZ` :math:`\hex{45}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\EQ` :math:`\hex{46}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\NE` :math:`\hex{47}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\LT\K{\_s}` :math:`\hex{48}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\LT\K{\_u}` :math:`\hex{49}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\GT\K{\_s}` :math:`\hex{4A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\GT\K{\_u}` :math:`\hex{4B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\LE\K{\_s}` :math:`\hex{4C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\LE\K{\_u}` :math:`\hex{4D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\GE\K{\_s}` :math:`\hex{4E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\GE\K{\_u}` :math:`\hex{4F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EQZ` :math:`\hex{50}` :math:`[\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EQ` :math:`\hex{51}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\NE` :math:`\hex{52}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\LT\K{\_s}` :math:`\hex{53}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\LT\K{\_u}` :math:`\hex{54}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\GT\K{\_s}` :math:`\hex{55}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\GT\K{\_u}` :math:`\hex{56}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\LE\K{\_s}` :math:`\hex{57}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\LE\K{\_u}` :math:`\hex{58}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\GE\K{\_s}` :math:`\hex{59}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\GE\K{\_u}` :math:`\hex{5A}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\EQ` :math:`\hex{5B}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\NE` :math:`\hex{5C}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\LT` :math:`\hex{5D}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\GT` :math:`\hex{5E}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\LE` :math:`\hex{5F}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\GE` :math:`\hex{60}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\EQ` :math:`\hex{61}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\NE` :math:`\hex{62}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\LT` :math:`\hex{63}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\GT` :math:`\hex{64}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\LE` :math:`\hex{65}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\GE` :math:`\hex{66}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\CLZ` :math:`\hex{67}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\CTZ` :math:`\hex{68}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\POPCNT` :math:`\hex{69}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\ADD` :math:`\hex{6A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\SUB` :math:`\hex{6B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\MUL` :math:`\hex{6C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\DIV\K{\_s}` :math:`\hex{6D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\DIV\K{\_u}` :math:`\hex{6E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\REM\K{\_s}` :math:`\hex{6F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\REM\K{\_u}` :math:`\hex{70}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\AND` :math:`\hex{71}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\OR` :math:`\hex{72}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\XOR` :math:`\hex{73}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\SHL` :math:`\hex{74}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\SHR\K{\_s}` :math:`\hex{75}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\SHR\K{\_u}` :math:`\hex{76}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\ROTL` :math:`\hex{77}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\ROTR` :math:`\hex{78}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\CLZ` :math:`\hex{79}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\CTZ` :math:`\hex{7A}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\POPCNT` :math:`\hex{7B}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\ADD` :math:`\hex{7C}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\SUB` :math:`\hex{7D}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\MUL` :math:`\hex{7E}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\DIV\K{\_s}` :math:`\hex{7F}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\DIV\K{\_u}` :math:`\hex{80}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\REM\K{\_s}` :math:`\hex{81}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\REM\K{\_u}` :math:`\hex{82}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\AND` :math:`\hex{83}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\OR` :math:`\hex{84}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\XOR` :math:`\hex{85}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\SHL` :math:`\hex{86}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\SHR\K{\_s}` :math:`\hex{87}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\SHR\K{\_u}` :math:`\hex{88}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\ROTL` :math:`\hex{89}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\ROTR` :math:`\hex{8A}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\ABS` :math:`\hex{8B}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\NEG` :math:`\hex{8C}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CEIL` :math:`\hex{8D}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\FLOOR` :math:`\hex{8E}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\TRUNC` :math:`\hex{8F}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\NEAREST` :math:`\hex{90}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\SQRT` :math:`\hex{91}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\ADD` :math:`\hex{92}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\SUB` :math:`\hex{93}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\MUL` :math:`\hex{94}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\DIV` :math:`\hex{95}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\FMIN` :math:`\hex{96}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\FMAX` :math:`\hex{97}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\COPYSIGN` :math:`\hex{98}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\ABS` :math:`\hex{99}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\NEG` :math:`\hex{9A}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CEIL` :math:`\hex{9B}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\FLOOR` :math:`\hex{9C}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\TRUNC` :math:`\hex{9D}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\NEAREST` :math:`\hex{9E}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\SQRT` :math:`\hex{9F}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\ADD` :math:`\hex{A0}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\SUB` :math:`\hex{A1}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\MUL` :math:`\hex{A2}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\DIV` :math:`\hex{A3}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\FMIN` :math:`\hex{A4}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\FMAX` :math:`\hex{A5}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\COPYSIGN` :math:`\hex{A6}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\WRAP\K{\_}\I64` :math:`\hex{A7}` :math:`[\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_}\F32\K{\_s}` :math:`\hex{A8}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_}\F32\K{\_u}` :math:`\hex{A9}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_}\F64\K{\_s}` :math:`\hex{AA}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_}\F64\K{\_u}` :math:`\hex{AB}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{\_}\I32\K{\_s}` :math:`\hex{AC}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{\_}\I32\K{\_u}` :math:`\hex{AD}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_}\F32\K{\_s}` :math:`\hex{AE}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_}\F32\K{\_u}` :math:`\hex{AF}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_}\F64\K{\_s}` :math:`\hex{B0}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_}\F64\K{\_u}` :math:`\hex{B1}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_}\I32\K{\_s}` :math:`\hex{B2}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_}\I32\K{\_u}` :math:`\hex{B3}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_}\I64\K{\_s}` :math:`\hex{B4}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_}\I64\K{\_u}` :math:`\hex{B5}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\DEMOTE\K{\_}\F64` :math:`\hex{B6}` :math:`[\F64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_}\I32\K{\_s}` :math:`\hex{B7}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_}\I32\K{\_u}` :math:`\hex{B8}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_}\I64\K{\_s}` :math:`\hex{B9}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_}\I64\K{\_u}` :math:`\hex{BA}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\PROMOTE\K{\_}\F32` :math:`\hex{BB}` :math:`[\F32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\REINTERPRET\K{\_}\F32` :math:`\hex{BC}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\REINTERPRET\K{\_}\F64` :math:`\hex{BD}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\REINTERPRET\K{\_}\I32` :math:`\hex{BE}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\REINTERPRET\K{\_}\I64` :math:`\hex{BF}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\EXTEND\K{8\_s}` :math:`\hex{C0}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\EXTEND\K{16\_s}` :math:`\hex{C1}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{8\_s}` :math:`\hex{C2}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{16\_s}` :math:`\hex{C3}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{32\_s}` :math:`\hex{C4}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +(reserved) :math:`\hex{C5}` +(reserved) :math:`\hex{C6}` +(reserved) :math:`\hex{C7}` +(reserved) :math:`\hex{C8}` +(reserved) :math:`\hex{C9}` +(reserved) :math:`\hex{CA}` +(reserved) :math:`\hex{CB}` +(reserved) :math:`\hex{CC}` +(reserved) :math:`\hex{CD}` +(reserved) :math:`\hex{CE}` +(reserved) :math:`\hex{CF}` +:math:`\REFNULL~\X{ht}` :math:`\hex{D0}` :math:`[] \to [(\REF~\NULL~\X{ht})]` :ref:`validation ` :ref:`execution ` +:math:`\REFISNULL` :math:`\hex{D1}` :math:`[(\REF~\NULL~\X{ht})] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\REFFUNC~x` :math:`\hex{D2}` :math:`[] \to [\FUNCREF]` :ref:`validation ` :ref:`execution ` +:math:`\REFASNONNULL` :math:`\hex{D3}` :math:`[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]` :ref:`validation ` :ref:`execution ` +:math:`\BRONNULL~l` :math:`\hex{D4}` :math:`[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{D5}` +:math:`\BRONNONNULL~l` :math:`\hex{D6}` :math:`[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast]` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{D7}` +(reserved) :math:`\hex{D8}` +(reserved) :math:`\hex{D9}` +(reserved) :math:`\hex{DA}` +(reserved) :math:`\hex{DB}` +(reserved) :math:`\hex{DC}` +(reserved) :math:`\hex{DD}` +(reserved) :math:`\hex{DE}` +(reserved) :math:`\hex{DF}` +(reserved) :math:`\hex{E0}` +(reserved) :math:`\hex{E1}` +(reserved) :math:`\hex{E2}` +(reserved) :math:`\hex{E3}` +(reserved) :math:`\hex{E4}` +(reserved) :math:`\hex{E5}` +(reserved) :math:`\hex{E6}` +(reserved) :math:`\hex{E7}` +(reserved) :math:`\hex{E8}` +(reserved) :math:`\hex{E9}` +(reserved) :math:`\hex{EA}` +(reserved) :math:`\hex{EB}` +(reserved) :math:`\hex{EC}` +(reserved) :math:`\hex{ED}` +(reserved) :math:`\hex{EE}` +(reserved) :math:`\hex{EF}` +(reserved) :math:`\hex{F0}` +(reserved) :math:`\hex{F1}` +(reserved) :math:`\hex{F2}` +(reserved) :math:`\hex{F3}` +(reserved) :math:`\hex{F4}` +(reserved) :math:`\hex{F5}` +(reserved) :math:`\hex{F6}` +(reserved) :math:`\hex{F7}` +(reserved) :math:`\hex{F8}` +(reserved) :math:`\hex{F9}` +(reserved) :math:`\hex{FA}` +(reserved) :math:`\hex{FB}` +:math:`\I32.\TRUNC\K{\_sat\_}\F32\K{\_s}` :math:`\hex{FC}~\hex{00}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_sat\_}\F32\K{\_u}` :math:`\hex{FC}~\hex{01}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_sat\_}\F64\K{\_s}` :math:`\hex{FC}~\hex{02}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_sat\_}\F64\K{\_u}` :math:`\hex{FC}~\hex{03}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_sat\_}\F32\K{\_s}` :math:`\hex{FC}~\hex{04}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_sat\_}\F32\K{\_u}` :math:`\hex{FC}~\hex{05}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_sat\_}\F64\K{\_s}` :math:`\hex{FC}~\hex{06}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_sat\_}\F64\K{\_u}` :math:`\hex{FC}~\hex{07}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\MEMORYINIT~x` :math:`\hex{FC}~\hex{08}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\DATADROP~x` :math:`\hex{FC}~\hex{09}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` +:math:`\MEMORYCOPY` :math:`\hex{FC}~\hex{0A}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\MEMORYFILL` :math:`\hex{FC}~\hex{0B}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\TABLEINIT~x~y` :math:`\hex{FC}~\hex{0C}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\ELEMDROP~x` :math:`\hex{FC}~\hex{0D}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` +:math:`\TABLECOPY~x~y` :math:`\hex{FC}~\hex{0E}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\TABLEGROW~x` :math:`\hex{FC}~\hex{0F}` :math:`[t~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\TABLESIZE~x` :math:`\hex{FC}~\hex{10}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\TABLEFILL~x` :math:`\hex{FC}~\hex{11}` :math:`[\I32~t~\I32] \to []` :ref:`validation ` :ref:`execution ` +========================================= ========================= =============================================================== ========================================= =============================================================== diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 9da4e188..f6e8051f 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -34,8 +34,11 @@ Control Instructions .. _binary-br: .. _binary-br_if: .. _binary-br_table: +.. _binary-br_on_null: +.. _binary-br_on_non_null: .. _binary-return: .. _binary-call: +.. _binary-call_ref: .. _binary-call_indirect: .. math:: @@ -62,7 +65,10 @@ Control Instructions &\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|& \hex{0F} &\Rightarrow& \RETURN \\ &&|& \hex{10}~~x{:}\Bfuncidx &\Rightarrow& \CALL~x \\ &&|& - \hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\ + \hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\ &&|& + \hex{14}~~x{:}\Bfuncidx &\Rightarrow& \CALLREF \\ &&|& + \hex{D4}~~x{:}\Bfuncidx &\Rightarrow& \BRONNULL \\ &&|& + \hex{D6}~~x{:}\Bfuncidx &\Rightarrow& \BRONNONNULL \\ \end{array} .. note:: @@ -82,14 +88,17 @@ Reference Instructions :ref:`Reference instructions ` are represented by single byte codes. .. _binary-ref.null: -.. _binary-ref.isnull: +.. _binary-ref.func: +.. _binary-ref.is_null: +.. _binary-ref.as_non_null: .. math:: \begin{array}{llclll} \production{instruction} & \Binstr &::=& \dots \\ &&|& \hex{D0}~~t{:}\Bheaptype &\Rightarrow& \REFNULL~t \\ &&|& \hex{D1} &\Rightarrow& \REFISNULL \\ &&|& - \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\ + \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\ &&|& + \hex{D3} &\Rightarrow& \REFASNONNULL \\ \end{array} diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 6f4c7dc7..2872970b 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -192,15 +192,35 @@ Reference Instructions .. _exec-ref.null: -:math:`\REFNULL~t` -.................. +:math:`\REFNULL~\X{ht}` +....................... -1. Push the value :math:`\REFNULL~t` to the stack. +1. Push the value :math:`\REFNULL~\X{ht}` to the stack. .. note:: No formal reduction rule is required for this instruction, since the |REFNULL| instruction is already a :ref:`value `. +.. _exec-ref.func: + +:math:`\REFFUNC~x` +.................. + +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIFUNCS[x]` exists. + +3. Let :math:`a` be the :ref:`function address ` :math:`F.\AMODULE.\MIFUNCS[x]`. + +4. Push the value :math:`\REFFUNCADDR~a` to the stack. + +.. math:: + \begin{array}{lcl@{\qquad}l} + F; \REFFUNC~x &\stepto& F; \REFFUNCADDR~a + & (\iff a = F.\AMODULE.\MIFUNCS[x]) \\ + \end{array} + + .. _exec-ref.is_null: :math:`\REFISNULL` @@ -210,7 +230,7 @@ Reference Instructions 2. Pop the value :math:`\val` from the stack. -3. If :math:`\val` is :math:`\REFNULL~t`, then: +3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then: a. Push the value :math:`\I32.\CONST~1` to the stack. @@ -221,29 +241,33 @@ Reference Instructions .. math:: \begin{array}{lcl@{\qquad}l} \val~\REFISNULL &\stepto& \I32.\CONST~1 - & (\iff \val = \REFNULL~t) \\ + & (\iff \val = \REFNULL~\X{ht}) \\ \val~\REFISNULL &\stepto& \I32.\CONST~0 & (\otherwise) \\ \end{array} -.. _exec-ref.func: +.. _exec-ref.as_non_null: -:math:`\REFFUNC~x` -.................. +:math:`\REFASNONNULL` +..................... -1. Let :math:`F` be the :ref:`current ` :ref:`frame `. +1. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. -2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIFUNCS[x]` exists. +2. Pop the value :math:`\val` from the stack. -3. Let :math:`a` be the :ref:`function address ` :math:`F.\AMODULE.\MIFUNCS[x]`. +3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then: -4. Push the value :math:`\REFFUNCADDR~a` to the stack. + a. Trap. + +4. Push the value :math:`\val` back to the stack. .. math:: \begin{array}{lcl@{\qquad}l} - F; \REFFUNC~x &\stepto& F; \REFFUNCADDR~a - & (\iff a = F.\AMODULE.\MIFUNCS[x]) \\ + \val~\REFASNONNULL &\stepto& \TRAP + & (\iff \val = \REFNULL~\X{ht}) \\ + \val~\REFASNONNULL &\stepto& \val + & (\otherwise) \\ \end{array} @@ -1722,6 +1746,60 @@ Control Instructions \end{array} +.. _exec-br_on_null: + +:math:`\BRONNULL~l` +................... + +1. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. + +2. Pop the value :math:`\val` from the stack. + +3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then: + + a. :ref:`Execute ` the instruction :math:`(\BR~l)`. + +4. Else: + + a. Push the value :math:`\val` back to the stack. + +.. math:: + \begin{array}{lcl@{\qquad}l} + \val~(\BRONNULL~l) &\stepto& (\BR~l) + & (\iff \val = \REFNULL~\X{ht}) \\ + \val~(\BRONNULL~l) &\stepto& \val + & (\otherwise) \\ + \end{array} + + +.. _exec-br_on_non_null: + +:math:`\BRONNONNULL~l` +...................... + +1. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. + +2. Pop the value :math:`\val` from the stack. + +3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then: + + a. Do nothing. + +4. Else: + + a. Push the value :math:`\val` back to the stack. + + b. :ref:`Execute ` the instruction :math:`(\BR~l)`. + +.. math:: + \begin{array}{lcl@{\qquad}l} + \val~(\BRONNONNULL~l) &\stepto& \epsilon + & (\iff \val = \REFNULL~\X{ht}) \\ + \val~(\BRONNONNULL~l) &\stepto& \val~(\BR~l) + & (\otherwise) \\ + \end{array} + + .. _exec-return: :math:`\RETURN` @@ -1776,6 +1854,23 @@ Control Instructions \end{array} +.. _exec-call_ref: + +:math:`\CALLREF` +................ + +1. Assert: due to :ref:`validation `, a :ref:`function reference ` is on the top of the stack. + +2. Pop the value :math:`\REFFUNCADDR~a` from the stack. + +3. :ref:`Invoke ` the function instance at address :math:`a`. + +.. math:: + \begin{array}{lcl@{\qquad}l} + F; (\REFFUNCADDR~a)~\CALLREF &\stepto& F; (\INVOKE~a) + \end{array} + + .. _exec-call_indirect: :math:`\CALLINDIRECT~x~y` @@ -1805,7 +1900,7 @@ Control Instructions 11. Let :math:`r` be the :ref:`reference ` :math:`\X{tab}.\TIELEM[i]`. -12. If :math:`r` is :math:`\REFNULL~t`, then: +12. If :math:`r` is :math:`\REFNULL~\X{ht}`, then: a. Trap. diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 67bc409e..3bebe174 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -174,8 +174,9 @@ Occasionally, it is convenient to group operators together according to the foll .. index:: ! reference instruction, reference, null pair: abstract syntax; instruction .. _syntax-ref.null: -.. _syntax-ref.is_null: .. _syntax-ref.func: +.. _syntax-ref.is_null: +.. _syntax-ref.as_non_null: .. _syntax-instr-ref: Reference Instructions @@ -188,11 +189,13 @@ Instructions in this group are concerned with accessing :ref:`references ` value, produce a reference to a given function, or check for a null value, respectively. +The |REFASNONNULL| casts a :ref:`nullable ` to a non-null one, and :ref:`traps ` if it encounters null. .. index:: ! parametric instruction, value type @@ -389,8 +392,11 @@ Instructions in this group affect the flow of control. \BR~\labelidx \\&&|& \BRIF~\labelidx \\&&|& \BRTABLE~\vec(\labelidx)~\labelidx \\&&|& + \BRONNULL~\labelidx \\&&|& + \BRONNONNULL~\labelidx \\&&|& \RETURN \\&&|& \CALL~\funcidx \\&&|& + \CALLREF \\&&|& \CALLINDIRECT~\tableidx~\typeidx \\ \end{array} @@ -427,6 +433,7 @@ Branch instructions come in several flavors: |BR| performs an unconditional branch, |BRIF| performs a conditional branch, and |BRTABLE| performs an indirect branch through an operand indexing into the label vector that is an immediate to the instruction, or to a default target if the operand is out of bounds. +The |BRONNULL| and |BRONNONNULL| instructions check whether a reference operand is :ref:`null ` and branch if that is the case or not the case, respectively. The |RETURN| instruction is a shortcut for an unconditional branch to the outermost block, which implicitly is the body of the current function. Taking a branch *unwinds* the operand stack up to the height where the targeted structured control instruction was entered. However, branches may additionally consume operands themselves, which they push back on the operand stack after unwinding. @@ -434,6 +441,7 @@ Forward branches require operands according to the output of the targeted block' Backward branches require operands according to the input of the targeted block's type, i.e., represent the values consumed by the restarted block. The |CALL| instruction invokes another :ref:`function `, consuming the necessary arguments from the stack and returning the result values of the call. +The |CALLREF| instruction invokes a function indirectly through a :ref:`function reference ` operand. The |CALLINDIRECT| instruction calls a function indirectly through an operand indexing into a :ref:`table ` that is denoted by a :ref:`table index ` and must contain :ref:`function references `. Since it may contain functions of heterogeneous type, the callee is dynamically checked against the :ref:`function type ` indexed by the instruction's second immediate, and the call is aborted with a :ref:`trap ` if it does not match. diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 0c350d00..d116523d 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -95,8 +95,11 @@ However, the special case of a type use that is syntactically empty or consists .. _text-br: .. _text-br_if: .. _text-br_table: +.. _text-br_on_null: +.. _text-br_on_non_null: .. _text-return: .. _text-call: +.. _text-call_ref: .. _text-call_indirect: All other control instruction are represented verbatim. @@ -110,8 +113,11 @@ All other control instruction are represented verbatim. \text{br\_if}~~l{:}\Tlabelidx_I &\Rightarrow& \BRIF~l \\ &&|& \text{br\_table}~~l^\ast{:}\Tvec(\Tlabelidx_I)~~l_N{:}\Tlabelidx_I &\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|& + \text{br\_on\_null}~~l{:}\Tlabelidx_I &\Rightarrow& \BRONNULL~l \\ &&|& + \text{br\_on\_non\_null}~~l{:}\Tlabelidx_I &\Rightarrow& \BRONNONNULL~l \\ &&|& \text{return} &\Rightarrow& \RETURN \\ &&|& \text{call}~~x{:}\Tfuncidx_I &\Rightarrow& \CALL~x \\ &&|& + \text{call\_ref} &\Rightarrow& \CALLREF \\ &&|& \text{call\_indirect}~~x{:}\Ttableidx~~y,I'{:}\Ttypeuse_I &\Rightarrow& \CALLINDIRECT~x~y & (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\ \end{array} @@ -152,15 +158,17 @@ Reference Instructions ~~~~~~~~~~~~~~~~~~~~~~ .. _text-ref.null: -.. _text-ref.is_null: .. _text-ref.func: +.. _text-ref.is_null: +.. _text-ref.as_non_null: .. math:: \begin{array}{llclll} \production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|& \text{ref.null}~~t{:}\Theaptype &\Rightarrow& \REFNULL~t \\ &&|& - \text{ref.is\_null} &\Rightarrow& \REFISNULL \\ &&|& \text{ref.func}~~x{:}\Tfuncidx &\Rightarrow& \REFFUNC~x \\ &&|& + \text{ref.is\_null} &\Rightarrow& \REFISNULL \\ &&|& + \text{ref.as\_non\_null} &\Rightarrow& \REFASNONNULL \\ \end{array} diff --git a/document/core/util/macros.def b/document/core/util/macros.def index dd900bcd..24e07740 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -351,8 +351,11 @@ .. |BR| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br}} .. |BRIF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_if}} .. |BRTABLE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_table}} +.. |BRONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_null}} +.. |BRONNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_non\_null}} .. |RETURN| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return}} .. |CALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call}} +.. |CALLREF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_ref}} .. |CALLINDIRECT| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_indirect}} .. |DROP| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{drop}} @@ -383,8 +386,9 @@ .. |DATADROP| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{data.drop}} .. |REFNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}null}} -.. |REFISNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}is\_null}} .. |REFFUNC| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}func}} +.. |REFISNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}is\_null}} +.. |REFASNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}as\_non\_null}} .. |CONST| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{const}} .. |EQZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eqz}} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 89c0c21e..22d6647e 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -166,32 +166,18 @@ Reference Instructions .. _valid-ref.null: -:math:`\REFNULL~t` -.................. - -* The instruction is valid with type :math:`[] \to [t]`. - -.. math:: - \frac{ - }{ - C \vdashinstr \REFNULL~t : [] \to [t] - } +:math:`\REFNULL~\X{ht}` +....................... -.. note:: - In future versions of WebAssembly, there may be reference types for which no null reference is allowed. +* The :ref:`heap type ` :math:`\X{ht}` must be :ref:`valid `. -.. _valid-ref.is_null: - -:math:`\REFISNULL` -.................. - -* The instruction is valid with type :math:`[t] \to [\I32]`, for any :ref:`reference type ` :math:`t`. +* Then the instruction is valid with type :math:`[] \to [(\REF~\NULL~\X{ht})]`. .. math:: \frac{ - t = \reftype + C \vdashheaptype \X{ht} \ok }{ - C \vdashinstr \REFISNULL : [t] \to [\I32] + C \vdashinstr \REFNULL~\X{ht} : [] \to [(\REF~\NULL~\X{ht})] } .. _valid-ref.func: @@ -214,6 +200,34 @@ Reference Instructions C \vdashinstr \REFFUNC~x : [] \to [\FUNCREF] } +.. _valid-ref.is_null: + +:math:`\REFISNULL` +.................. + +* The instruction is valid with type :math:`[(\REF~\NULL~\X{ht})] \to [\I32]`, for any :ref:`valid ` :ref:`heap type ` :math:`\X{ht}`. + +.. math:: + \frac{ + C \vdashheaptype \X{ht} \ok + }{ + C \vdashinstr \REFISNULL : [(\REF~\NULL~\X{ht})] \to [\I32] + } + +.. _valid-ref.as_non_null: + +:math:`\REFASNONNULL` +..................... + +* The instruction is valid with type :math:`[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]`, for any :ref:`valid ` :ref:`heap type ` :math:`\X{ht}`. + +.. math:: + \frac{ + C \vdashheaptype \X{ht} \ok + }{ + C \vdashinstr \REFASNONNULL : [(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})] + } + .. index:: parametric instructions, value type, polymorphism pair: validation; instruction @@ -228,10 +242,11 @@ Parametric Instructions :math:`\DROP` ............. -* The instruction is valid with type :math:`[t] \to []`, for any :ref:`value type ` :math:`t`. +* The instruction is valid with type :math:`[t] \to []`, for any :ref:`valid ` :ref:`value type ` :math:`t`. .. math:: \frac{ + C \vdashvaltype t \ok }{ C \vdashinstr \DROP : [t] \to [] } @@ -973,6 +988,52 @@ Control Instructions a simple :ref:`linear algorithm ` does not require this. +.. _valid-br_on_null: + +:math:`\BRONNULL~l` +................... + +* The label :math:`C.\CLABELS[l]` must be defined in the context. + +* Let :math:`[t^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. + +* Then the instruction is valid with type :math:`[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]` for any :ref:`valid ` :ref:`heap type ` :math:`\X{ht}`. + +.. math:: + \frac{ + C.\CLABELS[l] = [t^\ast] + \qquad + C \vdashheaptype \X{ht} \ok + }{ + C \vdashinstr \BRONNULL~l : [t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})] + } + + +.. _valid-br_on_non_null: + +:math:`\BRONNONNULL~l` +...................... + +* The label :math:`C.\CLABELS[l]` must be defined in the context. + +* Let :math:`[{t'}^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. + +* The result type :math:`[{t'}^\ast]` must contain at least one type. + +* Let the :ref:`value type ` :math:`t_l` be the last element in the sequence :math:`{t'}^\ast`, and :math:`[t^\ast]` the remainder of the sequence preceding it. + +* The value type :math:`t_l` must be a reference type of the form :math:`\REF~\NULL^?~\X{ht}`. + +* Then the instruction is valid with type :math:`[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast]`. + +.. math:: + \frac{ + C.\CLABELS[l] = [t^\ast~(\REF~\X{ht})] + }{ + C \vdashinstr \BRONNONNULL~l : [t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast] + } + + .. _valid-return: :math:`\RETURN` @@ -1018,6 +1079,23 @@ Control Instructions } +.. _valid-call_ref: + +:math:`\CALLREF` +................ + +* Let :math:`x` be some :ref:`type index ` for which :math:`C.\CTYPES[x]` is a :ref:`function type ` of the form :math:`[t_1^\ast] \to [t_2^\ast]`. + +* Then the instruction is valid with type :math:`[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]`. + +.. math:: + \frac{ + C.\CTYPES[x] = [t_1^\ast] \to [t_2^\ast] + }{ + C \vdashinstr \CALLREF : [t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast] + } + + .. _valid-call_indirect: :math:`\CALLINDIRECT~x~y` diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md index 7d08ed54..36dc946d 100644 --- a/proposals/function-references/Overview.md +++ b/proposals/function-references/Overview.md @@ -168,7 +168,7 @@ The following rules, now defined in terms of heap types, replace and extend the - `(ref ) <: (ref null )` - iff ` <: ` -##### Constructed Types +##### Heap Types * Any function type is a subtype of `func` - `$t <: func` From 5e694c9148f9cb116b534a20cdb6a5251e628ad7 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 28 Jun 2021 15:54:22 +0200 Subject: [PATCH 2/5] [spec] Fix a bunch of minor editorial issues (#1338) --- document/core/binary/instructions.rst | 3 ++- document/core/binary/types.rst | 4 ++-- document/core/exec/instructions.rst | 4 ++-- document/core/syntax/instructions.rst | 10 +++++----- document/core/text/instructions.rst | 6 +++--- document/core/util/macros.def | 2 +- document/core/valid/instructions.rst | 6 +++--- 7 files changed, 18 insertions(+), 17 deletions(-) diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index d6a60d83..26e0b8fc 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -82,7 +82,8 @@ Reference Instructions :ref:`Reference instructions ` are represented by single byte codes. .. _binary-ref.null: -.. _binary-ref.isnull: +.. _binary-ref.func: +.. _binary-ref.is_null: .. math:: \begin{array}{llclll} diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index 7c462e02..0d1dfec8 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -6,8 +6,8 @@ Types ----- .. note:: - In future versions of WebAssembly, value types may include types denoted by :ref:`type indices `. - Thus, the binary format for types corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, so that they can coexist with (positive) type indices in the future. + In some places, possible types include both type constructors or types denoted by :ref:`type indices `. + Thus, the binary format for type constructors corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, such that they can unambiguously occur in the same place as (positive) type indices. .. index:: number type diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 6f4c7dc7..78c43da7 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -978,7 +978,7 @@ Memory Instructions 9. If :math:`N` is not part of the instruction, then: - a. Let :math:`N` be the :ref:`bit width ` :math:`|t|` of :ref:`value type ` :math:`t`. + a. Let :math:`N` be the :ref:`bit width ` :math:`|t|` of :ref:`number type ` :math:`t`. 10. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: @@ -1058,7 +1058,7 @@ Memory Instructions 11. If :math:`N` is not part of the instruction, then: - a. Let :math:`N` be the :ref:`bit width ` :math:`|t|` of :ref:`value type ` :math:`t`. + a. Let :math:`N` be the :ref:`bit width ` :math:`|t|` of :ref:`number type ` :math:`t`. 12. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 039d4cfb..9c582d64 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -35,7 +35,7 @@ The following sections group instructions into a number of different categories. Numeric Instructions ~~~~~~~~~~~~~~~~~~~~ -Numeric instructions provide basic operations over numeric :ref:`values ` of specific :ref:`type `. +Numeric instructions provide basic operations over numeric :ref:`values ` of specific :ref:`type `. These operations closely match respective operations available in hardware. .. math:: @@ -118,7 +118,7 @@ These operations closely match respective operations available in hardware. \K{ge} \\ \end{array} -Numeric instructions are divided by :ref:`value type `. +Numeric instructions are divided by :ref:`number type `. For each type, several subcategories can be distinguished: * *Constants*: return a static constant. @@ -324,9 +324,9 @@ Instructions in this group are concerned with linear :ref:`memory `. \DATADROP~\dataidx \\ \end{array} -Memory is accessed with |LOAD| and |STORE| instructions for the different :ref:`value types `. +Memory is accessed with |LOAD| and |STORE| instructions for the different :ref:`number types `. They all take a *memory immediate* |memarg| that contains an address *offset* and the expected *alignment* (expressed as the exponent of a power of 2). -Integer loads and stores can optionally specify a *storage size* that is smaller than the :ref:`bit width ` of the respective value type. +Integer loads and stores can optionally specify a *storage size* that is smaller than the :ref:`bit width ` of the respective value type. In the case of loads, a sign extension mode |sx| is then required to select appropriate behavior. The static address offset is added to the dynamic address operand, yielding a 33 bit *effective address* that is the zero-based index at which the memory is accessed. @@ -351,7 +351,7 @@ The |DATADROP| instruction prevents further use of a passive data segment. This This restriction may be lifted in future versions. -.. index:: ! control instruction, ! structured control, ! label, ! block, ! block type, ! branch, ! unwinding, result type, label index, function index, type index, vector, trap, function, table, function type, value type, type index +.. index:: ! control instruction, ! structured control, ! label, ! block, ! block type, ! branch, ! unwinding, stack type, label index, function index, type index, vector, trap, function, table, function type, value type, type index pair: abstract syntax; instruction pair: abstract syntax; block type pair: block; type diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 45c2a059..6112a766 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -74,13 +74,13 @@ However, the special case of a type use that is syntactically empty or consists x,I'{:}\Ttypeuse_I &\Rightarrow& x & (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\ \end{array} \\ \production{block instruction} & \Tblockinstr_I &::=& - \text{block}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? + \text{block}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype_I~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? \\ &&&\qquad \Rightarrow\quad \BLOCK~\X{bt}~\X{in}^\ast~\END \qquad\quad~~ (\iff \Tid^? = \epsilon \vee \Tid^? = \Tlabel) \\ &&|& - \text{loop}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? + \text{loop}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype_I~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? \\ &&&\qquad \Rightarrow\quad \LOOP~\X{bt}~\X{in}^\ast~\END \qquad\qquad (\iff \Tid^? = \epsilon \vee \Tid^? = \Tlabel) \\ &&|& - \text{if}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}_1{:}\Tinstr_{I'})^\ast~~ + \text{if}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype_I~~(\X{in}_1{:}\Tinstr_{I'})^\ast~~ \text{else}~~\Tid_1^?~~(\X{in}_2{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid_2^? \\ &&&\qquad \Rightarrow\quad \IF~\X{bt}~\X{in}_1^\ast~\ELSE~\X{in}_2^\ast~\END \qquad (\iff \Tid_1^? = \epsilon \vee \Tid_1^? = \Tlabel, \Tid_2^? = \epsilon \vee \Tid_2^? = \Tlabel) \\ diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 42b310dd..cd1bf31d 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -308,7 +308,7 @@ .. Modules, non-terminals .. |module| mathdef:: \xref{syntax/modules}{syntax-module}{\X{module}} -.. |type| mathdef:: \xref{syntax/modules}{syntax-typedef}{\X{type}} +.. |type| mathdef:: \xref{syntax/types}{syntax-functype}{\X{type}} .. |func| mathdef:: \xref{syntax/modules}{syntax-func}{\X{func}} .. |table| mathdef:: \xref{syntax/modules}{syntax-table}{\X{table}} .. |mem| mathdef:: \xref{syntax/modules}{syntax-mem}{\X{mem}} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index f329a677..07e4921b 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -599,7 +599,7 @@ Memory Instructions * The memory :math:`C.\CMEMS[0]` must be defined in the context. -* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. +* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. * Then the instruction is valid with type :math:`[\I32] \to [t]`. @@ -639,7 +639,7 @@ Memory Instructions * The memory :math:`C.\CMEMS[0]` must be defined in the context. -* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. +* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. * Then the instruction is valid with type :math:`[\I32~t] \to []`. @@ -1124,7 +1124,7 @@ Expressions :math:`\expr` are classified by :ref:`result types ` with some :ref:`stack type ` :math:`[] \to [t'^\ast]`. +* The instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with some :ref:`stack type ` :math:`[] \to [{t'}^\ast]`. * For each :ref:`operand type ` :math:`t'_i` in :math:`{t'}^\ast` and corresponding :ref:`value type ` type :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches ` :math:`t_i`. From 2e629bc63aad31982d8941a4263e4ecacae00c94 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Fri, 16 Jul 2021 01:32:03 -0700 Subject: [PATCH 3/5] Create Github Actions workflow for CI (#1344) This addresses issue #1342 for spec publishing. The added workflow will run on commit and PRs and will run CI for both reference interpreter build/test and for building the spec documents. It will also publish them to the gh-pages branch. --- .github/workflows/main.yml | 91 +++++++++++++++++++++++ .travis.yml | 38 ---------- README.md | 2 +- deploy_key.enc | Bin 3248 -> 0 bytes document/travis-deploy.sh | 80 -------------------- interpreter/meta/travis/build-test.sh | 10 --- interpreter/meta/travis/install-ocaml.sh | 46 ------------ 7 files changed, 92 insertions(+), 175 deletions(-) create mode 100644 .github/workflows/main.yml delete mode 100644 .travis.yml delete mode 100644 deploy_key.enc delete mode 100755 document/travis-deploy.sh delete mode 100755 interpreter/meta/travis/build-test.sh delete mode 100755 interpreter/meta/travis/install-ocaml.sh diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml new file mode 100644 index 00000000..1386b4c6 --- /dev/null +++ b/.github/workflows/main.yml @@ -0,0 +1,91 @@ +name: CI + +on: + push: + branches: [ master ] + pull_request: + branches: [ master ] + + # Allows you to run this workflow manually from the Actions tab + workflow_dispatch: + +jobs: + ref-interpreter: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v2 + - name: Setup OCaml + uses: ocaml/setup-ocaml@v2 + with: + ocaml-compiler: 4.12.x + - run: opam install --yes ocamlbuild.0.14.0 + - run: cd interpreter && opam exec make all + + build-js-api-spec: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v2 + - name: Build JS API bikeshed + uses: netwerk-digitaal-erfgoed/bikeshed-action@v1 + with: + source: "document/js-api/index.bs" + destination: "document/js-api/index.html" + - uses: actions/upload-artifact@v2 + with: + name: js-api-rendered + path: document/js-api + + build-web-api-spec: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v2 + - name: Build JS API bikeshed + uses: netwerk-digitaal-erfgoed/bikeshed-action@v1 + with: + source: "document/web-api/index.bs" + destination: "document/web-api/index.html" + - uses: actions/upload-artifact@v2 + with: + name: web-api-rendered + path: document/web-api + + build-core-spec: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v2 + with: + submodules: "recursive" + - run: pip install bikeshed && bikeshed update + - run: pip install six + - run: sudo apt-get update -y && sudo apt-get install -y latexmk texlive-latex-recommended texlive-latex-extra texlive-fonts-recommended + - run: pip install sphinx==3.5.2 + - run: cd document/core && make all + - uses: actions/upload-artifact@v2 + with: + name: core-api-rendered + path: document/core/_build/html + + publish-spec: + runs-on: ubuntu-latest + needs: [build-core-spec, build-js-api-spec, build-web-api-spec] + steps: + - uses: actions/checkout@v2 + - run: mkdir _output && cp document/index.html _output/index.html + - uses: actions/download-artifact@v2 + with: + name: js-api-rendered + path: _output/js-api + - uses: actions/download-artifact@v2 + with: + name: web-api-rendered + path: _output/web-api + - uses: actions/download-artifact@v2 + with: + name: core-api-rendered + path: _output/core + - name: Publish HTML to GitHub Pages + if: github.ref == 'refs/heads/master' + uses: peaceiris/actions-gh-pages@v3 + with: + publish_dir: ./_output + github_token: ${{ secrets.GITHUB_TOKEN }} diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index b498e6ce..00000000 --- a/.travis.yml +++ /dev/null @@ -1,38 +0,0 @@ -language: python -python: - - "3.7" -dist: bionic - -addons: - apt: - sources: - - sourceline: 'ppa:avsm/ppa' - - sourceline: 'deb https://dl.yarnpkg.com/debian/ stable main' - key_url: 'https://dl.yarnpkg.com/debian/pubkey.gpg' - update: true - packages: - - opam - - texlive-full - - yarn - -install: - - opam init --auto-setup --compiler=4.07.1 - - eval $(opam env) - - opam --version - - ocaml --version - - opam install --yes ocamlbuild.0.14.0 - - pip install Sphinx==3.5.2 - - git clone https://github.com/tabatkins/bikeshed.git - - pip install --editable $PWD/bikeshed - - bikeshed update - -script: - - ./interpreter/meta/travis/build-test.sh - - bash ./document/travis-deploy.sh - -os: linux - -env: - global: - - ENCRYPTION_LABEL: "304454be9d6c" - - COMMIT_AUTHOR_EMAIL: "noreply@webassembly.org" diff --git a/README.md b/README.md index 83cdc4da..ab9cd995 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -[![Build Status](https://travis-ci.org/WebAssembly/spec.svg?branch=master)](https://travis-ci.org/WebAssembly/spec) +![Build Status](https://github.com/WebAssembly/spec/actions/workflows/main.yml/badge.svg) # spec diff --git a/deploy_key.enc b/deploy_key.enc deleted file mode 100644 index b6d3e2f19771652a9711760b1712a77fe1b4e579..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 3248 zcmV;h3{UeoaMr!6kTNmX>{8Y#<|(CVbO6TJr-;79Ag-eBM!B~g(FTQ5ldW}>C6w#F z7?FSyFeYZ$v_V^lQFEF>+7k9B7m`7vS_SQ$;wWv|QOclL{NpaXb;g5ti(%WUt|3;5 z3CA#OrS)XS){2AUta7q}MSmhTJq zo{c?28()!ibPsqvTfOAA!4zOONU^F*gLcD(DrJbnNphXRZ3yC#LaPJi{CC$C(2A_7 zNaF$Iwo+ftMAzTpRFW1@B>=0mk{V^}DS!4rt3&v*?r8!}EfiTzY#jX?%ckauU9h@W zx(fD`Pk=~T7D1zi5Xgo-F3df<=bCbjU0(ZD&z`12ST)Xxn<2-%!cB^F0IoG~-*{lROB{l$8;> zQYD6uvZB!WjR97=Gm5k(nd?fS-skc&EK?_V8WnS+v(_4N1NbVfWy{T9c3+w+eKW@y z`gzb1V%Tr>ul(ay+I}7y2o4<>nNeC`_9<4dQwbaZcv=lR5j&@)QY$OIg__IEl?CzP zj*w)N-7!X;zax-wu2%HYpX17nK^l2cLppXhM>Q8<9AmF4V+?wF~S-rGWRU;<& zEfi}`>wt%Un_w@H!oNoZ>x+M|o6OWL0ZWAvCDS3ci~T8hKI0BHLyhmaX>a@YdQNK^9SJORstB zfvrm3TfM$`MMQQXp+4m=U~?Y#8>LXJEJKe+QT3ai?lI{90Zbd!SJdk4H(U1tebkQS zElH@QyluL-tMcF~ED_;l>!0Ijv*4gtnDwmLYV{a3@tjZ`D zFgG=OkZ90lfbv6>Fy&2v?b=c~Y_N9G zUi9};vfpk;9dPn4FMkaR{o~nn&h!a-?Sdb%SZ)!fI~GWnk~X{F~0*MZTR*=jmm-h1@t zDL!$f-TC0j9#3k6yGm=yVm`^%@wfi3bq#*03KSe>$d+&xjHOcMc8uJt8)hN2{SBal z4ob$b$`dj=o#p1YnW?UI^yZ;rkMjLI{F#<8G09bp2NC-f7?!MtUZ(JwIdFlSzu%EdX7u+as(dHl z58QQZ`uk&2UcuOD{=l^SW7lbUC)YQxLZoD(4yfjbALj)ocgYIM0ZYz?(TpdH^*N^lP&fD?>5S3l5d9vDe0MYX}=L@v0ac*d^h zMC3X&i8_TGc*nis1+Hbb@FGCYM0^b7+Ks%np4Yi`?%nMjTjK}kiD^peA^u+*e>(aKEP(B~>~mZq#KO^e z%~M*@SsY^h6(tY`GdMou`@})%F*bIbRNZ>mC~Kmlo-i?%UtfW#dT*z*RcdL zpk60TCgJqxKBvX~s$%Shh(AI%*I`@P2!X_@lhC_lv0_yIg6%&*TKAQRPZQNW>=_H-#1pBvjD+m{Zb}zcH8nbpNqr9whn4 zA=y)BHKQ-DrD~ATW$s5sLj-tJ#cf~=mO{+4YNwZc;4(}zeG0i5iXTW*#VVOL90%~C zVKMQHgk?j=XH43>K+-CeY3%JXI)VIB$Ad;DSsk-VJs=GfjP+|s{r){_ozCKbFDNi| zfEk3yUlIo}(x+SiFz(8%;%1%!B5`O|M9Tgg3bui&lu)v`(ydUn{aib=ktlW8MU&;r zQ+2LIr_4e3%GTLQ5?58orh7HmWd&Z&T0Uz!9~Ha`K^gp=fQ`FR=0~z|>MuzT4#e%& zBXJPHh`^tE;|zIgNiR(*kU@PB&}J%3Coh;M^QnC8vP7h%*_Gozd?$RZWr_#dXYF>u zT>^8L;b}KO+gPONfMBv1ae%Hy6R+;S^w+Ng{zo&nGB`o<^fxC>{v`=!WnoSACN9e? z!P}dgK-N^z=5p%- zjAkKdA-dFrZxs{<7wntcycPzJOC})W{%YX>7&0{p8S%XXI0{sJi2me-X!z#kb@^(L zIrTxbTFMXTi!+maqh2OdhC54A&#rQ{4~>UL|6E*af1FP^b#OX~#=VRt;}}z+FhX7& z(?0)PAKjGZ*g(dZNg81514!QK;bQWS0-qDq&xgnv8vdcEkLzW9YdU7Q`jSwWHd*~b zqQ?O;jM%iLY>Zw*$r*lZ~?dz)vtCi6GqzmKd+b z!(zZgpXf?*+wbzsxQ&XJ3)2p#3|IEa$pe0b>QbH=rr|j)yS-i=SFADE7tJ`oCmN@} zL{UA^mr)_ZWdcbz>BGLSKFnFY^oV4EXulUCv6iQUG?d~nuNbxQiWI`F1pbLxAfG^h iY#Pu|2q&8>`3}#6q-2Cz`ZEbT?K&=q;2asiqpF?e?>4gl diff --git a/document/travis-deploy.sh b/document/travis-deploy.sh deleted file mode 100755 index 832d025b..00000000 --- a/document/travis-deploy.sh +++ /dev/null @@ -1,80 +0,0 @@ -#!/bin/bash - -# Adapted from https://github.com/heycam/webidl/blob/master/deploy.sh - -set -e # Exit with nonzero exit code if anything fails - -SOURCE_BRANCH="master" -TARGET_BRANCH="gh-pages" - -function doCompile { - # TODO(littledan): Integrate with document/deploy.sh - (cd document; make) -} - -# Pull requests and commits to other branches shouldn't try to deploy, just build to verify -if [[ "$TRAVIS_PULL_REQUEST" != "false" || "$TRAVIS_BRANCH" != "$SOURCE_BRANCH" ]]; then - echo "Skipping deploy; just doing a build." - doCompile - exit 0 -fi - -# Save some useful information -REPO=`git config remote.origin.url` -SSH_REPO=${REPO/https:\/\/github.com\//git@github.com:} -SHA=`git rev-parse --verify HEAD` - -# Get the deploy key by using Travis's stored variables to decrypt deploy_key.enc -ENCRYPTED_KEY_VAR="encrypted_${ENCRYPTION_LABEL}_key" -ENCRYPTED_IV_VAR="encrypted_${ENCRYPTION_LABEL}_iv" -ENCRYPTED_KEY=${!ENCRYPTED_KEY_VAR} -ENCRYPTED_IV=${!ENCRYPTED_IV_VAR} -openssl aes-256-cbc -K $ENCRYPTED_KEY -iv $ENCRYPTED_IV -in deploy_key.enc -out deploy_key -d || true -chmod 600 deploy_key -eval `ssh-agent -s` -ssh-add deploy_key || true - -# DON'T MOVE ABOVE AS IT WILL REVEAL KEYS! -# Turn on logging from here on. -set -x - -# Clone the existing gh-pages for this repo into _build/ -# Create a new empty branch if gh-pages doesn't exist yet (should only happen -# on first deploy). -# Clean document/*/_build. -(cd document; make clean) -# Ensure no checkout in _build. -rm -rf document/_build -# Clone a second checkout of our repo to _build. -git clone $REPO document/_build -( - # Checkout a parentless branch of gh-pages. - cd document/_build - git checkout $TARGET_BRANCH || git checkout --orphan $TARGET_BRANCH - - # Clean out existing contents (to be replaced with output from the build - # that happens after this). - rm -rf ./* -) - -# Run our compile script (output into _build). -doCompile - -# Set user info on the gh-pages repo in _build. -cd document/_build -git config user.name "Travis CI" -git config user.email "$COMMIT_AUTHOR_EMAIL" - -# If there are no changes to the compiled out (e.g. this is a README update) then just bail. -if [[ -z "$(git status --porcelain)" ]]; then - echo "No changes to the output on this push; exiting." - exit 0 -fi - -# Commit the "changes", i.e. the new version. -# The delta will show diffs between new and old versions. -git add --all . -git commit -m "Deploy to GitHub Pages: ${SHA}" - -# Now that we're all set up, we can push. -git push $SSH_REPO $TARGET_BRANCH diff --git a/interpreter/meta/travis/build-test.sh b/interpreter/meta/travis/build-test.sh deleted file mode 100755 index 622962ca..00000000 --- a/interpreter/meta/travis/build-test.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/bin/bash - -set -e -set -x - -# Move to a location relative to the script so it runs -# from anywhere. -cd $(dirname ${BASH_SOURCE[0]})/../.. - -make all diff --git a/interpreter/meta/travis/install-ocaml.sh b/interpreter/meta/travis/install-ocaml.sh deleted file mode 100755 index fa2c6c4f..00000000 --- a/interpreter/meta/travis/install-ocaml.sh +++ /dev/null @@ -1,46 +0,0 @@ -#!/bin/bash - -set -e - -download_from_gh_archive() { - local project=$1; - local version=$2; - local sha=$3; - - curl https://github.com/ocaml/${project}/archive/${version}.tar.gz -OL - CHECKSUM=$(shasum -a 256 ${version}.tar.gz | awk '{ print $1 }') - if [ ${CHECKSUM} != ${sha} ]; then - echo "Bad checksum ${project} download checksum!" - exit 1 - fi - tar xfz ${version}.tar.gz -} - -# Move to a location relative to the script so it runs -# from anywhere. Go three levels down to get out of interpreter/ -# and into the top-level dir, since we'll run ocamlbuild -# inside of interpreter/ and it goes pear-shaped if it -# encounters ocaml's own build directory. -cd $(dirname ${BASH_SOURCE[0]})/../../.. - -PREFIX=$PWD/ocaml/install - -rm -rf ocaml -mkdir ocaml -cd ocaml -mkdir install - -download_from_gh_archive ocaml 4.05.0 e5d8a6f629020c580473d8afcfcb06c3966d01929f7b734f41dc0c737cd8ea3f -cd ocaml-4.05.0 -./configure -prefix ${PREFIX} -make world.opt -make install -cd .. - -PATH=${PREFIX}/bin:${PATH} - -download_from_gh_archive ocamlbuild 0.11.0 1717edc841c9b98072e410f1b0bc8b84444b4b35ed3b4949ce2bec17c60103ee -cd ocamlbuild-0.11.0 -make configure -make -make install From 887e5de32bff194fd88e3ba5ffee52872764d031 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sat, 24 Jul 2021 14:21:59 +0200 Subject: [PATCH 4/5] Simplify func context --- interpreter/util/lib.ml | 9 +++++++++ interpreter/util/lib.mli | 3 +++ interpreter/valid/valid.ml | 15 +++++++-------- 3 files changed, 19 insertions(+), 8 deletions(-) diff --git a/interpreter/util/lib.ml b/interpreter/util/lib.ml index 23bace33..7becaf1f 100644 --- a/interpreter/util/lib.ml +++ b/interpreter/util/lib.ml @@ -153,6 +153,15 @@ struct and mapi' f i = function | [] -> [] | x::xs -> f i x :: mapi' f (Int32.add i 1l) xs + + let rec index_where p xs = index_where' p xs 0l + and index_where' p xs i = + match xs with + | [] -> None + | x::xs' when p x -> Some i + | x::xs' -> index_where' p xs' (Int32.add i 1l) + + let index_of x = index_where ((=) x) end module Array32 = diff --git a/interpreter/util/lib.mli b/interpreter/util/lib.mli index bde64f1d..1b260443 100644 --- a/interpreter/util/lib.mli +++ b/interpreter/util/lib.mli @@ -37,6 +37,9 @@ sig val take : int32 -> 'a list -> 'a list (* raises Failure *) val drop : int32 -> 'a list -> 'a list (* raises Failure *) val mapi : (int32 -> 'a -> 'b) -> 'a list -> 'b list + + val index_of : 'a -> 'a list -> int32 option + val index_where : ('a -> bool) -> 'a list -> int32 option end module Array32 : diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index f40b46ea..5a47b11f 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -18,7 +18,7 @@ let require b at s = if not b then error at s type context = { types : def_type list; - funcs : syn_var list; + funcs : func_type list; tables : table_type list; memories : memory_type list; globals : global_type list; @@ -42,7 +42,7 @@ let lookup category list x = error x.at ("unknown " ^ category ^ " " ^ I32.to_string_u x.it) let type_ (c : context) x = lookup "type" c.types x -let func_var (c : context) x = lookup "function" c.funcs x +let func (c : context) x = lookup "function" c.funcs x let table (c : context) x = lookup "table" c.tables x let memory (c : context) x = lookup "memory" c.memories x let global (c : context) x = lookup "global" c.globals x @@ -55,8 +55,6 @@ let func_type (c : context) x = match type_ c x with | FuncDefType ft -> ft -let func (c : context) x = func_type c (func_var c x @@ x.at) - let refer category (s : Free.Set.t) x = if not (Free.Set.mem x.it s) then error x.at @@ -534,7 +532,8 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type [RefType (Nullable, t)] --> [RefType (NonNullable, t)] | RefFunc x -> - let y = func_var c x in + let ft = func c x in + let y = Lib.Option.force (Lib.List32.index_of (FuncDefType ft) c.types) in refer_func c x; [] --> [RefType (NonNullable, DefHeapType (SynVar y))] @@ -683,8 +682,8 @@ let check_import (im : import) (c : context) : context = let {module_name = _; item_name = _; idesc} = im.it in match idesc.it with | FuncImport x -> - ignore (func_type c x); - {c with funcs = x.it :: c.funcs} + let ft = func_type c x in + {c with funcs = ft :: c.funcs} | TableImport tt -> check_table_type c tt idesc.at; {c with tables = tt :: c.tables} @@ -723,7 +722,7 @@ let check_module (m : module_) = in let c1 = { c0 with - funcs = c0.funcs @ List.map (fun f -> ignore (func_type c0 f.it.ftype); f.it.ftype.it) funcs; + funcs = c0.funcs @ List.map (fun f -> func_type c0 f.it.ftype) funcs; tables = c0.tables @ List.map (fun tab -> tab.it.ttype) tables; memories = c0.memories @ List.map (fun mem -> mem.it.mtype) memories; elems = List.map (fun elem -> elem.it.etype) elems; From e8d29098d795e4f2df818b3936e204d5849a288d Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 6 Aug 2021 18:31:46 +0200 Subject: [PATCH 5/5] [spec] Add concrete ref types (#49) --- document/core/appendix/index-rules.rst | 27 +- document/core/appendix/index-types.rst | 9 +- document/core/appendix/properties.rst | 14 +- document/core/binary/instructions.rst | 2 +- document/core/binary/types.rst | 26 +- document/core/exec/modules.rst | 2 +- document/core/exec/runtime.rst | 1 + document/core/syntax/instructions.rst | 2 +- document/core/syntax/modules.rst | 2 +- document/core/syntax/types.rst | 36 ++- document/core/text/instructions.rst | 8 +- document/core/text/modules.rst | 26 +- document/core/text/types.rst | 70 +++-- document/core/util/macros.def | 51 ++- document/core/valid/index.rst | 1 + document/core/valid/instructions.rst | 52 +-- document/core/valid/matching.rst | 347 ++++++++++++++++++++ document/core/valid/modules.rst | 76 +++-- document/core/valid/types.rst | 417 ++++++++++--------------- interpreter/binary/decode.ml | 26 +- interpreter/binary/encode.ml | 8 +- 21 files changed, 824 insertions(+), 379 deletions(-) create mode 100644 document/core/valid/matching.rst diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst index dde34900..75514218 100644 --- a/document/core/appendix/index-rules.rst +++ b/document/core/appendix/index-rules.rst @@ -13,13 +13,13 @@ Typing of Static Constructs =============================================== =============================================================================== Construct Judgement =============================================== =============================================================================== -:ref:`Limits ` :math:`\vdashlimits \limits : k` -:ref:`Function type ` :math:`\vdashfunctype \functype \ok` -:ref:`Block type ` :math:`\vdashblocktype \blocktype \ok` -:ref:`Table type ` :math:`\vdashtabletype \tabletype \ok` -:ref:`Memory type ` :math:`\vdashmemtype \memtype \ok` -:ref:`Global type ` :math:`\vdashglobaltype \globaltype \ok` -:ref:`External type ` :math:`\vdashexterntype \externtype \ok` +:ref:`Limits ` :math:`C \vdashlimits \limits : k` +:ref:`Function type ` :math:`C \vdashfunctype \functype \ok` +:ref:`Block type ` :math:`C \vdashblocktype \blocktype \ok` +:ref:`Table type ` :math:`C \vdashtabletype \tabletype \ok` +:ref:`Memory type ` :math:`C \vdashmemtype \memtype \ok` +:ref:`Global type ` :math:`C \vdashglobaltype \globaltype \ok` +:ref:`External type ` :math:`C \vdashexterntype \externtype \ok` :ref:`Instruction ` :math:`S;C \vdashinstr \instr : \functype` :ref:`Instruction sequence ` :math:`S;C \vdashinstrseq \instr^\ast : \functype` :ref:`Expression ` :math:`C \vdashexpr \expr : \resulttype` @@ -83,8 +83,17 @@ Matching =============================================== =============================================================================== Construct Judgement =============================================== =============================================================================== -:ref:`External type ` :math:`\vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2` -:ref:`Limits ` :math:`\vdashlimitsmatch \limits_1 \matcheslimits \limits_2` +:ref:`Number type ` :math:`C \vdashnumtypematch \numtype_1 \matchesnumtype \numtype_2` +:ref:`Heap type ` :math:`C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2` +:ref:`Reference type ` :math:`C \vdashreftypematch \reftype_1 \matchesreftype \reftype_2` +:ref:`Value type ` :math:`C \vdashvaltypematch \valtype_1 \matchesvaltype \valtype_2` +:ref:`Result type ` :math:`C \vdashresulttypematch \resulttype_1 \matchesresulttype \resulttype_2` +:ref:`Function type ` :math:`C \vdashfunctypematch \functype_1 \matchesfunctype \functype_2` +:ref:`Table type ` :math:`C \vdashtabletypematch \tabletype_1 \matchestabletype \tabletype_2` +:ref:`Memory type ` :math:`C \vdashmemtypematch \memtype_1 \matchesmemtype \memtype_2` +:ref:`Global type ` :math:`C \vdashglobaltypematch \globaltype_1 \matchesglobaltype \globaltype_2` +:ref:`External type ` :math:`C \vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2` +:ref:`Limits ` :math:`C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2` =============================================== =============================================================================== diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst index fd38fe20..90a41193 100644 --- a/document/core/appendix/index-types.rst +++ b/document/core/appendix/index-types.rst @@ -13,9 +13,12 @@ Category Constructor :ref:`Number type ` |F32| :math:`\hex{7D}` (-3 as |Bs7|) :ref:`Number type ` |F64| :math:`\hex{7C}` (-4 as |Bs7|) (reserved) :math:`\hex{7B}` .. :math:`\hex{71}` -:ref:`Reference type ` |FUNCREF| :math:`\hex{70}` (-16 as |Bs7|) -:ref:`Reference type ` |EXTERNREF| :math:`\hex{6F}` (-17 as |Bs7|) -(reserved) :math:`\hex{6E}` .. :math:`\hex{61}` +: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}` :ref:`Function type ` :math:`[\valtype^\ast] \to [\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/appendix/properties.rst b/document/core/appendix/properties.rst index cf1fd0fb..7aa01099 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -4,6 +4,10 @@ Soundness --------- +.. todo:: need to operate wrt semantic types +.. todo:: define "S \vdash t ok" +.. todo:: ensure wf of guessed valtypes + The :ref:`type system ` of WebAssembly is *sound*, implying both *type safety* and *memory safety* with respect to the WebAssembly semantics. For example: * All types declared and derived during validation are respected at run time; @@ -50,7 +54,7 @@ Results :ref:`Results ` :math:`\TRAP` ............................................ -* The result is valid with :ref:`result type ` :math:`[t^\ast]`, for any sequence :math:`t^\ast` of :ref:`value types `. +* The result is valid with :ref:`result type ` :math:`[t^\ast]`, for any sequence :math:`t^\ast` of :ref:`valid ` :ref:`value types `. .. math:: \frac{ @@ -221,6 +225,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co * Then the table instance is valid with :ref:`table type ` :math:`\limits~t`. +.. todo:: reftypematch needs C + .. math:: \frac{ \vdashtabletype \limits~t \ok @@ -229,7 +235,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \qquad (S \vdash \reff : t')^n \qquad - (\vdashreftypematch t' \matchesvaltype t)^n + (C \vdashreftypematch t' \matchesvaltype t)^n }{ S \vdashtableinst \{ \TITYPE~(\limits~t), \TIELEM~\reff^n \} : \limits~t } @@ -297,11 +303,13 @@ Module instances are classified by *module contexts*, which are regular :ref:`co * Then the table instance is valid. +.. todo:: reftypematch needs C + .. math:: \frac{ (S \vdash \reff : t')^\ast \qquad - (\vdashreftypematch t' \matchesvaltype t)^\ast + (C \vdashreftypematch t' \matchesvaltype t)^\ast }{ S \vdasheleminst \{ \EITYPE~t, \EIELEM~\reff^\ast \} \ok } diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 9c789978..89724697 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -88,7 +88,7 @@ Reference Instructions .. math:: \begin{array}{llclll} \production{instruction} & \Binstr &::=& \dots \\ &&|& - \hex{D0}~~t{:}\Breftype &\Rightarrow& \REFNULL~t \\ &&|& + \hex{D0}~~t{:}\Bheaptype &\Rightarrow& \REFNULL~t \\ &&|& \hex{D1} &\Rightarrow& \REFISNULL \\ &&|& \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\ \end{array} diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index 975f17ad..e9adc4df 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -29,6 +29,24 @@ Number Types \end{array} +.. index:: heap type + pair: binary format; heap type +.. _binary-heaptype: + +Heap Types +~~~~~~~~~~ + +:ref:`Heap types ` are encoded as either a single byte, or as a :ref:`type index ` encoded as a positive :ref:`signed integer `. + +.. math:: + \begin{array}{llclll@{\qquad\qquad}l} + \production{heap type} & \Bheaptype &::=& + \hex{6F} &\Rightarrow& \EXTERN \\ &&|& + \hex{70} &\Rightarrow& \FUNC \\ &&|& + x{:}\Bs33 &\Rightarrow& x & (\iff x \geq 0) \\ + \end{array} + + .. index:: reference type pair: binary format; reference type .. _binary-reftype: @@ -36,13 +54,15 @@ Number Types Reference Types ~~~~~~~~~~~~~~~ -:ref:`Reference types ` are also encoded by a single byte. +:ref:`Reference types ` are either encoded by a single byte followed by a :ref:`heap type `, or, as a short form, directly as a non-index heap type. .. math:: \begin{array}{llclll@{\qquad\qquad}l} \production{reference type} & \Breftype &::=& - \hex{70} &\Rightarrow& \FUNCREF \\ &&|& - \hex{6F} &\Rightarrow& \EXTERNREF \\ + \hex{6B}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\X{ht} \\ &&|& + \hex{6C}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\NULL~\X{ht} \\ &&|& + \hex{6F} &\Rightarrow& \EXTERNREF \\ &&|& + \hex{70} &\Rightarrow& \FUNCREF \\ \end{array} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index cf0cf087..2547aa49 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -3,7 +3,7 @@ Modules For modules, the execution semantics primarily defines :ref:`instantiation `, which :ref:`allocates ` instances for a module and its contained definitions, initializes :ref:`tables ` and :ref:`memories ` from contained :ref:`element ` and :ref:`data ` segments, and invokes the :ref:`start function ` if present. It also includes :ref:`invocation ` of exported functions. -Instantiation depends on a number of auxiliary notions for :ref:`type-checking imports ` and :ref:`allocating ` instances. +Instantiation depends on a number of auxiliary notions for :ref:`type-checking imports ` and :ref:`allocating ` instances. .. index:: external value, external type, validation, import, store diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 02b90c01..5f042cd5 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -13,6 +13,7 @@ Runtime Structure .. _syntax-ref: .. _syntax-ref.extern: .. _syntax-val: +.. _syntax-null: Values ~~~~~~ diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 9c582d64..ed3aff9c 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -434,7 +434,7 @@ Forward branches require operands according to the output of the targeted block' Backward branches require operands according to the input of the targeted block's type, i.e., represent the values consumed by the restarted block. The |CALL| instruction invokes another :ref:`function `, consuming the necessary arguments from the stack and returning the result values of the call. -The |CALLINDIRECT| instruction calls a function indirectly through an operand indexing into a :ref:`table ` that is denoted by a :ref:`table index ` and must have type |FUNCREF|. +The |CALLINDIRECT| instruction calls a function indirectly through an operand indexing into a :ref:`table ` that is denoted by a :ref:`table index ` and must contain :ref:`function references `. Since it may contain functions of heterogeneous type, the callee is dynamically checked against the :ref:`function type ` indexed by the instruction's second immediate, and the call is aborted with a :ref:`trap ` if it does not match. diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst index cfd8935a..f51a504f 100644 --- a/document/core/syntax/modules.rst +++ b/document/core/syntax/modules.rst @@ -273,7 +273,7 @@ The |EOFFSET| is given by a :ref:`constant ` :ref:`expression `. .. note:: - In the current version of WebAssembly, only tables of element type |FUNCREF| can be initialized with an element segment. + In the current version of WebAssembly, only tables whose elements are :ref:`function references ` can be initialized with an element segment. This limitation may be lifted in the future. diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 858fbc1a..ac8b224c 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -41,7 +41,29 @@ Conventions That is, :math:`|\I32| = |\F32| = 32` and :math:`|\I64| = |\F64| = 64`. -.. index:: ! reference type, reference, table, function, function type, null +.. index:: ! heap type, store, type index + pair: abstract syntax; heap type +.. _syntax-heaptype: + +Heap Types +~~~~~~~~~~ + +*Heap types* classify objects in the runtime :ref:`store `. + +.. math:: + \begin{array}{llll} + \production{heap type} & \heaptype &::=& + \FUNC ~|~ \EXTERN ~|~ \typeidx \\ + \end{array} + +The type |FUNC| denotes the infinite union of all types of :ref:`functions `, regardless of their concrete :ref:`function types `. + +The type |EXTERN| denotes the infinite union of all objects owned by the :ref:`embedder ` and that can be passed into WebAssembly under this type. + +A *concrete* heap type consists of a :ref:`type index ` and classifies an object of the respective :ref:`type ` defined in the module. + + +.. index:: ! reference type, heap type, reference, table, function, function type, null pair: abstract syntax; reference type pair: reference; type .. _syntax-reftype: @@ -49,26 +71,28 @@ Conventions Reference Types ~~~~~~~~~~~~~~~ -*Reference types* classify first-class references to objects in the runtime :ref:`store `. +*Reference types* classify :ref:`values ` that are first-class references to objects in the runtime :ref:`store `. .. math:: \begin{array}{llll} \production{reference type} & \reftype &::=& - \FUNCREF ~|~ \EXTERNREF \\ + \REF~\NULL^?~\heaptype \\ \end{array} -The type |FUNCREF| denotes the infinite union of all references to :ref:`functions `, regardless of their :ref:`function types `. +A reference type is characterised by the :ref:`heap type ` it points to. -The type |EXTERNREF| denotes the infinite union of all references to objects owned by the :ref:`embedder ` and that can be passed into WebAssembly under this type. +In addition, a reference type of the form :math:`\REF \NULL \X{ht}` is *nullable*, meaning that it can either be a proper reference to :math:`\X{ht}` or :ref:`null `. +Other references are *non-null*. Reference types are *opaque*, meaning that neither their size nor their bit pattern can be observed. Values of reference type can be stored in :ref:`tables `. -.. index:: ! value type, number type, reference type +.. index:: ! value type, number type, reference type, ! bottom type pair: abstract syntax; value type pair: value; type .. _syntax-valtype: +.. _syntax-bottype: Value Types ~~~~~~~~~~~ diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 6112a766..0c350d00 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -70,7 +70,7 @@ However, the special case of a type use that is syntactically empty or consists \begin{array}[t]{@{}c@{}} ::= \\ | \\ \end{array} & \begin{array}[t]{@{}lcll@{}} - (t{:}\Tresult)^? &\Rightarrow& t^? \\ + (t{:}\Tresult_I)^? &\Rightarrow& t^? \\ x,I'{:}\Ttypeuse_I &\Rightarrow& x & (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\ \end{array} \\ \production{block instruction} & \Tblockinstr_I &::=& @@ -128,9 +128,9 @@ The :math:`\text{else}` keyword of an :math:`\text{if}` instruction can be omitt .. math:: \begin{array}{llclll} \production{block instruction} & - \text{if}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{end} + \text{if}~~\Tlabel~~\Tblocktype_I~~\Tinstr^\ast~~\text{end} &\equiv& - \text{if}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{else}~~\text{end} + \text{if}~~\Tlabel~~\Tblocktype_I~~\Tinstr^\ast~~\text{else}~~\text{end} \end{array} Also, for backwards compatibility, the table index to :math:`\text{call\_indirect}` can be omitted, defaulting to :math:`0`. @@ -178,7 +178,7 @@ Parametric Instructions \begin{array}{llclll} \production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|& \text{drop} &\Rightarrow& \DROP \\ &&|& - \text{select}~((t{:}\Tresult)^\ast)^? &\Rightarrow& \SELECT~(t^\ast)^? \\ + \text{select}~((t{:}\Tresult_I)^\ast)^? &\Rightarrow& \SELECT~(t^\ast)^? \\ \end{array} diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index 848f6880..d9e75984 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -72,8 +72,8 @@ Type definitions can bind a symbolic :ref:`type identifier `. .. math:: \begin{array}{llclll} - \production{type definition} & \Ttype &::=& - \text{(}~\text{type}~~\Tid^?~~\X{ft}{:}\Tfunctype~\text{)} + \production{type definition} & \Ttype_I &::=& + \text{(}~\text{type}~~\Tid^?~~\X{ft}{:}\Tfunctype_I~\text{)} &\Rightarrow& \X{ft} \\ \end{array} @@ -167,11 +167,11 @@ The descriptors in imports can bind a symbolic function, table, memory, or globa \production{import description} & \Timportdesc_I &::=& \text{(}~\text{func}~~\Tid^?~~x,I'{:}\Ttypeuse_I~\text{)} &\Rightarrow& \IDFUNC~x \\ &&|& - \text{(}~\text{table}~~\Tid^?~~\X{tt}{:}\Ttabletype~\text{)} + \text{(}~\text{table}~~\Tid^?~~\X{tt}{:}\Ttabletype_I~\text{)} &\Rightarrow& \IDTABLE~\X{tt} \\ &&|& - \text{(}~\text{memory}~~\Tid^?~~\X{mt}{:}\Tmemtype~\text{)} + \text{(}~\text{memory}~~\Tid^?~~\X{mt}{:}\Tmemtype_I~\text{)} &\Rightarrow& \IDMEM~~\X{mt} \\ &&|& - \text{(}~\text{global}~~\Tid^?~~\X{gt}{:}\Tglobaltype~\text{)} + \text{(}~\text{global}~~\Tid^?~~\X{gt}{:}\Tglobaltype_I~\text{)} &\Rightarrow& \IDGLOBAL~\X{gt} \\ \end{array} @@ -198,11 +198,11 @@ Function definitions can bind a symbolic :ref:`function identifier `, a \begin{array}{llclll} \production{function} & \Tfunc_I &::=& \text{(}~\text{func}~~\Tid^?~~x,I'{:}\Ttypeuse_I~~ - (t{:}\Tlocal)^\ast~~(\X{in}{:}\Tinstr_{I''})^\ast~\text{)} \\ &&& \qquad + (t{:}\Tlocal_I)^\ast~~(\X{in}{:}\Tinstr_{I''})^\ast~\text{)} \\ &&& \qquad \Rightarrow\quad \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\X{in}^\ast~\END \} \\ &&& \qquad\qquad\qquad (\iff I'' = I' \compose \{\ILOCALS~\F{id}(\Tlocal)^\ast\} \idcwellformed) \\[1ex] - \production{local} & \Tlocal &::=& - \text{(}~\text{local}~~\Tid^?~~t{:}\Tvaltype~\text{)} + \production{local} & \Tlocal_I &::=& + \text{(}~\text{local}~~\Tid^?~~t{:}\Tvaltype_I~\text{)} \quad\Rightarrow\quad t \\ \end{array} @@ -265,7 +265,7 @@ Table definitions can bind a symbolic :ref:`table identifier `. .. math:: \begin{array}{llclll} \production{table} & \Ttable_I &::=& - \text{(}~\text{table}~~\Tid^?~~\X{tt}{:}\Ttabletype~\text{)} + \text{(}~\text{table}~~\Tid^?~~\X{tt}{:}\Ttabletype_I~\text{)} &\Rightarrow& \{ \TTYPE~\X{tt} \} \\ \end{array} @@ -334,7 +334,7 @@ Memory definitions can bind a symbolic :ref:`memory identifier `. .. math:: \begin{array}{llclll} \production{memory} & \Tmem_I &::=& - \text{(}~\text{memory}~~\Tid^?~~\X{mt}{:}\Tmemtype~\text{)} + \text{(}~\text{memory}~~\Tid^?~~\X{mt}{:}\Tmemtype_I~\text{)} &\Rightarrow& \{ \MTYPE~\X{mt} \} \\ \end{array} @@ -394,7 +394,7 @@ Global definitions can bind a symbolic :ref:`global identifier `. .. math:: \begin{array}{llclll} \production{global} & \Tglobal_I &::=& - \text{(}~\text{global}~~\Tid^?~~\X{gt}{:}\Tglobaltype~~e{:}\Texpr_I~\text{)} + \text{(}~\text{global}~~\Tid^?~~\X{gt}{:}\Tglobaltype_I~~e{:}\Texpr_I~\text{)} &\Rightarrow& \{ \GTYPE~\X{gt}, \GINIT~e \} \\ \end{array} @@ -505,7 +505,7 @@ Element segments allow for an optional :ref:`table index ` to ide \text{(}~\text{elem}~~\Tid^?~~\text{declare}~~(et, y^\ast){:}\Telemlist_I~\text{)} \\ &&& \qquad \Rightarrow\quad \{ \ETYPE~et, \EINIT~y^\ast, \EMODE~\EDECLARATIVE \} \\ \production{element list} & \Telemlist_I &::=& - t{:}\Treftype~~y^\ast{:}\Tvec(\Telemexpr_I) \qquad\Rightarrow\quad ( \ETYPE~t, \EINIT~y^\ast ) \\ + t{:}\Treftype_I~~y^\ast{:}\Tvec(\Telemexpr_I) \qquad\Rightarrow\quad ( \ETYPE~t, \EINIT~y^\ast ) \\ \production{element expression} & \Telemexpr_I &::=& \text{(}~\text{item}~~e{:}\Texpr_I~\text{)} \quad\Rightarrow\quad e \\ @@ -641,7 +641,7 @@ The name serves a documentary role only. \production{module field} & \Tmodulefield_I & \begin{array}[t]{@{}clll} ::=& - \X{ty}{:}\Ttype &\Rightarrow& \{\MTYPES~\X{ty}\} \\ |& + \X{ty}{:}\Ttype_I &\Rightarrow& \{\MTYPES~\X{ty}\} \\ |& \X{im}{:}\Timport_I &\Rightarrow& \{\MIMPORTS~\X{im}\} \\ |& \X{fn}{:}\Tfunc_I &\Rightarrow& \{\MFUNCS~\X{fn}\} \\ |& \X{ta}{:}\Ttable_I &\Rightarrow& \{\MTABLES~\X{ta}\} \\ |& diff --git a/document/core/text/types.rst b/document/core/text/types.rst index 6d4ee375..17a3f46a 100644 --- a/document/core/text/types.rst +++ b/document/core/text/types.rst @@ -14,7 +14,7 @@ Number Types .. math:: \begin{array}{llcll@{\qquad\qquad}l} - \production{number type} & \Tnumtype &::=& + \production{number type} & \Tnumtype_I &::=& \text{i32} &\Rightarrow& \I32 \\ &&|& \text{i64} &\Rightarrow& \I64 \\ &&|& \text{f32} &\Rightarrow& \F32 \\ &&|& @@ -22,22 +22,48 @@ Number Types \end{array} +.. index:: heap type + pair: text format; heap type +.. _text-heaptype: + +Heap Types +~~~~~~~~~~ + +.. math:: + \begin{array}{llcll@{\qquad\qquad}l} + \production{heap type} & \Theaptype_I &::=& + \text{func} &\Rightarrow& \FUNC \\ &&|& + \text{extern} &\Rightarrow& \EXTERN \\ &&|& + x{:}\Ttypeidx_I &\Rightarrow& x \\ + \end{array} + + .. index:: reference type pair: text format; reference type .. _text-reftype: -.. _text-heaptype: Reference Types ~~~~~~~~~~~~~~~ .. math:: \begin{array}{llcll@{\qquad\qquad}l} - \production{reference type} & \Treftype &::=& - \text{funcref} &\Rightarrow& \FUNCREF \\ &&|& - \text{externref} &\Rightarrow& \EXTERNREF \\ - \production{heap type} & \Theaptype &::=& - \text{func} &\Rightarrow& \FUNCREF \\ &&|& - \text{extern} &\Rightarrow& \EXTERNREF \\ + \production{reference type} & \Treftype_I &::=& + \text{(}~\text{ref}~~\X{ht}{:}\Theaptype~\text{)} + &\Rightarrow& \REF~\X{ht} \\ &&|& + \text{(}~\text{ref}~~\text{null}~~\X{ht}{:}\Theaptype~\text{)} + &\Rightarrow& \REF~\NULL~\X{ht} \\ + \end{array} + +Abbreviations +............. + +There are shorthands for references to abstract heap types. + +.. math:: + \begin{array}{llclll} + \production{reference type} & + \text{funcref} &\equiv& \text{(}~\text{ref}~~\text{null}~~\text{func}~\text{)} \\ + \text{externref} &\equiv& \text{(}~\text{ref}~~\text{null}~~\text{extern}~\text{)} \\ \end{array} @@ -50,9 +76,9 @@ Value Types .. math:: \begin{array}{llcll@{\qquad\qquad}l} - \production{value type} & \Tvaltype &::=& - t{:}\Tnumtype &\Rightarrow& t \\ &&|& - t{:}\Treftype &\Rightarrow& t \\ + \production{value type} & \Tvaltype_I &::=& + t{:}\Tnumtype_I &\Rightarrow& t \\ &&|& + t{:}\Treftype_I &\Rightarrow& t \\ \end{array} @@ -67,14 +93,14 @@ Function Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{function type} & \Tfunctype &::=& - \text{(}~\text{func}~~t_1^\ast{:\,}\Tvec(\Tparam)~~t_2^\ast{:\,}\Tvec(\Tresult)~\text{)} + \production{function type} & \Tfunctype_I &::=& + \text{(}~\text{func}~~t_1^\ast{:\,}\Tvec(\Tparam_I)~~t_2^\ast{:\,}\Tvec(\Tresult_I)~\text{)} &\Rightarrow& [t_1^\ast] \to [t_2^\ast] \\ - \production{parameter} & \Tparam &::=& - \text{(}~\text{param}~~\Tid^?~~t{:}\Tvaltype~\text{)} + \production{parameter} & \Tparam_I &::=& + \text{(}~\text{param}~~\Tid^?~~t{:}\Tvaltype_I~\text{)} &\Rightarrow& t \\ - \production{result} & \Tresult &::=& - \text{(}~\text{result}~~t{:}\Tvaltype~\text{)} + \production{result} & \Tresult_I &::=& + \text{(}~\text{result}~~t{:}\Tvaltype_I~\text{)} &\Rightarrow& t \\ \end{array} @@ -119,7 +145,7 @@ Memory Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{memory type} & \Tmemtype &::=& + \production{memory type} & \Tmemtype_I &::=& \X{lim}{:}\Tlimits &\Rightarrow& \X{lim} \\ \end{array} @@ -133,8 +159,8 @@ Table Types .. math:: \begin{array}{llclll} - \production{table type} & \Ttabletype &::=& - \X{lim}{:}\Tlimits~~\X{et}{:}\Treftype &\Rightarrow& \X{lim}~\X{et} \\ + \production{table type} & \Ttabletype_I &::=& + \X{lim}{:}\Tlimits~~\X{et}{:}\Treftype_I &\Rightarrow& \X{lim}~\X{et} \\ \end{array} @@ -148,7 +174,7 @@ Global Types .. math:: \begin{array}{llclll} - \production{global type} & \Tglobaltype &::=& + \production{global type} & \Tglobaltype_I &::=& t{:}\Tvaltype &\Rightarrow& \MCONST~t \\ &&|& - \text{(}~\text{mut}~~t{:}\Tvaltype~\text{)} &\Rightarrow& \MVAR~t \\ + \text{(}~\text{mut}~~t{:}\Tvaltype_I~\text{)} &\Rightarrow& \MVAR~t \\ \end{array} diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 0a7a9cf7..a4d950e9 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -179,8 +179,12 @@ .. |F32| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f32}} .. |F64| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f64}} -.. |FUNCREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{funcref}} -.. |EXTERNREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{externref}} +.. |REF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{ref}} +.. |NULL| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{null}} +.. |FUNC| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{func}} +.. |EXTERN| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{extern}} +.. |FUNCREF| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{funcref}} +.. |EXTERNREF| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{externref}} .. |MVAR| mathdef:: \xref{syntax/types}{syntax-mut}{\K{var}} .. |MCONST| mathdef:: \xref{syntax/types}{syntax-mut}{\K{const}} @@ -197,6 +201,7 @@ .. Types, non-terminals .. |numtype| mathdef:: \xref{syntax/types}{syntax-numtype}{\X{numtype}} +.. |heaptype| mathdef:: \xref{syntax/types}{syntax-heaptype}{\X{heaptype}} .. |reftype| mathdef:: \xref{syntax/types}{syntax-reftype}{\X{reftype}} .. |valtype| mathdef:: \xref{syntax/types}{syntax-valtype}{\X{valtype}} .. |resulttype| mathdef:: \xref{syntax/types}{syntax-resulttype}{\X{resulttype}} @@ -500,6 +505,7 @@ .. Types, non-terminals .. |Bnumtype| mathdef:: \xref{binary/types}{binary-numtype}{\B{numtype}} +.. |Bheaptype| mathdef:: \xref{binary/types}{binary-heaptype}{\B{heaptype}} .. |Breftype| mathdef:: \xref{binary/types}{binary-reftype}{\B{reftype}} .. |Bvaltype| mathdef:: \xref{binary/types}{binary-valtype}{\B{valtype}} .. |Bresulttype| mathdef:: \xref{binary/types}{binary-resulttype}{\B{resulttype}} @@ -661,8 +667,8 @@ .. Types, non-terminals .. |Tnumtype| mathdef:: \xref{text/types}{text-numtype}{\T{numtype}} -.. |Treftype| mathdef:: \xref{text/types}{text-reftype}{\T{reftype}} .. |Theaptype| mathdef:: \xref{text/types}{text-heaptype}{\T{heaptype}} +.. |Treftype| mathdef:: \xref{text/types}{text-reftype}{\T{reftype}} .. |Tvaltype| mathdef:: \xref{text/types}{text-valtype}{\T{valtype}} .. |Tfunctype| mathdef:: \xref{text/types}{text-functype}{\T{functype}} @@ -774,8 +780,17 @@ .. |ok| mathdef:: \mathrel{\mbox{ok}} .. |const| mathdef:: \xref{valid/instructions}{valid-constant}{\mathrel{\mbox{const}}} -.. |matchesvaltype| mathdef:: \xref{valid/types}{match-valtype}{\leq} -.. |matchesresulttype| mathdef:: \xref{valid/types}{match-resulttype}{\leq} +.. |matchesnumtype| mathdef:: \xref{valid/matching}{match-numtype}{\leq} +.. |matchesheaptype| mathdef:: \xref{valid/matching}{match-heaptype}{\leq} +.. |matchesreftype| mathdef:: \xref{valid/matching}{match-reftype}{\leq} +.. |matchesvaltype| mathdef:: \xref{valid/matching}{match-valtype}{\leq} +.. |matchesresulttype| mathdef:: \xref{valid/matching}{match-resulttype}{\leq} +.. |matchesfunctype| mathdef:: \xref{valid/matching}{match-functype}{\leq} +.. |matchestabletype| mathdef:: \xref{valid/matching}{match-tabletype}{\leq} +.. |matchesmemtype| mathdef:: \xref{valid/matching}{match-memtype}{\leq} +.. |matchesglobaltype| mathdef:: \xref{valid/matching}{match-globaltype}{\leq} +.. |matchesexterntype| mathdef:: \xref{exec/matching}{match-externtype}{\leq} +.. |matcheslimits| mathdef:: \xref{exec/matching}{match-limits}{\leq} .. Contexts @@ -795,6 +810,11 @@ .. Judgments +.. |vdashnumtype| mathdef:: \xref{valid/types}{valid-numtype}{\vdash} +.. |vdashheaptype| mathdef:: \xref{valid/types}{valid-heaptype}{\vdash} +.. |vdashreftype| mathdef:: \xref{valid/types}{valid-reftype}{\vdash} +.. |vdashvaltype| mathdef:: \xref{valid/types}{valid-valtype}{\vdash} +.. |vdashresulttype| mathdef:: \xref{valid/types}{valid-resulttype}{\vdash} .. |vdashlimits| mathdef:: \xref{valid/types}{valid-limits}{\vdash} .. |vdashblocktype| mathdef:: \xref{valid/types}{valid-blocktype}{\vdash} .. |vdashfunctype| mathdef:: \xref{valid/types}{valid-functype}{\vdash} @@ -803,10 +823,17 @@ .. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash} .. |vdashexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\vdash} -.. |vdashnumtypematch| mathdef:: \xref{valid/types}{match-numtype}{\vdash} -.. |vdashreftypematch| mathdef:: \xref{valid/types}{match-reftype}{\vdash} -.. |vdashvaltypematch| mathdef:: \xref{valid/types}{match-valtype}{\vdash} -.. |vdashresulttypematch| mathdef:: \xref{valid/types}{match-resulttype}{\vdash} +.. |vdashnumtypematch| mathdef:: \xref{valid/matching}{match-numtype}{\vdash} +.. |vdashheaptypematch| mathdef:: \xref{valid/matching}{match-heaptype}{\vdash} +.. |vdashreftypematch| mathdef:: \xref{valid/matching}{match-reftype}{\vdash} +.. |vdashvaltypematch| mathdef:: \xref{valid/matching}{match-valtype}{\vdash} +.. |vdashresulttypematch| mathdef:: \xref{valid/matching}{match-resulttype}{\vdash} +.. |vdashfunctypematch| mathdef:: \xref{valid/matching}{match-functype}{\vdash} +.. |vdashtabletypematch| mathdef:: \xref{valid/matching}{match-tabletype}{\vdash} +.. |vdashmemtypematch| mathdef:: \xref{valid/matching}{match-memtype}{\vdash} +.. |vdashglobaltypematch| mathdef:: \xref{valid/matching}{match-globaltype}{\vdash} +.. |vdashexterntypematch| mathdef:: \xref{exec/matching}{match-externtype}{\vdash} +.. |vdashlimitsmatch| mathdef:: \xref{exec/matching}{match-limits}{\vdash} .. |vdashinstr| mathdef:: \xref{valid/instructions}{valid-instr}{\vdash} .. |vdashinstrseq| mathdef:: \xref{valid/instructions}{valid-instr-seq}{\vdash} @@ -814,6 +841,7 @@ .. |vdashexprconst| mathdef:: \xref{valid/instructions}{valid-constant}{\vdash} .. |vdashinstrconst| mathdef:: \xref{valid/instructions}{valid-constant}{\vdash} +.. |vdashtypes| mathdef:: \xref{valid/modules}{valid-types}{\vdash} .. |vdashfunc| mathdef:: \xref{valid/modules}{valid-func}{\vdash} .. |vdashtable| mathdef:: \xref{valid/modules}{valid-table}{\vdash} .. |vdashmem| mathdef:: \xref{valid/modules}{valid-mem}{\vdash} @@ -837,8 +865,6 @@ .. |stepto| mathdef:: \xref{exec/conventions}{formal-notation}{\hookrightarrow} .. |extendsto| mathdef:: \xref{appendix/properties}{extend}{\preceq} -.. |matchesexterntype| mathdef:: \xref{exec/modules}{match-externtype}{\leq} -.. |matcheslimits| mathdef:: \xref{exec/modules}{match-limits}{\leq} .. Allocation @@ -1092,9 +1118,6 @@ .. |vdashexternval| mathdef:: \xref{exec/modules}{valid-externval}{\vdash} -.. |vdashlimitsmatch| mathdef:: \xref{exec/modules}{match-limits}{\vdash} -.. |vdashexterntypematch| mathdef:: \xref{exec/modules}{match-externtype}{\vdash} - .. Soundness .. --------- diff --git a/document/core/valid/index.rst b/document/core/valid/index.rst index 34cf3b90..cd5fce18 100644 --- a/document/core/valid/index.rst +++ b/document/core/valid/index.rst @@ -8,5 +8,6 @@ Validation conventions types + matching instructions modules diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 2594a1e0..9478e96c 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -201,17 +201,19 @@ Reference Instructions * The function :math:`C.\CFUNCS[x]` must be defined in the context. +* There must exist a :ref:`type index ` :math:`y` such that :math:`C.\CTYPES[y]` is the same :ref:`function type ` as :math:`C.\CFUNCS[x]`. + * The :ref:`function index ` :math:`x` must be contained in :math:`C.\CREFS`. -* The instruction is valid with type :math:`[] \to [\FUNCREF]`. +* The instruction is valid with type :math:`[] \to [(\REF~y)]`. .. math:: \frac{ - C.\CFUNCS[x] = \functype + C.\CFUNCS[x] = C.\CTYPES[y] \qquad x \in C.\CREFS }{ - C \vdashinstr \REFFUNC~x : [] \to [\FUNCREF] + C \vdashinstr \REFFUNC~x : [] \to [(\REF~y)] } @@ -248,22 +250,27 @@ Parametric Instructions * If :math:`t^\ast` is present, then: + * The :ref:`result type ` :math:`[t^\ast]` must be :ref:`valid `. + * The length of :math:`t^\ast` must be :math:`1`. * Then the instruction is valid with type :math:`[t^\ast~t^\ast~\I32] \to [t^\ast]`. * Else: - * The instruction is valid with type :math:`[t~t~\I32] \to [t]`, for any :ref:`value type ` :math:`t` that :ref:`matches ` some :ref:`number type `. + * The instruction is valid with type :math:`[t~t~\I32] \to [t]`, for any :ref:`valid ` :ref:`value type ` :math:`t` that :ref:`matches ` some :ref:`number type `. .. math:: \frac{ + C \vdashresulttype [t] \ok }{ C \vdashinstr \SELECT~t : [t~t~\I32] \to [t] } \qquad \frac{ - \vdashvaltypematch t \matchesvaltype \numtype + C \vdashresulttype [t] \ok + \qquad + C \vdashresulttypematch [t] \matchesresulttype [\numtype] }{ C \vdashinstr \SELECT : [t~t~\I32] \to [t] } @@ -501,7 +508,7 @@ Table Instructions \qquad C.\CTABLES[x] = \limits_2~t_2 \qquad - \vdashreftypematch t_2 \matchesvaltype t_1 + C \vdashreftypematch t_2 \matchesvaltype t_1 }{ C \vdashinstr \TABLECOPY~x~y : [\I32~\I32~\I32] \to [] } @@ -530,7 +537,7 @@ Table Instructions \qquad C.\CELEMS[y] = t_2 \qquad - \vdashreftypematch t_2 \matchesvaltype t_1 + C \vdashreftypematch t_2 \matchesvaltype t_1 }{ C \vdashinstr \TABLEINIT~x~y : [\I32~\I32~\I32] \to [] } @@ -778,10 +785,11 @@ Control Instructions :math:`\UNREACHABLE` .................... -* The instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. +* The instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, for any sequences of :ref:`valid ` :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ + C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok }{ C \vdashinstr \UNREACHABLE : [t_1^\ast] \to [t_2^\ast] } @@ -885,11 +893,13 @@ Control Instructions * Let :math:`[t^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. -* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. +* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`valid ` :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ C.\CLABELS[l] = [t^\ast] + \qquad + C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok }{ C \vdashinstr \BR~l : [t_1^\ast~t^\ast] \to [t_2^\ast] } @@ -942,13 +952,15 @@ Control Instructions * For all :math:`l_i` in :math:`l^\ast`, the result type :math:`[t^\ast]` :ref:`matches ` :math:`C.\CLABELS[l_i]`. -* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. +* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`, for any sequences of :ref:`valid ` :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ - (\vdashresulttypematch [t^\ast] \matchesresulttype C.\CLABELS[l])^\ast + (C \vdashresulttypematch [t^\ast] \matchesresulttype C.\CLABELS[l])^\ast \qquad - \vdashresulttypematch [t^\ast] \matchesresulttype C.\CLABELS[l_N] + C \vdashresulttypematch [t^\ast] \matchesresulttype C.\CLABELS[l_N] + \qquad + C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok }{ C \vdashinstr \BRTABLE~l^\ast~l_N : [t_1^\ast~t^\ast~\I32] \to [t_2^\ast] } @@ -972,11 +984,13 @@ Control Instructions * Let :math:`[t^\ast]` be the :ref:`result type ` of :math:`C.\CRETURN`. -* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. +* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`valid ` :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ C.\CRETURN = [t^\ast] + \qquad + C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok }{ C \vdashinstr \RETURN : [t_1^\ast~t^\ast] \to [t_2^\ast] } @@ -1015,7 +1029,7 @@ Control Instructions * Let :math:`\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. -* The :ref:`reference type ` :math:`t` must :ref:`match ` type |FUNCREF|. +* The :ref:`reference type ` :math:`t` must :ref:`match ` type :math:`\REF~\NULL~\FUNC`. * The type :math:`C.\CTYPES[y]` must be defined in the context. @@ -1027,7 +1041,7 @@ Control Instructions \frac{ C.\CTABLES[x] = \limits~t \qquad - \vdashvaltypematch t \leq \FUNCREF + C \vdashvaltypematch t \matchesreftype \REF~\NULL~\FUNC \qquad C.\CTYPES[y] = [t_1^\ast] \to [t_2^\ast] }{ @@ -1077,7 +1091,7 @@ Non-empty Instruction Sequence: :math:`\instr^\ast~\instr_N` \frac{ C \vdashinstrseq \instr^\ast : [t_1^\ast] \to [t_0^\ast~{t'}^\ast] \qquad - (\vdashvaltypematch t' \matchesvaltype t)^\ast + (C \vdashvaltypematch t' \matchesvaltype t)^\ast \qquad C \vdashinstr \instr_N : [t^\ast] \to [t_3^\ast] }{ @@ -1102,7 +1116,7 @@ Expressions :math:`\expr` are classified by :ref:`result types ` with some :ref:`type ` :math:`[] \to [{t'}^\ast]`. -* For each :ref:`value type ` :math:`t'_i` in :math:`{t'}^\ast` and corresponding :ref:`value type ` type :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches ` :math:`t_i`. +* For each :ref:`value type ` :math:`t'_i` in :math:`{t'}^\ast` and corresponding :ref:`valid ` :ref:`value type ` type :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches ` :math:`t_i`. * Then the expression is valid with :ref:`result type ` :math:`[t^\ast]`. @@ -1110,7 +1124,9 @@ Expressions :math:`\expr` are classified by :ref:`result types ` when checking the types of imports. + +.. todo:: externtype matching is used on semantic types; need to define how to reinterpret C for semantic types + + +.. index:: number type +.. _match-numtype: + +Number Types +~~~~~~~~~~~~ + +A :ref:`number type ` :math:`\numtype_1` matches a :ref:`number type ` :math:`\numtype_2` if and only if: + +* Both :math:`\numtype_1` and :math:`\numtype_2` are the same. + +.. math:: + ~\\[-1ex] + \frac{ + }{ + C \vdashnumtypematch \numtype \matchesvaltype \numtype + } + + +.. index:: heap type +.. _match-heaptype: + +Heap Types +~~~~~~~~~~ + +A :ref:`heap type ` :math:`\heaptype_1` matches a :ref:`heap type ` :math:`\heaptype_2` if and only if: + +* Either both :math:`\heaptype_1` and :math:`\heaptype_2` are the same. + +* Or :math:`\heaptype_1` is a :ref:`type index ` that defines a function type and :math:`\heaptype_2` is :math:`FUNC`. + +* Or :math:`\heaptype_1` is a :ref:`type index ` that defines a function type :math:`\functype_1`, and :math:`\heaptype_2` is a :ref:`type index ` that defines a function type :math:`\functype_2`, and :math:`\functype_1` :ref:`matches ` :math:`\functype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + }{ + C \vdashheaptypematch \heaptype \matchesheaptype \heaptype + } + \qquad + \frac{ + C.\CTYPES[\typeidx] = \functype + }{ + C \vdashheaptypematch \typeidx \matchesheaptype \FUNC + } + +.. math:: + ~\\[-1ex] + \frac{ + C.\CTYPES[\typeidx_1] = \functype_1 + \qquad + C.\CTYPES[\typeidx_2] = \functype_2 + \qquad + C \vdashfunctypematch \functype_1 \matchesfunctype \functype_2 + }{ + C \vdashheaptypematch \typeidx_1 \matchesheaptype \typeidx_2 + } + + +.. index:: reference type +.. _match-reftype: + +Reference Types +~~~~~~~~~~~~~~~ + +A :ref:`reference type ` :math:`\REF~\NULL_1^?~heaptype_1` matches a :ref:`reference type ` :math:`\REF~\NULL_2^?~heaptype_2` if and only if: + +* The :ref:`heap type ` :math:`\heaptype_1` :ref:`matches ` :math:`\heaptype_2`. + +* :math:`\NULL_1` is absent or :math:`\NULL_2` is present. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2 + }{ + C \vdashreftypematch \REF~\heaptype_1 \matchesreftype \REF~\heaptype_2 + } + \qquad + \frac{ + C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2 + }{ + C \vdashreftypematch \REF~\NULL~\heaptype_1 \matchesreftype \REF~\NULL^?~\heaptype_2 + } + + +.. index:: value type, number type, reference type +.. _match-valtype: + +Value Types +~~~~~~~~~~~ + +A :ref:`value type ` :math:`\valtype_1` matches a :ref:`value type ` :math:`\valtype_2` if and only if: + +* Either both :math:`\valtype_1` and :math:`\valtype_2` are :ref:`number types ` and :math:`\valtype_1` :ref:`matches ` :math:`\valtype_2`. + +* Or both :math:`\valtype_1` and :math:`\valtype_2` are :ref:`reference types ` and :math:`\valtype_1` :ref:`matches ` :math:`\valtype_2`. + +* Or :math:`\valtype_1` is :math:`\BOT`. + +.. math:: + ~\\[-1ex] + \frac{ + }{ + C \vdashvaltypematch \BOT \matchesvaltype \valtype + } + + +.. index:: result type, value type +.. _match-resulttype: + +Result Types +~~~~~~~~~~~~ + +Subtyping is lifted to :ref:`result types ` in a pointwise manner. +That is, a :ref:`result type ` :math:`[t_1^\ast]` matches a :ref:`result type ` :math:`[t_2^\ast]` if and only if: + +* Every :ref:`value type ` :math:`t_1` in :math:`[t_1^\ast]` :ref:`matches ` the corresponding :ref:`value type ` :math:`t_2` in :math:`[t_2^\ast]`. + +.. math:: + ~\\[-1ex] + \frac{ + (C \vdashvaltypematch t_1 \matchesvaltype t_2)^\ast + }{ + C \vdashresulttypematch [t_1^\ast] \matchesresulttype [t_2^\ast] + } + + +.. index:: function type, result type +.. _match-functype: + +Function Types +~~~~~~~~~~~~~~ + +Subtyping is also defined for :ref:`function types `. +However, it is required that they match in both directions, effectively demanding type equivalence. +That is, a :ref:`function type ` :math:`[t_{11}^\ast] \to [t_{12}^\ast]` matches a type :math:`[t_{21}^ast] \to [t_{22}^\ast]` if and only if: + +* The :ref:`result type ` :math:`[t_{11}^\ast]` :ref:`matches ` :math:`[t_{21}^\ast]`, and vice versa. + +* The :ref:`result type ` :math:`[t_{12}^\ast]` :ref:`matches ` :math:`[t_{22}^\ast]`, and vice versa. + +.. math:: + ~\\[-1ex] + \frac{ + \begin{array}{@{}c@{}} + C \vdashresulttypematch [t_{11}^\ast] \matchesresulttype [t_{21}^\ast] + \qquad + C \vdashresulttypematch [t_{12}^\ast] \matchesresulttype [t_{22}^\ast] + \\ + C \vdashresulttypematch [t_{21}^\ast] \matchesresulttype [t_{11}^\ast] + \qquad + C \vdashresulttypematch [t_{22}^\ast] \matchesresulttype [t_{12}^\ast] + \end{array} + }{ + C \vdashfunctypematch [t_{11}^\ast] \to [t_{12}^\ast] \matchesfunctype [t_{21}^\ast] \to [t_{22}^\ast] + } + +.. note:: + In future versions of WebAssembly, subtyping on function types may be relaxed to support co- and contra-variance. + + +.. index:: limits +.. _match-limits: + +Limits +~~~~~~ + +:ref:`Limits ` :math:`\{ \LMIN~n_1, \LMAX~m_1^? \}` match limits :math:`\{ \LMIN~n_2, \LMAX~m_2^? \}` if and only if: + +* :math:`n_1` is larger than or equal to :math:`n_2`. + +* Either: + + * :math:`m_2^?` is empty. + +* Or: + + * Both :math:`m_1^?` and :math:`m_2^?` are non-empty. + + * :math:`m_1` is smaller than or equal to :math:`m_2`. + +.. math:: + ~\\[-1ex] + \frac{ + n_1 \geq n_2 + }{ + C \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1^? \} \matcheslimits \{ \LMIN~n_2, \LMAX~\epsilon \} + } + \quad + \frac{ + n_1 \geq n_2 + \qquad + m_1 \leq m_2 + }{ + C \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1 \} \matcheslimits \{ \LMIN~n_2, \LMAX~m_2 \} + } + + +.. index:: table type, limits, element type +.. _match-tabletype: + +Table Types +~~~~~~~~~~~ + +A :ref:`table type ` :math:`(\limits_1~\reftype_1)` matches :math:`(\limits_2~\reftype_2)` if and only if: + +* Limits :math:`\limits_1` :ref:`match ` :math:`\limits_2`. + +* The :ref:`reference type ` :math:`\reftype_1` :ref:`matches ` :math:`\reftype_2`, and vice versa. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 + \qquad + C \vdashreftypematch \reftype_1 \matchesreftype \reftype_2 + \qquad + C \vdashreftypematch \reftype_2 \matchesreftype \reftype_1 + }{ + C \vdashtabletypematch \limits_1~\reftype_1 \matchestabletype \limits_2~\reftype_2 + } + + +.. index:: memory type, limits +.. _match-memtype: + +Memory Types +~~~~~~~~~~~~ + +A :ref:`memory type ` :math:`\limits_1` matches :math:`\limits_2` if and only if: + +* Limits :math:`\limits_1` :ref:`match ` :math:`\limits_2`. + + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 + }{ + C \vdashmemtypematch \limits_1 \matchesmemtype \limits_2 + } + + +.. index:: global type, value type, mutability +.. _match-globaltype: + +Global Types +~~~~~~~~~~~~ + +A :ref:`global type ` :math:`(\mut_1~t_1)` matches :math:`(\mut_2~t_2)` if and only if: + +* Either both :math:`\mut_1` and :math:`\mut_2` are |MVAR| and :math:`t_1` and :math:`t_2` are the same. + +* Or both :math:`\mut_1` and :math:`\mut_2` are |MCONST| and :math:`t_1` :ref:`matches ` :math:`t_2`. + +.. math:: + ~\\[-1ex] + \frac{ + }{ + C \vdashglobaltypematch \MVAR~t \matchesglobaltype \MVAR~t + } + \qquad + \frac{ + C \vdashvaltypematch t_1 \matchesvaltype t_2 + }{ + C \vdashglobaltypematch \MCONST~t_1 \matchesglobaltype \MCONST~t_2 + } + + +.. index:: external type, function type, table type, memory type, global type +.. _match-externtype: + +External Types +~~~~~~~~~~~~~~ + +Functions +......... + +An :ref:`external type ` :math:`\ETFUNC~\functype_1` matches :math:`\ETFUNC~\functype_2` if and only if: + +* Function type :math:`\functype_1` :ref:`matches ` :math:`\functype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashfunctypematch \functype_1 \matchesfunctype \functype_2 + }{ + C \vdashexterntypematch \ETFUNC~\functype_1 \matchesexterntype \ETFUNC~\functype_2 + } + + +Tables +...... + +An :ref:`external type ` :math:`\ETTABLE~\tabletype_1` matches :math:`\ETTABLE~\tabletype_2` if and only if: + +* Table type :math:`\tabletype_1` :ref:`matches ` :math:`\tabletype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashtabletypematch \tabletype_1 \matchestabletype \tabletype_2 + }{ + C \vdashexterntypematch \ETTABLE~\tabletype_1 \matchesexterntype \ETTABLE~\tabletype_2 + } + + +Memories +........ + +An :ref:`external type ` :math:`\ETMEM~\memtype_1` matches :math:`\ETMEM~\memtype_2` if and only if: + +* Memory type :math:`\memtype_1` :ref:`matches ` :math:`\memtype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashmemtypematch \memtype_1 \matchesmemtype \memtype_2 + }{ + C \vdashexterntypematch \ETMEM~\memtype_1 \matchesexterntype \ETMEM~\memtype_2 + } + + +Globals +....... + +An :ref:`external type ` :math:`\ETGLOBAL~\globaltype_1` matches :math:`\ETGLOBAL~\globaltype_2` if and only if: + +* Global type :math:`\globaltype_1` :ref:`matches ` :math:`\globaltype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashglobaltypematch \globaltype_1 \matchesglobaltype \globaltype_2 + }{ + C \vdashexterntypematch \ETGLOBAL~\globaltype_1 \matchesexterntype \ETGLOBAL~\globaltype_2 + } diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 87546493..1d28153c 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -67,7 +67,7 @@ Tables :math:`\table` are classified by :ref:`table types `. .. math:: \frac{ - \vdashtabletype \tabletype \ok + C \vdashtabletype \tabletype \ok }{ C \vdashtable \{ \TTYPE~\tabletype \} : \tabletype } @@ -92,7 +92,7 @@ Memories :math:`\mem` are classified by :ref:`memory types `. .. math:: \frac{ - \vdashmemtype \memtype \ok + C \vdashmemtype \memtype \ok }{ C \vdashmem \{ \MTYPE~\memtype \} : \memtype } @@ -122,7 +122,7 @@ Globals :math:`\global` are classified by :ref:`global types .. math:: \frac{ - \vdashglobaltype \mut~t \ok + C \vdashglobaltype \mut~t \ok \qquad C \vdashexpr \expr : [t] \qquad @@ -147,6 +147,8 @@ Element segments :math:`\elem` are classified by the :ref:`reference type ` :math:`t` must be :ref:`valid `. + * For each :math:`e_i` in :math:`e^\ast`, * The expression :math:`e_i` must be :ref:`valid `. @@ -155,20 +157,22 @@ Element segments :math:`\elem` are classified by the :ref:`reference type ` :math:`t'`. -* The :ref:`reference type ` :math:`t` must :ref:`match ` the reference type :math:`t'`. +* The reference type :math:`t` must :ref:`match ` the reference type :math:`t'`. * Then the element segment is valid with :ref:`reference type ` :math:`t`. .. math:: \frac{ + C \vdashreftype t \ok + \qquad (C \vdashexpr e \ok)^\ast \qquad (C \vdashexprconst e \const)^\ast \qquad C \vdashelemmode \elemmode : t' \qquad - \vdashreftypematch t \matchesvaltype t' + C \vdashreftypematch t \matchesreftype t' }{ C \vdashelem \{ \ETYPE~t, \EINIT~e^\ast, \EMODE~\elemmode \} : t } @@ -179,10 +183,11 @@ Element segments :math:`\elem` are classified by the :ref:`reference type `. +* The element mode is valid with any :ref:`valid ` :ref:`reference type `. .. math:: \frac{ + C \vdashreftype \reftype \ok }{ C \vdashelemmode \EPASSIVE : \reftype } @@ -217,10 +222,11 @@ Element segments :math:`\elem` are classified by the :ref:`reference type `. +* The element mode is valid with any :ref:`valid ` :ref:`reference type `. .. math:: \frac{ + C \vdashreftype \reftype \ok }{ C \vdashelemmode \EDECLARATIVE : \reftype } @@ -436,7 +442,7 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi :math:`\IDFUNC~x` ................. -* The function :math:`C.\CTYPES[x]` must be defined in the context. +* The function type :math:`C.\CTYPES[x]` must be defined in the context. * Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type ` :math:`C.\CTYPES[x]`. @@ -459,7 +465,7 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi .. math:: \frac{ - \vdashtable \tabletype \ok + C \vdashtable \tabletype \ok }{ C \vdashimportdesc \IDTABLE~\tabletype : \ETTABLE~\tabletype } @@ -474,7 +480,7 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi .. math:: \frac{ - \vdashmemtype \memtype \ok + C \vdashmemtype \memtype \ok }{ C \vdashimportdesc \IDMEM~\memtype : \ETMEM~\memtype } @@ -489,7 +495,7 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi .. math:: \frac{ - \vdashglobaltype \globaltype \ok + C \vdashglobaltype \globaltype \ok }{ C \vdashimportdesc \IDGLOBAL~\globaltype : \ETGLOBAL~\globaltype } @@ -540,21 +546,26 @@ Instead, the context :math:`C` for validation of the module's content is constru * :math:`C.\CREFS` is the set :math:`\freefuncidx(\module \with \MFUNCS = \epsilon \with \MSTART = \epsilon)`, i.e., the set of :ref:`function indices ` occurring in the module, except in its :ref:`functions ` or :ref:`start function `. -* Let :math:`C'` be the :ref:`context ` where: +* For each function type :math:`\functype_i` in :math:`\module.\MTYPES`: + + * Let :math:`C'_i` be the :ref:`context ` where :math:`C'_i.\CTYPES` is :math:`C.\CTYPES[0 \slice i]` and all other fields are empty. + + * The function :math:`\functype_i` must be :ref:`valid ` under context :math:`C'_i`. + +* Let :math:`C''` be the :ref:`context ` where: - * :math:`C'.\CGLOBALS` is the sequence :math:`\etglobals(\X{it}^\ast)`, + * :math:`C''.\CGLOBALS` is the sequence :math:`\etglobals(\X{it}^\ast)`, - * :math:`C'.\CFUNCS` is the same as :math:`C.\CFUNCS`, + * :math:`C''.\CTYPES` is the same as :math:`C.\CTYPES`, - * :math:`C'.\CREFS` is the same as :math:`C.\CREFS`, + * :math:`C''.\CFUNCS` is the same as :math:`C.\CFUNCS`, + + * :math:`C''.\CREFS` is the same as :math:`C.\CREFS`, * all other fields are empty. * Under the context :math:`C`: - * For each :math:`\functype_i` in :math:`\module.\MTYPES`, - the :ref:`function type ` :math:`\functype_i` must be :ref:`valid `. - * 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`. @@ -566,7 +577,7 @@ Instead, the context :math:`C` for validation of the module's content is constru * For each :math:`\global_i` in :math:`\module.\MGLOBALS`: - * Under the context :math:`C'`, + * Under the context :math:`C''`, the definition :math:`\global_i` must be :ref:`valid ` with a :ref:`global type ` :math:`\X{gt}_i`. * For each :math:`\elem_i` in :math:`\module.\MELEMS`, @@ -607,7 +618,7 @@ Instead, the context :math:`C` for validation of the module's content is constru .. math:: \frac{ \begin{array}{@{}c@{}} - (\vdashfunctype \type \ok)^\ast + \vdashtypes \type^\ast \ok \quad (C \vdashfunc \func : \X{ft})^\ast \quad @@ -615,7 +626,7 @@ Instead, the context :math:`C` for validation of the module's content is constru \quad (C \vdashmem \mem : \X{mt})^\ast \quad - (C' \vdashglobal \global : \X{gt})^\ast + (C'' \vdashglobal \global : \X{gt})^\ast \\ (C \vdashelem \elem : \X{rt})^\ast \quad @@ -639,7 +650,9 @@ Instead, the context :math:`C` for validation of the module's content is constru \\ C = \{ \CTYPES~\type^\ast, \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' = \{ \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \} + (C' = \{ \CTYPES~\type^\ast \})^\ast + \\ + C'' = \{ \CTYPES~\type^\ast, \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \} \qquad |C.\CMEMS| \leq 1 \qquad @@ -663,6 +676,25 @@ Instead, the context :math:`C` for validation of the module's content is constru \vdashmodule \module : \X{it}^\ast \to \X{et}^\ast } +.. _valid-types: + +where: + +.. math:: + \frac{ + \vdashtypes \type^\ast \ok + \qquad + \{\CTYPES~\type^\ast\} \vdashtypes \type \ok + }{ + \vdashtypes \type^\ast~\type \ok + } + \qquad + \frac{ + }{ + \vdashtypes \epsilon \ok + } + + .. note:: Most definitions in a module -- particularly functions -- are mutually recursive. Consequently, the definition of the :ref:`context ` :math:`C` in this rule is recursive: diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 1b790bb4..1fd575b1 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -1,14 +1,147 @@ Types ----- -Most :ref:`types ` are universally valid. -However, restrictions apply to :ref:`function types ` as well as the :ref:`limits ` of :ref:`table types ` and :ref:`memory types `, which must be checked during validation. - -On :ref:`value types `, a simple notion of subtyping is defined. +Simple :ref:`types `, such as :ref:`number types ` are universally valid. +However, restrictions apply to most other types, such as :ref:`reference types `, :ref:`function types `, as well as the :ref:`limits ` of :ref:`table types ` and :ref:`memory types `, which must be checked during validation. Moreover, :ref:`block types ` are converted to plain :ref:`function types ` for ease of processing. +.. index:: number type + pair: validation; number type + single: abstract syntax; number type +.. _valid-numtype: + +Number Types +~~~~~~~~~~~~ + +:ref:`Number types ` are always valid. + +.. math:: + \frac{ + }{ + C \vdashnumtype \numtype \ok + } + + +.. index:: heap type + pair: validation; heap type + single: abstract syntax; heap type +.. _valid-heaptype: + +Heap Types +~~~~~~~~~~ + +Concrete :ref:`Heap types ` are only valid when the :ref:`type index ` is. + +:math:`\FUNC` +............. + +* The heap type is valid. + +.. math:: + \frac{ + }{ + C \vdashheaptype \FUNC \ok + } + +:math:`\EXTERN` +............... + +* The heap type is valid. + +.. math:: + \frac{ + }{ + C \vdashheaptype \EXTERN \ok + } + +:math:`\typeidx` +................ + +* The type :math:`C.\CTYPES[\typeidx]` must be defined in the context. + +* Then the heap type is valid. + +.. math:: + \frac{ + C.\CTYPES[\typeidx] = \functype + }{ + C \vdashheaptype \typeidx \ok + } + + +.. index:: reference type, heap type + pair: validation; reference type + single: abstract syntax; reference type +.. _valid-reftype: + +Reference Types +~~~~~~~~~~~~~~~ + +:ref:`Reference types ` are valid when the referenced :ref:`heap type ` is. + +:math:`\REF~\NULL^?~\heaptype` +.............................. + +* The heap type :math:`\heaptype` must be :ref:`valid `. + +* Then the reference type is valid. + +.. math:: + \frac{ + C \vdashreftype \heaptype \ok + }{ + C \vdashreftype \REF~\NULL^?~\heaptype \ok + } + + +.. index:: value type, reference type, heap type, bottom type + pair: validation; value type + single: abstract syntax; value type +.. _valid-valtype: +.. _valid-bottype: + +Value Types +~~~~~~~~~~~ + +Valid :ref:`value types ` are either valid :ref:`number type `, :ref:`reference type `, or the :ref:`bottom type `. + +:math:`\BOT` +............ + +* The value type is valid. + +.. math:: + \frac{ + }{ + C \vdashvaltype \BOT \ok + } + + +.. index:: result type, value type + pair: validation; result type + single: abstract syntax; result type +.. _valid-resulttype: + +Result Types +~~~~~~~~~~~~ + +:math:`[t^\ast]` +................ + +* Each :ref:`value type ` :math:`t_i` in the type sequence :math:`t^\ast` must be :ref:`valid `. + +* Then the result type is valid. + +.. math:: + \frac{ + (C \vdashvaltype t \ok)^\ast + }{ + C \vdashresulttype [t^\ast] \ok + } + + .. index:: limits pair: validation; limits single: abstract syntax; limits @@ -40,7 +173,7 @@ Limits \qquad (n \leq m)^? }{ - \vdashlimits \{ \LMIN~n, \LMAX~m^? \} : k + C \vdashlimits \{ \LMIN~n, \LMAX~m^? \} : k } @@ -72,10 +205,13 @@ Block Types :math:`[\valtype^?]` .................... -* The block type is valid as :ref:`function type ` :math:`[] \to [\valtype^?]`. +* The value type :math:`\valtype` must either be absent, or :ref:`valid `. + +* Then the block type is valid as :ref:`function type ` :math:`[] \to [\valtype^?]`. .. math:: \frac{ + (C \vdashvaltype \valtype \ok)^? }{ C \vdashblocktype [\valtype^?] : [] \to [\valtype^?] } @@ -89,17 +225,22 @@ Block Types Function Types ~~~~~~~~~~~~~~ -:ref:`Function types ` are always valid. +:math:`[t_1^\ast] \to [t_2^\ast]` +................................. -:math:`[t_1^n] \to [t_2^m]` -........................... +* The :ref:`result type ` :math:`[t_1^\ast]` must be :ref:`valid `. -* The function type is valid. +* The :ref:`result type ` :math:`[t_2^\ast]` must be :ref:`valid `. + +* Then the function type is valid. .. math:: \frac{ + C \vdashvaltype [t_1^\ast] \ok + \qquad + C \vdashvaltype [t_2^\ast] \ok }{ - \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok + C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok } @@ -116,13 +257,17 @@ Table Types * The limits :math:`\limits` must be :ref:`valid ` within range :math:`2^{32}-1`. +* The reference type :math:`\reftype` must be :ref:`valid `. + * Then the table type is valid. .. math:: \frac{ - \vdashlimits \limits : 2^{32} - 1 + C \vdashlimits \limits : 2^{32} - 1 + \qquad + C \vdashreftype \reftype \ok }{ - \vdashtabletype \limits~\reftype \ok + C \vdashtabletype \limits~\reftype \ok } @@ -143,9 +288,9 @@ Memory Types .. math:: \frac{ - \vdashlimits \limits : 2^{16} + C \vdashlimits \limits : 2^{16} }{ - \vdashmemtype \limits \ok + C \vdashmemtype \limits \ok } @@ -160,12 +305,15 @@ Global Types :math:`\mut~\valtype` ..................... -* The global type is valid. +* The value type :math:`\valtype` must be :ref:`valid `. + +* Then the global type is valid. .. math:: \frac{ + C \vdashreftype \valtype \ok }{ - \vdashglobaltype \mut~\valtype \ok + C \vdashglobaltype \mut~\valtype \ok } @@ -186,9 +334,9 @@ External Types .. math:: \frac{ - \vdashfunctype \functype \ok + C \vdashfunctype \functype \ok }{ - \vdashexterntype \ETFUNC~\functype \ok + C \vdashexterntype \ETFUNC~\functype \ok } :math:`\ETTABLE~\tabletype` @@ -200,9 +348,9 @@ External Types .. math:: \frac{ - \vdashtabletype \tabletype \ok + C \vdashtabletype \tabletype \ok }{ - \vdashexterntype \ETTABLE~\tabletype \ok + C \vdashexterntype \ETTABLE~\tabletype \ok } :math:`\ETMEM~\memtype` @@ -214,9 +362,9 @@ External Types .. math:: \frac{ - \vdashmemtype \memtype \ok + C \vdashmemtype \memtype \ok }{ - \vdashexterntype \ETMEM~\memtype \ok + C \vdashexterntype \ETMEM~\memtype \ok } :math:`\ETGLOBAL~\globaltype` @@ -228,226 +376,7 @@ External Types .. math:: \frac{ - \vdashglobaltype \globaltype \ok - }{ - \vdashexterntype \ETGLOBAL~\globaltype \ok - } - - -.. index:: subtyping - -Value Subtyping -~~~~~~~~~~~~~~~ - -.. index:: number type - -.. _match-numtype: - -Number Types -............ - -A :ref:`number type ` :math:`\numtype_1` matches a :ref:`number type ` :math:`\numtype_2` if and only if: - -* Both :math:`\numtype_1` and :math:`\numtype_2` are the same. - -.. math:: - ~\\[-1ex] - \frac{ - }{ - \vdashnumtypematch \numtype \matchesvaltype \numtype - } - - - -.. index:: reference type - -.. _match-reftype: - -Reference Types -............... - -A :ref:`reference type ` :math:`\reftype_1` matches a :ref:`reference type ` :math:`\reftype_2` if and only if: - -* Either both :math:`\reftype_1` and :math:`\reftype_2` are the same. - -.. math:: - ~\\[-1ex] - \frac{ - }{ - \vdashreftypematch \reftype \matchesvaltype \reftype - } - - -.. index:: value type, number type, reference type - -.. _match-valtype: - -Value Types -........... - -A :ref:`value type ` :math:`\valtype_1` matches a :ref:`value type ` :math:`\valtype_2` if and only if: - -* Either both :math:`\valtype_1` and :math:`\valtype_2` are :ref:`number types ` and :math:`\valtype_1` :ref:`matches ` :math:`\valtype_2`. - -* Or both :math:`\valtype_1` and :math:`\valtype_2` are :ref:`reference types ` and :math:`\valtype_1` :ref:`matches ` :math:`\valtype_2`. - -* Or :math:`\valtype_1` is :math:`\BOT`. - -.. math:: - ~\\[-1ex] - \frac{ - }{ - \vdashvaltypematch \BOT \matchesvaltype \valtype - } - - -.. _match-resulttype: - -Result Types -............ - -Subtyping is lifted to :ref:`result types ` in a pointwise manner. -That is, a :ref:`result type ` :math:`[t_1^\ast]` matches a :ref:`result type ` :math:`[t_2^\ast]` if and only if: - -* Every :ref:`value type ` :math:`t_1` in :math:`[t_1^\ast]` :ref:`matches ` the corresponding :ref:`value type ` :math:`t_2` in :math:`[t_2^\ast]`. - -.. math:: - ~\\[-1ex] - \frac{ - (\vdashvaltypematch t_1 \matchesvaltype t_2)^\ast - }{ - \vdashresulttypematch [t_1^\ast] \matchesresulttype [t_2^ast] - } - - -.. index:: ! matching, external type -.. _exec-import: -.. _match: - -Import Subtyping -~~~~~~~~~~~~~~~~ - -When :ref:`instantiating ` a module, -:ref:`external values ` must be provided whose :ref:`types ` are *matched* against the respective :ref:`external types ` classifying each import. -In some cases, this allows for a simple form of subtyping, as defined here. - - -.. index:: limits -.. _match-limits: - -Limits -...... - -:ref:`Limits ` :math:`\{ \LMIN~n_1, \LMAX~m_1^? \}` match limits :math:`\{ \LMIN~n_2, \LMAX~m_2^? \}` if and only if: - -* :math:`n_1` is larger than or equal to :math:`n_2`. - -* Either: - - * :math:`m_2^?` is empty. - -* Or: - - * Both :math:`m_1^?` and :math:`m_2^?` are non-empty. - - * :math:`m_1` is smaller than or equal to :math:`m_2`. - -.. math:: - ~\\[-1ex] - \frac{ - n_1 \geq n_2 - }{ - \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1^? \} \matcheslimits \{ \LMIN~n_2, \LMAX~\epsilon \} - } - \quad - \frac{ - n_1 \geq n_2 - \qquad - m_1 \leq m_2 - }{ - \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1 \} \matcheslimits \{ \LMIN~n_2, \LMAX~m_2 \} - } - - -.. _match-externtype: - -.. index:: function type -.. _match-functype: - -Functions -......... - -An :ref:`external type ` :math:`\ETFUNC~\functype_1` matches :math:`\ETFUNC~\functype_2` if and only if: - -* Both :math:`\functype_1` and :math:`\functype_2` are the same. - -.. math:: - ~\\[-1ex] - \frac{ - }{ - \vdashexterntypematch \ETFUNC~\functype \matchesexterntype \ETFUNC~\functype - } - - -.. index:: table type, limits, element type -.. _match-tabletype: - -Tables -...... - -An :ref:`external type ` :math:`\ETTABLE~(\limits_1~\reftype_1)` matches :math:`\ETTABLE~(\limits_2~\reftype_2)` if and only if: - -* Limits :math:`\limits_1` :ref:`match ` :math:`\limits_2`. - -* Both :math:`\reftype_1` and :math:`\reftype_2` are the same. - -.. math:: - \frac{ - \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 - }{ - \vdashexterntypematch \ETTABLE~(\limits_1~\reftype) \matchesexterntype \ETTABLE~(\limits_2~\reftype) - } - - -.. index:: memory type, limits -.. _match-memtype: - -Memories -........ - -An :ref:`external type ` :math:`\ETMEM~\limits_1` matches :math:`\ETMEM~\limits_2` if and only if: - -* Limits :math:`\limits_1` :ref:`match ` :math:`\limits_2`. - -.. math:: - \frac{ - \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 - }{ - \vdashexterntypematch \ETMEM~\limits_1 \matchesexterntype \ETMEM~\limits_2 - } - - -.. index:: global type, value type, mutability -.. _match-globaltype: - -Globals -....... - -An :ref:`external type ` :math:`\ETGLOBAL~(\mut_1~t_1)` matches :math:`\ETGLOBAL~(\mut_2~t_2)` if and only if: - -* Either both :math:`\mut_1` and :math:`\mut_2` are |MVAR| and :math:`t_1` and :math:`t_2` are the same. - -* Or both :math:`\mut_1` and :math:`\mut_2` are |MCONST| and :math:`t_1` :ref:`matches ` :math:`t_2`. - -.. math:: - ~\\[-1ex] - \frac{ - }{ - \vdashexterntypematch \ETGLOBAL~(\MVAR~t) \matchesexterntype \ETGLOBAL~(\MVAR~t) - } - \qquad - \frac{ - \vdashvaltypematch t_1 \matchesvaltype t_2 + C \vdashglobaltype \globaltype \ok }{ - \vdashexterntypematch \ETGLOBAL~(\MCONST~t_1) \matchesexterntype \ETGLOBAL~(\MCONST~t_2) + C \vdashexterntype \ETGLOBAL~\globaltype \ok } diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 646d8a43..471e11d7 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -148,19 +148,25 @@ let num_type s = let heap_type s = let pos = pos s in - match vs33 s with - | -0x10l -> FuncHeapType - | -0x11l -> ExternHeapType - | i when i >= 0l -> DefHeapType (SynVar i) - | _ -> error s pos "malformed heap type" + match peek s with + | Some i when i land 0xc0 = 0x40 -> + (match vs7 s with + | -0x10 -> FuncHeapType + | -0x11 -> ExternHeapType + | _ -> error s pos "malformed heap type" + ) + | _ -> + match vs33 s with + | i when i >= 0l -> DefHeapType (SynVar i) + | _ -> error s pos "malformed heap type" let ref_type s = let pos = pos s in - match vs33 s with - | -0x10l -> (Nullable, FuncHeapType) - | -0x11l -> (Nullable, ExternHeapType) - | -0x14l -> (Nullable, heap_type s) - | -0x15l -> (NonNullable, heap_type s) + match vs7 s with + | -0x10 -> (Nullable, FuncHeapType) + | -0x11 -> (Nullable, ExternHeapType) + | -0x14 -> (Nullable, heap_type s) + | -0x15 -> (NonNullable, heap_type s) | _ -> error s pos "malformed reference type" let value_type s = diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 567dcc33..051606d9 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -108,10 +108,10 @@ struct | BotHeapType -> assert false let ref_type = function - | (Nullable, FuncHeapType) -> vs32 (-0x10l) - | (Nullable, ExternHeapType) -> vs32 (-0x11l) - | (Nullable, t) -> vs33 (-0x14l); heap_type t - | (NonNullable, t) -> vs33 (-0x15l); heap_type t + | (Nullable, FuncHeapType) -> vs7 (-0x10) + | (Nullable, ExternHeapType) -> vs7 (-0x11) + | (Nullable, t) -> vs7 (-0x14); heap_type t + | (NonNullable, t) -> vs7 (-0x15); heap_type t let value_type = function | NumType t -> num_type t