Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Pass on instruciton syntax #137

Merged
merged 2 commits into from
Jan 13, 2025
Merged

Pass on instruciton syntax #137

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
073be71
Pass on instruciton syntax
rossberg Jan 10, 2025
31aa554
Modify loadop for wasm 1 and 2
f52985 Jan 13, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 7 additions & 12 deletions document/core/syntax/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ The ${:UNREACHABLE} instruction causes an unconditional :ref:`trap <trap>`.
The ${:DROP} instruction simply throws away a single operand.

The ${:SELECT} instruction selects one of its first two operands based on whether its third operand is zero or not.
It may include a :ref:`value type <syntax-valtype>` determining the type of these operands. If missing, the operands must be of :ref:`numeric type <syntax-numtype>`.
It may include a :ref:`value type <syntax-valtype>` determining the type of these operands. If the type immediate is absent, the operands must be of :ref:`numeric type <syntax-numtype>`.

.. note::
In future versions of WebAssembly, the type annotation on ${:SELECT} may allow for more than a single value being selected at the same time.
Expand Down Expand Up @@ -119,22 +119,22 @@ Vector instructions (also known as *SIMD* instructions, *single instruction mult

$${syntax: {lanetype dim shape ishape bshape} half__ zero__ laneidx instr/vec}

$${syntax:
vvunop vvbinop vvternop vvtestop
vunop_ vbinop_ vternop_ vtestop_ vrelop_ vswizzlop_ vshiftop_ vextunop__ vextbinop__ vextternop__ vcvtop__
}

Vector instructions have a naming convention involving a *shape* prefix that
determines how their operands will be interpreted,
written ${:t#X#N}, and consisting of a *lane type* ${:t}, a possibly *packed* :ref:`numeric type <syntax-numtype>`, and the number of *lanes* ${:N} of that type.
Operations are performed point-wise on the values of each lane.

Instructions prefixed with ${:V128} do not involve a specific interpretation, and treat the ${:V128} as either an ${:i128} value or a vector of ${:128} individual bits.

.. note::
For example, the shape ${shape: I32 X `4} interprets the operand
as four ${:i32} values, packed into an ${:i128}.
The bit width of the lane type ${:t} times ${:N} always is ${:128}.

Instructions prefixed with ${:V128} do not involve a specific interpretation, and treat the ${:V128} as either an ${:i128} value or a vector of ${:128} individual bits.
$${syntax:
vvunop vvbinop vvternop vvtestop
vunop_ vbinop_ vternop_ vtestop_ vrelop_ vswizzlop_ vshiftop_ vextunop__ vextbinop__ vextternop__ vcvtop__
}

Vector instructions can be grouped into several subcategories:

Expand Down Expand Up @@ -352,11 +352,6 @@ The ${:MEMORY.INIT} instruction copies data from a :ref:`passive data segment <s

The ${:DATA.DROP} instruction prevents further use of a passive data segment. This instruction is intended to be used as an optimization hint. After a data segment is dropped its data can no longer be retrieved, so the memory used by this segment may be freed.

.. note::
In the current version of WebAssembly,
all memory instructions implicitly operate on :ref:`memory <syntax-mem>` :ref:`index <syntax-memidx>` ${:0}.
This restriction may be lifted in future versions.


.. index:: ! control instruction, ! structured control, ! exception, ! label, ! block, ! block type, ! branch, ! unwinding, stack type, label index, function index, type index, list, trap, function, table, tag, function type, value type, tag type, try block, type index
pair: abstract syntax; instruction
Expand Down
5 changes: 5 additions & 0 deletions document/core/util/macros.def
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -219,6 +219,11 @@
.. |VNX| mathdef:: \xref{syntax/types}{syntax-vectype}{\K{v}}
.. |VN| mathdef:: \xref{syntax/types}{syntax-vectype}{\K{v}\scriptstyle\kern-0.1emN}

.. |ntI| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{i}}
.. |ntF| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{f}}
.. |ntV| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{v}}
.. |ntN| mathdef:: \xref{syntax/types}{syntax-numtype}{\scriptstyle\kern-0.1emN}

