Skip to content

Commit

Permalink
added vcvtop: simd 96.17%
Browse files Browse the repository at this point in the history
  • Loading branch information
@702fbtngus
702fbtngus committed Feb 26, 2024
1 parent d95d924 commit 348a56f
Show file tree
Hide file tree
Showing 7 changed files with 3,744 additions and 1,076 deletions.
22 changes: 20 additions & 2 deletions spectec/spec/wasm-3.0/3-numerics.watsup
View file
Original file line number Diff line number Diff line change
Expand Up @@ -222,6 +222,8 @@ def $vbinop(shape, vbinop_(shape), vec_(V128), vec_(V128)) : vec_(V128)*
hint(show %2#_%1#(%3, %4))
def $vrelop(shape, vrelop_(shape), vec_(V128), vec_(V128)) : vec_(V128)
hint(show %2#_%1#(%3, %4))
def $vcvtop(shape_1, shape_2, vcvtop, sx?, lane_($lanetype(shape_1))) : lane_($lanetype(shape_2))
hint(show %3#$_((%1,%2))^(%5)#((%6)))

def $vunop(imm X N, ABS, v128_1) = v128
-- if lane_1* = $lanes_(imm X N, v128_1)
Expand Down Expand Up @@ -417,8 +419,24 @@ def $vrelop(F64 X N, GE, v128_1, v128_2) = v128
-- if lane_3* = $ext(1, 64, S, $fge(64, lane_1, lane_2))*
-- if v128 = $invlanes_(I64 X N, lane_3*)

def $vcvtop(shape_1, shape_2, vcvtop, sx?, lane_($lanetype(shape_1))) : lane_($lanetype(shape_2))
hint(show %3#$_((%1,%2))^(%5)#((%6)))
def $vcvtop(I8 X N_1, I16 X N_2, EXTEND, sx, i8) = i16
-- if i16 = $ext(8, 16, sx, i8)
def $vcvtop(I16 X N_1, I32 X N_2, EXTEND, sx, i16) = i32
-- if i32 = $ext(16, 32, sx, i16)
def $vcvtop(I32 X N_1, I64 X N_2, EXTEND, sx, i32) = i64
-- if i64 = $ext(32, 64, sx, i32)
def $vcvtop(F32 X N_1, I32 X N_2, TRUNC_SAT, sx, f32) = i32
-- if i32 = $trunc_sat(32, 32, sx, f32)
def $vcvtop(F64 X N_1, I32 X N_2, TRUNC_SAT, sx, f64) = i32
-- if i32 = $trunc_sat(64, 32, sx, f64)
def $vcvtop(I32 X N_1, F32 X N_2, CONVERT, sx, i32) = f32
-- if f32 = $convert(32, 32, sx, i32)
def $vcvtop(I32 X N_1, F64 X N_2, CONVERT, sx, i32) = f64
-- if f64 = $convert(32, 64, sx, i32)
def $vcvtop(F64 X N_1, F32 X N_2, DEMOTE, sx, f64) = f32
-- if f32 = $demote(64, 32, f64)
def $vcvtop(F32 X N_1, F64 X N_2, PROMOTE, sx, f32) = f64
-- if f64 = $promote(32, 64, f32)

def $vextunop(ishape_1, ishape_2, vextunop_(ishape_1, ishape_2), sx, vec_(V128)) : vec_(V128)
hint(show %3#$_((%1,%2))^(%5)#((%6)))
Expand Down
45 changes: 39 additions & 6 deletions spectec/test-frontend/TEST.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1939,12 +1939,45 @@ def $vrelop(shape : shape, vrelop_ : vrelop_(shape), vec_ : vec_(V128_vnn), vec_

;; 3-numerics.watsup
def $vcvtop(shape_1 : shape, shape_2 : shape, vcvtop : vcvtop, sx?, lane_ : lane_($lanetype(shape_1))) : lane_($lanetype(shape_2))
;; 3-numerics.watsup
def $vcvtop{N_1 : N, N_2 : N, sx : sx, i8 : lane_($lanetype(`%X%`(I8_lanetype, N_1))), i16 : lane_($lanetype(`%X%`(I16_lanetype, N_2)))}(`%X%`(I8_lanetype, N_1), `%X%`(I16_lanetype, N_2), EXTEND_vcvtop, ?(sx), i8) = i16
-- if (i16 = $ext(8, 16, sx, i8))
;; 3-numerics.watsup
def $vcvtop{N_1 : N, N_2 : N, sx : sx, i16 : lane_($lanetype(`%X%`(I16_lanetype, N_1))), i32 : lane_($lanetype(`%X%`(I32_lanetype, N_2)))}(`%X%`(I16_lanetype, N_1), `%X%`(I32_lanetype, N_2), EXTEND_vcvtop, ?(sx), i16) = i32
-- if (i32 = $ext(16, 32, sx, i16))
;; 3-numerics.watsup
def $vcvtop{N_1 : N, N_2 : N, sx : sx, i32 : lane_($lanetype(`%X%`(I32_lanetype, N_1))), i64 : lane_($lanetype(`%X%`(I64_lanetype, N_2)))}(`%X%`(I32_lanetype, N_1), `%X%`(I64_lanetype, N_2), EXTEND_vcvtop, ?(sx), i32) = i64
-- if (i64 = $ext(32, 64, sx, i32))
;; 3-numerics.watsup
def $vcvtop{N_1 : N, N_2 : N, sx : sx, f32 : f32, i32 : lane_($lanetype(`%X%`(I32_lanetype, N_2)))}(`%X%`(F32_lanetype, N_1), `%X%`(I32_lanetype, N_2), TRUNC_SAT_vcvtop, ?(sx), f32) = i32
-- if (i32 = $trunc_sat(32, 32, sx, f32))
;; 3-numerics.watsup
def $vcvtop{N_1 : N, N_2 : N, sx : sx, f64 : f64, i32 : lane_($lanetype(`%X%`(I32_lanetype, N_2)))}(`%X%`(F64_lanetype, N_1), `%X%`(I32_lanetype, N_2), TRUNC_SAT_vcvtop, ?(sx), f64) = i32
-- if (i32 = $trunc_sat(64, 32, sx, f64))
;; 3-numerics.watsup
def $vcvtop{N_1 : N, N_2 : N, sx : sx, i32 : lane_($lanetype(`%X%`(I32_lanetype, N_1))), f32 : f32}(`%X%`(I32_lanetype, N_1), `%X%`(F32_lanetype, N_2), CONVERT_vcvtop, ?(sx), i32) = f32
-- if (f32 = $convert(32, 32, sx, i32))
;; 3-numerics.watsup
def $vcvtop{N_1 : N, N_2 : N, sx : sx, i32 : lane_($lanetype(`%X%`(I32_lanetype, N_1))), f64 : f64}(`%X%`(I32_lanetype, N_1), `%X%`(F64_lanetype, N_2), CONVERT_vcvtop, ?(sx), i32) = f64
-- if (f64 = $convert(32, 64, sx, i32))
;; 3-numerics.watsup
def $vcvtop{N_1 : N, N_2 : N, sx : sx, f64 : f64, f32 : f32}(`%X%`(F64_lanetype, N_1), `%X%`(F32_lanetype, N_2), DEMOTE_vcvtop, ?(sx), f64) = f32
-- if (f32 = $demote(64, 32, f64))
;; 3-numerics.watsup
def $vcvtop{N_1 : N, N_2 : N, sx : sx, f32 : f32, f64 : f64}(`%X%`(F32_lanetype, N_1), `%X%`(F64_lanetype, N_2), PROMOTE_vcvtop, ?(sx), f32) = f64
-- if (f64 = $promote(32, 64, f32))

;; 3-numerics.watsup
def $vextunop(ishape_1 : ishape, ishape_2 : ishape, vextunop_ : vextunop_(ishape_1, ishape_2), sx : sx, vec_ : vec_(V128_vnn)) : vec_(V128_vnn)

;; 3-numerics.watsup
def $vextbinop(ishape_1 : ishape, ishape_2 : ishape, vextbinop_ : vextbinop_(ishape_1, ishape_2), sx : sx, vec_ : vec_(V128_vnn), vec_ : vec_(V128_vnn)) : vec_(V128_vnn)
;; 3-numerics.watsup
def $vextbinop{inn_1 : inn, N_1 : N, inn_2 : inn, N_2 : N, sx : sx, c_1 : vec_(V128_vnn), c_2 : vec_(V128_vnn), c : vec_(V128_vnn), cj_1 : iN($lsize((inn_1 : inn <: lanetype))), cj_2 : iN($lsize((inn_1 : inn <: lanetype))), ci_1* : lane_($lanetype(`%X%`((inn_2 : inn <: lanetype), N_2)))*, ci_2* : lane_($lanetype(`%X%`((inn_2 : inn <: lanetype), N_2)))*}(`%X%`((inn_1 : inn <: imm), N_1), `%X%`((inn_2 : inn <: imm), N_2), DOT_vextbinop_(`%X%`((inn_1 : inn <: imm), N_1), `%X%`((inn_2 : inn <: imm), N_2)), sx, c_1, c_2) = c
-- if (ci_1*{ci_1} = $lanes_(`%X%`((inn_2 : inn <: lanetype), N_2), c_1))
-- if (ci_2*{ci_2} = $lanes_(`%X%`((inn_2 : inn <: lanetype), N_2), c_2))
-- if ($concat_(syntax iN($lsize((inn_1 : inn <: lanetype))), [cj_1 cj_2]*{}) = $imul($lsize((inn_1 : inn <: lanetype)), $ext($lsize((inn_2 : inn <: lanetype)), $lsize((inn_1 : inn <: lanetype)), S_sx, ci_1), $ext($lsize((inn_2 : inn <: lanetype)), $lsize((inn_1 : inn <: lanetype)), S_sx, ci_2))*{ci_1 ci_2})
-- if (c = $invlanes_(`%X%`((inn_1 : inn <: lanetype), N_1), $iadd($lsize((inn_1 : inn <: lanetype)), cj_1, cj_2)^N_1{}))

;; 3-numerics.watsup
def $vishiftop(ishape : ishape, vshiftop_ : vshiftop_(ishape), lane_ : lane_($lanetype((ishape : ishape <: shape))), u32 : u32) : lane_($lanetype((ishape : ishape <: shape)))
Expand Down Expand Up @@ -4374,7 +4407,7 @@ relation Step_pure: `%*_~>%*`(admininstr*, admininstr*)
rule vbitmask{c : vec_(V128_vnn), inn : inn, N : N, ci : num_(I32_numtype), ci_1* : lane_($lanetype(`%X%`((inn : inn <: lanetype), N)))*}:
`%*_~>%*`([VCONST_admininstr(V128_vectype, c) VBITMASK_admininstr(`%X%`((inn : inn <: imm), N))], [CONST_admininstr(I32_numtype, ci)])
-- if (ci_1*{ci_1} = $lanes_(`%X%`((inn : inn <: lanetype), N), c))
-- if ($ibits(32, ci) = $ilt($size((inn : inn <: valtype)), S_sx, ci_1, 0)*{ci_1})
-- if ($ibits(32, ci) = $ilt($lsize((inn : inn <: lanetype)), S_sx, ci_1, 0)*{ci_1})

;; 8-reduction.watsup
rule vnarrow{c_1 : vec_(V128_vnn), c_2 : vec_(V128_vnn), inn_1 : inn, N_1 : N, inn_2 : inn, N_2 : N, sx : sx, c : vec_(V128_vnn), ci_1* : lane_($lanetype(`%X%`((inn_1 : inn <: lanetype), N_1)))*, ci_2* : lane_($lanetype(`%X%`((inn_1 : inn <: lanetype), N_1)))*, cj_1* : iN($size((inn_2 : inn <: valtype)))*, cj_2* : iN($size((inn_2 : inn <: valtype)))*}:
Expand Down Expand Up @@ -4867,16 +4900,16 @@ relation Step_read: `%~>%*`(config, admininstr*)
-- if (c = $ext(N, 128, U_sx, j))

;; 8-reduction.watsup
rule vload_lane-oob{z : state, i : nat, vt : vectype, c_1 : vec_(vt), N : N, x : idx, mo : memop, j : nat}:
`%~>%*`(`%;%*`(z, [CONST_admininstr(I32_numtype, i) VCONST_admininstr(vt, c_1) VLOAD_LANE_admininstr(N, x, mo, j)]), [TRAP_admininstr])
rule vload_lane-oob{z : state, i : nat, c_1 : vec_(V128_vnn), N : N, x : idx, mo : memop, j : nat}:
`%~>%*`(`%;%*`(z, [CONST_admininstr(I32_numtype, i) VCONST_admininstr(V128_vectype, c_1) VLOAD_LANE_admininstr(N, x, mo, j)]), [TRAP_admininstr])
-- if (((i + (mo.OFFSET_memop : uN(32) <: nat)) + (N / 8)) > |$mem(z, x).DATA_meminst|)

;; 8-reduction.watsup
rule vload_lane-val{z : state, i : nat, vt : vectype, c_1 : vec_(vt), N : N, x : idx, mo : memop, j : nat, c : vec_(vt), k : nat, imm : imm, M : M}:
`%~>%*`(`%;%*`(z, [CONST_admininstr(I32_numtype, i) VCONST_admininstr(vt, c_1) VLOAD_LANE_admininstr(N, x, mo, j)]), [VCONST_admininstr(vt, c)])
rule vload_lane-val{z : state, i : nat, c_1 : vec_(V128_vnn), N : N, x : idx, mo : memop, j : nat, c : vec_(V128_vnn), k : nat, imm : imm, M : M}:
`%~>%*`(`%;%*`(z, [CONST_admininstr(I32_numtype, i) VCONST_admininstr(V128_vectype, c_1) VLOAD_LANE_admininstr(N, x, mo, j)]), [VCONST_admininstr(V128_vectype, c)])
-- if ($ibytes(N, k) = $mem(z, x).DATA_meminst[(i + (mo.OFFSET_memop : uN(32) <: nat)) : (N / 8)])
-- if (N = $lsize((imm : imm <: lanetype)))
-- if (M = ($size((vt : vectype <: valtype)) / N))
-- if (M = ($size(V128_valtype) / N))
-- if (c = $invlanes_(`%X%`((imm : imm <: lanetype), M), $lanes_(`%X%`((imm : imm <: lanetype), M), c_1)[[j] = (k : nat <: lane_($lanetype(`%X%`((imm : imm <: lanetype), M))))]))

;; 8-reduction.watsup
Expand Down
Loading

0 comments on commit 348a56f

Please sign in to comment.