Skip to content

Commit

Permalink
Merge pull request #389 from WebAssembly/spec.indices
Browse files Browse the repository at this point in the history
Extend type/instr/rule indices
  • Loading branch information
rossberg authored Jul 23, 2023
2 parents 901e249 + 0246567 commit 153ff9c
Show file tree
Hide file tree
Showing 6 changed files with 116 additions and 44 deletions.
35 changes: 33 additions & 2 deletions document/core/appendix/index-instructions.py
Original file line number Diff line number Diff line change
Expand Up @@ -282,7 +282,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
Instruction(r'\REFFUNC~x', r'\hex{D2}', r'[] \to [\FUNCREF]', r'valid-ref.func', r'exec-ref.func'),
Instruction(r'\REFASNONNULL', r'\hex{D3}', r'[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]', r'valid-ref.as_non_null', r'exec-ref.as_non_null'),
Instruction(r'\BRONNULL~l', r'\hex{D4}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]', r'valid-br_on_null', r'exec-br_on_null'),
Instruction(None, r'\hex{D5}'),
Instruction(r'\REFEQ', r'\hex{D5}', r'[\EQREF~\EQREF] \to [\I32]', r'valid-ref.eq', r'exec-ref.eq'),
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}'),
Expand Down Expand Up @@ -320,7 +320,37 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
Instruction(None, r'\hex{F8}'),
Instruction(None, r'\hex{F9}'),
Instruction(None, r'\hex{FA}'),
Instruction(None, r'\hex{FB}'),
Instruction(r'\STRUCTNEW~x', r'\hex{FB}~\hex{01}', r'[t^\ast] \to [(\REF~x)]', r'valid-struct.new', r'exec-struct.new'),
Instruction(r'\STRUCTNEWDEFAULT~x', r'\hex{FB}~\hex{02}', r'[] \to [(\REF~x)]', r'valid-struct.new_default', r'exec-struct.new_default'),
Instruction(r'\STRUCTGET~x~i', r'\hex{FB}~\hex{03}', r'[(\REF~\NULL~x)] \to [t]', r'valid-struct.get', r'exec-struct.get'),
Instruction(r'\STRUCTGETS~x~i', r'\hex{FB}~\hex{04}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'),
Instruction(r'\STRUCTGETU~x~i', r'\hex{FB}~\hex{05}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'),
Instruction(r'\STRUCTSET~x~i', r'\hex{FB}~\hex{06}', r'[(\REF~\NULL~x)~t] \to []', r'valid-struct.set', r'exec-struct.set'),
Instruction(r'\ARRAYFILL~x', r'\hex{FB}~\hex{0F}', r'[(\REF~\NULL~x)~\I32~t~\I32] \to []', r'valid-array.fill', r'exec-array.fill'),
Instruction(r'\ARRAYNEW~x', r'\hex{FB}~\hex{11}', r'[t] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'),
Instruction(r'\ARRAYNEWDEFAULT~x', r'\hex{FB}~\hex{12}', r'[] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'),
Instruction(r'\ARRAYGET~x', r'\hex{FB}~\hex{13}', r'[(\REF~\NULL~x)~\I32] \to [t]', r'valid-array.get', r'exec-array.get'),
Instruction(r'\ARRAYGETS~x', r'\hex{FB}~\hex{14}', r'[(\REF~\NULL~x)~\I32] \to [\I32]', r'valid-array.get', r'exec-array.get'),
Instruction(r'\ARRAYGETU~x', r'\hex{FB}~\hex{15}', r'[(\REF~\NULL~x)~\I32] \to [\I32]', r'valid-array.get', r'exec-array.get'),
Instruction(r'\ARRAYSET~x', r'\hex{FB}~\hex{16}', r'[(\REF~\NULL~x)~\I32~t] \to []', r'valid-array.set', r'exec-array.set'),
Instruction(r'\ARRAYLEN', r'\hex{FB}~\hex{17}', r'[\ARRAYREF] \to []', r'valid-array.len', r'exec-array.len'),
Instruction(r'\ARRAYCOPY~x~y', r'\hex{FB}~\hex{18}', r'[(\REF~\NULL~x)~\I32~(\REF~\NULL~y)~\I32~\I32] \to []', r'valid-array.copy', r'exec-array.copy'),
Instruction(r'\ARRAYNEWFIXED~x~n', r'\hex{FB}~\hex{19}', r'[t^n] \to [(\REF~x)]', r'valid-array.new_fixed', r'exec-array.new_fixed'),
Instruction(r'\ARRAYNEWDATA~x~y', r'\hex{FB}~\hex{1B}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_data', r'exec-array.new_data'),
Instruction(r'\ARRAYNEWELEM~x~y', r'\hex{FB}~\hex{1C}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_elem', r'exec-array.new_elem'),
Instruction(r'\I31NEW', r'\hex{FB}~\hex{20}', r'[\I32] \to [\I31REF]', r'valid-i31.new', r'exec-i31.new'),
Instruction(r'\I31GETS', r'\hex{FB}~\hex{21}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'),
Instruction(r'\I31GETU', r'\hex{FB}~\hex{22}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'),
Instruction(r'\REFTEST~(\REF~t)', r'\hex{FB}~\hex{40}', r"[(\REF~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'),
Instruction(r'\REFCAST~(\REF~t)', r'\hex{FB}~\hex{41}', r"[(\REF~t')] \to [(\REF~t)]", r'valid-ref.test', r'exec-ref.test'),
Instruction(r'\REFTEST~(\REF~\NULL~t)', r'\hex{FB}~\hex{48}', r"[(REF~\NULL~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'),
Instruction(r'\REFCAST~(\REF~\NULL~t)', r'\hex{FB}~\hex{49}', r"[(\REF~\NULL~t')] \to [(\REF~\NULL~t)]", r'valid-ref.cast', r'exec-ref.cast'),
Instruction(r'\BRONCAST~t_1~t_2', r'\hex{FB}~\hex{4E}', r'[t_1] \to [t_1\reftypediff t_2]', r'valid-br_on_cast', r'exec-br_on_cast'),
Instruction(r'\BRONCASTFAIL~t_1~t_2', r'\hex{FB}~\hex{4F}', r'[t_1] \to [t_2]', r'valid-br_on_cast_fail', r'exec-br_on_cast_fail'),
Instruction(r'\ARRAYINITDATA~x~y', r'\hex{FB}~\hex{54}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_data', r'exec-array.init_data'),
Instruction(r'\ARRAYINITELEM~x~y', r'\hex{FB}~\hex{55}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_elem', r'exec-array.init_elem'),
Instruction(r'\EXTERNINTERNALIZE', r'\hex{FB}~\hex{70}', r'[\EXTERNREF] \to [\ANYREF]', r'valid-extern.internalize', r'exec-extern.internalize'),
Instruction(r'\EXTERNEXTERNALIZE', r'\hex{FB}~\hex{71}', r'[\ANYREF] \to [\EXTERNREF]', r'valid-extern.externalize', r'exec-extern.externalize'),
Instruction(r'\I32.\TRUNC\K{\_sat\_}\F32\K{\_s}', r'\hex{FC}~\hex{00}', r'[\F32] \to [\I32]', r'valid-cvtop', r'exec-cvtop', r'op-trunc_sat_s'),
Instruction(r'\I32.\TRUNC\K{\_sat\_}\F32\K{\_u}', r'\hex{FC}~\hex{01}', r'[\F32] \to [\I32]', r'valid-cvtop', r'exec-cvtop', r'op-trunc_sat_u'),
Instruction(r'\I32.\TRUNC\K{\_sat\_}\F64\K{\_s}', r'\hex{FC}~\hex{02}', r'[\F64] \to [\I32]', r'valid-cvtop', r'exec-cvtop', r'op-trunc_sat_s'),
Expand Down Expand Up @@ -578,6 +608,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
]



def ColumnWidth(n):
return max([len(instr[n]) for instr in INSTRUCTIONS])

Expand Down
46 changes: 37 additions & 9 deletions document/core/appendix/index-rules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -4,35 +4,55 @@ Index of Semantic Rules
-----------------------


.. index:: validation
.. index:: validation, type
.. _index-valid:

Typing of Static Constructs
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Well-formedness of Types
~~~~~~~~~~~~~~~~~~~~~~~~

=============================================== ===============================================================================
Construct Judgement
=============================================== ===============================================================================
:ref:`Limits <valid-limits>` :math:`C \vdashlimits \limits : k`
:ref:`Numeric type <valid-numtype>` :math:`C \vdashnumtype \numtype \ok`
:ref:`Vector type <valid-vectype>` :math:`C \vdashvectype \vectype \ok`
:ref:`Heap type <valid-heaptype>` :math:`C \vdashheaptype \heaptype \ok`
:ref:`Reference type <valid-reftype>` :math:`C \vdashreftype \reftype \ok`
:ref:`Value type <valid-valtype>` :math:`C \vdashvaltype \valtype \ok`
:ref:`Packed type <valid-packedtype>` :math:`C \vdashpackedtype \packedtype \ok`
:ref:`Storage type <valid-storagetype>` :math:`C \vdashstoragetype \storagetype \ok`
:ref:`Field type <valid-fieldtype>` :math:`C \vdashfieldtype \fieldtype \ok`
:ref:`Result type <valid-resulttype>` :math:`C \vdashresulttype \resulttype \ok`
:ref:`Instruction type <valid-instrtype>` :math:`C \vdashinstrtype \instrtype \ok`
:ref:`Function type <valid-functype>` :math:`C \vdashfunctype \functype \ok`
:ref:`Structure type <valid-structtype>` :math:`C \vdashstructtype \structtype \ok`
:ref:`Array type <valid-arraytype>` :math:`C \vdasharraytype \arraytype \ok`
:ref:`Compound type <valid-comptype>` :math:`C \vdashcomptype \comptype \ok`
:ref:`Sub type <valid-subtype>` :math:`C \vdashsubtype \subtype \ok`
:ref:`Recursive type <valid-rectype>` :math:`C \vdashrectype \rectype \ok`
:ref:`Defined type <valid-deftype>` :math:`C \vdashdeftype \deftype \ok`
:ref:`Block type <valid-blocktype>` :math:`C \vdashblocktype \blocktype : \instrtype`
:ref:`Instruction type <valid-instrtype>` :math:`C \vdashinstrtype \instrtype \ok`
:ref:`Table type <valid-tabletype>` :math:`C \vdashtabletype \tabletype \ok`
:ref:`Memory type <valid-memtype>` :math:`C \vdashmemtype \memtype \ok`
:ref:`Global type <valid-globaltype>` :math:`C \vdashglobaltype \globaltype \ok`
:ref:`External type <valid-externtype>` :math:`C \vdashexterntype \externtype \ok`
:ref:`Type definitions <valid-type>` :math:`C \vdashtypes \type^\ast \ok`
=============================================== ===============================================================================


Typing of Static Constructs
~~~~~~~~~~~~~~~~~~~~~~~~~~~

=============================================== ===============================================================================
Construct Judgement
=============================================== ===============================================================================
:ref:`Instruction <valid-instr>` :math:`S;C \vdashinstr \instr : \functype`
:ref:`Instruction sequence <valid-instr-seq>` :math:`S;C \vdashinstrseq \instr^\ast : \functype`
:ref:`Expression <valid-expr>` :math:`C \vdashexpr \expr : \resulttype`
:ref:`Function <valid-func>` :math:`C \vdashfunc \func : \functype`
:ref:`Local <valid-local>` :math:`C \vdashlocal \local : \localtype`
:ref:`Table <valid-table>` :math:`C \vdashtable \table : \tabletype`
:ref:`Memory <valid-mem>` :math:`C \vdashmem \mem : \memtype`
:ref:`Limits <valid-limits>` :math:`C \vdashlimits \limits : k`
:ref:`Global <valid-global>` :math:`C \vdashglobal \global : \globaltype`
:ref:`Element segment <valid-elem>` :math:`C \vdashelem \elem : \reftype`
:ref:`Element mode <valid-elemmode>` :math:`C \vdashelemmode \elemmode : \reftype`
Expand Down Expand Up @@ -97,22 +117,30 @@ Construct Judgement
Matching
~~~~~~~~

=============================================== ===============================================================================
=============================================== ==================================================================================
Construct Judgement
=============================================== ===============================================================================
=============================================== ==================================================================================
:ref:`Number type <match-numtype>` :math:`C \vdashnumtypematch \numtype_1 \matchesnumtype \numtype_2`
:ref:`Vector type <match-vectype>` :math:`C \vdashvectypematch \vectype_1 \matchesvectype \vectype_2`
:ref:`Heap type <match-heaptype>` :math:`C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2`
:ref:`Reference type <match-reftype>` :math:`C \vdashreftypematch \reftype_1 \matchesreftype \reftype_2`
:ref:`Value type <match-valtype>` :math:`C \vdashvaltypematch \valtype_1 \matchesvaltype \valtype_2`
:ref:`Packed type <match-packedtype>` :math:`C \vdashpackedtypematch \packedtype_1 \matchespackedtype \packedtype_2`
:ref:`Storage type <match-storagetype>` :math:`C \vdashstoragetypematch \storagetype_1 \matchesstoragetype \storagetype_2`
:ref:`Field type <match-fieldtype>` :math:`C \vdashfieldtypematch \fieldtype_1 \matchesfieldtype \fieldtype_2`
:ref:`Result type <match-resulttype>` :math:`C \vdashresulttypematch \resulttype_1 \matchesresulttype \resulttype_2`
:ref:`Instruction type <match-instrtype>` :math:`C \vdashinstrtypematch \instrtype_1 \matchesinstrtype \instrtype_2`
:ref:`Function type <match-functype>` :math:`C \vdashfunctypematch \functype_1 \matchesfunctype \functype_2`
:ref:`Structure type <match-structtype>` :math:`C \vdashstructtypematch \structtype_1 \matchesstructtype \structtype_2`
:ref:`Array type <match-arraytype>` :math:`C \vdasharraytypematch \arraytype_1 \matchesarraytype \arraytype_2`
:ref:`Compound type <match-comptype>` :math:`C \vdashcomptypematch \comptype_1 \matchescomptype \comptype_2`
:ref:`Defined type <match-deftype>` :math:`C \vdashdeftypematch \deftype_1 \matchesdeftype \deftype_2`
:ref:`Table type <match-tabletype>` :math:`C \vdashtabletypematch \tabletype_1 \matchestabletype \tabletype_2`
:ref:`Memory type <match-memtype>` :math:`C \vdashmemtypematch \memtype_1 \matchesmemtype \memtype_2`
:ref:`Global type <match-globaltype>` :math:`C \vdashglobaltypematch \globaltype_1 \matchesglobaltype \globaltype_2`
:ref:`External type <match-externtype>` :math:`C \vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2`
:ref:`Limits <match-limits>` :math:`C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2`
=============================================== ===============================================================================
=============================================== ==================================================================================


Store Extension
Expand All @@ -125,7 +153,7 @@ Construct Judgement
:ref:`Table instance <extend-tableinst>` :math:`\vdashtableinstextends \tableinst_1 \extendsto \tableinst_2`
:ref:`Memory instance <extend-meminst>` :math:`\vdashmeminstextends \meminst_1 \extendsto \meminst_2`
:ref:`Global instance <extend-globalinst>` :math:`\vdashglobalinstextends \globalinst_1 \extendsto \globalinst_2`
:ref:`Element instance <extend-eleminst>` :math:`\vdasheleminstextends \eleminst_1 \extendsto \eleminst_2`
:ref:`Element instance <extend-eleminst>` :math:`\vdasheleminstextends \eleminst_1 \extendsto \eleminst_2`
:ref:`Data instance <extend-datainst>` :math:`\vdashdatainstextends \datainst_1 \extendsto \datainst_2`
:ref:`Store <extend-store>` :math:`\vdashstoreextends \store_1 \extendsto \store_2`
=============================================== ===============================================================================
Expand Down
Loading

0 comments on commit 153ff9c

Please sign in to comment.