.. |ANYREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{anyref}}
.. |EQREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{eqref}}
.. |I31REF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{i{\scriptstyle31}ref}}
Expand Down
2 changes: 1 addition & 1 deletion spectec/spec/wasm-1.0/1-syntax.watsup
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,7 @@ syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32}
var ao : memarg

syntax loadop_(valtype)
syntax loadop_(Inn) = sz sx hint(show %0#_#%1) -- if sz < $size(Inn)
syntax loadop_(Inn) = sz _ sx hint(show %0#_#%2) -- if sz < $size(Inn)


;; Instructions
Expand Down
4 changes: 2 additions & 2 deletions spectec/spec/wasm-1.0/6-typing.watsup
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -270,7 +270,7 @@ rule Instr_ok/memory.grow:

(;
rule Instr_ok/load:
C |- LOAD t (n sx)? memarg : I32 -> t
C |- LOAD t (n _ sx)? memarg : I32 -> t
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= $size(t)/8)
-- if $(2^(memarg.ALIGN) <= n/8 < $size(t)/8)?
Expand All @@ -283,7 +283,7 @@ rule Instr_ok/load-val:
-- if $(2^(memarg.ALIGN) <= $size(t)/8)

rule Instr_ok/load-pack:
C |- LOAD Inn (M sx) memarg : I32 -> Inn
C |- LOAD Inn (M _ sx) memarg : I32 -> Inn
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= M/8)

Expand Down
4 changes: 2 additions & 2 deletions spectec/spec/wasm-1.0/8-reduction.watsup
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -233,11 +233,11 @@ rule Step_read/load-num-val:
-- if $bytes_(t, c) = $mem(z, 0).BYTES[i + ao.OFFSET : $size(t)/8]

rule Step_read/load-pack-trap:
z; (CONST I32 i) (LOAD Inn (n sx) ao) ~> TRAP
z; (CONST I32 i) (LOAD Inn (n _ sx) ao) ~> TRAP
-- if $(i + ao.OFFSET + n/8 > |$mem(z, 0).BYTES|)

rule Step_read/load-pack-val:
z; (CONST I32 i) (LOAD Inn (n sx) ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c))
z; (CONST I32 i) (LOAD Inn (n _ sx) ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c))
-- if $ibytes_(n, c) = $mem(z, 0).BYTES[i + ao.OFFSET : n/8]


Expand Down
20 changes: 10 additions & 10 deletions spectec/spec/wasm-1.0/A-binary.watsup
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -181,16 +181,16 @@ grammar Binstr/memory : instr = ...
| 0x29 ao:Bmemarg => LOAD I64 ao
| 0x2A ao:Bmemarg => LOAD F32 ao
| 0x2B ao:Bmemarg => LOAD F64 ao
| 0x2C ao:Bmemarg => LOAD I32 (8 S) ao
| 0x2D ao:Bmemarg => LOAD I32 (8 U) ao
| 0x2E ao:Bmemarg => LOAD I32 (16 S) ao
| 0x2F ao:Bmemarg => LOAD I32 (16 U) ao
| 0x30 ao:Bmemarg => LOAD I64 (8 S) ao
| 0x31 ao:Bmemarg => LOAD I64 (8 U) ao
| 0x32 ao:Bmemarg => LOAD I64 (16 S) ao
| 0x33 ao:Bmemarg => LOAD I64 (16 U) ao
| 0x34 ao:Bmemarg => LOAD I64 (32 S) ao
| 0x35 ao:Bmemarg => LOAD I64 (32 U) ao
| 0x2C ao:Bmemarg => LOAD I32 (8 _ S) ao
| 0x2D ao:Bmemarg => LOAD I32 (8 _ U) ao
| 0x2E ao:Bmemarg => LOAD I32 (16 _ S) ao
| 0x2F ao:Bmemarg => LOAD I32 (16 _ U) ao
| 0x30 ao:Bmemarg => LOAD I64 (8 _ S) ao
| 0x31 ao:Bmemarg => LOAD I64 (8 _ U) ao
| 0x32 ao:Bmemarg => LOAD I64 (16 _ S) ao
| 0x33 ao:Bmemarg => LOAD I64 (16 _ U) ao
| 0x34 ao:Bmemarg => LOAD I64 (32 _ S) ao
| 0x35 ao:Bmemarg => LOAD I64 (32 _ U) ao
| 0x36 ao:Bmemarg => STORE I32 ao
| 0x37 ao:Bmemarg => STORE I64 ao
| 0x38 ao:Bmemarg => STORE F32 ao
Expand Down
8 changes: 4 additions & 4 deletions spectec/spec/wasm-2.0/1-syntax.watsup
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -345,12 +345,12 @@ syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32}
var ao : memarg

