Merge wide-arithmetic proposal into the specification

.github/workflows/ci-interpreter.yml

@@ -22,6 +22,8 @@ jobs:
         uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: 5.04.x
+      - name: Setup OCaml tools
+        run: opam install --yes stdint.0.7.2
       - name: Build interpreter
         run: cd interpreter && opam exec make jsdeps wasm
       # Neither V8 nor SpiderMonkey can currently handle all 3.0 tests, so we disable checking JS translation for now.

.github/workflows/ci-spec.yml

@@ -34,7 +34,7 @@ jobs:
         with:
           ocaml-compiler: 5.04.x
       - name: Setup Dune
-        run: opam install --yes dune menhir mdx zarith && opam exec dune --version
+        run: opam install --yes dune menhir mdx zarith stdint.0.7.2 && opam exec dune --version
       - name: Setup Node.js
         uses: actions/setup-node@v4
         with:

.github/workflows/ci-spectec.yml

@@ -23,7 +23,7 @@ jobs:
         with:
           ocaml-compiler: 5.04.x
       - name: Setup Dune
-        run: opam install --yes dune menhir mdx zarith
+        run: opam install --yes dune menhir mdx zarith stdint.0.7.2
       - name: Setup Latex
         run: sudo apt-get update -y && sudo apt-get install -y latexmk texlive-latex-recommended texlive-latex-extra texlive-fonts-recommended
       - name: Setup Sphinx

document/core/binary/instructions.rst

