Switch arg order for cvtop in wasm 2

Wasm-DSL · Apr 8, 2024 · 945af10 · 945af10
1 parent 4e5666d
commit 945af10
Show file tree

Hide file tree

Showing 6 changed files with 36 additions and 600 deletions.
diff --git a/spectec/spec/wasm-2.0/1-syntax.watsup b/spectec/spec/wasm-2.0/1-syntax.watsup
@@ -419,7 +419,7 @@ syntax instr/vec hint(desc "vector instruction") = ...
     ;; TODO: /\ (vextbinop =/= DOT \/ sx = S)
   | VNARROW ishape_1 ishape_2 sx        hint(show %.NARROW#_#%#_#%)
     -- if $($lsize($lanetype(ishape_2)) = 2*$lsize($lanetype(ishape_1)) <= 32)
-  | VCVTOP shape vcvtop half? shape sx? zero?
+  | VCVTOP shape shape vcvtop half? sx? zero?
     hint(show %.%#_#%#_#%#_#%) hint(show %.%#_#%#_#%#_#%) hint(show %.%#_#%#_#%#_#%#_#%)
     ;; TODO: missing constraints
   | ...

diff --git a/spectec/spec/wasm-2.0/6-typing.watsup b/spectec/spec/wasm-2.0/6-typing.watsup
@@ -354,7 +354,7 @@ rule Instr_ok/vnarrow:
   C |- VNARROW sh_1 sh_2 sx : V128 V128 -> V128
 
 rule Instr_ok/vcvtop:
-  C |- VCVTOP sh_1 vcvtop hf? sh_2 sx? zero? : V128 -> V128
+  C |- VCVTOP sh_1 sh_2 vcvtop hf? sx? zero? : V128 -> V128
 
 
 ;; Local instructions

diff --git a/spectec/spec/wasm-2.0/8-reduction.watsup b/spectec/spec/wasm-2.0/8-reduction.watsup
@@ -323,18 +323,18 @@ rule Step_pure/vnarrow:
 
 
 rule Step_pure/vcvtop-full:
-  (VCONST V128 c_1) (VCVTOP (lnn_2 X N_2) vcvtop eps (lnn_1 X N_1) sx) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (lnn_2 X N_2) (lnn_1 X N_1) vcvtop eps sx) ~> (VCONST V128 c)
   -- if c'* = $lanes_(lnn_1 X N_1, c_1)
   -- if c = $invlanes_(lnn_2 X N_2, $vcvtop(lnn_1 X N_1, lnn_2 X N_2, vcvtop, sx, c')*)
 
 var hf : half  ;; TODO: this declaration shouldn't be needed
 rule Step_pure/vcvtop-half:
-  (VCONST V128 c_1) (VCVTOP (lnn_2 X N_2) vcvtop hf (lnn_1 X N_1) sx?) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (lnn_2 X N_2) (lnn_1 X N_1) vcvtop hf sx?) ~> (VCONST V128 c)
   -- if ci* = $lanes_(lnn_1 X N_1, c_1)[$halfop(hf, 0, N_2) : N_2]
   -- if c = $invlanes_(lnn_2 X N_2, $vcvtop(lnn_1 X N_1, lnn_2 X N_2, vcvtop, sx?, ci)*)
 
 rule Step_pure/vcvtop-zero:
-  (VCONST V128 c_1) (VCVTOP (nt_2 X N_2) vcvtop eps (nt_1 X N_1) sx? ZERO) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (nt_2 X N_2) (nt_1 X N_1) vcvtop eps sx? ZERO) ~> (VCONST V128 c)
   -- if ci* = $lanes_(nt_1 X N_1, c_1)
   -- if c = $invlanes_(nt_2 X N_2, $vcvtop(nt_1 X N_1, nt_2 X N_2, vcvtop, sx?, ci)* $zero(nt_2)^N_1)
 

diff --git a/spectec/spec/wasm-2.0/A-binary.watsup b/spectec/spec/wasm-2.0/A-binary.watsup
@@ -615,10 +615,10 @@ grammar Binstr/vector-v-i16x8 : instr = ...
   | 0xFD 132:Bu32 => VBITMASK (I16 X 8)
   | 0xFD 133:Bu32 => VNARROW (I16 X 8) (I32 X 4) S
   | 0xFD 134:Bu32 => VNARROW (I16 X 8) (I32 X 4) U
-  | 0xFD 135:Bu32 => VCVTOP (I16 X 8) EXTEND LOW (I8 X 16) S
-  | 0xFD 136:Bu32 => VCVTOP (I16 X 8) EXTEND HIGH (I8 X 16) S
-  | 0xFD 137:Bu32 => VCVTOP (I16 X 8) EXTEND LOW (I8 X 16) U
-  | 0xFD 138:Bu32 => VCVTOP (I16 X 8) EXTEND HIGH (I8 X 16) U
+  | 0xFD 135:Bu32 => VCVTOP (I16 X 8) (I8 X 16) EXTEND LOW S
+  | 0xFD 136:Bu32 => VCVTOP (I16 X 8) (I8 X 16) EXTEND HIGH S
+  | 0xFD 137:Bu32 => VCVTOP (I16 X 8) (I8 X 16) EXTEND LOW U
+  | 0xFD 138:Bu32 => VCVTOP (I16 X 8) (I8 X 16) EXTEND HIGH U
   | 0xFD 139:Bu32 => VSHIFTOP (I16 X 8) SHL
   | 0xFD 140:Bu32 => VSHIFTOP (I16 X 8) (SHR S)
   | 0xFD 141:Bu32 => VSHIFTOP (I16 X 8) (SHR U)
@@ -647,10 +647,10 @@ grammar Binstr/vector-v-i32x4 : instr = ...
   | 0xFD 161:Bu32 => VUNOP (I32 X 4) NEG
   | 0xFD 163:Bu32 => VTESTOP (I32 X 4) ALL_TRUE
   | 0xFD 164:Bu32 => VBITMASK (I32 X 4)
-  | 0xFD 167:Bu32 => VCVTOP (I32 X 4) EXTEND LOW (I16 X 8) S
-  | 0xFD 168:Bu32 => VCVTOP (I32 X 4) EXTEND HIGH (I16 X 8) S
-  | 0xFD 169:Bu32 => VCVTOP (I32 X 4) EXTEND LOW (I16 X 8) U
-  | 0xFD 170:Bu32 => VCVTOP (I32 X 4) EXTEND HIGH (I16 X 8) U
+  | 0xFD 167:Bu32 => VCVTOP (I32 X 4) (I16 X 8) EXTEND LOW S
+  | 0xFD 168:Bu32 => VCVTOP (I32 X 4) (I16 X 8) EXTEND HIGH S
+  | 0xFD 169:Bu32 => VCVTOP (I32 X 4) (I16 X 8) EXTEND LOW U
+  | 0xFD 170:Bu32 => VCVTOP (I32 X 4) (I16 X 8) EXTEND HIGH U
   | 0xFD 171:Bu32 => VSHIFTOP (I32 X 4) SHL
   | 0xFD 172:Bu32 => VSHIFTOP (I32 X 4) (SHR S)
   | 0xFD 173:Bu32 => VSHIFTOP (I32 X 4) (SHR U)
@@ -673,10 +673,10 @@ grammar Binstr/vector-v-i64x2 : instr = ...
   | 0xFD 193:Bu32 => VUNOP (I64 X 2) NEG
   | 0xFD 195:Bu32 => VTESTOP (I64 X 2) ALL_TRUE
   | 0xFD 196:Bu32 => VBITMASK (I64 X 2)
-  | 0xFD 199:Bu32 => VCVTOP (I64 X 2) EXTEND LOW (I32 X 4) S
-  | 0xFD 200:Bu32 => VCVTOP (I64 X 2) EXTEND HIGH (I32 X 4) S
-  | 0xFD 201:Bu32 => VCVTOP (I64 X 2) EXTEND LOW (I32 X 4) U
-  | 0xFD 202:Bu32 => VCVTOP (I64 X 2) EXTEND HIGH (I32 X 4) U
+  | 0xFD 199:Bu32 => VCVTOP (I64 X 2) (I32 X 4) EXTEND LOW S
+  | 0xFD 200:Bu32 => VCVTOP (I64 X 2) (I32 X 4) EXTEND HIGH S
+  | 0xFD 201:Bu32 => VCVTOP (I64 X 2) (I32 X 4) EXTEND LOW U
+  | 0xFD 202:Bu32 => VCVTOP (I64 X 2) (I32 X 4) EXTEND HIGH U
   | 0xFD 203:Bu32 => VSHIFTOP (I64 X 2) SHL
   | 0xFD 204:Bu32 => VSHIFTOP (I64 X 2) (SHR S)
   | 0xFD 205:Bu32 => VSHIFTOP (I64 X 2) (SHR U)
@@ -726,16 +726,16 @@ grammar Binstr/vector-v-f64x2 : instr = ...
   | ...
 
 grammar Binstr/vector-cvt : instr = ...
-  | 0xFD 248:Bu32 => VCVTOP (I32 X 4) TRUNC_SAT (F32 X 4) S
-  | 0xFD 249:Bu32 => VCVTOP (I32 X 4) TRUNC_SAT (F32 X 4) U
-  | 0xFD 250:Bu32 => VCVTOP (F32 X 4) CONVERT (I32 X 4) S
-  | 0xFD 251:Bu32 => VCVTOP (F32 X 4) CONVERT (I32 X 4) U
-  | 0xFD 252:Bu32 => VCVTOP (I32 X 4) TRUNC_SAT (F64 X 2) S ZERO
-  | 0xFD 253:Bu32 => VCVTOP (I32 X 4) TRUNC_SAT (F64 X 2) U ZERO
-  | 0xFD 254:Bu32 => VCVTOP (F64 X 2) CONVERT LOW (I32 X 4) S
-  | 0xFD 255:Bu32 => VCVTOP (F64 X 2) CONVERT LOW (I32 X 4) U
-  | 0xFD 94:Bu32 => VCVTOP (F32 X 4) DEMOTE (F64 X 2) ZERO
-  | 0xFD 95:Bu32 => VCVTOP (F64 X 2) PROMOTE LOW (F32 X 4)
+  | 0xFD 248:Bu32 => VCVTOP (I32 X 4) (F32 X 4) TRUNC_SAT S
+  | 0xFD 249:Bu32 => VCVTOP (I32 X 4) (F32 X 4) TRUNC_SAT U
+  | 0xFD 250:Bu32 => VCVTOP (F32 X 4) (I32 X 4) CONVERT S
+  | 0xFD 251:Bu32 => VCVTOP (F32 X 4) (I32 X 4) CONVERT U
+  | 0xFD 252:Bu32 => VCVTOP (I32 X 4) (F64 X 2) TRUNC_SAT S ZERO
+  | 0xFD 253:Bu32 => VCVTOP (I32 X 4) (F64 X 2) TRUNC_SAT U ZERO
+  | 0xFD 254:Bu32 => VCVTOP (F64 X 2) (I32 X 4) CONVERT LOW S
+  | 0xFD 255:Bu32 => VCVTOP (F64 X 2) (I32 X 4) CONVERT LOW U
+  | 0xFD 94:Bu32 => VCVTOP (F32 X 4) (F64 X 2) DEMOTE ZERO
+  | 0xFD 95:Bu32 => VCVTOP (F64 X 2) (F32 X 4) PROMOTE LOW
 
 
 ;; Expressions