syntax loadop_(numtype)
syntax loadop_(Inn) = sz sx hint(show %0#_#%1) -- if sz < $sizenn(Inn)
syntax loadop_(Inn) = sz _ sx hint(show %0#_#%2) -- if sz < $sizenn(Inn)

syntax vloadop =
| SHAPE nat X nat sx hint(show %#X#%#_#%)
| SPLAT nat hint(show %#_#SPLAT)
| ZERO nat hint(show %#_#ZERO)
| SHAPE nat X nat _ sx hint(show %1#X#%3#_#%5)
| SPLAT nat hint(show %#_#SPLAT)
| ZERO nat hint(show %#_#ZERO)


;;
Expand Down
6 changes: 3 additions & 3 deletions spectec/spec/wasm-2.0/6-typing.watsup
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -448,7 +448,7 @@ rule Instr_ok/data.drop:

(;
rule Instr_ok/load:
C |- LOAD nt (n sx)? memarg : I32 -> nt
C |- LOAD nt (n _ sx)? memarg : I32 -> nt
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= $size(nt)/8)
-- if $(2^(memarg.ALIGN) <= n/8 < $size(nt)/8)?
Expand All @@ -461,7 +461,7 @@ rule Instr_ok/load-val:
-- if $(2^(memarg.ALIGN) <= $size(nt)/8)

rule Instr_ok/load-pack:
C |- LOAD Inn (M sx) memarg : I32 -> Inn
C |- LOAD Inn (M _ sx) memarg : I32 -> Inn
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= M/8)

Expand All @@ -485,7 +485,7 @@ rule Instr_ok/store-pack:
-- if $(2^(memarg.ALIGN) <= M/8)

rule Instr_ok/vload:
C |- VLOAD V128 (SHAPE M X N sx) memarg : I32 -> V128
C |- VLOAD V128 (SHAPE M X N _ sx) memarg : I32 -> V128
-- if C.MEMS[0] = mt
-- if $(2^(memarg.ALIGN) <= M/8 * N)

Expand Down
12 changes: 6 additions & 6 deletions spectec/spec/wasm-2.0/8-reduction.watsup
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -492,11 +492,11 @@ rule Step_read/load-num-val:
-- if $nbytes_(nt, c) = $mem(z, 0).BYTES[i + ao.OFFSET : $size(nt)/8]

rule Step_read/load-pack-trap:
z; (CONST I32 i) (LOAD Inn (n sx) ao) ~> TRAP
z; (CONST I32 i) (LOAD Inn (n _ sx) ao) ~> TRAP
-- if $(i + ao.OFFSET + n/8 > |$mem(z, 0).BYTES|)

rule Step_read/load-pack-val:
z; (CONST I32 i) (LOAD Inn (n sx) ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c))
z; (CONST I32 i) (LOAD Inn (n _ sx) ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c))
-- if $ibytes_(n, c) = $mem(z, 0).BYTES[i + ao.OFFSET : n/8]

rule Step_read/vload-oob:
Expand All @@ -509,11 +509,11 @@ rule Step_read/vload-val:


rule Step_read/vload-shape-oob:
z; (CONST I32 i) (VLOAD V128 (SHAPE M X N sx) ao) ~> TRAP
z; (CONST I32 i) (VLOAD V128 (SHAPE M X N _ sx) ao) ~> TRAP
-- if $(i + ao.OFFSET + M * N/8) > |$mem(z, 0).BYTES|

rule Step_read/vload-shape-val:
z; (CONST I32 i) (VLOAD V128 (SHAPE M X N sx) ao) ~> (VCONST V128 c)
z; (CONST I32 i) (VLOAD V128 (SHAPE M X N _ sx) ao) ~> (VCONST V128 c)
-- (if $ibytes_(M, j) = $mem(z, 0).BYTES[i + ao.OFFSET + k * M/8 : M/8])^(k<N)
-- if $lsize(Jnn) = $(M * 2) ;; TODO: relate implicitly
-- if c = $invlanes_(Jnn X N, $extend__(M, $lsize(Jnn), sx, j)^N)
Expand Down Expand Up @@ -629,14 +629,14 @@ rule Step_read/memory.copy-zero:

rule Step_read/memory.copy-le:
z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (MEMORY.COPY) ~>
(CONST I32 j) (CONST I32 i) (LOAD I32 (8 U) $memarg0) (STORE I32 8 $memarg0)
(CONST I32 j) (CONST I32 i) (LOAD I32 (8 _ U) $memarg0) (STORE I32 8 $memarg0)
(CONST I32 $(j+1)) (CONST I32 $(i+1)) (CONST I32 $(n-1)) (MEMORY.COPY)
-- otherwise
-- if j <= i

rule Step_read/memory.copy-gt:
z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (MEMORY.COPY) ~>
(CONST I32 $(j+n-1)) (CONST I32 $(i+n-1)) (LOAD I32 (8 U) $memarg0) (STORE I32 8 $memarg0)
(CONST I32 $(j+n-1)) (CONST I32 $(i+n-1)) (LOAD I32 (8 _ U) $memarg0) (STORE I32 8 $memarg0)
(CONST I32 j) (CONST I32 i) (CONST I32 $(n-1)) (MEMORY.COPY)
-- otherwise

Expand Down
32 changes: 16 additions & 16 deletions spectec/spec/wasm-2.0/A-binary.watsup
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -221,16 +221,16 @@ grammar Binstr/memory : instr = ...
| 0x29 ao:Bmemarg => LOAD I64 ao
| 0x2A ao:Bmemarg => LOAD F32 ao
| 0x2B ao:Bmemarg => LOAD F64 ao
| 0x2C ao:Bmemarg => LOAD I32 (8 S) ao
| 0x2D ao:Bmemarg => LOAD I32 (8 U) ao
| 0x2E ao:Bmemarg => LOAD I32 (16 S) ao
| 0x2F ao:Bmemarg => LOAD I32 (16 U) ao
| 0x30 ao:Bmemarg => LOAD I64 (8 S) ao
| 0x31 ao:Bmemarg => LOAD I64 (8 U) ao
| 0x32 ao:Bmemarg => LOAD I64 (16 S) ao
| 0x33 ao:Bmemarg => LOAD I64 (16 U) ao
| 0x34 ao:Bmemarg => LOAD I64 (32 S) ao
| 0x35 ao:Bmemarg => LOAD I64 (32 U) ao
| 0x2C ao:Bmemarg => LOAD I32 (8 _ S) ao
| 0x2D ao:Bmemarg => LOAD I32 (8 _ U) ao
| 0x2E ao:Bmemarg => LOAD I32 (16 _ S) ao
| 0x2F ao:Bmemarg => LOAD I32 (16 _ U) ao
| 0x30 ao:Bmemarg => LOAD I64 (8 _ S) ao
| 0x31 ao:Bmemarg => LOAD I64 (8 _ U) ao
| 0x32 ao:Bmemarg => LOAD I64 (16 _ S) ao
| 0x33 ao:Bmemarg => LOAD I64 (16 _ U) ao
| 0x34 ao:Bmemarg => LOAD I64 (32 _ S) ao
| 0x35 ao:Bmemarg => LOAD I64 (32 _ U) ao
| 0x36 ao:Bmemarg => STORE I32 ao
| 0x37 ao:Bmemarg => STORE I64 ao
| 0x38 ao:Bmemarg => STORE F32 ao
Expand Down Expand Up @@ -454,12 +454,12 @@ grammar Blaneidx : laneidx =

grammar Binstr/vector-memory : instr = ...
| 0xFD 0:Bu32 ao:Bmemarg => VLOAD V128 ao
| 0xFD 1:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 8 X 8 S) ao
| 0xFD 2:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 8 X 8 U) ao
| 0xFD 3:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 16 X 4 S) ao
| 0xFD 4:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 16 X 4 U) ao
| 0xFD 5:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 32 X 2 S) ao
| 0xFD 6:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 32 X 2 U) ao
| 0xFD 1:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 8 X 8 _ S) ao
| 0xFD 2:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 8 X 8 _ U) ao
| 0xFD 3:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 16 X 4 _ S) ao
| 0xFD 4:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 16 X 4 _ U) ao
| 0xFD 5:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 32 X 2 _ S) ao
| 0xFD 6:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 32 X 2 _ U) ao
| 0xFD 7:Bu32 ao:Bmemarg => VLOAD V128 (SPLAT 8) ao
| 0xFD 8:Bu32 ao:Bmemarg => VLOAD V128 (SPLAT 16) ao
| 0xFD 9:Bu32 ao:Bmemarg => VLOAD V128 (SPLAT 32) ao
Expand Down
33 changes: 18 additions & 15 deletions spectec/spec/wasm-3.0/1-syntax.watsup
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -185,9 +185,9 @@ syntax valtype/syn hint(desc "value type") =
syntax valtype/sem =
| ... | BOT

