Convert binary instruction section

.github/workflows/ci-interpreter.yml

@@ -31,6 +31,6 @@ jobs:
       - name: Build interpreter
         run: cd interpreter && opam exec make
       - name: Run tests
-        # TODO: reactiate node once it supports all of Wasm 3.0
+        # TODO: reactivate node once it supports all of Wasm 3.0
         # run: cd interpreter && opam exec make JS=node ci
         run: cd interpreter && opam exec make ci

document/core/exec/instructions.rst

@@ -45,7 +45,7 @@ $${rule-prose: exec/select}
 $${rule: {Step_pure/select-*}}
 
 .. note::
-   In future versions of WebAssembly, |SELECT| may allow more than one value per choice.
+   In future versions of WebAssembly, ${:SELECT} may allow more than one value per choice.
 
 
 .. index:: numeric instruction, determinism, trap, NaN, value, value type

document/core/syntax/instructions.rst

@@ -63,7 +63,7 @@ Numeric Instructions
 Numeric instructions provide basic operations over numeric :ref:`values <syntax-value>` of specific :ref:`type <syntax-numtype>`.
 These operations closely match respective operations available in hardware.
 
-$${syntax: {sz sx} num_ instr/num unop_ binop_ testop_ relop_ cvtop}
+$${syntax: {sz sx} num_ instr/num unop_ binop_ testop_ relop_ cvtop_}
 
 Numeric instructions are divided by :ref:`number type <syntax-numtype>`.
 For each type, several subcategories can be distinguished:
@@ -445,6 +445,7 @@ The ${:ELEM.DROP} instruction prevents further use of a passive element segment.
 .. _syntax-loadn:
 .. _syntax-storen:
 .. _syntax-memarg:
+.. _syntax-loadop:
 .. _syntax-vloadop:
 .. _syntax-lanewidth:
 .. _syntax-instr-memory:
@@ -454,7 +455,7 @@ Memory Instructions
 
 Instructions in this group are concerned with linear :ref:`memory <syntax-mem>`.
 
-$${syntax: memarg vloadop {instr/memory instr/data}}
+$${syntax: memarg loadop_ vloadop_ {instr/memory instr/data}}
 
 Memory is accessed with ${:LOAD} and ${:STORE} instructions for the different :ref:`number types <syntax-numtype>` and `vector types <syntax-vectype>`.
 They all take a :ref:`memory index <syntax-memidx>` and a *memory argument* ${:memarg} that contains an address *offset* and the expected *alignment* (expressed as the exponent of a power of 2).

document/core/util/macros.def

@@ -196,8 +196,11 @@
 .. |F32| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{f\scriptstyle32}}
 .. |F64| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{f\scriptstyle64}}
 .. |V128| mathdef:: \xref{syntax/types}{syntax-vectype}{\K{v\scriptstyle128}}
+.. |INX| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{i}}
 .. |IN| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{i}\scriptstyle\kern-0.1emN}
+.. |FNX| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{f}}
 .. |FN| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{f}\scriptstyle\kern-0.1emN}
+.. |VNX| mathdef:: \xref{syntax/types}{syntax-vectype}{\K{v}}
 .. |VN| mathdef:: \xref{syntax/types}{syntax-vectype}{\K{v}\scriptstyle\kern-0.1emN}
 
 .. |ANYREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{anyref}}
@@ -730,11 +733,13 @@
 .. |viminmaxop| mathdef:: \xref{syntax/instructions}{syntax-vbinop}{\X{viminmaxop}}
 .. |visatbinop| mathdef:: \xref{syntax/instructions}{syntax-vbinop}{\X{visatbinop}}
 