@@ -256,6 +256,13 @@ whereas the actual opcode is encoded by a variable-length :ref:`unsigned integer
 
 $${grammar: Binstr/num-cvt-sat}
 
+.. _binary-num-wide:
+
+wide-arithmetic instructions have a 1-byte prefix and the actual opcode is
+encoded by a variable-length :ref:`unsigned integer <binary-uint>`.
+
+$${grammar: Binstr/num-wide}
+
 
 .. index:: vector instruction
    pair: binary format; instruction

document/core/exec/instructions.rst

@@ -941,6 +941,20 @@ $${rule-prose: Step_pure/cvtop}
 $${rule: {Step_pure/cvtop-*}}
 
 
+.. _exec-wideop:
+
+$${rule-prose: Step_pure/wideop}
+
+$${rule: {Step_pure/wideop}}
+
+
+.. _exec-extwideop:
+
+$${rule-prose: Step_pure/extwideop}
+
+$${rule: {Step_pure/extwideop}}
+
+
 .. index:: vector instruction
    pair: execution; instruction
    single: abstract syntax; instruction

document/core/exec/numerics.rst

@@ -934,6 +934,37 @@ The integer result of predicates -- i.e., :ref:`tests <syntax-testop>` and :ref:
    \iq15mulrsats_N(i_1, i_2) &=& \signed_N^{-1}(\sats_N(\ishrs_N(i_1 \cdot i_2 + 2^{14}, 15)))
    \end{array}
 
+.. _op-iconcat:
+
+:math:`\iconcat_{M,N}(i_1, i_2)`
+.................................
+
+* Let :math:`h` be the result of :math:`\ishl_N(\extend^u_{M,N}(i_2), M)`
+
+* Return the result of :math:`\ior_N(\extend^u_{M,N}(i_1), h)`
+
+.. math::
+   \begin{array}{lll@{\qquad}l}
+   \iconcat_{M,N}(i_1, i_2) &=& \ior_N(\extend^u_{M,N}(i_1), \ishl_N(\extend^u_{M,N}(i_2), M))
+   \end{array}
+
+
+.. _op-isplit:
+
+:math:`\isplit_{M,N}(i)`
+.................................
+
+* Let :math:`l` be the result of :math:`\wrap_{M,N}(i)`
+
+* Let :math:`h` be the result of :math:`\wrap_{M,N}(\ishru_M(i, N))`
+
+* Return :math:`l, h`
+
+.. math::
+   \begin{array}{lll@{\qquad}l}
+   \isplit_{M,N}(i) &=& \wrap_{M,N}(i), \wrap_{M,N}(\ishru_M(i, N))
+   \end{array}
+
 
 .. index:: floating-point, IEEE 754
 .. _float-ops:

document/core/syntax/instructions.rst

@@ -330,14 +330,16 @@ The instructions ${:ANY.CONVERT_EXTERN} and ${:EXTERN.CONVERT_ANY} allow lossles
 .. _syntax-relop:
 .. _syntax-cvtop:
 .. _syntax-instr-numeric:
+.. _syntax-wideop:
+.. _syntax-extwideop:
 
 Numeric Instructions
 ~~~~~~~~~~~~~~~~~~~~
 
 Numeric instructions provide basic operations over numeric :ref:`values <syntax-value>` of specific :ref:`type <syntax-numtype>`.
 These operations closely match respective operations available in hardware.
 
-$${syntax: {sz sx} num_ instr/num unop_ binop_ testop_ relop_ cvtop__}
+$${syntax: {sz sx} num_ instr/num unop_ binop_ testop_ relop_ cvtop__ wideop_ extwideop_}
 
 Numeric instructions are divided by :ref:`number type <syntax-numtype>`.
 For each type, several subcategories can be distinguished:

document/core/text/instructions.rst

@@ -297,6 +297,12 @@ $${grammar: {
   Tplaininstr_/num-cvt-reinterpret
 }}
 
+.. _text-wideop:
+
+$${grammar: {
+  Tplaininstr_/num-wide
+}}
+
 
 .. index:: vector instruction
    pair: text format; instruction

document/core/util/macros.def

@@ -616,6 +616,10 @@
 .. |DEMOTE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{demote}}
 .. |REINTERPRET| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{reinterpret}}
 
+.. |ADD128| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{add128}}
+.. |SUB128| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{sub128}}
+.. |MULWIDE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{mul\_wide}}
+
 .. |VCONST| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{const}}
 .. |VSHUFFLE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{shuffle}}
 .. |VSWIZZLE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{swizzle}}
@@ -694,6 +698,8 @@
 .. |testop| mathdef:: \xref{syntax/instructions}{syntax-testop}{\X{testop}}
 .. |relop| mathdef:: \xref{syntax/instructions}{syntax-relop}{\X{relop}}
 .. |cvtop| mathdef:: \xref{syntax/instructions}{syntax-cvtop}{\X{cvtop}}
+.. |wideop| mathdef:: \xref{syntax/instructions}{syntax-wideop}{\X{wideop}}
+.. |extwideop| mathdef:: \xref{syntax/instructions}{syntax-extwideop}{\X{extwideop}}
 
 .. |unopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{unop}}
 .. |binopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{binop}}
@@ -1637,6 +1643,8 @@
 .. |iavgru| mathdef:: \xref{exec/numerics}{op-iavgr}{\F{iavgr\_u}}
 .. |iq15mulrsat| mathdef:: \xref{exec/numerics}{op-iq15mulrsat}{\F{iq15mulrsat}}
 .. |iq15mulrsats| mathdef:: \xref{exec/numerics}{op-iq15mulrsat}{\F{iq15mulrsat\_s}}
+.. |isplit| mathdef:: \xref{exec/numerics}{op-isplit}{\F{isplit}}
+.. |iconcat| mathdef:: \xref{exec/numerics}{op-iconcat}{\F{iconcat}}
 
 .. |fadd| mathdef:: \xref{exec/numerics}{op-fadd}{\F{fadd}}
 .. |fsub| mathdef:: \xref{exec/numerics}{op-fsub}{\F{fsub}}

document/core/valid/instructions.rst

@@ -1111,6 +1111,26 @@ $${rule-prose: Instr_ok/cvtop}
 $${rule: Instr_ok/cvtop}
 
 
+.. _valid-wideop:
+
+:math:`t_1\K{.}\wideop`
+..........................................
+
+$${rule-prose: Instr_ok/wideop}
+
+$${rule: Instr_ok/wideop}
+
+
+.. _valid-extwideop:
+
+:math:`t_1\K{.}\extwideop`
+..........................................
+
+$${rule-prose: Instr_ok/extwideop}
+
+$${rule: Instr_ok/extwideop}
+
+
 .. index:: vector instruction
    pair: validation; instruction
    single: abstract syntax; instruction

interpreter/binary/decode.ml

@@ -677,6 +677,10 @@ let rec instr s =
     | 0x0fl -> let x = at idx s in table_grow x
     | 0x10l -> let x = at idx s in table_size x
     | 0x11l -> let x = at idx s in table_fill x
+    | 0x13l -> i64_add128
+    | 0x14l -> i64_sub128
+    | 0x15l -> i64_mul_wide_s
+    | 0x16l -> i64_mul_wide_u
 
     | n -> illegal2 s pos b n
     )

interpreter/binary/encode.ml

@@ -902,6 +902,17 @@ struct
     | VecReplace (V128 (F32x4 V128Op.(Replace i))) -> vecop 0x20l; u8 i
     | VecReplace (V128 (F64x2 V128Op.(Replace i))) -> vecop 0x22l; u8 i
 
+    | Wide (I64 I64Op.Add128) -> op 0xfc; u32 0x13l
+    | Wide (I64 I64Op.Sub128) -> op 0xfc; u32 0x14l
+    | Wide (I32 _) -> .
+    | Wide (F32 _) -> .
+    | Wide (F64 _) -> .
+    | Extwide (I64 (I64Op.MulWide S)) -> op 0xfc; u32 0x15l
+    | Extwide (I64 (I64Op.MulWide U)) -> op 0xfc; u32 0x16l
+    | Extwide (I32 _) -> .
+    | Extwide (F32 _) -> .
+    | Extwide (F64 _) -> .
+
   and catch c =
     match c.it with
     | Catch (x1, x2) -> byte 0x00; idx x1; idx x2

interpreter/dune

@@ -3,6 +3,7 @@
 (library
   (public_name wasm)
   (modules :standard \ main wasm wast smallint)
+  (libraries stdint)
 )
 
 (executable

interpreter/dune-project

@@ -16,5 +16,6 @@
   (depends
     (ocaml (>= 4.14))
     (menhir (>= 20220210))
+    (stdint (>= 0.7.2))
   )
 )

interpreter/exec/eval.ml

@@ -1024,6 +1024,14 @@ let rec step (c : config) : config =
         (try Vec (Eval_vec.eval_vreplaceop replaceop v r) :: vs', []
         with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at])
 
+      | Wide op, Num rhs_hi :: Num rhs_lo :: Num lhs_hi :: Num lhs_lo :: vs' ->
+        let (lo, hi) = Eval_num.eval_wideop op lhs_lo lhs_hi rhs_lo rhs_hi
+        in Num hi :: Num lo :: vs', []
+
+      | Extwide op, Num rhs :: Num lhs :: vs' ->
+        let (lo, hi) = Eval_num.eval_extwideop op lhs rhs
+        in Num hi :: Num lo :: vs', []
+
       | _ ->
         let s1 = string_of_values (List.rev vs) in
         let s2 = string_of_resulttype (List.map type_of_value (List.rev vs)) in

interpreter/exec/eval_num.ml

@@ -56,8 +56,35 @@ struct
     in fun v1 v2 -> f (of_num 1 v1) (of_num 2 v2)
 end
 
-module I32Op = IntOp (I32) (I32Num)
-module I64Op = IntOp (I64) (I64Num)
+module I32Op = struct
+  include IntOp (I32) (I32Num)
+
+  let wideop (op: Ast.I32Op.wideop) = match op with _ -> .
+  let extwideop (op: Ast.I32Op.extwideop) = match op with _ -> .
+end
+module I64Op = struct
+  include IntOp (I64) (I64Num)
+
+  open Ast.IntOp
+  open I64Num
+
+  let wideop op =
+    let f = match op with
+      | Ast.I64Op.Add128 -> I64.add128
+      | Ast.I64Op.Sub128 -> I64.sub128
+    in fun v1 v2 v3 v4 ->
+        let (a, b) = f (of_num 1 v1) (of_num 2 v2) (of_num 3 v3) (of_num 4 v4)
+        in (to_num a, to_num b)
+
+  let extwideop op =
+    let f = match op with
+      | Ast.I64Op.MulWide S -> I64.mul_wide_s
+      | Ast.I64Op.MulWide U -> I64.mul_wide_u
+    in fun v1 v2 ->
+        let (a, b) = f (of_num 1 v1) (of_num 2 v2)
+        in (to_num a, to_num b)
+end
+
 
 
 (* Float operators *)
@@ -100,6 +127,9 @@ struct
       | Gt -> FXX.gt
       | Ge -> FXX.ge
     in fun v1 v2 -> f (of_num 1 v1) (of_num 2 v2)
+
+  let wideop (op: Ast.FloatOp.wideop) = match op with _ -> .
+  let extwideop (op: Ast.FloatOp.extwideop) = match op with _ -> .
 end
 
 module F32Op = FloatOp (F32) (F32Num)
@@ -194,3 +224,5 @@ let eval_binop = op I32Op.binop I64Op.binop F32Op.binop F64Op.binop
 let eval_testop = op I32Op.testop I64Op.testop F32Op.testop F64Op.testop
 let eval_relop = op I32Op.relop I64Op.relop F32Op.relop F64Op.relop
 let eval_cvtop = op I32CvtOp.cvtop I64CvtOp.cvtop F32CvtOp.cvtop F64CvtOp.cvtop
+let eval_wideop = op I32Op.wideop I64Op.wideop F32Op.wideop F64Op.wideop
+let eval_extwideop = op I32Op.extwideop I64Op.extwideop F32Op.extwideop F64Op.extwideop

interpreter/exec/eval_num.mli

@@ -5,3 +5,5 @@ val eval_binop : Ast.binop -> num -> num -> num
 val eval_testop : Ast.testop -> num -> bool
 val eval_relop : Ast.relop -> num -> num -> bool
 val eval_cvtop : Ast.cvtop -> num -> num
+val eval_wideop : Ast.wideop -> num -> num -> num -> num -> num * num
+val eval_extwideop : Ast.extwideop -> num -> num -> num * num

interpreter/exec/i64.ml

@@ -8,3 +8,25 @@ include Ixx.Make
     let to_int64 = Fun.id
     let to_hex_string = Printf.sprintf "%Lx"
   end)
+
+open Stdint
+
+let to_i128 lo hi =
+  let lo = Int128.of_uint64 (Uint64.of_int64 lo) in
+  let hi = Int128.of_uint64 (Uint64.of_int64 hi) in
+  Int128.logor lo (Int128.shift_left hi 64)
+
+let split_i128 v =
+  let lo = Int64.of_int128 v in
+  let hi = Int64.of_int128 (Int128.shift_right v 64) in
+  (lo, hi)
+
+let add128 a b c d = split_i128 (Int128.add (to_i128 a b) (to_i128 c d))
+let sub128 a b c d = split_i128 (Int128.sub (to_i128 a b) (to_i128 c d))
+
+let mul_wide_s a b = split_i128 (Int128.mul (Int128.of_int64 a) (Int128.of_int64 b))
+let mul_wide_u a b =
+  let a = Uint64.of_int64 a in
+  let b = Uint64.of_int64 b in
+  let c = Uint128.mul (Uint128.of_uint64 a) (Uint128.of_uint64 b) in
+  split_i128 (Int128.of_uint128 c)

interpreter/syntax/ast.ml

@@ -52,10 +52,20 @@ struct
   type cvtop = ConvertI32 of sx | ConvertI64 of sx
              | PromoteF32 | DemoteF64
              | ReinterpretInt
+  type wideop = |
+  type extwideop = |
 end
 
-module I32Op = IntOp
-module I64Op = IntOp
+module I32Op = struct
+  include IntOp
+  type wideop = |
+  type extwideop = |
+end
+module I64Op = struct
+  include IntOp
+  type wideop = Add128 | Sub128
+  type extwideop = MulWide of sx
+end
 module F32Op = FloatOp
 module F64Op = FloatOp
 
@@ -114,6 +124,8 @@ type unop = (I32Op.unop, I64Op.unop, F32Op.unop, F64Op.unop) Value.op
 type binop = (I32Op.binop, I64Op.binop, F32Op.binop, F64Op.binop) Value.op
 type relop = (I32Op.relop, I64Op.relop, F32Op.relop, F64Op.relop) Value.op
 type cvtop = (I32Op.cvtop, I64Op.cvtop, F32Op.cvtop, F64Op.cvtop) Value.op
+type wideop = (I32Op.wideop, I64Op.wideop, F32Op.wideop, F64Op.wideop) Value.op
+type extwideop = (I32Op.extwideop, I64Op.extwideop, F32Op.extwideop, F64Op.extwideop) Value.op
 
 type vtestop = (V128Op.testop) Value.vecop
 type vrelop = (V128Op.relop) Value.vecop
@@ -245,6 +257,8 @@ and instr' =
   | Compare of relop                     (* numeric comparison *)
   | Unary of unop                        (* unary numeric operator *)
   | Binary of binop                      (* binary numeric operator *)
+  | Wide of wideop                       (* binop producing wide result *)
+  | Extwide of extwideop                 (* binop producing wide result, extending args *)
   | Convert of cvtop                     (* conversion *)
   | VecConst of vec                      (* constant *)
   | VecTest of vtestop                   (* vector test *)

interpreter/syntax/free.ml

@@ -182,6 +182,7 @@ let rec instr (e : instr) =
   | ArrayInitElem (x, y) -> types (idx x) ++ elems (idx y)
   | ExternConvert _ -> empty
   | Const _ | Test _ | Compare _ | Unary _ | Binary _ | Convert _ -> empty
+  | Wide _ | Extwide _ -> empty
   | VecConst _ | VecTest _
   | VecUnary _ | VecBinary _ | VecTernary _ | VecCompare _
   | VecConvert _ | VecShift _ | VecBitmask _

interpreter/syntax/mnemonics.ml

@@ -585,3 +585,8 @@ let f64x2_relaxed_min = VecBinary (V128 (F64x2 V128Op.RelaxedMin))
 let f64x2_relaxed_max = VecBinary (V128 (F64x2 V128Op.RelaxedMax))
 let i16x8_relaxed_dot_i8x16_i7x16_s = VecBinary (V128 (I16x8 V128Op.RelaxedDot))
 let i32x4_relaxed_dot_i8x16_i7x16_add_s = VecTernary (V128 (I32x4 V128Op.RelaxedDotAddS))
+
+let i64_add128 = Wide (I64 I64Op.Add128)
+let i64_sub128 = Wide (I64 I64Op.Sub128)
+let i64_mul_wide_s = Extwide (I64 (I64Op.MulWide S))
+let i64_mul_wide_u = Extwide (I64 (I64Op.MulWide U))