Added floating point and conversion numerics

commented out remote_dead_assignemnt

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

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

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 ->

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