+.. |loadop| mathdef:: \xref{syntax/instructions}{syntax-loadop}{\X{loadop}}
 .. |vloadop| mathdef:: \xref{syntax/instructions}{syntax-vloadop}{\X{vloadop}}
 
 .. |sx| mathdef:: \xref{syntax/instructions}{syntax-sx}{\X{sx}}
 .. |sz| mathdef:: \xref{syntax/instructions}{syntax-sz}{\X{sz}}
 .. |half| mathdef:: \xref{syntax/instructions}{syntax-half}{\X{half}}
+.. |zero| mathdef:: \xref{syntax/instructions}{syntax-zero}{\X{zero}}
 .. |memarg| mathdef:: \xref{syntax/instructions}{syntax-memarg}{\X{memarg}}
 .. |laneidx| mathdef:: \xref{syntax/instructions}{syntax-laneidx}{\X{laneidx}}
 
@@ -880,7 +885,7 @@
 
 .. |Bmemarg| mathdef:: \xref{binary/instructions}{binary-memarg}{\B{memarg}}
 .. |Bblocktype| mathdef:: \xref{binary/instructions}{binary-blocktype}{\B{blocktype}}
-.. |Bcastflags| mathdef:: \xref{binary/instructions}{binary-castflags}{\B{castflags}}
+.. |Bcastop| mathdef:: \xref{binary/instructions}{binary-castop}{\B{castop}}
 
 .. |Binstr| mathdef:: \xref{binary/instructions}{binary-instr}{\B{instr}}
 .. |Bexpr| mathdef:: \xref{binary/instructions}{binary-expr}{\B{expr}}

spectec/spec/wasm-3.0/1-syntax.watsup

@@ -343,7 +343,7 @@ syntax sz hint(desc "pack size") = `8 | `16 | `32 | `64
 syntax sx hint(desc "signedness") = U | S
 
 syntax unop_(numtype)
