Merge remote-tracking branch 'upstream/main'

Author: tlively

document/core/appendix/index-types.rst

@@ -17,7 +17,7 @@ Category                                  Constructor
 :ref:`Packed type <syntax-packtype>`      |I8|                                                   :math:`\hex{78}` (-8 as |Bs7|)
 :ref:`Packed type <syntax-packtype>`      |I16|                                                  :math:`\hex{77}` (-9 as |Bs7|)
 (reserved)                                                                                       :math:`\hex{78}` .. :math:`\hex{75}`
-:ref:`Heap type <syntax-heaptype>`        |NOEXN|                                                :math:`\hex{74}` (-14 as |Bs7|)
+:ref:`Heap type <syntax-heaptype>`        |NOEXN|                                                :math:`\hex{74}` (-12 as |Bs7|)
 :ref:`Heap type <syntax-heaptype>`        |NOFUNC|                                               :math:`\hex{73}` (-13 as |Bs7|)
 :ref:`Heap type <syntax-heaptype>`        |NOEXTERN|                                             :math:`\hex{72}` (-14 as |Bs7|)
 :ref:`Heap type <syntax-heaptype>`        |NONE|                                                 :math:`\hex{71}` (-15 as |Bs7|)

document/core/binary/instructions.rst

@@ -54,6 +54,10 @@ Control Instructions
 .. _binary-br:
 .. _binary-br_if:
 .. _binary-br_table:
+.. _binary-br_on_null:
+.. _binary-br_on_non_null:
+.. _binary-br_on_cast:
+.. _binary-br_on_cast_fail:
 .. _binary-return:
 .. _binary-call:
 .. _binary-call_ref:
@@ -65,8 +69,10 @@ Control Instructions
 .. _binary-throw_ref:
 .. _binary-try_table:
 .. _binary-catch:
+.. _binary-castop:
 
-$${grammar: Bblocktype {Binstr/block Binstr/control} Bcatch}
+$${grammar: Bblocktype {Binstr/block Binstr/control} Bcatch Bcastop}
+$${syntax-ignore: castop}
 
 .. note::
    The ${:ELSE} opcode ${:0x05} in the encoding of an ${:IF} instruction can be omitted if the following instruction sequence is empty.
@@ -140,10 +146,6 @@ $${grammar: Bmemarg Binstr/memory}
 .. index:: reference instruction
    pair: binary format; instruction
 .. _binary-instr-ref:
-.. _binary-br_on_null:
-.. _binary-br_on_non_null:
-.. _binary-br_on_cast:
-.. _binary-br_on_cast_fail:
 
 Reference Instructions
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -154,6 +156,24 @@ Generic :ref:`reference instructions <syntax-instr-ref>` are represented by sing
 .. _binary-ref.func:
 .. _binary-ref.is_null:
 .. _binary-ref.as_non_null:
+.. _binary-ref.test:
+.. _binary-ref.cast:
+
+$${grammar: {Binstr/ref}}
+
+
+.. index:: aggregate instruction
+   pair: binary format; instruction
+.. _binary-instr-aggr:
+
+Aggregate Instructions
+~~~~~~~~~~~~~~~~~~~~~~
+
+:ref:`Aggregate instructions <syntax-instr-aggr>` all use a prefix.
+
+.. _binary-ref.i31:
+.. _binary-i31.get_s:
+.. _binary-i31.get_u:
 .. _binary-struct.new:
 .. _binary-struct.new_default:
 .. _binary-struct.get:
@@ -174,17 +194,10 @@ Generic :ref:`reference instructions <syntax-instr-ref>` are represented by sing
 .. _binary-array.copy:
 .. _binary-array.init_data:
 .. _binary-array.init_elem:
-.. _binary-ref.i31:
-.. _binary-i31.get_s:
-.. _binary-i31.get_u:
-.. _binary-ref.test:
-.. _binary-ref.cast:
 .. _binary-any.convert_extern:
 .. _binary-extern.convert_any:
-.. _binary-castop:
 
-$${grammar: {Binstr/ref Binstr/struct Binstr/array Binstr/cast Binstr/extern Binstr/i31} Bcastop}
-$${syntax-ignore: castop}
+$${grammar: {Binstr/struct Binstr/array Binstr/extern Binstr/i31}}
 
 
 .. index:: numeric instruction
