diff --git a/doc/src/sap/examples.md b/doc/src/sap/examples.md index ac8b7e82c..1e44d64c1 100644 --- a/doc/src/sap/examples.md +++ b/doc/src/sap/examples.md @@ -134,7 +134,7 @@ Then we use `owi_assert(p.getPoly() != 0)`. Which should fail as this polynomial $ owi c++ ./poly.cpp -w1 --no-assert-failure-expression-printing owi: [ERROR] Assert failure model { - symbol symbol_0 i32 2 + symbol symbol_0 i32 4 } owi: [ERROR] Reached problem! [13] diff --git a/doc/src/symex/quickstart.md b/doc/src/symex/quickstart.md index 50b069f49..6bcff10cc 100644 --- a/doc/src/symex/quickstart.md +++ b/doc/src/symex/quickstart.md @@ -367,8 +367,8 @@ owi: [ERROR] Reached problem! $ owi rust ./mean.rs --entry-point=check --invoke-with-symbols -w1 --fail-on-assertion-only --no-assert-failure-expression-printing --deterministic-result-order owi: [ERROR] Assert failure model { - symbol symbol_0 i32 915013628 - symbol symbol_1 i32 -1225654275 + symbol symbol_0 i32 1069400062 + symbol symbol_1 i32 -1881784317 } owi: [ERROR] Reached problem! @@ -380,8 +380,8 @@ owi: [ERROR] Reached problem! $ owi zig ./mean.zig --entry-point=check --invoke-with-symbols -w1 --fail-on-assertion-only --no-assert-failure-expression-printing --deterministic-result-order owi: [ERROR] Assert failure model { - symbol symbol_0 i32 -722535840 - symbol symbol_1 i32 -418314849 + symbol symbol_0 i32 1610570242 + symbol symbol_1 i32 -1610637823 } owi: [ERROR] Reached problem! diff --git a/dune-project b/dune-project index 7ed58e996..1b97b3d8e 100644 --- a/dune-project +++ b/dune-project @@ -41,7 +41,7 @@ (depends ;; build (ocaml - (>= 5.2)) + (>= 5.4)) (menhir (and :build diff --git a/owi.opam b/owi.opam index c71d9ab67..f87b50e56 100644 --- a/owi.opam +++ b/owi.opam @@ -25,7 +25,7 @@ homepage: "https://github.com/ocamlpro/owi" bug-reports: "https://github.com/ocamlpro/owi/issues" depends: [ "dune" {>= "3.7"} - "ocaml" {>= "5.2"} + "ocaml" {>= "5.4"} "menhir" {build & >= "20220210"} "dune-build-info" {build} "dune-site" {build} diff --git a/shell.nix b/shell.nix index 7f9741493..acc61e1ea 100644 --- a/shell.nix +++ b/shell.nix @@ -1,32 +1,30 @@ -{ pkgs ? import (builtins.fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/master.tar.gz"; - }) {} -}: - let - smtml = pkgs.ocamlPackages.smtml.overrideAttrs (old: { + pkgs = import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/nixos-unstable.tar.gz") {}; + ocamlPackages = pkgs.ocaml-ng.ocamlPackages_5_4; + smtml = ocamlPackages.smtml.overrideAttrs (old: { src = pkgs.fetchFromGitHub { owner = "formalsec"; repo = "smtml"; - rev = "3b08a5368718068fa46547e60df4e44caa51db78"; - hash = "sha256-iD2UGddGYvE/jn+KM5jj05DHcNPjSq9IiH1BlnfO+Sg="; + rev = "27aa552f228cdaf36283396ade722cdcae5d1712"; + hash = "sha256-VnkF+bZXeqaj9LSpyzqH5AM9EQsrW4Rlj5kvyTfYTKE="; }; doCheck = false; }); - synchronizer = pkgs.ocamlPackages.synchronizer.overrideAttrs (old: { + synchronizer = ocamlPackages.synchronizer.overrideAttrs (old: { src = pkgs.fetchFromGitHub { owner = "ocamlpro"; repo = "synchronizer"; rev = "cb5fd995e8a42e5244acf68f238221594fd19a8d"; hash = "sha256-0XtPHpDlyH1h8W2ZlRvJbZjCN9WP5mzk2N01WFd8eLQ="; }; + doCheck = false; }); in pkgs.mkShell { name = "owi-dev-shell"; dontDetectOcamlConflicts = true; - nativeBuildInputs = with pkgs.ocamlPackages; [ + nativeBuildInputs = with ocamlPackages; [ dune_3 findlib bisect_ppx @@ -51,7 +49,7 @@ pkgs.mkShell { pkgs.zig pkgs.makeWrapper ]; - buildInputs = with pkgs.ocamlPackages; [ + buildInputs = with ocamlPackages; [ bos cmdliner crowbar diff --git a/src/cmd/cmd_call_graph.ml b/src/cmd/cmd_call_graph.ml index 7c7880707..202073c88 100644 --- a/src/cmd/cmd_call_graph.ml +++ b/src/cmd/cmd_call_graph.ml @@ -18,7 +18,7 @@ let find_functions_with_func_type func_type (acc, i) in if Text.func_type_eq func_type ft then (S.add i acc, i + 1) else (acc, i + 1) -let rec find_children mode tables (funcs : 'a array) acc (l : Binary.expr) = +let rec find_children mode tables (funcs : 'a Iarray.t) acc (l : Binary.expr) = match (l, mode) with | [], _ -> acc | ({ raw = Call i | Return_call i; _ } as instr) :: l, _ -> @@ -32,7 +32,7 @@ let rec find_children mode tables (funcs : 'a array) acc (l : Binary.expr) = :: l , Complete ) -> let children, _ = - Array.fold_left (find_functions_with_func_type ft) (S.empty, 0) funcs + Iarray.fold_left (find_functions_with_func_type ft) (S.empty, 0) funcs in Annotated.update_functions_called instr children; let acc = S.union children acc in @@ -45,7 +45,7 @@ let rec find_children mode tables (funcs : 'a array) acc (l : Binary.expr) = let t_opt = M.find_opt i tables in let f = Option.bind t_opt (fun t -> - match Array.get t (Int32.to_int x) with + match Iarray.get t (Int32.to_int x) with | Ok n -> Some (Int32.to_int n) | _ -> None ) in @@ -97,17 +97,17 @@ let get_const_global env id = let eval_const_instr env stack instr = match instr.Annotated.raw with - | Binary.I32_const n -> ok @@ Stack.push_i32 stack n - | I64_const n -> ok @@ Stack.push_i64 stack n - | F32_const f -> ok @@ Stack.push_f32 stack f - | F64_const f -> ok @@ Stack.push_f64 stack f - | V128_const f -> ok @@ Stack.push_v128 stack f - | I_binop (nn, op) -> ok @@ eval_ibinop stack nn op - | Ref_null t -> ok @@ Stack.push_ref stack (Concrete_ref.null t) + | Binary.I32_const n -> Result.ok @@ Stack.push_i32 stack n + | I64_const n -> Result.ok @@ Stack.push_i64 stack n + | F32_const f -> Result.ok @@ Stack.push_f32 stack f + | F64_const f -> Result.ok @@ Stack.push_f64 stack f + | V128_const f -> Result.ok @@ Stack.push_v128 stack f + | I_binop (nn, op) -> Result.ok @@ eval_ibinop stack nn op + | Ref_null t -> Result.ok @@ Stack.push_ref stack (Concrete_ref.null t) | Global_get id -> let* g = get_const_global env id in - ok @@ Stack.push_i32 stack g - | Ref_func id -> ok @@ Stack.push_i32_of_int stack id + Result.ok @@ Stack.push_i32 stack g + | Ref_func id -> Result.ok @@ Stack.push_i32_of_int stack id | _ -> assert false let eval_const env exp = @@ -125,7 +125,7 @@ let eval_tables tables env = let t = List.map (fun (n, elem) -> - (n, Array.of_list (List.map (eval_const env) elem.Binary.Elem.init)) ) + (n, Iarray.of_list (List.map (eval_const env) elem.Binary.Elem.init)) ) tables in M.of_list t @@ -150,7 +150,7 @@ let rec find_tables acc (e : Binary.instr Annotated.t) = let find_tables_to_remove export_tables funcs = let l = List.map (fun (x : Binary.Export.t) -> x.id) export_tables in - Array.fold_left + Iarray.fold_left (fun acc f -> match f with | Origin.Local x -> List.fold_left find_tables acc x.Binary.Func.body.raw @@ -169,7 +169,7 @@ let rec remove_tables (l1 : (int * Binary.Elem.t) list) l2 acc = let find_entry_points (m : Binary.Module.t) = let l = Option.to_list m.start in - Array.fold_left + Iarray.fold_left (fun acc (x : Binary.Export.t) -> x.id :: acc) l m.exports.func @@ -177,7 +177,7 @@ let find_entries entry_point (m : Binary.Module.t) = let entries = Option.bind (Option.bind entry_point (fun x -> - Array.find_index + Iarray.find_index (function | Origin.Local (y : Binary.Func.t) -> Option.compare String.compare (Some x) y.id = 0 @@ -201,20 +201,20 @@ let build_call_graph call_graph_mode (m : Binary.Module.t) entry_point = match e.Binary.Elem.mode with | Active (Some n, _) -> Some (n, e) | _ -> None ) - (Array.to_list m.elem) + (Iarray.to_list m.elem) in - let t = find_tables_to_remove (Array.to_list m.exports.table) funcs in + let t = find_tables_to_remove (Iarray.to_list m.exports.table) funcs in remove_tables (List.sort_uniq (fun x y -> compare (fst x) (fst y)) elems) (List.sort_uniq compare t) [] in - let env, _ = Array.fold_left build_env (M.empty, 0) m.global in + let env, _ = Iarray.fold_left build_env (M.empty, 0) m.global in eval_tables tables env in let l, _ = - Array.fold_left (build_graph call_graph_mode tables funcs) ([], 0) funcs + Iarray.fold_left (build_graph call_graph_mode tables funcs) ([], 0) funcs in let entries = find_entries entry_point m in Call_graph.init l entries diff --git a/src/cmd/cmd_cfg.ml b/src/cmd/cmd_cfg.ml index 3ee6b30b0..f87d34361 100644 --- a/src/cmd/cmd_cfg.ml +++ b/src/cmd/cmd_cfg.ml @@ -97,7 +97,7 @@ let rec build_graph (l : Binary.expr) nodes n node edges let nodes = (n, instr :: node) :: nodes in let edges_to_add = (n, Ind i, None) :: edges_to_add in let edges_to_add, _ = - Array.fold_left + Iarray.fold_left (fun (acc, x) (i : Binary.indice) -> ((n, Ind i, Some (Int32.of_int x)) :: acc, x + 1) ) (edges_to_add, 0) inds @@ -130,7 +130,7 @@ let build_cfg_from_text_module modul entry = match m with | Ok m -> let f = - match Array.get m.func entry with + match Iarray.get m.func entry with | Origin.Local f -> f | _ -> assert false in @@ -150,7 +150,7 @@ let cmd ~source_file ~entry_point = match int_of_string_opt x with | Some _ as x -> x | None -> - Array.find_index + Iarray.find_index (function | Origin.Local (y : Binary.Func.t) -> Option.compare String.compare (Some x) y.id = 0 @@ -159,7 +159,7 @@ let cmd ~source_file ~entry_point = ~default:0 in let f = - match Array.get m.func entry with Origin.Local f -> f | _ -> assert false + match Iarray.get m.func entry with Origin.Local f -> f | _ -> assert false in let nodes, edges = build_cfg f.body.raw in let graph = Control_flow_graph.init nodes edges in diff --git a/src/cmd/cmd_iso.ml b/src/cmd/cmd_iso.ml index e8470e881..e5732d9a6 100644 --- a/src/cmd/cmd_iso.ml +++ b/src/cmd/cmd_iso.ml @@ -326,36 +326,36 @@ let cmd ~deterministic_result_order ~fail_mode ~exploration_strategy ~files let funcexports1 = module1.exports.func - |> Array.map (fun { Binary.Export.name; id } -> + |> Iarray.map (fun { Binary.Export.name; id } -> let typ = Binary.Module.get_func_type id module1 in (name, typ) ) in let funcexports2 = module2.exports.func - |> Array.map (fun { Binary.Export.name; id } -> + |> Iarray.map (fun { Binary.Export.name; id } -> let typ = Binary.Module.get_func_type id module2 in (name, typ) ) in - let exports_name_1 = Array.map fst funcexports1 in - let exports_name_2 = Array.map fst funcexports2 in + let exports_name_1 = Iarray.map fst funcexports1 in + let exports_name_2 = Iarray.map fst funcexports2 in Log.debug (fun m -> m "%a exports: %a" Fpath.pp file1 - (Fmt.array ~sep:(fun fmt () -> Fmt.pf fmt " ") Fmt.string) + (Fmt.iter Iarray.iter ~sep:(fun fmt () -> Fmt.pf fmt " ") Fmt.string) exports_name_1 ); Log.debug (fun m -> m "%a exports: %a" Fpath.pp file2 - (Fmt.array ~sep:(fun fmt () -> Fmt.pf fmt " ") Fmt.string) + (Fmt.iter Iarray.iter ~sep:(fun fmt () -> Fmt.pf fmt " ") Fmt.string) exports_name_2 ); - let array_to_string_set a = - Array.fold_left (fun s v -> String_set.add v s) String_set.empty a + let iarray_to_string_set a = + Iarray.fold_left (fun s v -> String_set.add v s) String_set.empty a in - let exports_name_1 = array_to_string_set exports_name_1 in - let exports_name_2 = array_to_string_set exports_name_2 in + let exports_name_1 = iarray_to_string_set exports_name_1 in + let exports_name_2 = iarray_to_string_set exports_name_2 in let common_exports = String_set.inter exports_name_1 exports_name_2 |> String_set.to_list @@ -365,12 +365,12 @@ let cmd ~deterministic_result_order ~fail_mode ~exploration_strategy ~files List.fold_left (fun common_exports name -> let typ1 = - Array.find_opt + Iarray.find_opt (fun (name', _typ) -> String.equal name name') funcexports1 in let typ2 = - Array.find_opt + Iarray.find_opt (fun (name', _typ) -> String.equal name name') funcexports2 in diff --git a/src/cmd/cmd_replay.ml b/src/cmd/cmd_replay.ml index 623f438de..fd056fb69 100644 --- a/src/cmd/cmd_replay.ml +++ b/src/cmd/cmd_replay.ml @@ -40,7 +40,7 @@ let compile_file ~unsafe ~entry_point ~invoke_with_symbols filename model = let symbol_i32 () = let i = next () in - match model.(i) with + match Iarray.get model i with | Concrete_value.I32 n -> add_sym i; Ok n @@ -51,7 +51,7 @@ let compile_file ~unsafe ~entry_point ~invoke_with_symbols filename model = let symbol_i64 () = let i = next () in - match model.(i) with + match Iarray.get model i with | Concrete_value.I64 n -> add_sym i; Ok n @@ -62,7 +62,7 @@ let compile_file ~unsafe ~entry_point ~invoke_with_symbols filename model = let symbol_f32 () = let i = next () in - match model.(i) with + match Iarray.get model i with | Concrete_value.F32 n -> add_sym i; Ok n @@ -73,7 +73,7 @@ let compile_file ~unsafe ~entry_point ~invoke_with_symbols filename model = let symbol_f64 () = let i = next () in - match model.(i) with + match Iarray.get model i with | Concrete_value.F64 n -> add_sym i; Ok n @@ -84,7 +84,7 @@ let compile_file ~unsafe ~entry_point ~invoke_with_symbols filename model = let symbol_v128 () = let i = next () in - match model.(i) with + match Iarray.get model i with | Concrete_value.V128 n -> add_sym i; Ok n @@ -108,7 +108,7 @@ let compile_file ~unsafe ~entry_point ~invoke_with_symbols filename model = let symbol_range _ _ = let i = next () in - match model.(i) with + match Iarray.get model i with | Concrete_value.I32 n -> add_sym i; Ok n @@ -129,7 +129,7 @@ let compile_file ~unsafe ~entry_point ~invoke_with_symbols filename model = if Int32.gt p 255l || Int32.lt p 0l then trap `Invalid_character_in_memory else let ch = char_of_int (Int32.to_int p) in - if Char.equal ch '\x00' then return (List.rev accu |> Array.of_list) + if Char.equal ch '\x00' then return (List.rev accu |> Iarray.of_list) else make_str m (ch :: accu) (Int32.add i (Int32.of_int 1)) let cov_label_is_covered id = @@ -139,13 +139,13 @@ let compile_file ~unsafe ~entry_point ~invoke_with_symbols filename model = let cov_label_set m id str_ptr = let+ chars = make_str m [] str_ptr in - let str = String.init (Array.length chars) (Array.get chars) in + let str = String.init (Iarray.length chars) (Iarray.get chars) in Hashtbl.add covered_labels id str; Log.debug (fun m -> m "reached %ld@." id) let open_scope m strptr = let+ chars = make_str m [] strptr in - let str = String.init (Array.length chars) (Array.get chars) in + let str = String.init (Iarray.length chars) (Iarray.get chars) in scopes := Symbol_scope.open_scope str !scopes let close_scope () = @@ -227,7 +227,7 @@ let parse_model replay_file = (Fmt.str "unexpected value type: %a" Smtml.Value.pp v) ) ) bindings in - Array.of_list model + Iarray.of_list model let cmd ~unsafe ~replay_file ~source_file ~entry_point ~invoke_with_symbols = let* model = parse_model replay_file in diff --git a/src/compile/assigned.ml b/src/compile/assigned.ml index 61a72826d..69955623f 100644 --- a/src/compile/assigned.ml +++ b/src/compile/assigned.ml @@ -5,7 +5,7 @@ open Syntax type t = - { typ : Text.func_type Array.t + { typ : Text.func_type Iarray.t ; typ_names : (string, int) Hashtbl.t ; global_names : (string, int) Hashtbl.t ; table_names : (string, int) Hashtbl.t @@ -41,7 +41,7 @@ let pp fmt Func names: %a@\n\ Elem names: %a@\n\ Data names: %a@\n" - (Fmt.array Text.pp_func_type) + (Fmt.iter Iarray.iter Text.pp_func_type) typ pp_table typ_names pp_table global_names pp_table table_names pp_table mem_names pp_table func_names pp_table elem_names pp_table data_names @@ -54,11 +54,11 @@ module Typetbl = Hashtbl.Make (struct end) let assign_types typ function_type : - Text.func_type Array.t * (string, int) Hashtbl.t = + Text.func_type Iarray.t * (string, int) Hashtbl.t = let all_types = Typetbl.create 64 in let named_types = Hashtbl.create 64 in let declared_types = Dynarray.create () in - Array.iter + Iarray.iter (fun (name, typ) -> let id = Dynarray.length declared_types in begin match name with @@ -68,7 +68,7 @@ let assign_types typ function_type : Dynarray.add_last declared_types typ; Typetbl.add all_types typ id ) typ; - Array.iter + Iarray.iter (fun typ -> match Typetbl.find_opt all_types typ with | Some _id -> () @@ -77,7 +77,7 @@ let assign_types typ function_type : Dynarray.add_last declared_types typ; Typetbl.add all_types typ id ) function_type; - let declared_types = Dynarray.to_array declared_types in + let declared_types = Dynarray.to_array declared_types |> Iarray.of_array in (declared_types, named_types) let get_origin_name (get_name : 'a -> string option) (elt : ('a, 'b) Origin.t) : @@ -89,7 +89,7 @@ let get_origin_name (get_name : 'a -> string option) (elt : ('a, 'b) Origin.t) : let name kind ~get_name values = let named = Hashtbl.create 64 in let+ () = - array_iteri + iarray_iteri (fun i elt_v -> match get_name elt_v with | None -> Ok () @@ -104,7 +104,7 @@ let name kind ~get_name values = in named -let check_type_id (types : Text.func_type Array.t) +let check_type_id (types : Text.func_type Iarray.t) (typ_names : (string, int) Hashtbl.t) (id, func_type) = let id = match id with @@ -114,9 +114,9 @@ let check_type_id (types : Text.func_type Array.t) | None -> assert false | Some v -> v ) in - if id >= Array.length types then Error (`Unknown_type (Text.Raw id)) + if id >= Iarray.length types then Error (`Unknown_type (Text.Raw id)) else - let func_type' = Array.unsafe_get types id in + let func_type' = Iarray.unsafe_get types id in if not (Text.func_type_eq func_type func_type') then Error `Inline_function_type else Ok () @@ -152,7 +152,7 @@ let of_grouped let* data_names = name "data" ~get_name:(fun (data : Text.Data.t) -> data.id) data in - let+ () = array_iter (check_type_id typ typ_names) type_checks in + let+ () = iarray_iter (check_type_id typ typ_names) type_checks in let modul = { typ @@ -189,12 +189,12 @@ let find_elem modul id = find modul.elem_names (`Unknown_elem id) id let find_type modul id = find modul.typ_names (`Unknown_type id) id let get_type modul idx = - if idx >= Array.length modul.typ then None - else Some (Array.unsafe_get modul.typ idx) + if idx >= Iarray.length modul.typ then None + else Some (Iarray.unsafe_get modul.typ idx) let get_types modul = modul.typ let find_raw_type modul func_type = - match Array.find_index (Text.func_type_eq func_type) modul.typ with + match Iarray.find_index (Text.func_type_eq func_type) modul.typ with | None -> assert false | Some idx -> idx diff --git a/src/compile/assigned.mli b/src/compile/assigned.mli index 7197369e1..613c6fc70 100644 --- a/src/compile/assigned.mli +++ b/src/compile/assigned.mli @@ -22,7 +22,7 @@ val find_type : t -> Text.indice -> Binary.indice Result.t val get_type : t -> int -> Text.func_type Option.t -val get_types : t -> Text.func_type Array.t +val get_types : t -> Text.func_type Iarray.t val find_raw_type : t -> Text.func_type -> Binary.indice diff --git a/src/compile/binary_to_text.ml b/src/compile/binary_to_text.ml index 47c50d405..b2b5446fa 100644 --- a/src/compile/binary_to_text.ml +++ b/src/compile/binary_to_text.ml @@ -11,7 +11,7 @@ let convert_block_type : Binary.block_type -> Text.block_type = function let rec convert_instr : Binary.instr -> Text.instr = function | Br_table (ids, id) -> - let ids = Array.map convert_indice ids in + let ids = Iarray.map convert_indice ids in let id = convert_indice id in Br_table (ids, id) | Br_if id -> @@ -194,12 +194,13 @@ let convert_data : Binary.Data.t -> Text.Data.t = function { id; init; mode } let from_types types : Text.Module.Field.t list = - Array.map (fun (t : Text.Typedef.t) -> Text.Module.Field.Typedef t) types - |> Array.to_list + Iarray.map (fun (t : Text.Typedef.t) -> Text.Module.Field.Typedef t) types + |> Iarray.to_list -let from_global (global : (Binary.Global.t, Text.Global.Type.t) Origin.t array) - : Text.Module.Field.t list = - Array.map +let from_global + (global : (Binary.Global.t, Text.Global.Type.t) Origin.t Iarray.t) : + Text.Module.Field.t list = + Iarray.map (function | Origin.Local (g : Binary.Global.t) -> let init = convert_expr g.init in @@ -209,30 +210,30 @@ let from_global (global : (Binary.Global.t, Text.Global.Type.t) Origin.t array) let typ = Text.Import.Type.Global (assigned_name, typ) in Text.Module.Field.Import { modul_name; name; typ } ) global - |> Array.to_list + |> Iarray.to_list let from_table table : Text.Module.Field.t list = - Array.map + Iarray.map (function | Origin.Local (name, t) -> Text.Module.Field.Table (name, t) | Imported { modul_name; name; assigned_name; typ } -> let typ = Text.Import.Type.Table (assigned_name, typ) in Import { modul_name; name; typ } ) table - |> Array.to_list + |> Iarray.to_list let from_mem mem : Text.Module.Field.t list = - Array.map + Iarray.map (function | Origin.Local (name, t) -> Text.Module.Field.Mem (name, t) | Imported { modul_name; name; assigned_name; typ } -> let typ = Text.Import.Type.Mem (assigned_name, typ) in Import { modul_name; name; typ } ) mem - |> Array.to_list + |> Iarray.to_list let from_func func : Text.Module.Field.t list = - Array.map + Iarray.map (function | Origin.Local (func : Binary.Func.t) -> let type_f = convert_block_type func.type_f in @@ -244,28 +245,28 @@ let from_func func : Text.Module.Field.t list = let typ = Text.Import.Type.Func (assigned_name, typ) in Text.Module.Field.Import { modul_name; name; typ } ) func - |> Array.to_list + |> Iarray.to_list let from_elem elem : Text.Module.Field.t list = - Array.map + Iarray.map (fun (elem : Binary.Elem.t) -> let elem = convert_elem elem in Text.Module.Field.Elem elem ) elem - |> Array.to_list + |> Iarray.to_list let from_data data : Text.Module.Field.t list = - Array.map + Iarray.map (fun (data : Binary.Data.t) -> let data = convert_data data in Text.Module.Field.Data data ) data - |> Array.to_list + |> Iarray.to_list let from_exports (exports : Binary.Module.Exports.t) : Text.Module.Field.t list = let global = - Array.map + Iarray.map (fun ({ name; id } : Binary.Export.t) -> let id = Some (Text.Raw id) in Text.Module.Field.Export { name; typ = Global id } ) @@ -273,7 +274,7 @@ let from_exports (exports : Binary.Module.Exports.t) : Text.Module.Field.t list in let mem = - Array.map + Iarray.map (fun ({ name; id } : Binary.Export.t) -> let id = Some (Text.Raw id) in Text.Module.Field.Export { name; typ = Mem id } ) @@ -281,7 +282,7 @@ let from_exports (exports : Binary.Module.Exports.t) : Text.Module.Field.t list in let table = - Array.map + Iarray.map (fun ({ name; id } : Binary.Export.t) -> let id = Some (Text.Raw id) in Text.Module.Field.Export { name; typ = Table id } ) @@ -289,15 +290,15 @@ let from_exports (exports : Binary.Module.Exports.t) : Text.Module.Field.t list in let func = - Array.map + Iarray.map (fun ({ name; id } : Binary.Export.t) -> let id = Some (Text.Raw id) in Text.Module.Field.Export { name; typ = Func id } ) exports.func in - Array.to_list global @ Array.to_list mem @ Array.to_list table - @ Array.to_list func + Iarray.to_list global @ Iarray.to_list mem @ Iarray.to_list table + @ Iarray.to_list func let from_start = function | None -> [] diff --git a/src/compile/grouped.ml b/src/compile/grouped.ml index c12bbb7e1..7399aed7f 100644 --- a/src/compile/grouped.ml +++ b/src/compile/grouped.ml @@ -14,57 +14,59 @@ let curr_id (curr : int) (i : indice option) = type t = { id : string option - ; typ : Typedef.t Array.t - ; function_type : func_type Array.t + ; typ : Typedef.t Iarray.t + ; function_type : func_type Iarray.t (** Types comming from function declarations. It contains potential duplication. *) - ; type_checks : (indice * func_type) Array.t + ; type_checks : (indice * func_type) Iarray.t (** Types checks to perform after assignment. Come from function declarations with type indicies. *) - ; global : (Text.Global.t, Global.Type.t) Origin.t Array.t - ; table : (Table.t, Table.Type.t) Origin.t Array.t - ; mem : (Mem.t, limits) Origin.t Array.t - ; func : (Func.t, block_type) Origin.t Array.t - ; elem : Text.Elem.t Array.t - ; data : Text.Data.t Array.t - ; global_exports : opt_export Array.t - ; mem_exports : opt_export Array.t - ; table_exports : opt_export Array.t - ; func_exports : opt_export Array.t + ; global : (Text.Global.t, Global.Type.t) Origin.t Iarray.t + ; table : (Table.t, Table.Type.t) Origin.t Iarray.t + ; mem : (Mem.t, limits) Origin.t Iarray.t + ; func : (Func.t, block_type) Origin.t Iarray.t + ; elem : Text.Elem.t Iarray.t + ; data : Text.Data.t Iarray.t + ; global_exports : opt_export Iarray.t + ; mem_exports : opt_export Iarray.t + ; table_exports : opt_export Iarray.t + ; func_exports : opt_export Iarray.t ; start : indice option } let pp_id fmt id = Text.pp_id_opt fmt id -let pp_typ fmt typ = Fmt.array Text.Typedef.pp fmt typ +let pp_typ fmt typ = Fmt.iter Iarray.iter Text.Typedef.pp fmt typ let pp_function_type fmt function_type = - Fmt.array Text.pp_func_type fmt function_type + Fmt.iter Iarray.iter Text.pp_func_type fmt function_type let pp_type_check fmt (indice, func_type) = Fmt.pf fmt "(%a, %a)" pp_indice indice pp_func_type func_type -let pp_type_checks fmt type_checks = Fmt.array pp_type_check fmt type_checks +let pp_type_checks fmt type_checks = + Fmt.iter Iarray.iter pp_type_check fmt type_checks -let pp_runtime_array ~pp_local ~pp_imported fmt l = - Fmt.array (Origin.pp ~pp_local ~pp_imported) fmt l +let pp_runtime_iarray ~pp_local ~pp_imported fmt l = + Fmt.iter Iarray.iter (Origin.pp ~pp_local ~pp_imported) fmt l let pp_global fmt g = - pp_runtime_array ~pp_local:Text.Global.pp ~pp_imported:Text.Global.Type.pp fmt - g + pp_runtime_iarray ~pp_local:Text.Global.pp ~pp_imported:Text.Global.Type.pp + fmt g let pp_table fmt t = - pp_runtime_array ~pp_local:Text.Table.pp ~pp_imported:Text.Table.Type.pp fmt t + pp_runtime_iarray ~pp_local:Text.Table.pp ~pp_imported:Text.Table.Type.pp fmt + t let pp_mem fmt m = - pp_runtime_array ~pp_local:Text.Mem.pp ~pp_imported:Text.pp_limits fmt m + pp_runtime_iarray ~pp_local:Text.Mem.pp ~pp_imported:Text.pp_limits fmt m let pp_func fmt f = - pp_runtime_array ~pp_local:Text.Func.pp ~pp_imported:Text.pp_block_type fmt f + pp_runtime_iarray ~pp_local:Text.Func.pp ~pp_imported:Text.pp_block_type fmt f -let pp_elem fmt e = Fmt.array Text.Elem.pp fmt e +let pp_elem fmt e = Fmt.iter Iarray.iter Text.Elem.pp fmt e -let pp_data fmt d = Fmt.array Text.Data.pp fmt d +let pp_data fmt d = Fmt.iter Iarray.iter Text.Data.pp fmt d let pp_start fmt s = Text.pp_indice_opt fmt s @@ -205,21 +207,22 @@ let of_text { Text.Module.fields; id } = (add_field typ function_type type_checks global table mem func elem data global_exports mem_exports table_exports func_exports start ) fields; + let freeze_dynarray a = Dynarray.to_array a |> Iarray.of_array in let modul = { id - ; typ = Dynarray.to_array typ - ; function_type = Dynarray.to_array function_type - ; type_checks = Dynarray.to_array type_checks - ; global = Dynarray.to_array global - ; table = Dynarray.to_array table - ; mem = Dynarray.to_array mem - ; func = Dynarray.to_array func - ; elem = Dynarray.to_array elem - ; data = Dynarray.to_array data - ; global_exports = Dynarray.to_array global_exports - ; mem_exports = Dynarray.to_array mem_exports - ; table_exports = Dynarray.to_array table_exports - ; func_exports = Dynarray.to_array func_exports + ; typ = freeze_dynarray typ + ; function_type = freeze_dynarray function_type + ; type_checks = freeze_dynarray type_checks + ; global = freeze_dynarray global + ; table = freeze_dynarray table + ; mem = freeze_dynarray mem + ; func = freeze_dynarray func + ; elem = freeze_dynarray elem + ; data = freeze_dynarray data + ; global_exports = freeze_dynarray global_exports + ; mem_exports = freeze_dynarray mem_exports + ; table_exports = freeze_dynarray table_exports + ; func_exports = freeze_dynarray func_exports ; start = !start } in diff --git a/src/compile/grouped.mli b/src/compile/grouped.mli index 6228ca794..03f146fb5 100644 --- a/src/compile/grouped.mli +++ b/src/compile/grouped.mli @@ -11,23 +11,23 @@ type opt_export = private type t = private { id : string option - ; typ : Typedef.t Array.t - ; function_type : func_type Array.t + ; typ : Typedef.t Iarray.t + ; function_type : func_type Iarray.t (* Types comming from function declarations. It contains potential duplication *) - ; type_checks : (indice * func_type) Array.t + ; type_checks : (indice * func_type) Iarray.t (* Types checks to perform after assignment. Come from function declarations with type indicies *) - ; global : (Global.t, Global.Type.t) Origin.t Array.t - ; table : (Table.t, Table.Type.t) Origin.t Array.t - ; mem : (Mem.t, limits) Origin.t Array.t - ; func : (Func.t, block_type) Origin.t Array.t - ; elem : Elem.t Array.t - ; data : Data.t Array.t - ; global_exports : opt_export Array.t - ; mem_exports : opt_export Array.t - ; table_exports : opt_export Array.t - ; func_exports : opt_export Array.t + ; global : (Global.t, Global.Type.t) Origin.t Iarray.t + ; table : (Table.t, Table.Type.t) Origin.t Iarray.t + ; mem : (Mem.t, limits) Origin.t Iarray.t + ; func : (Func.t, block_type) Origin.t Iarray.t + ; elem : Elem.t Iarray.t + ; data : Data.t Iarray.t + ; global_exports : opt_export Iarray.t + ; mem_exports : opt_export Iarray.t + ; table_exports : opt_export Iarray.t + ; func_exports : opt_export Iarray.t ; start : indice option } diff --git a/src/compile/rewrite.ml b/src/compile/rewrite.ml index bc65b5c2f..6f9552f1b 100644 --- a/src/compile/rewrite.ml +++ b/src/compile/rewrite.ml @@ -80,7 +80,7 @@ let rewrite_expr (assigned : Assigned.t) (locals : Text.param list) match instr.Annotated.raw with | Br_table (ids, id) -> let block_id_to_raw = block_id_to_raw (loop_count, block_ids) in - let* ids = array_map block_id_to_raw ids in + let* ids = iarray_map block_id_to_raw ids in let+ id = block_id_to_raw id in Binary.Br_table (ids, id) | Br_if id -> @@ -302,9 +302,9 @@ let rewrite_data (assigned : Assigned.t) (data : Text.Data.t) : in { Binary.Data.mode; id = data.id; init = data.init } -let rewrite_export find assigned (exports : Grouped.opt_export Array.t) : - Binary.Export.t Array.t Result.t = - array_map +let rewrite_export find assigned (exports : Grouped.opt_export Iarray.t) : + Binary.Export.t Iarray.t Result.t = + iarray_map (fun { Grouped.name; id } -> match find assigned id with | Error _ -> Error (`Unknown_export id) @@ -337,21 +337,21 @@ let modul (modul : Grouped.t) (assigned : Assigned.t) : Binary.Module.t Result.t = Log.debug (fun m -> m "rewriting ..."); let* global = - array_map + iarray_map (Origin.monadic_map ~f_local:(rewrite_global assigned) ~f_imported:Result.ok ) modul.global in - let* elem = array_map (rewrite_elem assigned) modul.elem in - let* data = array_map (rewrite_data assigned) modul.data in + let* elem = iarray_map (rewrite_elem assigned) modul.elem in + let* data = iarray_map (rewrite_data assigned) modul.data in let* exports = rewrite_exports modul assigned in let* func = let f_imported = rewrite_block_type assigned in let f_local = rewrite_func assigned in let runtime = Origin.monadic_map ~f_local ~f_imported in - array_map runtime modul.func + iarray_map runtime modul.func in - let* types = array_map rewrite_types (Assigned.get_types assigned) in + let* types = iarray_map rewrite_types (Assigned.get_types assigned) in let+ start = match modul.start with | None -> Ok None diff --git a/src/concrete/concrete_elem.ml b/src/concrete/concrete_elem.ml index 21fbefbd8..7cd191647 100644 --- a/src/concrete/concrete_elem.ml +++ b/src/concrete/concrete_elem.ml @@ -2,10 +2,10 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -type t = { mutable value : Concrete_ref.t array } +type t = { mutable value : Concrete_ref.t Iarray.t } -let get (e : t) i = e.value.(i) +let get (e : t) i = Iarray.get e.value i -let size (e : t) = Array.length e.value +let size (e : t) = Iarray.length e.value let drop (e : t) = e.value <- [||] diff --git a/src/concrete/concrete_elem.mli b/src/concrete/concrete_elem.mli index 5289ee264..84ee6eeff 100644 --- a/src/concrete/concrete_elem.mli +++ b/src/concrete/concrete_elem.mli @@ -3,6 +3,6 @@ (* Written by the Owi programmers *) (* TODO: make it opaque *) -type t = { mutable value : Concrete_ref.t array } +type t = { mutable value : Concrete_ref.t Iarray.t } include Elem_intf.T with type reference := Concrete_ref.t and type t := t diff --git a/src/data_structures/priority_queue.ml b/src/data_structures/priority_queue.ml deleted file mode 100644 index 48c01a8aa..000000000 --- a/src/data_structures/priority_queue.ml +++ /dev/null @@ -1,56 +0,0 @@ -module Make (Prio : Map.OrderedType) = struct - type 'a t = (Prio.t * 'a) Dynarray.t - - let empty = Dynarray.create - - let is_empty h = Dynarray.length h = 0 - - let rec move_up (h : 'a t) x i = - if i = 0 then Dynarray.set h i x - else - let fi = (i - 1) / 2 in - let y = Dynarray.get h fi in - if Prio.compare (fst y) (fst x) > 0 then begin - Dynarray.set h i y; - move_up h x fi - end - else Dynarray.set h i x - - let push x h = - let n = Dynarray.length h in - Dynarray.add_last h x; - move_up h x n - - let min (h : 'a t) l r = - let xr = Dynarray.get h r in - let xl = Dynarray.get h l in - if Prio.compare (fst xr) (fst xl) < 0 then r else l - - let smallest_node h x i = - let l = (2 * i) + 1 in - let n = Dynarray.length h in - if l >= n then i - else - let r = l + 1 in - let j = if r < n then min h l r else l in - if Prio.compare (fst (Dynarray.get h j)) (fst x) < 0 then j else i - - let rec move_down h x i = - let j = smallest_node h x i in - if j = i then Dynarray.set h i x - else begin - Dynarray.set h i (Dynarray.get h j); - move_down h x j - end - - let pop h = - let n = Dynarray.length h in - if n = 0 then None - else - let y = Dynarray.get h 0 in - match Dynarray.pop_last_opt h with - | None -> None - | Some x -> - if n > 1 then move_down h x 0; - Some (snd y) -end diff --git a/src/data_structures/priority_queue.mli b/src/data_structures/priority_queue.mli deleted file mode 100644 index 23f33cdd3..000000000 --- a/src/data_structures/priority_queue.mli +++ /dev/null @@ -1,15 +0,0 @@ -module Make (Prio : sig - type t - - val compare : t -> t -> int -end) : sig - type 'a t - - val empty : unit -> 'a t - - val is_empty : 'a t -> bool - - val pop : 'a t -> 'a option - - val push : Prio.t * 'a -> 'a t -> unit -end diff --git a/src/data_structures/stack.ml b/src/data_structures/stack.ml index d82fd5824..7f91e8540 100644 --- a/src/data_structures/stack.ml +++ b/src/data_structures/stack.ml @@ -92,8 +92,6 @@ module type S = sig val push_concrete_v128 : t -> Concrete_v128.t -> t val push_ref : t -> ref_value -> t - - val push_array : t -> unit Array.t -> t end module Make (Value : Value_intf.T) : @@ -143,8 +141,6 @@ module Make (Value : Value_intf.T) : let push_ref s r = push s (Ref r) - let push_array _ _ = assert false - let pp fmt (s : t) = Fmt.list ~sep:(fun fmt () -> Fmt.string fmt " ; ") Value.pp fmt s diff --git a/src/dune b/src/dune index cc6c0f325..ac85529e0 100644 --- a/src/dune +++ b/src/dune @@ -84,7 +84,6 @@ owi parse prio - priority_queue ref_intf result rewrite diff --git a/src/exploration/prio.ml b/src/exploration/prio.ml index e1319715f..e3a8aca9f 100644 --- a/src/exploration/prio.ml +++ b/src/exploration/prio.ml @@ -267,8 +267,12 @@ module type S = sig val work_while : ('a -> (metrics * 'a -> unit) -> unit) -> 'a t -> unit end -module Make (P : T) : S = struct - module Priority_queue = Priority_queue.Make (P) +module Make (Prio : T) : S = struct + module Pqueue = Pqueue.MakeMaxPoly (struct + type 'a t = Prio.t * 'a + + let compare (p1, _) (p2, _) = Prio.compare p1 p2 + end) type 'a t = ('a, metrics * 'a) Synchronizer.t @@ -291,12 +295,12 @@ module Make (P : T) : S = struct let close = Synchronizer.close let writter (prio, v) q = - let prio = P.of_metrics prio in + let prio = Prio.of_metrics prio in let prio_and_value = (prio, v) in - Priority_queue.push prio_and_value q + Pqueue.add q prio_and_value let make () = - let q = Priority_queue.empty () in + let q = Pqueue.create () in let writter prio_and_value = writter prio_and_value q in - Synchronizer.init (fun () -> Priority_queue.pop q) writter + Synchronizer.init (fun () -> Pqueue.pop_max q |> Option.map snd) writter end diff --git a/src/infra/syntax.ml b/src/infra/syntax.ml index e90e71925..567994c4c 100644 --- a/src/infra/syntax.ml +++ b/src/infra/syntax.ml @@ -3,12 +3,7 @@ (* Written by the Owi programmers *) open Prelude.Result - -let[@inline] ( let* ) o f = match o with Ok v -> f v | Error _ as e -> e - -let[@inline] ( let+ ) o f = match o with Ok v -> Ok (f v) | Error _ as e -> e - -let[@inline] ok v = Ok v +include Syntax let[@inline] list_iter f l = let rec aux = function @@ -53,24 +48,11 @@ let[@inline] list_fold_left_map f acc l = in (acc, List.rev l) -let[@inline] array_iter f a = - let err = ref None in - try - for i = 0 to Array.length a - 1 do - match f (Array.unsafe_get a i) with - | Error _e as e -> - err := Some e; - raise Exit - | Ok () -> () - done; - Ok () - with Exit -> ( match !err with None -> assert false | Some e -> e ) - -let[@inline] array_iteri f a = +let[@inline] iarray_iter f a = let err = ref None in try - for i = 0 to Array.length a - 1 do - match f i (Array.unsafe_get a i) with + for i = 0 to Iarray.length a - 1 do + match f (Iarray.unsafe_get a i) with | Error _e as e -> err := Some e; raise Exit @@ -79,11 +61,11 @@ let[@inline] array_iteri f a = Ok () with Exit -> ( match !err with None -> assert false | Some e -> e ) -let[@inline] dynarray_iter f a = +let[@inline] iarray_iteri f a = let err = ref None in try - for i = 0 to Dynarray.length a - 1 do - match f (Dynarray.get a i) with + for i = 0 to Iarray.length a - 1 do + match f i (Iarray.unsafe_get a i) with | Error _e as e -> err := Some e; raise Exit @@ -92,25 +74,12 @@ let[@inline] dynarray_iter f a = Ok () with Exit -> ( match !err with None -> assert false | Some e -> e ) -let[@inline] dynarray_iteri f a = - let err = ref None in - try - for i = 0 to Dynarray.length a - 1 do - match f i (Dynarray.get a i) with - | Error _e as e -> - err := Some e; - raise Exit - | Ok () -> () - done; - Ok () - with Exit -> ( match !err with None -> assert false | Some e -> e ) - -let[@inline] array_map f a = +let[@inline] iarray_map f a = let err = ref None in try ok - @@ Array.init (Array.length a) (fun i -> - let v = Array.get a i in + @@ Iarray.init (Iarray.length a) (fun i -> + let v = Iarray.get a i in match f v with | Error _e as e -> err := Some e; @@ -118,38 +87,9 @@ let[@inline] array_map f a = | Ok v -> v ) with Exit -> ( match !err with None -> assert false | Some e -> e ) -let[@inline] dynarray_map f a = - let err = ref None in - try - ok - @@ Dynarray.init (Dynarray.length a) (fun i -> - let v = Dynarray.get a i in - match f v with - | Error _e as e -> - err := Some e; - raise Exit - | Ok v -> v ) - with Exit -> ( match !err with None -> assert false | Some e -> e ) - -let[@inline] array_fold_left f acc l = - Array.fold_left +let[@inline] iarray_fold_left f acc l = + Iarray.fold_left (fun acc v -> let* acc in f acc v ) (Ok acc) l - -let[@inline] dynarray_fold_left f acc l = - Dynarray.fold_left - (fun acc v -> - let* acc in - f acc v ) - (Ok acc) l - -let[@inline] dynarray_fold_lefti f acc l = - snd - @@ Dynarray.fold_left - (fun (i, acc) v -> - ( succ i - , let* acc in - f i acc v ) ) - (0, Ok acc) l diff --git a/src/infra/syntax.mli b/src/infra/syntax.mli index c3c969579..7c7096e76 100644 --- a/src/infra/syntax.mli +++ b/src/infra/syntax.mli @@ -10,8 +10,6 @@ val ( let* ) : val ( let+ ) : ('a, 'err) Prelude.Result.t -> ('a -> 'b) -> ('b, 'err) Prelude.Result.t -val ok : 'a -> ('a, 'err) Prelude.Result.t - val list_iter : ('a -> (unit, 'err) Prelude.Result.t) -> 'a list @@ -39,50 +37,23 @@ val list_fold_left_map : -> 'b list -> ('a * 'c list, 'err) Prelude.Result.t -val array_iter : - ('a -> (unit, 'err) Prelude.Result.t) - -> 'a array - -> (unit, 'err) Prelude.Result.t - -val array_iteri : - (int -> 'a -> (unit, 'err) Prelude.Result.t) - -> 'a array - -> (unit, 'err) Prelude.Result.t - -val dynarray_iter : +val iarray_iter : ('a -> (unit, 'err) Prelude.Result.t) - -> 'a Dynarray.t + -> 'a Iarray.t -> (unit, 'err) Prelude.Result.t -val dynarray_iteri : +val iarray_iteri : (int -> 'a -> (unit, 'err) Prelude.Result.t) - -> 'a Dynarray.t + -> 'a Iarray.t -> (unit, 'err) Prelude.Result.t -val array_map : - ('a -> ('b, 'err) Prelude.Result.t) - -> 'a array - -> ('b array, 'err) Prelude.Result.t - -val dynarray_map : +val iarray_map : ('a -> ('b, 'err) Prelude.Result.t) - -> 'a Dynarray.t - -> ('b Dynarray.t, 'err) Prelude.Result.t - -val array_fold_left : - ('a -> 'b -> ('a, 'err) Prelude.Result.t) - -> 'a - -> 'b array - -> ('a, 'err) Prelude.Result.t + -> 'a Iarray.t + -> ('b Iarray.t, 'err) Prelude.Result.t -val dynarray_fold_left : +val iarray_fold_left : ('a -> 'b -> ('a, 'err) Prelude.Result.t) -> 'a - -> 'b Dynarray.t - -> ('a, 'err) Prelude.Result.t - -val dynarray_fold_lefti : - (int -> 'a -> 'b -> ('a, 'err) Prelude.Result.t) - -> 'a - -> 'b Dynarray.t + -> 'b Iarray.t -> ('a, 'err) Prelude.Result.t diff --git a/src/instrument/label.ml b/src/instrument/label.ml index ff15b18b2..f5a503973 100644 --- a/src/instrument/label.ml +++ b/src/instrument/label.ml @@ -27,7 +27,7 @@ let annotate_fc m cov_label_set_idx = let count = ref ~-1 in let func = m.Binary.Module.func in let func = - Array.map + Iarray.map (function | Origin.Imported _ as v -> (* TODO: should we write a wrapper for the imported function so that it gets counted in FC? *) @@ -54,7 +54,7 @@ let annotate_sc m cov_label_set_idx = let count = ref ~-1 in let func = m.Binary.Module.func in let func = - Array.map + Iarray.map (function | Origin.Imported _ as v -> (* TODO: should we write a wrapper for the imported function so that it gets counted in FC? *) @@ -103,7 +103,7 @@ let annotate_dc m cov_label_set_idx = let count = ref ~-1 in let func = m.Binary.Module.func in let func = - Array.map + Iarray.map (function | Origin.Imported _ as v -> v | Origin.Local f -> diff --git a/src/interpret/interpret.ml b/src/interpret/interpret.ml index 52f63f42c..93f56b40c 100644 --- a/src/interpret/interpret.ml +++ b/src/interpret/interpret.ml @@ -648,6 +648,7 @@ struct val set : t -> int -> value -> t end = struct + (* TODO: is this really the good datastructure for this...? *) type t = value array let of_list = Array.of_list @@ -1590,13 +1591,13 @@ struct st stack | Br_table (inds, i) -> let target, stack = Stack.pop_i32 stack in - let> out = I32.(ge_u target (I32.of_int (Array.length inds))) in + let> out = I32.(ge_u target (I32.of_int (Iarray.length inds))) in let* target = if out then return i else let+ target = Choice.select_i32 target in let target = Int32.to_int target in - inds.(target) + Iarray.get inds target in let state = { state with stack } in State.branch state target diff --git a/src/ir/binary.ml b/src/ir/binary.ml index ef34f8fff..dc2b8697e 100644 --- a/src/ir/binary.ml +++ b/src/ir/binary.ml @@ -116,7 +116,7 @@ type instr = string option * block_type option * expr Annotated.t * expr Annotated.t | Br of indice | Br_if of indice - | Br_table of indice array * indice + | Br_table of indice Iarray.t * indice | Return | Return_call of indice | Return_call_indirect of indice * block_type @@ -249,7 +249,9 @@ let rec pp_instr ~short fmt = function | Br id -> pf fmt "br %a" pp_indice id | Br_if id -> pf fmt "br_if %a" pp_indice id | Br_table (ids, id) -> - pf fmt "br_table %a %a" (array ~sep:sp pp_indice) ids pp_indice id + pf fmt "br_table %a %a" + (iter Iarray.iter ~sep:sp pp_indice) + ids pp_indice id | Return -> pf fmt "return" | Return_call id -> pf fmt "return_call %a" pp_indice id | Return_call_indirect (tbl_id, ty_id) -> @@ -391,22 +393,23 @@ end module Module = struct module Exports = struct type t = - { global : Export.t Array.t - ; mem : Export.t Array.t - ; table : Export.t Array.t - ; func : Export.t Array.t + { global : Export.t Iarray.t + ; mem : Export.t Iarray.t + ; table : Export.t Iarray.t + ; func : Export.t Iarray.t } end type t = { id : string option - ; types : Text.Typedef.t array - ; global : (Global.t, Text.Global.Type.t) Origin.t array - ; table : (Text.Table.t, Text.Table.Type.t) Origin.t array - ; mem : (Text.Mem.t, Text.limits) Origin.t array - ; func : (Func.t, block_type) Origin.t array (* TODO: switch to func_type *) - ; elem : Elem.t array - ; data : Data.t array + ; types : Text.Typedef.t Iarray.t + ; global : (Global.t, Text.Global.Type.t) Origin.t Iarray.t + ; table : (Text.Table.t, Text.Table.Type.t) Origin.t Iarray.t + ; mem : (Text.Mem.t, Text.limits) Origin.t Iarray.t + ; func : + (Func.t, block_type) Origin.t Iarray.t (* TODO: switch to func_type *) + ; elem : Elem.t Iarray.t + ; data : Data.t Iarray.t ; exports : Exports.t ; start : int option ; custom : Custom.t list @@ -468,23 +471,23 @@ module Module = struct Origin.Local { f with body } in let func = - Array.init - (Array.length m.func + 1) + Iarray.init + (Iarray.length m.func + 1) (fun j -> if i = j then if update_function_itself then update_function f else f else begin - update_function @@ if i < j then m.func.(j - 1) else m.func.(j) + update_function @@ Iarray.get m.func (if i < j then j - 1 else j) end ) in let elem = - Array.map + Iarray.map (fun (elem : Elem.t) -> let init = List.map handle_expr elem.init in { elem with init } ) m.elem in let global = - Array.map + Iarray.map (function | Origin.Imported _ as v -> v | Local (global : Global.t) -> @@ -497,7 +500,7 @@ module Module = struct let exports = let func = - Array.map + Iarray.map (fun export -> let id = update_idx (export : Export.t).id in { export with id } ) @@ -511,20 +514,20 @@ module Module = struct (** Add a function [f] at the end of a module [m] and returns the module and the index of the added function. *) let add_func f m = - let len = Array.length m.func in + let len = Iarray.length m.func in let func = - Array.init - (Array.length m.func + 1) - (fun i -> if i = len then f else m.func.(i)) + Iarray.init + (Iarray.length m.func + 1) + (fun i -> if i = len then f else Iarray.get m.func i) in ({ m with func }, len) (** Return the type of the function at index [id]. *) let get_func_type id m = - if id >= Array.length m.func then None + if id >= Iarray.length m.func then None else - match m.func.(id) with + match Iarray.get m.func id with | Local f -> Some f.type_f | Imported i -> Some i.typ @@ -533,7 +536,7 @@ module Module = struct (** Return the first function exported as [name] if it exists. Return [None] otherwise.*) let find_exported_func_from_name name m = - Array.find_opt + Iarray.find_opt (function { Export.name = name'; _ } -> String.equal name name') m.exports.func @@ -542,7 +545,7 @@ module Module = struct (** Return the index of a function imported from a given [modul_name] and [func_name] if it exists. Return [None] otherwise. *) let find_imported_func_index ~modul_name ~func_name m = - Array.find_index + Iarray.find_index (function | Origin.Imported { Origin.modul_name = modul_name' @@ -558,7 +561,7 @@ module Module = struct no imported functions. *) let find_last_import_index m = let _i, last = - Array.fold_left + Iarray.fold_left (fun (i, last) -> function | Origin.Imported _ -> (succ i, i) | Origin.Local _ -> (succ i, last) ) (0, ~-1) m.func diff --git a/src/ir/binary.mli b/src/ir/binary.mli index 6578cf846..f6cbdbe42 100644 --- a/src/ir/binary.mli +++ b/src/ir/binary.mli @@ -87,7 +87,7 @@ type instr = string option * block_type option * expr Annotated.t * expr Annotated.t | Br of indice | Br_if of indice - | Br_table of indice array * indice + | Br_table of indice Iarray.t * indice | Return | Return_call of indice | Return_call_indirect of indice * block_type @@ -168,22 +168,23 @@ end module Module : sig module Exports : sig type t = - { global : Export.t Array.t - ; mem : Export.t Array.t - ; table : Export.t Array.t - ; func : Export.t Array.t + { global : Export.t Iarray.t + ; mem : Export.t Iarray.t + ; table : Export.t Iarray.t + ; func : Export.t Iarray.t } end type t = { id : string option - ; types : Text.Typedef.t array - ; global : (Global.t, Text.Global.Type.t) Origin.t array - ; table : (Text.Table.t, Text.Table.Type.t) Origin.t array - ; mem : (Text.Mem.t, Text.limits) Origin.t array - ; func : (Func.t, block_type) Origin.t array (* TODO: switch to func_type *) - ; elem : Elem.t array - ; data : Data.t array + ; types : Text.Typedef.t Iarray.t + ; global : (Global.t, Text.Global.Type.t) Origin.t Iarray.t + ; table : (Text.Table.t, Text.Table.Type.t) Origin.t Iarray.t + ; mem : (Text.Mem.t, Text.limits) Origin.t Iarray.t + ; func : + (Func.t, block_type) Origin.t Iarray.t (* TODO: switch to func_type *) + ; elem : Elem.t Iarray.t + ; data : Data.t Iarray.t ; exports : Exports.t ; start : int option ; custom : Custom.t list diff --git a/src/ir/binary_encoder.ml b/src/ir/binary_encoder.ml index be32d3742..b4f5d4b9c 100644 --- a/src/ir/binary_encoder.ml +++ b/src/ir/binary_encoder.ml @@ -99,7 +99,7 @@ let encode_vector_list buf datas encode_func = encode_vector List.length List.iter buf datas encode_func let encode_vector_array buf datas encode_func = - encode_vector Array.length Array.iter buf datas encode_func + encode_vector Iarray.length Iarray.iter buf datas encode_func let write_resulttype buf (rt : Text.result_type) = encode_vector_list buf rt write_valtype @@ -680,18 +680,18 @@ let encode_globals buf globals = encode_vector_list buf globals write_global let encode_exports buf ({ global; mem; table; func } : Module.Exports.t) = let exp_buf = Buffer.create 16 in let len = - Array.length global + Array.length mem + Array.length table - + Array.length func + Iarray.length global + Iarray.length mem + Iarray.length table + + Iarray.length func in - let array_rev_iter f a = - for i = Array.length a - 1 downto 0 do - f a.(i) + let iarray_rev_iter f a = + for i = Iarray.length a - 1 downto 0 do + f @@ Iarray.get a i done in - array_rev_iter (write_export exp_buf '\x03') global; - array_rev_iter (write_export exp_buf '\x02') mem; - array_rev_iter (write_export exp_buf '\x01') table; - array_rev_iter (write_export exp_buf '\x00') func; + iarray_rev_iter (write_export exp_buf '\x03') global; + iarray_rev_iter (write_export exp_buf '\x02') mem; + iarray_rev_iter (write_export exp_buf '\x01') table; + iarray_rev_iter (write_export exp_buf '\x00') func; write_u32_of_int buf len; Buffer.add_buffer buf exp_buf @@ -704,7 +704,7 @@ let encode_elements buf elems = encode_vector_array buf elems write_element (* datacount: section 12 *) let encode_datacount buf datas = - let len = Array.length datas in + let len = Iarray.length datas in write_u32_of_int buf len (* code: section 10 *) @@ -722,12 +722,12 @@ let encode_datas buf datas = encode_vector_array buf datas write_data let keep_local values = List.filter_map (function Origin.Local data -> Some data | Origin.Imported _data -> None) - (Array.to_list values) + (Iarray.to_list values) let keep_imported values = List.filter_map (function Origin.Local _data -> None | Origin.Imported data -> Some data) - (Array.to_list values) + (Iarray.to_list values) let encode ({ func; table; global; exports; start; data; mem; types; elem; _ } : diff --git a/src/ir/text.ml b/src/ir/text.ml index dd0bc6396..195207ee3 100644 --- a/src/ir/text.ml +++ b/src/ir/text.ml @@ -443,7 +443,7 @@ type instr = string option * block_type option * expr Annotated.t * expr Annotated.t | Br of indice | Br_if of indice - | Br_table of indice array * indice + | Br_table of indice Iarray.t * indice | Return | Return_call of indice | Return_call_indirect of indice * block_type @@ -569,7 +569,9 @@ let rec pp_instr ~short fmt = function | Br id -> pf fmt "br %a" pp_indice id | Br_if id -> pf fmt "br_if %a" pp_indice id | Br_table (ids, id) -> - pf fmt "br_table %a %a" (array ~sep:sp pp_indice) ids pp_indice id + pf fmt "br_table %a %a" + (iter Iarray.iter ~sep:sp pp_indice) + ids pp_indice id | Return -> pf fmt "return" | Return_call id -> pf fmt "return_call %a" pp_indice id | Return_call_indirect (tbl_id, ty_id) -> diff --git a/src/ir/text.mli b/src/ir/text.mli index d4ed7d070..8fdf15cbf 100644 --- a/src/ir/text.mli +++ b/src/ir/text.mli @@ -278,7 +278,7 @@ type instr = string option * block_type option * expr Annotated.t * expr Annotated.t | Br of indice | Br_if of indice - | Br_table of indice array * indice + | Br_table of indice Iarray.t * indice | Return | Return_call of indice | Return_call_indirect of indice * block_type diff --git a/src/link/link.ml b/src/link/link.ml index 02ae9088d..1eac122a2 100644 --- a/src/link/link.ml +++ b/src/link/link.ml @@ -105,20 +105,20 @@ module Eval_const = struct (* TODO: binary+const instr *) let instr env stack instr = match instr.Annotated.raw with - | Binary.I32_const n -> ok @@ Stack.push_i32 stack n - | I64_const n -> ok @@ Stack.push_i64 stack n - | F32_const f -> ok @@ Stack.push_f32 stack f - | F64_const f -> ok @@ Stack.push_f64 stack f - | V128_const f -> ok @@ Stack.push_v128 stack f - | I_binop (nn, op) -> ok @@ ibinop stack nn op - | Ref_null t -> ok @@ Stack.push_ref stack (Concrete_ref.null t) + | Binary.I32_const n -> Result.ok @@ Stack.push_i32 stack n + | I64_const n -> Result.ok @@ Stack.push_i64 stack n + | F32_const f -> Result.ok @@ Stack.push_f32 stack f + | F64_const f -> Result.ok @@ Stack.push_f64 stack f + | V128_const f -> Result.ok @@ Stack.push_v128 stack f + | I_binop (nn, op) -> Result.ok @@ ibinop stack nn op + | Ref_null t -> Result.ok @@ Stack.push_ref stack (Concrete_ref.null t) | Ref_func f -> let* f = Link_env.Build.get_func env f in let value = Concrete_value.Ref (Func (Some f)) in - ok @@ Stack.push stack value + Result.ok @@ Stack.push stack value | Global_get id -> let* g = Link_env.Build.get_const_global env id in - ok @@ Stack.push stack g + Result.ok @@ Stack.push stack g | _ -> assert false (* TODO: binary+const expr *) @@ -143,7 +143,7 @@ let eval_global ls env (global : (Binary.Global.t, Text.Global.Type.t) Origin.t) let eval_globals ls env globals : Link_env.Build.t Result.t = let+ env, _i = - array_fold_left + iarray_fold_left (fun (env, i) global -> let+ global = eval_global ls env global in let env = Link_env.Build.add_global i global env in @@ -173,12 +173,12 @@ let load_memory (ls : 'f State.t) (import : Text.limits Origin.imported) : let eval_memory ls (memory : (Text.Mem.t, Text.limits) Origin.t) : Concrete_memory.t Result.t = match memory with - | Local (_label, mem_type) -> ok @@ Concrete_memory.init mem_type + | Local (_label, mem_type) -> Result.ok @@ Concrete_memory.init mem_type | Imported import -> load_memory ls import let eval_memories ls env memories = let+ env, _i = - array_fold_left + iarray_fold_left (fun (env, id) mem -> let+ memory = eval_memory ls mem in let env = Link_env.Build.add_memory id memory env in @@ -201,12 +201,13 @@ let load_table (ls : 'f State.t) (import : Text.Table.Type.t Origin.imported) : let eval_table ls (table : (_, Text.Table.Type.t) Origin.t) : table Result.t = match table with - | Local (label, table_type) -> ok @@ Concrete_table.init ?label table_type + | Local (label, table_type) -> + Result.ok @@ Concrete_table.init ?label table_type | Imported import -> load_table ls import let eval_tables ls env tables = let+ env, _i = - array_fold_left + iarray_fold_left (fun (env, i) table -> let+ table = eval_table ls table in let env = Link_env.Build.add_table i table env in @@ -240,12 +241,12 @@ let load_func (ls : 'f State.t) (import : Binary.block_type Origin.imported) : let eval_func ls (finished_env : int) func : func Result.t = match func with - | Origin.Local func -> ok @@ Kind.wasm func finished_env + | Origin.Local func -> Result.ok @@ Kind.wasm func finished_env | Imported import -> load_func ls import let eval_functions ls (finished_env : int) env functions = let+ env, _i = - array_fold_left + iarray_fold_left (fun (env, i) func -> let+ func = eval_func ls finished_env func in let env = Link_env.Build.add_func i func env in @@ -280,7 +281,7 @@ let get_i32 = function let define_data env data = let+ env, init, _i = - array_fold_left + iarray_fold_left (fun (env, init, id) (data : Binary.Data.t) -> let data' : Concrete_data.t = { value = data.init } in let env = Link_env.Build.add_data id data' env in @@ -291,7 +292,7 @@ let define_data env data = let length = Int32.of_int @@ String.length data.init in let* offset = get_i32 offset in let* v = active_data_expr env ~offset ~length ~mem ~data:id in - ok @@ (v :: init) + Result.ok @@ (v :: init) | Passive -> Ok init in (env, init, succ id) ) @@ -301,7 +302,7 @@ let define_data env data = let define_elem env elem = let+ env, inits, _i = - array_fold_left + iarray_fold_left (fun (env, inits, i) (elem : Binary.Elem.t) -> let* init = list_map (Eval_const.expr env) elem.init in let* init_as_ref = @@ -313,7 +314,7 @@ let define_elem env elem = in let value = match elem.mode with - | Active _ | Passive -> Array.of_list init_as_ref + | Active _ | Passive -> Iarray.of_list init_as_ref | Declarative -> (* Declarative element have no runtime value *) [||] @@ -326,7 +327,8 @@ let define_elem env elem = let length = Int32.of_int @@ List.length init in let* offset = Eval_const.expr env offset in let* offset = get_i32 offset in - ok @@ (active_elem_expr ~offset ~length ~table ~elem:i :: inits) + Result.ok + @@ (active_elem_expr ~offset ~length ~table ~elem:i :: inits) | Passive | Declarative -> Ok inits in (env, inits, succ i) ) @@ -337,7 +339,7 @@ let define_elem env elem = let populate_exports env (exports : Binary.Module.Exports.t) : State.exports Result.t = let fill_exports get_env exports names = - array_fold_left + iarray_fold_left (fun (acc, names) ({ name; id; _ } : Binary.Export.t) -> let value = get_env env id in if StringSet.mem name names then Error `Duplicate_export_name @@ -345,7 +347,7 @@ let populate_exports env (exports : Binary.Module.Exports.t) : (StringMap.empty, names) exports in let fill_exports' get_env exports names = - array_fold_left + iarray_fold_left (fun (acc, names) ({ name; id; _ } : Binary.Export.t) -> let* value = get_env env id in if StringSet.mem name names then Error `Duplicate_export_name diff --git a/src/link/link_env.ml b/src/link/link_env.ml index 2e0c40311..ddc389633 100644 --- a/src/link/link_env.ml +++ b/src/link/link_env.ml @@ -91,7 +91,7 @@ module Build = struct let get_const_global (env : t) id = let* g = get_global env id in match g.mut with - | Const -> ok g.value + | Const -> Result.ok g.value | Var -> Error `Constant_expression_required let get_func (env : t) id = diff --git a/src/owi.mli b/src/owi.mli index 2d27a997b..91ad1e020 100644 --- a/src/owi.mli +++ b/src/owi.mli @@ -412,7 +412,7 @@ module Text : sig string option * block_type option * expr Annotated.t * expr Annotated.t | Br of indice | Br_if of indice - | Br_table of indice array * indice + | Br_table of indice Iarray.t * indice | Return | Return_call of indice | Return_call_indirect of indice * block_type @@ -653,7 +653,7 @@ module Binary : sig string option * block_type option * expr Annotated.t * expr Annotated.t | Br of indice | Br_if of indice - | Br_table of indice array * indice + | Br_table of indice Iarray.t * indice | Return | Return_call of indice | Return_call_indirect of indice * block_type @@ -734,23 +734,23 @@ module Binary : sig module Module : sig module Exports : sig type t = - { global : Export.t Array.t - ; mem : Export.t Array.t - ; table : Export.t Array.t - ; func : Export.t Array.t + { global : Export.t Iarray.t + ; mem : Export.t Iarray.t + ; table : Export.t Iarray.t + ; func : Export.t Iarray.t } end type t = { id : string option - ; types : Text.Typedef.t array - ; global : (Global.t, Text.Global.Type.t) Origin.t array - ; table : (Text.Table.t, Text.Table.Type.t) Origin.t array - ; mem : (Text.Mem.t, Text.limits) Origin.t array + ; types : Text.Typedef.t Iarray.t + ; global : (Global.t, Text.Global.Type.t) Origin.t Iarray.t + ; table : (Text.Table.t, Text.Table.Type.t) Origin.t Iarray.t + ; mem : (Text.Mem.t, Text.limits) Origin.t Iarray.t ; func : - (Func.t, block_type) Origin.t array (* TODO: switch to func_type *) - ; elem : Elem.t array - ; data : Data.t array + (Func.t, block_type) Origin.t Iarray.t (* TODO: switch to func_type *) + ; elem : Elem.t Iarray.t + ; data : Data.t Iarray.t ; exports : Exports.t ; start : int option ; custom : Custom.t list diff --git a/src/parser/binary_parser.ml b/src/parser/binary_parser.ml index 096713f22..3e23d5349 100644 --- a/src/parser/binary_parser.ml +++ b/src/parser/binary_parser.ml @@ -385,7 +385,9 @@ let block_type_of_type_def (_id, (pt, rt)) = let read_block_type types input = match read_S33 input with | Ok (i, input) when Int64.ge i 0L -> - let block_type = block_type_of_type_def types.(Int64.to_int i) in + let block_type = + block_type_of_type_def @@ Iarray.get types (Int64.to_int i) + in Ok (block_type, input) | Error _ | Ok _ -> begin match read_byte ~msg:"read_block_type" input with @@ -432,7 +434,7 @@ let rec read_instr types input = (Br_if labelidx, input) | '\x0E' -> let* xs, input = vector_no_id read_indice input in - let xs = Array.of_list xs in + let xs = Iarray.of_list xs in let+ x, input = read_indice input in (Br_table (xs, x), input) | '\x0F' -> Ok (Return, input) @@ -442,21 +444,23 @@ let rec read_instr types input = | '\x11' -> let* typeidx, input = read_indice input in let+ tableidx, input = read_indice input in - (Call_indirect (tableidx, block_type_of_type_def types.(typeidx)), input) + ( Call_indirect (tableidx, block_type_of_type_def (Iarray.get types typeidx)) + , input ) | '\x12' -> let+ funcidx, input = read_indice input in (Return_call funcidx, input) | '\x13' -> let* typeidx, input = read_indice input in let+ tableidx, input = read_indice input in - ( Return_call_indirect (tableidx, block_type_of_type_def types.(typeidx)) + ( Return_call_indirect + (tableidx, block_type_of_type_def (Iarray.get types typeidx)) , input ) | '\x14' -> let+ funcidx, input = read_indice input in (Call_ref funcidx, input) | '\x15' -> let+ typeidx, input = read_indice input in - (Return_call_ref (block_type_of_type_def types.(typeidx)), input) + (Return_call_ref (block_type_of_type_def (Iarray.get types typeidx)), input) | '\x1A' -> Ok (Drop, input) | '\x1B' -> Ok (Select None, input) | '\x1C' -> @@ -1017,7 +1021,7 @@ let sections_iterate (input : Input.t) = let* types, input = section_parse input ~expected_id:'\x01' [] (vector read_type) in - let types = Array.of_list types in + let types = Iarray.of_list types in (* Custom *) let* custom_sections', input = parse_many_custom_section input in @@ -1131,10 +1135,10 @@ let sections_iterate (input : Input.t) = section_parse input ~expected_id:'\x0B' [] (vector_no_id (read_data types)) in - let data = Array.of_list data in + let data = Iarray.of_list data in let* () = - match (Array.length data, data_count_section) with + match (Iarray.length data, data_count_section) with | 0, None -> Ok () | _data_len, None -> let code_use_dataidx = ref false in @@ -1174,7 +1178,7 @@ let sections_iterate (input : Input.t) = | _not_a_memory_import -> None ) import_section in - Array.of_list (imported @ local) + Iarray.of_list (imported @ local) in (* Globals *) @@ -1190,7 +1194,7 @@ let sections_iterate (input : Input.t) = | _not_a_global_import -> None ) import_section in - Array.of_list (imported @ local) + Iarray.of_list (imported @ local) in (* Functions *) @@ -1199,7 +1203,7 @@ let sections_iterate (input : Input.t) = List.map2 (fun typeidx (locals, body) -> Origin.Local - { Func.type_f = block_type_of_type_def types.(typeidx) + { Func.type_f = block_type_of_type_def (Iarray.get types typeidx) ; locals ; body ; id = None @@ -1210,13 +1214,13 @@ let sections_iterate (input : Input.t) = List.filter_map (function | modul_name, name, Func idx -> - let typ = block_type_of_type_def types.(idx) in + let typ = block_type_of_type_def (Iarray.get types idx) in Option.some @@ Origin.imported ~modul_name ~name ~assigned_name:None ~typ | _not_a_function_import -> None ) import_section in - Array.of_list (imported @ local) + Iarray.of_list (imported @ local) in (* Tables *) @@ -1232,11 +1236,11 @@ let sections_iterate (input : Input.t) = | _not_a_table_import -> None ) import_section in - Array.of_list (imported @ local) + Iarray.of_list (imported @ local) in (* Elems *) - let elem = Array.of_list element_section in + let elem = Iarray.of_list element_section in (* Exports *) (* We use an intermediate stack because the values are in reverse order *) @@ -1255,7 +1259,7 @@ let sections_iterate (input : Input.t) = | _ -> Fmt.failwith "read_exportdesc error" ) export_section; let stack_to_array s = - Array.init (Stack.length s) (fun _i -> + Iarray.init (Stack.length s) (fun _i -> match Stack.pop_opt s with Some v -> v | None -> assert false ) in let exports = diff --git a/src/parser/text_lexer.ml b/src/parser/text_lexer.ml index 8c7126d73..dbe5d1ef8 100644 --- a/src/parser/text_lexer.ml +++ b/src/parser/text_lexer.ml @@ -143,7 +143,7 @@ let annot_atom = let keywords = let tbl = Hashtbl.create 512 in - Array.iter + Iarray.iter (fun (k, v) -> Hashtbl.add tbl k v) [| ("align", ALIGN) ; ("any", ANY) diff --git a/src/parser/text_parser.mly b/src/parser/text_parser.mly index e7af778cf..3eed8f934 100644 --- a/src/parser/text_parser.mly +++ b/src/parser/text_parser.mly @@ -264,9 +264,9 @@ let plain_instr := | BR; ~ = indice;
| BR_IF; ~ = indice; | BR_TABLE; l = nonempty_list(indice); { - let xs = Array.of_list l in - let n = Array.length xs in - Br_table (Array.sub xs 0 (n - 1), xs.(n - 1)) + let xs = Iarray.of_list l in + let n = Iarray.length xs in + Br_table (Iarray.sub xs ~pos:0 ~len:(n - 1), Iarray.get xs (n - 1)) } | RETURN; { Return } | RETURN_CALL; ~ = indice; diff --git a/src/primitives/int32.ml b/src/primitives/int32.ml index de98c7fdc..20530b84d 100644 --- a/src/primitives/int32.ml +++ b/src/primitives/int32.ml @@ -68,20 +68,6 @@ let extend_s n x = (* String conversion that allows leading signs and unsigned values *) -(* TODO: replace by Char.Ascii.digit_to_int once on 5.4 *) -let dec_digit = function - | '0' .. '9' as c -> Char.code c - Char.code '0' - | _ -> assert false -[@@inline] - -(* TODO: replace by Char.Ascii.hex_digit_to_int once on 5.4 *) -let hex_digit = function - | '0' .. '9' as c -> Char.code c - Char.code '0' - | 'a' .. 'f' as c -> 0xa + Char.code c - Char.code 'a' - | 'A' .. 'F' as c -> 0xa + Char.code c - Char.code 'A' - | _ -> assert false -[@@inline] - let max_upper = unsigned_div minus_one 10l let max_lower = unsigned_rem minus_one 10l @@ -103,7 +89,7 @@ let of_string_exn s = let c = s.[i] in if Char.equal c '_' then parse_hex (i + 1) num else begin - let digit = of_int (hex_digit c) in + let digit = of_int (Char.Ascii.hex_digit_to_int c) in if not (le_u num (lshr minus_one (of_int 4))) then Fmt.failwith "of_string (int32)" else parse_hex (i + 1) (logor (shift_left num 4) digit) @@ -116,7 +102,7 @@ let of_string_exn s = let c = s.[i] in if Char.equal c '_' then parse_dec (i + 1) num else begin - let digit = of_int (dec_digit c) in + let digit = of_int (Char.Ascii.digit_to_int c) in if not (lt_u num max_upper || (eq num max_upper && le_u digit max_lower)) then Fmt.failwith "of_string (int32)" else parse_dec (i + 1) (add (mul num 10l) digit) diff --git a/src/primitives/int64.ml b/src/primitives/int64.ml index 6c72b95fa..4e13674dc 100644 --- a/src/primitives/int64.ml +++ b/src/primitives/int64.ml @@ -82,20 +82,6 @@ let extend_s n x = (* String conversion that allows leading signs and unsigned values *) -(* TODO: replace by Char.Ascii.digit_to_int once on 5.4 *) -let dec_digit = function - | '0' .. '9' as c -> Char.code c - Char.code '0' - | _ -> assert false -[@@inline] - -(* TODO: replace by Char.Ascii.hex_digit_to_int once on 5.4 *) -let hex_digit = function - | '0' .. '9' as c -> Char.code c - Char.code '0' - | 'a' .. 'f' as c -> 0xa + Char.code c - Char.code 'a' - | 'A' .. 'F' as c -> 0xa + Char.code c - Char.code 'A' - | _ -> assert false -[@@inline] - let max_upper = unsigned_div minus_one 10L let max_lower = unsigned_rem minus_one 10L @@ -109,7 +95,7 @@ let of_string_exn s = let c = s.[i] in if Char.equal c '_' then parse_hex (i + 1) num else begin - let digit = of_int (hex_digit c) in + let digit = of_int (Char.Ascii.hex_digit_to_int c) in if not (le_u num (lshr minus_one (of_int 4))) then Fmt.failwith "of_string (int64)" else parse_hex (i + 1) (logor (shift_left num 4) digit) @@ -122,7 +108,7 @@ let of_string_exn s = let c = s.[i] in if Char.equal c '_' then parse_dec (i + 1) num else begin - let digit = of_int (dec_digit c) in + let digit = of_int (Char.Ascii.digit_to_int c) in if not (lt_u num max_upper || (eq num max_upper && le_u digit max_lower)) then Fmt.failwith "of_string (int64)" else parse_dec (i + 1) (add (mul num 10L) digit) @@ -136,14 +122,10 @@ let of_string_exn s = else parse_dec i zero in - let parsed = - match s.[0] with - | '+' -> parse_int 1 - | '-' -> - let n = parse_int 1 in - if not (ge (sub n one) minus_one) then Fmt.failwith "of_string (int64)" - else neg n - | _ -> parse_int 0 - in - - parsed + match s.[0] with + | '+' -> parse_int 1 + | '-' -> + let n = parse_int 1 in + if not (ge (sub n one) minus_one) then Fmt.failwith "of_string (int64)" + else neg n + | _ -> parse_int 0 diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index d47e9d0fe..7509346e0 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -78,7 +78,7 @@ let run exploration_strategy ~workers solver t thread ~at_worker_value let sched = Scheduler.init () in Scheduler.add_init_task sched (Fun.const @@ State_monad.run t thread); if workers > 1 then Logs_threaded.enable (); - Array.init workers (fun _i -> + Iarray.init workers (fun _i -> Scheduler.spawn_worker sched ~at_worker_value ~at_worker_init ~finally:at_worker_end ) diff --git a/src/symbolic/symbolic_choice.mli b/src/symbolic/symbolic_choice.mli index ac753298d..06676c7e7 100644 --- a/src/symbolic/symbolic_choice.mli +++ b/src/symbolic/symbolic_choice.mli @@ -60,7 +60,7 @@ val run : (close_work_queue:(unit -> unit) -> ('a, Bug.t) result * Thread.t -> unit) -> at_worker_init:(unit -> unit) -> at_worker_end:(unit -> unit) - -> unit Domain.t array + -> unit Domain.t Iarray.t val ite : Symbolic_boolean.t diff --git a/src/symbolic/symbolic_driver.ml b/src/symbolic/symbolic_driver.ml index 0f015b4a5..f9688c915 100644 --- a/src/symbolic/symbolic_driver.ml +++ b/src/symbolic/symbolic_driver.ml @@ -63,7 +63,7 @@ let handle_result ~exploration_strategy ~workers ~no_stop_at_failure ~no_value mk_callback no_stop_at_failure fail_mode bug_stack path_count in let time_before = (Unix.times ()).tms_utime in - let domains : unit Domain.t Array.t = + let domains : unit Domain.t Iarray.t = Symbolic_choice.run exploration_strategy ~workers solver result thread ~at_worker_value ~at_worker_init:(fun () -> Bugs.new_pledge bug_stack) @@ -80,7 +80,7 @@ let handle_result ~exploration_strategy ~workers ~no_stop_at_failure ~no_value (* We don't want to wait for domain to complete in normal/quiet mode because it may take quite some time (if a solver is running a long query, the interpreter is in a long concrete loop, or if the work queue was not correctly closed for instance) *) let wait_for_all_domains () = - Array.iter + Iarray.iter (fun domain -> try Domain.join domain with | Z3.Error msg -> diff --git a/src/symbolic/symbolic_elem.ml b/src/symbolic/symbolic_elem.ml index caeb07a59..c246766bb 100644 --- a/src/symbolic/symbolic_elem.ml +++ b/src/symbolic/symbolic_elem.ml @@ -5,8 +5,8 @@ type t = Concrete_elem.t let get (elem : t) i : Symbolic_ref.t = - match elem.value.(i) with Func f -> Func f | _ -> assert false + match Concrete_elem.get elem i with Func f -> Func f | _ -> assert false -let size (elem : t) = Array.length elem.value +let size (elem : t) = Iarray.length elem.value let drop (e : t) = e.value <- [||] diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml index de737b467..7f39f0675 100644 --- a/src/symbolic/symbolic_wasm_ffi.ml +++ b/src/symbolic/symbolic_wasm_ffi.ml @@ -112,7 +112,7 @@ module M : if Int32.gt c 255l || Int32.lt c 0l then trap `Invalid_character_in_memory else let ch = char_of_int (Int32.to_int c) in - if Char.equal ch '\x00' then return (List.rev accu |> Array.of_list) + if Char.equal ch '\x00' then return (List.rev accu |> Iarray.of_list) else make_str m (ch :: accu) (Int32.add i (Int32.of_int 1)) | _ -> assert false @@ -137,7 +137,7 @@ module M : if Hashtbl.mem covered_labels id || in_seacoral_store id then abort () else let* chars = make_str m [] ptr in - let str = String.init (Array.length chars) (Array.get chars) in + let str = String.init (Iarray.length chars) (Iarray.get chars) in Hashtbl.add covered_labels id str; add_label (Int32.to_int id, str) | _ -> @@ -152,7 +152,7 @@ module M : let open Symbolic_choice in let* ptr = select_i32 ptr in let* chars = make_str m [] ptr in - let str = String.init (Array.length chars) (Array.get chars) in + let str = String.init (Iarray.length chars) (Iarray.get chars) in open_scope str let close_scope = Symbolic_choice.close_scope diff --git a/src/validate/binary_validate.ml b/src/validate/binary_validate.ml index 5d4a6c287..417c84337 100644 --- a/src/validate/binary_validate.ml +++ b/src/validate/binary_validate.ml @@ -45,11 +45,11 @@ module Index = struct end let check_mem modul n = - if n >= Array.length modul.mem then Error (`Unknown_memory (Text.Raw n)) + if n >= Iarray.length modul.mem then Error (`Unknown_memory (Text.Raw n)) else Ok () let check_data modul n = - if n >= Array.length modul.data then Error (`Unknown_data (Text.Raw n)) + if n >= Iarray.length modul.data then Error (`Unknown_data (Text.Raw n)) else Ok () let check_align memarg_align align = @@ -70,15 +70,15 @@ module Env = struct | Some v -> Ok v let global_get i modul = - if i >= Array.length modul.global then Error (`Unknown_global (Text.Raw i)) + if i >= Iarray.length modul.global then Error (`Unknown_global (Text.Raw i)) else - match modul.global.(i) with + match Iarray.get modul.global i with | Origin.Local { typ; _ } | Imported { typ; _ } -> Ok typ let func_get i modul = - if i >= Array.length modul.func then Error (`Unknown_func (Text.Raw i)) + if i >= Iarray.length modul.func then Error (`Unknown_func (Text.Raw i)) else - match modul.func.(i) with + match Iarray.get modul.func i with | Origin.Local { Func.type_f = Bt_raw (_, t); _ } | Imported { typ = Bt_raw (_, t); _ } -> Ok t @@ -89,14 +89,14 @@ module Env = struct | Some bt -> Ok bt let table_type_get i (modul : Binary.Module.t) = - if i >= Array.length modul.table then Error (`Unknown_table (Text.Raw i)) + if i >= Iarray.length modul.table then Error (`Unknown_table (Text.Raw i)) else - match modul.table.(i) with + match Iarray.get modul.table i with | Origin.Local (_, (_, t)) | Imported { typ = _, t; _ } -> Ok t let elem_type_get i modul = - if i >= Array.length modul.elem then Error (`Unknown_elem (Text.Raw i)) - else match modul.elem.(i) with value -> Ok value.typ + if i >= Iarray.length modul.elem then Error (`Unknown_elem (Text.Raw i)) + else match Iarray.get modul.elem i with value -> Ok value.typ let make ~params ~locals ~modul ~result_type ~refs = let l = List.mapi (fun i v -> (i, v)) (params @ locals) in @@ -216,7 +216,7 @@ end = struct | Any :: _ -> Ok [ Any ] | _ :: tl -> Ok tl - let push t stack = ok @@ t @ stack + let push t stack = Result.ok @@ t @ stack let pop_push (Bt_raw (_, (pt, rt)) : block_type) stack = let pt, rt = (List.rev_map typ_of_pt pt, List.rev_map typ_of_val_type rt) in @@ -483,8 +483,8 @@ let rec typecheck_instr (env : Env.t) (stack : stack) (instr : instr Annotated.t match stack with | Ref_type _ :: _tl -> Error (`Type_mismatch "select implicit") | Any :: _ -> Ok [ Something; Any ] - | hd :: Any :: _ -> ok @@ (hd :: [ Any ]) - | hd :: hd' :: tl when Stack.match_types hd hd' -> ok @@ (hd :: tl) + | hd :: Any :: _ -> Result.ok @@ (hd :: [ Any ]) + | hd :: hd' :: tl when Stack.match_types hd hd' -> Result.ok @@ (hd :: tl) | _ -> Error (`Type_mismatch "select") end | Some t -> @@ -510,7 +510,7 @@ let rec typecheck_instr (env : Env.t) (stack : stack) (instr : instr Annotated.t let* default_jt = Env.block_type_get i env in let* _stack = Stack.pop default_jt stack in let* () = - array_iter + iarray_iter (fun (i : indice) -> let* jt = Env.block_type_get i env in if not (List.length jt = List.length default_jt) then @@ -590,10 +590,10 @@ let typecheck_const_instr (modul : Module.t) refs stack instr = Hashtbl.add refs i (); Stack.push [ Ref_type Func_ht ] stack | Global_get i -> - if i >= Array.length modul.global then Error (`Unknown_global (Text.Raw i)) + if i >= Iarray.length modul.global then Error (`Unknown_global (Text.Raw i)) else let* mut, typ = - match modul.global.(i) with + match Iarray.get modul.global i with | Origin.Local _ -> Error (`Unknown_global (Text.Raw i)) | Imported { typ; _ } -> Ok typ in @@ -676,8 +676,8 @@ let typecheck_start { start; func; _ } = | None -> Ok () | Some idx -> ( let* f = - if idx >= Array.length func then Error (`Unknown_func (Text.Raw idx)) - else Ok func.(idx) + if idx >= Iarray.length func then Error (`Unknown_func (Text.Raw idx)) + else Ok (Iarray.get func idx) in match f with | Local { type_f = Bt_raw (_, ([], [])); _ } @@ -687,27 +687,27 @@ let typecheck_start { start; func; _ } = let validate_exports modul = let* () = - array_iter + iarray_iter (fun { Export.id; name = _ } -> let* _t = Env.func_get id modul in Ok () ) modul.exports.func in let* () = - array_iter + iarray_iter (fun { Export.id; name = _ } -> let* _t = Env.table_type_get id modul in Ok () ) modul.exports.table in let* () = - array_iter + iarray_iter (fun { Export.id; name = _ } -> let* _t = Env.global_get id modul in Ok () ) modul.exports.global in - array_iter + iarray_iter (fun { id; Export.name = _ } -> let* () = check_mem modul id in Ok () ) @@ -720,14 +720,14 @@ let check_limit { Text.min; max } = if min > max then Error `Size_minimum_greater_than_maximum else Ok () let validate_tables modul = - array_iter + iarray_iter (function | Origin.Local (_, (limits, _)) | Imported { typ = limits, _; _ } -> check_limit limits ) modul.table let validate_mem modul = - array_iter + iarray_iter (function | Origin.Local (_, typ) | Imported { typ; _ } -> let* () = @@ -744,14 +744,14 @@ let modul (modul : Module.t) = Log.info (fun m -> m "typechecking ..."); Log.bench_fn "typechecking time" @@ fun () -> let refs = Hashtbl.create 512 in - let* () = array_iter (typecheck_global modul refs) modul.global in - let* () = array_iter (typecheck_elem modul refs) modul.elem in - let* () = array_iter (typecheck_data modul refs) modul.data in + let* () = iarray_iter (typecheck_global modul refs) modul.global in + let* () = iarray_iter (typecheck_elem modul refs) modul.elem in + let* () = iarray_iter (typecheck_data modul refs) modul.data in let* () = typecheck_start modul in let* () = validate_exports modul in let* () = validate_tables modul in let* () = validate_mem modul in - Array.iter + Iarray.iter (fun (export : Export.t) -> Hashtbl.add refs export.id ()) modul.exports.func; - array_iter (fun func -> typecheck_function modul func refs) modul.func + iarray_iter (fun func -> typecheck_function modul func refs) modul.func diff --git a/test/replay/assert_false.t b/test/replay/assert_false.t index 02047f22f..4a6dcdea0 100644 --- a/test/replay/assert_false.t +++ b/test/replay/assert_false.t @@ -1,8 +1,8 @@ $ owi sym assert_false.wat -w1 owi: [ERROR] Assert failure: (i32.lt_u symbol_1 symbol_0) model { - symbol symbol_0 i32 1224779914 - symbol symbol_1 i32 -922707831 + symbol symbol_0 i32 134252706 + symbol symbol_1 i32 -2013230943 } owi: [ERROR] Reached problem! [13]