diff --git a/spectec/spec/wasm-3.0/1-syntax.watsup b/spectec/spec/wasm-3.0/1-syntax.watsup index bd924e310d..d4cb405717 100644 --- a/spectec/spec/wasm-3.0/1-syntax.watsup +++ b/spectec/spec/wasm-3.0/1-syntax.watsup @@ -304,7 +304,7 @@ syntax relop_(inn) = syntax relop_(fnn) = | EQ | NE | LT | GT | LE | GE -syntax cvtop = | CONVERT | REINTERPRET +syntax cvtop = | CONVERT | REINTERPRET | CONVERT_SAT ;; Vector operators diff --git a/spectec/spec/wasm-3.0/3-numerics.watsup b/spectec/spec/wasm-3.0/3-numerics.watsup index 42af7b72a2..7bfd293058 100644 --- a/spectec/spec/wasm-3.0/3-numerics.watsup +++ b/spectec/spec/wasm-3.0/3-numerics.watsup @@ -32,6 +32,12 @@ def $cvtop(numtype_1, numtype_2, cvtop, sx?, num_(numtype_1)) : num_(numtype_2)* def $wrap(M, N, iN(M)) : iN(N) hint(show $wrap_((%,%))#((%))) def $ext(M, N, sx, iN(M)) : iN(N) hint(show $ext_((%,%))^(%)#((%))) +def $trunc(M, N, sx, fN(M)) : iN(N) hint(show $trunc_((%,%))^(%)#((%))) +def $trunc_sat(M, N, sx, fN(M)) : iN(N) hint(show $trunc_sat_((%,%))^(%)#((%))) +def $demote(M, N, fN(M)) : fN(N) hint(show $demote_((%,%))#((%))) +def $promote(M, N, fN(M)) : fN(N) hint(show $promote_((%,%))#((%))) +def $convert(M, N, sx, iN(M)) : fN(N) hint(show $convert_((%,%))^(%)#((%))) +def $narrow(M, N, sx, iN(M)) : iN(N) hint(show $narrow_((%,%))^(%)#(%)) def $ibits(N, iN(N)) : bit* hint(show $bits_(i#%,%)) def $fbits(N, fN(N)) : bit* hint(show $bits_(f#%,%)) @@ -74,34 +80,81 @@ def $ile(N, sx, iN(N), iN(N)) : u32 hint(show $ile_%^(%)(%,%)) def $ige(N, sx, iN(N), iN(N)) : u32 hint(show $ihe_%^(%)(%,%)) def $fadd(N, fN(N), fN(N)) : fN(N) hint(show $fadd_%(%,%)) - -def $narrow(M, N, sx, iN(M)) : iN(N) hint(show $narrow_((%,%))^(%)#(%)) - -def $binop(inn, ADD, i, j) = $iadd($size(inn), i, j) -def $binop(inn, SUB, i, j) = $isub($size(inn), i, j) -def $binop(inn, MUL, i, j) = $imul($size(inn), i, j) -def $binop(inn, DIV sx, i, j) = $idiv($size(inn), sx, i, j) -def $binop(inn, REM sx, i, j) = $irem($size(inn), sx, i, j) -def $binop(inn, AND, i, j) = $iand($size(inn), i, j) -def $binop(inn, OR, i, j) = $ior($size(inn), i, j) -def $binop(inn, XOR, i, j) = $ixor($size(inn), i, j) -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(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) +def $fsub(N, fN(N), fN(N)) : fN(N) hint(show $fsub_%(%,%)) +def $fmul(N, fN(N), fN(N)) : fN(N) hint(show $fmul_%(%,%)) +def $fdiv(N, fN(N), fN(N)) : fN(N) hint(show $fdiv_%(%,%)) +def $fmin(N, fN(N), fN(N)) : fN(N) hint(show $fmin_%(%,%)) +def $fmax(N, fN(N), fN(N)) : fN(N) hint(show $fmax_%(%,%)) +def $fcopysign(N, fN(N), fN(N)) : fN(N) hint(show $fcopysign_%(%,%)) +def $fabs(N, fN(N)) : fN(N) hint(show $fabs_%(%)) +def $fneg(N, fN(N)) : fN(N) hint(show $fneg_%(%)) +def $fsqrt(N, fN(N)) : fN(N) hint(show $fsqrt_%(%)) +def $fceil(N, fN(N)) : fN(N) hint(show $fceil_%(%)) +def $ffloor(N, fN(N)) : fN(N) hint(show $ffloor_%(%)) +def $ftrunc(N, fN(N)) : fN(N) hint(show $ftrunc_%(%)) +def $fnearest(N, fN(N)) : fN(N) hint(show $fnearest_%(%)) +def $feq(N, fN(N), fN(N)) : u32 hint(show $feq_%(%,%)) +def $fne(N, fN(N), fN(N)) : u32 hint(show $fne_%(%,%)) +def $flt(N, fN(N), fN(N)) : u32 hint(show $flt_%(%,%)) +def $fgt(N, fN(N), fN(N)) : u32 hint(show $fgt_%(%,%)) +def $fle(N, fN(N), fN(N)) : u32 hint(show $fle_%(%,%)) +def $fge(N, fN(N), fN(N)) : u32 hint(show $fge_%(%,%)) + + +def $binop(inn, ADD, iN_1, iN_2) = $iadd($size(inn), iN_1, iN_2) +def $binop(inn, SUB, iN_1, iN_2) = $isub($size(inn), iN_1, iN_2) +def $binop(inn, MUL, iN_1, iN_2) = $imul($size(inn), iN_1, iN_2) +def $binop(inn, DIV sx, iN_1, iN_2) = $idiv($size(inn), sx, iN_1, iN_2) +def $binop(inn, REM sx, iN_1, iN_2) = $irem($size(inn), sx, iN_1, iN_2) +def $binop(inn, AND, iN_1, iN_2) = $iand($size(inn), iN_1, iN_2) +def $binop(inn, OR, iN_1, iN_2) = $ior($size(inn), iN_1, iN_2) +def $binop(inn, XOR, iN_1, iN_2) = $ixor($size(inn), iN_1, iN_2) +def $binop(inn, SHL, iN_1, iN_2) = $ishl($size(inn), iN_1, iN_2) +def $binop(inn, SHR sx, iN_1, iN_2) = $ishr($size(inn), sx, iN_1, iN_2) +def $binop(inn, ROTL, iN_1, iN_2) = $irotl($size(inn), iN_1, iN_2) +def $binop(inn, ROTR, iN_1, iN_2) = $irotr($size(inn), iN_1, iN_2) +def $unop(inn, CLZ, iN) = $iclz($size(inn), iN) +def $unop(inn, CTZ, iN) = $ictz($size(inn), iN) +def $unop(inn, POPCNT, iN) = $ipopcnt($size(inn), iN) +def $unop(inn, EXTEND N, iN) = $ext(N, $size(inn), S, $wrap($size(inn), N, iN)) +def $testop(inn, EQZ, iN) = $ieqz($size(inn), iN) +def $relop(inn, EQ, iN_1, iN_2) = $ieq($size(inn), iN_1, iN_2) +def $relop(inn, NE, iN_1, iN_2) = $ine($size(inn), iN_1, iN_2) +def $relop(inn, LT sx, iN_1, iN_2) = $ilt($size(inn), sx, iN_1, iN_2) +def $relop(inn, GT sx, iN_1, iN_2) = $igt($size(inn), sx, iN_1, iN_2) +def $relop(inn, LE sx, iN_1, iN_2) = $ile($size(inn), sx, iN_1, iN_2) +def $relop(inn, GE sx, iN_1, iN_2) = $ige($size(inn), sx, iN_1, iN_2) + +def $binop(fnn, ADD, fN_1, fN_2) = $fadd($size(fnn), fN_1, fN_2) +def $binop(fnn, SUB, fN_1, fN_2) = $fsub($size(fnn), fN_1, fN_2) +def $binop(fnn, MUL, fN_1, fN_2) = $fmul($size(fnn), fN_1, fN_2) +def $binop(fnn, DIV, fN_1, fN_2) = $fdiv($size(fnn), fN_1, fN_2) +def $binop(fnn, MIN, fN_1, fN_2) = $fmin($size(fnn), fN_1, fN_2) +def $binop(fnn, MAX, fN_1, fN_2) = $fmax($size(fnn), fN_1, fN_2) +def $binop(fnn, COPYSIGN, fN_1, fN_2) = $fcopysign($size(fnn), fN_1, fN_2) + +def $unop(fnn, ABS, fN) = $fabs($size(fnn), fN) +def $unop(fnn, NEG, fN) = $fneg($size(fnn), fN) +def $unop(fnn, SQRT, fN) = $fsqrt($size(fnn), fN) +def $unop(fnn, CEIL, fN) = $fceil($size(fnn), fN) +def $unop(fnn, FLOOR, fN) = $ffloor($size(fnn), fN) +def $unop(fnn, TRUNC, fN) = $ftrunc($size(fnn), fN) +def $unop(fnn, NEAREST, fN) = $fnearest($size(fnn), fN) + +def $relop(fnn, EQ, fN_1, fN_2) = $feq($size(fnn), fN_1, fN_2) +def $relop(fnn, NE, fN_1, fN_2) = $fne($size(fnn), fN_1, fN_2) +def $relop(fnn, LT, fN_1, fN_2) = $flt($size(fnn), fN_1, fN_2) +def $relop(fnn, GT, fN_1, fN_2) = $fgt($size(fnn), fN_1, fN_2) +def $relop(fnn, LE, fN_1, fN_2) = $fle($size(fnn), fN_1, fN_2) +def $relop(fnn, GE, fN_1, fN_2) = $fge($size(fnn), fN_1, fN_2) + +def $cvtop(I32, I64, CONVERT, sx, iN) = $ext(32, 64, sx, iN) +def $cvtop(I64, I32, CONVERT, sx?, iN) = $wrap(32, 64, iN) +def $cvtop(fnn, inn, CONVERT, sx, fN) = $trunc($size(fnn), $size(inn), sx, fN) +def $cvtop(fnn, inn, CONVERT_SAT, sx, fN) = $trunc_sat($size(fnn), $size(inn), sx, fN) +def $cvtop(F32, F64, CONVERT, sx?, fN) = $demote(32, 64, fN) +def $cvtop(F64, F32, CONVERT, sx?, fN) = $promote(64, 32, fN) +def $cvtop(inn, fnn, CONVERT, sx, iN) = $convert($size(inn), $size(fnn), sx, iN) -- if $size(inn) =/= $size(fnn) ;; Packed values diff --git a/spectec/src/backend-interpreter/construct.ml b/spectec/src/backend-interpreter/construct.ml index 4810f7d6a9..48bbf270d7 100644 --- a/spectec/src/backend-interpreter/construct.ml +++ b/spectec/src/backend-interpreter/construct.ml @@ -354,45 +354,45 @@ let al_to_float_relop: value -> FloatOp.relop = function let al_to_relop: value list -> relop = al_to_op al_to_int_relop al_to_float_relop let al_to_int_cvtop: value list -> IntOp.cvtop = function - | CaseV ("EXTEND", []) :: args -> - (match args with - | [ CaseV ("I32", []); OptV (Some (CaseV ("S", []))) ] -> IntOp.ExtendSI32 - | [ CaseV ("I32", []); OptV (Some (CaseV ("U", []))) ] -> IntOp.ExtendUI32 - | l -> fail_list "extend" l) - | [ CaseV ("Wrap", []); CaseV ("I64", []); OptV None ] -> IntOp.WrapI64 - | CaseV ("TRUNC", []) :: args -> + | [ CaseV ("I64", []); CaseV ("CONVERT", []); CaseV ("I32", []); opt ] as l -> + (match opt with + | OptV (Some (CaseV ("S", []))) -> IntOp.ExtendSI32 + | OptV (Some (CaseV ("U", []))) -> IntOp.ExtendUI32 + | _ -> fail_list "extend" l) + | CaseV ("I32", []) :: [ CaseV ("CONVERT", []); CaseV ("I64", []); OptV None ] -> IntOp.WrapI64 + | CaseV (_, []) :: CaseV ("CONVERT", []) :: args -> (match args with | [ CaseV ("F32", []); OptV (Some (CaseV ("S", []))) ] -> IntOp.TruncSF32 | [ CaseV ("F32", []); OptV (Some (CaseV ("U", []))) ] -> IntOp.TruncUF32 | [ CaseV ("F64", []); OptV (Some (CaseV ("S", []))) ] -> IntOp.TruncSF64 | [ CaseV ("F64", []); OptV (Some (CaseV ("U", []))) ] -> IntOp.TruncUF64 | l -> fail_list "trunc" l) - | CaseV ("TRUNCSAT", []) :: args -> + | CaseV (_, []) :: CaseV ("CONVERT_SAT", []) :: args -> (match args with | [ CaseV ("F32", []); OptV (Some (CaseV ("S", []))) ] -> IntOp.TruncSatSF32 | [ CaseV ("F32", []); OptV (Some (CaseV ("U", []))) ] -> IntOp.TruncSatUF32 | [ CaseV ("F64", []); OptV (Some (CaseV ("S", []))) ] -> IntOp.TruncSatSF64 | [ CaseV ("F64", []); OptV (Some (CaseV ("U", []))) ] -> IntOp.TruncSatUF64 | l -> fail_list "truncsat" l) - | [ CaseV ("REINTERPRET", []); _; OptV None ] -> IntOp.ReinterpretFloat + | [ _; CaseV ("REINTERPRET", []); _; OptV None ] -> IntOp.ReinterpretFloat | l -> fail_list "integer cvtop" l let al_to_float_cvtop : value list -> FloatOp.cvtop = function - | CaseV ("CONVERT", []) :: args -> - (match args with - | [ CaseV ("I32", []); OptV (Some (CaseV (("S", [])))) ] -> FloatOp.ConvertSI32 - | [ CaseV ("I32", []); OptV (Some (CaseV (("U", [])))) ] -> FloatOp.ConvertUI32 - | [ CaseV ("I64", []); OptV (Some (CaseV (("S", [])))) ] -> FloatOp.ConvertSI64 - | [ CaseV ("I64", []); OptV (Some (CaseV (("U", [])))) ] -> FloatOp.ConvertUI64 - | l -> fail_list "convert" l) - | [ CaseV ("PROMOTE", []); CaseV ("F32", []); OptV None ] -> FloatOp.PromoteF32 - | [ CaseV ("DEMOTE", []); CaseV ("F64", []); OptV None ] -> FloatOp.DemoteF64 - | [ CaseV ("REINTERPRET", []); _; OptV None ] -> FloatOp.ReinterpretInt + | [ CaseV (_, []); CaseV ("CONVERT", []); CaseV (nt, []); OptV (Some (CaseV (opt, []))) ] as l -> + (match nt, opt with + | "I32", "S" -> FloatOp.ConvertSI32 + | "I32", "U" -> FloatOp.ConvertUI32 + | "I64", "S" -> FloatOp.ConvertSI64 + | "I64", "U" -> FloatOp.ConvertUI64 + | _ -> fail_list "convert" l) + | [ CaseV ("F64", []); CaseV ("CONVERT", []); CaseV ("F32", []); OptV None ] -> FloatOp.PromoteF32 + | [ CaseV ("F32", []); CaseV ("CONVERT", []); CaseV ("F64", []); OptV None ] -> FloatOp.DemoteF64 + | [ _; CaseV ("REINTERPRET", []); _; OptV None ] -> FloatOp.ReinterpretInt | l -> fail_list "float cvtop" l let al_to_cvtop: value list -> cvtop = function - | CaseV ("I32", []) :: op -> I32 (al_to_int_cvtop op) - | CaseV ("I64", []) :: op -> I64 (al_to_int_cvtop op) - | CaseV ("F32", []) :: op -> F32 (al_to_float_cvtop op) - | CaseV ("F64", []) :: op -> F64 (al_to_float_cvtop op) + | CaseV ("I32", []) :: _ as op -> I32 (al_to_int_cvtop op) + | CaseV ("I64", []) :: _ as op -> I64 (al_to_int_cvtop op) + | CaseV ("F32", []) :: _ as op -> F32 (al_to_float_cvtop op) + | CaseV ("F64", []) :: _ as op -> F64 (al_to_float_cvtop op) | l -> fail_list "cvtop" l (* Vector operator *) @@ -1257,25 +1257,25 @@ let al_of_float_relop = function let al_of_relop = al_of_op al_of_int_relop al_of_float_relop let al_of_int_cvtop num_bits = function - | IntOp.ExtendSI32 -> "Extend", "I32", Some (nullary "S") - | IntOp.ExtendUI32 -> "Extend", "I32", Some (nullary "U") - | IntOp.WrapI64 -> "Wrap", "I64", None - | IntOp.TruncSF32 -> "Trunc", "F32", Some (nullary "S") - | IntOp.TruncUF32 -> "Trunc", "F32", Some (nullary "U") - | IntOp.TruncSF64 -> "Trunc", "F64", Some (nullary "S") - | IntOp.TruncUF64 -> "Trunc", "F64", Some (nullary "U") - | IntOp.TruncSatSF32 -> "TruncSat", "F32", Some (nullary "S") - | IntOp.TruncSatUF32 -> "TruncSat", "F32", Some (nullary "U") - | IntOp.TruncSatSF64 -> "TruncSat", "F64", Some (nullary "S") - | IntOp.TruncSatUF64 -> "TruncSat", "F64", Some (nullary "U") + | IntOp.ExtendSI32 -> "Convert", "I64", Some (nullary "S") + | IntOp.ExtendUI32 -> "Convert", "I64", Some (nullary "U") + | IntOp.WrapI64 -> "Convert", "I64", None + | IntOp.TruncSF32 -> "Convert", "F32", Some (nullary "S") + | IntOp.TruncUF32 -> "Convert", "F32", Some (nullary "U") + | IntOp.TruncSF64 -> "Convert", "F64", Some (nullary "S") + | IntOp.TruncUF64 -> "Convert", "F64", Some (nullary "U") + | IntOp.TruncSatSF32 -> "Convert_sat", "F32", Some (nullary "S") + | IntOp.TruncSatUF32 -> "Convert_sat", "F32", Some (nullary "U") + | IntOp.TruncSatSF64 -> "Convert_sat", "F64", Some (nullary "S") + | IntOp.TruncSatUF64 -> "Convert_sat", "F64", Some (nullary "U") | IntOp.ReinterpretFloat -> "Reinterpret", "F" ^ num_bits, None let al_of_float_cvtop num_bits = function | FloatOp.ConvertSI32 -> "Convert", "I32", Some (nullary ("S")) | FloatOp.ConvertUI32 -> "Convert", "I32", Some (nullary ("U")) | FloatOp.ConvertSI64 -> "Convert", "I64", Some (nullary ("S")) | FloatOp.ConvertUI64 -> "Convert", "I64", Some (nullary ("U")) - | FloatOp.PromoteF32 -> "Promote", "F32", None - | FloatOp.DemoteF64 -> "Demote", "F64", None + | FloatOp.PromoteF32 -> "Convert", "F32", None + | FloatOp.DemoteF64 -> "Convert", "F64", None | FloatOp.ReinterpretInt -> "Reinterpret", "I" ^ num_bits, None let al_of_cvtop = function | I32 op -> diff --git a/spectec/src/backend-interpreter/ds.ml b/spectec/src/backend-interpreter/ds.ml index 405b591873..3e69fca305 100644 --- a/spectec/src/backend-interpreter/ds.ml +++ b/spectec/src/backend-interpreter/ds.ml @@ -233,7 +233,7 @@ module WasmContext = struct | h :: _ -> h | _ -> failwith "Wasm context stack underflow" - let init_context () = context_stack := [top_level_context] + let init_context () = context_stack := [FrameV (None, strV Record.empty), [], []; top_level_context] let push_context ctx = context_stack := ctx :: !context_stack diff --git a/spectec/src/backend-interpreter/numerics.ml b/spectec/src/backend-interpreter/numerics.ml index e17ed3e9ad..eaf14569c6 100644 --- a/spectec/src/backend-interpreter/numerics.ml +++ b/spectec/src/backend-interpreter/numerics.ml @@ -21,9 +21,6 @@ let i16_to_i32 i16 = (* NOTE: This operation extends the sign of i8 to i32 *) I32.shr_s (I32.shl i16 16l) 16l -let i32_to_i8 i32 = Int32.logand 0xffl i32 -let i32_to_i16 i32 = Int32.logand 0xffffl i32 - let signed : numerics = { name = "signed"; @@ -67,7 +64,7 @@ let sat : numerics = inverse_of_signed.f [ NumV z; NumV Z.(shift_left one n |> pred) ] else NumV i - | v -> fail_list "Invalid idiv" v + | v -> fail_list "Invalid isat" v ); } @@ -121,7 +118,7 @@ let idiv : numerics = | v -> fail_list "Invalid idiv" v ); } -let irem: numerics = +let irem : numerics = { name = "irem"; f = @@ -281,7 +278,7 @@ let ipopcnt : numerics = let acc' = if Z.(equal (logand n one) one) then acc + 1 else acc in loop acc' (i - 1) (Z.shift_right n 1) in al_of_int (loop 0 (Z.to_int z) m) - | v -> fail_list "Invalid popcnt" v + | v -> fail_list "Invalid ipopcnt" v ); } let ieqz : numerics = @@ -448,6 +445,247 @@ let iq15mulrsat_s : numerics = ); } +let fadd : numerics = + { + name = "fadd"; + f = + (function + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 32 -> + F32.add (al_to_float32 f1) (al_to_float32 f2) |> al_of_float32 + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 64 -> + F64.add (al_to_float64 f1) (al_to_float64 f2) |> al_of_float64 + | v -> fail_list "Invalid fadd" v + ); + } +let fsub : numerics = + { + name = "fsub"; + f = + (function + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 32 -> + F32.sub (al_to_float32 f1) (al_to_float32 f2) |> al_of_float32 + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 64 -> + F64.sub (al_to_float64 f1) (al_to_float64 f2) |> al_of_float64 + | v -> fail_list "Invalid fsub" v + ); + } +let fmul : numerics = + { + name = "fmul"; + f = + (function + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 32 -> + F32.mul (al_to_float32 f1) (al_to_float32 f2) |> al_of_float32 + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 64 -> + F64.mul (al_to_float64 f1) (al_to_float64 f2) |> al_of_float64 + | v -> fail_list "Invalid fmul" v + ); + } +let fdiv : numerics = + { + name = "fdiv"; + f = + (function + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 32 -> + F32.div (al_to_float32 f1) (al_to_float32 f2) |> al_of_float32 + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 64 -> + F64.div (al_to_float64 f1) (al_to_float64 f2) |> al_of_float64 + | v -> fail_list "Invalid fdiv" v + ); + } +let fmin : numerics = + { + name = "fmin"; + f = + (function + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 32 -> + F32.min (al_to_float32 f1) (al_to_float32 f2) |> al_of_float32 + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 64 -> + F64.min (al_to_float64 f1) (al_to_float64 f2) |> al_of_float64 + | v -> fail_list "Invalid fmin" v + ); + } +let fmax : numerics = + { + name = "fmax"; + f = + (function + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 32 -> + F32.max (al_to_float32 f1) (al_to_float32 f2) |> al_of_float32 + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 64 -> + F64.max (al_to_float64 f1) (al_to_float64 f2) |> al_of_float64 + | v -> fail_list "Invalid fmax" v + ); + } +let fcopysign : numerics = + { + name = "fcopysign"; + f = + (function + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 32 -> + F32.copysign (al_to_float32 f1) (al_to_float32 f2) |> al_of_float32 + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 64 -> + F64.copysign (al_to_float64 f1) (al_to_float64 f2) |> al_of_float64 + | v -> fail_list "Invalid fcopysign" v + ); + } +let fabs : numerics = + { + name = "fabs"; + f = + (function + | [ NumV z; CaseV _ as f ] when z = Z.of_int 32 -> + F32.abs (al_to_float32 f) |> al_of_float32 + | [ NumV z; CaseV _ as f ] when z = Z.of_int 64 -> + F64.abs (al_to_float64 f) |> al_of_float64 + | v -> fail_list "Invalid fabs" v + ); + } +let fneg : numerics = + { + name = "fneg"; + f = + (function + | [ NumV z; CaseV _ as f ] when z = Z.of_int 32 -> + F32.neg (al_to_float32 f) |> al_of_float32 + | [ NumV z; CaseV _ as f ] when z = Z.of_int 64 -> + F64.neg (al_to_float64 f) |> al_of_float64 + | v -> fail_list "Invalid fneg" v + ); + } +let fsqrt : numerics = + { + name = "fsqrt"; + f = + (function + | [ NumV z; CaseV _ as f ] when z = Z.of_int 32 -> + F32.sqrt (al_to_float32 f) |> al_of_float32 + | [ NumV z; CaseV _ as f ] when z = Z.of_int 64 -> + F64.sqrt (al_to_float64 f) |> al_of_float64 + | v -> fail_list "Invalid fsqrt" v + ); + } +let fceil : numerics = + { + name = "fceil"; + f = + (function + | [ NumV z; CaseV _ as f ] when z = Z.of_int 32 -> + F32.ceil (al_to_float32 f) |> al_of_float32 + | [ NumV z; CaseV _ as f ] when z = Z.of_int 64 -> + F64.ceil (al_to_float64 f) |> al_of_float64 + | v -> fail_list "Invalid fceil" v + ); + } +let ffloor : numerics = + { + name = "ffloor"; + f = + (function + | [ NumV z; CaseV _ as f ] when z = Z.of_int 32 -> + F32.floor (al_to_float32 f) |> al_of_float32 + | [ NumV z; CaseV _ as f ] when z = Z.of_int 64 -> + F64.floor (al_to_float64 f) |> al_of_float64 + | v -> fail_list "Invalid ffloor" v + ); + } +let ftrunc : numerics = + { + name = "ftrunc"; + f = + (function + | [ NumV z; CaseV _ as f ] when z = Z.of_int 32 -> + F32.trunc (al_to_float32 f) |> al_of_float32 + | [ NumV z; CaseV _ as f ] when z = Z.of_int 64 -> + F64.trunc (al_to_float64 f) |> al_of_float64 + | v -> fail_list "Invalid ftrunc" v + ); + } +let fnearest : numerics = + { + name = "fnearest"; + f = + (function + | [ NumV z; CaseV _ as f ] when z = Z.of_int 32 -> + F32.nearest (al_to_float32 f) |> al_of_float32 + | [ NumV z; CaseV _ as f ] when z = Z.of_int 64 -> + F64.nearest (al_to_float64 f) |> al_of_float64 + | v -> fail_list "Invalid fnearest" v + ); + } +let feq : numerics = + { + name = "feq"; + f = + (function + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 32 -> + F32.eq (al_to_float32 f1) (al_to_float32 f2) |> al_of_bool + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 64 -> + F64.eq (al_to_float64 f1) (al_to_float64 f2) |> al_of_bool + | v -> fail_list "Invalid feq" v + ); + } +let fne : numerics = + { + name = "fne"; + f = + (function + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 32 -> + F32.ne (al_to_float32 f1) (al_to_float32 f2) |> al_of_bool + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 64 -> + F64.ne (al_to_float64 f1) (al_to_float64 f2) |> al_of_bool + | v -> fail_list "Invalid fne" v + ); + } +let flt : numerics = + { + name = "flt"; + f = + (function + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 32 -> + F32.lt (al_to_float32 f1) (al_to_float32 f2) |> al_of_bool + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 64 -> + F64.lt (al_to_float64 f1) (al_to_float64 f2) |> al_of_bool + | v -> fail_list "Invalid flt" v + ); + } +let fgt : numerics = + { + name = "fgt"; + f = + (function + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 32 -> + F32.gt (al_to_float32 f1) (al_to_float32 f2) |> al_of_bool + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 64 -> + F64.gt (al_to_float64 f1) (al_to_float64 f2) |> al_of_bool + | v -> fail_list "Invalid fgt" v + ); + } +let fle : numerics = + { + name = "fle"; + f = + (function + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 32 -> + F32.le (al_to_float32 f1) (al_to_float32 f2) |> al_of_bool + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 64 -> + F64.le (al_to_float64 f1) (al_to_float64 f2) |> al_of_bool + | v -> fail_list "Invalid fle" v + ); + } +let fge : numerics = + { + name = "fge"; + f = + (function + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 32 -> + F32.ge (al_to_float32 f1) (al_to_float32 f2) |> al_of_bool + | [ NumV z; CaseV _ as f1; CaseV _ as f2; ] when z = Z.of_int 64 -> + F64.ge (al_to_float64 f1) (al_to_float64 f2) |> al_of_bool + | v -> fail_list "Invalid fge" v + ); + } + let ext : numerics = { name = "ext"; @@ -461,6 +699,56 @@ let ext : numerics = ); } +let trunc : numerics = + { + name = "trunc"; + f = + (function + | [ NumV m; NumV n; CaseV ("U", []); NumV _ as i ] when m = Z.of_int 32 && n = Z.of_int 32 -> + i |> al_to_float32 |> I32_convert.trunc_f32_u |> al_of_int32 + | [ NumV m; NumV n; CaseV ("U", []); NumV _ as i ] when m = Z.of_int 64 && n = Z.of_int 32 -> + i |> al_to_float32 |> I64_convert.trunc_f32_u |> al_of_int64 + | [ NumV m; NumV n; CaseV ("U", []); NumV _ as i ] when m = Z.of_int 32 && n = Z.of_int 64 -> + i |> al_to_float64 |> I32_convert.trunc_f64_u |> al_of_int32 + | [ NumV m; NumV n; CaseV ("U", []); NumV _ as i ] when m = Z.of_int 64 && n = Z.of_int 64 -> + i |> al_to_float64 |> I64_convert.trunc_f64_u |> al_of_int64 + | [ NumV m; NumV n; CaseV ("S", []); NumV _ as i ] when m = Z.of_int 32 && n = Z.of_int 32 -> + i |> al_to_float32 |> I32_convert.trunc_f32_s |> al_of_int32 + | [ NumV m; NumV n; CaseV ("S", []); NumV _ as i ] when m = Z.of_int 64 && n = Z.of_int 32 -> + i |> al_to_float32 |> I64_convert.trunc_f32_s |> al_of_int64 + | [ NumV m; NumV n; CaseV ("S", []); NumV _ as i ] when m = Z.of_int 32 && n = Z.of_int 64 -> + i |> al_to_float64 |> I32_convert.trunc_f64_s |> al_of_int32 + | [ NumV m; NumV n; CaseV ("S", []); NumV _ as i ] when m = Z.of_int 64 && n = Z.of_int 64 -> + i |> al_to_float64 |> I64_convert.trunc_f64_s |> al_of_int64 + | v -> fail_list "Invalid trunc" v + ); + } + +let trunc_sat : numerics = + { + name = "trunc_sat"; + f = + (function + | [ NumV m; NumV n; CaseV ("U", []); NumV _ as i ] when m = Z.of_int 32 && n = Z.of_int 32 -> + i |> al_to_float32 |> I32_convert.trunc_sat_f32_u |> al_of_int32 + | [ NumV m; NumV n; CaseV ("U", []); NumV _ as i ] when m = Z.of_int 64 && n = Z.of_int 32 -> + i |> al_to_float32 |> I64_convert.trunc_sat_f32_u |> al_of_int64 + | [ NumV m; NumV n; CaseV ("U", []); NumV _ as i ] when m = Z.of_int 32 && n = Z.of_int 64 -> + i |> al_to_float64 |> I32_convert.trunc_sat_f64_u |> al_of_int32 + | [ NumV m; NumV n; CaseV ("U", []); NumV _ as i ] when m = Z.of_int 64 && n = Z.of_int 64 -> + i |> al_to_float64 |> I64_convert.trunc_sat_f64_u |> al_of_int64 + | [ NumV m; NumV n; CaseV ("S", []); NumV _ as i ] when m = Z.of_int 32 && n = Z.of_int 32 -> + i |> al_to_float32 |> I32_convert.trunc_sat_f32_s |> al_of_int32 + | [ NumV m; NumV n; CaseV ("S", []); NumV _ as i ] when m = Z.of_int 64 && n = Z.of_int 32 -> + i |> al_to_float32 |> I64_convert.trunc_sat_f32_s |> al_of_int64 + | [ NumV m; NumV n; CaseV ("S", []); NumV _ as i ] when m = Z.of_int 32 && n = Z.of_int 64 -> + i |> al_to_float64 |> I32_convert.trunc_sat_f64_s |> al_of_int32 + | [ NumV m; NumV n; CaseV ("S", []); NumV _ as i ] when m = Z.of_int 64 && n = Z.of_int 64 -> + i |> al_to_float64 |> I64_convert.trunc_sat_f64_s |> al_of_int64 + | v -> fail_list "Invalid trunc_sat" v + ); + } + let ibytes : numerics = { name = "ibytes"; @@ -876,18 +1164,8 @@ let narrow : numerics = name = "narrow"; f = (function - | [ NumV _; NumV n; CaseV ("S", []); NumV i ] -> ( - match z_to_int64 n with - | 8L -> NumV (i |> z_to_int32 |> i16_to_i32 |> I8.saturate_s |> i32_to_i8 |> Z.of_int32) - | 16L -> NumV (i |> z_to_int32 |> I16.saturate_s |> i32_to_i16 |> Z.of_int32) - | _ -> failwith "Invalid narrow" - ) - | [ NumV _; NumV n; CaseV ("U", []); NumV i ] -> ( - match z_to_int64 n with - | 8L -> NumV (i |> z_to_int32 |> i16_to_i32 |> I8.saturate_u |> Z.of_int32) - | 16L -> NumV (i |> z_to_int32 |> I16.saturate_u |> i32_to_i16 |> Z.of_int32) - | _ -> failwith "Invalid narrow" - ) + | [ NumV _ as m; NumV _ as n; CaseV (_, []) as sx; NumV _ as i ] -> + sat.f [ n; sx; signed.f [ m; i ]] | _ -> failwith "Invalid narrow"); } @@ -1058,11 +1336,33 @@ let numerics_list : numerics list = [ iaddsat; isubsat; iq15mulrsat_s; + fadd; + fsub; + fmul; + fdiv; + fmin; + fmax; + fcopysign; + fabs; + fneg; + fsqrt; + fceil; + ffloor; + ftrunc; + fnearest; + feq; + fne; + flt; + fgt; + fle; + fge; ext; wrap; + trunc; + trunc_sat; + narrow; vrelop; vishiftop; - narrow; lanes; inverse_of_lanes; inverse_of_lsize; diff --git a/spectec/src/il2al/transpile.ml b/spectec/src/il2al/transpile.ml index 00d883afe9..c7ac6217c2 100644 --- a/spectec/src/il2al/transpile.ml +++ b/spectec/src/il2al/transpile.ml @@ -94,8 +94,10 @@ let unify_tail l1 l2 = let unified, l1', l2' = unify [] (List.rev l1) (List.rev l2) in List.rev unified, List.rev l1', List.rev l2' +(* let intersect_list xs ys = List.filter (fun x -> List.mem x ys) xs let diff_list xs ys = Lib.List.filter_not (fun x -> List.mem x ys) xs +*) (* AL -> AL transpilers *) @@ -265,6 +267,7 @@ let merge_three_branches i = ifI (binE (AndOp, neg e1, e2), il2, il1) ~at:at | _ -> i +(* let remove_dead_assignment il = let rec remove_dead_assignment' il pair = List.fold_right @@ -294,6 +297,7 @@ let remove_dead_assignment il = il pair in remove_dead_assignment' il ([], []) |> fst +*) let remove_sub e = let e' = @@ -407,7 +411,6 @@ let rec enhance_readability instrs = let instrs' = instrs - |> remove_dead_assignment |> unify_if |> infer_else |> List.concat_map remove_unnecessary_branch @@ -493,7 +496,7 @@ let remove_state algo = match Walk.walk walk_config algo with | FuncA (name, params, body) -> (match params with | { it = TupE [ _; { it = VarE "f"; _ } ]; _ } :: tail -> - FuncA (name, tail, letI (varE "f", getCurFrameE ()) :: body |> remove_dead_assignment) + FuncA (name, tail, letI (varE "f", getCurFrameE ()) :: body) | { it = VarE ("s" | "z"); _ } :: tail -> FuncA (name, tail, body) | _ -> FuncA(name, params, body))