@@ -384,31 +397,6 @@ $${grammar: {
 
 $${grammar: {Binstr/vec-cvt}}
 
-.. math::
-   \begin{array}{llclll}
-   \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{vechaslongerinstructionnames} \\[-2ex] &&|&
-     \hex{FD}~~256{:}\Bu32 &\Rightarrow& \I16X8.\VRELAXEDSWIZZLE \\ &&|&
-     \hex{FD}~~257{:}\Bu32 &\Rightarrow& \I32X4.\VRELAXEDTRUNC\K{\_f32x4\_s} \\ &&|&
-     \hex{FD}~~258{:}\Bu32 &\Rightarrow& \I32X4.\VRELAXEDTRUNC\K{\_f32x4\_u} \\ &&|&
-     \hex{FD}~~259{:}\Bu32 &\Rightarrow& \I32X4.\VRELAXEDTRUNC\K{\_f32x4\_s\_zero} \\ &&|&
-     \hex{FD}~~260{:}\Bu32 &\Rightarrow& \I32X4.\VRELAXEDTRUNC\K{\_f32x4\_u\_zero} \\ &&|&
-     \hex{FD}~~261{:}\Bu32 &\Rightarrow& \F32X4.\VRELAXEDMADD \\ &&|&
-     \hex{FD}~~262{:}\Bu32 &\Rightarrow& \F32X4.\VRELAXEDNMADD \\ &&|&
-     \hex{FD}~~263{:}\Bu32 &\Rightarrow& \F64X2.\VRELAXEDMADD \\ &&|&
-     \hex{FD}~~264{:}\Bu32 &\Rightarrow& \F64X2.\VRELAXEDNMADD \\ &&|&
-     \hex{FD}~~265{:}\Bu32 &\Rightarrow& \I8X16.\VRELAXEDLANESELECT \\ &&|&
-     \hex{FD}~~266{:}\Bu32 &\Rightarrow& \I16X8.\VRELAXEDLANESELECT \\ &&|&
-     \hex{FD}~~267{:}\Bu32 &\Rightarrow& \I32X4.\VRELAXEDLANESELECT \\ &&|&
-     \hex{FD}~~268{:}\Bu32 &\Rightarrow& \I64X2.\VRELAXEDLANESELECT \\ &&|&
-     \hex{FD}~~269{:}\Bu32 &\Rightarrow& \F32X4.\VRELAXEDMIN \\ &&|&
-     \hex{FD}~~270{:}\Bu32 &\Rightarrow& \F32X4.\VRELAXEDMAX \\ &&|&
-     \hex{FD}~~271{:}\Bu32 &\Rightarrow& \F64X2.\VRELAXEDMIN \\ &&|&
-     \hex{FD}~~272{:}\Bu32 &\Rightarrow& \F64X2.\VRELAXEDMAX \\ &&|&
-     \hex{FD}~~273{:}\Bu32 &\Rightarrow& \I16X8.\VRELAXEDQ15MULR\K{\_s} \\ &&|&
-     \hex{FD}~~274{:}\Bu32 &\Rightarrow& \I16X8.\VRELAXEDDOT\K{\_i8x16\_i7x16\_s} \\ &&|&
-     \hex{FD}~~275{:}\Bu32 &\Rightarrow& \I16X8.\VRELAXEDDOT\K{\_i8x16\_i7x16\_add\_s} \\
-   \end{array}
-
 
 .. index:: expression
    pair: binary format; expression

document/core/syntax/instructions.rst

@@ -61,15 +61,19 @@ If missing, the operands must be of :ref:`numeric <syntax-numtype>` or :ref:`vec
 .. _syntax-br_on_non_null:
 .. _syntax-br_on_cast:
 .. _syntax-br_on_cast_fail:
-.. _syntax-return:
 .. _syntax-call:
+.. _syntax-call_ref:
 .. _syntax-call_indirect:
-.. _syntax-instrs:
-.. _syntax-instr-control:
+.. _syntax-return:
+.. _syntax-return_call:
+.. _syntax-return_call_ref:
+.. _syntax-return_call_indirect:
 .. _syntax-throw:
 .. _syntax-throw_ref:
 .. _syntax-try_table:
 .. _syntax-catch:
+.. _syntax-instrs:
+.. _syntax-instr-control:
 .. _exception:
 
 Control Instructions
@@ -284,6 +288,7 @@ while the latter performs a downcast and :ref:`traps <trap>` if the operand's ty
 .. _syntax-i31.get_u:
 .. _syntax-any.convert_extern:
 .. _syntax-extern.convert_any:
+.. _syntax-instr-aggr:
 .. _syntax-instr-struct:
 .. _syntax-instr-array:
 .. _syntax-instr-i31:

document/core/text/instructions.rst

@@ -201,6 +201,22 @@ Reference Instructions
 .. _text-ref.func:
 .. _text-ref.is_null:
 .. _text-ref.as_non_null:
+.. _text-ref.test:
+.. _text-ref.cast:
+
+$${grammar: {Tplaininstr_/ref}}
+
+
+.. index:: aggregate instruction
+   pair: text format; instruction
+.. _text-instr-aggr:
+
+Aggregate Instructions
+~~~~~~~~~~~~~~~~~~~~~~
+
+.. _text-ref.i31:
+.. _text-i31.get_s:
+.. _text-i31.get_u:
 .. _text-struct.new:
 .. _text-struct.new_default:
 .. _text-struct.get:
@@ -221,15 +237,10 @@ Reference Instructions
 .. _text-array.copy:
 .. _text-array.init_data:
 .. _text-array.init_elem:
-.. _text-ref.i31:
-.. _text-i31.get_s:
-.. _text-i31.get_u:
-.. _text-ref.test:
-.. _text-ref.cast:
 .. _text-any.convert_extern:
 .. _text-extern.convert_any:
 
-$${grammar: {Tplaininstr_/ref Tplaininstr_/i31 Tplaininstr_/struct Tplaininstr_/array Tplaininstr_/extern}}
+$${grammar: {Tplaininstr_/i31 Tplaininstr_/struct Tplaininstr_/array Tplaininstr_/extern}}
 
 
 .. index:: numeric instruction

document/core/valid/matching.rst

@@ -167,7 +167,7 @@ Limits
 
 $${rule-prose: Limits_sub}
 
-$${rule: Limits_sub}
+$${rule: {Limits_sub/*}}
 
 
 .. index:: tag type

interpreter/valid/valid.ml

@@ -904,7 +904,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
     require (i < Lib.List32.length fts) e.at
       ("unknown field " ^ I32.to_string_u i);
     let FieldT (mut, st) = Lib.List32.nth fts i in
-    require (mut == Var) e.at "field is immutable";
+    require (mut == Var) e.at "immutable field";
     let t = unpacked_storagetype st in
     [RefT (Null, UseHT (Inexact, Def (type_ c x))); t] --> [], []
 
@@ -946,7 +946,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
 
   | ArraySet x ->
     let FieldT (mut, st) = array_type c x in
-    require (mut == Var) e.at "array is immutable";
+    require (mut == Var) e.at "immutable array";
     let t = unpacked_storagetype st in
     [RefT (Null, UseHT (Inexact, Def (type_ c x))); NumT I32T; t] --> [], []
 
@@ -956,19 +956,19 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
   | ArrayCopy (x, y) ->
     let FieldT (mutd, std) = array_type c x in
     let FieldT (_muts, sts) = array_type c y in
-    require (mutd = Var) e.at "array is immutable";
+    require (mutd = Var) e.at "immutable array";
     require (match_storagetype c.types sts std) e.at "array types do not match";
     [RefT (Null, UseHT (Inexact, Def (type_ c x))); NumT I32T; RefT (Null, UseHT (Inexact, Def (type_ c y))); NumT I32T; NumT I32T] --> [], []
 
   | ArrayFill x ->
     let FieldT (mut, st) = array_type c x in
-    require (mut = Var) e.at "array is immutable";
+    require (mut = Var) e.at "immutable array";
     let t = unpacked_storagetype st in
     [RefT (Null, UseHT (Inexact, Def (type_ c x))); NumT I32T; t; NumT I32T] --> [], []
 
   | ArrayInitData (x, y) ->
     let FieldT (mut, st) = array_type c x in
-    require (mut = Var) e.at "array is immutable";
+    require (mut = Var) e.at "immutable array";
     let () = data c y in
     let t = unpacked_storagetype st in
     require (is_numtype t || is_vectype t) x.at
@@ -977,7 +977,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
 
   | ArrayInitElem (x, y) ->
     let FieldT (mut, st) = array_type c x in
-    require (mut = Var) e.at "array is immutable";
+    require (mut = Var) e.at "immutable array";
     let rt = elem c y in
     require (match_valtype c.types (RefT rt) (unpacked_storagetype st)) x.at
       ("type mismatch: element segment's type " ^ string_of_reftype rt ^

specification/wasm-3.0/1.3-syntax.instructions.spectec

@@ -165,14 +165,14 @@ syntax vcvtop__(Jnn_1 X M_1, Jnn_2 X M_2) =
   | EXTEND half sx hint(show EXTEND#_#%#_#%)
     -- if $lsizenn2(Jnn_2) = $(2 * $lsizenn1(Jnn_1))
 syntax vcvtop__(Jnn_1 X M_1, Fnn_2 X M_2) =
-  | CONVERT half? sx hint(show CONVERT#_#%#_#%) hint(show CONVERT#_#%)
+  | CONVERT half? sx hint(show CONVERT#_#%) hint(show CONVERT#_#%#_#%)
     -- if $sizenn2(Fnn_2) = $lsizenn1(Jnn_1) = `32 /\ half? = eps
        \/ $sizenn2(Fnn_2) = $(2 * $lsizenn1(Jnn_1)) /\ half? = LOW
 syntax vcvtop__(Fnn_1 X M_1, Jnn_2 X M_2) =
-  | TRUNC_SAT sx zero? hint(show TRUNC_SAT#_#%#_#%) hint(show TRUNC_SAT#_#%)
+  | TRUNC_SAT sx zero? hint(show TRUNC_SAT#_#%) hint(show TRUNC_SAT#_#%#_#%)
     -- if $sizenn1(Fnn_1) = $lsizenn2(Jnn_2) = `32 /\ zero? = eps
        \/ $sizenn1(Fnn_1) = $(2 * $lsizenn2(Jnn_2)) /\ zero? = ZERO
-  | RELAXED_TRUNC sx zero? hint(show RELAXED_TRUNC#_#%#_#%) hint(show RELAXED_TRUNC#_#%)
+  | RELAXED_TRUNC sx zero? hint(show RELAXED_TRUNC#_#%) hint(show RELAXED_TRUNC#_#%#_#%)
     -- if $sizenn1(Fnn_1) = $lsizenn2(Jnn_2) = `32 /\ zero? = eps
        \/ $sizenn1(Fnn_1) = $(2 * $lsizenn2(Jnn_2)) /\ zero? = ZERO
 syntax vcvtop__(Fnn_1 X M_1, Fnn_2 X M_2) =

specification/wasm-3.0/2.2-validation.subtyping.spectec

@@ -196,10 +196,15 @@ relation Tabletype_sub: context |- tabletype <: tabletype    hint(name "S-table"
 relation Externtype_sub: context |- externtype <: externtype hint(name "S-extern") hint(macro "%externtypematch")
 
 
-rule Limits_sub:
-  C |- `[n_1 .. m_1] <: `[n_2 .. m_2]
+rule Limits_sub/max:
+  C |- `[n_1 .. m_1] <: `[n_2 .. m_2?]
   -- if n_1 >= n_2
-  -- if m_1 <= m_2
+  -- (if m_1 <= m_2)?
+
+rule Limits_sub/eps:
+  C |- `[n_1 .. eps] <: `[n_2 .. eps]
+  -- if n_1 >= n_2
+
 
 rule Tagtype_sub:
   C |- deftype_1 <: deftype_2

specification/wasm-3.0/5.3-binary.instructions.spectec

@@ -15,6 +15,14 @@ grammar Binstr/parametric : instr =
 
 ;; Control instructions
 
+syntax castop = (null?, null?)
+
+grammar Bcastop : castop =
+  | 0x00 => (eps, eps)
+  | 0x01 => (NULL, eps)
+  | 0x02 => (eps, NULL)
+  | 0x03 => (NULL, NULL)
+
 grammar Bblocktype : blocktype =
   | 0x40 => _RESULT eps
   | t:Bvaltype => _RESULT t
@@ -39,7 +47,15 @@ grammar Binstr/control : instr = ...
   | 0x11 y:Btypeidx x:Btableidx => CALL_INDIRECT x (_IDX y)
   | 0x12 x:Bfuncidx => RETURN_CALL x
   | 0x13 y:Btypeidx x:Btableidx => RETURN_CALL_INDIRECT x (_IDX y)
+  | 0x14 x:Btypeidx => CALL_REF (_IDX x)
+  | 0x15 x:Btypeidx => RETURN_CALL_REF (_IDX x)
   | 0x1F bt:Bblocktype c*:Blist(Bcatch) (in:Binstr)* 0x0B => TRY_TABLE bt c* in*
+  | 0xD5 l:Blabelidx => BR_ON_NULL l
+  | 0xD6 l:Blabelidx => BR_ON_NON_NULL l
+  | 0xFB 24:Bu32 (null_1?, null_2?):Bcastop
+    l:Blabelidx ht_1:Bheaptype ht_2:Bheaptype => BR_ON_CAST l (REF null_1? ht_1) (REF null_2? ht_2)
+  | 0xFB 25:Bu32 (null_1?, null_2?):Bcastop
+    l:Blabelidx ht_1:Bheaptype ht_2:Bheaptype => BR_ON_CAST_FAIL l (REF null_1? ht_1) (REF null_2? ht_2)
   | ...
 
 grammar Bcatch : catch =
@@ -120,22 +136,16 @@ grammar Binstr/memory : instr = ...
 
 ;; Reference instructions
 
-syntax castop = (null?, null?)
-
-grammar Bcastop : castop =
-  | 0x00 => (eps, eps)
-  | 0x01 => (NULL, eps)
-  | 0x02 => (eps, NULL)
-  | 0x03 => (NULL, NULL)
-
 grammar Binstr/ref : instr = ...
   | 0xD0 ht:Bheaptype => REF.NULL ht
   | 0xD1 => REF.IS_NULL
   | 0xD2 x:Bfuncidx => REF.FUNC x
   | 0xD3 => REF.EQ
   | 0xD4 => REF.AS_NON_NULL
-  | 0xD5 l:Blabelidx => BR_ON_NULL l
-  | 0xD6 l:Blabelidx => BR_ON_NON_NULL l
+  | 0xFB 20:Bu32 ht:Bheaptype => REF.TEST (REF ht)
+  | 0xFB 21:Bu32 ht:Bheaptype => REF.TEST (REF NULL ht)
+  | 0xFB 22:Bu32 ht:Bheaptype => REF.CAST (REF ht)
+  | 0xFB 23:Bu32 ht:Bheaptype => REF.CAST (REF NULL ht)
   | ...
 
 grammar Binstr/struct : instr = ...
@@ -164,17 +174,6 @@ grammar Binstr/array : instr = ...
   | 0xFB 19:Bu32 x:Btypeidx y:Belemidx => ARRAY.INIT_ELEM x y
   | ...
 
-grammar Binstr/cast : instr = ...
-  | 0xFB 20:Bu32 ht:Bheaptype => REF.TEST (REF ht)
-  | 0xFB 21:Bu32 ht:Bheaptype => REF.TEST (REF NULL ht)
-  | 0xFB 22:Bu32 ht:Bheaptype => REF.CAST (REF ht)
-  | 0xFB 23:Bu32 ht:Bheaptype => REF.CAST (REF NULL ht)
-  | 0xFB 24:Bu32 (null_1?, null_2?):Bcastop
-    l:Blabelidx ht_1:Bheaptype ht_2:Bheaptype => BR_ON_CAST l (REF null_1? ht_1) (REF null_2? ht_2)
-  | 0xFB 25:Bu32 (null_1?, null_2?):Bcastop
-    l:Blabelidx ht_1:Bheaptype ht_2:Bheaptype => BR_ON_CAST_FAIL l (REF null_1? ht_1) (REF null_2? ht_2)
-  | ...
-
 grammar Binstr/extern : instr = ...
   | 0xFB 26:Bu32 => ANY.CONVERT_EXTERN
   | 0xFB 27:Bu32 => EXTERN.CONVERT_ANY
@@ -369,7 +368,7 @@ grammar Binstr/num-cvt : instr = ...
   | 0xB8 => CVTOP F64 I32 CONVERT U
   | 0xB9 => CVTOP F64 I64 CONVERT S
   | 0xBA => CVTOP F64 I64 CONVERT U
-  | 0xBB => CVTOP F32 F64 PROMOTE
+  | 0xBB => CVTOP F64 F32 PROMOTE
   | 0xBC => CVTOP I32 F32 REINTERPRET
   | 0xBD => CVTOP I64 F64 REINTERPRET
   | 0xBE => CVTOP F32 I32 REINTERPRET

spectec/Makefile

@@ -23,10 +23,15 @@ ROOTDIR = ..
 INTERPRETERDIR = $(ROOTDIR)/interpreter
 CLONEDIR = src/backend-interpreter/reference-interpreter
 CLONERM = dune-project jslib
+OPAMPACKAGES = zarith menhir mdx
+
 
 .PHONY: exe
 
-exe: $(CLONEDIR)
+packages:
+	opam install $(OPAMPACKAGES)
+
+exe: $(CLONEDIR) packages
 	rm -f ./$(NAME)
 	dune build $(SRCDIR)/$(EXE)
 	ln -f $(OUTDIR)/$(EXE) ./$(NAME)