From 0112afcc558b644641cadea587d98769267f1823 Mon Sep 17 00:00:00 2001 From: krtab <53921575+krtab@users.noreply.github.com> Date: Wed, 15 May 2024 15:35:26 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20OCamlPro?= =?UTF-8?q?/owi@a786bcc7314383d26be20a81ec375ad83047aea6=20=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- coverage/badge.svg | 10 +- coverage/index.html | 20 +- coverage/src/bin/owi.ml.html | 124 +-- coverage/src/c_processing/c_share.ml.html | 20 +- coverage/src/cmd/cmd_c.ml.html | 487 +++++------- coverage/src/cmd/cmd_conc.ml.html | 2 +- coverage/src/cmd/cmd_sym.ml.html | 542 +++++++------ coverage/src/cmd/testcase.ml.html | 28 +- coverage/src/compile.ml.html | 30 +- coverage/src/concolic/concolic_value.ml.html | 174 ++--- coverage/src/concrete/concrete_memory.ml.html | 6 +- coverage/src/concrete/concrete_table.ml.html | 10 +- coverage/src/concrete/concrete_value.ml.html | 34 +- coverage/src/concrete/thread.ml.html | 24 +- coverage/src/data_structures/env_id.ml.html | 14 +- coverage/src/data_structures/func_id.ml.html | 12 +- coverage/src/data_structures/indexed.ml.html | 16 +- coverage/src/data_structures/named.ml.html | 4 +- coverage/src/data_structures/stack.ml.html | 48 +- coverage/src/interpret/interpret.ml.html | 578 +++++++------- coverage/src/link/link.ml.html | 184 ++--- coverage/src/link/link_env.ml.html | 22 +- coverage/src/parser/binary_parser.ml.html | 720 +++++++++--------- coverage/src/parser/parse.ml.html | 10 +- coverage/src/primitives/convert.ml.html | 2 +- coverage/src/primitives/float32.ml.html | 12 +- coverage/src/primitives/float64.ml.html | 12 +- coverage/src/primitives/int32.ml.html | 20 +- coverage/src/primitives/int64.ml.html | 28 +- coverage/src/result.ml.html | 4 +- coverage/src/script/script.ml.html | 2 +- coverage/src/symbolic/solver.ml.html | 4 +- coverage/src/symbolic/symbolic.ml.html | 72 +- coverage/src/symbolic/symbolic_choice.ml.html | 322 ++++---- coverage/src/symbolic/symbolic_global.ml.html | 52 +- coverage/src/symbolic/symbolic_memory.ml.html | 197 +++-- coverage/src/symbolic/symbolic_table.ml.html | 30 +- coverage/src/symbolic/symbolic_value.ml.html | 104 +-- coverage/src/tracing.ml.html | 8 +- coverage/src/typecheck/typecheck.ml.html | 210 ++--- coverage/src/utils/log.ml.html | 8 +- coverage/src/utils/syntax.ml.html | 30 +- coverage/src/utils/wutf8.ml.html | 10 +- coverage/src/v.ml.html | 4 +- 44 files changed, 2093 insertions(+), 2157 deletions(-) diff --git a/coverage/badge.svg b/coverage/badge.svg index da6a43dc7..aebaea8ac 100644 --- a/coverage/badge.svg +++ b/coverage/badge.svg @@ -1,5 +1,5 @@ - - coverage: 80% + + coverage: 79% @@ -7,13 +7,13 @@ - + diff --git a/coverage/index.html b/coverage/index.html index ec5358dfc..ed92cde69 100644 --- a/coverage/index.html +++ b/coverage/index.html @@ -3,13 +3,13 @@ Coverage report - +
@@ -95,9 +95,9 @@

80.15%

- + - 91% (156 / 171) + 87% (102 / 116) src/cmd/cmd_c.ml @@ -149,9 +149,9 @@

80.15%

- + - 87% (144 / 164) + 85% (145 / 170) src/cmd/cmd_sym.ml @@ -410,9 +410,9 @@

80.15%

- + - 61% (619 / 1012) + 60% (613 / 1010) src/parser/binary_parser.ml @@ -527,9 +527,9 @@

80.15%

- + - 84% (174 / 205) + 83% (172 / 205) src/symbolic/symbolic_memory.ml diff --git a/coverage/src/bin/owi.ml.html b/coverage/src/bin/owi.ml.html index 2563dd979..c31879037 100644 --- a/coverage/src/bin/owi.ml.html +++ b/coverage/src/bin/owi.ml.html @@ -699,13 +699,13 @@

78.76%

let debug = let doc = "debug mode" in - Cmdliner.Arg.(value & flag & info [ "debug"; "d" ] ~doc) + Cmdliner.Arg.(value & flag & info [ "debug"; "d" ] ~doc) let existing_non_dir_file = let parse s = - let path = Fpath.v s in - match Bos.OS.File.exists path with - | Ok true -> `Ok path + let path = Fpath.v s in + match Bos.OS.File.exists path with + | Ok true -> `Ok path | Ok false -> `Error (Format.asprintf "no file '%a'" Fpath.pp path) | Error (`Msg s) -> `Error s in @@ -718,38 +718,38 @@

78.76%

let files = let doc = "source files" in let f = existing_non_dir_file in - Cmdliner.Arg.(value & pos_all f [] (info [] ~doc)) + Cmdliner.Arg.(value & pos_all f [] (info [] ~doc)) let no_exhaustion = let doc = "no exhaustion tests" in - Cmdliner.Arg.(value & flag & info [ "no-exhaustion" ] ~doc) + Cmdliner.Arg.(value & flag & info [ "no-exhaustion" ] ~doc) let no_stop_at_failure = let doc = "do not stop when a program failure is encountered" in - Cmdliner.Arg.(value & flag & info [ "no-stop-at-failure" ] ~doc) + Cmdliner.Arg.(value & flag & info [ "no-stop-at-failure" ] ~doc) let no_values = let doc = "do not display a value for each symbol" in - Cmdliner.Arg.(value & flag & info [ "no-value" ] ~doc) + Cmdliner.Arg.(value & flag & info [ "no-value" ] ~doc) let deterministic_result_order = let doc = "Guarantee a fixed deterministic order of found failures. This implies \ --no-stop-at-failure." in - Cmdliner.Arg.(value & flag & info [ "deterministic-result-order" ] ~doc) + Cmdliner.Arg.(value & flag & info [ "deterministic-result-order" ] ~doc) let optimize = let doc = "optimize mode" in - Cmdliner.Arg.(value & flag & info [ "optimize" ] ~doc) + Cmdliner.Arg.(value & flag & info [ "optimize" ] ~doc) let profiling = let doc = "profiling mode" in - Cmdliner.Arg.(value & flag & info [ "profiling"; "p" ] ~doc) + Cmdliner.Arg.(value & flag & info [ "profiling"; "p" ] ~doc) let unsafe = let doc = "skip typechecking pass" in - Cmdliner.Arg.(value & flag & info [ "unsafe"; "u" ] ~doc) + Cmdliner.Arg.(value & flag & info [ "unsafe"; "u" ] ~doc) let workers = let doc = @@ -758,15 +758,15 @@

78.76%

in Cmdliner.Arg.( value - & opt int (Domain.recommended_domain_count ()) - & info [ "workers"; "w" ] ~doc ~absent:"n" ) + & opt int (Domain.recommended_domain_count ()) + & info [ "workers"; "w" ] ~doc ~absent:"n" ) let workspace = let doc = "path to the workspace directory" in Cmdliner.Arg.( - value & opt dir_file (Fpath.v "owi-out") & info [ "workspace" ] ~doc ) + value & opt dir_file (Fpath.v "owi-out") & info [ "workspace" ] ~doc ) -let copts_t = Cmdliner.Term.(const []) +let copts_t = Cmdliner.Term.(const []) let sdocs = Cmdliner.Manpage.s_common_options @@ -782,120 +782,120 @@

78.76%

"Compile a C file to Wasm and run the symbolic interpreter on it" in let man = [] @ shared_man in - Cmd.info "c" ~version ~doc ~sdocs ~man + Cmd.info "c" ~version ~doc ~sdocs ~man in let arch = let doc = "data model" in - Arg.(value & opt int 32 & info [ "arch"; "m" ] ~doc) + Arg.(value & opt int 32 & info [ "arch"; "m" ] ~doc) in let property = let doc = "property file" in - Arg.(value & opt (some string) None & info [ "property" ] ~doc) + Arg.(value & opt (some string) None & info [ "property" ] ~doc) in let includes = let doc = "headers path" in - Arg.(value & opt_all dir_file [] & info [ "I" ] ~doc) + Arg.(value & opt_all dir_file [] & info [ "I" ] ~doc) in let opt_lvl = let doc = "specify which optimization level to use" in - Arg.(value & opt string "0" & info [ "O" ] ~doc) + Arg.(value & opt string "0" & info [ "O" ] ~doc) in let testcomp = let doc = "test-comp mode" in - Arg.(value & flag & info [ "testcomp" ] ~doc) + Arg.(value & flag & info [ "testcomp" ] ~doc) in let output = let doc = "write results to dir" in - Arg.(value & opt string "owi-out" & info [ "output"; "o" ] ~doc) + Arg.(value & opt string "owi-out" & info [ "output"; "o" ] ~doc) in let concolic = let doc = "concolic mode" in - Arg.(value & flag & info [ "concolic" ] ~doc) + Arg.(value & flag & info [ "concolic" ] ~doc) in - Cmd.v info + Cmd.v info Term.( - const Cmd_c.cmd $ debug $ arch $ property $ testcomp $ output $ workers - $ opt_lvl $ includes $ files $ profiling $ unsafe $ optimize - $ no_stop_at_failure $ no_values $ deterministic_result_order $ concolic ) + const Cmd_c.cmd $ debug $ arch $ property $ testcomp $ output $ workers + $ opt_lvl $ includes $ files $ profiling $ unsafe $ optimize + $ no_stop_at_failure $ no_values $ deterministic_result_order $ concolic ) let fmt_cmd = let open Cmdliner in let info = let doc = "Format a .wat or .wast file" in let man = [] @ shared_man in - Cmd.info "fmt" ~version ~doc ~sdocs ~man + Cmd.info "fmt" ~version ~doc ~sdocs ~man in let inplace = let doc = "Format in-place, overwriting input file" in - Cmdliner.Arg.(value & flag & info [ "inplace"; "i" ] ~doc) + Cmdliner.Arg.(value & flag & info [ "inplace"; "i" ] ~doc) in - Cmd.v info Term.(const Cmd_fmt.cmd $ inplace $ files) + Cmd.v info Term.(const Cmd_fmt.cmd $ inplace $ files) let opt_cmd = let open Cmdliner in let info = let doc = "Optimize a module" in let man = [] @ shared_man in - Cmd.info "opt" ~version ~doc ~sdocs ~man + Cmd.info "opt" ~version ~doc ~sdocs ~man in - Cmd.v info Term.(const Cmd_opt.cmd $ debug $ unsafe $ files) + Cmd.v info Term.(const Cmd_opt.cmd $ debug $ unsafe $ files) let run_cmd = let open Cmdliner in let info = let doc = "Run the concrete interpreter" in let man = [] @ shared_man in - Cmd.info "run" ~version ~doc ~sdocs ~man + Cmd.info "run" ~version ~doc ~sdocs ~man in - Cmd.v info - Term.(const Cmd_run.cmd $ profiling $ debug $ unsafe $ optimize $ files) + Cmd.v info + Term.(const Cmd_run.cmd $ profiling $ debug $ unsafe $ optimize $ files) let validate_cmd = let open Cmdliner in let info = let doc = "Validate a module" in let man = [] @ shared_man in - Cmd.info "validate" ~version ~doc ~sdocs ~man + Cmd.info "validate" ~version ~doc ~sdocs ~man in - Cmd.v info Term.(const Cmd_validate.cmd $ debug $ files) + Cmd.v info Term.(const Cmd_validate.cmd $ debug $ files) let script_cmd = let open Cmdliner in let info = let doc = "Run a reference test suite script" in let man = [] @ shared_man in - Cmd.info "script" ~version ~doc ~sdocs ~man + Cmd.info "script" ~version ~doc ~sdocs ~man in - Cmd.v info + Cmd.v info Term.( - const Cmd_script.cmd $ profiling $ debug $ optimize $ files - $ no_exhaustion ) + const Cmd_script.cmd $ profiling $ debug $ optimize $ files + $ no_exhaustion ) let sym_cmd = let open Cmdliner in let info = let doc = "Run the symbolic interpreter" in let man = [] @ shared_man in - Cmd.info "sym" ~version ~doc ~sdocs ~man + Cmd.info "sym" ~version ~doc ~sdocs ~man in - Cmd.v info + Cmd.v info Term.( - const Cmd_sym.cmd $ profiling $ debug $ unsafe $ optimize $ workers - $ no_stop_at_failure $ no_values $ deterministic_result_order $ workspace - $ files ) + const Cmd_sym.cmd $ profiling $ debug $ unsafe $ optimize $ workers + $ no_stop_at_failure $ no_values $ deterministic_result_order $ workspace + $ files ) let conc_cmd = let open Cmdliner in let info = let doc = "Run the concolic interpreter" in let man = [] @ shared_man in - Cmd.info "conc" ~version ~doc ~sdocs ~man + Cmd.info "conc" ~version ~doc ~sdocs ~man in - Cmd.v info + Cmd.v info Term.( - const Cmd_conc.cmd $ profiling $ debug $ unsafe $ optimize $ workers - $ no_stop_at_failure $ no_values $ deterministic_result_order $ workspace - $ files ) + const Cmd_conc.cmd $ profiling $ debug $ unsafe $ optimize $ workers + $ no_stop_at_failure $ no_values $ deterministic_result_order $ workspace + $ files ) let wasm2wat_cmd = let open Cmdliner in @@ -905,9 +905,9 @@

78.76%

(.wasm)" in let man = [] @ shared_man in - Cmd.info "wasm2wat" ~version ~doc ~sdocs ~man + Cmd.info "wasm2wat" ~version ~doc ~sdocs ~man in - Cmd.v info Term.(const Cmd_wasm2wat.cmd $ files) + Cmd.v info Term.(const Cmd_wasm2wat.cmd $ files) let cli = let open Cmdliner in @@ -915,12 +915,12 @@

78.76%

let doc = "OCaml WebAssembly Interpreter" in let sdocs = Manpage.s_common_options in let man = [ `S Manpage.s_bugs; `P "Email them to <contact@ndrs.fr>." ] in - Cmd.info "owi" ~version ~doc ~sdocs ~man + Cmd.info "owi" ~version ~doc ~sdocs ~man in let default = - Term.(ret (const (fun (_ : _ list) -> `Help (`Plain, None)) $ copts_t)) + Term.(ret (const (fun (_ : _ list) -> `Help (`Plain, None)) $ copts_t)) in - Cmd.group info ~default + Cmd.group info ~default [ c_cmd ; fmt_cmd ; opt_cmd @@ -936,12 +936,12 @@

78.76%

let open Cmdliner.Cmd.Exit in match Cmdliner.Cmd.eval_value cli with | Ok (`Help | `Version) -> ok - | Ok (`Ok result) -> begin + | Ok (`Ok result) -> begin match result with | Ok () -> ok - | Error e -> begin - Format.pp_err "%s" (Result.err_to_string e); - match e with + | Error e -> begin + Format.pp_err "%s" (Result.err_to_string e); + match e with | `No_error -> ok | `Alignment_too_large -> 1 | `Assert_failure -> 2 @@ -955,7 +955,7 @@

78.76%

| `Duplicate_local _id -> 10 | `Duplicate_memory _id -> 11 | `Duplicate_table _id -> 12 - | `Found_bug _count -> 13 + | `Found_bug _count -> 13 | `Global_is_immutable -> 14 | `Illegal_escape _txt -> 15 | `Import_after_function -> 16 diff --git a/coverage/src/c_processing/c_share.ml.html b/coverage/src/c_processing/c_share.ml.html index beab77458..e1f0585f6 100644 --- a/coverage/src/c_processing/c_share.ml.html +++ b/coverage/src/c_processing/c_share.ml.html @@ -90,27 +90,27 @@

83.33%

open Syntax -let py_location = List.map Fpath.v C_share_site.Sites.pyc +let py_location = List.map Fpath.v C_share_site.Sites.pyc -let bin_location = List.map Fpath.v C_share_site.Sites.binc +let bin_location = List.map Fpath.v C_share_site.Sites.binc -let lib_location = List.map Fpath.v C_share_site.Sites.libc +let lib_location = List.map Fpath.v C_share_site.Sites.libc let find location file = - let* l = - list_map + let* l = + list_map (fun dir -> - let filename = Fpath.append dir file in - match Bos.OS.File.exists filename with - | Ok true -> Ok (Some filename) + let filename = Fpath.append dir file in + match Bos.OS.File.exists filename with + | Ok true -> Ok (Some filename) | Ok false -> Ok None | Error (`Msg msg) -> Error (`Msg msg) ) location in - Ok (List.find (function None -> false | Some _filename -> true) l) + Ok (List.find (function None -> false | Some _filename -> true) l) let libc = - Option.get @@ Result.get_ok @@ find bin_location (Fpath.v "libc.wasm") + Option.get @@ Result.get_ok @@ find bin_location (Fpath.v "libc.wasm")
diff --git a/coverage/src/cmd/cmd_c.ml.html b/coverage/src/cmd/cmd_c.ml.html index 57c96b923..e960bd0bf 100644 --- a/coverage/src/cmd/cmd_c.ml.html +++ b/coverage/src/cmd/cmd_c.ml.html @@ -3,7 +3,7 @@ cmd_c.ml — Coverage report - + @@ -15,20 +15,19 @@

src/cmd/cmd_c.ml

-

91.23%

+

87.93%

@@ -47,213 +46,167 @@

91.23%

- - + + - + - + - - - - + + + + - + - - - - - - + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + + - + - + - - - + + + - + - + - + - - + + - - - - - - + + + + + + - - + + - + - + - - + + - + - + - - + + - + - - - - + + + + - + - + - + - - + + - + - - + + - - - - + + + + - + - + - + - + - + - - - - - + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + +
@@ -433,52 +386,6 @@

91.23%

173 174 175 -176 -177 -178 -179 -180 -181 -182 -183 -184 -185 -186 -187 -188 -189 -190 -191 -192 -193 -194 -195 -196 -197 -198 -199 -200 -201 -202 -203 -204 -205 -206 -207 -208 -209 -210 -211 -212 -213 -214 -215 -216 -217 -218 -219 -220 -221 
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
 (* Copyright © 2021-2024 OCamlPro *)
@@ -487,47 +394,15 @@ 
91.23%

 open Bos
 open Syntax
 
-type deps =
-  { clang : flags:Cmd.t -> out:Fpath.t -> Fpath.t -> Cmd.t
-  ; opt : Fpath.t -> Cmd.t
-  ; llc : bc:Fpath.t -> obj:Fpath.t -> Cmd.t
-  ; ld : flags:Cmd.t -> out:Fpath.t -> Fpath.t list -> Cmd.t
-  }
-
 type metadata =
   { arch : int
   ; property : string option
   ; files : Fpath.t list
   }
 
-let clang bin ~flags ~out file : Bos.Cmd.t =
-  Cmd.(bin %% flags % "-o" % p out % p file)
-
-let opt bin file : Bos.Cmd.t = Cmd.(bin % "-O1" % "-o" % p file % p file)
-
-let llc bin ~bc ~obj : Bos.Cmd.t =
-  let flags = Cmd.of_list [ "-O1"; "-march=wasm32"; "-filetype=obj"; "-o" ] in
-  Cmd.(bin %% flags % p obj % p bc)
-
-let ld bin ~flags ~out files : Bos.Cmd.t =
-  let files = List.fold_left (fun acc f -> Cmd.(acc % p f)) Cmd.empty files in
-  Cmd.(bin %% flags % "-o" % p out %% files % p C_share.libc)
-
-let check_dependencies () : deps Result.t =
-  let* clang_bin = OS.Cmd.resolve @@ Cmd.v "clang" in
-  let* opt_bin = OS.Cmd.resolve @@ Cmd.v "opt" in
-  let* llc_bin = OS.Cmd.resolve @@ Cmd.v "llc" in
-  let* ld_bin = OS.Cmd.resolve @@ Cmd.v "wasm-ld" in
-  Ok
-    { clang = clang clang_bin
-    ; opt = opt opt_bin
-    ; llc = llc llc_bin
-    ; ld = ld ld_bin
-    }
-
 let pre_patterns : (Re2.t * string) array =
-  Array.map
-    (fun (regex, template) -> (Re2.create_exn regex, template))
+  Array.map
+    (fun (regex, template) -> (Re2.create_exn regex, template))
     [| ( "void\\s+reach_error\\(\\)\\s*\\{.*\\}"
        , "void reach_error() { owi_assert(0); }" )
        (* ugly: Hack to solve duplicate errors on compilation *)
@@ -555,14 +430,14 @@ 
91.23%

   OS.File.write dst data
 
 let copy ~src ~dst : Fpath.t Result.t =
-  let* data = OS.File.read src in
-  let+ () = OS.File.write dst data in
-  dst
+  let* data = OS.File.read src in
+  let+ () = OS.File.write dst data in
+  dst
 
 let instrument_file ?(skip = false) ~includes ~workspace file : Fpath.t Result.t
     =
-  let dst = Fpath.(workspace // base (file -+ ".c")) in
-  if skip then copy ~src:file ~dst
+  let dst = Fpath.(workspace // base (file -+ ".c")) in
+  if skip then copy ~src:file ~dst
   else begin
     Logs.app (fun m -> m "instrumenting %a" Fpath.pp file);
     let* () = patch ~src:file ~dst in
@@ -586,121 +461,107 @@ 
91.23%

     dst
   end
 
-let compile ~deps ~includes ~opt_lvl file : Fpath.t Result.t =
-  Logs.app (fun m -> m "compiling %a" Fpath.pp file);
-  let cflags =
-    let includes = Cmd.of_list ~slip:"-I" (List.map Fpath.to_string includes) in
-    let warnings =
-      Cmd.of_list
-        [ "-Wno-int-conversion"
-        ; "-Wno-pointer-sign"
-        ; "-Wno-string-plus-int"
-        ; "-Wno-implicit-function-declaration"
-        ; "-Wno-incompatible-library-redeclaration"
-        ; "-Wno-incompatible-function-pointer-types"
-        ; "-Wno-incompatible-pointer-types"
+let compile ~includes ~opt_lvl (files : Fpath.t list) : Fpath.t Result.t =
+  let flags =
+    let stack_size = 8 * 1024 * 1024 |> string_of_int in
+    let includes = Cmd.of_list ~slip:"-I" (List.map Fpath.to_string includes) in
+    Cmd.(
+      of_list
+        [ "-O" ^ opt_lvl
+        ; "--target=wasm32"
+        ; "-m32"
+        ; "-ffreestanding"
+        ; "--no-standard-libraries"
+        ; "-Wno-everything"
+        ; "-flto=thin"
+        ; (* LINKER FLAGS: *)
+          "-Wl,--entry=main"
+        ; "-Wl,--export=main"
+          (* TODO: allow this behind a flag, this is slooooow *)
+        ; "-Wl,--lto-O0"
+        ; "-Wl,-z,stack-size=" ^ stack_size
         ]
-    in
-    Cmd.(
-      of_list
-        [ "-O" ^ opt_lvl; "-g"; "-emit-llvm"; "--target=wasm32"; "-m32"; "-c" ]
-      %% warnings %% includes )
+      %% includes )
   in
-  let bc = Fpath.(file -+ ".bc") in
-  let obj = Fpath.(file -+ ".o") in
-  let* () = OS.Cmd.run @@ deps.clang ~flags:cflags ~out:bc file in
-  let* () = OS.Cmd.run @@ deps.opt bc in
-  let+ () = OS.Cmd.run @@ deps.llc ~bc ~obj in
-  obj
 
-let link ~deps ~workspace files : Fpath.t Result.t =
-  let ldflags ~entry =
-    let stack_size = 8 * (1024 * 1024) in
-    Cmd.(
-      of_list
-        [ "-z"; "stack-size=" ^ string_of_int stack_size; "--export=" ^ entry ] )
-  in
-  let wasm = Fpath.(workspace / "a.out.wasm") in
-  let+ () =
-    OS.Cmd.run @@ deps.ld ~flags:(ldflags ~entry:"_start") ~out:wasm files
-  in
-  wasm
+  let* clang_bin = OS.Cmd.resolve @@ Cmd.v "clang" in
+
+  let out = Fpath.(v "a.out.wasm") in
+  let files = Cmd.of_list (List.map Fpath.to_string (C_share.libc :: files)) in
+  let clang : Bos.Cmd.t = Cmd.(clang_bin %% flags % "-o" % p out %% files) in
+
+  let+ () = OS.Cmd.run clang in
+
+  out
 
 let pp_tm fmt Unix.{ tm_year; tm_mon; tm_mday; tm_hour; tm_min; tm_sec; _ } :
   unit =
-  Format.pp fmt "%04d-%02d-%02dT%02d:%02d:%02dZ" (tm_year + 1900) tm_mon tm_mday
+  Format.pp fmt "%04d-%02d-%02dT%02d:%02d:%02dZ" (tm_year + 1900) tm_mon tm_mday
     tm_hour tm_min tm_sec
 
 let metadata ~workspace arch property files : unit Result.t =
-  let out_metadata chan { arch; property; files } =
-    let o = Xmlm.make_output ~nl:true ~indent:(Some 2) (`Channel chan) in
-    let tag n = (("", n), []) in
-    let el n d = `El (tag n, [ `Data d ]) in
+  let out_metadata chan { arch; property; files } =
+    let o = Xmlm.make_output ~nl:true ~indent:(Some 2) (`Channel chan) in
+    let tag n = (("", n), []) in
+    let el n d = `El (tag n, [ `Data d ]) in
     let* spec =
-      match property with None -> Ok "" | Some f -> OS.File.read @@ Fpath.v f
+      match property with None -> Ok "" | Some f -> OS.File.read @@ Fpath.v f
     in
-    let file = String.concat " " (List.map Fpath.to_string files) in
-    let* hash =
-      list_fold_left
+    let file = String.concat " " (List.map Fpath.to_string files) in
+    let* hash =
+      list_fold_left
         (fun context file ->
-          match Bos.OS.File.read file with
+          match Bos.OS.File.read file with
           | Error (`Msg msg) -> Error (`Msg msg)
-          | Ok str -> Ok (Digestif.SHA256.feed_string context str) )
+          | Ok str -> Ok (Digestif.SHA256.feed_string context str) )
         Digestif.SHA256.empty files
     in
-    let hash = Digestif.SHA256.to_hex (Digestif.SHA256.get hash) in
-    let time = Unix.time () |> Unix.localtime in
-    let test_metadata =
+    let hash = Digestif.SHA256.to_hex (Digestif.SHA256.get hash) in
+    let time = Unix.time () |> Unix.localtime in
+    let test_metadata =
       `El
-        ( tag "test-metadata"
-        , [ el "sourcecodelang" "C"
-          ; el "producer" "owic"
-          ; el "specification" (String.trim spec)
-          ; el "programfile" file
-          ; el "programhash" hash
-          ; el "entryfunction" "main"
-          ; el "architecture" (Format.sprintf "%dbit" arch)
-          ; el "creationtime" (Format.asprintf "%a" pp_tm time)
+        ( tag "test-metadata"
+        , [ el "sourcecodelang" "C"
+          ; el "producer" "owic"
+          ; el "specification" (String.trim spec)
+          ; el "programfile" file
+          ; el "programhash" hash
+          ; el "entryfunction" "main"
+          ; el "architecture" (Format.sprintf "%dbit" arch)
+          ; el "creationtime" (Format.asprintf "%a" pp_tm time)
           ] )
     in
     let dtd =
       {xml|<!DOCTYPE test-metadata PUBLIC "+//IDN sosy-lab.org//DTD test-format test-metadata 1.1//EN" "https://sosy-lab.org/test-format/test-metadata-1.1.dtd">|xml}
     in
     Xmlm.output o (`Dtd (Some dtd));
-    Xmlm.output_tree Fun.id o test_metadata;
-    Ok ()
+    Xmlm.output_tree Fun.id o test_metadata;
+    Ok ()
   in
   let fpath = Fpath.(workspace / "test-suite" / "metadata.xml") in
-  let* (_exists : bool) = OS.Dir.create ~path:true (Fpath.parent fpath) in
-  let* res = OS.File.with_oc fpath out_metadata { arch; property; files } in
-  res
+  let* (_exists : bool) = OS.Dir.create ~path:true (Fpath.parent fpath) in
+  let* res = OS.File.with_oc fpath out_metadata { arch; property; files } in
+  res
 
 let cmd debug arch property testcomp workspace workers opt_lvl includes files
   profiling unsafe optimize no_stop_at_failure no_values
   deterministic_result_order concolic : unit Result.t =
-  if debug then Logs.set_level (Some Debug);
-  let workspace = Fpath.v workspace in
-  let includes = C_share.lib_location @ includes in
-  let* (deps : deps) = check_dependencies () in
-  let* (_exists : bool) = OS.Dir.create ~path:true workspace in
+  if debug then Logs.set_level (Some Debug);
+  let workspace = Fpath.v workspace in
+  let includes = C_share.lib_location @ includes in
+  let* (_exists : bool) = OS.Dir.create ~path:true workspace in
   (* skip instrumentation if not in test-comp mode *)
-  let skip = (not testcomp) || Sys.getenv_opt "RUNNER_OS" = Some "macOS" in
+  let skip = (not testcomp) || Sys.getenv_opt "RUNNER_OS" = Some "macOS" in
   let* (nfiles : Fpath.t list) =
-    list_map (instrument_file ~skip ~includes ~workspace) files
-  in
-  let* (objects : Fpath.t list) =
-    list_map (compile ~deps ~includes ~opt_lvl) nfiles
+    list_map (instrument_file ~skip ~includes ~workspace) files
   in
-  let* modul = link ~deps ~workspace objects in
-  let* () = metadata ~workspace arch property files in
-  let files = [ modul ] in
-  let workspace = Fpath.(workspace / "test-suite") in
-  if concolic then
-    Cmd_conc.cmd profiling debug unsafe optimize workers no_stop_at_failure
-      no_values deterministic_result_order workspace files
-  else
-    Cmd_sym.cmd profiling debug unsafe optimize workers no_stop_at_failure
-      no_values deterministic_result_order workspace files
+  let* modul = compile ~includes ~opt_lvl nfiles in
+  let* () = metadata ~workspace arch property files in
+  let workspace = Fpath.(workspace / "test-suite") in
+  let files = [ modul ] in
+  (if concolic then Cmd_conc.cmd else Cmd_sym.cmd)
+    profiling debug unsafe optimize workers no_stop_at_failure no_values
+    deterministic_result_order workspace files
diff --git a/coverage/src/cmd/cmd_conc.ml.html b/coverage/src/cmd/cmd_conc.ml.html index c3ea4222c..e4e1874cb 100644 --- a/coverage/src/cmd/cmd_conc.ml.html +++ b/coverage/src/cmd/cmd_conc.ml.html @@ -1309,7 +1309,7 @@

43.45%

module Choice = Concolic.P.Choice (* let () = Random.self_init () *) -let () = Random.init 42 +let () = Random.init 42 let debug = false diff --git a/coverage/src/cmd/cmd_sym.ml.html b/coverage/src/cmd/cmd_sym.ml.html index 43b7feefa..66f53236d 100644 --- a/coverage/src/cmd/cmd_sym.ml.html +++ b/coverage/src/cmd/cmd_sym.ml.html @@ -3,7 +3,7 @@ cmd_sym.ml — Coverage report - + @@ -15,25 +15,28 @@

src/cmd/cmd_sym.ml

-

87.80%

+

85.29%

@@ -57,7 +60,7 @@

87.80%

- + @@ -178,154 +181,177 @@

87.80%

- + - - + + - + - - - + + + - - + + - - - - - - - + + + + + + + - - - - - + + + + + - - + + - + - - + + - - + + - + - - + + - - - - + + + + - - + + - - + + - + - + - - - - + + + + - - + + - - + + - - - - + + + + - - - - + + + + - - - + + + - - - - - + + + + + - + - + - - - - + + + + - + - + - + - - - - + + + + - - - + + + + + + + + + + + + + + + + + + + + + + + + + +
@@ -618,6 +644,29 @@

87.80%

286 287 288 +289 +290 +291 +292 +293 +294 +295 +296 +297 +298 +299 +300 +301 +302 +303 +304 +305 +306 +307 +308 +309 +310 +311 
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
 (* Copyright © 2021-2024 OCamlPro *)
@@ -631,14 +680,14 @@ 
87.80%

 let symbolic_extern_module :
   Symbolic.P.Extern_func.extern_func Link.extern_module =
   let sym_cnt = Atomic.make 0 in
-  let symbol ty () : Value.int32 Choice.t =
-    let id = Atomic.fetch_and_add sym_cnt 1 in
-    let sym = Format.kasprintf (Smtml.Symbol.make ty) "symbol_%d" id in
-    let sym_expr = Expr.mk_symbol sym in
-    Choice.with_thread (fun thread ->
-        thread.symbol_set <- sym :: thread.symbol_set;
+  let symbol ty () : Value.int32 Choice.t =
+    let id = Atomic.fetch_and_add sym_cnt 1 in
+    let sym = Format.kasprintf (Smtml.Symbol.make ty) "symbol_%d" id in
+    let sym_expr = Expr.mk_symbol sym in
+    Choice.with_thread (fun thread ->
+        thread.symbol_set <- sym :: thread.symbol_set;
         match ty with
-        | Ty_bitv 8 -> Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, sym_expr))
+        | Ty_bitv 8 -> Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, sym_expr))
         | _ -> sym_expr )
   in
   let assume_i32 (i : Value.int32) : unit Choice.t =
@@ -650,26 +699,26 @@ 
87.80%

     Choice.add_pc c
   in
   let assert_i32 (i : Value.int32) : unit Choice.t =
-    let c = Value.I32.to_bool i in
-    Choice.assertion c
+    let c = Value.I32.to_bool i in
+    Choice.assertion c
   in
   (* we need to describe their types *)
   let functions =
     [ ( "i8_symbol"
       , Symbolic.P.Extern_func.Extern_func
-          (Func (UArg Res, R1 I32), symbol (Ty_bitv 8)) )
+          (Func (UArg Res, R1 I32), symbol (Ty_bitv 8)) )
     ; ( "i32_symbol"
       , Symbolic.P.Extern_func.Extern_func
-          (Func (UArg Res, R1 I32), symbol (Ty_bitv 32)) )
+          (Func (UArg Res, R1 I32), symbol (Ty_bitv 32)) )
     ; ( "i64_symbol"
       , Symbolic.P.Extern_func.Extern_func
-          (Func (UArg Res, R1 I64), symbol (Ty_bitv 64)) )
+          (Func (UArg Res, R1 I64), symbol (Ty_bitv 64)) )
     ; ( "f32_symbol"
       , Symbolic.P.Extern_func.Extern_func
-          (Func (UArg Res, R1 F32), symbol (Ty_fp 32)) )
+          (Func (UArg Res, R1 F32), symbol (Ty_fp 32)) )
     ; ( "f64_symbol"
       , Symbolic.P.Extern_func.Extern_func
-          (Func (UArg Res, R1 F64), symbol (Ty_fp 64)) )
+          (Func (UArg Res, R1 F64), symbol (Ty_fp 64)) )
     ; ( "assume"
       , Symbolic.P.Extern_func.Extern_func
           (Func (Arg (I32, Res), R0), assume_i32) )
