Skip to content

Commit

Permalink
Moved ExtendN to unop
Browse files Browse the repository at this point in the history
  • Loading branch information
HoseongLee committed Feb 22, 2024
1 parent b4983b4 commit 0e09411
Show file tree
Hide file tree
Showing 9 changed files with 27 additions and 52 deletions.
3 changes: 1 addition & 2 deletions spectec/spec/wasm-3.0/1-syntax.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -271,7 +271,7 @@ syntax zval_(packtype) = pack_(packtype)
syntax sx hint(desc "signedness") = | U | S

syntax unop_(numtype)
syntax unop_(inn) = | CLZ | CTZ | POPCNT
syntax unop_(inn) = | CLZ | CTZ | POPCNT | EXTEND n
syntax unop_(fnn) = | ABS | NEG | SQRT | CEIL | FLOOR | TRUNC | NEAREST

syntax binop_(numtype)
Expand Down Expand Up @@ -413,7 +413,6 @@ syntax instr/numeric hint(desc "numeric instruction") = ...
| TESTOP numtype testop_(numtype) hint(show %.%)
| RELOP numtype relop_(numtype) hint(show %.%)
| CVTOP numtype cvtop numtype sx? hint(show %.%#_#%#_#%)
| EXTEND numtype n hint(show %.EXTEND#%)
| ...

syntax half hint(desc "lane part") = | LOW | HIGH
Expand Down
22 changes: 11 additions & 11 deletions spectec/spec/wasm-3.0/3-numerics.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -89,17 +89,17 @@ def $binop(inn, SHL, i, j) = $ishl($size(inn), i, j)
def $binop(inn, SHR sx, i, j) = $ishr($size(inn), sx, i, j)
def $binop(inn, ROTL, i, j) = $irotl($size(inn), i, j)
def $binop(inn, ROTR, i, j) = $irotr($size(inn), i, j)

def $unop(I32, CLZ, i) = $iclz($size(I32), i)
def $unop(I32, CTZ, i) = $ictz($size(I32), i)
def $unop(I32, POPCNT, i) = $ipopcnt($size(I32), i)
def $testop(I32, EQZ, i) = $ieqz($size(I32), i)
def $relop(I32, EQ, i, j) = $ieq($size(I32), i, j)
def $relop(I32, NE, i, j) = $ine($size(I32), i, j)
def $relop(I32, LT sx, i, j) = $ilt($size(I32), sx, i, j)
def $relop(I32, GT sx, i, j) = $igt($size(I32), sx, i, j)
def $relop(I32, LE sx, i, j) = $ile($size(I32), sx, i, j)
def $relop(I32, GE sx, i, j) = $ige($size(I32), sx, i, j)
def $unop(inn, CLZ, i) = $iclz($size(inn), i)
def $unop(inn, CTZ, i) = $ictz($size(inn), i)
def $unop(inn, POPCNT, i) = $ipopcnt($size(inn), i)
def $unop(inn, EXTEND N, i) = $ext(N, $size(inn), S, $wrap($size(inn), N, i))
def $testop(inn, EQZ, i) = $ieqz($size(inn), i)
def $relop(inn, EQ, i, j) = $ieq($size(inn), i, j)
def $relop(inn, NE, i, j) = $ine($size(inn), i, j)
def $relop(inn, LT sx, i, j) = $ilt($size(inn), sx, i, j)
def $relop(inn, GT sx, i, j) = $igt($size(inn), sx, i, j)
def $relop(inn, LE sx, i, j) = $ile($size(inn), sx, i, j)
def $relop(inn, GE sx, i, j) = $ige($size(inn), sx, i, j)

def $binop(F32, ADD, f32_1, f32_2) = $fadd(32, f32_1, f32_2)

Expand Down
4 changes: 0 additions & 4 deletions spectec/spec/wasm-3.0/6-typing.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -693,10 +693,6 @@ rule Instr_ok/relop:
C |- RELOP nt relop_nt : nt nt -> I32


rule Instr_ok/extend:
C |- EXTEND nt n : nt -> nt
-- if n <= $size(nt)

rule Instr_ok/reinterpret:
C |- CVTOP nt_1 REINTERPRET nt_2 : nt_2 -> nt_1
-- if nt_1 =/= nt_2
Expand Down
4 changes: 0 additions & 4 deletions spectec/spec/wasm-3.0/8-reduction.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -229,10 +229,6 @@ rule Step_pure/relop:
-- if c = $relop(nt, relop, c_1, c_2)


rule Step_pure/extend:
(CONST inn c) (EXTEND inn N) ~> (CONST inn $ext(N, $size(inn), S, $wrap($size(inn), N, c)))


rule Step_pure/cvtop-val:
(CONST nt_1 c_1) (CVTOP nt_2 cvtop nt_1 sx?) ~> (CONST nt_2 c)
-- if $cvtop(nt_1, nt_2, cvtop, sx?, c_1) = c ;; TODO
Expand Down
10 changes: 5 additions & 5 deletions spectec/spec/wasm-3.0/A-binary.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -479,6 +479,7 @@ grammar Binstr/numeric-un-f64 : instr = ...
| 0x9D => UNOP F64 TRUNC
| 0x9E => UNOP F64 NEAREST
| 0x9F => UNOP F64 SQRT
| 0xC4 => UNOP I32 (EXTEND 32)
| ...

grammar Binstr/numeric-bin-f64 : instr = ...
Expand Down Expand Up @@ -521,11 +522,10 @@ grammar Binstr/numeric-cvt : instr = ...
| ...

grammar Binstr/numeric-extend : instr = ...
| 0xC0 => EXTEND I32 8
| 0xC1 => EXTEND I32 16
| 0xC2 => EXTEND I64 8
| 0xC3 => EXTEND I64 16
| 0xC4 => EXTEND I64 32
| 0xC0 => UNOP I32 (EXTEND 8)
| 0xC1 => UNOP I32 (EXTEND 16)
| 0xC2 => UNOP I32 (EXTEND 8)
| 0xC3 => UNOP I32 (EXTEND 16)
| ...


Expand Down
16 changes: 8 additions & 8 deletions spectec/src/backend-interpreter/construct.ml
Original file line number Diff line number Diff line change
Expand Up @@ -279,10 +279,10 @@ let al_to_int_unop: value -> IntOp.unop = function
| CaseV ("CLZ", []) -> IntOp.Clz
| CaseV ("CTZ", []) -> IntOp.Ctz
| CaseV ("POPCNT", []) -> IntOp.Popcnt
| CaseV ("EXTEND8S", []) -> IntOp.ExtendS Pack.Pack8
| CaseV ("EXTEND16S", []) -> IntOp.ExtendS Pack.Pack16
| CaseV ("EXTEND32S", []) -> IntOp.ExtendS Pack.Pack32
| CaseV ("EXTEND64S", []) -> IntOp.ExtendS Pack.Pack64
| CaseV ("EXTEND", [NumV z]) when z = Z.of_int 8 -> IntOp.ExtendS Pack.Pack8
| CaseV ("EXTEND", [NumV z]) when z = Z.of_int 16 -> IntOp.ExtendS Pack.Pack16
| CaseV ("EXTEND", [NumV z]) when z = Z.of_int 32 -> IntOp.ExtendS Pack.Pack32
| CaseV ("EXTEND", [NumV z]) when z = Z.of_int 64 -> IntOp.ExtendS Pack.Pack64
| v -> fail "integer unop" v
let al_to_float_unop: value -> FloatOp.unop = function
| CaseV ("NEG", []) -> FloatOp.Neg
Expand Down Expand Up @@ -1190,10 +1190,10 @@ let al_of_int_unop = function
| IntOp.Clz -> CaseV ("CLZ", [])
| IntOp.Ctz -> CaseV ("CTZ", [])
| IntOp.Popcnt -> CaseV ("POPCNT", [])
| IntOp.ExtendS Pack.Pack8 -> CaseV ("EXTEND8S", [])
| IntOp.ExtendS Pack.Pack16 -> CaseV ("EXTEND16S", [])
| IntOp.ExtendS Pack.Pack32 -> CaseV ("EXTEND32S", [])
| IntOp.ExtendS Pack.Pack64 -> CaseV ("EXTEND64S", [])
| IntOp.ExtendS Pack.Pack8 -> CaseV ("EXTEND", [al_of_int 8])
| IntOp.ExtendS Pack.Pack16 -> CaseV ("EXTEND", [al_of_int 16])
| IntOp.ExtendS Pack.Pack32 -> CaseV ("EXTEND", [al_of_int 32])
| IntOp.ExtendS Pack.Pack64 -> CaseV ("EXTEND", [al_of_int 64])
let al_of_float_unop = function
| FloatOp.Neg -> CaseV ("NEG", [])
| FloatOp.Abs -> CaseV ("ABS", [])
Expand Down
4 changes: 2 additions & 2 deletions spectec/src/backend-interpreter/numerics.ml
Original file line number Diff line number Diff line change
Expand Up @@ -455,8 +455,8 @@ let ext : numerics =
(function
| [ NumV z; _; CaseV ("U", []); NumV v ] when z = Z.of_int 128 -> V128.I64x2.of_lanes [ z_to_int64 v; 0L ] |> al_of_vec128 (* HARDCODE *)
| [ _; _; CaseV ("U", []); v ] -> v
| [ NumV _ as n; NumV _ as m; CaseV ("S", []); NumV _ as i ] ->
inverse_of_signed.f [ n; signed.f [ m; i] ]
| [ NumV _ as m; NumV _ as n; CaseV ("S", []); NumV _ as i ] ->
inverse_of_signed.f [ n; signed.f [ m; i ] ]
| _ -> failwith "Invalid argument fot ext"
);
}
Expand Down
8 changes: 0 additions & 8 deletions spectec/test-prose/doc/exec/instructions-in.rst
Original file line number Diff line number Diff line change
Expand Up @@ -38,14 +38,6 @@ $${rule-prose: exec/relop}

$${rule: Step_pure/relop}

.. _exec-extend:

$${rule-prose: exec/extend}

\

$${rule: Step_pure/extend}

.. _exec-cvtop:

$${rule-prose: exec/cvtop}
Expand Down
8 changes: 0 additions & 8 deletions spectec/test-prose/doc/valid/instructions-in.rst
Original file line number Diff line number Diff line change
Expand Up @@ -51,14 +51,6 @@ $${rule-prose: valid/relop}

$${rule: Instr_ok/relop}

.. _valid-extend:

$${rule-prose: valid/extend}

\

$${rule: Instr_ok/extend}

.. _valid-cvtop:

$${rule-prose: valid/cvtop}
Expand Down

0 comments on commit 0e09411

Please sign in to comment.