-syntax unop_(Inn) = CLZ | CTZ | POPCNT | EXTEND n
+syntax unop_(Inn) = CLZ | CTZ | POPCNT | EXTEND sz hint(show EXTEND#%#_#S) -- if $(sz < $sizenn(Inn))
 syntax unop_(Fnn) = ABS | NEG | SQRT | CEIL | FLOOR | TRUNC | NEAREST
 
 syntax binop_(numtype)
@@ -365,8 +365,10 @@ syntax relop_(Inn) =
 syntax relop_(Fnn) =
   | EQ | NE | LT | GT | LE | GE
 
-;; TODO: constrain CONVERT_SAT and REINTERPRET
-syntax cvtop = CONVERT | CONVERT_SAT | REINTERPRET
+syntax cvtop_(numtype_1, numtype_2) =
+  | CONVERT
+  | CONVERT_SAT  -- if numtype_1 = Inn /\ numtype_2 = Fnn
+  | REINTERPRET  -- if $size(numtype_1) =/= $size(numtype_2)
 
 
 ;; Vector operators
@@ -418,6 +420,7 @@ syntax vrelop_(Fnn X M) = EQ | NE | LT | GT | LE | GE
 syntax vcvtop_(shape_1, shape_2) hint(show vcvtop_((%,%))) hint(macro "%" "V%")
 syntax vcvtop_(Jnn_1 X M_1, Jnn_2 X M_2) =
   | EXTEND    -- if $lsizenn2(Jnn_2) = $(2 * $lsizenn1(Jnn_1))
+  ;; TODO: turn back into VEXTEND
 syntax vcvtop_(Jnn_1 X M_1, Fnn_2 X M_2) =
   | CONVERT   -- if $sizenn2(Fnn_2) >= $lsizenn1(Jnn_1) = `32
 syntax vcvtop_(Fnn_1 X M_1, Jnn_2 X M_2) =
@@ -462,10 +465,15 @@ syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32}
 
 var ao : memarg
 
-syntax vloadop hint(macro "%" "L%") =
-  | SHAPE sz X M sx  hint(show %1#X#%3#_#%4) hint(macro "%shape") -- if $(sz * M = 64)
+syntax loadop_(numtype)
+syntax loadop_(Inn) =
+  sz sx hint(show %0#_#%1) -- if sz < $sizenn(Inn)
+;; syntax loadop_(Fnn) = |           ;; uninhabited
+
+syntax vloadop_(vectype) hint(macro "%" "L%") =
+  | SHAPE sz X M sx  hint(show %1#X#%3#_#%4) hint(macro "%shape") -- if $(sz * M = $vsize(vectype)/2)
   | SPLAT sz         hint(show %#_#SPLAT)
-  | ZERO sz          hint(show %#_#ZERO)
+  | ZERO sz          hint(show %#_#ZERO) -- if sz >= `32
 
 
 ;;
@@ -513,53 +521,51 @@ syntax instr/call hint(desc "function instruction") = ...
 
 syntax instr/num hint(desc "numeric instruction") = ...
   | CONST numtype num_(numtype)      hint(show %.CONST %)
-  | UNOP numtype unop_(numtype)      hint(show %.%)
-  | BINOP numtype binop_(numtype)    hint(show %.%)
-  | TESTOP numtype testop_(numtype)  hint(show %.%)
-  | RELOP numtype relop_(numtype)    hint(show %.%)
-  | CVTOP numtype_1 numtype_2 cvtop sx?  hint(show %1.%3#_#%2#_#%4) hint(show %1.%3#_#%2)
+  | UNOP numtype unop_(numtype)      hint(show %.##%)
+  | BINOP numtype binop_(numtype)    hint(show %.##%)
+  | TESTOP numtype testop_(numtype)  hint(show %.##%)
+  | RELOP numtype relop_(numtype)    hint(show %.##%)
+  | CVTOP numtype_1 numtype_2 cvtop_(numtype_2, numtype_1) sx?  hint(show %1.%3#_#%2) hint(show %1.%3#_#%2#_#%4)
     -- if numtype_1 =/= numtype_2
-  | EXTEND numtype sz                hint(show %.EXTEND#%#_#S)
-    -- if numtype = Inn /\ sz < $sizenn(Inn)
+    ;; TODO: constrain sx? or move it into cvtop
   | ...
 
 syntax instr/vec hint(desc "vector instruction") = ...
   | VCONST vectype vec_(vectype)        hint(show %.CONST %)
-  | VVUNOP vectype vvunop               hint(show %.%)
-  | VVBINOP vectype vvbinop             hint(show %.%)
-  | VVTERNOP vectype vvternop           hint(show %.%)
-  | VVTESTOP vectype vvtestop           hint(show %.%)
-  | VUNOP shape vunop_(shape)           hint(show ##%.%)
-  | VBINOP shape vbinop_(shape)         hint(show ##%.%)
-  | VTESTOP shape vtestop_(shape)       hint(show ##%.%)
-  | VRELOP shape vrelop_(shape)         hint(show ##%.%)
-  | VSHIFTOP ishape vshiftop_(ishape)   hint(show ##%.%)
+  | VVUNOP vectype vvunop               hint(show %.##%)
+  | VVBINOP vectype vvbinop             hint(show %.##%)
+  | VVTERNOP vectype vvternop           hint(show %.##%)
+  | VVTESTOP vectype vvtestop           hint(show %.##%)
+  | VUNOP shape vunop_(shape)           hint(show ##%.##%)
+  | VBINOP shape vbinop_(shape)         hint(show ##%.##%)
+  | VTESTOP shape vtestop_(shape)       hint(show ##%.##%)
+  | VRELOP shape vrelop_(shape)         hint(show ##%.##%)
+  | VSHIFTOP ishape vshiftop_(ishape)   hint(show ##%.##%)
   | VBITMASK ishape                     hint(show ##%.BITMASK)   hint(macro "VBITMASK")
   | VSWIZZLE ishape                     hint(show ##%.SWIZZLE)   hint(macro "VSWIZZLE")
     -- if ishape = I8 X `16
   | VSHUFFLE ishape laneidx*            hint(show ##%.SHUFFLE %) hint(macro "VSHUFFLE")
     -- if ishape = I8 X `16 /\ |laneidx*| = `16
     ;; TODO: allow ^16 in type
   | VEXTUNOP ishape_1 ishape_2 vextunop_(ishape_1) sx
-    hint(show ##%1.%3#_# ##%2#_#%4)
+    hint(show ##%1.##%3#_# ##%2#_#%4)
     -- if $($lsize($lanetype(ishape_1)) = 2*$lsize($lanetype(ishape_2)))
   | VEXTBINOP ishape_1 ishape_2 vextbinop_(ishape_1) sx
-    hint(show ##%1.%3#_# ##%2#_#%4)
+    hint(show ##%1.##%3#_# ##%2#_#%4)
     -- if $($lsize($lanetype(ishape_1)) = 2*$lsize($lanetype(ishape_2)))
     ;; TODO: /\ (vextbinop =/= DOT \/ sx = S)
   | VNARROW ishape_1 ishape_2 sx        hint(show ##%.NARROW#_# ##%#_#%) hint(macro "VNARROW")
     -- if $($lsize($lanetype(ishape_2)) = 2*$lsize($lanetype(ishape_1)) <= `32)
   | VCVTOP shape_1 shape_2 vcvtop_(shape_2, shape_1) half_(shape_2, shape_1)? sx? zero_(shape_2, shape_1)?
-    hint(show ##%1.%3#_#%4#_# ##%2#_#%5#_#%6)
-    hint(show ##%1.%3#_#%4#_# ##%2#_#%5)   ;; TODO: this is wrong when half is present
-    hint(show ##%1.%3#_# ##%2#_#%4)        ;; TODO: this is wrong when half is absent
     hint(show ##%1.%3#_# ##%2)
+    hint(show ##%1.%3#_# ##%2#_#%4)        ;; TODO: this is wrong when half is absent
+    hint(show ##%1.%3#_#%5#_# ##%2#_#%4)   ;; TODO: this is wrong when half is present
     -- if $lanetype(shape_1) =/= $lanetype(shape_2)
-    ;; TODO: constrain sx
-  | VSPLAT shape                        hint(show ##%.SPLAT)     hint(macro "VSPLAT")
-  | VEXTRACT_LANE shape sx? laneidx     hint(show ##%.EXTRACT_LANE#_#% %) hint(macro "VEXTRACT_LANE")
+    ;; TODO: constrain sx? or move it into vcvtop
+  | VSPLAT shape                        hint(show ##%.SPLAT) hint(macro "VSPLAT")
+  | VEXTRACT_LANE shape sx? laneidx     hint(show ##%.EXTRACT_LANE %) hint(show ##%.EXTRACT_LANE#_#% %) hint(macro "VEXTRACT_LANE")
     -- if $lanetype(shape) = numtype <=> sx? = eps
-  | VREPLACE_LANE shape laneidx         hint(show ##%.REPLACE_LANE %)     hint(macro "VREPLACE_LANE")
+  | VREPLACE_LANE shape laneidx         hint(show ##%.REPLACE_LANE %) hint(macro "VREPLACE_LANE")
   | ...
 
 syntax instr/ref hint(desc "reference instruction") = ...
@@ -633,14 +639,12 @@ syntax instr/elem hint(desc "element instruction") = ...
   | ...
 
 syntax instr/memory hint(desc "memory instruction") = ...
-  | LOAD numtype (sz _ sx)? memidx memarg         hint(show %.LOAD % %) hint(show %.LOAD#% % %)
-    -- (if numtype = Inn /\ sz < $size(Inn))?     ;; TODO: take size implicitly
-  | STORE numtype sz? memidx memarg               hint(show %.STORE % %) hint(show %.STORE#% % %)
-    -- (if numtype = Inn /\ sz < $size(Inn))?     ;; TODO: take size implicitly
-  | VLOAD vectype vloadop? memidx memarg          hint(show %.LOAD % %) hint(show %.LOAD# ##% % %) hint(macro "V%")
-  | VLOAD_LANE vectype sz memidx memarg laneidx   hint(show %.LOAD#%#_#LANE % % %) hint(macro "V%")
-  | VSTORE vectype memidx memarg                  hint(show %.STORE % %) hint(macro "V%")
-  | VSTORE_LANE vectype sz memidx memarg laneidx  hint(show %.STORE#%#_#LANE % % %) hint(macro "V%")
+  | LOAD numtype loadop_(numtype)? memidx memarg   hint(show %.LOAD % %) hint(show %.LOAD# ##% % %)
+  | STORE numtype sz? memidx memarg                hint(show %.STORE % %) hint(show %.STORE#% % %)
+  | VLOAD vectype vloadop_(vectype)? memidx memarg hint(show %.LOAD % %) hint(show %.LOAD# ##% % %) hint(macro "V%")
+  | VLOAD_LANE vectype sz memidx memarg laneidx    hint(show %.LOAD#%#_#LANE % % %) hint(macro "V%")
+  | VSTORE vectype memidx memarg                   hint(show %.STORE % %) hint(macro "V%")
+  | VSTORE_LANE vectype sz memidx memarg laneidx   hint(show %.STORE#%#_#LANE % % %) hint(macro "V%")
   | MEMORY.SIZE memidx
   | MEMORY.GROW memidx
   | MEMORY.FILL memidx

spectec/spec/wasm-3.0/2-syntax-aux.watsup

@@ -70,11 +70,11 @@ def $zsize(numtype) = $size(numtype)
 def $zsize(vectype) = $vsize(vectype)
 def $zsize(packtype) = $psize(packtype)
 
-def $IN(N) : numtype  hint(show I#%) hint(macro "numtype")
+def $IN(N) : numtype  hint(show I#%) hint(macro "INX")
 def $IN(32) = I32
 def $IN(64) = I64
 
-def $FN(N) : numtype  hint(show F#%) hint(macro "numtype")
+def $FN(N) : numtype  hint(show F#%) hint(macro "FNX")
 def $FN(32) = F32
 def $FN(64) = F64
 

spectec/spec/wasm-3.0/3-numerics.watsup

@@ -27,7 +27,7 @@ def $testop(numtype, testop_(numtype), num_(numtype)) : num_(I32)
     hint(show %2#$_(%1)#((%3)))
 def $relop(numtype, relop_(numtype), num_(numtype), num_(numtype)) : num_(I32)
     hint(show %2#$_(%1)#(%3, %4))
-def $cvtop(numtype_1, numtype_2, cvtop, sx?, num_(numtype_1)) : num_(numtype_2)*
+def $cvtop(numtype_1, numtype_2, cvtop_(numtype_1, numtype_2), sx?, num_(numtype_1)) : num_(numtype_2)*
     hint(show %3#$_((%1,%2))^(%4)#((%5)))
 
 def $wrap(M, N, iN(M)) : iN(N)                      hint(show $wrap_((%,%))#((%)))
@@ -51,8 +51,8 @@ def $zbytes(storagetype, lit_(storagetype)) : byte* hint(show $bytes_(%,%))
 def $cbytes(Cnn, lit_(Cnn)) : byte*                 hint(show $bytes_(%,%))
 
 
-def $invibytes(N, byte*) : iN(N) hint(show $bytes_(%)^(-1)#((%)))
-def $invfbytes(N, byte*) : fN(N) hint(show $bytes_(%)^(-1)#((%)))
+def $invibytes(N, byte*) : iN(N) hint(show $bytes_($IN(%))^(-1)#((%)))
+def $invfbytes(N, byte*) : fN(N) hint(show $bytes_($FN(%))^(-1)#((%)))
 
 def $invibytes(N, b*) = n  -- if $ibytes(N, n) = b*
 def $invfbytes(N, b*) = p  -- if $fbytes(N, p) = b*

spectec/spec/wasm-3.0/6-typing.watsup

@@ -1032,7 +1032,7 @@ rule Instr_ok/data.drop:
 
 (;
 rule Instr_ok/load:
-  C |- LOAD nt (N _ sx)? x memarg : I32 -> nt
+  C |- LOAD nt (N sx)? x memarg : I32 -> nt
   -- if C.MEMS[x] = mt
   -- if $(2^(memarg.ALIGN) <= $size(nt)/8)
   -- if $(2^(memarg.ALIGN) <= N/8 < $size(nt)/8)?
@@ -1045,7 +1045,7 @@ rule Instr_ok/load-val:
   -- if $(2^(memarg.ALIGN) <= $size(nt)/8)
 
 rule Instr_ok/load-pack:
-  C |- LOAD Inn (M _ sx) x memarg : I32 -> Inn
+  C |- LOAD Inn (M sx) x memarg : I32 -> Inn
   -- if C.MEMS[x] = mt
   -- if $(2^(memarg.ALIGN) <= M/8)
 

spectec/spec/wasm-3.0/8-reduction.watsup

@@ -858,12 +858,12 @@ rule Step_read/load-num-val:
   -- if $nbytes(nt, c) = $mem(z, x).BYTES[i + ao.OFFSET : $size(nt)/8]
 
 rule Step_read/load-pack-oob:
-  z; (CONST I32 i) (LOAD Inn (n _ sx) x ao)  ~>  TRAP
+  z; (CONST I32 i) (LOAD Inn (n sx) x ao)  ~>  TRAP
   ----
   -- if $(i + ao.OFFSET + n/8 > |$mem(z, x).BYTES|)
 
 rule Step_read/load-pack-val:
-  z; (CONST I32 i) (LOAD Inn (n _ sx) x ao)  ~>  (CONST Inn $ext(n, $size(Inn), sx, c))
+  z; (CONST I32 i) (LOAD Inn (n sx) x ao)  ~>  (CONST Inn $ext(n, $size(Inn), sx, c))
   ----
   -- if $ibytes(n, c) = $mem(z, x).BYTES[i + ao.OFFSET : n/8]
 
@@ -1005,14 +1005,14 @@ rule Step_read/memory.copy-zero:
 
 rule Step_read/memory.copy-le:
   z; (CONST I32 i_1) (CONST I32 i_2) (CONST I32 n) (MEMORY.COPY x_1 x_2)  ~>
-    (CONST I32 i_1) (CONST I32 i_2) (LOAD I32 (8 _ U) x_2 $memarg0) (STORE I32 8 x_1 $memarg0)
+    (CONST I32 i_1) (CONST I32 i_2) (LOAD I32 (8 U) x_2 $memarg0) (STORE I32 8 x_1 $memarg0)
     (CONST I32 $(i_1 + 1)) (CONST I32 $(i_2 + 1)) (CONST I32 $(n - 1)) (MEMORY.COPY x_1 x_2)
   -- otherwise
   -- if i_1 <= i_2
 
 rule Step_read/memory.copy-gt:
   z; (CONST I32 i_1) (CONST I32 i_2) (CONST I32 n) (MEMORY.COPY x_1 x_2)  ~>
-    (CONST I32 $(i_1+n-1)) (CONST I32 $(i_2+n-1)) (LOAD I32 (8 _ U) x_2 $memarg0) (STORE I32 8 x_1 $memarg0)
+    (CONST I32 $(i_1+n-1)) (CONST I32 $(i_2+n-1)) (LOAD I32 (8 U) x_2 $memarg0) (STORE I32 8 x_1 $memarg0)
     (CONST I32 i_1) (CONST I32 i_2) (CONST I32 $(n-1)) (MEMORY.COPY x_1 x_2)
   -- otherwise