@@ -689,40 +738,40 @@ 
87.80%

   let abort () : unit Choice.t = Choice.add_pc @@ Value.Bool.const false in
 
   let i32 v : int32 Choice.t =
-    match view v with
-    | Val (Num (I32 v)) -> Choice.return v
+    match view v with
+    | Val (Num (I32 v)) -> Choice.return v
     | _ ->
       Log.debug2 {|alloc: cannot allocate base pointer "%a"|} Expr.pp v;
       Choice.bind (abort ()) (fun () -> Choice.return 666l)
   in
   let ptr v : int32 Choice.t =
-    match view v with
-    | Ptr (b, _) -> Choice.return b
+    match view v with
+    | Ptr (b, _) -> Choice.return b
     | _ ->
       Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v;
       Choice.bind (abort ()) (fun () -> Choice.return 667l)
   in
   let alloc (base : Value.int32) (size : Value.int32) : Value.int32 Choice.t =
-    Choice.bind (i32 base) (fun base ->
-        Choice.with_thread (fun t ->
+    Choice.bind (i32 base) (fun base ->
+        Choice.with_thread (fun t ->
             let memories = Thread.memories t in
-            Symbolic_memory.iter
+            Symbolic_memory.iter
               (fun tbl ->
-                Symbolic_memory.ITbl.iter
+                Symbolic_memory.ITbl.iter
                   (fun _ (m : Symbolic_memory.t) ->
-                    Symbolic_memory.replace_size m base size )
+                    Symbolic_memory.replace_size m base size )
                   tbl )
               memories;
-            Expr.make (Ptr (base, Value.const_i32 0l)) ) )
+            Expr.make (Ptr (base, Value.const_i32 0l)) ) )
   in
   let free (p : Value.int32) : unit Choice.t =
