diff --git a/shell.nix b/shell.nix index b8455eb85..7459dd872 100644 --- a/shell.nix +++ b/shell.nix @@ -4,6 +4,10 @@ }: let + bootstrapGhcWasm = pkgs.fetchurl { + url = "https://gitlab.haskell.org/haskell-wasm/ghc-wasm-meta/-/raw/master/bootstrap.sh"; + sha256 = "sha256-ma3MaYD8TWhTGb/Sohivp08GJMYR/2Nqt5ymuX7cvJc="; + }; ocamlPackages = pkgs.ocamlPackages.overrideScope (self: super: { ocaml = (super.ocaml.overrideAttrs { doCheck = false; @@ -29,7 +33,7 @@ let smtml = super.smtml.overrideAttrs (old: { src = fetchGit { url = "https://github.com/formalsec/smtml"; - rev = "d1f09d5aeb4c6cbde5f2604c3e25915fbb28817d"; + rev = "65c7da28d2aa7c2a94cc1ffdc727382cdf38c136"; }; }); }); @@ -61,10 +65,13 @@ pkgs.mkShell { ocb odoc sedlex - # unwrapped because wrapped tries to enforce a target and the build script wants to do its own thing - pkgs.llvmPackages.clang-unwrapped + pkgs.curl + pkgs.git + pkgs.jq # lld + llc isn't included in unwrapped, so we pull it in here pkgs.llvmPackages.bintools-unwrapped + # unwrapped because wrapped tries to enforce a target and the build script wants to do its own thing + pkgs.llvmPackages.clang-unwrapped tinygo pkgs.rustc pkgs.zig @@ -104,5 +111,12 @@ pkgs.mkShell { pkgs.rustc pkgs.zig ]} + + if [ ! -f "$HOME/.ghc-wasm/env" ]; then + echo "Running ghc-wasm bootstrap..." + bash "${bootstrapGhcWasm}" + fi + + source "$HOME/.ghc-wasm/env" ''; } diff --git a/src/compile/binary_to_text.ml b/src/compile/binary_to_text.ml index 174098ffa..82f021017 100644 --- a/src/compile/binary_to_text.ml +++ b/src/compile/binary_to_text.ml @@ -234,7 +234,26 @@ let convert_f64_instr : Binary.f64_instr -> Text.f64_instr = function let convert_v128_instr : Binary.v128_instr -> Text.v128_instr = function | Const n -> Const n + | Not -> Not | And -> And + | Or -> Or + | Any_true -> Any_true + | Load16x4_s (indice, memarg) -> + let indice = convert_indice indice in + let memarg = convert_memarg memarg in + Load16x4_s (indice, memarg) + | Load16x4_u (indice, memarg) -> + let indice = convert_indice indice in + let memarg = convert_memarg memarg in + Load16x4_u (indice, memarg) + | Load32_lane (indice, memarg, n) -> + let indice = convert_indice indice in + let memarg = convert_memarg memarg in + Load32_lane (indice, memarg, n) + | Load64_zero (indice, memarg) -> + let indice = convert_indice indice in + let memarg = convert_memarg memarg in + Load64_zero (indice, memarg) | Load (indice, memarg) -> let indice = convert_indice indice in let memarg = convert_memarg memarg in diff --git a/src/compile/rewrite.ml b/src/compile/rewrite.ml index 54c8b232d..5dd370807 100644 --- a/src/compile/rewrite.ml +++ b/src/compile/rewrite.ml @@ -276,7 +276,26 @@ let rewrite_f64_instr assigned : Text.f64_instr -> Binary.f64_instr Result.t = let rewrite_v128_instr assigned : Text.v128_instr -> Binary.v128_instr Result.t = function | Const f -> Ok (Const f : Binary.v128_instr) + | Not -> Ok Not | And -> Ok And + | Or -> Ok Or + | Any_true -> Ok Any_true + | Load16x4_s (indice, memarg) -> + let* memarg = rewrite_memarg memarg in + let+ indice = Assigned.find_memory assigned indice in + (Load16x4_s (indice, memarg) : Binary.v128_instr) + | Load16x4_u (indice, memarg) -> + let* memarg = rewrite_memarg memarg in + let+ indice = Assigned.find_memory assigned indice in + (Load16x4_u (indice, memarg) : Binary.v128_instr) + | Load32_lane (indice, memarg, n) -> + let* memarg = rewrite_memarg memarg in + let+ indice = Assigned.find_memory assigned indice in + (Load32_lane (indice, memarg, n) : Binary.v128_instr) + | Load64_zero (indice, memarg) -> + let* memarg = rewrite_memarg memarg in + let+ indice = Assigned.find_memory assigned indice in + (Load64_zero (indice, memarg) : Binary.v128_instr) | Load (indice, memarg) -> let* memarg = rewrite_memarg memarg in let+ indice = Assigned.find_memory assigned indice in diff --git a/src/concrete/concrete_i32.ml b/src/concrete/concrete_i32.ml index 93aa7e161..8107e5623 100644 --- a/src/concrete/concrete_i32.ml +++ b/src/concrete/concrete_i32.ml @@ -96,3 +96,11 @@ let pp = Fmt.int32 let of_int32 (v : int32) : t = v let to_int32 (v : t) : int32 = v + +let min_int = Int32.min_int + +let eqz (v : t) = eq v zero + +let ( = ) = eq + +let ( + ) = add diff --git a/src/concrete/concrete_i64.ml b/src/concrete/concrete_i64.ml index 2e274dcde..07509d56d 100644 --- a/src/concrete/concrete_i64.ml +++ b/src/concrete/concrete_i64.ml @@ -97,3 +97,15 @@ let pp = Fmt.int64 let of_int64 (v : int64) : t = v let to_int64 (v : t) : int64 = v + +let min_int = Int64.min_int + +let eqz (v : t) = eq v zero + +let ( = ) = eq + +let ( + ) = add + +let ( * ) = mul + +let ( / ) = div diff --git a/src/concrete/concrete_memory.ml b/src/concrete/concrete_memory.ml index 20ff985f3..1a41bf132 100644 --- a/src/concrete/concrete_memory.ml +++ b/src/concrete/concrete_memory.ml @@ -84,6 +84,13 @@ let store_64 mem ~addr n = let addr = Int32.to_int addr in Ok (Bytes.set_int64_le mem.data addr n) +let store_128 mem ~addr n = + let addr = Int32.to_int addr in + let left, right = Concrete_v128.to_i64x2 n in + Bytes.set_int64_le mem.data addr left; + Bytes.set_int64_le mem.data (addr + 8) right; + Ok () + let load_8_s mem addr = let addr = Int32.to_int addr in Ok (Int32.of_int @@ Bytes.get_int8 mem.data addr) @@ -108,6 +115,13 @@ let load_64 mem addr = let addr = Int32.to_int addr in Ok (Bytes.get_int64_le mem.data addr) +let load_128 mem addr = + let addr = Int32.to_int addr in + let left = Bytes.get_int64_le mem.data addr in + let right = Bytes.get_int64_le mem.data (addr + 8) in + let v = Concrete_v128.of_i64x2 left right in + Ok v + let size_in_pages mem = Int32.of_int @@ (Bytes.length mem.data / page_size) let size mem = Int32.of_int @@ Bytes.length mem.data diff --git a/src/concrete/concrete_memory.mli b/src/concrete/concrete_memory.mli index d169102d2..dd4ac5e99 100644 --- a/src/concrete/concrete_memory.mli +++ b/src/concrete/concrete_memory.mli @@ -9,6 +9,7 @@ include with type t := t and type i32 := Concrete_i32.t and type i64 := Concrete_i64.t + and type v128 := Concrete_v128.t and type 'a choice := 'a Concrete_choice.t val get_limits : t -> Binary.Mem.Type.limits diff --git a/src/concrete/concrete_v128.ml b/src/concrete/concrete_v128.ml index 163b02471..4dcb21b84 100644 --- a/src/concrete/concrete_v128.ml +++ b/src/concrete/concrete_v128.ml @@ -68,6 +68,10 @@ let to_i32x4 = function | I32x4 (a, b, c, d) -> (a, b, c, d) | v -> i64x2_to_i32x4 (to_i64x2 v) +let to_i8x16 _ = raise @@ Failure "TODO" + +let to_i16x8 _ = raise @@ Failure "TODO" + let zero = of_i64x2 0L 0L let eq a b = diff --git a/src/concrete/concrete_value.ml b/src/concrete/concrete_value.ml index 1fbd2a169..e8d149b70 100644 --- a/src/concrete/concrete_value.ml +++ b/src/concrete/concrete_value.ml @@ -4,6 +4,10 @@ type boolean = Concrete_boolean.t +type i8 = int + +type i16 = int + type i32 = Concrete_i32.t type i64 = Concrete_i64.t @@ -17,12 +21,12 @@ type v128 = Concrete_v128.t type reference = Concrete_ref.t module Boolean = Concrete_boolean -module Ref = Concrete_ref module I32 = Concrete_i32 module I64 = Concrete_i64 module F32 = Concrete_f32 module F64 = Concrete_f64 module V128 = Concrete_v128 +module Ref = Concrete_ref type t = | I32 of i32 diff --git a/src/interpret/interpret.ml b/src/interpret/interpret.ml index ed07a40e0..b087bb66c 100644 --- a/src/interpret/interpret.ml +++ b/src/interpret/interpret.ml @@ -43,6 +43,7 @@ module Make Memory_intf.T with type i32 := Value.i32 and type i64 := Value.i64 + and type v128 := Value.v128 and type 'a choice := 'a Choice.t) (Extern_func : Extern.Func.T @@ -68,36 +69,6 @@ struct open Choice module Stack = Stack.Make [@inlined hint] (Value) - module I32 = struct - include I32 - - (* TODO: move all of this to I32_intf *) - let ( + ) = add - - let ( = ) = eq - - let eqz v = v = zero - - let min_int = I32.of_int32 Int32.min_int - end - - module I64 = struct - include I64 - - (* TODO: move all of this to I64_intf *) - let ( + ) = add - - let ( * ) = mul - - let ( / ) = div - - let ( = ) = eq - - let eqz v = v = zero - - let min_int = I64.of_int64 Int64.min_int - end - let page_size = I64.of_int64 65_536L let pop_choice stack ~instr_counter_true ~instr_counter_false = @@ -254,6 +225,8 @@ struct let mk_addr_check_bounds_8L = mk_addr_check_bounds 8L + let mk_addr_check_bounds_16L = mk_addr_check_bounds 16L + let exec_i32_instr env instr_counter stack : Binary.i32_instr -> Stack.t Choice.t = function | Const n -> Stack.push_concrete_i32 stack n |> Choice.return @@ -736,20 +709,96 @@ struct let+ () = Memory.store_64 mem ~addr (F64.to_bits n) in stack - let exec_v128_instr stack (i : Binary.v128_instr) = + let exec_v128_instr env instr_counter stack (i : Binary.v128_instr) : + Stack.t Choice.t = match i with - | Const n -> Stack.push_concrete_v128 stack n - | And | Load _ | Store _ -> raise @@ Failure "todo" + | Const n -> + let stack = Stack.push_concrete_v128 stack n in + Choice.return stack + | Not -> raise @@ Failure "TODO (Not)" + | And -> raise @@ Failure "TODO (And)" + | Or -> raise @@ Failure "TODO (Or)" + | Load32_lane _ -> raise @@ Failure "TODO (Load32_lane)" + | Load64_zero _ -> raise @@ Failure "TODO (Load64_zero)" + | Load (memory_indice, { offset; _ }) -> + let pos, stack = Stack.pop_i32 stack in + let* addr = + mk_addr_check_bounds_16L env memory_indice ~pos ~offset instr_counter + in + let* mem = Env.get_memory env memory_indice in + let+ res = Memory.load_128 mem addr in + Stack.push_v128 stack res + | Store (memory_indice, { offset; _ }) -> + let n, stack = Stack.pop_v128 stack in + let pos, stack = Stack.pop_i32 stack in + let* addr = + mk_addr_check_bounds_16L env memory_indice ~pos ~offset instr_counter + in + let* mem = Env.get_memory env memory_indice in + let+ () = Memory.store_128 mem ~addr n in + stack + | Load16x4_s _ -> raise @@ Failure "TODO (Load16x4_s)" + | Load16x4_u _ -> raise @@ Failure "TODO (Load16x4_u)" + | Any_true -> raise @@ Failure "TODO (Any_true)" let exec_i8x16_instr _stack : Text.i8x16_instr -> _ = function - | _ -> - (* TODO *) - raise @@ Failure "todo" + | Add -> raise @@ Failure "TODO (i8x16.add)" + | Sub -> raise @@ Failure "TODO (i8x16.sub)" + | Eq -> + (* + let (n1, n2), stack = Stack.pop2_v128 stack in + let a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1 = + V128.to_i8x16 n1 + in + let a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2 = + V128.to_i8x16 n2 + in + let a = I8.eq a1 a2 in + let b = I8.eq b1 b2 in + let c = I8.eq c1 c2 in + let d = I8.eq d1 d2 in + let e = I8.eq e1 e2 in + let f = I8.eq f1 f2 in + let g = I8.eq g1 g2 in + let h = I8.eq h1 h2 in + let i = I8.eq i1 i2 in + let j = I8.eq j1 j2 in + let k = I8.eq k1 k2 in + let l = I8.eq l1 l2 in + let m = I8.eq m1 m2 in + let n = I8.eq n1 n2 in + let o = I8.eq o1 o2 in + let p = I8.eq p1 p2 in + Stack.push_v128 stack (V128.of_i8x16 a b c d e f g h i j k l m n o p) +*) + raise @@ Failure "TODO (i8x16.eq)" + | Ne -> raise @@ Failure "TODO (i8x16.ne)" + | Abs -> raise @@ Failure "TODO (i8x16.abs)" + | Neg -> raise @@ Failure "TODO (i8x16.neg)" + | Popcnt -> raise @@ Failure "TODO (i8x16.popcnt)" + | All_true -> raise @@ Failure "TODO (i8x16.all_true)" + | Bitmask -> raise @@ Failure "TODO (i8x16.bitmask)" + | Swizzle -> raise @@ Failure "TODO (i8x16.swizzle)" + | Splat -> raise @@ Failure "TODO (i8x16.splat)" + | Lt _ -> raise @@ Failure "TODO (i8x16.lt)" + | Gt _ -> raise @@ Failure "TODO (i8x16.gt)" + | Le _ -> raise @@ Failure "TODO (i8x16.le)" + | Ge _ -> raise @@ Failure "TODO (i8x16.ge)" + | Shuffle _ -> raise @@ Failure "TODO (i8x16.shuffle)" let exec_i16x8_instr _stack : Text.i16x8_instr -> _ = function - | _ -> - (* TODO *) - raise @@ Failure "todo" + | Add -> raise @@ Failure "TODO (i16x8.add)" + | Sub -> raise @@ Failure "TODO (i16x8.sub)" + | Mul -> raise @@ Failure "TODO (i16x8.mul)" + | Eq -> raise @@ Failure "TODO (i16x8.eq)" + | Ne -> raise @@ Failure "TODO (i16x8.ne)" + | Splat -> raise @@ Failure "TODO (i16x8.splat)" + | Lt _ -> raise @@ Failure "TODO (i16x8.lt)" + | Gt _ -> raise @@ Failure "TODO (i16x8.gt)" + | Le _ -> raise @@ Failure "TODO (i16x8.le)" + | Ge _ -> raise @@ Failure "TODO (i16x8.ge)" + | Extract_lane_s _ -> raise @@ Failure "TODO (i16x8.extract_lane_s)" + | Extract_lane_u _ -> raise @@ Failure "TODO (i16x8.extract_lane_u)" let exec_i32x4_instr stack : Text.i32x4_instr -> _ = function | Add -> @@ -770,7 +819,22 @@ struct let c = I32.sub c1 c2 in let d = I32.sub d1 d2 in Stack.push_v128 stack (V128.of_i32x4 a b c d) - | Mul -> raise @@ Failure "todo" + | Mul -> raise @@ Failure "TODO (i32x4.Mul)" + | Shl -> raise @@ Failure "TODO (i32x4.Shl)" + | Shr _ -> raise @@ Failure "TODO (i32x4.Shr)" + | Eq -> raise @@ Failure "TODO (i32x4.Eq)" + | Ne -> raise @@ Failure "TODO (i32x4.Ne)" + | Lt _ -> raise @@ Failure "TODO (i32x4.Lt)" + | Gt _ -> raise @@ Failure "TODO (i32x4.Gt)" + | Le _ -> raise @@ Failure "TODO (i32x4.Le)" + | Ge _ -> raise @@ Failure "TODO (i32x4.Ge)" + | Splat -> raise @@ Failure "TODO (i32x4.Splat)" + | Extract_lane _ -> raise @@ Failure "TODO (i32x4.Extract_lane)" + | Replace_lane _ -> raise @@ Failure "TODO (i32x4.Replace_lane)" + | Extend_low_i16x8_s -> raise @@ Failure "TODO (i32x4.Extend_low_i16x8_s)" + | Extend_high_i16x8_s -> raise @@ Failure "TODO (i32x4.Extend_high_i16x8_s)" + | Extend_low_i16x8_u -> raise @@ Failure "TODO (i32x4.Extend_low_i16x8_u)" + | Extend_high_i16x8_u -> raise @@ Failure "TODO (i32x4.Extend_high_i16x8_u)" let exec_i64x2_instr stack : Text.i64x2_instr -> _ = function | Add -> @@ -787,7 +851,15 @@ struct let a = I64.sub a1 a2 in let b = I64.sub b1 b2 in Stack.push_v128 stack (V128.of_i64x2 a b) - | Mul -> raise @@ Failure "todo" + | Mul -> raise @@ Failure "TODO (i64x2.Mul)" + | Extend_low_i32x4 _ -> raise @@ Failure "TODO (i64x2.Extend_low_i32x4)" + | Splat -> raise @@ Failure "TODO (i64x2.Splat)" + | Eq -> raise @@ Failure "TODO (i64x2.Eq)" + | Ne -> raise @@ Failure "TODO (i64x2.Ne)" + | Lt_s -> raise @@ Failure "TODO (i64x2.Lt_s)" + | Gt_s -> raise @@ Failure "TODO (i64x2.Gt_s)" + | Le_s -> raise @@ Failure "TODO (i64x2.Le_s)" + | Ge_s -> raise @@ Failure "TODO (i64x2.Ge_s)" let exec_ref_instr env stack (i : Binary.ref_instr) = match i with @@ -1382,7 +1454,9 @@ struct | F64 i -> let* stack = exec_f64_instr env instr_counter stack i in ret stack - | V128 i -> ret @@ exec_v128_instr stack i + | V128 i -> + let* stack = exec_v128_instr env instr_counter stack i in + ret stack | I8x16 i -> exec_i8x16_instr stack i | I16x8 i -> exec_i16x8_instr stack i | I32x4 i -> ret @@ exec_i32x4_instr stack i diff --git a/src/intf/i32_intf.ml b/src/intf/i32_intf.ml index 05b1db9fe..58a85818e 100644 --- a/src/intf/i32_intf.ml +++ b/src/intf/i32_intf.ml @@ -34,4 +34,12 @@ module type T = sig val of_int : int -> t val pp : t Fmt.t + + val min_int : t + + val eqz : t -> boolean + + val ( = ) : t -> t -> boolean + + val ( + ) : t -> t -> t end diff --git a/src/intf/i64_intf.ml b/src/intf/i64_intf.ml index 27308694c..3507d7f0d 100644 --- a/src/intf/i64_intf.ml +++ b/src/intf/i64_intf.ml @@ -36,4 +36,16 @@ module type T = sig val of_int : int -> t val pp : t Fmt.t + + val min_int : t + + val eqz : t -> boolean + + val ( = ) : t -> t -> boolean + + val ( + ) : t -> t -> t + + val ( * ) : t -> t -> t + + val ( / ) : t -> t -> t end diff --git a/src/intf/memory_intf.ml b/src/intf/memory_intf.ml index df8e9b802..454192ce7 100644 --- a/src/intf/memory_intf.ml +++ b/src/intf/memory_intf.ml @@ -9,6 +9,8 @@ module type T = sig type i64 + type v128 + type 'a choice val load_8_s : t -> i32 -> i32 choice @@ -23,6 +25,8 @@ module type T = sig val load_64 : t -> i32 -> i64 choice + val load_128 : t -> i32 -> v128 choice + val store_8 : t -> addr:i32 -> i32 -> unit choice val store_16 : t -> addr:i32 -> i32 -> unit choice @@ -31,6 +35,8 @@ module type T = sig val store_64 : t -> addr:i32 -> i64 -> unit choice + val store_128 : t -> addr:i32 -> v128 -> unit choice + val grow : t -> i32 -> unit choice val fill : t -> pos:i32 -> len:i32 -> char -> unit choice diff --git a/src/intf/v128_intf.ml b/src/intf/v128_intf.ml index 4e24a41a3..52d925299 100644 --- a/src/intf/v128_intf.ml +++ b/src/intf/v128_intf.ml @@ -5,12 +5,58 @@ module type T = sig type t + type i8 + + type i16 + type i32 type i64 val zero : t + val of_i8x16 : + i8 + -> i8 + -> i8 + -> i8 + -> i8 + -> i8 + -> i8 + -> i8 + -> i8 + -> i8 + -> i8 + -> i8 + -> i8 + -> i8 + -> i8 + -> i8 + -> t + + val to_i8x16 : + t + -> i8 + * i8 + * i8 + * i8 + * i8 + * i8 + * i8 + * i8 + * i8 + * i8 + * i8 + * i8 + * i8 + * i8 + * i8 + * i8 + + val of_i16x8 : i16 -> i16 -> i16 -> i16 -> i16 -> i16 -> i16 -> i16 -> t + + val to_i16x8 : t -> i16 * i16 * i16 * i16 * i16 * i16 * i16 * i16 + val of_i32x4 : i32 -> i32 -> i32 -> i32 -> t val to_i32x4 : t -> i32 * i32 * i32 * i32 diff --git a/src/intf/value_intf.ml b/src/intf/value_intf.ml index 092e44ae8..20f15a6a0 100644 --- a/src/intf/value_intf.ml +++ b/src/intf/value_intf.ml @@ -3,6 +3,10 @@ (* Written by the Owi programmers *) module type T = sig + type i8 + + type i16 + type i32 type i64 @@ -50,7 +54,12 @@ module type T = sig and type i64 := i64 module V128 : - V128_intf.T with type t := v128 and type i32 := i32 and type i64 := i64 + V128_intf.T + with type t := v128 + and type i8 := i8 + and type i16 := i16 + and type i32 := i32 + and type i64 := i64 module Ref : Ref_intf.T diff --git a/src/ir/binary.ml b/src/ir/binary.ml index eb74c6d52..65eef7821 100644 --- a/src/ir/binary.ml +++ b/src/ir/binary.ml @@ -539,13 +539,31 @@ let pp_f64_instr ppf = function (** V128 instructions *) type v128_instr = | Const of Concrete_v128.t + | Not | And + | Or + | Any_true + | Load16x4_s of (indice * memarg) + | Load16x4_u of (indice * memarg) + | Load32_lane of (indice * memarg * int) + | Load64_zero of (indice * memarg) | Load of (indice * memarg) | Store of (indice * memarg) let pp_v128_instr ppf = function | Const n -> pf ppf "v128.const %a" Concrete_v128.pp n + | Not -> pf ppf "v128.not" | And -> pf ppf "v128.and" + | Or -> pf ppf "v128.or" + | Any_true -> pf ppf "v128.any_true" + | Load16x4_s (indice, memarg) -> + pf ppf "v128.load16x4_s%a%a" pp_indice_not0 indice pp_memarg memarg + | Load16x4_u (indice, memarg) -> + pf ppf "v128.load16x4_u%a%a" pp_indice_not0 indice pp_memarg memarg + | Load32_lane (indice, memarg, n) -> + pf ppf "v128.load32_lane%a%a %d" pp_indice_not0 indice pp_memarg memarg n + | Load64_zero (indice, memarg) -> + pf ppf "v128.load64_zero%a%a" pp_indice_not0 indice pp_memarg memarg | Load (indice, memarg) -> pf ppf "v128.load%a%a" pp_indice_not0 indice pp_memarg memarg | Store (indice, memarg) -> diff --git a/src/ir/binary.mli b/src/ir/binary.mli index a6f1f92f9..f91983f98 100644 --- a/src/ir/binary.mli +++ b/src/ir/binary.mli @@ -234,7 +234,14 @@ type f64_instr = (** V128 instructions *) type v128_instr = | Const of Concrete_v128.t + | Not | And + | Or + | Any_true + | Load16x4_s of (indice * memarg) + | Load16x4_u of (indice * memarg) + | Load32_lane of (indice * memarg * int) + | Load64_zero of (indice * memarg) | Load of (indice * memarg) | Store of (indice * memarg) diff --git a/src/ir/binary_encoder.ml b/src/ir/binary_encoder.ml index 06ad877b7..b308cd8c6 100644 --- a/src/ir/binary_encoder.ml +++ b/src/ir/binary_encoder.ml @@ -490,26 +490,91 @@ let write_v128_instr buf (i : Binary.v128_instr) = let a, b = Concrete_v128.to_i64x2 v in write_bytes_8 buf a; write_bytes_8 buf b - | And | Load _ | Store _ -> raise @@ Failure "TODO" + | Not -> write_fd buf 0x4D + | And -> write_fd buf 0x4E + | Or -> write_fd buf 0x50 + | Any_true -> write_fd buf 0x53 + | Load32_lane _ | Load64_zero _ | Load _ | Store _ | Load16x4_s _ + | Load16x4_u _ -> + raise @@ Failure "TODO" let write_i8x16_instr buf : Text.i8x16_instr -> _ = function - | Add -> write_fd buf 110 - | Sub -> write_fd buf 113 + | Add -> write_fd buf 0x6E + | Sub -> write_fd buf 0x71 + | Eq -> write_fd buf 0x23 + | Ne -> write_fd buf 0x24 + | Lt S -> write_fd buf 0x25 + | Lt U -> write_fd buf 0x26 + | Gt S -> write_fd buf 0x27 + | Gt U -> write_fd buf 0x28 + | Le S -> write_fd buf 0x29 + | Le U -> write_fd buf 0x2A + | Ge S -> write_fd buf 0x2B + | Ge U -> write_fd buf 0x2C + | Abs -> write_fd buf 0x60 + | Neg -> write_fd buf 0x61 + | Popcnt -> write_fd buf 0x62 + | All_true -> write_fd buf 0x63 + | Bitmask -> write_fd buf 0x64 + | Shuffle _ -> raise @@ Failure "TODO" + | Swizzle -> write_fd buf 0x0E + | Splat -> write_fd buf 0x0F let write_i16x8_instr buf : Text.i16x8_instr -> _ = function - | Add -> write_fd buf 142 - | Sub -> write_fd buf 145 - | Mul -> raise @@ Failure "TODO" + | Eq -> write_fd buf 0x2D + | Ne -> write_fd buf 0x2E + | Lt S -> write_fd buf 0x2F + | Lt U -> write_fd buf 0x30 + | Gt S -> write_fd buf 0x31 + | Gt U -> write_fd buf 0x32 + | Le S -> write_fd buf 0x33 + | Le U -> write_fd buf 0x34 + | Ge S -> write_fd buf 0x35 + | Ge U -> write_fd buf 0x36 + | Add -> write_fd buf 0x8E + | Sub -> write_fd buf 0x91 + | Mul -> write_fd buf 0x95 + | Splat -> write_fd buf 0x10 + | Extract_lane_s _n -> raise @@ Failure "TODO" + | Extract_lane_u _n -> raise @@ Failure "TODO" let write_i32x4_instr buf : Text.i32x4_instr -> _ = function | Add -> write_fd buf 174 | Sub -> write_fd buf 177 - | Mul -> raise @@ Failure "TODO" + | Mul -> write_fd buf 0xB5 + | Shl -> write_fd buf 0xAB + | Shr S -> write_fd buf 0xAC + | Shr U -> write_fd buf 0xAD + | Eq -> write_fd buf 0x37 + | Ne -> write_fd buf 0x38 + | Lt S -> write_fd buf 0x39 + | Lt U -> write_fd buf 0x3A + | Gt S -> write_fd buf 0x3B + | Gt U -> write_fd buf 0x3C + | Le S -> write_fd buf 0x3D + | Le U -> write_fd buf 0x3E + | Ge S -> write_fd buf 0x3F + | Ge U -> write_fd buf 0x40 + | Splat -> write_fd buf 0x11 + | Extract_lane _n -> raise @@ Failure "TODO" + | Replace_lane _n -> raise @@ Failure "TODO" + | Extend_low_i16x8_s -> write_fd buf 0xA7 + | Extend_high_i16x8_s -> write_fd buf 0xA8 + | Extend_low_i16x8_u -> write_fd buf 0xA9 + | Extend_high_i16x8_u -> write_fd buf 0xAA let write_i64x2_instr buf : Text.i64x2_instr -> _ = function - | Add -> write_fd buf 206 - | Sub -> write_fd buf 209 - | Mul -> raise @@ Failure "TODO" + | Add -> write_fd buf 0xCE + | Sub -> write_fd buf 0xD1 + | Mul -> write_fd buf 0xD5 + | Eq -> write_fd buf 0xD6 + | Ne -> write_fd buf 0xD7 + | Lt_s -> write_fd buf 0xD8 + | Gt_s -> write_fd buf 0xD9 + | Le_s -> write_fd buf 0xDA + | Ge_s -> write_fd buf 0xDB + | Splat -> write_fd buf 0x12 + | Extend_low_i32x4 _ -> raise @@ Failure "TODO" let write_ref_instr buf : Binary.ref_instr -> _ = let add_char c = Buffer.add_char buf c in diff --git a/src/ir/text.ml b/src/ir/text.ml index 531b79ba7..57c783aed 100644 --- a/src/ir/text.ml +++ b/src/ir/text.ml @@ -692,13 +692,31 @@ let pp_f64_instr ppf = function (** V128 instructions *) type v128_instr = | Const of Concrete_v128.t + | Not | And + | Or + | Any_true + | Load16x4_s of (indice * memarg) + | Load16x4_u of (indice * memarg) + | Load32_lane of (indice * memarg * int) + | Load64_zero of (indice * memarg) | Load of (indice * memarg) | Store of (indice * memarg) let pp_v128_instr ppf = function | Const n -> pf ppf "v128.const %a" Concrete_v128.pp n + | Not -> pf ppf "v128.not" | And -> pf ppf "v128.and" + | Or -> pf ppf "v128.or" + | Any_true -> pf ppf "v128.any_true" + | Load16x4_s (indice, memarg) -> + pf ppf "v128.load16x4_s%a%a" pp_indice_not0 indice pp_memarg memarg + | Load16x4_u (indice, memarg) -> + pf ppf "v128.load16x4_u%a%a" pp_indice_not0 indice pp_memarg memarg + | Load32_lane (indice, memarg, n) -> + pf ppf "v128.load32_lane%a%a %d" pp_indice_not0 indice pp_memarg memarg n + | Load64_zero (indice, memarg) -> + pf ppf "v128.load64_zero%a%a" pp_indice_not0 indice pp_memarg memarg | Load (indice, memarg) -> pf ppf "v128.load%a%a" pp_indice_not0 indice pp_memarg memarg | Store (indice, memarg) -> @@ -708,43 +726,152 @@ let pp_v128_instr ppf = function type i8x16_instr = | Add | Sub + | Eq + | Ne + | Lt of sx + | Gt of sx + | Le of sx + | Ge of sx + | Abs + | Neg + | Popcnt + | All_true + | Bitmask + | Shuffle of int array (* TODO: make this immutable at some point *) + | Swizzle + | Splat let pp_i8x16_instr ppf = function | Add -> pf ppf "i8x16.add" | Sub -> pf ppf "i8x16.sub" + | Eq -> pf ppf "i8x16.eq" + | Ne -> pf ppf "i8x16.ne" + | Lt S -> pf ppf "i8x16.lt_s" + | Lt U -> pf ppf "i8x16.lt_u" + | Gt S -> pf ppf "i8x16.gt_s" + | Gt U -> pf ppf "i8x16.gt_u" + | Le S -> pf ppf "i8x16.le_s" + | Le U -> pf ppf "i8x16.le_u" + | Ge S -> pf ppf "i8x16.ge_s" + | Ge U -> pf ppf "i8x16.ge_u" + | Abs -> pf ppf "i8x16.abs" + | Neg -> pf ppf "i8x16.neg" + | Popcnt -> pf ppf "i8x16.popcnt" + | All_true -> pf ppf "i8x16.all_true" + | Bitmask -> pf ppf "i8x16.bitmask" + | Shuffle is -> + pf ppf "i8x16.suffle %a" + (Fmt.array ~sep:(fun ppf () -> Fmt.pf ppf " ") Fmt.int) + is + | Swizzle -> pf ppf "i8x16.swizzle" + | Splat -> pf ppf "i8x16.splat" (** I16x8 instructions *) type i16x8_instr = | Add | Sub | Mul + | Eq + | Ne + | Lt of sx + | Gt of sx + | Le of sx + | Ge of sx + | Splat + | Extract_lane_s of int + | Extract_lane_u of int let pp_i16x8_instr ppf = function | Add -> pf ppf "i16x8.add" | Sub -> pf ppf "i16x8.sub" | Mul -> pf ppf "i16x8.mul" + | Eq -> pf ppf "i16x8.eq" + | Ne -> pf ppf "i16x8.ne" + | Lt S -> pf ppf "i16x8.lt_s" + | Lt U -> pf ppf "i16x8.lt_u" + | Gt S -> pf ppf "i16x8.gt_s" + | Gt U -> pf ppf "i16x8.gt_u" + | Le S -> pf ppf "i16x8.le_s" + | Le U -> pf ppf "i16x8.le_u" + | Ge S -> pf ppf "i16x8.ge_s" + | Ge U -> pf ppf "i16x8.ge_u" + | Splat -> pf ppf "i16x8.splat" + | Extract_lane_s n -> pf ppf "i16x8.extract_lane_s %d" n + | Extract_lane_u n -> pf ppf "i16x8.extract_lane_u %d" n (* I32x4 instructions *) type i32x4_instr = | Add | Sub | Mul + | Shl + | Shr of sx + | Eq + | Ne + | Lt of sx + | Gt of sx + | Le of sx + | Ge of sx + | Splat + | Extract_lane of int + | Replace_lane of int + | Extend_low_i16x8_s + | Extend_high_i16x8_s + | Extend_low_i16x8_u + | Extend_high_i16x8_u let pp_i32x4_instr ppf = function | Add -> pf ppf "i32x4.add" | Sub -> pf ppf "i32x4.sub" | Mul -> pf ppf "i32x4.mul" + | Shl -> pf ppf "i32x4.shl" + | Shr S -> pf ppf "i32x4.shr_s" + | Shr U -> pf ppf "i32x4.shr_u" + | Eq -> pf ppf "i32x4.eq" + | Ne -> pf ppf "i32x4.ne" + | Lt S -> pf ppf "i32x4.lt_s" + | Lt U -> pf ppf "i32x4.lt_u" + | Gt S -> pf ppf "i32x4.gt_s" + | Gt U -> pf ppf "i32x4.gt_u" + | Le S -> pf ppf "i32x4.le_s" + | Le U -> pf ppf "i32x4.le_u" + | Ge S -> pf ppf "i32x4.ge_s" + | Ge U -> pf ppf "i32x4.ge_u" + | Splat -> pf ppf "i32x4.splat" + | Extract_lane n -> pf ppf "i32x4.extract_lane %d" n + | Replace_lane n -> pf ppf "i32x4.replace_lane %d" n + | Extend_low_i16x8_s -> pf ppf "i32x4.extend_low_i16x8_s" + | Extend_high_i16x8_s -> pf ppf "i32x4.extend_high_i16x8_s" + | Extend_low_i16x8_u -> pf ppf "i32x4.extend_low_i16x8_u" + | Extend_high_i16x8_u -> pf ppf "i32x4.extend_high_i16x8_u" (** I64x2 instructions *) type i64x2_instr = | Add | Sub | Mul + | Eq + | Ne + | Lt_s + | Gt_s + | Le_s + | Ge_s + | Splat + | Extend_low_i32x4 of sx let pp_i64x2_instr ppf = function | Add -> pf ppf "i64x2.add" | Sub -> pf ppf "i64x2.sub" | Mul -> pf ppf "i64x2.mul" + | Eq -> pf ppf "i64x2.eq" + | Ne -> pf ppf "i64x2.ne" + | Lt_s -> pf ppf "i64x2.lt_s" + | Gt_s -> pf ppf "i64x2.gt_s" + | Le_s -> pf ppf "i64x2.le_s" + | Ge_s -> pf ppf "i64x2.ge_s" + | Splat -> pf ppf "i64x2.splat" + | Extend_low_i32x4 S -> pf ppf "i64x2.extend_low_i32x4_s" + | Extend_low_i32x4 U -> pf ppf "i64x2.extend_low_i32x4_u" (** Reference instructions *) type ref_instr = diff --git a/src/ir/text.mli b/src/ir/text.mli index 11636307f..a604d2344 100644 --- a/src/ir/text.mli +++ b/src/ir/text.mli @@ -319,7 +319,14 @@ type f64_instr = (** V128 instructions *) type v128_instr = | Const of Concrete_v128.t + | Not | And + | Or + | Any_true + | Load16x4_s of (indice * memarg) + | Load16x4_u of (indice * memarg) + | Load32_lane of (indice * memarg * int) + | Load64_zero of (indice * memarg) | Load of (indice * memarg) | Store of (indice * memarg) @@ -329,6 +336,20 @@ val pp_v128_instr : v128_instr Fmt.t type i8x16_instr = | Add | Sub + | Eq + | Ne + | Lt of sx + | Gt of sx + | Le of sx + | Ge of sx + | Abs + | Neg + | Popcnt + | All_true + | Bitmask + | Shuffle of int array (* TODO: make this immutable at some point *) + | Swizzle + | Splat val pp_i8x16_instr : i8x16_instr Fmt.t @@ -337,6 +358,15 @@ type i16x8_instr = | Add | Sub | Mul + | Eq + | Ne + | Lt of sx + | Gt of sx + | Le of sx + | Ge of sx + | Splat + | Extract_lane_s of int + | Extract_lane_u of int val pp_i16x8_instr : i16x8_instr Fmt.t @@ -345,6 +375,21 @@ type i32x4_instr = | Add | Sub | Mul + | Shl + | Shr of sx + | Eq + | Ne + | Lt of sx + | Gt of sx + | Le of sx + | Ge of sx + | Splat + | Extract_lane of int + | Replace_lane of int + | Extend_low_i16x8_s + | Extend_high_i16x8_s + | Extend_low_i16x8_u + | Extend_high_i16x8_u val pp_i32x4_instr : i32x4_instr Fmt.t @@ -353,6 +398,14 @@ type i64x2_instr = | Add | Sub | Mul + | Eq + | Ne + | Lt_s + | Gt_s + | Le_s + | Ge_s + | Splat + | Extend_low_i32x4 of sx val pp_i64x2_instr : i64x2_instr Fmt.t diff --git a/src/owi.mli b/src/owi.mli index e0cbc27ef..5e40e8e39 100644 --- a/src/owi.mli +++ b/src/owi.mli @@ -463,7 +463,14 @@ module Text : sig (** V128 instructions *) type v128_instr = | Const of Concrete_v128.t + | Not | And + | Or + | Any_true + | Load16x4_s of (indice * memarg) + | Load16x4_u of (indice * memarg) + | Load32_lane of (indice * memarg * int) + | Load64_zero of (indice * memarg) | Load of (indice * memarg) | Store of (indice * memarg) @@ -471,24 +478,70 @@ module Text : sig type i8x16_instr = | Add | Sub + | Eq + | Ne + | Lt of sx + | Gt of sx + | Le of sx + | Ge of sx + | Abs + | Neg + | Popcnt + | All_true + | Bitmask + | Shuffle of int array (* TODO: make this immutable at some point *) + | Swizzle + | Splat (** I16x8 instructions *) type i16x8_instr = | Add | Sub | Mul + | Eq + | Ne + | Lt of sx + | Gt of sx + | Le of sx + | Ge of sx + | Splat + | Extract_lane_s of int + | Extract_lane_u of int (* I32x4 instructions *) type i32x4_instr = | Add | Sub | Mul + | Shl + | Shr of sx + | Eq + | Ne + | Lt of sx + | Gt of sx + | Le of sx + | Ge of sx + | Splat + | Extract_lane of int + | Replace_lane of int + | Extend_low_i16x8_s + | Extend_high_i16x8_s + | Extend_low_i16x8_u + | Extend_high_i16x8_u (** I64x2 instructions *) type i64x2_instr = | Add | Sub | Mul + | Eq + | Ne + | Lt_s + | Gt_s + | Le_s + | Ge_s + | Splat + | Extend_low_i32x4 of sx (** Reference instructions *) type ref_instr = @@ -986,7 +1039,14 @@ module Binary : sig (** V128 instructions *) type v128_instr = | Const of Concrete_v128.t + | Not | And + | Or + | Any_true + | Load16x4_s of (indice * memarg) + | Load16x4_u of (indice * memarg) + | Load32_lane of (indice * memarg * int) + | Load64_zero of (indice * memarg) | Load of (indice * memarg) | Store of (indice * memarg) diff --git a/src/parser/binary_parser.ml b/src/parser/binary_parser.ml index 381d862f7..cf3e89be1 100644 --- a/src/parser/binary_parser.ml +++ b/src/parser/binary_parser.ml @@ -159,6 +159,10 @@ let read_F32 input = let i32 = Int32.logor i32 i1 in (Float32.of_bits i32, input) +let read_u8 input = + let+ b, input = read_byte ~msg:"read_u8" input in + (int_of_char b, input) + let read_F64 input = let i64_of_byte input = let+ b, input = read_byte ~msg:"read_F64" input in @@ -354,12 +358,12 @@ let read_memarg max_align input = in if is_malformed align then parse_fail "malformed memop flags" else if Int32.to_int align > max_align then + (* TODO: move this to validation phase *) parse_fail "alignment must not be larger than natural" else let+ offset, input = read_U32 input in let offset = Int64.of_int offset in (memidx, { Binary.align; offset }, input) -(* TODO: should the checks be moved to validate? *) let read_castop input = let* b, input = @@ -534,11 +538,17 @@ let read_FD input = let* i, input = read_U32 input in match i with | 0x00 -> - let+ idx, memarg, input = read_memarg 128 input in - (V128 (Load (idx, memarg)), input) + let+ indice, memarg, input = read_memarg 128 input in + (V128 (Load (indice, memarg)), input) + | 0x03 -> + let+ indice, memarg, input = read_memarg 128 input in + (V128 (Load16x4_s (indice, memarg)), input) + | 0x04 -> + let+ indice, memarg, input = read_memarg 128 input in + (V128 (Load16x4_u (indice, memarg)), input) | 0x0b -> - let+ idx, memarg, input = read_memarg 128 input in - (V128 (Store (idx, memarg)), input) + let+ indice, memarg, input = read_memarg 128 input in + (V128 (Store (indice, memarg)), input) | 0x0C -> let* data = Input.sub_prefix 16 input in let+ input = Input.sub_suffix 16 input in @@ -547,18 +557,116 @@ let read_FD input = let low = String.get_int64_le data 8 in let v128 = Concrete_v128.of_i64x2 high low in (V128 (Const v128), input) + | 0x0D -> + let* i0, input = read_u8 input in + let* i1, input = read_u8 input in + let* i2, input = read_u8 input in + let* i3, input = read_u8 input in + let* i4, input = read_u8 input in + let* i5, input = read_u8 input in + let* i6, input = read_u8 input in + let* i7, input = read_u8 input in + let* i8, input = read_u8 input in + let* i9, input = read_u8 input in + let* i10, input = read_u8 input in + let* i11, input = read_u8 input in + let* i12, input = read_u8 input in + let* i13, input = read_u8 input in + let* i14, input = read_u8 input in + let* i15, input = read_u8 input in + let is = + [| i0; i1; i2; i3; i4; i5; i6; i7; i8; i9; i10; i11; i12; i13; i14; i15 |] + in + Ok (I8x16 (Shuffle is), input) + | 0x0E -> Ok (I8x16 Swizzle, input) + | 0x0F -> Ok (I8x16 Splat, input) + | 0x10 -> Ok (I16x8 Splat, input) + | 0x11 -> Ok (I32x4 Splat, input) + | 0x12 -> Ok (I64x2 Splat, input) + | 0x18 -> + let* n, input = read_u8 input in + Ok (I16x8 (Extract_lane_s n), input) + | 0x19 -> + let* n, input = read_u8 input in + Ok (I16x8 (Extract_lane_u n), input) + | 0x1B -> + let* n, input = read_u8 input in + Ok (I32x4 (Extract_lane n), input) + | 0x1C -> + let* n, input = read_u8 input in + Ok (I32x4 (Replace_lane n), input) + | 0x23 -> Ok (I8x16 Eq, input) + | 0x24 -> Ok (I8x16 Ne, input) + | 0x25 -> Ok (I8x16 (Lt S), input) + | 0x26 -> Ok (I8x16 (Lt U), input) + | 0x27 -> Ok (I8x16 (Gt S), input) + | 0x28 -> Ok (I8x16 (Gt U), input) + | 0x29 -> Ok (I8x16 (Le S), input) + | 0x2A -> Ok (I8x16 (Le U), input) + | 0x2B -> Ok (I8x16 (Ge S), input) + | 0x2C -> Ok (I8x16 (Ge U), input) + | 0x2D -> Ok (I16x8 Eq, input) + | 0x2E -> Ok (I16x8 Ne, input) + | 0x2F -> Ok (I16x8 (Lt S), input) + | 0x30 -> Ok (I16x8 (Lt U), input) + | 0x31 -> Ok (I16x8 (Gt S), input) + | 0x32 -> Ok (I16x8 (Gt U), input) + | 0x33 -> Ok (I16x8 (Le S), input) + | 0x34 -> Ok (I16x8 (Le U), input) + | 0x35 -> Ok (I16x8 (Ge S), input) + | 0x36 -> Ok (I16x8 (Ge U), input) + | 0x37 -> Ok (I32x4 Eq, input) + | 0x38 -> Ok (I32x4 Ne, input) + | 0x39 -> Ok (I32x4 (Lt S), input) + | 0x3A -> Ok (I32x4 (Lt U), input) + | 0x3B -> Ok (I32x4 (Gt S), input) + | 0x3C -> Ok (I32x4 (Gt U), input) + | 0x3D -> Ok (I32x4 (Le S), input) + | 0x3E -> Ok (I32x4 (Le U), input) + | 0x3F -> Ok (I32x4 (Ge S), input) + | 0x40 -> Ok (I32x4 (Ge U), input) + | 0x4D -> Ok (V128 Not, input) | 0x4E -> Ok (V128 And, input) + | 0x50 -> Ok (V128 Or, input) + | 0x53 -> Ok (V128 Any_true, input) + | 0x56 -> + let* idx, memarg, input = read_memarg 128 input in + let+ n, input = read_u8 input in + (V128 (Load32_lane (idx, memarg, n)), input) + | 0x5C -> + let+ idx, memarg, input = read_memarg 128 input in + (V128 (Load64_zero (idx, memarg)), input) + | 0x60 -> Ok (I8x16 Abs, input) + | 0x61 -> Ok (I8x16 Neg, input) + | 0x62 -> Ok (I8x16 Popcnt, input) + | 0x63 -> Ok (I8x16 All_true, input) + | 0x64 -> Ok (I8x16 Bitmask, input) | 0x6E -> Ok (I8x16 Add, input) | 0x71 -> Ok (I8x16 Sub, input) | 0x8E -> Ok (I16x8 Add, input) | 0x91 -> Ok (I16x8 Sub, input) | 0x95 -> Ok (I16x8 Mul, input) + | 0xA7 -> Ok (I32x4 Extend_low_i16x8_s, input) + | 0xA8 -> Ok (I32x4 Extend_high_i16x8_s, input) + | 0xA9 -> Ok (I32x4 Extend_low_i16x8_u, input) + | 0xAA -> Ok (I32x4 Extend_high_i16x8_u, input) + | 0xAB -> Ok (I32x4 Shl, input) + | 0xAC -> Ok (I32x4 (Shr S), input) + | 0xAD -> Ok (I32x4 (Shr U), input) | 0xAE -> Ok (I32x4 Add, input) | 0xB1 -> Ok (I32x4 Sub, input) | 0xB5 -> Ok (I32x4 Mul, input) + | 0xC8 -> Ok (I64x2 (Extend_low_i32x4 S), input) + | 0xC9 -> Ok (I64x2 (Extend_low_i32x4 U), input) | 0xCE -> Ok (I64x2 Add, input) | 0xD1 -> Ok (I64x2 Sub, input) | 0xD5 -> Ok (I64x2 Mul, input) + | 0xD6 -> Ok (I64x2 Eq, input) + | 0xD7 -> Ok (I64x2 Ne, input) + | 0xD8 -> Ok (I64x2 Lt_s, input) + | 0xD9 -> Ok (I64x2 Gt_s, input) + | 0xDA -> Ok (I64x2 Le_s, input) + | 0xDB -> Ok (I64x2 Ge_s, input) | i -> parse_fail "illegal opcode (read_FD) 0x%02X" i let block_type_of_type_def ty = diff --git a/src/symbolic/symbolic_i32.ml b/src/symbolic/symbolic_i32.ml index 36c9dce48..0a1e67fcf 100644 --- a/src/symbolic/symbolic_i32.ml +++ b/src/symbolic/symbolic_i32.ml @@ -40,3 +40,11 @@ let logor e1 e2 = let eq_concrete (e : t) (c : Int32.t) : Symbolic_boolean.t = let c = of_int32 c in Smtml.Typed.Bitv32.eq c e + +let min_int = of_int32 Int32.min_int + +let eqz (v : t) = eq v zero + +let ( = ) = eq + +let ( + ) = add diff --git a/src/symbolic/symbolic_i64.ml b/src/symbolic/symbolic_i64.ml index c9eef8871..fea90aa6e 100644 --- a/src/symbolic/symbolic_i64.ml +++ b/src/symbolic/symbolic_i64.ml @@ -7,3 +7,15 @@ include Smtml.Typed.Bitv64 let eq_concrete (e : t) (c : Int64.t) : Symbolic_boolean.t = let c = of_int64 c in Smtml.Typed.Bitv64.eq c e + +let min_int = of_int64 Int64.min_int + +let eqz (v : t) = eq v zero + +let ( = ) = eq + +let ( + ) = add + +let ( * ) = mul + +let ( / ) = div diff --git a/src/symbolic/symbolic_memory.ml b/src/symbolic/symbolic_memory.ml index 5d2d1f2e1..ad0f4b567 100644 --- a/src/symbolic/symbolic_memory.ml +++ b/src/symbolic/symbolic_memory.ml @@ -166,13 +166,26 @@ let load_32 m a = let v = load_32_unchecked m a in Smtml.Typed.simplify v -let load_64 m a = - let open Symbolic_choice in - let+ a = must_be_valid_address m a 8 in +let load_64_unchecked m a : Smtml.Typed.Bitv64.t = let low = load_32_unchecked m a in let high = load_32_unchecked m (Int32.add a 4l) in Smtml.Typed.Bitv32.concat high low +let load_64 m a = + let open Symbolic_choice in + let+ a = must_be_valid_address m a 8 in + load_64_unchecked m a + +let load_128_unchecked m a : Smtml.Typed.Bitv128.t = + let low = load_64_unchecked m a in + let high = load_64_unchecked m (Int32.add a 8l) in + Smtml.Typed.Bitv64.concat high low + +let load_128 m a = + let open Symbolic_choice in + let+ a = must_be_valid_address m a 16 in + load_128_unchecked m a + let store_8 m ~addr v = let open Symbolic_choice in let* a = must_be_valid_address m addr 1 in @@ -213,6 +226,12 @@ let store_64 m ~(addr : Symbolic_i32.t) v = let data = store_byte_list m.data a (Smtml.Typed.Bitv64.to_bytes v) in replace { m with data } +let store_128 m ~(addr : Symbolic_i32.t) v = + let open Symbolic_choice in + let* a = must_be_valid_address m addr 16 in + let data = store_byte_list m.data a (Smtml.Typed.Bitv128.to_bytes v) in + replace { m with data } + (* This function uses `m` for bounds checks but return an updated version of `data` *) let store_8_no_replace m data ~(addr : Symbolic_i32.t) v = let open Symbolic_choice in diff --git a/src/symbolic/symbolic_memory.mli b/src/symbolic/symbolic_memory.mli index b190384d9..25d341a59 100644 --- a/src/symbolic/symbolic_memory.mli +++ b/src/symbolic/symbolic_memory.mli @@ -9,6 +9,7 @@ include with type t := t and type i32 := Symbolic_i32.t and type i64 := Symbolic_i64.t + and type v128 := Symbolic_v128.t and type 'a choice := 'a Symbolic_choice.t val replace : t -> unit Symbolic_choice.t diff --git a/src/symbolic/symbolic_value.ml b/src/symbolic/symbolic_value.ml index a5b0cc960..c12e99343 100644 --- a/src/symbolic/symbolic_value.ml +++ b/src/symbolic/symbolic_value.ml @@ -2,16 +2,12 @@ (* Copyright © 2021-2026 OCamlPro *) (* Written by the Owi programmers *) -module Boolean = Symbolic_boolean -module I32 = Symbolic_i32 -module F32 = Symbolic_f32 -module I64 = Symbolic_i64 -module F64 = Symbolic_f64 -module V128 = Symbolic_v128 -module Ref = Symbolic_ref - type boolean = Smtml.Typed.Bool.t +type i8 = Smtml.Typed.Bitv8.t + +type i16 = Smtml.Typed.Bitv16.t + type i32 = Smtml.Typed.Bitv32.t type i64 = Smtml.Typed.Bitv64.t @@ -22,6 +18,14 @@ type f64 = Smtml.Typed.Float64.t type v128 = Smtml.Typed.Bitv128.t +module Boolean = Symbolic_boolean +module I32 = Symbolic_i32 +module F32 = Symbolic_f32 +module I64 = Symbolic_i64 +module F64 = Symbolic_f64 +module V128 = Symbolic_v128 +module Ref = Symbolic_ref + type t = | I32 of Smtml.Typed.Bitv32.t | I64 of Smtml.Typed.Bitv64.t diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml index eabb7d2dd..5c83b0a16 100644 --- a/src/symbolic/symbolic_wasm_ffi.ml +++ b/src/symbolic/symbolic_wasm_ffi.ml @@ -220,19 +220,97 @@ let symbolic_extern_module = in { Extern.Module.functions; func_type = Symbolic_extern_func.extern_type } +let args_get _ _ = + (* TODO *) + Log.warn (fun m -> m "used dummy args_get implementation"); + Symbolic_choice.return Symbolic_i32.zero + +let args_sizes_get _ _ = + (* TODO *) + Log.warn (fun m -> m "used dummy args_sizes_get implementation"); + Symbolic_choice.return Symbolic_i32.zero + +let clock_time_get _ _ _ = assert false + +let environ_get _ _ = assert false + +let environ_sizes_get _ _ = + (* TODO *) + Log.warn (fun m -> m "used dummy environ_sizes_get implementation"); + Symbolic_choice.return Symbolic_i32.zero + +let fd_close _ = assert false + +let fd_fdstat_get _ _ = assert false + +let fd_fdstat_set_flags _ _ = assert false + +let fd_filestat_get _ _ = assert false + +let fd_filestat_set_size _ _ = assert false + +let fd_prestat_get _ _ = assert false + +let fd_prestat_dir_name _ _ _ = assert false + +let fd_read _ _ _ _ = assert false + +let fd_seek _ _ _ _ = assert false + let fd_write _ _ _ _ = assert false +let path_create_directory _ _ _ = assert false + +let path_filestat_get _ _ _ _ _ = assert false + +let path_open _ _ _ _ _ _ _ _ _ = assert false + +let poll_oneoff _ _ _ _ = assert false + let proc_exit _ = + (* TODO *) Log.warn (fun m -> m "used dummy proc_exit implementation"); Symbolic_choice.return () let random_get _ _ = + (* TODO *) Log.warn (fun m -> m "used dummy random_get implementation"); - Symbolic_choice.return @@ Symbolic_i32.zero + Symbolic_choice.return Symbolic_i32.zero let wasi_snapshot_preview1 = let functions = - [ ("fd_write", Extern_func (i32 ^-> i32 ^-> i32 ^-> i32 ^->. i32, fd_write)) + [ ("args_get", Extern_func (i32 ^-> i32 ^->. i32, args_get)) + ; ("args_sizes_get", Extern_func (i32 ^-> i32 ^->. i32, args_sizes_get)) + ; ("environ_get", Extern_func (i32 ^-> i32 ^->. i32, environ_get)) + ; ( "environ_sizes_get" + , Extern_func (i32 ^-> i32 ^->. i32, environ_sizes_get) ) + ; ( "clock_time_get" + , Extern_func (i32 ^-> i64 ^-> i32 ^->. i32, clock_time_get) ) + ; ("fd_close", Extern_func (i32 ^->. i32, fd_close)) + ; ("fd_fdstat_get", Extern_func (i32 ^-> i32 ^->. i32, fd_fdstat_get)) + ; ( "fd_fdstat_set_flags" + , Extern_func (i32 ^-> i32 ^->. i32, fd_fdstat_set_flags) ) + ; ("fd_filestat_get", Extern_func (i32 ^-> i32 ^->. i32, fd_filestat_get)) + ; ( "fd_filestat_set_size" + , Extern_func (i32 ^-> i64 ^->. i32, fd_filestat_set_size) ) + ; ("fd_prestat_get", Extern_func (i32 ^-> i32 ^->. i32, fd_prestat_get)) + ; ( "fd_prestat_dir_name" + , Extern_func (i32 ^-> i32 ^-> i32 ^->. i32, fd_prestat_dir_name) ) + ; ("fd_read", Extern_func (i32 ^-> i32 ^-> i32 ^-> i32 ^->. i32, fd_read)) + ; ("fd_seek", Extern_func (i32 ^-> i64 ^-> i32 ^-> i32 ^->. i32, fd_seek)) + ; ("fd_write", Extern_func (i32 ^-> i32 ^-> i32 ^-> i32 ^->. i32, fd_write)) + ; ( "path_create_directory" + , Extern_func (i32 ^-> i32 ^-> i32 ^->. i32, path_create_directory) ) + ; ( "path_filestat_get" + , Extern_func + (i32 ^-> i32 ^-> i32 ^-> i32 ^-> i32 ^->. i32, path_filestat_get) ) + ; ( "path_open" + , Extern_func + ( i32 ^-> i32 ^-> i32 ^-> i32 ^-> i32 ^-> i64 ^-> i64 ^-> i32 ^-> i32 + ^->. i32 + , path_open ) ) + ; ( "poll_oneoff" + , Extern_func (i32 ^-> i32 ^-> i32 ^-> i32 ^->. i32, poll_oneoff) ) ; ("proc_exit", Extern_func (i32 ^->. unit, proc_exit)) ; ("random_get", Extern_func (i32 ^-> i32 ^->. i32, random_get)) ] diff --git a/src/validate/binary_validate.ml b/src/validate/binary_validate.ml index 8aba8b898..1aa5ed6e0 100644 --- a/src/validate/binary_validate.ml +++ b/src/validate/binary_validate.ml @@ -593,35 +593,135 @@ let typecheck_v128_instr (env : Env.t) stack : Binary.v128_instr -> _ = function | Const _ -> let+ stack = Stack.push [ v128 ] stack in (env, stack) - | And -> + | Not -> + let* stack = Stack.pop env.modul [ v128 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) + | Any_true -> + let* stack = Stack.pop env.modul [ v128 ] stack in + let+ stack = Stack.push [ i32 ] stack in + (env, stack) + | And | Or -> let* stack = Stack.pop env.modul [ v128; v128 ] stack in let+ stack = Stack.push [ v128 ] stack in (env, stack) - | _ -> raise @@ Failure "TODO" + | Load (indice, memarg) + | Load16x4_s (indice, memarg) + | Load16x4_u (indice, memarg) -> + let* is_i64 = check_mem env.modul indice in + let* () = check_memarg ~is_i64 memarg 16l in + let* stack = Stack.pop env.modul [ i32 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) + | Load32_lane (indice, memarg, lane) -> + if lane >= 4 then Fmt.error_msg "invalid lane index" + else + let* is_i64 = check_mem env.modul indice in + let* () = check_memarg ~is_i64 memarg 8l in + let* stack = Stack.pop env.modul [ v128; i32 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) + | Load64_zero (indice, memarg) -> + let* is_i64 = check_mem env.modul indice in + let* () = check_memarg ~is_i64 memarg 8l in + let* stack = Stack.pop env.modul [ i32 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) + | Store (indice, memarg) -> + let* is_i64 = check_mem env.modul indice in + let* () = check_memarg ~is_i64 memarg 16l in + let+ stack = Stack.pop env.modul [ v128; i32 ] stack in + (env, stack) let typecheck_i8x16_instr (env : Env.t) stack = function - | (Add : Text.i8x16_instr) | Sub -> + | (Add : Text.i8x16_instr) + | Sub | Eq | Ne | Lt _ | Gt _ | Le _ | Ge _ | Swizzle -> let* stack = Stack.pop env.modul [ v128; v128 ] stack in let+ stack = Stack.push [ v128 ] stack in (env, stack) + | Shuffle indices -> + if Array.exists (fun i -> i >= 32) indices then + Fmt.error_msg "invalid lane index" + else + let* stack = Stack.pop env.modul [ v128; v128 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) + | Splat -> + let* stack = Stack.pop env.modul [ i32 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) + | Bitmask | All_true -> + let* stack = Stack.pop env.modul [ v128 ] stack in + let+ stack = Stack.push [ i32 ] stack in + (env, stack) + | Abs | Neg | Popcnt -> + let* stack = Stack.pop env.modul [ v128 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) let typecheck_i16x8_instr (env : Env.t) stack = function - | (Add : Text.i16x8_instr) | Sub | Mul -> + | (Add : Text.i16x8_instr) | Sub | Mul | Eq | Ne | Lt _ | Gt _ | Le _ | Ge _ + -> let* stack = Stack.pop env.modul [ v128; v128 ] stack in let+ stack = Stack.push [ v128 ] stack in (env, stack) + | Extract_lane_s i | Extract_lane_u i -> + if i >= 8 then Fmt.error_msg "invalid lane index" + else + let* stack = Stack.pop env.modul [ v128 ] stack in + let+ stack = Stack.push [ i32 ] stack in + (env, stack) + | Splat -> + let* stack = Stack.pop env.modul [ i32 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) let typecheck_i32x4_instr (env : Env.t) stack = function - | (Add : Text.i32x4_instr) | Sub | Mul -> + | (Add : Text.i32x4_instr) | Sub | Mul | Lt _ | Gt _ | Le _ | Ge _ | Eq | Ne + -> let* stack = Stack.pop env.modul [ v128; v128 ] stack in let+ stack = Stack.push [ v128 ] stack in (env, stack) + | Shl | Shr (S | U) -> + let* stack = Stack.pop env.modul [ i32; v128 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) + | Extract_lane i -> + if i >= 4 then Fmt.error_msg "invalid lane index" + else + let* stack = Stack.pop env.modul [ v128 ] stack in + let+ stack = Stack.push [ i32 ] stack in + (env, stack) + | Splat -> + let* stack = Stack.pop env.modul [ i32 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) + | Replace_lane i -> + if i >= 4 then Fmt.error_msg "invalid lane index" + else + let* stack = Stack.pop env.modul [ i32; v128 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) + | Extend_low_i16x8_s | Extend_high_i16x8_s | Extend_low_i16x8_u + | Extend_high_i16x8_u -> + let* stack = Stack.pop env.modul [ v128 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) let typecheck_i64x2_instr (env : Env.t) stack = function - | (Add : Text.i64x2_instr) | Sub | Mul -> + | (Add : Text.i64x2_instr) | Sub | Mul | Eq | Ne | Lt_s | Gt_s | Le_s | Ge_s + -> let* stack = Stack.pop env.modul [ v128; v128 ] stack in let+ stack = Stack.push [ v128 ] stack in (env, stack) + | Splat -> + let* stack = Stack.pop env.modul [ i64 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) + | Extend_low_i32x4 (S | U) -> + let* stack = Stack.pop env.modul [ v128 ] stack in + let+ stack = Stack.push [ v128 ] stack in + (env, stack) let typecheck_ref_instr (env : Env.t) stack = function | Is_null -> @@ -633,9 +733,9 @@ let typecheck_ref_instr (env : Env.t) stack = function let* t = ref_type_as_non_null t in let+ stack = Stack.push [ t ] stack in (env, stack) - (* TODO: The type can be Something/Any, and if its a Ref_type the heap_type - can be a TypeUse or Extern_ht. The pushed type should account for that - and restrict whatever the type is to non_null. *) + (* TODO: The type can be Something/Any, and if its a Ref_type the heap_type + can be a TypeUse or Extern_ht. The pushed type should account for that + and restrict whatever the type is to non_null. *) | Null rt -> let+ stack = Stack.push [ Ref_type (Null, rt) ] stack in (env, stack) diff --git a/test/fuzz/basic.ml b/test/fuzz/basic.ml index 39c09c925..8279cddb9 100644 --- a/test/fuzz/basic.ml +++ b/test/fuzz/basic.ml @@ -263,13 +263,13 @@ let funop_32 : instr gen = let funop_64 : instr gen = let+ funop = choose - [ const Abs - ; const Neg - ; const Sqrt - ; const Ceil - ; const Floor - ; const Trunc - ; const Nearest + [ const (Abs : f64_instr) + ; const (Neg : f64_instr) + ; const (Sqrt : f64_instr) + ; const (Ceil : f64_instr) + ; const (Floor : f64_instr) + ; const (Trunc : f64_instr) + ; const (Nearest : f64_instr) ] in F64 funop @@ -291,11 +291,11 @@ let frelop_64 : instr gen = let+ frelop = choose [ const (Owi.Text.Eq : f64_instr) - ; const Ne - ; const Lt - ; const Gt - ; const Le - ; const Ge + ; const (Ne : f64_instr) + ; const (Lt : f64_instr) + ; const (Gt : f64_instr) + ; const (Le : f64_instr) + ; const (Ge : f64_instr) ] in F64 frelop