syntax Inn hint(show I#N) hint(macro none) = I32 | I64
syntax Fnn hint(show F#N) hint(macro none) = F32 | F64
syntax Vnn hint(show V#N) hint(macro none) = V128
syntax Inn hint(show I#N) hint(macro "nt%") = I32 | I64
syntax Fnn hint(show F#N) hint(macro "nt%") = F32 | F64
syntax Vnn hint(show V#N) hint(macro "nt%") = V128
syntax Cnn hint(show t) = Inn | Fnn | Vnn


Expand Down Expand Up @@ -224,9 +224,9 @@ syntax packtype hint(desc "packed type") = I8 | I16
syntax lanetype hint(desc "lane type") = numtype | packtype
syntax storagetype hint(desc "storage type") = valtype | packtype

syntax Pnn hint(show I#N) hint(macro none) = I8 | I16
syntax Jnn hint(show I#N) hint(macro none) = Inn | Pnn
syntax Lnn hint(show I#N) hint(macro none) = Inn | Fnn | Pnn
syntax Pnn hint(show I#N) hint(macro "nt%") = I8 | I16
syntax Jnn hint(show I#N) hint(macro "nt%") = Inn | Pnn
syntax Lnn hint(show I#N) hint(macro "nt%") = Inn | Fnn | Pnn


;; Result types
Expand Down Expand Up @@ -439,6 +439,7 @@ syntax relop_(Inn) =
syntax relop_(Fnn) =
| EQ | NE | LT | GT | LE | GE

;; TODO(3, rossberg): change order of parameters?
syntax cvtop__(numtype_1, numtype_2)
syntax cvtop__(Inn_1, Inn_2) =
| EXTEND sx hint(show %0#_#%1) -- if $sizenn1(Inn_1) < $sizenn2(Inn_2)
Expand Down Expand Up @@ -479,11 +480,11 @@ syntax bshape hint(desc "byte shape") = shape -- if $lanetype(shape) = I8
;; Vector operators

syntax half__(shape_1, shape_2)
syntax half__(Jnn_1 X M_1, Jnn_2 X M_2) = LOW | HIGH -- if $(2 * $lsizenn1(Jnn_1)) = $lsizenn1(Jnn_2)
syntax half__(Lnn_1 X M_1, Fnn_2 X M_2) = LOW -- if $(2 * $lsizenn1(Lnn_1)) = $sizenn1(Fnn_2) = `64
syntax half__(Jnn_1 X M_1, Jnn_2 X M_2) = LOW | HIGH -- if $(2 * $lsizenn1(Jnn_1)) = $lsizenn2(Jnn_2)
syntax half__(Lnn_1 X M_1, Fnn_2 X M_2) = LOW -- if $(2 * $lsizenn1(Lnn_1)) = $sizenn2(Fnn_2) = 64

syntax zero__(shape_1, shape_2)
syntax zero__(Fnn_1 X M_1, Lnn_2 X M_2) = ZERO -- if $(2 * $lsizenn2(Lnn_2)) = $sizenn1(Fnn_1) = `64
syntax zero__(Fnn_1 X M_1, Lnn_2 X M_2) = ZERO -- if $(2 * $lsizenn2(Lnn_2)) = $sizenn1(Fnn_1) = 64

syntax vvunop hint(macro "%" "V%") = NOT
syntax vvbinop hint(macro "%" "V%") = AND | ANDNOT | OR | XOR
Expand All @@ -507,7 +508,8 @@ syntax vbinop_(Jnn X M) =
| RELAXED_Q15MULR S hint(show RELAXED_Q15MULR#_#%) -- if $lsizenn(Jnn) = `16
| MIN sx hint(show MIN#_#%) -- if $lsizenn(Jnn) <= `32
| MAX sx hint(show MAX#_#%) -- if $lsizenn(Jnn) <= `32
syntax vbinop_(Fnn X M) = ADD | SUB | MUL | DIV | MIN | MAX | PMIN | PMAX | RELAXED_MIN | RELAXED_MAX
syntax vbinop_(Fnn X M) = ADD | SUB | MUL | DIV | MIN | MAX | PMIN | PMAX
| RELAXED_MIN | RELAXED_MAX

syntax vternop_(shape) hint(macro "%" "V%")
syntax vternop_(Jnn X M) = RELAXED_LANESELECT
Expand Down Expand Up @@ -575,15 +577,15 @@ syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32}
var ao : memarg

syntax loadop_(numtype)
syntax loadop_(Inn) = sz sx hint(show %0#_#%1) -- if sz < $sizenn(Inn)
syntax loadop_(Inn) = sz _ sx hint(show %0#_#%2) -- if sz < $sizenn(Inn)

syntax storeop_(numtype)
syntax storeop_(Inn) = sz -- if sz < $sizenn(Inn)
syntax storeop_(Inn) = sz -- if sz < $sizenn(Inn)

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) -- if sz >= `32
| SHAPE sz X M _ sx hint(show %1#X#%3#_#%5) hint(macro "%shape") -- if $(sz * M = $vsize(vectype)/2)
| SPLAT sz hint(show %#_#SPLAT)
| ZERO sz hint(show %#_#ZERO) -- if sz >= `32


;; Block types
Expand Down Expand Up @@ -681,6 +683,7 @@ syntax instr/vec hint(desc "vector instruction") = ...
| 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)? zero__(shape_2, shape_1)?
;; TODO(1, rossberg): fix overlong line
hint(show ##%1.%3#_# ##%2)
hint(show ##%1.%3#_# ##%2#_#%4) ;; TODO(2, rossberg): this is wrong when half is absent
hint(show ##%1.%3#_#%5#_# ##%2#_#%4) ;; TODO(2, rossberg): this is wrong when half is present
Expand Down
6 changes: 3 additions & 3 deletions spectec/spec/wasm-3.0/3-typing.watsup
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1074,7 +1074,7 @@ rule Instr_ok/data.drop:

(;
rule Instr_ok/load:
C |- LOAD nt (N sx)? x memarg : at -> nt
C |- LOAD nt (N _ sx)? x memarg : at -> nt
-- if C.MEMS[x] = at lim PAGE
-- if $(2^(memarg.ALIGN) <= $size(nt)/8)
-- if $(2^(memarg.ALIGN) <= N/8 < $size(nt)/8)?
Expand All @@ -1087,7 +1087,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 : at -> Inn
C |- LOAD Inn (M _ sx) x memarg : at -> Inn
-- if C.MEMS[x] = at lim PAGE
-- if $(2^(memarg.ALIGN) <= M/8)

Expand Down Expand Up @@ -1116,7 +1116,7 @@ rule Instr_ok/vload-val:
-- if $(2^(memarg.ALIGN) <= $vsize(V128)/8)

rule Instr_ok/vload-pack:
C |- VLOAD V128 (SHAPE M X N sx) x memarg : at -> V128
C |- VLOAD V128 (SHAPE M X N _ sx) x memarg : at -> V128
-- if C.MEMS[x] = at lim PAGE
-- if $(2^(memarg.ALIGN) <= M/8 * N)

Expand Down
Loading
Loading