-    Choice.bind (ptr p) (fun base ->
-        Choice.with_thread (fun t ->
-            let memories = Thread.memories t in
-            Symbolic_memory.iter
+    Choice.bind (ptr p) (fun base ->
+        Choice.with_thread (fun t ->
+            let memories = Thread.memories t in
+            Symbolic_memory.iter
               (fun tbl ->
-                Symbolic_memory.ITbl.iter
-                  (fun _ (m : Symbolic_memory.t) -> Symbolic_memory.free m base)
+                Symbolic_memory.ITbl.iter
+                  (fun _ (m : Symbolic_memory.t) -> Symbolic_memory.free m base)
                   tbl )
               memories ) )
   in
@@ -746,93 +795,116 @@ 
87.80%

 
 let ( let*/ ) (t : 'a Result.t) (f : 'a -> 'b Result.t Choice.t) :
   'b Result.t Choice.t =
-  match t with Error e -> Choice.return (Error e) | Ok x -> f x
+  match t with Error e -> Choice.return (Error e) | Ok x -> f x
 
-let run_text_modul ~unsafe ~optimize (pc : unit Result.t Choice.t)
-  (m : Text.modul) =
-  let link_state = Link.empty_state in
-  let link_state =
-    Link.extern_module' link_state ~name:"symbolic"
-      ~func_typ:Symbolic.P.Extern_func.extern_type symbolic_extern_module
-  in
-  let link_state =
-    Link.extern_module' link_state ~name:"summaries"
-      ~func_typ:Symbolic.P.Extern_func.extern_type summaries_extern_module
-  in
-  let*/ to_run, link_state =
-    let has_start =
-      List.exists (function Text.MStart _ -> true | _ -> false) m.fields
-    in
-    let has_start_id_function =
-      List.exists
-        (function Text.MFunc { id = Some "_start"; _ } -> true | _ -> false)
-        m.fields
-    in
-    let fields =
-      if has_start || not has_start_id_function then m.fields
-      else MStart (Text "_start") :: m.fields
-    in
-    let m = { m with fields } in
-    let+ m, state =
-      Compile.Text.until_link ~unsafe link_state ~optimize ~name:None m
-    in
-    let m = Symbolic.convert_module_to_run m in
-    (m, state)
-  in
-  let c = (Interpret.SymbolicP.modul link_state.envs) to_run in
-  Choice.bind pc (fun r ->
-      match r with Error _ -> Choice.return r | Ok () -> c )
+let link_state =
+  lazy
+    (let func_typ = Symbolic.P.Extern_func.extern_type in
+     let link_state =
+       Link.extern_module' Link.empty_state ~name:"symbolic" ~func_typ
+         symbolic_extern_module
+     in
+     Link.extern_module' link_state ~name:"summaries" ~func_typ
+       summaries_extern_module )
 
 let run_binary_modul ~unsafe ~optimize (pc : unit Result.t Choice.t)
   (m : Binary.modul) =
-  let link_state = Link.empty_state in
-  let link_state =
-    Link.extern_module' link_state ~name:"symbolic"
-      ~func_typ:Symbolic.P.Extern_func.extern_type symbolic_extern_module
-  in
-  let link_state =
-    Link.extern_module' link_state ~name:"summaries"
-      ~func_typ:Symbolic.P.Extern_func.extern_type summaries_extern_module
+  (* We are checking if there's a start function *)
+  let*/ m =
+    if Option.is_some m.start then Ok m
+    else
+      (* If there is none, we look for a function exported with the name `main` *)
+      match
+        List.find_opt
+          (function { Binary.name = "main"; _ } -> true | _ -> false)
+          m.exports.func
+      with
+      | None ->
+        (* TODO: fail/display a warning saying nothing will be done ? *)
+        Ok m
+      | Some export -> (
+        (* We found a main function, so we check its type and build a start function that put the right values on the stack, call the main function and drop the results *)
+        let main_id = export.id in
+        match Indexed.get_at main_id m.func.values with
+        | None -> Error (`Msg "can't find a main function")
+        | Some main_function ->
+          let (Bt_raw main_type) =
+            match main_function with
+            | Local f -> f.type_f
+            | Imported i -> i.desc
+          in
+          let default_value_of_t = function
+            | Types.Num_type I32 -> Ok (Types.I32_const 0l)
+            | Num_type I64 -> Ok (Types.I64_const 0L)
+            | Num_type F32 -> Ok (Types.F32_const (Float32.of_float 0.))
+            | Num_type F64 -> Ok (Types.F64_const (Float64.of_float 0.))
+            | Ref_type (Types.Null, t) -> Ok (Types.Ref_null t)
+            | Ref_type (Types.No_null, t) ->
+              Error
+                (`Msg
+                  (Format.asprintf "can not create default value of type %a"
+                     Types.pp_heap_type t ) )
+          in
+          let+ body =
+            let pt, rt = snd main_type in
+            let+ args = list_map (fun (_, t) -> default_value_of_t t) pt in
+            let after_call =
+              List.map (fun (_ : _ Types.val_type) -> Types.Drop) rt
+            in
+            args @ [ Types.Call (Raw main_id) ] @ after_call
+          in
+          let type_f : Types.binary Types.block_type =
+            Types.Bt_raw (None, ([], []))
+          in
+          let start_code : Types.binary Types.func =
+            { Types.type_f; locals = []; body; id = None }
+          in
+          let start_func = Runtime.Local start_code in
+          let named = m.func.named in
+          (* We need to add the new start function to the funcs of the module at the next free index *)
+          let next_free_index =
+            List.fold_left
+              (fun next_free_index v ->
+                let index = Indexed.get_index v in
+                if next_free_index > index then next_free_index else index + 1
+                )
+              0 m.func.values
+          in
+          let values =
+            Indexed.return next_free_index start_func :: m.func.values
+          in
+          let func = { Named.named; values } in
+          let start = Some next_free_index in
+          { m with func; start } )
   in
-  let*/ to_run, link_state =
-    let start =
-      if Option.is_some m.start then m.start
-      else
-        match
-          List.find_opt
-            (function { Binary.name = "_start"; _ } -> true | _ -> false)
-            m.exports.func
-        with
-        | None -> None
-        | Some export -> Some export.id
-    in
-    let m = { m with start } in
-    (* TODO: handle start function like in text ? *)
-    let+ m, state =
-      Compile.Binary.until_link ~unsafe link_state ~optimize ~name:None m
-    in
-    let m = Symbolic.convert_module_to_run m in
-    (m, state)
+
+  let link_state = Lazy.force link_state in
+
+  let*/ m, link_state =
+    Compile.Binary.until_link ~unsafe link_state ~optimize ~name:None m
   in
-  let c = (Interpret.SymbolicP.modul link_state.envs) to_run in
-  Choice.bind pc (fun r ->
-      match r with Error _ -> Choice.return r | Ok () -> c )
+  let m = Symbolic.convert_module_to_run m in
+  let c = Interpret.SymbolicP.modul link_state.envs m in
+  Choice.bind pc (fun r ->
+      match r with Error _ -> Choice.return r | Ok () -> c )
 
 let run_file ~unsafe ~optimize pc filename =
-  let*/ m = Parse.guess_from_file filename in
-  match m with
-  | Either.Left (Either.Left text_module) ->
-    run_text_modul ~unsafe ~optimize pc text_module
-  | Either.Left (Either.Right _text_scrpt) ->
-    Choice.return @@ Error (`Msg "can't run symbolic interpreter on a script")
-  | Either.Right binary_module ->
-    run_binary_modul ~unsafe ~optimize pc binary_module
+  let*/ m = Parse.guess_from_file filename in
+  let*/ m =
+    match m with
+    | Either.Left (Either.Left text_module) ->
+      Compile.Text.until_binary ~unsafe text_module
+    | Either.Left (Either.Right _text_scrpt) ->
+      Error (`Msg "can't run symbolic interpreter on a script")
+    | Either.Right binary_module -> Ok binary_module
+  in
+  run_binary_modul ~unsafe ~optimize pc m
 
 let get_model ~symbols solver pc =
-  assert (`Sat = Solver.Z3Batch.check solver pc);
+  assert (`Sat = Solver.Z3Batch.check solver pc);
   match Solver.Z3Batch.model ~symbols solver with
   | None -> assert false
-  | Some model -> model
+  | Some model -> model
 
 (* NB: This function propagates potential errors (Result.err) occurring
    during evaluation (OS, syntax error, etc.), except for Trap and Assert,
@@ -840,55 +912,55 @@ 
87.80%

    monad, hence the let*. *)
 let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
   deterministic_result_order (workspace : Fpath.t) files =
-  if profiling then Log.profiling_on := true;
-  if debug then Log.debug_on := true;
+  if profiling then Log.profiling_on := true;
+  if debug then Log.debug_on := true;
   (* deterministic_result_order implies no_stop_at_failure *)
-  let no_stop_at_failure = deterministic_result_order || no_stop_at_failure in
-  let* _created_dir = Bos.OS.Dir.create ~path:true ~mode:0o755 workspace in
-  let pc = Choice.return (Ok ()) in
-  let solver = Solver.Z3Batch.create () in
-  let result = List.fold_left (run_file ~unsafe ~optimize) pc files in
-  let thread : Thread.t = Thread.create () in
+  let no_stop_at_failure = deterministic_result_order || no_stop_at_failure in
+  let* _created_dir = Bos.OS.Dir.create ~path:true ~mode:0o755 workspace in
+  let pc = Choice.return (Ok ()) in
+  let solver = Solver.Z3Batch.create () in
+  let result = List.fold_left (run_file ~unsafe ~optimize) pc files in
+  let thread : Thread.t = Thread.create () in
   let results = Choice.run ~workers result thread in
-  let print_bug = function
+  let print_bug = function
     | `ETrap (tr, model) ->
       Format.pp_std "Trap: %s@\n" (Trap.to_string tr);
       Format.pp_std "Model:@\n  @[<v>%a@]@." (Smtml.Model.pp ~no_values) model
-    | `EAssert (assertion, model) ->
+    | `EAssert (assertion, model) ->
       Format.pp_std "Assert failure: %a@\n" Expr.pp assertion;
-      Format.pp_std "Model:@\n  @[<v>%a@]@." (Smtml.Model.pp ~no_values) model
+      Format.pp_std "Model:@\n  @[<v>%a@]@." (Smtml.Model.pp ~no_values) model
   in
   let rec print_and_count_failures count_acc results =
-    match results () with
+    match results () with
     | Seq.Nil -> Ok count_acc
-    | Seq.Cons ((result, thread), tl) ->
+    | Seq.Cons ((result, thread), tl) ->
       let pc = Thread.pc thread in
-      let symbols = thread.symbol_set in
+      let symbols = thread.symbol_set in
       let model = get_model ~symbols solver pc in
-      let* is_err =
+      let* is_err =
         let open Symbolic_choice.Multicore in
         match result with
-        | EAssert assertion ->
+        | EAssert assertion ->
           print_bug (`EAssert (assertion, model));
-          Ok true
+          Ok true
         | ETrap tr ->
           print_bug (`ETrap (tr, model));
           Ok true
-        | EVal (Ok ()) -> Ok false
+        | EVal (Ok ()) -> Ok false
         | EVal (Error e) -> Error e
       in
-      let count_acc = if is_err then succ count_acc else count_acc in
+      let count_acc = if is_err then succ count_acc else count_acc in
       let* () =
         if not no_values then
-          let testcase =
-            List.sort compare (Smtml.Model.get_bindings model) |> List.map snd
+          let testcase =
+            List.sort compare (Smtml.Model.get_bindings model) |> List.map snd
           in
-          Testcase.write_testcase ~dir:workspace ~err:is_err testcase
-        else Ok ()
+          Testcase.write_testcase ~dir:workspace ~err:is_err testcase
+        else Ok ()
       in
-      if (not is_err) || no_stop_at_failure then
-        print_and_count_failures count_acc tl
-      else Ok count_acc
+      if (not is_err) || no_stop_at_failure then
+        print_and_count_failures count_acc tl
+      else Ok count_acc
   in
   let results =
     if deterministic_result_order then
@@ -897,12 +969,12 @@ 
87.80%

            (x, List.rev @@ Thread.breadcrumbs th) )
       |> List.of_seq
       |> List.sort (fun (_, bc1) (_, bc2) ->
-             List.compare Stdlib.Int32.compare bc1 bc2 )
+             List.compare Stdlib.Int32.compare bc1 bc2 )
       |> List.to_seq |> Seq.map fst
-    else results
+    else results
   in
-  let* count = print_and_count_failures 0 results in
-  if count > 0 then Error (`Found_bug count)
+  let* count = print_and_count_failures 0 results in
+  if count > 0 then Error (`Found_bug count)
   else begin
     Format.pp_std "All OK";
     Ok ()
diff --git a/coverage/src/cmd/testcase.ml.html b/coverage/src/cmd/testcase.ml.html
index d37acaf68..9c3450290 100644
--- a/coverage/src/cmd/testcase.ml.html
+++ b/coverage/src/cmd/testcase.ml.html
@@ -96,30 +96,30 @@ 
100.00%

 open Syntax
 
 let out_testcase ~dst ~err testcase =
-  let o = Xmlm.make_output ~nl:true ~indent:(Some 2) dst in
-  let tag ?(atts = []) name = (("", name), atts) in
-  let atts = if err then Some [ (("", "coversError"), "true") ] else None in
-  let to_string v = Format.asprintf "%a" Smtml.Value.pp_num v in
-  let input v = `El (tag "input", [ `Data (to_string v) ]) in
-  let testcase = `El (tag ?atts "testcase", List.map input testcase) in
+  let o = Xmlm.make_output ~nl:true ~indent:(Some 2) dst in
+  let tag ?(atts = []) name = (("", name), atts) in
+  let atts = if err then Some [ (("", "coversError"), "true") ] else None in
+  let to_string v = Format.asprintf "%a" Smtml.Value.pp_num v in
+  let input v = `El (tag "input", [ `Data (to_string v) ]) in
+  let testcase = `El (tag ?atts "testcase", List.map input testcase) in
   let dtd =
     {|<!DOCTYPE testcase PUBLIC "+//IDN sosy-lab.org//DTD test-format testcase 1.1//EN" "https://sosy-lab.org/test-format/testcase-1.1.dtd">|}
   in
   Xmlm.output o (`Dtd (Some dtd));
-  Xmlm.output_tree Fun.id o testcase
+  Xmlm.output_tree Fun.id o testcase
 
 let write_testcase =
   let cnt = ref 0 in
   fun ~dir ~err testcase ->
-    incr cnt;
-    let name = Format.ksprintf Fpath.v "testcase-%d.xml" !cnt in
-    let path = Fpath.append dir name in
-    let* res =
-      Bos.OS.File.with_oc path
-        (fun chan () -> Ok (out_testcase ~dst:(`Channel chan) ~err testcase))
+    incr cnt;
+    let name = Format.ksprintf Fpath.v "testcase-%d.xml" !cnt in
+    let path = Fpath.append dir name in
+    let* res =
+      Bos.OS.File.with_oc path
+        (fun chan () -> Ok (out_testcase ~dst:(`Channel chan) ~err testcase))
         ()
     in
-    res
+    res
diff --git a/coverage/src/compile.ml.html b/coverage/src/compile.ml.html index f39f33d76..ba01f64f3 100644 --- a/coverage/src/compile.ml.html +++ b/coverage/src/compile.ml.html @@ -193,19 +193,19 @@

88.14%

Rewrite.modul m let until_typecheck ~unsafe m = - let* m = until_binary ~unsafe m in - if unsafe then Ok m + let* m = until_binary ~unsafe m in + if unsafe then Ok m else - let+ () = Typecheck.modul m in - m + let+ () = Typecheck.modul m in + m let until_optimize ~unsafe ~optimize m = - let+ m = until_typecheck ~unsafe m in - if optimize then Optimize.modul m else m + let+ m = until_typecheck ~unsafe m in + if optimize then Optimize.modul m else m let until_link ~unsafe link_state ~optimize ~name m = - let* m = until_optimize ~unsafe ~optimize m in - Link.modul link_state ~name m + let* m = until_optimize ~unsafe ~optimize m in + Link.modul link_state ~name m let until_interpret link_state ~unsafe ~optimize ~name m = let* m, link_state = until_link link_state ~unsafe ~optimize ~name m in @@ -215,18 +215,18 @@

88.14%

module Binary = struct let until_typecheck ~unsafe m = - if unsafe then Ok m + if unsafe then Ok m else - let+ () = Typecheck.modul m in - m + let+ () = Typecheck.modul m in + m let until_optimize ~unsafe ~optimize m = - let+ m = until_typecheck ~unsafe m in - if optimize then Optimize.modul m else m + let+ m = until_typecheck ~unsafe m in + if optimize then Optimize.modul m else m let until_link ~unsafe link_state ~optimize ~name m = - let* m = until_optimize ~unsafe ~optimize m in - Link.modul link_state ~name m + let* m = until_optimize ~unsafe ~optimize m in + Link.modul link_state ~name m let until_interpret link_state ~unsafe ~optimize ~name m = let* m = diff --git a/coverage/src/concolic/concolic_value.ml.html b/coverage/src/concolic/concolic_value.ml.html index c8d3c366a..35aaf5e4d 100644 --- a/coverage/src/concolic/concolic_value.ml.html +++ b/coverage/src/concolic/concolic_value.ml.html @@ -1065,7 +1065,7 @@

60.90%

| F64 of float64 | Ref of ref_value - let pair concrete symbolic = { concrete; symbolic } + let pair concrete symbolic = { concrete; symbolic } (* Bof... *) let value_pair (c : C.t) (s : S.t) = @@ -1103,7 +1103,7 @@

60.90%

} [@@inline always] - let f_pair_1_cst fc fs v = { concrete = fc v; symbolic = fs v } + let f_pair_1_cst fc fs v = { concrete = fc v; symbolic = fs v } [@@inline always] let f_pair_2_cst fc fs v1 v2 = { concrete = fc v1 v2; symbolic = fs v1 v2 } @@ -1113,9 +1113,9 @@

60.90%

{ concrete = fc cs.concrete v2; symbolic = fs cs.symbolic v2 } [@@inline always] - let const_i32 v = f_pair_1_cst C.const_i32 S.const_i32 v + let const_i32 v = f_pair_1_cst C.const_i32 S.const_i32 v - let const_i64 v = f_pair_1_cst C.const_i64 S.const_i64 v + let const_i64 v = f_pair_1_cst C.const_i64 S.const_i64 v let const_f32 v = f_pair_1_cst C.const_f32 S.const_f32 v @@ -1171,17 +1171,17 @@

60.90%

end module Bool = struct - let const = f_pair_1_cst C.Bool.const S.Bool.const + let const = f_pair_1_cst C.Bool.const S.Bool.const - let not = f_pair_1 C.Bool.not S.Bool.not + let not = f_pair_1 C.Bool.not S.Bool.not - let or_ = f_pair_2 C.Bool.or_ S.Bool.or_ + let or_ = f_pair_2 C.Bool.or_ S.Bool.or_ - let and_ = f_pair_2 C.Bool.and_ S.Bool.and_ + let and_ = f_pair_2 C.Bool.and_ S.Bool.and_ - let int32 = f_pair_1 C.Bool.int32 S.Bool.int32 + let int32 = f_pair_1 C.Bool.int32 S.Bool.int32 - let pp = mk_pp C.Bool.pp S.Bool.pp + let pp = mk_pp C.Bool.pp S.Bool.pp end module type CFop = sig @@ -1225,59 +1225,59 @@

60.90%

and type int32 := int32 and type int64 := int64 and type same_size_int := (CIT.t, SIT.t) cs = struct - let zero = pair CFop.zero SFop.zero + let zero = pair CFop.zero SFop.zero - let abs = f_pair_1 CFop.abs SFop.abs + let abs = f_pair_1 CFop.abs SFop.abs - let neg = f_pair_1 CFop.neg SFop.neg + let neg = f_pair_1 CFop.neg SFop.neg - let sqrt = f_pair_1 CFop.sqrt SFop.sqrt + let sqrt = f_pair_1 CFop.sqrt SFop.sqrt - let ceil = f_pair_1 CFop.ceil SFop.ceil + let ceil = f_pair_1 CFop.ceil SFop.ceil - let floor = f_pair_1 CFop.floor SFop.floor + let floor = f_pair_1 CFop.floor SFop.floor - let trunc = f_pair_1 CFop.trunc SFop.trunc + let trunc = f_pair_1 CFop.trunc SFop.trunc - let nearest = f_pair_1 CFop.nearest SFop.nearest + let nearest = f_pair_1 CFop.nearest SFop.nearest - let add = f_pair_2 CFop.add SFop.add + let add = f_pair_2 CFop.add SFop.add - let sub = f_pair_2 CFop.sub SFop.sub + let sub = f_pair_2 CFop.sub SFop.sub - let mul = f_pair_2 CFop.mul SFop.mul + let mul = f_pair_2 CFop.mul SFop.mul - let div = f_pair_2 CFop.div SFop.div + let div = f_pair_2 CFop.div SFop.div - let min = f_pair_2 CFop.min SFop.min + let min = f_pair_2 CFop.min SFop.min - let max = f_pair_2 CFop.max SFop.max + let max = f_pair_2 CFop.max SFop.max - let copy_sign = f_pair_2 CFop.copy_sign SFop.copy_sign + let copy_sign = f_pair_2 CFop.copy_sign SFop.copy_sign - let eq = f_pair_2 CFop.eq SFop.eq + let eq = f_pair_2 CFop.eq SFop.eq - let ne = f_pair_2 CFop.ne SFop.ne + let ne = f_pair_2 CFop.ne SFop.ne - let lt = f_pair_2 CFop.lt SFop.lt + let lt = f_pair_2 CFop.lt SFop.lt - let gt = f_pair_2 CFop.gt SFop.gt + let gt = f_pair_2 CFop.gt SFop.gt - let le = f_pair_2 CFop.le SFop.le + let le = f_pair_2 CFop.le SFop.le - let ge = f_pair_2 CFop.ge SFop.ge + let ge = f_pair_2 CFop.ge SFop.ge - let convert_i32_s = f_pair_1 CFop.convert_i32_s SFop.convert_i32_s + let convert_i32_s = f_pair_1 CFop.convert_i32_s SFop.convert_i32_s - let convert_i32_u = f_pair_1 CFop.convert_i32_u SFop.convert_i32_u + let convert_i32_u = f_pair_1 CFop.convert_i32_u SFop.convert_i32_u - let convert_i64_s = f_pair_1 CFop.convert_i64_s SFop.convert_i64_s + let convert_i64_s = f_pair_1 CFop.convert_i64_s SFop.convert_i64_s - let convert_i64_u = f_pair_1 CFop.convert_i64_u SFop.convert_i64_u + let convert_i64_u = f_pair_1 CFop.convert_i64_u SFop.convert_i64_u - let of_bits = f_pair_1 CFop.of_bits SFop.of_bits + let of_bits = f_pair_1 CFop.of_bits SFop.of_bits - let to_bits = f_pair_1 CFop.to_bits SFop.to_bits + let to_bits = f_pair_1 CFop.to_bits SFop.to_bits end module type CIop = sig @@ -1320,81 +1320,81 @@

60.90%

and type vbool := vbool and type float32 := float32 and type float64 := float64 = struct - let zero = pair CIop.zero SIop.zero + let zero = pair CIop.zero SIop.zero - let clz = f_pair_1 CIop.clz SIop.clz + let clz = f_pair_1 CIop.clz SIop.clz - let ctz = f_pair_1 CIop.ctz SIop.ctz + let ctz = f_pair_1 CIop.ctz SIop.ctz - let popcnt = f_pair_1 CIop.popcnt SIop.popcnt + let popcnt = f_pair_1 CIop.popcnt SIop.popcnt - let add = f_pair_2 CIop.add SIop.add + let add = f_pair_2 CIop.add SIop.add - let sub = f_pair_2 CIop.sub SIop.sub + let sub = f_pair_2 CIop.sub SIop.sub - let mul = f_pair_2 CIop.mul SIop.mul + let mul = f_pair_2 CIop.mul SIop.mul - let div = f_pair_2 CIop.div SIop.div + let div = f_pair_2 CIop.div SIop.div - let unsigned_div = f_pair_2 CIop.unsigned_div SIop.unsigned_div + let unsigned_div = f_pair_2 CIop.unsigned_div SIop.unsigned_div - let rem = f_pair_2 CIop.rem SIop.rem + let rem = f_pair_2 CIop.rem SIop.rem - let unsigned_rem = f_pair_2 CIop.unsigned_rem SIop.unsigned_rem + let unsigned_rem = f_pair_2 CIop.unsigned_rem SIop.unsigned_rem - let logand = f_pair_2 CIop.logand SIop.logand + let logand = f_pair_2 CIop.logand SIop.logand - let logor = f_pair_2 CIop.logor SIop.logor + let logor = f_pair_2 CIop.logor SIop.logor - let logxor = f_pair_2 CIop.logxor SIop.logxor + let logxor = f_pair_2 CIop.logxor SIop.logxor - let shl = f_pair_2 CIop.shl SIop.shl + let shl = f_pair_2 CIop.shl SIop.shl - let shr_s = f_pair_2 CIop.shr_s SIop.shr_s + let shr_s = f_pair_2 CIop.shr_s SIop.shr_s - let shr_u = f_pair_2 CIop.shr_u SIop.shr_u + let shr_u = f_pair_2 CIop.shr_u SIop.shr_u - let rotl = f_pair_2 CIop.rotl SIop.rotl + let rotl = f_pair_2 CIop.rotl SIop.rotl - let rotr = f_pair_2 CIop.rotr SIop.rotr + let rotr = f_pair_2 CIop.rotr SIop.rotr - let eq_const = f_pair_2_cst' CIop.eq_const SIop.eq_const + let eq_const = f_pair_2_cst' CIop.eq_const SIop.eq_const - let eq = f_pair_2 CIop.eq SIop.eq + let eq = f_pair_2 CIop.eq SIop.eq - let ne = f_pair_2 CIop.ne SIop.ne + let ne = f_pair_2 CIop.ne SIop.ne - let lt = f_pair_2 CIop.lt SIop.lt + let lt = f_pair_2 CIop.lt SIop.lt - let gt = f_pair_2 CIop.gt SIop.gt + let gt = f_pair_2 CIop.gt SIop.gt - let lt_u = f_pair_2 CIop.lt_u SIop.lt_u + let lt_u = f_pair_2 CIop.lt_u SIop.lt_u - let gt_u = f_pair_2 CIop.gt_u SIop.gt_u + let gt_u = f_pair_2 CIop.gt_u SIop.gt_u - let le = f_pair_2 CIop.le SIop.le + let le = f_pair_2 CIop.le SIop.le - let ge = f_pair_2 CIop.ge SIop.ge + let ge = f_pair_2 CIop.ge SIop.ge - let le_u = f_pair_2 CIop.le_u SIop.le_u + let le_u = f_pair_2 CIop.le_u SIop.le_u - let ge_u = f_pair_2 CIop.ge_u SIop.ge_u + let ge_u = f_pair_2 CIop.ge_u SIop.ge_u - let trunc_f32_s = f_pair_1 CIop.trunc_f32_s SIop.trunc_f32_s + let trunc_f32_s = f_pair_1 CIop.trunc_f32_s SIop.trunc_f32_s - let trunc_f32_u = f_pair_1 CIop.trunc_f32_u SIop.trunc_f32_u + let trunc_f32_u = f_pair_1 CIop.trunc_f32_u SIop.trunc_f32_u - let trunc_f64_s = f_pair_1 CIop.trunc_f64_s SIop.trunc_f64_s + let trunc_f64_s = f_pair_1 CIop.trunc_f64_s SIop.trunc_f64_s - let trunc_f64_u = f_pair_1 CIop.trunc_f64_u SIop.trunc_f64_u + let trunc_f64_u = f_pair_1 CIop.trunc_f64_u SIop.trunc_f64_u - let trunc_sat_f32_s = f_pair_1 CIop.trunc_sat_f32_s SIop.trunc_sat_f32_s + let trunc_sat_f32_s = f_pair_1 CIop.trunc_sat_f32_s SIop.trunc_sat_f32_s - let trunc_sat_f32_u = f_pair_1 CIop.trunc_sat_f32_u SIop.trunc_sat_f32_u + let trunc_sat_f32_u = f_pair_1 CIop.trunc_sat_f32_u SIop.trunc_sat_f32_u - let trunc_sat_f64_s = f_pair_1 CIop.trunc_sat_f64_s SIop.trunc_sat_f64_s + let trunc_sat_f64_s = f_pair_1 CIop.trunc_sat_f64_s SIop.trunc_sat_f64_s - let trunc_sat_f64_u = f_pair_1 CIop.trunc_sat_f64_u SIop.trunc_sat_f64_u + let trunc_sat_f64_u = f_pair_1 CIop.trunc_sat_f64_u SIop.trunc_sat_f64_u let extend_s symbolic cs = { concrete = CIop.extend_s symbolic cs.concrete @@ -1420,9 +1420,9 @@

60.90%

(C.F32) (S.F32) - let demote_f64 = f_pair_1 C.F32.demote_f64 S.F32.demote_f64 + let demote_f64 = f_pair_1 C.F32.demote_f64 S.F32.demote_f64 - let reinterpret_i32 = f_pair_1 C.F32.reinterpret_i32 S.F32.reinterpret_i32 + let reinterpret_i32 = f_pair_1 C.F32.reinterpret_i32 S.F32.reinterpret_i32 end module F64 = struct @@ -1443,9 +1443,9 @@

60.90%

(C.F64) (S.F64) - let promote_f32 = f_pair_1 C.F64.promote_f32 S.F64.promote_f32 + let promote_f32 = f_pair_1 C.F64.promote_f32 S.F64.promote_f32 - let reinterpret_i64 = f_pair_1 C.F64.reinterpret_i64 S.F64.reinterpret_i64 + let reinterpret_i64 = f_pair_1 C.F64.reinterpret_i64 S.F64.reinterpret_i64 end module I32 = struct @@ -1463,11 +1463,11 @@

60.90%

(C.I32) (S.I32) - let to_bool = f_pair_1 C.I32.to_bool S.I32.to_bool + let to_bool = f_pair_1 C.I32.to_bool S.I32.to_bool - let reinterpret_f32 = f_pair_1 C.I32.reinterpret_f32 S.I32.reinterpret_f32 + let reinterpret_f32 = f_pair_1 C.I32.reinterpret_f32 S.I32.reinterpret_f32 - let wrap_i64 = f_pair_1 C.I32.wrap_i64 S.I32.wrap_i64 + let wrap_i64 = f_pair_1 C.I32.wrap_i64 S.I32.wrap_i64 end module I64 = struct @@ -1485,15 +1485,15 @@

60.90%

(C.I64) (S.I64) - let of_int32 = f_pair_1 C.I64.of_int32 S.I64.of_int32 + let of_int32 = f_pair_1 C.I64.of_int32 S.I64.of_int32 - let to_int32 = f_pair_1 C.I64.to_int32 S.I64.to_int32 + let to_int32 = f_pair_1 C.I64.to_int32 S.I64.to_int32 - let reinterpret_f64 = f_pair_1 C.I64.reinterpret_f64 S.I64.reinterpret_f64 + let reinterpret_f64 = f_pair_1 C.I64.reinterpret_f64 S.I64.reinterpret_f64 - let extend_i32_s = f_pair_1 C.I64.extend_i32_s S.I64.extend_i32_s + let extend_i32_s = f_pair_1 C.I64.extend_i32_s S.I64.extend_i32_s - let extend_i32_u = f_pair_1 C.I64.extend_i32_u S.I64.extend_i32_u + let extend_i32_u = f_pair_1 C.I64.extend_i32_u S.I64.extend_i32_u end end diff --git a/coverage/src/concrete/concrete_memory.ml.html b/coverage/src/concrete/concrete_memory.ml.html index 96a13186f..25f5e914e 100644 --- a/coverage/src/concrete/concrete_memory.ml.html +++ b/coverage/src/concrete/concrete_memory.ml.html @@ -271,8 +271,8 @@

94.81%

} let init limits : t = - let data = Bytes.make (page_size * limits.min) '\x00' in - { limits; data } + let data = Bytes.make (page_size * limits.min) '\x00' in + { limits; data } let update_memory mem data = let limits = @@ -367,7 +367,7 @@

94.81%

let addr = Int32.to_int addr in Bytes.get_int64_le mem.data addr -let size_in_pages mem = Int32.of_int @@ (Bytes.length mem.data / page_size) +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/coverage/src/concrete/concrete_table.ml.html b/coverage/src/concrete/concrete_table.ml.html index f426f796e..11a6591e2 100644 --- a/coverage/src/concrete/concrete_table.ml.html +++ b/coverage/src/concrete/concrete_table.ml.html @@ -161,14 +161,14 @@

100.00%

let fresh = let r = ref (-1) in fun () -> - incr r; - !r + incr r; + !r let init ?label (typ : binary table_type) : t = - let limits, ((_null, heap_type) as ref_type) = typ in + let limits, ((_null, heap_type) as ref_type) = typ in let null = Concrete_value.ref_null' heap_type in - let table = Array.make limits.min null in - { id = fresh (); label; limits; typ = ref_type; data = table } + let table = Array.make limits.min null in + { id = fresh (); label; limits; typ = ref_type; data = table } let update table data = table.data <- data diff --git a/coverage/src/concrete/concrete_value.ml.html b/coverage/src/concrete/concrete_value.ml.html index 63972e34e..40d38f612 100644 --- a/coverage/src/concrete/concrete_value.ml.html +++ b/coverage/src/concrete/concrete_value.ml.html @@ -398,42 +398,42 @@

63.38%

type extern_func = Extern_func : 'a func_type * 'a -> extern_func let elt_type (type t) (e : t telt) : binary val_type = - match e with - | I32 -> Num_type I32 - | I64 -> Num_type I64 - | F32 -> Num_type F32 - | F64 -> Num_type F64 + match e with + | I32 -> Num_type I32 + | I64 -> Num_type I64 + | F32 -> Num_type F32 + | F64 -> Num_type F64 | Externref _ -> Ref_type (Null, Extern_ht) let res_type (type t) (r : t rtype) : binary result_type = - match r with - | R0 -> [] - | R1 a -> [ elt_type a ] + match r with + | R0 -> [] + | R1 a -> [ elt_type a ] | R2 (a, b) -> [ elt_type a; elt_type b ] | R3 (a, b, c) -> [ elt_type a; elt_type b; elt_type c ] | R4 (a, b, c, d) -> [ elt_type a; elt_type b; elt_type c; elt_type d ] let rec arg_type : type t r. (t, r) atype -> binary param_type = function - | UArg tl -> arg_type tl - | Arg (hd, tl) -> (None, elt_type hd) :: arg_type tl + | UArg tl -> arg_type tl + | Arg (hd, tl) -> (None, elt_type hd) :: arg_type tl | NArg (name, hd, tl) -> (Some name, elt_type hd) :: arg_type tl - | Res -> [] + | Res -> [] (* let extern_type (Func (arg, res)) : Simplified.func_type = *) (* (arg_type arg, res_type res) *) let extern_type (Extern_func (Func (arg, res), _)) : binary Types.func_type = - (arg_type arg, res_type res) + (arg_type arg, res_type res) type t = Func_intf.t let fresh = - let r = ref ~-1 in + let r = ref ~-1 in fun () -> - incr r; - !r + incr r; + !r - let wasm func env : t = WASM (fresh (), func, env) + let wasm func env : t = WASM (fresh (), func, env) (* let typ = function *) (* | Func_intf.WASM (_, func, _env) -> func.type_f *) @@ -505,7 +505,7 @@

63.38%

| Ref r -> pp_ref_value fmt r let ref_null' = function - | Func_ht -> Funcref None + | Func_ht -> Funcref None | Extern_ht -> Externref None | Array_ht -> Arrayref None | Any_ht | None_ht | Eq_ht | I31_ht | Struct_ht | No_func_ht | No_extern_ht diff --git a/coverage/src/concrete/thread.ml.html b/coverage/src/concrete/thread.ml.html index 95f932ced..34fe45a5b 100644 --- a/coverage/src/concrete/thread.ml.html +++ b/coverage/src/concrete/thread.ml.html @@ -125,31 +125,31 @@

100.00%

; breadcrumbs : int32 list } -let pc t = t.pc +let pc t = t.pc -let memories t = t.memories +let memories t = t.memories -let tables t = t.tables +let tables t = t.tables -let globals t = t.globals +let globals t = t.globals let breadcrumbs t = t.breadcrumbs let create () = - { choices = 0 + { choices = 0 ; symbol_set = [] ; pc = [] - ; memories = Symbolic_memory.init () - ; tables = Symbolic_table.init () - ; globals = Symbolic_global.init () + ; memories = Symbolic_memory.init () + ; tables = Symbolic_table.init () + ; globals = Symbolic_global.init () ; breadcrumbs = [] } let clone { choices; symbol_set; pc; memories; tables; globals; breadcrumbs } = - let memories = Symbolic_memory.clone memories in - let tables = Symbolic_table.clone tables in - let globals = Symbolic_global.clone globals in - { choices; symbol_set; pc; memories; tables; globals; breadcrumbs } + let memories = Symbolic_memory.clone memories in + let tables = Symbolic_table.clone tables in + let globals = Symbolic_global.clone globals in + { choices; symbol_set; pc; memories; tables; globals; breadcrumbs } diff --git a/coverage/src/data_structures/env_id.ml.html b/coverage/src/data_structures/env_id.ml.html index 5414805af..ed78119c2 100644 --- a/coverage/src/data_structures/env_id.ml.html +++ b/coverage/src/data_structures/env_id.ml.html @@ -106,20 +106,20 @@

77.78%

let empty = { c = Map.empty; last = 0 } let with_fresh_id f { c; last } = - let open Syntax in - let+ e, r = f last in - let c = Map.add last e c in - let last = succ last in - ({ c; last }, r) + let open Syntax in + let+ e, r = f last in + let c = Map.add last e c in + let last = succ last in + ({ c; last }, r) -let get i c = Map.find i c.c +let get i c = Map.find i c.c let map f c = { c with c = Map.map f c.c } module Tbl = Hashtbl.Make (struct include Int - let hash x = x + let hash x = x end) diff --git a/coverage/src/data_structures/func_id.ml.html b/coverage/src/data_structures/func_id.ml.html index eb47f207b..60f1efce9 100644 --- a/coverage/src/data_structures/func_id.ml.html +++ b/coverage/src/data_structures/func_id.ml.html @@ -101,16 +101,16 @@

100.00%

let empty = { c = IMap.empty; last = 0 } let add f t { last; c } = - let c = IMap.add last (f, t) c in - (last, { c; last = succ last }) + let c = IMap.add last (f, t) c in + (last, { c; last = succ last }) let get i c = - let v, _ = IMap.find i c.c in - v + let v, _ = IMap.find i c.c in + v let get_typ i c = - let _, t = IMap.find i c.c in - t + let _, t = IMap.find i c.c in + t diff --git a/coverage/src/data_structures/indexed.ml.html b/coverage/src/data_structures/indexed.ml.html index 81f6c9517..40f5c1c95 100644 --- a/coverage/src/data_structures/indexed.ml.html +++ b/coverage/src/data_structures/indexed.ml.html @@ -95,24 +95,24 @@

92.86%

; value : 'a } -let get v = v.value +let get v = v.value -let get_index v = v.index +let get_index v = v.index let map f v = { index = v.index; value = f v.value } -let return index value = { index; value } +let return index value = { index; value } -let has_index idx { index; _ } = idx = index +let has_index idx { index; _ } = idx = index let get_at_exn i values = - let { value; _ } = List.find (has_index i) values in - value + let { value; _ } = List.find (has_index i) values in + value let get_at i values = - match List.find_opt (has_index i) values with + match List.find_opt (has_index i) values with | None -> None - | Some { value; _ } -> Some value + | Some { value; _ } -> Some value let pp f fmt v = f fmt v.value diff --git a/coverage/src/data_structures/named.ml.html b/coverage/src/data_structures/named.ml.html index d9ae1ca70..400b3ff47 100644 --- a/coverage/src/data_structures/named.ml.html +++ b/coverage/src/data_structures/named.ml.html @@ -80,8 +80,8 @@

100.00%

let empty = { values = []; named = String_map.empty } let fold f v acc = - List.fold_left - (fun acc v -> f (Indexed.get_index v) (Indexed.get v) acc) + List.fold_left + (fun acc v -> f (Indexed.get_index v) (Indexed.get v) acc) acc v.values let map f v = diff --git a/coverage/src/data_structures/stack.ml.html b/coverage/src/data_structures/stack.ml.html index f063b49df..58e61aa87 100644 --- a/coverage/src/data_structures/stack.ml.html +++ b/coverage/src/data_structures/stack.ml.html @@ -581,17 +581,17 @@

82.76%

let empty = [] - let push s v = v :: s + let push s v = v :: s - let push_bool s b = push s (I32 (V.Bool.int32 b)) + let push_bool s b = push s (I32 (V.Bool.int32 b)) - let push_const_i32 s i = push s (I32 (V.const_i32 i)) + let push_const_i32 s i = push s (I32 (V.const_i32 i)) - let push_i32 s i = push s (I32 i) + let push_i32 s i = push s (I32 i) let push_i32_of_int s i = push_const_i32 s (Int32.of_int i) - let push_const_i64 s i = push s (I64 (V.const_i64 i)) + let push_const_i64 s i = push s (I64 (V.const_i64 i)) let push_i64 s i = push s (I64 i) @@ -610,27 +610,27 @@

82.76%

let pp fmt (s : t) = Format.pp_list ~pp_sep:(fun fmt () -> Format.pp_string fmt " ; ") V.pp fmt s - let pop = function [] -> raise Empty | hd :: tl -> (hd, tl) + let pop = function [] -> raise Empty | hd :: tl -> (hd, tl) - let drop = function [] -> raise Empty | _hd :: tl -> tl + let drop = function [] -> raise Empty | _hd :: tl -> tl let pop_i32 s = - let hd, tl = pop s in - match hd with - | I32 n -> (n, tl) + let hd, tl = pop s in + match hd with + | I32 n -> (n, tl) | _ -> Log.err "invalid type (expected i32)" let pop2_i32 s = - let n2, s = pop s in - let n1, tl = pop s in - match (n1, n2) with - | I32 n1, I32 n2 -> ((n1, n2), tl) + let n2, s = pop s in + let n1, tl = pop s in + match (n1, n2) with + | I32 n1, I32 n2 -> ((n1, n2), tl) | _ -> Log.err "invalid type (expected i32)" let pop_i64 s = - let hd, tl = pop s in - match hd with - | I64 n -> (n, tl) + let hd, tl = pop s in + match hd with + | I64 n -> (n, tl) | _ -> Log.err "invalid type (expected i64)" let pop2_i64 s = @@ -679,19 +679,19 @@

82.76%

| _ -> Log.err "invalid type (expected ref)" let pop_bool s = - let hd, tl = pop s in - match hd with - | I32 n -> (V.I32.to_bool n, tl) + let hd, tl = pop s in + match hd with + | I32 n -> (V.I32.to_bool n, tl) | _ -> Log.err "invalid type (expected i32 (bool))" let pop_n s n = - (List.filteri (fun i _hd -> i < n) s, List.filteri (fun i _hd -> i >= n) s) + (List.filteri (fun i _hd -> i < n) s, List.filteri (fun i _hd -> i >= n) s) - let keep s n = List.filteri (fun i _hd -> i < n) s + let keep s n = List.filteri (fun i _hd -> i < n) s let rec drop_n s n = - if n = 0 then s - else match s with [] -> invalid_arg "drop_n" | _ :: tl -> drop_n tl (n - 1) + if n = 0 then s + else match s with [] -> invalid_arg "drop_n" | _ :: tl -> drop_n tl (n - 1) end diff --git a/coverage/src/interpret/interpret.ml.html b/coverage/src/interpret/interpret.ml.html index 4218d2a45..a8e2caa3c 100644 --- a/coverage/src/interpret/interpret.ml.html +++ b/coverage/src/interpret/interpret.ml.html @@ -3333,9 +3333,9 @@

91.59%

let ( = ) = eq - let eqz v = v = zero + let eqz v = v = zero - let min_int = const_i32 Int32.min_int + let min_int = const_i32 Int32.min_int end module I64 = struct @@ -3365,33 +3365,33 @@

91.59%

let eqz v = v = zero - let min_int = const_i64 Int64.min_int + let min_int = const_i64 Int64.min_int end - let page_size = const_i64 65_536L + let page_size = const_i64 65_536L let pop_choice stack = - let b, stack = Stack.pop_bool stack in - let* b = select b in - return (b, stack) + let b, stack = Stack.pop_bool stack in + let* b = select b in + return (b, stack) - let p_type_eq (_id1, t1) (_id2, t2) = t1 = t2 + let p_type_eq (_id1, t1) (_id2, t2) = t1 = t2 let ( let> ) v f = - let* v = select v in - f v + let* v = select v in + f v let const = const_i32 - let consti i = const_i32 (Int32.of_int i) + let consti i = const_i32 (Int32.of_int i) let exec_iunop stack nn op = - match nn with - | S32 -> + match nn with + | S32 -> let n, stack = Stack.pop_i32 stack in - let res = + let res = let open I32 in - match op with Clz -> clz n | Ctz -> ctz n | Popcnt -> popcnt n + match op with Clz -> clz n | Ctz -> ctz n | Popcnt -> popcnt n in Stack.push_i32 stack res | S64 -> @@ -3434,15 +3434,15 @@

91.59%

Stack.push_f64 stack res let exec_ibinop (stack : Stack.t) nn (op : ibinop) : Stack.t Choice.t = - match nn with - | S32 -> + match nn with + | S32 -> let (n1, n2), stack = Stack.pop2_i32 stack in - let+ res = + let+ res = let open I32 in match op with - | Add -> Choice.return @@ add n1 n2 - | Sub -> Choice.return @@ sub n1 n2 - | Mul -> Choice.return @@ mul n1 n2 + | Add -> Choice.return @@ add n1 n2 + | Sub -> Choice.return @@ sub n1 n2 + | Mul -> Choice.return @@ mul n1 n2 | Div s -> begin let> cond = eqz n2 in if cond then Choice.trap Integer_divide_by_zero @@ -3454,24 +3454,24 @@

91.59%

else Choice.return @@ div n1 n2 | U -> Choice.return @@ unsigned_div n1 n2 end - | Rem s -> begin - let> cond = eqz n2 in - if cond then Choice.trap Integer_divide_by_zero + | Rem s -> begin + let> cond = eqz n2 in + if cond then Choice.trap Integer_divide_by_zero else - match s with - | S -> Choice.return @@ rem n1 n2 + match s with + | S -> Choice.return @@ rem n1 n2 | U -> Choice.return @@ unsigned_rem n1 n2 end - | And -> Choice.return @@ logand n1 n2 + | And -> Choice.return @@ logand n1 n2 | Or -> Choice.return @@ logor n1 n2 - | Xor -> Choice.return @@ logxor n1 n2 - | Shl -> Choice.return @@ shl n1 n2 - | Shr S -> Choice.return @@ shr_s n1 n2 - | Shr U -> Choice.return @@ shr_u n1 n2 + | Xor -> Choice.return @@ logxor n1 n2 + | Shl -> Choice.return @@ shl n1 n2 + | Shr S -> Choice.return @@ shr_s n1 n2 + | Shr U -> Choice.return @@ shr_u n1 n2 | Rotl -> Choice.return @@ rotl n1 n2 | Rotr -> Choice.return @@ rotr n1 n2 in - Stack.push_i32 stack res + Stack.push_i32 stack res | S64 -> let (n1, n2), stack = Stack.pop2_i64 stack in let+ res = @@ -3541,10 +3541,10 @@

91.59%

| Copysign -> copy_sign f1 f2 ) let exec_itestop stack nn op = - match nn with - | S32 -> + match nn with + | S32 -> let n, stack = Stack.pop_i32 stack in - let res = match op with Eqz -> I32.eq_const n 0l in + let res = match op with Eqz -> I32.eq_const n 0l in Stack.push_bool stack res | S64 -> let n, stack = Stack.pop_i64 stack in @@ -3552,22 +3552,22 @@

91.59%

Stack.push_bool stack res let exec_irelop stack nn (op : irelop) = - match nn with - | S32 -> + match nn with + | S32 -> let (n1, n2), stack = Stack.pop2_i32 stack in - let res = + let res = let open I32 in match op with - | Eq -> eq n1 n2 - | Ne -> ne n1 n2 - | Lt S -> lt n1 n2 - | Lt U -> lt_u n1 n2 - | Gt S -> gt n1 n2 + | Eq -> eq n1 n2 + | Ne -> ne n1 n2 + | Lt S -> lt n1 n2 + | Lt U -> lt_u n1 n2 + | Gt S -> gt n1 n2 | Gt U -> gt_u n1 n2 | Le S -> le n1 n2 | Le U -> le_u n1 n2 - | Ge S -> ge n1 n2 - | Ge U -> ge_u n1 n2 + | Ge S -> ge n1 n2 + | Ge U -> ge_u n1 n2 in Stack.push_bool stack res | S64 -> @@ -3761,8 +3761,8 @@

91.59%

end let init_local (_id, t) : Value.t = - match t with - | Num_type I32 -> I32 I32.zero + match t with + | Num_type I32 -> I32 I32.zero | Num_type I64 -> I64 I64.zero | Num_type F32 -> F32 F32.zero | Num_type F64 -> F64 F64.zero @@ -3774,10 +3774,10 @@

91.59%

type extern_func = Extern_func.extern_func let exec_extern_func stack (f : extern_func) = - let pop_arg (type ty) stack (arg : ty Extern_func.telt) : + let pop_arg (type ty) stack (arg : ty Extern_func.telt) : (ty * Stack.t) Choice.t = - match arg with - | I32 -> Choice.return @@ Stack.pop_i32 stack + match arg with + | I32 -> Choice.return @@ Stack.pop_i32 stack | I64 -> Choice.return @@ Stack.pop_i64 stack | F32 -> Choice.return @@ Stack.pop_f32 stack | F64 -> Choice.return @@ Stack.pop_f64 stack @@ -3791,45 +3791,45 @@

91.59%

let rec split_args : type f r. Stack.t -> (f, r) Extern_func.atype -> Stack.t * Stack.t = fun stack ty -> - let[@local] split_one_arg args = - let elt, stack = Stack.pop stack in - let elts, stack = split_args stack args in - (elt :: elts, stack) + let[@local] split_one_arg args = + let elt, stack = Stack.pop stack in + let elts, stack = split_args stack args in + (elt :: elts, stack) in match ty with - | Extern_func.Arg (_, args) -> split_one_arg args - | UArg args -> split_args stack args + | Extern_func.Arg (_, args) -> split_one_arg args + | UArg args -> split_args stack args | NArg (_, _, args) -> split_one_arg args - | Res -> ([], stack) + | Res -> ([], stack) in let rec apply : type f r. Stack.t -> (f, r) Extern_func.atype -> f -> r Choice.t = fun stack ty f -> - match ty with - | Extern_func.Arg (arg, args) -> - let* v, stack = pop_arg stack arg in - apply stack args (f v) - | UArg args -> apply stack args (f ()) + match ty with + | Extern_func.Arg (arg, args) -> + let* v, stack = pop_arg stack arg in + apply stack args (f v) + | UArg args -> apply stack args (f ()) | NArg (_, arg, args) -> let* v, stack = pop_arg stack arg in apply stack args (f v) - | Res -> Choice.return f + | Res -> Choice.return f in let (Extern_func.Extern_func (Func (atype, rtype), func)) = f in let args, stack = split_args stack atype in - let* r = apply (List.rev args) atype func in - let push_val (type ty) (arg : ty Extern_func.telt) (v : ty) stack = - match arg with - | I32 -> Stack.push_i32 stack v + let* r = apply (List.rev args) atype func in + let push_val (type ty) (arg : ty Extern_func.telt) (v : ty) stack = + match arg with + | I32 -> Stack.push_i32 stack v | I64 -> Stack.push_i64 stack v | F32 -> Stack.push_f32 stack v | F64 -> Stack.push_f64 stack v | Externref ty -> Stack.push_as_externref stack ty v in let+ r in - match (rtype, r) with - | R0, () -> stack - | R1 t1, v1 -> push_val t1 v1 stack + match (rtype, r) with + | R0, () -> stack + | R1 t1, v1 -> push_val t1 v1 stack | R2 (t1, t2), (v1, v2) -> push_val t1 v1 stack |> push_val t2 v2 | R3 (t1, t2, t3), (v1, v2, v3) -> push_val t1 v1 stack |> push_val t2 v2 |> push_val t3 v3 @@ -3854,12 +3854,12 @@

91.59%

let of_list = Array.of_list - let get t i = Array.unsafe_get t i + let get t i = Array.unsafe_get t i let set t i v = - let locals = Array.copy t in - Array.unsafe_set locals i v; - locals + let locals = Array.copy t in + Array.unsafe_set locals i v; + locals end type pc = binary instr list @@ -3936,19 +3936,19 @@

91.59%

calls count.calls let empty_count name = - { name; enter = 0; instructions = 0; calls = Hashtbl.create 0 } + { name; enter = 0; instructions = 0; calls = Hashtbl.create 0 } let count_instruction state = - state.count.instructions <- state.count.instructions + 1 + state.count.instructions <- state.count.instructions + 1 let enter_function_count count func_name func = - let c = + let c = match Hashtbl.find_opt count.calls func with - | None -> + | None -> let c = empty_count func_name in - Hashtbl.add count.calls func c; - c - | Some c -> c + Hashtbl.add count.calls func c; + c + | Some c -> c in c.enter <- c.enter + 1; c @@ -3958,50 +3958,50 @@

91.59%

| Continue of exec_state let return (state : exec_state) = - let args = Stack.keep state.stack (List.length state.func_rt) in - match state.return_state with - | None -> Return args - | Some state -> + let args = Stack.keep state.stack (List.length state.func_rt) in + match state.return_state with + | None -> Return args + | Some state -> let stack = args @ state.stack in Continue { state with stack } let branch (state : exec_state) n = - let block_stack = Stack.drop_n state.block_stack n in - match block_stack with + let block_stack = Stack.drop_n state.block_stack n in + match block_stack with | [] -> Choice.return (return state) - | block :: block_stack_tl -> + | block :: block_stack_tl -> let block_stack = - if block.is_loop then block_stack else block_stack_tl + if block.is_loop then block_stack else block_stack_tl in - let args = Stack.keep state.stack (List.length block.branch_rt) in - let stack = args @ block.stack in + let args = Stack.keep state.stack (List.length block.branch_rt) in + let stack = args @ block.stack in Choice.return (Continue { state with block_stack; pc = block.branch; stack }) let end_block (state : exec_state) = - match state.block_stack with - | [] -> Choice.return (return state) - | block :: block_stack -> - let args = Stack.keep state.stack (List.length block.continue_rt) in - let stack = args @ block.stack in + match state.block_stack with + | [] -> Choice.return (return state) + | block :: block_stack -> + let args = Stack.keep state.stack (List.length block.continue_rt) in + let stack = args @ block.stack in Choice.return (Continue { state with block_stack; pc = block.continue; stack }) end let exec_block (state : State.exec_state) ~is_loop (bt : binary block_type option) expr = - let pt, rt = + let pt, rt = match bt with | None -> ([], []) - | Some (Bt_raw ((None | Some _), (pt, rt))) -> (List.map snd pt, rt) + | Some (Bt_raw ((None | Some _), (pt, rt))) -> (List.map snd pt, rt) in let block : State.block = - let branch_rt, branch = if is_loop then (pt, expr) else (rt, state.pc) in + let branch_rt, branch = if is_loop then (pt, expr) else (rt, state.pc) in { branch ; branch_rt ; continue = state.pc ; continue_rt = rt - ; stack = Stack.drop_n state.stack (List.length pt) + ; stack = Stack.drop_n state.stack (List.length pt) ; is_loop } in @@ -4011,17 +4011,17 @@

91.59%

let exec_func ~return ~id (state : State.exec_state) env (func : binary Types.func) = - Log.debug1 "calling func : func %s@." - (Option.value func.id ~default:"anonymous"); - let (Bt_raw ((None | Some _), (param_type, result_type))) = func.type_f in - let args, stack = Stack.pop_n state.stack (List.length param_type) in - let return_state = - if return then state.return_state else Some { state with stack } + Log.debug1 "calling func : func %s@." + (Option.value func.id ~default:"anonymous"); + let (Bt_raw ((None | Some _), (param_type, result_type))) = func.type_f in + let args, stack = Stack.pop_n state.stack (List.length param_type) in + let return_state = + if return then state.return_state else Some { state with stack } in let locals = - State.Locals.of_list @@ List.rev args @ List.map init_local func.locals + State.Locals.of_list @@ List.rev args @ List.map init_local func.locals in - State. + State. { stack = [] ; locals ; pc = func.body @@ -4030,24 +4030,24 @@

91.59%

; return_state ; env ; envs = state.envs - ; count = enter_function_count state.count func.id id + ; count = enter_function_count state.count func.id id } let exec_vfunc ~return (state : State.exec_state) (func : Func_intf.t) = - match func with - | WASM (id, func, env_id) -> + match func with + | WASM (id, func, env_id) -> let env = Env_id.get env_id state.envs in - let id = Raw id in - Choice.return (State.Continue (exec_func ~return ~id state env func)) - | Extern f -> + let id = Raw id in + Choice.return (State.Continue (exec_func ~return ~id state env func)) + | Extern f -> let f = Env.get_extern_func state.env f in - let+ stack = exec_extern_func state.stack f in - let state = { state with stack } in - if return then State.return state else State.Continue state + let+ stack = exec_extern_func state.stack f in + let state = { state with stack } in + if return then State.return state else State.Continue state let func_type (state : State.exec_state) (f : Func_intf.t) = - match f with - | WASM (_, func, _) -> + match f with + | WASM (_, func, _) -> let (Bt_raw ((None | Some _), t)) = func.type_f in t | Extern f -> @@ -4075,56 +4075,56 @@

91.59%

let call_indirect ~return (state : State.exec_state) (tbl_i, (Bt_raw ((None | Some _), typ_i) : binary block_type)) = - let fun_i, stack = Stack.pop_i32 state.stack in - let state = { state with stack } in - let* t = Env.get_table state.env tbl_i in - let _null, ref_kind = Table.typ t in - if ref_kind <> Func_ht then Choice.trap Indirect_call_type_mismatch + let fun_i, stack = Stack.pop_i32 state.stack in + let state = { state with stack } in + let* t = Env.get_table state.env tbl_i in + let _null, ref_kind = Table.typ t in + if ref_kind <> Func_ht then Choice.trap Indirect_call_type_mismatch else - let size = Table.size t in - let> out_of_bounds = - Bool.or_ I32.(fun_i < const 0l) @@ I32.(consti size <= fun_i) + let size = Table.size t in + let> out_of_bounds = + Bool.or_ I32.(fun_i < const 0l) @@ I32.(consti size <= fun_i) in - if out_of_bounds then Choice.trap Undefined_element + if out_of_bounds then Choice.trap Undefined_element else - let* fun_i = Choice.select_i32 fun_i in - let fun_i = Int32.to_int fun_i in - let f_ref = Table.get t fun_i in - match Ref.get_func f_ref with + let* fun_i = Choice.select_i32 fun_i in + let fun_i = Int32.to_int fun_i in + let f_ref = Table.get t fun_i in + match Ref.get_func f_ref with | Null -> Choice.trap (Uninitialized_element fun_i) | Type_mismatch -> Choice.trap Element_type_error - | Ref_value func -> + | Ref_value func -> let pt, rt = func_type state func in - let pt', rt' = typ_i in - if not (rt = rt' && List.equal p_type_eq pt pt') then + let pt', rt' = typ_i in + if not (rt = rt' && List.equal p_type_eq pt pt') then Choice.trap Indirect_call_type_mismatch - else exec_vfunc ~return state func + else exec_vfunc ~return state func let exec_instr instr (state : State.exec_state) : State.instr_result Choice.t = - State.count_instruction state; - let stack = state.stack in + State.count_instruction state; + let stack = state.stack in let env = state.env in let locals = state.locals in - let st stack = Choice.return (State.Continue { state with stack }) in + let st stack = Choice.return (State.Continue { state with stack }) in Log.debug2 "stack : [ %a ]@." Stack.pp stack; - Log.debug2 "running instr: %a@." Types.pp_instr instr; - match instr with + Log.debug2 "running instr: %a@." Types.pp_instr instr; + match instr with | Return -> Choice.return (State.return state) | Nop -> Choice.return (State.Continue state) | Unreachable -> Choice.trap Unreachable - | I32_const n -> st @@ Stack.push_const_i32 stack n - | I64_const n -> st @@ Stack.push_const_i64 stack n + | I32_const n -> st @@ Stack.push_const_i32 stack n + | I64_const n -> st @@ Stack.push_const_i64 stack n | F32_const f -> st @@ Stack.push_const_f32 stack f | F64_const f -> st @@ Stack.push_const_f64 stack f - | I_unop (nn, op) -> st @@ exec_iunop stack nn op + | I_unop (nn, op) -> st @@ exec_iunop stack nn op | F_unop (nn, op) -> st @@ exec_funop stack nn op - | I_binop (nn, op) -> - let* stack = exec_ibinop stack nn op in - st stack + | I_binop (nn, op) -> + let* stack = exec_ibinop stack nn op in + st stack | F_binop (nn, op) -> st @@ exec_fbinop stack nn op - | I_testop (nn, op) -> st @@ exec_itestop stack nn op - | I_relop (nn, op) -> st @@ exec_irelop stack nn op + | I_testop (nn, op) -> st @@ exec_itestop stack nn op + | I_relop (nn, op) -> st @@ exec_irelop stack nn op | F_relop (nn, op) -> st @@ exec_frelop stack nn op | I_extend8_s nn -> begin match nn with @@ -4183,31 +4183,31 @@

91.59%

| Ref_func (Raw i) -> let f = Env.get_func env i in st @@ Stack.push stack (ref_func f) - | Drop -> st @@ Stack.drop stack - | Local_get (Raw i) -> st @@ Stack.push stack (State.Locals.get locals i) - | Local_set (Raw i) -> + | Drop -> st @@ Stack.drop stack + | Local_get (Raw i) -> st @@ Stack.push stack (State.Locals.get locals i) + | Local_set (Raw i) -> let v, stack = Stack.pop stack in - let locals = State.Locals.set locals i v in - Choice.return (State.Continue { state with locals; stack }) + let locals = State.Locals.set locals i v in + Choice.return (State.Continue { state with locals; stack }) | If_else (_id, bt, e1, e2) -> let* b, stack = pop_choice stack in let state = { state with stack } in exec_block state ~is_loop:false bt (if b then e1 else e2) - | Call (Raw i) -> begin + | Call (Raw i) -> begin let func = Env.get_func env i in - exec_vfunc ~return:false state func + exec_vfunc ~return:false state func end | Return_call (Raw i) -> begin let func = Env.get_func env i in exec_vfunc ~return:true state func end - | Br (Raw i) -> State.branch state i - | Br_if (Raw i) -> - let* b, stack = pop_choice stack in - let state = { state with stack } in - if b then State.branch state i else Choice.return (State.Continue state) - | Loop (_id, bt, e) -> exec_block state ~is_loop:true bt e - | Block (_id, bt, e) -> exec_block state ~is_loop:false bt e + | Br (Raw i) -> State.branch state i + | Br_if (Raw i) -> + let* b, stack = pop_choice stack in + let state = { state with stack } in + if b then State.branch state i else Choice.return (State.Continue state) + | Loop (_id, bt, e) -> exec_block state ~is_loop:true bt e + | Block (_id, bt, e) -> exec_block state ~is_loop:false bt e | Memory_size -> let* mem = Env.get_memory env mem_0 in let len = Memory.size_in_pages mem in @@ -4276,13 +4276,13 @@

91.59%

let> out_of_bounds = Memory.blit_string mem data ~src ~dst ~len in if out_of_bounds then Choice.trap Out_of_bounds_memory_access else st stack - | Select _t -> - if use_ite_for_select then begin + | Select _t -> + if use_ite_for_select then begin let b, stack = Stack.pop_bool stack in - let o2, stack = Stack.pop stack in - let o1, stack = Stack.pop stack in - let* res = P.select b ~if_true:o1 ~if_false:o2 in - st @@ Stack.push stack res + let o2, stack = Stack.pop stack in + let o1, stack = Stack.pop stack in + let* res = P.select b ~if_true:o1 ~if_false:o2 in + st @@ Stack.push stack res end else begin let* b, stack = pop_choice stack in @@ -4290,25 +4290,25 @@

91.59%

let o1, stack = Stack.pop stack in st @@ Stack.push stack (if b then o1 else o2) end - | Local_tee (Raw i) -> + | Local_tee (Raw i) -> let v, stack = Stack.pop stack in - let locals = State.Locals.set locals i v in - let stack = Stack.push stack v in - Choice.return (State.Continue { state with locals; stack }) - | Global_get (Raw i) -> - let* g = Env.get_global env i in - st @@ Stack.push stack (Global.value g) - | Global_set (Raw i) -> - let* global = Env.get_global env i in - if Global.mut global = Const then Log.err "Can't set const global"; - let v, stack = + let locals = State.Locals.set locals i v in + let stack = Stack.push stack v in + Choice.return (State.Continue { state with locals; stack }) + | Global_get (Raw i) -> + let* g = Env.get_global env i in + st @@ Stack.push stack (Global.value g) + | Global_set (Raw i) -> + let* global = Env.get_global env i in + if Global.mut global = Const then Log.err "Can't set const global"; + let v, stack = match Global.typ global with | Ref_type _rt -> Stack.pop_ref stack - | Num_type nt -> ( + | Num_type nt -> ( match nt with - | I32 -> + | I32 -> let v, stack = Stack.pop_i32 stack in - (I32 v, stack) + (I32 v, stack) | I64 -> let v, stack = Stack.pop_i64 stack in (I64 v, stack) @@ -4320,7 +4320,7 @@

91.59%

(F64 v, stack) ) in Global.set_value global v; - st stack + st stack | Table_get (Raw i) -> let* t = Env.get_table env i in let i, stack = Stack.pop_i32 stack in @@ -4478,75 +4478,75 @@

91.59%

match nn with | S32 -> Stack.push_i32 stack res | S64 -> Stack.push_i64 stack (I64.of_int32 res) ) - | I_load8 (nn, sx, { offset; _ }) -> ( - let* mem = Env.get_memory env mem_0 in - let pos, stack = Stack.pop_i32 stack in - let offset = const offset in - let addr = I32.(pos + offset) in + | I_load8 (nn, sx, { offset; _ }) -> ( + let* mem = Env.get_memory env mem_0 in + let pos, stack = Stack.pop_i32 stack in + let offset = const offset in + let addr = I32.(pos + offset) in let> out_of_bounds = - Bool.or_ I32.(offset < const 0l) - @@ Bool.or_ I32.(Memory.size mem < addr + const 1l) - @@ Bool.or_ I32.(pos < const 0l) - @@ Bool.or_ I32.(addr + const 1l < const 0l) - @@ I32.(addr < const 0l) + Bool.or_ I32.(offset < const 0l) + @@ Bool.or_ I32.(Memory.size mem < addr + const 1l) + @@ Bool.or_ I32.(pos < const 0l) + @@ Bool.or_ I32.(addr + const 1l < const 0l) + @@ I32.(addr < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access + if out_of_bounds then Choice.trap Out_of_bounds_memory_access else - let* res = - (if sx = S then Memory.load_8_s else Memory.load_8_u) mem addr + let* res = + (if sx = S then Memory.load_8_s else Memory.load_8_u) mem addr in - st + st @@ match nn with - | S32 -> Stack.push_i32 stack res + | S32 -> Stack.push_i32 stack res | S64 -> Stack.push_i64 stack (I64.of_int32 res) ) - | I_store8 (nn, { offset; _ }) -> - let* mem = Env.get_memory env mem_0 in - let n, stack = + | I_store8 (nn, { offset; _ }) -> + let* mem = Env.get_memory env mem_0 in + let n, stack = match nn with - | S32 -> + | S32 -> let n, stack = Stack.pop_i32 stack in - (n, stack) + (n, stack) | S64 -> let n, stack = Stack.pop_i64 stack in (I64.to_int32 n, stack) in let pos, stack = Stack.pop_i32 stack in - let offset = const offset in - let addr = I32.(pos + offset) in + let offset = const offset in + let addr = I32.(pos + offset) in let> out_of_bounds = - Bool.or_ I32.(offset < const 0l) - @@ Bool.or_ I32.(Memory.size mem < addr + const 1l) - @@ Bool.or_ I32.(pos < const 0l) - @@ Bool.or_ I32.(addr + const 1l < const 0l) - @@ I32.(addr < const 0l) + Bool.or_ I32.(offset < const 0l) + @@ Bool.or_ I32.(Memory.size mem < addr + const 1l) + @@ Bool.or_ I32.(pos < const 0l) + @@ Bool.or_ I32.(addr + const 1l < const 0l) + @@ I32.(addr < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else begin - let* () = Memory.store_8 mem ~addr n in + if out_of_bounds then Choice.trap Out_of_bounds_memory_access + else begin + let* () = Memory.store_8 mem ~addr n in (* Thread memory ? *) - st stack + st stack end - | I_load (nn, { offset; _ }) -> - let* mem = Env.get_memory env mem_0 in - let pos, stack = Stack.pop_i32 stack in - let memory_length = Memory.size mem in - let offset = const offset in - let addr = I32.(pos + offset) in + | I_load (nn, { offset; _ }) -> + let* mem = Env.get_memory env mem_0 in + let pos, stack = Stack.pop_i32 stack in + let memory_length = Memory.size mem in + let offset = const offset in + let addr = I32.(pos + offset) in let> out_of_bounds = - Bool.or_ I32.(offset < const 0l) - @@ Bool.or_ I32.(pos < const 0l) - @@ I32.(addr < const 0l) + Bool.or_ I32.(offset < const 0l) + @@ Bool.or_ I32.(pos < const 0l) + @@ I32.(addr < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else begin + if out_of_bounds then Choice.trap Out_of_bounds_memory_access + else begin match nn with - | S32 -> - let> out_of_bounds = I32.(lt_u memory_length (addr + const 4l)) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access + | S32 -> + let> out_of_bounds = I32.(lt_u memory_length (addr + const 4l)) in + if out_of_bounds then Choice.trap Out_of_bounds_memory_access else - let* res = Memory.load_32 mem addr in - st @@ Stack.push_i32 stack res + let* res = Memory.load_32 mem addr in + st @@ Stack.push_i32 stack res | S64 -> let> out_of_bounds = I32.(lt_u memory_length (addr + const 8l)) in if out_of_bounds then Choice.trap Out_of_bounds_memory_access @@ -4581,39 +4581,39 @@

91.59%

let res = F64.of_bits res in st @@ Stack.push_f64 stack res end - | I_store (nn, { offset; _ }) -> ( - let* mem = Env.get_memory env mem_0 in - let memory_length = Memory.size mem in - let offset = const offset in - let> out_of_bounds = I32.(offset < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access + | I_store (nn, { offset; _ }) -> ( + let* mem = Env.get_memory env mem_0 in + let memory_length = Memory.size mem in + let offset = const offset in + let> out_of_bounds = I32.(offset < const 0l) in + if out_of_bounds then Choice.trap Out_of_bounds_memory_access else - match nn with - | S32 -> + match nn with + | S32 -> let n, stack = Stack.pop_i32 stack in - let pos, stack = Stack.pop_i32 stack in - let addr = I32.(pos + offset) in + let pos, stack = Stack.pop_i32 stack in + let addr = I32.(pos + offset) in let> out_of_bounds = - Bool.or_ I32.(lt_u memory_length (addr + const 4l)) - @@ I32.(pos < const 0l) + Bool.or_ I32.(lt_u memory_length (addr + const 4l)) + @@ I32.(pos < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else begin - let* () = Memory.store_32 mem ~addr n in - st stack + if out_of_bounds then Choice.trap Out_of_bounds_memory_access + else begin + let* () = Memory.store_32 mem ~addr n in + st stack end - | S64 -> + | S64 -> let n, stack = Stack.pop_i64 stack in - let pos, stack = Stack.pop_i32 stack in - let addr = I32.(pos + offset) in + let pos, stack = Stack.pop_i32 stack in + let addr = I32.(pos + offset) in let> out_of_bounds = - Bool.or_ I32.(lt_u memory_length (addr + const 8l)) - @@ I32.(pos < const 0l) + Bool.or_ I32.(lt_u memory_length (addr + const 8l)) + @@ I32.(pos < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else begin - let* () = Memory.store_64 mem ~addr n in - st stack + if out_of_bounds then Choice.trap Out_of_bounds_memory_access + else begin + let* () = Memory.store_64 mem ~addr n in + st stack end ) | F_store (nn, { offset; _ }) -> ( let* mem = Env.get_memory env mem_0 in @@ -4736,13 +4736,13 @@

91.59%

if out then return i else let+ target = Choice.select_i32 target in - let target = Int32.to_int target in - let (Raw i) = inds.(target) in - i + let target = Int32.to_int target in + let (Raw i) = inds.(target) in + i in - let state = { state with stack } in + let state = { state with stack } in State.branch state target - | Call_indirect (Raw tbl_i, typ_i) -> + | Call_indirect (Raw tbl_i, typ_i) -> call_indirect ~return:false state (tbl_i, typ_i) | Return_call_indirect (Raw tbl_i, typ_i) -> call_indirect ~return:true state (tbl_i, typ_i) @@ -4772,25 +4772,25 @@

91.59%

st stack let rec loop (state : State.exec_state) = - match state.pc with - | instr :: pc -> begin - let* state = exec_instr instr { state with pc } in - match state with - | State.Continue state -> loop state + match state.pc with + | instr :: pc -> begin + let* state = exec_instr instr { state with pc } in + match state with + | State.Continue state -> loop state | State.Return res -> Choice.return res end - | [] -> ( + | [] -> ( Log.debug2 "stack : [ %a ]@." Stack.pp state.stack; - let* state = State.end_block state in - match state with - | State.Continue state -> loop state - | State.Return res -> Choice.return res ) + let* state = State.end_block state in + match state with + | State.Continue state -> loop state + | State.Return res -> Choice.return res ) let exec_expr envs env locals stack expr bt = - let count = State.empty_count (Some "start") in - count.enter <- count.enter + 1; + let count = State.empty_count (Some "start") in + count.enter <- count.enter + 1; let state : State.exec_state = - let func_rt = match bt with None -> [] | Some rt -> rt in + let func_rt = match bt with None -> [] | Some rt -> rt in { stack ; locals ; env @@ -4802,36 +4802,36 @@

91.59%

; count } in - let+ state = loop state in - (state, count) + let+ state = loop state in + (state, count) let modul envs (modul : Module_to_run.t) = - Log.debug0 "interpreting ...@\n"; + Log.debug0 "interpreting ...@\n"; - try + try begin let+ () = - List.fold_left + List.fold_left (fun u to_run -> - let* () = u in - let+ end_stack, count = + let* () = u in + let+ end_stack, count = let env = Module_to_run.env modul in - exec_expr envs env (State.Locals.of_list []) Stack.empty to_run + exec_expr envs env (State.Locals.of_list []) Stack.empty to_run None in - Log.profile3 "Exec module %s@.%a@." - (Option.value (Module_to_run.modul modul).id + Log.profile3 "Exec module %s@.%a@." + (Option.value (Module_to_run.modul modul).id ~default:"anonymous" ) State.print_count count; - match end_stack with - | [] -> () + match end_stack with + | [] -> () | _ :: _ -> Format.pp_err "non empty stack@\n%a@." Stack.pp end_stack; assert false ) - (Choice.return ()) - (Module_to_run.to_run modul) + (Choice.return ()) + (Module_to_run.to_run modul) in - Ok () + Ok () end with | Trap msg -> Choice.return (Error (`Msg msg)) diff --git a/coverage/src/link/link.ml.html b/coverage/src/link/link.ml.html index b4d7e7afd..f21b0a664 100644 --- a/coverage/src/link/link.ml.html +++ b/coverage/src/link/link.ml.html @@ -1005,15 +1005,15 @@

85.29%

} let load_from_module ls f (import : _ Imported.t) = - match StringMap.find import.modul ls.by_name with + match StringMap.find import.modul ls.by_name with | exception Not_found -> Error (`Unknown_module import.modul) - | exports -> ( - match StringMap.find import.name (f exports) with + | exports -> ( + match StringMap.find import.name (f exports) with | exception Not_found -> if StringSet.mem import.name exports.defined_names then Error `Incompatible_import_type else Error (`Unknown_import (import.modul, import.name)) - | v -> Ok v ) + | v -> Ok v ) let load_global (ls : 'f state) (import : binary global_type Imported.t) : global Result.t = @@ -1055,8 +1055,8 @@

85.29%

(* TODO: binary+const instr *) let instr env stack instr = - match instr with - | I32_const n -> ok @@ Stack.push_i32 stack n + match instr with + | 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 @@ -1088,31 +1088,31 @@

85.29%

(* TODO: binary+const expr *) let expr env e : Concrete_value.t Result.t = - let* stack = list_fold_left (instr env) Stack.empty e in - match stack with + let* stack = list_fold_left (instr env) Stack.empty e in + match stack with | [] -> Error (`Type_mismatch "const expr returning zero values") | _ :: _ :: _ -> Error (`Type_mismatch "const expr returning more than one value") - | [ result ] -> Ok result + | [ result ] -> Ok result end let eval_global ls env (global : (Binary.global, binary global_type) Runtime.t) : global Result.t = - match global with - | Local global -> - let* value = Eval_const.expr env global.init in - let mut, typ = global.typ in + match global with + | Local global -> + let* value = Eval_const.expr env global.init in + let mut, typ = global.typ in let global : global = { value; label = global.id; mut; typ } in Ok global | Imported import -> load_global ls import let eval_globals ls env globals : Link_env.Build.t Result.t = - Named.fold + Named.fold (fun id global env -> - let* env in - let* global = eval_global ls env global in - let env = Link_env.Build.add_global id global env in - Ok env ) + let* env in + let* global = eval_global ls env global in + let env = Link_env.Build.add_global id global env in + Ok env ) globals (Ok env) (* @@ -1144,17 +1144,17 @@

85.29%

let eval_memory ls (memory : (mem, limits) Runtime.t) : Concrete_memory.t Result.t = - match memory with - | Local (_label, mem_type) -> ok @@ Concrete_memory.init mem_type + match memory with + | Local (_label, mem_type) -> ok @@ Concrete_memory.init mem_type | Imported import -> load_memory ls import let eval_memories ls env memories = - Named.fold + Named.fold (fun id mem env -> - let* env in - let* memory = eval_memory ls mem in - let env = Link_env.Build.add_memory id memory env in - Ok env ) + let* env in + let* memory = eval_memory ls mem in + let env = Link_env.Build.add_memory id memory env in + Ok env ) memories (Ok env) let table_types_are_compatible (import, (t1 : binary ref_type)) (imported, t2) = @@ -1168,53 +1168,53 @@

85.29%

else Error `Incompatible_import_type let eval_table ls (table : (_, binary table_type) Runtime.t) : table Result.t = - match table with - | Local (label, table_type) -> ok @@ Concrete_table.init ?label table_type + match table with + | Local (label, table_type) -> ok @@ Concrete_table.init ?label table_type | Imported import -> load_table ls import let eval_tables ls env tables = - Named.fold + Named.fold (fun id table env -> - let* env in - let* table = eval_table ls table in - let env = Link_env.Build.add_table id table env in - Ok env ) + let* env in + let* table = eval_table ls table in + let env = Link_env.Build.add_table id table env in + Ok env ) tables (Ok env) let func_types_are_compatible a b = (* TODO: copied from Simplify_bis.equal_func_types => should factorize *) - let remove_param (pt, rt) = - let pt = List.map (fun (_id, vt) -> (None, vt)) pt in - (pt, rt) + let remove_param (pt, rt) = + let pt = List.map (fun (_id, vt) -> (None, vt)) pt in + (pt, rt) in - remove_param a = remove_param b + remove_param a = remove_param b let load_func (ls : 'f state) (import : binary block_type Imported.t) : func Result.t = - let (Bt_raw ((None | Some _), typ)) = import.desc in - let* func = load_from_module ls (fun (e : exports) -> e.functions) import in - let type' = + let (Bt_raw ((None | Some _), typ)) = import.desc in + let* func = load_from_module ls (fun (e : exports) -> e.functions) import in + let type' = match func with | Func_intf.WASM (_, func, _) -> let (Bt_raw ((None | Some _), t)) = func.type_f in t - | Extern func_id -> Func_id.get_typ func_id ls.collection + | Extern func_id -> Func_id.get_typ func_id ls.collection in - if func_types_are_compatible typ type' then Ok func + if func_types_are_compatible typ type' then Ok func else Error `Incompatible_import_type let eval_func ls (finished_env : Link_env.t') func : func Result.t = - match func with - | Runtime.Local func -> ok @@ Concrete_value.Func.wasm func finished_env - | Imported import -> load_func ls import + match func with + | Runtime.Local func -> ok @@ Concrete_value.Func.wasm func finished_env + | Imported import -> load_func ls import let eval_functions ls (finished_env : Link_env.t') env functions = - Named.fold + Named.fold (fun id func env -> - let* env in - let* func = eval_func ls finished_env func in - let env = Link_env.Build.add_func id func env in - Ok env ) + let* env in + let* func = eval_func ls finished_env func in + let env = Link_env.Build.add_func id func env in + Ok env ) functions (Ok env) let active_elem_expr ~offset ~length ~table ~elem = @@ -1241,7 +1241,7 @@

85.29%

| _ -> Error (`Type_mismatch "get_i32") let define_data env data = - Named.fold + Named.fold (fun id (data : Binary.data) env_and_init -> let* env, init = env_and_init in let data' : Link_env.data = { value = data.init } in @@ -1263,7 +1263,7 @@

85.29%

(Ok (env, [])) let define_elem env elem = - Named.fold + Named.fold (fun id (elem : Binary.elem) env_and_inits -> let* env, inits = env_and_inits in let* init = list_map (Eval_const.expr env) elem.init in @@ -1298,83 +1298,83 @@

85.29%

(Ok (env, [])) let populate_exports env (exports : Binary.exports) : exports Result.t = - let fill_exports get_env exports names = - list_fold_left + let fill_exports get_env exports names = + list_fold_left (fun (acc, names) (export : Binary.export) -> - let value = get_env env export.id in - if StringSet.mem export.name names then Error `Duplicate_export_name + let value = get_env env export.id in + if StringSet.mem export.name names then Error `Duplicate_export_name else - Ok - ( StringMap.add export.name value acc - , StringSet.add export.name names ) ) + Ok + ( StringMap.add export.name value acc + , StringSet.add export.name names ) ) (StringMap.empty, names) exports in let names = StringSet.empty in - let* globals, names = fill_exports Link_env.get_global exports.global names in - let* memories, names = fill_exports Link_env.get_memory exports.mem names in - let* tables, names = fill_exports Link_env.get_table exports.table names in - let* functions, names = fill_exports Link_env.get_func exports.func names in - Ok { globals; memories; tables; functions; defined_names = names } + let* globals, names = fill_exports Link_env.get_global exports.global names in + let* memories, names = fill_exports Link_env.get_memory exports.mem names in + let* tables, names = fill_exports Link_env.get_table exports.table names in + let* functions, names = fill_exports Link_env.get_func exports.func names in + Ok { globals; memories; tables; functions; defined_names = names } let modul (ls : 'f state) ~name (modul : Binary.modul) = - Log.debug0 "linking ...@\n"; - let* envs, (env, init_active_data, init_active_elem) = - Env_id.with_fresh_id + Log.debug0 "linking ...@\n"; + let* envs, (env, init_active_data, init_active_elem) = + Env_id.with_fresh_id (fun env_id -> - let env = Link_env.Build.empty in - let* env = eval_functions ls env_id env modul.func in - let* env = eval_globals ls env modul.global in - let* env = eval_memories ls env modul.mem in - let* env = eval_tables ls env modul.table in - let* env, init_active_data = define_data env modul.data in - let+ env, init_active_elem = define_elem env modul.elem in - let finished_env = Link_env.freeze env_id env ls.collection in - (finished_env, (finished_env, init_active_data, init_active_elem)) ) + let env = Link_env.Build.empty in + let* env = eval_functions ls env_id env modul.func in + let* env = eval_globals ls env modul.global in + let* env = eval_memories ls env modul.mem in + let* env = eval_tables ls env modul.table in + let* env, init_active_data = define_data env modul.data in + let+ env, init_active_elem = define_elem env modul.elem in + let finished_env = Link_env.freeze env_id env ls.collection in + (finished_env, (finished_env, init_active_data, init_active_elem)) ) ls.envs in - let* by_id_exports = populate_exports env modul.exports in - let by_id = + let* by_id_exports = populate_exports env modul.exports in + let by_id = match modul.id with - | None -> ls.by_id + | None -> ls.by_id | Some id -> StringMap.add id (by_id_exports, Link_env.id env) ls.by_id in let by_name = match name with - | None -> ls.by_name + | None -> ls.by_name | Some name -> StringMap.add name by_id_exports ls.by_name in let start = - Option.map (fun start_id -> [ Call (Raw start_id) ]) modul.start + Option.map (fun start_id -> [ Call (Raw start_id) ]) modul.start in - let start = Option.fold ~none:[] ~some:(fun s -> [ s ]) start in - let to_run = (init_active_data @ init_active_elem) @ start in + let start = Option.fold ~none:[] ~some:(fun s -> [ s ]) start in + let to_run = (init_active_data @ init_active_elem) @ start in let module_to_run = { modul; env; to_run } in Ok ( module_to_run , { by_id ; by_name - ; last = Some (by_id_exports, Link_env.id env) + ; last = Some (by_id_exports, Link_env.id env) ; collection = ls.collection ; envs } ) let extern_module' (ls : 'f state) ~name ~(func_typ : 'f -> binary func_type) (module_ : 'f extern_module) = - let functions, collection = + let functions, collection = List.fold_left (fun (functions, collection) (name, func) -> - let typ = func_typ func in - let id, collection = Func_id.add func typ collection in - ((name, Func_intf.Extern id) :: functions, collection) ) + let typ = func_typ func in + let id, collection = Func_id.add func typ collection in + ((name, Func_intf.Extern id) :: functions, collection) ) ([], ls.collection) module_.functions in - let functions = StringMap.of_seq (List.to_seq functions) in - let defined_names = + let functions = StringMap.of_seq (List.to_seq functions) in + let defined_names = StringMap.fold - (fun name _ set -> StringSet.add name set) + (fun name _ set -> StringSet.add name set) functions StringSet.empty in - let exports = + let exports = { functions ; globals = StringMap.empty ; memories = StringMap.empty @@ -1382,7 +1382,7 @@

85.29%

; defined_names } in - { ls with by_name = StringMap.add name exports ls.by_name; collection } + { ls with by_name = StringMap.add name exports ls.by_name; collection } let extern_module ls ~name modul = extern_module' ls ~name ~func_typ:Concrete_value.Func.extern_type modul diff --git a/coverage/src/link/link_env.ml.html b/coverage/src/link/link_env.ml.html index 9ac09b47c..a31d51275 100644 --- a/coverage/src/link/link_env.ml.html +++ b/coverage/src/link/link_env.ml.html @@ -357,21 +357,21 @@

91.18%

; id : Env_id.t } -let id (env : _ t) = env.id +let id (env : _ t) = env.id -let get_global (env : _ t) id = IMap.find id env.globals +let get_global (env : _ t) id = IMap.find id env.globals -let get_memory (env : _ t) id = IMap.find id env.memories +let get_memory (env : _ t) id = IMap.find id env.memories -let get_table (env : _ t) id = IMap.find id env.tables +let get_table (env : _ t) id = IMap.find id env.tables -let get_func (env : _ t) id = IMap.find id env.functions +let get_func (env : _ t) id = IMap.find id env.functions let get_data (env : _ t) id = IMap.find id env.data let get_elem (env : _ t) id = IMap.find id env.elem -let get_extern_func env id = Func_id.get id env.extern_funcs +let get_extern_func env id = Func_id.get id env.extern_funcs module Build = struct type t = @@ -393,16 +393,16 @@

91.18%

} let add_global id const (env : t) = - { env with globals = IMap.add id const env.globals } + { env with globals = IMap.add id const env.globals } let add_memory id mem (env : t) = - { env with memories = IMap.add id mem env.memories } + { env with memories = IMap.add id mem env.memories } let add_table id table (env : t) = - { env with tables = IMap.add id table env.tables } + { env with tables = IMap.add id table env.tables } let add_func id func (env : t) = - { env with functions = IMap.add id func env.functions } + { env with functions = IMap.add id func env.functions } let add_data id data (env : t) = { env with data = IMap.add id data env.data } @@ -473,7 +473,7 @@

91.18%

let freeze id ({ globals; memories; tables; functions; data; elem } : Build.t) extern_funcs = - { id; globals; memories; tables; functions; data; elem; extern_funcs } + { id; globals; memories; tables; functions; data; elem; extern_funcs } diff --git a/coverage/src/parser/binary_parser.ml.html b/coverage/src/parser/binary_parser.ml.html index cbe487da1..bb63216e3 100644 --- a/coverage/src/parser/binary_parser.ml.html +++ b/coverage/src/parser/binary_parser.ml.html @@ -3,7 +3,7 @@ binary_parser.ml — Coverage report - + @@ -15,10 +15,11 @@

src/parser/binary_parser.ml

-

61.17%

+

60.69%

diff --git a/coverage/src/parser/parse.ml.html b/coverage/src/parser/parse.ml.html index 5356d5d41..25a4e2029 100644 --- a/coverage/src/parser/parse.ml.html +++ b/coverage/src/parser/parse.ml.html @@ -219,7 +219,7 @@

82.35%

struct let from_lexbuf = let parser = MenhirLib.Convert.Simplified.traditional2revised M.rule in - fun buf -> + fun buf -> Log.debug0 "parsing ...@\n"; let provider () = let tok = Text_lexer.token buf in @@ -276,16 +276,16 @@

82.35%

end let guess_from_file file = - match Fpath.get_ext ~multi:false file with + match Fpath.get_ext ~multi:false file with | ".wat" -> let+ m = Text.Module.from_file file in Either.Left (Either.Left m) | ".wast" -> let+ m = Text.Script.from_file file in Either.Left (Either.Right m) - | ".wasm" -> - let+ m = Binary.Module.from_file file in - Either.Right m + | ".wasm" -> + let+ m = Binary.Module.from_file file in + Either.Right m | ext -> Error (`Unsupported_file_extension ext) diff --git a/coverage/src/primitives/convert.ml.html b/coverage/src/primitives/convert.ml.html index 8e376cde7..5c25dd598 100644 --- a/coverage/src/primitives/convert.ml.html +++ b/coverage/src/primitives/convert.ml.html @@ -655,7 +655,7 @@

99.63%

let extend_i32_s x = Int64.of_int32 x - let extend_i32_u x = Int64.logand (Int64.of_int32 x) 0x0000_0000_ffff_ffffL + let extend_i32_u x = Int64.logand (Int64.of_int32 x) 0x0000_0000_ffff_ffffL let trunc_f32_s x = if Float32.ne x x then raise @@ Types.Trap "invalid conversion to integer" diff --git a/coverage/src/primitives/float32.ml.html b/coverage/src/primitives/float32.ml.html index c5e7c3a60..a8d95378e 100644 --- a/coverage/src/primitives/float32.ml.html +++ b/coverage/src/primitives/float32.ml.html @@ -718,13 +718,13 @@

91.84%

let bare_nan = 0x7f80_0000l -let to_hex_string = Printf.sprintf "%lx" +let to_hex_string = Printf.sprintf "%lx" type t = Int32.t -let pos_inf = Int32.bits_of_float (1.0 /. 0.0) +let pos_inf = Int32.bits_of_float (1.0 /. 0.0) -let neg_inf = Int32.bits_of_float (-.(1.0 /. 0.0)) +let neg_inf = Int32.bits_of_float (-.(1.0 /. 0.0)) let of_float = Int32.bits_of_float @@ -732,7 +732,7 @@

91.84%

let of_bits x = x -let to_bits x = x +let to_bits x = x let is_inf x = x = pos_inf || x = neg_inf @@ -785,7 +785,7 @@

91.84%

let t = op (to_float x) in if t = t then of_float t else determine_unary_nan x -let zero = of_float 0.0 +let zero = of_float 0.0 let add x y = binary x ( +. ) y @@ -1033,7 +1033,7 @@

91.84%

group_digits is_digit n (if s.[String.length s - 1] = '.' then s ^ "0" else s) -let to_string = to_string' (Printf.sprintf "%.17g") is_digit 3 +let to_string = to_string' (Printf.sprintf "%.17g") is_digit 3 let pp fmt v = Format.pp_string fmt (to_string v) diff --git a/coverage/src/primitives/float64.ml.html b/coverage/src/primitives/float64.ml.html index 01a4b7c0d..28b59654e 100644 --- a/coverage/src/primitives/float64.ml.html +++ b/coverage/src/primitives/float64.ml.html @@ -726,13 +726,13 @@

91.28%

let bare_nan = 0x7ff0_0000_0000_0000L -let to_hex_string = Printf.sprintf "%Lx" +let to_hex_string = Printf.sprintf "%Lx" type t = Int64.t -let pos_inf = Int64.bits_of_float (1.0 /. 0.0) +let pos_inf = Int64.bits_of_float (1.0 /. 0.0) -let neg_inf = Int64.bits_of_float (-.(1.0 /. 0.0)) +let neg_inf = Int64.bits_of_float (-.(1.0 /. 0.0)) let of_float = Int64.bits_of_float @@ -740,7 +740,7 @@

91.28%

let of_bits x = x -let to_bits x = x +let to_bits x = x let is_inf x = x = pos_inf || x = neg_inf @@ -793,7 +793,7 @@

91.28%

let t = op (to_float x) in if t = t then of_float t else determine_unary_nan x -let zero = of_float 0.0 +let zero = of_float 0.0 let add x y = binary x ( +. ) y @@ -1041,7 +1041,7 @@

91.28%

group_digits is_digit n (if s.[String.length s - 1] = '.' then s ^ "0" else s) -let to_string = to_string' (Printf.sprintf "%.17g") is_digit 3 +let to_string = to_string' (Printf.sprintf "%.17g") is_digit 3 let to_hex_string x = if is_inf x then to_string x diff --git a/coverage/src/primitives/int32.ml.html b/coverage/src/primitives/int32.ml.html index 20586fc63..4f0c19ec1 100644 --- a/coverage/src/primitives/int32.ml.html +++ b/coverage/src/primitives/int32.ml.html @@ -367,24 +367,24 @@

98.35%

(* If bit (32 - 1) is set, sx will sign-extend t to maintain the * invariant that small ints are stored sign-extended inside a wider int. *) let sx x = - Int64.to_int32 - @@ Int64.shift_right (Int64.shift_left (Int64.of_int32 x) 32) 32 + Int64.to_int32 + @@ Int64.shift_right (Int64.shift_left (Int64.of_int32 x) 32) 32 (* We don't override min_int and max_int since those are used * by other functions (like parsing), and rely on it being * min/max for int32 *) (* The smallest signed |32|-bits int. *) -let low_int = shift_left minus_one 31 +let low_int = shift_left minus_one 31 (* The largest signed |32|-bits int. *) -let high_int = logxor low_int minus_one +let high_int = logxor low_int minus_one (* WebAssembly's shifts mask the shift count according to the 32. *) -let shift f x y = f x (to_int (logand y 31l)) +let shift f x y = f x (to_int (logand y 31l)) -let shl x y = sx (shift shift_left x y) +let shl x y = sx (shift shift_left x y) -let shr_s x y = shift shift_right x y +let shr_s x y = shift shift_right x y let shr_u x y = sx (shift shift_right_logical x y) @@ -402,7 +402,7 @@

98.35%

let eq (x : int32) y = x = y -let ne (x : int32) y = x <> y +let ne (x : int32) y = x <> y let lt (x : int32) y = x < y @@ -434,9 +434,9 @@

98.35%

| 'A' .. 'F' as c -> 0xa + Char.code c - Char.code 'A' | _ -> Log.err "of_string" -let max_upper = unsigned_div minus_one 10l +let max_upper = unsigned_div minus_one 10l -let max_lower = unsigned_rem minus_one 10l +let max_lower = unsigned_rem minus_one 10l let sign_extend i = let sign_bit = logand (of_int (1 lsl (32 - 1))) i in diff --git a/coverage/src/primitives/int64.ml.html b/coverage/src/primitives/int64.ml.html index 211c8fb29..1694e03ab 100644 --- a/coverage/src/primitives/int64.ml.html +++ b/coverage/src/primitives/int64.ml.html @@ -409,7 +409,7 @@

96.67%

(* * Unsigned comparison in terms of signed comparison. *) -let cmp_u x op y = op (add x min_int) (add y min_int) +let cmp_u x op y = op (add x min_int) (add y min_int) (* * Unsigned division and remainder in terms of signed division; algorithm from @@ -417,29 +417,29 @@

96.67%

* "Unsigned Short Division from Signed Division". *) let divrem_u n d = - if d = zero then raise Division_by_zero + if d = zero then raise Division_by_zero else - let t = shift_right d 63 in - let n' = logand n (lognot t) in - let q = shift_left (div (shift_right_logical n' 1) d) 1 in - let r = sub n (mul q d) in - if cmp_u r ( < ) d then (q, r) else (add q one, sub r d) + let t = shift_right d 63 in + let n' = logand n (lognot t) in + let q = shift_left (div (shift_right_logical n' 1) d) 1 in + let r = sub n (mul q d) in + if cmp_u r ( < ) d then (q, r) else (add q one, sub r d) (* We don't override min_int and max_int since those are used * by other functions (like parsing), and rely on it being * min/max for int32 *) (* The smallest signed |bitwidth|-bits int. *) -let low_int = shift_left minus_one 63 +let low_int = shift_left minus_one 63 (* The largest signed |bitwidth|-bits int. *) -let high_int = logxor low_int minus_one +let high_int = logxor low_int minus_one (* WebAssembly's shifts mask the shift count according to the bitwidth. *) -let shift f x y = f x (to_int (logand y (of_int 63))) +let shift f x y = f x (to_int (logand y (of_int 63))) -let shl x y = shift shift_left x y +let shl x y = shift shift_left x y -let shr_s x y = shift shift_right x y +let shr_s x y = shift shift_right x y let shr_u x y = shift shift_right_logical x y @@ -467,7 +467,7 @@

96.67%

let ge (x : int64) y = x >= y -let lt_u x y = cmp_u x ( < ) y +let lt_u x y = cmp_u x ( < ) y let le_u x y = cmp_u x ( <= ) y @@ -489,7 +489,7 @@

96.67%

| 'A' .. 'F' as c -> 0xa + Char.code c - Char.code 'A' | _ -> Log.err "of_string" -let max_upper, max_lower = divrem_u minus_one 10L +let max_upper, max_lower = divrem_u minus_one 10L let of_string s = let len = String.length s in diff --git a/coverage/src/result.ml.html b/coverage/src/result.ml.html index 9d2c00d6c..92fc07939 100644 --- a/coverage/src/result.ml.html +++ b/coverage/src/result.ml.html @@ -368,9 +368,9 @@

70.18%

| `Duplicate_table id -> Format.sprintf "duplicate table %s" id | `Failed_with_but_expected (got, expected) -> Format.sprintf "expected %s but got (%s)" expected (err_to_string got) - | `Found_bug n -> + | `Found_bug n -> if n > 1 then Format.sprintf "Reached %d problems!" n - else Format.sprintf "Reached problem!" + else Format.sprintf "Reached problem!" | `Global_is_immutable -> "global is immutable" | `Illegal_escape txt -> Format.sprintf "illegal escape %S" txt | `Import_after_function -> "import after function" diff --git a/coverage/src/script/script.ml.html b/coverage/src/script/script.ml.html index 9863f1d07..c59282fb2 100644 --- a/coverage/src/script/script.ml.html +++ b/coverage/src/script/script.ml.html @@ -594,7 +594,7 @@

80.83%

module Host_externref = struct type t = int - let ty : t Type.Id.t = Type.Id.make () + let ty : t Type.Id.t = Type.Id.make () let value i = Concrete_value.Externref (Some (Concrete_value.E (ty, i))) end diff --git a/coverage/src/symbolic/solver.ml.html b/coverage/src/symbolic/solver.ml.html index d5eb0288f..5dfd34ae7 100644 --- a/coverage/src/symbolic/solver.ml.html +++ b/coverage/src/symbolic/solver.ml.html @@ -74,10 +74,10 @@

100.00%

let solver_mod : Z3Batch.t solver_module = (module Z3Batch) let fresh_solver () = - let module Mapping = Smtml.Z3_mappings.Fresh.Make () in + let module Mapping = Smtml.Z3_mappings.Fresh.Make () in let module Batch = Smtml.Solver.Batch (Mapping) in let solver = Batch.create ~logic:QF_BVFP () in - S ((module Batch), solver) + S ((module Batch), solver) diff --git a/coverage/src/symbolic/symbolic.ml.html b/coverage/src/symbolic/symbolic.ml.html index 7524a6572..1ac07a572 100644 --- a/coverage/src/symbolic/symbolic.ml.html +++ b/coverage/src/symbolic/symbolic.ml.html @@ -468,9 +468,9 @@

78.21%

let select (c : Value.vbool) ~(if_true : Value.t) ~(if_false : Value.t) : Value.t Choice.t = - match (if_true, if_false) with - | I32 if_true, I32 if_false -> - Choice.return (Value.I32 (Value.Bool.select_expr c ~if_true ~if_false)) + match (if_true, if_false) with + | I32 if_true, I32 if_false -> + Choice.return (Value.I32 (Value.Bool.select_expr c ~if_true ~if_false)) | I64 if_true, I64 if_false -> Choice.return (Value.I64 (Value.Bool.select_expr c ~if_true ~if_false)) | F32 if_true, F32 if_false -> @@ -499,12 +499,12 @@

78.21%

include Symbolic_memory let concretise (a : Smtml.Expr.t) : Smtml.Expr.t Choice.t = - let open Choice in + let open Choice in let open Smtml in match Expr.view a with (* Avoid unecessary re-hashconsing and allocation when the value is already concrete. *) - | Val _ | Ptr (_, { node = Val _; _ }) -> return a + | Val _ | Ptr (_, { node = Val _; _ }) -> return a | Ptr (base, offset) -> let+ offset = select_i32 offset in Expr.make (Ptr (base, Symbolic_value.const_i32 offset)) @@ -513,43 +513,43 @@

78.21%

Symbolic_value.const_i32 v let check_within_bounds m a = - match check_within_bounds m a with + match check_within_bounds m a with | Error t -> Choice.trap t - | Ok (cond, ptr) -> + | Ok (cond, ptr) -> let open Choice in - let* out_of_bounds = select cond in - if out_of_bounds then trap Trap.Memory_heap_buffer_overflow - else return ptr + let* out_of_bounds = select cond in + if out_of_bounds then trap Trap.Memory_heap_buffer_overflow + else return ptr let with_concrete (m : t) a f : 'a Choice.t = - let open Choice in - let* addr = concretise a in - let+ ptr = check_within_bounds m addr in - f m ptr + let open Choice in + let* addr = concretise a in + let+ ptr = check_within_bounds m addr in + f m ptr - let load_8_s m a = with_concrete m a load_8_s + let load_8_s m a = with_concrete m a load_8_s - let load_8_u m a = with_concrete m a load_8_u + let load_8_u m a = with_concrete m a load_8_u let load_16_s m a = with_concrete m a load_16_s let load_16_u m a = with_concrete m a load_16_u - let load_32 m a = with_concrete m a load_32 + let load_32 m a = with_concrete m a load_32 let load_64 m a = with_concrete m a load_64 let store_8 m ~addr v = - with_concrete m addr (fun m addr -> store_8 m ~addr v) + with_concrete m addr (fun m addr -> store_8 m ~addr v) let store_16 m ~addr v = with_concrete m addr (fun m addr -> store_16 m ~addr v) let store_32 m ~addr v = - with_concrete m addr (fun m addr -> store_32 m ~addr v) + with_concrete m addr (fun m addr -> store_32 m ~addr v) let store_64 m ~addr v = - with_concrete m addr (fun m addr -> store_64 m ~addr v) + with_concrete m addr (fun m addr -> store_64 m ~addr v) end module Data = struct @@ -564,10 +564,10 @@

78.21%

type t' = Env_id.t let get_memory env id = - let orig_mem = Link_env.get_memory env id in - let f (t : thread) = - let memories = Thread.memories t in - Symbolic_memory.get_memory (Link_env.id env) orig_mem memories id + let orig_mem = Link_env.get_memory env id in + let f (t : thread) = + let memories = Thread.memories t in + Symbolic_memory.get_memory (Link_env.id env) orig_mem memories id in Choice.with_thread f @@ -576,10 +576,10 @@

78.21%

let get_extern_func = Link_env.get_extern_func let get_table (env : t) i : Table.t Choice.t = - let orig_table = Link_env.get_table env i in - let f (t : thread) = - let tables = Thread.tables t in - Symbolic_table.get_table (Link_env.id env) orig_table tables i + let orig_table = Link_env.get_table env i in + let f (t : thread) = + let tables = Thread.tables t in + Symbolic_table.get_table (Link_env.id env) orig_table tables i in Choice.with_thread f @@ -590,10 +590,10 @@

78.21%

Choice.return data let get_global (env : t) i : Global.t Choice.t = - let orig_global = Link_env.get_global env i in - let f (t : thread) = - let globals = Thread.globals t in - Symbolic_global.get_global (Link_env.id env) orig_global globals i + let orig_global = Link_env.get_global env i in + let f (t : thread) = + let globals = Thread.globals t in + Symbolic_global.get_global (Link_env.id env) orig_global globals i in Choice.with_thread f @@ -612,11 +612,11 @@

78.21%

; to_run : Types.binary Types.expr list } - let env (t : t) = t.env + let env (t : t) = t.env - let modul (t : t) = t.modul + let modul (t : t) = t.modul - let to_run (t : t) = t.to_run + let to_run (t : t) = t.to_run end end @@ -631,7 +631,7 @@

78.21%

end let convert_module_to_run (m : 'f Link.module_to_run) = - P.Module_to_run.{ modul = m.modul; env = m.env; to_run = m.to_run } + P.Module_to_run.{ modul = m.modul; env = m.env; to_run = m.to_run } let convert_module_to_run_minimalist (m : 'f Link.module_to_run) = M.Module_to_run.{ modul = m.modul; env = m.env; to_run = m.to_run } diff --git a/coverage/src/symbolic/symbolic_choice.ml.html b/coverage/src/symbolic/symbolic_choice.ml.html index 07664d590..1e99975db 100644 --- a/coverage/src/symbolic/symbolic_choice.ml.html +++ b/coverage/src/symbolic/symbolic_choice.ml.html @@ -1308,48 +1308,48 @@

82.19%

} let take q pledge = - Mutex.lock q.mutex; - let r = + Mutex.lock q.mutex; + let r = try - while Queue.is_empty q.queue do - if q.pledges = 0 || q.failed then raise Exit; - Condition.wait q.cond q.mutex + while Queue.is_empty q.queue do + if q.pledges = 0 || q.failed then raise Exit; + Condition.wait q.cond q.mutex done; let v = Queue.pop q.queue in - if pledge then q.pledges <- q.pledges + 1; - Some v - with Exit -> + if pledge then q.pledges <- q.pledges + 1; + Some v + with Exit -> Condition.broadcast q.cond; - None + None in Mutex.unlock q.mutex; - r + r let make_pledge q = - Mutex.lock q.mutex; - q.pledges <- q.pledges + 1; + Mutex.lock q.mutex; + q.pledges <- q.pledges + 1; Mutex.unlock q.mutex let end_pledge q = - Mutex.lock q.mutex; - q.pledges <- q.pledges - 1; + Mutex.lock q.mutex; + q.pledges <- q.pledges - 1; Condition.broadcast q.cond; - Mutex.unlock q.mutex + Mutex.unlock q.mutex let rec read_as_seq (q : 'a t) ?(finalizer = Fun.const ()) : 'a Seq.t = - fun () -> - match take q false with + fun () -> + match take q false with | None -> finalizer (); Nil - | Some v -> Cons (v, read_as_seq q ~finalizer) + | Some v -> Cons (v, read_as_seq q ~finalizer) let push v q = - Mutex.lock q.mutex; - let was_empty = Queue.is_empty q.queue in - Queue.push v q.queue; - if was_empty then Condition.broadcast q.cond; - Mutex.unlock q.mutex + Mutex.lock q.mutex; + let was_empty = Queue.is_empty q.queue in + Queue.push v q.queue; + if was_empty then Condition.broadcast q.cond; + Mutex.unlock q.mutex let fail q = Mutex.lock q.mutex; @@ -1358,9 +1358,9 @@

82.19%

Mutex.unlock q.mutex let init () = - { mutex = Mutex.create () - ; cond = Condition.create () - ; queue = Queue.create () + { mutex = Mutex.create () + ; cond = Condition.create () + ; queue = Queue.create () ; pledges = 0 ; failed = false } @@ -1445,43 +1445,43 @@

82.19%

| Choice of (('a, 'wls) status * ('a, 'wls) status) | Stop - let run (Sched mxf) wls = mxf wls + let run (Sched mxf) wls = mxf wls - let return x : _ t = Sched (Fun.const (Now x)) + let return x : _ t = Sched (Fun.const (Now x)) - let return_status status = Sched (Fun.const status) + let return_status status = Sched (Fun.const status) let rec bind (mx : ('a, 'wls) t) (f : 'a -> ('b, 'wls) t) : _ t = - let rec bind_status (x : _ status) (f : _ -> _ status) : _ status = - match x with - | Now x -> f x - | Yield (prio, lx) -> - Yield (prio, Sched (fun wls -> bind_status (run lx wls) f)) - | Choice (mx1, mx2) -> Choice (bind_status mx1 f, bind_status mx2 f) - | Stop -> Stop + let rec bind_status (x : _ status) (f : _ -> _ status) : _ status = + match x with + | Now x -> f x + | Yield (prio, lx) -> + Yield (prio, Sched (fun wls -> bind_status (run lx wls) f)) + | Choice (mx1, mx2) -> Choice (bind_status mx1 f, bind_status mx2 f) + | Stop -> Stop in Sched (fun wls -> - let argumented_f x = run (f x) wls in + let argumented_f x = run (f x) wls in match run mx wls with - | Yield (prio, mx) -> Yield (prio, bind mx f) - | x -> bind_status x argumented_f ) + | Yield (prio, mx) -> Yield (prio, bind mx f) + | x -> bind_status x argumented_f ) let ( let* ) = bind let map x f = - let* x in - return (f x) + let* x in + return (f x) let ( let+ ) = map - let yield prio = return_status (Yield (prio, Sched (Fun.const (Now ())))) + let yield prio = return_status (Yield (prio, Sched (Fun.const (Now ())))) - let choose a b = Sched (fun wls -> Choice (run a wls, run b wls)) + let choose a b = Sched (fun wls -> Choice (run a wls, run b wls)) - let stop : ('a, 'b) t = return_status Stop + let stop : ('a, 'b) t = return_status Stop - let worker_local : ('a, 'a) t = Sched (fun wls -> Now wls) + let worker_local : ('a, 'a) t = Sched (fun wls -> Now wls) end module Scheduler = struct @@ -1498,37 +1498,37 @@

82.19%

} let init_scheduler () = - let work_queue = WQ.init () in - let res_writer = WQ.init () in - { work_queue; res_writer } + let work_queue = WQ.init () in + let res_writer = WQ.init () in + { work_queue; res_writer } - let add_init_task sched task = WQ.push task sched.work_queue + let add_init_task sched task = WQ.push task sched.work_queue let rec work wls sched = - let rec handle_status (t : _ Schedulable.status) sched = - match t with - | Stop -> () - | Now x -> WQ.push x sched.res_writer - | Yield (_prio, f) -> WQ.push f sched.work_queue - | Choice (m1, m2) -> + let rec handle_status (t : _ Schedulable.status) sched = + match t with + | Stop -> () + | Now x -> WQ.push x sched.res_writer + | Yield (_prio, f) -> WQ.push f sched.work_queue + | Choice (m1, m2) -> handle_status m1 sched; - handle_status m2 sched + handle_status m2 sched in match WQ.take sched.work_queue true with - | None -> () - | Some f -> begin - handle_status (Schedulable.run f wls) sched; - WQ.end_pledge sched.work_queue; - work wls sched + | None -> () + | Some f -> begin + handle_status (Schedulable.run f wls) sched; + WQ.end_pledge sched.work_queue; + work wls sched end let spawn_worker sched wls_init = - WQ.make_pledge sched.res_writer; - Domain.spawn (fun () -> - let wls = wls_init () in - try + WQ.make_pledge sched.res_writer; + Domain.spawn (fun () -> + let wls = wls_init () in + try work wls sched; - WQ.end_pledge sched.res_writer + WQ.end_pledge sched.res_writer with e -> let bt = Printexc.get_raw_backtrace () in WQ.fail sched.work_queue; @@ -1545,37 +1545,37 @@

82.19%

type 'a t = St of (Thread.t -> ('a * Thread.t, solver) M.t) [@@unboxed] - let run (St mxf) st = mxf st + let run (St mxf) st = mxf st - let return x = St (fun st -> M.return (x, st)) + let return x = St (fun st -> M.return (x, st)) let lift x = - let ( let+ ) = M.( let+ ) in + let ( let+ ) = M.( let+ ) in St (fun st -> - let+ x in - (x, st) ) + let+ x in + (x, st) ) let bind mx f = - St + St (fun st -> - let ( let* ) = M.( let* ) in - let* x, new_st = run mx st in - run (f x) new_st ) + let ( let* ) = M.( let* ) in + let* x, new_st = run mx st in + run (f x) new_st ) let ( let* ) = bind let map x f = - let* x in - return (f x) + let* x in + return (f x) - let liftF2 f x y = St (fun st -> f (run x st) (run y st)) + let liftF2 f x y = St (fun st -> f (run x st) (run y st)) let ( let+ ) = map - let with_state f = St (fun st -> M.return (f st)) + let with_state f = St (fun st -> M.return (f st)) - let modify_state f = St (fun st -> M.return ((), f st)) + let modify_state f = St (fun st -> M.return ((), f st)) end module Eval = struct @@ -1592,30 +1592,30 @@

82.19%

type 'a t = 'a eval M.t - let return x : _ t = M.return (EVal x) + let return x : _ t = M.return (EVal x) let lift x = - let ( let+ ) = M.( let+ ) in + let ( let+ ) = M.( let+ ) in let+ x in - EVal x + EVal x let bind (mx : _ t) f : _ t = - let ( let* ) = M.( let* ) in + let ( let* ) = M.( let* ) in let* mx in - match mx with - | EVal x -> f x - | ETrap _ as mx -> M.return mx - | EAssert _ as mx -> M.return mx + match mx with + | EVal x -> f x + | ETrap _ as mx -> M.return mx + | EAssert _ as mx -> M.return mx let ( let* ) = bind let map mx f = - let ( let+ ) = M.( let+ ) in + let ( let+ ) = M.( let+ ) in let+ mx in - match mx with - | EVal x -> EVal (f x) - | ETrap _ as mx -> mx - | EAssert _ as mx -> mx + match mx with + | EVal x -> EVal (f x) + | ETrap _ as mx -> mx + | EAssert _ as mx -> mx let ( let+ ) = map end @@ -1628,52 +1628,52 @@

82.19%

*) let lift_schedulable (v : ('a, _) Schedulable.t) : 'a t = - lift (State.lift v) + lift (State.lift v) - let with_thread f = lift (State.with_state (fun st -> (f st, st))) + let with_thread f = lift (State.with_state (fun st -> (f st, st))) - let thread = with_thread Fun.id + let thread = with_thread Fun.id - let modify_thread f = lift (State.modify_state f) + let modify_thread f = lift (State.modify_state f) - let set_thread st = modify_thread (Fun.const st) + let set_thread st = modify_thread (Fun.const st) - let clone_thread = modify_thread Thread.clone + let clone_thread = modify_thread Thread.clone - let solver = lift_schedulable Schedulable.worker_local + let solver = lift_schedulable Schedulable.worker_local let choose a b = - let a = + let a = let* () = clone_thread in - a + a in let b = let* () = clone_thread in - b + b in State.liftF2 Schedulable.choose a b - let yield = lift_schedulable @@ Schedulable.yield Prio.default + let yield = lift_schedulable @@ Schedulable.yield Prio.default - let stop = lift_schedulable Schedulable.stop + let stop = lift_schedulable Schedulable.stop type 'a run_result = ('a eval * Thread.t) Seq.t let run ~workers t thread = - let open Scheduler in + let open Scheduler in let sched = init_scheduler () in - add_init_task sched (State.run t thread); - let join_handles = + add_init_task sched (State.run t thread); + let join_handles = Array.map - (fun () -> spawn_worker sched fresh_solver) - (Array.init workers (Fun.const ())) + (fun () -> spawn_worker sched fresh_solver) + (Array.init workers (Fun.const ())) in - WQ.read_as_seq sched.res_writer ~finalizer:(fun () -> + WQ.read_as_seq sched.res_writer ~finalizer:(fun () -> Array.iter Domain.join join_handles ) - let trap t = State.return (ETrap t) + let trap t = State.return (ETrap t) - let assertion_fail c = State.return (EAssert c) + let assertion_fail c = State.return (EAssert c) end (* @@ -1684,17 +1684,17 @@

82.19%

include CoreImpl let add_pc (c : vbool) = - match Expr.view c with + match Expr.view c with | Val True -> return () | Val False -> stop - | _ -> + | _ -> let* thread in - let new_thread = { thread with pc = c :: thread.pc } in + let new_thread = { thread with pc = c :: thread.pc } in set_thread new_thread [@@inline] let add_breadcrumb crumb = - modify_thread (fun t -> { t with breadcrumbs = crumb :: t.breadcrumbs }) + modify_thread (fun t -> { t with breadcrumbs = crumb :: t.breadcrumbs }) (* Yielding is currently done each time the solver is about to be called, @@ -1702,56 +1702,56 @@

82.19%

*) let check_reachability = let* () = yield in - let* (S (solver_module, s)) = solver in - let module Solver = (val solver_module) in + let* (S (solver_module, s)) = solver in + let module Solver = (val solver_module) in let* thread in - match Solver.check s thread.pc with - | `Sat -> return () - | `Unsat | `Unknown -> stop + match Solver.check s thread.pc with + | `Sat -> return () + | `Unsat | `Unknown -> stop let get_model symbol = - let* () = yield in - let* (S (solver_module, s)) = solver in - let module Solver = (val solver_module) in + let* () = yield in + let* (S (solver_module, s)) = solver in + let module Solver = (val solver_module) in let+ thread in - match Solver.check s thread.pc with - | `Unsat | `Unknown -> None - | `Sat -> begin + match Solver.check s thread.pc with + | `Unsat | `Unknown -> None + | `Sat -> begin let model = Solver.model ~symbols:[ symbol ] s in - match model with + match model with | None -> failwith "Unreachable: The problem is sat so a model should exist" - | Some model -> begin + | Some model -> begin match Model.evaluate model symbol with | None -> failwith "Unreachable: The model exists so this symbol should evaluate" - | Some _ as v -> v + | Some _ as v -> v end end let get_model_or_stop symbol = - let* model = get_model symbol in - match model with Some v -> return v | None -> stop + let* model = get_model symbol in + match model with Some v -> return v | None -> stop let select (cond : Symbolic_value.vbool) = - let v = Expr.simplify cond in - match Expr.view v with - | Val True -> return true - | Val False -> return false + let v = Expr.simplify cond in + match Expr.view v with + | Val True -> return true + | Val False -> return false | Val (Num (I32 _)) -> failwith "unreachable (type error)" - | _ -> + | _ -> let true_branch = - let* () = add_pc v in - let* () = add_breadcrumb 1l in - let+ () = check_reachability in - true + let* () = add_pc v in + let* () = add_breadcrumb 1l in + let+ () = check_reachability in + true in let false_branch = - let* () = add_pc (Symbolic_value.Bool.not v) in - let* () = add_breadcrumb 0l in - let+ () = check_reachability in - false + let* () = add_pc (Symbolic_value.Bool.not v) in + let* () = add_breadcrumb 0l in + let+ () = check_reachability in + false in choose true_branch false_branch [@@inline] @@ -1769,42 +1769,42 @@

82.19%

(Some assign, sym) let select_i32 (i : Symbolic_value.int32) = - let sym_int = Expr.simplify i in - match Expr.view sym_int with - | Val (Num (I32 i)) -> return i + let sym_int = Expr.simplify i in + match Expr.view sym_int with + | Val (Num (I32 i)) -> return i | _ -> let* assign, symbol = summary_symbol sym_int in let* () = match assign with Some assign -> add_pc assign | None -> return () in let rec generator () = - let* possible_value = get_model_or_stop symbol in - let i = + let* possible_value = get_model_or_stop symbol in + let i = match possible_value with - | Num (I32 i) -> i + | Num (I32 i) -> i | _ -> failwith "Unreachable: found symbol must be a value" in - let this_value_cond = Expr.Bitv.I32.(Expr.mk_symbol symbol = v i) in + let this_value_cond = Expr.Bitv.I32.(Expr.mk_symbol symbol = v i) in let not_this_value_cond = (* != is **not** the physical equality here *) - Expr.Bitv.I32.(Expr.mk_symbol symbol != v i) + Expr.Bitv.I32.(Expr.mk_symbol symbol != v i) in let this_val_branch = - let* () = add_breadcrumb i in - let+ () = add_pc this_value_cond in - i + let* () = add_breadcrumb i in + let+ () = add_pc this_value_cond in + i in let not_this_val_branch = - let* () = add_pc not_this_value_cond in - generator () + let* () = add_pc not_this_value_cond in + generator () in choose this_val_branch not_this_val_branch in generator () let assertion c = - let* assertion_true = select c in - if assertion_true then return () else assertion_fail c + let* assertion_true = select c in + if assertion_true then return () else assertion_fail c end diff --git a/coverage/src/symbolic/symbolic_global.ml.html b/coverage/src/symbolic/symbolic_global.ml.html index d4f1ce640..12612e450 100644 --- a/coverage/src/symbolic/symbolic_global.ml.html +++ b/coverage/src/symbolic/symbolic_global.ml.html @@ -171,7 +171,7 @@

97.44%

module ITbl = Hashtbl.Make (struct include Int - let hash x = x + let hash x = x end) type t = @@ -181,24 +181,24 @@

97.44%

type collection = t ITbl.t Env_id.Tbl.t -let init () = Env_id.Tbl.create 0 +let init () = Env_id.Tbl.create 0 -let global_copy r = { r with value = r.value } +let global_copy r = { r with value = r.value } let clone collection = (* TODO: this is ugly and should be rewritten... *) - let s = Env_id.Tbl.to_seq collection in - Env_id.Tbl.of_seq - @@ Seq.map + let s = Env_id.Tbl.to_seq collection in + Env_id.Tbl.of_seq + @@ Seq.map (fun (i, t) -> - let s = ITbl.to_seq t in - (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, global_copy a)) s) ) + let s = ITbl.to_seq t in + (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, global_copy a)) s) ) s let convert_values (v : Concrete_value.t) : Symbolic_value.t = (* TODO share various versions *) - match v with - | I32 v -> I32 (Symbolic_value.const_i32 v) + match v with + | I32 v -> I32 (Symbolic_value.const_i32 v) | I64 v -> I64 (Symbolic_value.const_i64 v) | F32 v -> F32 (Symbolic_value.const_f32 v) | F64 v -> F64 (Symbolic_value.const_f64 v) @@ -206,32 +206,32 @@

97.44%

| Ref _ -> assert false let convert (orig_global : Concrete_global.t) : t = - { value = convert_values orig_global.value; orig = orig_global } + { value = convert_values orig_global.value; orig = orig_global } let get_env env_id tables = - match Env_id.Tbl.find_opt tables env_id with - | Some env -> env - | None -> + match Env_id.Tbl.find_opt tables env_id with + | Some env -> env + | None -> let t = ITbl.create 0 in - Env_id.Tbl.add tables env_id t; - t + Env_id.Tbl.add tables env_id t; + t let get_global env_id (orig_global : Concrete_global.t) collection g_id = - let env = get_env env_id collection in - match ITbl.find_opt env g_id with - | Some t -> t - | None -> + let env = get_env env_id collection in + match ITbl.find_opt env g_id with + | Some t -> t + | None -> let t = convert orig_global in - ITbl.add env g_id t; - t + ITbl.add env g_id t; + t -let value v = v.value +let value v = v.value -let set_value v x = v.value <- x +let set_value v x = v.value <- x -let mut v = v.orig.mut +let mut v = v.orig.mut -let typ v = v.orig.typ +let typ v = v.orig.typ diff --git a/coverage/src/symbolic/symbolic_memory.ml.html b/coverage/src/symbolic/symbolic_memory.ml.html index 9c068ef53..50ed6b8e3 100644 --- a/coverage/src/symbolic/symbolic_memory.ml.html +++ b/coverage/src/symbolic/symbolic_memory.ml.html @@ -3,7 +3,7 @@ symbolic_memory.ml — Coverage report - + @@ -15,7 +15,7 @@

src/symbolic/symbolic_memory.ml

-

84.88%

+

83.90%

diff --git a/coverage/src/symbolic/symbolic_table.ml.html b/coverage/src/symbolic/symbolic_table.ml.html index 1e31bd77f..19bdf0bcb 100644 --- a/coverage/src/symbolic/symbolic_table.ml.html +++ b/coverage/src/symbolic/symbolic_table.ml.html @@ -224,7 +224,7 @@

71.11%

module ITbl = Hashtbl.Make (struct include Int - let hash x = x + let hash x = x end) type t = @@ -233,20 +233,20 @@

71.11%

; typ : binary ref_type } -let clone_t { limits; data; typ } = { typ; limits; data = Array.copy data } +let clone_t { limits; data; typ } = { typ; limits; data = Array.copy data } type collection = t ITbl.t Env_id.Tbl.t -let init () = Env_id.Tbl.create 0 +let init () = Env_id.Tbl.create 0 let clone (collection : collection) = (* TODO: this is ugly and should be rewritten *) - let s = Env_id.Tbl.to_seq collection in - Env_id.Tbl.of_seq - @@ Seq.map + let s = Env_id.Tbl.to_seq collection in + Env_id.Tbl.of_seq + @@ Seq.map (fun (i, t) -> let s = ITbl.to_seq t in - (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, clone_t a)) s) ) + (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, clone_t a)) s) ) s let convert_ref_values (v : Concrete_value.ref_value) : Symbolic_value.ref_value @@ -260,8 +260,8 @@

71.11%

} let get_env env_id tables = - match Env_id.Tbl.find_opt tables env_id with - | Some env -> env + match Env_id.Tbl.find_opt tables env_id with + | Some env -> env | None -> let t = ITbl.create 0 in Env_id.Tbl.add tables env_id t; @@ -269,21 +269,21 @@

71.11%

let get_table env_id (orig_table : Concrete_table.t) (collection : collection) t_id = - let env = get_env env_id collection in - match ITbl.find_opt env t_id with - | Some t -> t + let env = get_env env_id collection in + match ITbl.find_opt env t_id with + | Some t -> t | None -> let t = convert orig_table in ITbl.add env t_id t; t -let get t i = t.data.(i) +let get t i = t.data.(i) let set t i v = t.data.(i) <- v -let size t = Array.length t.data +let size t = Array.length t.data -let typ t = t.typ +let typ t = t.typ let max_size t = t.limits.max diff --git a/coverage/src/symbolic/symbolic_value.ml.html b/coverage/src/symbolic/symbolic_value.ml.html index 044cf86fe..38a327e2c 100644 --- a/coverage/src/symbolic/symbolic_value.ml.html +++ b/coverage/src/symbolic/symbolic_value.ml.html @@ -965,13 +965,13 @@

85.12%

| F64 of float64 | Ref of ref_value -let const_i32 (i : Int32.t) : int32 = value (Num (I32 i)) +let const_i32 (i : Int32.t) : int32 = value (Num (I32 i)) -let const_i64 (i : Int64.t) : int64 = value (Num (I64 i)) +let const_i64 (i : Int64.t) : int64 = value (Num (I64 i)) -let const_f32 (f : Float32.t) : float32 = value (Num (F32 (Float32.to_bits f))) +let const_f32 (f : Float32.t) : float32 = value (Num (F32 (Float32.to_bits f))) -let const_f64 (f : Float64.t) : float64 = value (Num (F64 (Float64.to_bits f))) +let const_f64 (f : Float64.t) : float64 = value (Num (F64 (Float64.to_bits f))) let ref_null _ty = Ref (Funcref None) @@ -996,8 +996,8 @@

85.12%

module Ref = struct let get_func (r : ref_value) : Func_intf.t Value_intf.get_ref = - match r with - | Funcref (Some f) -> Ref_value f + match r with + | Funcref (Some f) -> Ref_value f | Funcref None -> Null | Externref _ -> Type_mismatch @@ -1012,22 +1012,22 @@

85.12%

end module Bool = struct - let const b = Bool.v b + let const b = Bool.v b - let not e = Bool.not e + let not e = Bool.not e - let or_ e1 e2 = Bool.or_ e1 e2 + let or_ e1 e2 = Bool.or_ e1 e2 - let and_ e1 e2 = Bool.and_ e1 e2 + let and_ e1 e2 = Bool.and_ e1 e2 let int32 e = - match view e with - | Val True -> const_i32 1l - | Val False -> const_i32 0l + match view e with + | Val True -> const_i32 1l + | Val False -> const_i32 0l | Cvtop (Ty_bitv 32, ToBool, e') -> e' - | _ -> make (Cvtop (Ty_bitv 32, OfBool, e)) + | _ -> make (Cvtop (Ty_bitv 32, OfBool, e)) - let select_expr c ~if_true ~if_false = Bool.ite c if_true if_false + let select_expr c ~if_true ~if_false = Bool.ite c if_true if_false let pp ppf (e : vbool) = Expr.pp ppf e end @@ -1035,9 +1035,9 @@

85.12%

module I32 = struct let ty = Ty_bitv 32 - let zero = const_i32 0l + let zero = const_i32 0l - let clz e = unop ty Clz e + let clz e = unop ty Clz e let ctz e = unop ty Ctz e @@ -1045,81 +1045,81 @@

85.12%

(* TODO *) assert false - let add e1 e2 = binop ty Add e1 e2 + let add e1 e2 = binop ty Add e1 e2 - let sub e1 e2 = binop ty Sub e1 e2 + let sub e1 e2 = binop ty Sub e1 e2 - let mul e1 e2 = binop ty Mul e1 e2 + let mul e1 e2 = binop ty Mul e1 e2 let div e1 e2 = binop ty Div e1 e2 let unsigned_div e1 e2 = binop ty DivU e1 e2 - let rem e1 e2 = binop ty Rem e1 e2 + let rem e1 e2 = binop ty Rem e1 e2 let unsigned_rem e1 e2 = binop ty RemU e1 e2 let boolify e = - match view e with - | Val (Num (I32 0l)) -> Some (Bool.const false) - | Val (Num (I32 1l)) -> Some (Bool.const true) - | Cvtop (_, OfBool, cond) -> Some cond - | _ -> None + match view e with + | Val (Num (I32 0l)) -> Some (Bool.const false) + | Val (Num (I32 1l)) -> Some (Bool.const true) + | Cvtop (_, OfBool, cond) -> Some cond + | _ -> None let logand e1 e2 = - match (boolify e1, boolify e2) with - | Some b1, Some b2 -> Bool.int32 (Bool.and_ b1 b2) - | _ -> binop ty And e1 e2 + match (boolify e1, boolify e2) with + | Some b1, Some b2 -> Bool.int32 (Bool.and_ b1 b2) + | _ -> binop ty And e1 e2 let logor e1 e2 = match (boolify e1, boolify e2) with | Some b1, Some b2 -> Bool.int32 (Bool.or_ b1 b2) | _ -> binop ty Or e1 e2 - let logxor e1 e2 = binop ty Xor e1 e2 + let logxor e1 e2 = binop ty Xor e1 e2 - let shl e1 e2 = binop ty Shl e1 e2 + let shl e1 e2 = binop ty Shl e1 e2 - let shr_s e1 e2 = binop ty ShrA e1 e2 + let shr_s e1 e2 = binop ty ShrA e1 e2 - let shr_u e1 e2 = binop ty ShrL e1 e2 + let shr_u e1 e2 = binop ty ShrL e1 e2 let rotl e1 e2 = binop ty Rotl e1 e2 let rotr e1 e2 = binop ty Rotr e1 e2 let eq_const e c = - match view e with - | Cvtop (_, OfBool, cond) -> begin - match c with 0l -> Bool.not cond | 1l -> cond | _ -> Bool.const false + match view e with + | Cvtop (_, OfBool, cond) -> begin + match c with 0l -> Bool.not cond | 1l -> cond | _ -> Bool.const false end - | _ -> relop Ty_bool Eq e (const_i32 c) + | _ -> relop Ty_bool Eq e (const_i32 c) - let eq e1 e2 = if e1 == e2 then Bool.const true else relop Ty_bool Eq e1 e2 + let eq e1 e2 = if e1 == e2 then Bool.const true else relop Ty_bool Eq e1 e2 - let ne e1 e2 = if e1 == e2 then Bool.const false else relop Ty_bool Ne e1 e2 + let ne e1 e2 = if e1 == e2 then Bool.const false else relop Ty_bool Ne e1 e2 - let lt e1 e2 = if e1 == e2 then Bool.const false else relop ty Lt e1 e2 + let lt e1 e2 = if e1 == e2 then Bool.const false else relop ty Lt e1 e2 - let gt e1 e2 = if e1 == e2 then Bool.const false else relop ty Gt e1 e2 + let gt e1 e2 = if e1 == e2 then Bool.const false else relop ty Gt e1 e2 - let lt_u e1 e2 = if e1 == e2 then Bool.const false else relop ty LtU e1 e2 + let lt_u e1 e2 = if e1 == e2 then Bool.const false else relop ty LtU e1 e2 let gt_u e1 e2 = if e1 == e2 then Bool.const false else relop ty GtU e1 e2 - let le e1 e2 = if e1 == e2 then Bool.const true else relop ty Le e1 e2 + let le e1 e2 = if e1 == e2 then Bool.const true else relop ty Le e1 e2 - let ge e1 e2 = if e1 == e2 then Bool.const true else relop ty Ge e1 e2 + let ge e1 e2 = if e1 == e2 then Bool.const true else relop ty Ge e1 e2 let le_u e1 e2 = if e1 == e2 then Bool.const true else relop ty LeU e1 e2 - let ge_u e1 e2 = if e1 == e2 then Bool.const true else relop ty GeU e1 e2 + let ge_u e1 e2 = if e1 == e2 then Bool.const true else relop ty GeU e1 e2 let to_bool (e : vbool) = - match view e with - | Val (Num (I32 i)) -> Bool.const @@ Int32.ne i 0l - | Cvtop (_, OfBool, cond) -> cond - | _ -> make (Cvtop (ty, ToBool, e)) + match view e with + | Val (Num (I32 i)) -> Bool.const @@ Int32.ne i 0l + | Cvtop (_, OfBool, cond) -> cond + | _ -> make (Cvtop (ty, ToBool, e)) let trunc_f32_s x = cvtop ty TruncSF32 x @@ -1149,7 +1149,7 @@

85.12%

module I64 = struct let ty = Ty_bitv 64 - let zero = const_i64 0L + let zero = const_i64 0L let clz e = unop ty Clz e @@ -1245,7 +1245,7 @@

85.12%

module F32 = struct let ty = Ty_fp 32 - let zero = const_f32 Float32.zero + let zero = const_f32 Float32.zero let abs x = unop ty Abs x @@ -1310,7 +1310,7 @@

85.12%

module F64 = struct let ty = Ty_fp 64 - let zero = const_f64 Float64.zero + let zero = const_f64 Float64.zero let abs x = unop ty Abs x diff --git a/coverage/src/tracing.ml.html b/coverage/src/tracing.ml.html index 14a68bc74..0ec592805 100644 --- a/coverage/src/tracing.ml.html +++ b/coverage/src/tracing.ml.html @@ -107,19 +107,19 @@

57.14%

type Runtime_events.User.tag += Solver_model let check = - Runtime_events.User.register "solver_check" Solver_check + Runtime_events.User.register "solver_check" Solver_check Runtime_events.Type.span let check_true = - Runtime_events.User.register "solver_check_true" Solver_check_true + Runtime_events.User.register "solver_check_true" Solver_check_true Runtime_events.Type.span let check_false = - Runtime_events.User.register "solver_check_false" Solver_check_false + Runtime_events.User.register "solver_check_false" Solver_check_false Runtime_events.Type.span let model = - Runtime_events.User.register "solver_model" Solver_model + Runtime_events.User.register "solver_model" Solver_model Runtime_events.Type.span let with_ev ev f = diff --git a/coverage/src/typecheck/typecheck.ml.html b/coverage/src/typecheck/typecheck.ml.html index 538e6e524..18188fb29 100644 --- a/coverage/src/typecheck/typecheck.ml.html +++ b/coverage/src/typecheck/typecheck.ml.html @@ -1342,9 +1342,9 @@

86.18%

let typ_of_val_type = function | Types.Ref_type (_null, t) -> Ref_type t - | Num_type t -> Num_type t + | Num_type t -> Num_type t -let typ_of_pt pt = typ_of_val_type @@ snd pt +let typ_of_pt pt = typ_of_val_type @@ snd pt module Index = struct module M = Int @@ -1364,7 +1364,7 @@

86.18%

; refs : (int, unit) Hashtbl.t } - let local_get i env = match Index.Map.find i env.locals with v -> v + let local_get i env = match Index.Map.find i env.locals with v -> v let global_get i env = let value = Indexed.get_at_exn i env.globals.values in @@ -1374,19 +1374,19 @@

86.18%

typ let func_get i env = - let value = Indexed.get_at_exn i env.funcs.values in - match value with - | Local { type_f; _ } -> + let value = Indexed.get_at_exn i env.funcs.values in + match value with + | Local { type_f; _ } -> let (Bt_raw ((None | Some _), t)) = type_f in t - | Runtime.Imported t -> + | Runtime.Imported t -> let (Bt_raw ((None | Some _), t)) = t.desc in t let block_type_get i env = - match List.nth_opt env.blocks i with + match List.nth_opt env.blocks i with | None -> Error `Unknown_label - | Some bt -> Ok bt + | Some bt -> Ok bt let table_type_get_from_module i (modul : Binary.modul) = let value = Indexed.get_at_exn i modul.table.values in @@ -1405,15 +1405,15 @@

86.18%

value.typ let make ~params ~locals ~globals ~funcs ~result_type ~tables ~elems ~refs = - let l = List.mapi (fun i v -> (i, v)) (params @ locals) in - let locals = + let l = List.mapi (fun i v -> (i, v)) (params @ locals) in + let locals = List.fold_left (fun locals (i, (_, typ)) -> - let typ = typ_of_val_type typ in - Index.Map.add i typ locals ) + let typ = typ_of_val_type typ in + Index.Map.add i typ locals ) Index.Map.empty l in - { locals; globals; result_type; funcs; tables; elems; blocks = []; refs } + { locals; globals; result_type; funcs; tables; elems; blocks = []; refs } end type env = Env.t @@ -1432,7 +1432,7 @@

86.18%

let any = Any -let itype = function S32 -> i32 | S64 -> i64 +let itype = function S32 -> i32 | S64 -> i64 let ftype = function S32 -> f32 | S64 -> f64 @@ -1466,9 +1466,9 @@

86.18%

let pp fmt (s : stack) = pp fmt "[%a]" pp_typ_list s let match_num_type (required : num_type) (got : num_type) = - match (required, got) with - | I32, I32 -> true - | I64, I64 -> true + match (required, got) with + | I32, I32 -> true + | I64, I64 -> true | F32, F32 -> true | F64, F64 -> true | _, _ -> false @@ -1490,36 +1490,36 @@

86.18%

false let match_types required got = - match (required, got) with + match (required, got) with | Something, _ | _, Something -> true | Any, _ | _, Any -> true - | Num_type required, Num_type got -> match_num_type required got + | Num_type required, Num_type got -> match_num_type required got | Ref_type required, Ref_type got -> match_ref_type required got | Num_type _, Ref_type _ | Ref_type _, Num_type _ -> false let rec equal s s' = - match (s, s') with - | [], s | s, [] -> List.for_all (( = ) Any) s + match (s, s') with + | [], s | s, [] -> List.for_all (( = ) Any) s | Any :: tl, Any :: tl' -> equal tl s' || equal s tl' | Any :: tl, hd :: tl' | hd :: tl', Any :: tl -> equal tl (hd :: tl') || equal (Any :: tl) tl' - | hd :: tl, hd' :: tl' -> match_types hd hd' && equal tl tl' + | hd :: tl, hd' :: tl' -> match_types hd hd' && equal tl tl' let ( ||| ) l r = match (l, r) with None, v | v, None -> v | _l, r -> r let rec match_prefix ~prefix ~stack = - match (prefix, stack) with - | [], stack -> Some stack + match (prefix, stack) with + | [], stack -> Some stack | _hd :: _tl, [] -> None | _hd :: tl, Any :: tl' -> match_prefix ~prefix ~stack:tl' ||| match_prefix ~prefix:tl ~stack - | hd :: tl, hd' :: tl' -> - if match_types hd hd' then match_prefix ~prefix:tl ~stack:tl' else None + | hd :: tl, hd' :: tl' -> + if match_types hd hd' then match_prefix ~prefix:tl ~stack:tl' else None let pop required stack = - match match_prefix ~prefix:required ~stack with + match match_prefix ~prefix:required ~stack with | None -> Error (`Type_mismatch "pop") - | Some stack -> Ok stack + | Some stack -> Ok stack let pop_ref = function | (Something | Ref_type _) :: tl -> Ok tl @@ -1527,12 +1527,12 @@

86.18%

| _ -> Error (`Type_mismatch "pop_ref") let drop stack = - match stack with + match stack with | [] -> Error (`Type_mismatch "drop") | Any :: _ -> Ok [ Any ] - | _ :: tl -> Ok tl + | _ :: tl -> Ok tl - let push t stack = ok @@ t @ stack + let push t stack = ok @@ t @ stack let pop_push (Bt_raw ((None | Some _), (pt, rt))) stack = let pt, rt = (List.rev_map typ_of_pt pt, List.rev_map typ_of_val_type rt) in @@ -1542,27 +1542,27 @@

86.18%

let rec typecheck_instr (env : env) (stack : stack) (instr : binary instr) : stack Result.t = - match instr with + match instr with | Nop -> Ok stack - | Drop -> Stack.drop stack + | Drop -> Stack.drop stack | Return -> let+ _stack = Stack.pop (List.rev_map typ_of_val_type env.result_type) stack in [ any ] - | Unreachable -> Ok [ any ] - | I32_const _ -> Stack.push [ i32 ] stack - | I64_const _ -> Stack.push [ i64 ] stack + | Unreachable -> Ok [ any ] + | I32_const _ -> Stack.push [ i32 ] stack + | I64_const _ -> Stack.push [ i64 ] stack | F32_const _ -> Stack.push [ f32 ] stack | F64_const _ -> Stack.push [ f64 ] stack | I_unop (s, _op) -> let t = itype s in let* stack = Stack.pop [ t ] stack in Stack.push [ t ] stack - | I_binop (s, _op) -> + | I_binop (s, _op) -> let t = itype s in - let* stack = Stack.pop [ t; t ] stack in - Stack.push [ t ] stack + let* stack = Stack.pop [ t; t ] stack in + Stack.push [ t ] stack | F_unop (s, _op) -> let t = ftype s in let* stack = Stack.pop [ t ] stack in @@ -1571,25 +1571,25 @@

86.18%

let t = ftype s in let* stack = Stack.pop [ t; t ] stack in Stack.push [ t ] stack - | I_testop (nn, _) -> - let* stack = Stack.pop [ itype nn ] stack in - Stack.push [ i32 ] stack - | I_relop (nn, _) -> + | I_testop (nn, _) -> + let* stack = Stack.pop [ itype nn ] stack in + Stack.push [ i32 ] stack + | I_relop (nn, _) -> let t = itype nn in - let* stack = Stack.pop [ t; t ] stack in - Stack.push [ i32 ] stack + let* stack = Stack.pop [ t; t ] stack in + Stack.push [ i32 ] stack | F_relop (nn, _) -> let t = ftype nn in let* stack = Stack.pop [ t; t ] stack in Stack.push [ i32 ] stack - | Local_get (Raw i) -> Stack.push [ Env.local_get i env ] stack - | Local_set (Raw i) -> + | Local_get (Raw i) -> Stack.push [ Env.local_get i env ] stack + | Local_set (Raw i) -> let t = Env.local_get i env in - Stack.pop [ t ] stack - | Local_tee (Raw i) -> + Stack.pop [ t ] stack + | Local_tee (Raw i) -> let t = Env.local_get i env in - let* stack = Stack.pop [ t ] stack in - Stack.push [ t ] stack + let* stack = Stack.pop [ t ] stack in + Stack.push [ t ] stack | Global_get (Raw i) -> Stack.push [ typ_of_val_type @@ Env.global_get i env ] stack | Global_set (Raw i) -> @@ -1600,14 +1600,14 @@

86.18%

let* stack_e1 = typecheck_expr env e1 ~is_loop:false block_type ~stack in let+ _stack_e2 = typecheck_expr env e2 ~is_loop:false block_type ~stack in stack_e1 - | I_load (nn, _) | I_load16 (nn, _, _) | I_load8 (nn, _, _) -> - let* stack = Stack.pop [ i32 ] stack in - Stack.push [ itype nn ] stack + | I_load (nn, _) | I_load16 (nn, _, _) | I_load8 (nn, _, _) -> + let* stack = Stack.pop [ i32 ] stack in + Stack.push [ itype nn ] stack | I64_load32 _ -> let* stack = Stack.pop [ i32 ] stack in Stack.push [ i64 ] stack - | I_store8 (nn, _) | I_store16 (nn, _) | I_store (nn, _) -> - Stack.pop [ itype nn; i32 ] stack + | I_store8 (nn, _) | I_store16 (nn, _) | I_store (nn, _) -> + Stack.pop [ itype nn; i32 ] stack | I64_store32 _ -> Stack.pop [ i64; i32 ] stack | F_load (nn, _) -> let* stack = Stack.pop [ i32 ] stack in @@ -1650,15 +1650,15 @@

86.18%

| Memory_size -> Stack.push [ i32 ] stack | Memory_copy | Memory_init _ | Memory_fill -> Stack.pop [ i32; i32; i32 ] stack - | Block (_, bt, expr) -> typecheck_expr env expr ~is_loop:false bt ~stack - | Loop (_, bt, expr) -> typecheck_expr env expr ~is_loop:true bt ~stack + | Block (_, bt, expr) -> typecheck_expr env expr ~is_loop:false bt ~stack + | Loop (_, bt, expr) -> typecheck_expr env expr ~is_loop:true bt ~stack | Call_indirect (_, bt) -> let* stack = Stack.pop [ i32 ] stack in Stack.pop_push bt stack - | Call (Raw i) -> + | Call (Raw i) -> let pt, rt = Env.func_get i env in - let* stack = Stack.pop (List.rev_map typ_of_pt pt) stack in - Stack.push (List.rev_map typ_of_val_type rt) stack + let* stack = Stack.pop (List.rev_map typ_of_pt pt) stack in + Stack.push (List.rev_map typ_of_val_type rt) stack | Call_ref _t -> let+ stack = Stack.pop_ref stack in (* TODO: @@ -1745,15 +1745,15 @@

86.18%

| Ref_func (Raw i) -> if not @@ Hashtbl.mem env.refs i then Error `Undeclared_function_reference else Stack.push [ Ref_type Func_ht ] stack - | Br (Raw i) -> - let* jt = Env.block_type_get i env in - let* _stack = Stack.pop jt stack in - Ok [ any ] - | Br_if (Raw i) -> - let* stack = Stack.pop [ i32 ] stack in - let* jt = Env.block_type_get i env in - let* stack = Stack.pop jt stack in - Stack.push jt stack + | Br (Raw i) -> + let* jt = Env.block_type_get i env in + let* _stack = Stack.pop jt stack in + Ok [ any ] + | Br_if (Raw i) -> + let* stack = Stack.pop [ i32 ] stack in + let* jt = Env.block_type_get i env in + let* stack = Stack.pop jt stack in + Stack.push jt stack | Br_table (branches, Raw i) -> let* stack = Stack.pop [ i32 ] stack in let* default_jt = Env.block_type_get i env in @@ -1798,29 +1798,29 @@

86.18%

and typecheck_expr env expr ~is_loop (block_type : binary block_type option) ~stack:previous_stack : stack Result.t = - let pt, rt = + let pt, rt = Option.fold ~none:([], []) ~some:(fun (Bt_raw ((None | Some _), (pt, rt)) : binary block_type) -> - (List.rev_map typ_of_pt pt, List.rev_map typ_of_val_type rt) ) + (List.rev_map typ_of_pt pt, List.rev_map typ_of_val_type rt) ) block_type in - let jump_type = if is_loop then pt else rt in + let jump_type = if is_loop then pt else rt in let env = { env with blocks = jump_type :: env.blocks } in - let* stack = list_fold_left (typecheck_instr env) pt expr in - if not (Stack.equal rt stack) then Error (`Type_mismatch "typecheck_expr 1") + let* stack = list_fold_left (typecheck_instr env) pt expr in + if not (Stack.equal rt stack) then Error (`Type_mismatch "typecheck_expr 1") else - match Stack.match_prefix ~prefix:pt ~stack:previous_stack with + match Stack.match_prefix ~prefix:pt ~stack:previous_stack with | None -> Error (`Type_mismatch (Format.asprintf "expected a prefix of %a but stack has type %a" Stack.pp pt Stack.pp previous_stack ) ) - | Some stack_to_push -> Stack.push rt stack_to_push + | Some stack_to_push -> Stack.push rt stack_to_push let typecheck_function (modul : modul) func refs = - match func with - | Runtime.Imported _ -> Ok () - | Local func -> + match func with + | Runtime.Imported _ -> Ok () + | Local func -> let (Bt_raw ((None | Some _), (params, result))) = func.type_f in let env = Env.make ~params ~funcs:modul.func ~locals:func.locals @@ -1828,17 +1828,17 @@

86.18%

~elems:modul.elem ~refs in let* stack = - typecheck_expr env func.body ~is_loop:false + typecheck_expr env func.body ~is_loop:false (Some (Bt_raw (None, ([], result)))) ~stack:[] in - let required = List.rev_map typ_of_val_type result in - if not @@ Stack.equal required stack then + let required = List.rev_map typ_of_val_type result in + if not @@ Stack.equal required stack then Error (`Type_mismatch "typecheck_function") - else Ok () + else Ok () let typecheck_const_instr (modul : modul) refs stack = function - | I32_const _ -> Stack.push [ i32 ] stack + | I32_const _ -> Stack.push [ i32 ] stack | I64_const _ -> Stack.push [ i64 ] stack | F32_const _ -> Stack.push [ f32 ] stack | F64_const _ -> Stack.push [ f64 ] stack @@ -1869,19 +1869,19 @@

86.18%

| _ -> assert false let typecheck_const_expr (modul : modul) refs = - list_fold_left (typecheck_const_instr modul refs) [] + list_fold_left (typecheck_const_instr modul refs) [] let typecheck_global (modul : modul) refs (global : (global, binary global_type) Runtime.t Indexed.t) = - match Indexed.get global with + match Indexed.get global with | Imported _ -> Ok () - | Local { typ; init; _ } -> ( - let* real_type = typecheck_const_expr modul refs init in - match real_type with - | [ real_type ] -> - let expected = typ_of_val_type @@ snd typ in - if expected <> real_type then Error (`Type_mismatch "typecheck global 1") - else Ok () + | Local { typ; init; _ } -> ( + let* real_type = typecheck_const_expr modul refs init in + match real_type with + | [ real_type ] -> + let expected = typ_of_val_type @@ snd typ in + if expected <> real_type then Error (`Type_mismatch "typecheck global 1") + else Ok () | _whatever -> Error (`Type_mismatch "typecheck_global 2") ) let typecheck_elem modul refs (elem : elem Indexed.t) = @@ -1925,18 +1925,18 @@

86.18%

| _whatever -> Error (`Type_mismatch "typecheck_data") ) let modul (modul : modul) = - Log.debug0 "typechecking ...@\n"; - let refs = Hashtbl.create 512 in - let* () = list_iter (typecheck_global modul refs) modul.global.values in - let* () = list_iter (typecheck_elem modul refs) modul.elem.values in - let* () = list_iter (typecheck_data modul refs) modul.data.values in - List.iter - (fun (export : export) -> Hashtbl.add refs export.id ()) + Log.debug0 "typechecking ...@\n"; + let refs = Hashtbl.create 512 in + let* () = list_iter (typecheck_global modul refs) modul.global.values in + let* () = list_iter (typecheck_elem modul refs) modul.elem.values in + let* () = list_iter (typecheck_data modul refs) modul.data.values in + List.iter + (fun (export : export) -> Hashtbl.add refs export.id ()) modul.exports.func; - Named.fold + Named.fold (fun _index func acc -> - let* () = acc in - typecheck_function modul func refs ) + let* () = acc in + typecheck_function modul func refs ) modul.func (Ok ()) diff --git a/coverage/src/utils/log.ml.html b/coverage/src/utils/log.ml.html index 5d6274955..e2d7081d9 100644 --- a/coverage/src/utils/log.ml.html +++ b/coverage/src/utils/log.ml.html @@ -75,15 +75,15 @@

81.82%

let profiling_on = ref false -let debug0 t : unit = if !debug_on then Format.pp_err t +let debug0 t : unit = if !debug_on then Format.pp_err t -let debug1 t a : unit = if !debug_on then Format.pp_err t a +let debug1 t a : unit = if !debug_on then Format.pp_err t a -let debug2 t a b : unit = if !debug_on then Format.pp_err t a b +let debug2 t a b : unit = if !debug_on then Format.pp_err t a b let debug5 t a b c d e : unit = if !debug_on then Format.pp_err t a b c d e -let profile3 t a b c : unit = if !profiling_on then Format.pp_err t a b c +let profile3 t a b c : unit = if !profiling_on then Format.pp_err t a b c let err f = Format.kasprintf failwith f diff --git a/coverage/src/utils/syntax.ml.html b/coverage/src/utils/syntax.ml.html index a14f7cbf2..cf408e6ac 100644 --- a/coverage/src/utils/syntax.ml.html +++ b/coverage/src/utils/syntax.ml.html @@ -221,49 +221,49 @@

81.63%

open Stdlib.Result -let ( let* ) o f = match o with Ok v -> f v | Error _ as e -> e +let ( let* ) o f = match o with Ok v -> f v | Error _ as e -> e -let ( let+ ) o f = match o with Ok v -> Ok (f v) | Error _ as e -> e +let ( let+ ) o f = match o with Ok v -> Ok (f v) | Error _ as e -> e let error v = Error v let error_s format = Format.kasprintf error format -let ok v = Ok v +let ok v = Ok v let list_iter f l = - let err = ref None in + let err = ref None in try List.iter (fun v -> - match f v with + match f v with | Error _e as e -> err := Some e; raise Exit - | Ok () -> () ) + | Ok () -> () ) l; - Ok () + Ok () with Exit -> Option.get !err let list_map f l = - let err = ref None in + let err = ref None in try - ok - @@ List.map + ok + @@ List.map (fun v -> - match f v with + match f v with | Error _e as e -> err := Some e; raise Exit - | Ok v -> v ) + | Ok v -> v ) l with Exit -> Option.get !err let list_fold_left f acc l = - List.fold_left + List.fold_left (fun acc v -> - let* acc in - f acc v ) + let* acc in + f acc v ) (Ok acc) l let array_iter f a = diff --git a/coverage/src/utils/wutf8.ml.html b/coverage/src/utils/wutf8.ml.html index 238f731ae..af26d34f4 100644 --- a/coverage/src/utils/wutf8.ml.html +++ b/coverage/src/utils/wutf8.ml.html @@ -166,14 +166,14 @@

16.67%

| _ -> raise Utf8 let check_utf8 s = - let open Uutf in + let open Uutf in let decoder = decoder ~encoding:`UTF_8 (`String s) in - let rec loop () = - match decode decoder with + let rec loop () = + match decode decoder with | `Malformed s -> Error (`Malformed_utf8_encoding s) | `Await -> assert false - | `End -> Ok () - | `Uchar _ -> loop () + | `End -> Ok () + | `Uchar _ -> loop () in loop () diff --git a/coverage/src/v.ml.html b/coverage/src/v.ml.html index 2224acb9a..e813d2270 100644 --- a/coverage/src/v.ml.html +++ b/coverage/src/v.ml.html @@ -219,9 +219,9 @@

86.67%

type float64 = Float64.t - let const_i32 x = x + let const_i32 x = x - let const_i64 x = x + let const_i64 x = x let const_f32 x = x