diff --git a/doc/src/hacking/benchmarking.md b/doc/src/hacking/benchmarking.md index 897cac202..0d7e06392 100644 --- a/doc/src/hacking/benchmarking.md +++ b/doc/src/hacking/benchmarking.md @@ -6,10 +6,11 @@ OCAML_LANDMARKS=on dune exec --instrument-with landmarks --profile release -- owi run test/run/binary_loop.wasm ``` -Note: it seems landmarks is not compatible with domains and thus won't work with most sub-commands. +See the discussion in [#871] to understand landmarks limitations in Owi. ## Test-comp See [Symbocalypse]. +[#871]: https://github.com/OCamlPro/owi/pull/871 [Symbocalypse]: https://github.com/OCamlPro/symbocalypse diff --git a/doc/src/manpages/owi-c.md b/doc/src/manpages/owi-c.md index 295cc7fb8..56d4783e5 100644 --- a/doc/src/manpages/owi-c.md +++ b/doc/src/manpages/owi-c.md @@ -68,6 +68,9 @@ OPTIONS --no-value do not display a value for each symbol + --no-worker-isolation + Do not force each worker to run on an isolated physical core. + -o FILE, --output=FILE Output the generated .wasm or .wat to FILE. @@ -88,7 +91,7 @@ OPTIONS skip typechecking pass -w VAL, --workers=VAL (absent=n) - number of workers for symbolic execution. Defaults to the number + Number of workers for symbolic execution. Defaults to the number of physical cores. --with-breadcrumbs diff --git a/doc/src/manpages/owi-cpp.md b/doc/src/manpages/owi-cpp.md index 088aed0fb..34ade695e 100644 --- a/doc/src/manpages/owi-cpp.md +++ b/doc/src/manpages/owi-cpp.md @@ -63,6 +63,9 @@ OPTIONS --no-value do not display a value for each symbol + --no-worker-isolation + Do not force each worker to run on an isolated physical core. + -o FILE, --output=FILE Output the generated .wasm or .wat to FILE. @@ -77,7 +80,7 @@ OPTIONS skip typechecking pass -w VAL, --workers=VAL (absent=n) - number of workers for symbolic execution. Defaults to the number + Number of workers for symbolic execution. Defaults to the number of physical cores. --with-breadcrumbs diff --git a/doc/src/manpages/owi-iso.md b/doc/src/manpages/owi-iso.md index b9d48ac50..8c74fee57 100644 --- a/doc/src/manpages/owi-iso.md +++ b/doc/src/manpages/owi-iso.md @@ -47,6 +47,9 @@ OPTIONS --no-value do not display a value for each symbol + --no-worker-isolation + Do not force each worker to run on an isolated physical core. + -s VALUE, --solver=VALUE (absent=Z3) SMT solver to use. VALUE must be one of the 5 available solvers: Z3, Bitwuzla, Colibri2, cvc5, Alt-Ergo @@ -55,7 +58,7 @@ OPTIONS skip typechecking pass -w VAL, --workers=VAL (absent=n) - number of workers for symbolic execution. Defaults to the number + Number of workers for symbolic execution. Defaults to the number of physical cores. --with-breadcrumbs diff --git a/doc/src/manpages/owi-rust.md b/doc/src/manpages/owi-rust.md index e00017fc2..9c25d3f59 100644 --- a/doc/src/manpages/owi-rust.md +++ b/doc/src/manpages/owi-rust.md @@ -63,6 +63,9 @@ OPTIONS --no-value do not display a value for each symbol + --no-worker-isolation + Do not force each worker to run on an isolated physical core. + -o FILE, --output=FILE Output the generated .wasm or .wat to FILE. @@ -77,7 +80,7 @@ OPTIONS skip typechecking pass -w VAL, --workers=VAL (absent=n) - number of workers for symbolic execution. Defaults to the number + Number of workers for symbolic execution. Defaults to the number of physical cores. --with-breadcrumbs diff --git a/doc/src/manpages/owi-sym.md b/doc/src/manpages/owi-sym.md index d46321e85..8173264af 100644 --- a/doc/src/manpages/owi-sym.md +++ b/doc/src/manpages/owi-sym.md @@ -56,6 +56,9 @@ OPTIONS --no-value do not display a value for each symbol + --no-worker-isolation + Do not force each worker to run on an isolated physical core. + -s VALUE, --solver=VALUE (absent=Z3) SMT solver to use. VALUE must be one of the 5 available solvers: Z3, Bitwuzla, Colibri2, cvc5, Alt-Ergo @@ -64,7 +67,7 @@ OPTIONS skip typechecking pass -w VAL, --workers=VAL (absent=n) - number of workers for symbolic execution. Defaults to the number + Number of workers for symbolic execution. Defaults to the number of physical cores. --with-breadcrumbs diff --git a/doc/src/manpages/owi-zig.md b/doc/src/manpages/owi-zig.md index e011011ca..24832bf9c 100644 --- a/doc/src/manpages/owi-zig.md +++ b/doc/src/manpages/owi-zig.md @@ -60,6 +60,9 @@ OPTIONS --no-value do not display a value for each symbol + --no-worker-isolation + Do not force each worker to run on an isolated physical core. + -o FILE, --output=FILE Output the generated .wasm or .wat to FILE. @@ -71,7 +74,7 @@ OPTIONS skip typechecking pass -w VAL, --workers=VAL (absent=n) - number of workers for symbolic execution. Defaults to the number + Number of workers for symbolic execution. Defaults to the number of physical cores. --with-breadcrumbs diff --git a/dune-project b/dune-project index 7ed58e996..21a8aab23 100644 --- a/dune-project +++ b/dune-project @@ -80,6 +80,7 @@ (>= 1.0.3)) (xmlm (>= 1.4.0)) + domainpc ;; doc (odoc (and diff --git a/owi.opam b/owi.opam index c71d9ab67..2a5a7d73f 100644 --- a/owi.opam +++ b/owi.opam @@ -42,6 +42,7 @@ depends: [ "synchronizer" {>= "0.2"} "uutf" {>= "1.0.3"} "xmlm" {>= "1.4.0"} + "domainpc" "odoc" {>= "3.0.0" & with-doc} "mdx" {with-test & >= "2.1"} "frama-c" {>= "29.0" & with-test} @@ -82,3 +83,8 @@ post-messages: [ "Join our community on Zulip: https://owi.zulipchat.com/" "Explore tutorials and documentation here: https://ocamlpro.github.io/owi/" ] +pin-depends: [ + ["domainpc.dev" "git+https://github.com/ocamlpro/domainpc.git"] + ["landmarks.1.5" "git+https://github.com/hra687261/landmarks.git#cfc017b604f2c41ac0d8841f30a0b55b0d89cbaf"] + ["landmarks-ppx.1.5" "git+https://github.com/hra687261/landmarks.git#cfc017b604f2c41ac0d8841f30a0b55b0d89cbaf"] +] diff --git a/owi.opam.template b/owi.opam.template index abe9a436a..e60187165 100644 --- a/owi.opam.template +++ b/owi.opam.template @@ -11,3 +11,8 @@ post-messages: [ "Join our community on Zulip: https://owi.zulipchat.com/" "Explore tutorials and documentation here: https://ocamlpro.github.io/owi/" ] +pin-depends: [ + ["domainpc.dev" "git+https://github.com/ocamlpro/domainpc.git"] + ["landmarks.1.5" "git+https://github.com/hra687261/landmarks.git#cfc017b604f2c41ac0d8841f30a0b55b0d89cbaf"] + ["landmarks-ppx.1.5" "git+https://github.com/hra687261/landmarks.git#cfc017b604f2c41ac0d8841f30a0b55b0d89cbaf"] +] diff --git a/shell.nix b/shell.nix index 7f9741493..f5319b253 100644 --- a/shell.nix +++ b/shell.nix @@ -8,11 +8,27 @@ let src = pkgs.fetchFromGitHub { owner = "formalsec"; repo = "smtml"; - rev = "3b08a5368718068fa46547e60df4e44caa51db78"; - hash = "sha256-iD2UGddGYvE/jn+KM5jj05DHcNPjSq9IiH1BlnfO+Sg="; + rev = "e259d5b7d108cb2d1102c188132a6c86bbf7705e"; + hash = "sha256-8OzNJIyJhfqgDw3ioINN0D0WVTSliG9TP4cUNlrm4s8="; }; doCheck = false; }); + domainpc = pkgs.ocamlPackages.buildDunePackage (finalAttrs: { + + pname = "domainpc"; + version = "0.1"; + + src = pkgs.fetchFromGitHub { + owner = "ocamlpro"; + repo = "domainpc"; + rev = "9d5596c57154d925c6d7f17fe37dc2b9da0434bc"; + hash = "sha256-ttuv/G2J+7DsmDMMRtUOT1jITUtCoj9qQUXzfJ/yRfc="; + }; + + propagatedBuildInputs = [ + pkgs.ocamlPackages.processor + ]; + }); synchronizer = pkgs.ocamlPackages.synchronizer.overrideAttrs (old: { src = pkgs.fetchFromGitHub { owner = "ocamlpro"; @@ -21,6 +37,23 @@ let hash = "sha256-0XtPHpDlyH1h8W2ZlRvJbZjCN9WP5mzk2N01WFd8eLQ="; }; }); + landmarks = pkgs.ocamlPackages.landmarks.overrideAttrs (old: { + src = pkgs.fetchFromGitHub { + owner = "hra687261"; + repo = "landmarks"; + rev = "17be3567a63650090f9cf94654fcc8d99f946e27"; + hash = "sha256-3ui4uvSAvUgzk2UMVtH9A4BhAX6nWbwx7q0YwkANNv8="; + }; + }); + landmarks-ppx = pkgs.ocamlPackages.landmarks-ppx.overrideAttrs (old: { + src = pkgs.fetchFromGitHub { + owner = "hra687261"; + repo = "landmarks"; + rev = "17be3567a63650090f9cf94654fcc8d99f946e27"; + hash = "sha256-3ui4uvSAvUgzk2UMVtH9A4BhAX6nWbwx7q0YwkANNv8="; + }; + meta.broken = false; + }); in pkgs.mkShell { @@ -31,6 +64,8 @@ pkgs.mkShell { findlib bisect_ppx pkgs.framac + landmarks + landmarks-ppx pkgs.mdbook pkgs.mdbook-plugins mdx @@ -57,6 +92,7 @@ pkgs.mkShell { crowbar digestif dolmen_type + domainpc dune-build-info dune-site hc diff --git a/src/bin/owi.ml b/src/bin/owi.ml index c60dc810d..76e941bef 100644 --- a/src/bin/owi.ml +++ b/src/bin/owi.ml @@ -173,6 +173,10 @@ let no_value = let doc = "do not display a value for each symbol" in Arg.(value & flag & info [ "no-value" ] ~doc) +let no_worker_isolation = + let doc = "Do not force each worker to run on an isolated physical core." in + Arg.(value & flag & info [ "no-worker-isolation" ] ~doc) + let opt_lvl = let doc = "specify which optimization level to use" in Arg.(value & opt string "3" & info [ "O" ] ~doc) @@ -234,13 +238,10 @@ let unsafe = let workers = let doc = - "number of workers for symbolic execution. Defaults to the number of \ + "Number of workers for symbolic execution. Defaults to the number of \ physical cores." in - Arg.( - value - & opt int Processor.Query.core_count - & info [ "workers"; "w" ] ~doc ~absent:"n" ) + Arg.(value & opt (some int) None & info [ "workers"; "w" ] ~doc ~absent:"n") let workspace = let doc = "write results and intermediate compilation artifacts to dir" in @@ -259,6 +260,7 @@ let no_ite_for_select = let symbolic_parameters default_entry_point = let+ unsafe and+ workers + and+ no_worker_isolation and+ no_stop_at_failure and+ no_value and+ no_assert_failure_expression_printing @@ -276,6 +278,7 @@ let symbolic_parameters default_entry_point = let use_ite_for_select = not no_ite_for_select in { Symbolic_parameters.unsafe ; workers + ; no_worker_isolation ; no_stop_at_failure ; no_value ; no_assert_failure_expression_printing @@ -446,14 +449,15 @@ let iso_cmd = and+ solver and+ unsafe and+ workers + and+ no_worker_isolation and+ model_out_file and+ with_breadcrumbs and+ workspace in Cmd_iso.cmd ~deterministic_result_order ~fail_mode ~exploration_strategy ~files ~model_format ~no_assert_failure_expression_printing - ~no_stop_at_failure ~no_value ~solver ~unsafe ~workers ~workspace - ~model_out_file ~with_breadcrumbs + ~no_stop_at_failure ~no_value ~solver ~unsafe ~workers ~no_worker_isolation + ~workspace ~model_out_file ~with_breadcrumbs (* owi replay *) diff --git a/src/cmd/cmd_iso.ml b/src/cmd/cmd_iso.ml index 0bf3e3126..5ef402b36 100644 --- a/src/cmd/cmd_iso.ml +++ b/src/cmd/cmd_iso.ml @@ -297,8 +297,8 @@ module String_set = Set.Make (String) let cmd ~deterministic_result_order ~fail_mode ~exploration_strategy ~files ~model_format ~no_assert_failure_expression_printing ~no_stop_at_failure - ~no_value ~solver ~unsafe ~workers ~workspace ~model_out_file - ~with_breadcrumbs = + ~no_value ~solver ~unsafe ~workers ~no_worker_isolation ~workspace + ~model_out_file ~with_breadcrumbs = let* workspace = match workspace with | Some path -> Ok path @@ -407,7 +407,7 @@ let cmd ~deterministic_result_order ~fail_mode ~exploration_strategy ~files let run_time = if Log.is_bench_enabled () then Some 0. else None in Symbolic_driver.handle_result ~exploration_strategy ~fail_mode ~workers - ~solver ~deterministic_result_order ~model_format ~no_value - ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure - ~model_out_file ~with_breadcrumbs ~run_time result ) + ~no_worker_isolation ~solver ~deterministic_result_order ~model_format + ~no_value ~no_assert_failure_expression_printing ~workspace + ~no_stop_at_failure ~model_out_file ~with_breadcrumbs ~run_time result ) () common_exports diff --git a/src/cmd/cmd_iso.mli b/src/cmd/cmd_iso.mli index 0320e81cd..a5a54d97d 100644 --- a/src/cmd/cmd_iso.mli +++ b/src/cmd/cmd_iso.mli @@ -9,7 +9,8 @@ val cmd : -> no_value:bool -> solver:Smtml.Solver_type.t -> unsafe:bool - -> workers:int + -> workers:Int.t Option.t + -> no_worker_isolation:Bool.t -> workspace:Fpath.t option -> model_out_file:Fpath.t option -> with_breadcrumbs:bool diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index 05cdfe9c4..b97ca3035 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -54,6 +54,7 @@ let cmd ~parameters ~source_file = let { Symbolic_parameters.exploration_strategy ; fail_mode ; workers + ; no_worker_isolation ; solver ; deterministic_result_order ; model_format @@ -82,6 +83,6 @@ let cmd ~parameters ~source_file = let* result, run_time = run_file ~parameters ~source_file in Symbolic_driver.handle_result ~exploration_strategy ~fail_mode ~workers - ~solver ~deterministic_result_order ~model_format ~no_value - ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure - ~model_out_file ~with_breadcrumbs ~run_time result + ~no_worker_isolation ~solver ~deterministic_result_order ~model_format + ~no_value ~no_assert_failure_expression_printing ~workspace + ~no_stop_at_failure ~model_out_file ~with_breadcrumbs ~run_time result diff --git a/src/compile/binary_to_text.ml b/src/compile/binary_to_text.ml index bcf3a4a67..bb6ee50f8 100644 --- a/src/compile/binary_to_text.ml +++ b/src/compile/binary_to_text.ml @@ -2,7 +2,7 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -let convert_indice : Binary.indice -> Text.indice = function i -> Raw i +let convert_indice : Binary.indice -> Text.indice = function i -> Text.Raw i let convert_heap_type : Binary.heap_type -> Text.heap_type = function | TypeUse id -> TypeUse (Raw id) @@ -27,15 +27,15 @@ let convert_func_type ((pt, rt) : Binary.func_type) : Text.func_type = , List.map convert_val_type rt ) let convert_block_type : Binary.block_type -> Text.block_type = function - | Bt_raw (opt, ft) -> + | Binary.Bt_raw (opt, ft) -> let opt = Option.map convert_indice opt in - Bt_raw (opt, convert_func_type ft) + Text.Bt_raw (opt, convert_func_type ft) let rec convert_instr : Binary.instr -> Text.instr = function - | Br_table (ids, id) -> + | Binary.Br_table (ids, id) -> let ids = Array.map convert_indice ids in let id = convert_indice id in - Br_table (ids, id) + Text.Br_table (ids, id) | Br_if id -> let id = convert_indice id in Br_if id @@ -198,7 +198,7 @@ and convert_expr (e : Binary.expr Annotated.t) : Text.expr Annotated.t = e let convert_elem_mode : Binary.Elem.Mode.t -> Text.Elem.Mode.t = function - | Passive -> Passive + | Binary.Elem.Mode.Passive -> Text.Elem.Mode.Passive | Declarative -> Declarative | Active (opt, e) -> let opt = Option.map (fun i -> Text.Raw i) opt in @@ -206,21 +206,21 @@ let convert_elem_mode : Binary.Elem.Mode.t -> Text.Elem.Mode.t = function Active (opt, e) let convert_elem : Binary.Elem.t -> Text.Elem.t = function - | { id; typ; init; mode; explicit_typ } -> + | { Binary.Elem.id; typ; init; mode; explicit_typ } -> let init = List.map convert_expr init in let mode = convert_elem_mode mode in - { id; typ = convert_ref_type typ; init; mode; explicit_typ } + { Text.Elem.id; typ = convert_ref_type typ; init; mode; explicit_typ } let convert_data_mode : Binary.Data.Mode.t -> Text.Data.Mode.t = function - | Passive -> Passive + | Binary.Data.Mode.Passive -> Text.Data.Mode.Passive | Active (i, e) -> let e = convert_expr e in Active (Some (Raw i), e) let convert_data : Binary.Data.t -> Text.Data.t = function - | { id; init; mode } -> + | { Binary.Data.id; init; mode } -> let mode = convert_data_mode mode in - { id; init; mode } + { Text.Data.id; init; mode } let from_types types : Text.Module.Field.t list = Array.map diff --git a/src/dune b/src/dune index cc6c0f325..ac8e017a2 100644 --- a/src/dune +++ b/src/dune @@ -136,6 +136,7 @@ (libraries bos digestif + domainpc dune-build-info dune-site fmt diff --git a/src/ir/extern.ml b/src/ir/extern.ml index 838193545..80dcb0436 100644 --- a/src/ir/extern.ml +++ b/src/ir/extern.ml @@ -172,12 +172,15 @@ module Func = struct | 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 - | Mem (_, tl) -> 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 -> [] + let arg_type = + let rec aux : type t r. (t, r) atype -> Binary.param_type = function + | Mem (_, tl) -> aux tl + | UArg tl -> aux tl + | Arg (hd, tl) -> (None, elt_type hd) :: aux tl + | NArg (name, hd, tl) -> (Some name, elt_type hd) :: aux tl + | Res -> [] + in + aux (* TODO: we could move this out, as it does not really depend on the functor's parameters *) let extern_type (Extern_func (Func (arg, res), _)) : Binary.func_type = @@ -234,18 +237,24 @@ module Func = struct let label s (Elt v) = Elt_labeled (s, v) - let ( ^-> ) : type lr k a b. - (lr, k, a) t -> b func_type -> (a -> b) func_type = - fun a (Func (b, r)) -> - match a with - | Elt a -> Func (Arg (a, b), r) - | Elt_labeled (label, a) -> Func (NArg (label, a, b), r) - | Unit -> Func (UArg b, r) - | Memory id -> Func (Mem (id, b), r) - - let ( ^->. ) : type ll k kk a b. - (ll, k, a) t -> (lr, kk, b) t -> (a -> b m) func_type = - fun a b -> match b with Elt _ -> a ^-> r1 b | Unit -> a ^-> r0 + let ( ^-> ) = + let aux : type lr k a b. + (lr, k, a) t -> b func_type -> (a -> b) func_type = + fun a (Func (b, r)) -> + match a with + | Elt a -> Func (Arg (a, b), r) + | Elt_labeled (label, a) -> Func (NArg (label, a, b), r) + | Unit -> Func (UArg b, r) + | Memory id -> Func (Mem (id, b), r) + in + aux + + let ( ^->. ) = + let aux : type ll k kk a b. + (ll, k, a) t -> (lr, kk, b) t -> (a -> b m) func_type = + fun a b -> match b with Elt _ -> a ^-> r1 b | Unit -> a ^-> r0 + in + aux let ( ^->.. ) : type ll k a b1 b2. (ll, k, a) t diff --git a/src/owi.mli b/src/owi.mli index 8ec5cc551..e4b8bde52 100644 --- a/src/owi.mli +++ b/src/owi.mli @@ -1216,7 +1216,8 @@ module Symbolic_parameters : sig type t = { unsafe : bool - ; workers : int + ; workers : Int.t Option.t + ; no_worker_isolation : Bool.t ; no_stop_at_failure : bool ; no_value : bool ; no_assert_failure_expression_printing : bool @@ -1237,7 +1238,8 @@ end module Symbolic_driver : sig val handle_result : exploration_strategy:Symbolic_parameters.Exploration_strategy.t - -> workers:int + -> workers:Int.t Option.t + -> no_worker_isolation:Bool.t -> no_stop_at_failure:bool -> no_value:bool -> no_assert_failure_expression_printing:bool @@ -1323,7 +1325,8 @@ module Cmd_iso : sig -> no_value:bool -> solver:Smtml.Solver_type.t -> unsafe:bool - -> workers:int + -> workers:Int.t Option.t + -> no_worker_isolation:Bool.t -> workspace:Fpath.t option -> model_out_file:Fpath.t option -> with_breadcrumbs:bool diff --git a/src/script/script.ml b/src/script/script.ml index b9d724fb3..b29501e5d 100644 --- a/src/script/script.ml +++ b/src/script/script.ml @@ -147,7 +147,7 @@ let compare_result_const result (const : Concrete_value.t) = assert false let value_of_const : Wast.const -> Concrete_value.t = function - | Const_I32 v -> Concrete_value.I32 v + | Wast.Const_I32 v -> Concrete_value.I32 v | Const_I64 v -> Concrete_value.I64 v | Const_F32 v -> Concrete_value.F32 v | Const_F64 v -> Concrete_value.F64 v diff --git a/src/symbolic/scheduler.ml b/src/symbolic/scheduler.ml index 9424ba156..6c8896f72 100644 --- a/src/symbolic/scheduler.ml +++ b/src/symbolic/scheduler.ml @@ -59,27 +59,25 @@ module Make (Work_datastructure : Prio.S) = struct (fun f write_back -> inner (f ()) write_back) sched.work_queue - let spawn_worker sched - ~(at_worker_value : close_work_queue:(unit -> unit) -> 'a -> unit) - ~at_worker_init ~finally = - at_worker_init (); - Domain.spawn (fun () -> - Fun.protect ~finally (fun () -> - try - work sched - (at_worker_value ~close_work_queue:(fun () -> - Work_datastructure.close sched.work_queue ) ) - with e -> - let e_s = Printexc.to_string e in - let bt = Printexc.get_raw_backtrace () in - let bt_s = Printexc.raw_backtrace_to_string bt in - let bt_s = - if String.equal "" bt_s then - "use OCAMLRUNPARAM=b to get the backtrace" - else bt_s - in - Log.err (fun m -> - m "a worker ended with exception %s, backtrace is: @\n@[%s@]" e_s - bt_s ); - Printexc.raise_with_backtrace e bt ) ) + let run_worker sched + ~(at_worker_value : close_work_queue:(unit -> unit) -> 'a -> unit) ~finally + = + Fun.protect ~finally (fun () -> + try + work sched + (at_worker_value ~close_work_queue:(fun () -> + Work_datastructure.close sched.work_queue ) ) + with e -> + let e_s = Printexc.to_string e in + let bt = Printexc.get_raw_backtrace () in + let bt_s = Printexc.raw_backtrace_to_string bt in + let bt_s = + if String.equal "" bt_s then + "use OCAMLRUNPARAM=b to get the backtrace" + else bt_s + in + Log.err (fun m -> + m "a worker ended with exception %s, backtrace is: @\n@[%s@]" e_s + bt_s ); + Printexc.raise_with_backtrace e bt ) end diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index d47e9d0fe..aad2d5b16 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -67,8 +67,8 @@ let stop = lift_schedulable Scheduler.Schedulable.stop Now this is actual symbolic execution stuff! ============================================ *) -let run exploration_strategy ~workers solver t thread ~at_worker_value - ~at_worker_init ~at_worker_end = +let run exploration_strategy ~workers solver t thread ~no_worker_isolation + ~at_worker_value ~at_worker_init ~at_worker_end = solver_to_use := Some solver; let module M = ( val Symbolic_parameters.Exploration_strategy.to_work_ds_module @@ -77,10 +77,32 @@ let run exploration_strategy ~workers solver t thread ~at_worker_value let module Scheduler = Scheduler.Make (M) in let sched = Scheduler.init () in Scheduler.add_init_task sched (Fun.const @@ State_monad.run t thread); + + (* + * TODO: try this at some point? It's likely going to make things bad but who knows... + * Domainpc.isolate_current (); + *) + let workers = + match workers with + | None -> + let n = Domainpc.get_available_cores () in + assert (n > 0); + n + | Some n -> n + in + + assert (workers > 0); + if workers > 1 then Logs_threaded.enable (); - Array.init workers (fun _i -> - Scheduler.spawn_worker sched ~at_worker_value ~at_worker_init - ~finally:at_worker_end ) + + for _i = 1 to workers do + at_worker_init () + done; + + let isolated = not no_worker_isolation in + + Domainpc.spawn_n ~isolated ~n:workers (fun () -> + Scheduler.run_worker sched ~at_worker_value ~finally:at_worker_end ) let add_pc (c : Symbolic_boolean.t) = let c = Smtml.Typed.simplify c in diff --git a/src/symbolic/symbolic_choice.mli b/src/symbolic/symbolic_choice.mli index ac753298d..775782143 100644 --- a/src/symbolic/symbolic_choice.mli +++ b/src/symbolic/symbolic_choice.mli @@ -52,10 +52,11 @@ val close_scope : unit -> unit t val run : Symbolic_parameters.Exploration_strategy.t - -> workers:int + -> workers:int option -> Smtml.Solver_type.t -> 'a t -> Thread.t + -> no_worker_isolation:bool -> at_worker_value: (close_work_queue:(unit -> unit) -> ('a, Bug.t) result * Thread.t -> unit) -> at_worker_init:(unit -> unit) diff --git a/src/symbolic/symbolic_driver.ml b/src/symbolic/symbolic_driver.ml index 0f015b4a5..5d3eb6f58 100644 --- a/src/symbolic/symbolic_driver.ml +++ b/src/symbolic/symbolic_driver.ml @@ -52,10 +52,11 @@ let mk_callback no_stop_at_failure fail_mode res_stack path_count = end end -let handle_result ~exploration_strategy ~workers ~no_stop_at_failure ~no_value - ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode - ~workspace ~solver ~model_format ~model_out_file ~with_breadcrumbs ~run_time - (result : unit Symbolic_choice.t) = +let handle_result ~exploration_strategy ~workers ~no_worker_isolation + ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing + ~deterministic_result_order ~fail_mode ~workspace ~solver ~model_format + ~model_out_file ~with_breadcrumbs ~run_time (result : unit Symbolic_choice.t) + = let thread = Thread.init () in let bug_stack = Bugs.make () in let path_count = Atomic.make 0 in @@ -65,7 +66,7 @@ let handle_result ~exploration_strategy ~workers ~no_stop_at_failure ~no_value let time_before = (Unix.times ()).tms_utime in let domains : unit Domain.t Array.t = Symbolic_choice.run exploration_strategy ~workers solver result thread - ~at_worker_value + ~no_worker_isolation ~at_worker_value ~at_worker_init:(fun () -> Bugs.new_pledge bug_stack) ~at_worker_end:(fun () -> Bugs.end_pledge bug_stack) in @@ -111,8 +112,14 @@ let handle_result ~exploration_strategy ~workers ~no_stop_at_failure ~no_value Benchmark.print_final ~bench_stats ~execution_time_a:run_time ~execution_time_b ~wait_for_all_domains end - else if Log.is_debug_enabled () then begin - (* we only do this in debug mode because otherwise it makes performances very bad *) + else if + let landmark_profiling_enabled = + Option.is_some @@ Bos.OS.Env.var "OCAML_LANDMARKS" + in + Log.is_debug_enabled () || landmark_profiling_enabled + then begin + (* we only do this in debug mode or when landmarks profiling is on because + otherwise it makes performances very bad *) wait_for_all_domains () end; diff --git a/src/symbolic/symbolic_driver.mli b/src/symbolic/symbolic_driver.mli index 6c829577d..b735d2b08 100644 --- a/src/symbolic/symbolic_driver.mli +++ b/src/symbolic/symbolic_driver.mli @@ -4,7 +4,8 @@ val handle_result : exploration_strategy:Symbolic_parameters.Exploration_strategy.t - -> workers:int + -> workers:Int.t Option.t + -> no_worker_isolation:Bool.t -> no_stop_at_failure:bool -> no_value:bool -> no_assert_failure_expression_printing:bool diff --git a/src/symbolic/symbolic_parameters.ml b/src/symbolic/symbolic_parameters.ml index 15f9cb147..ff768b364 100644 --- a/src/symbolic/symbolic_parameters.ml +++ b/src/symbolic/symbolic_parameters.ml @@ -17,7 +17,7 @@ module Exploration_strategy = struct | Rarity_depth_loop_aging_random let to_priority_module : t -> (module Prio.T) = function - | LIFO -> (module Prio.LIFO) + | LIFO -> (module Prio.LIFO : Prio.T) | FIFO -> (module Prio.FIFO) | Random -> (module Prio.Random_prio) | Random_unseen_then_random -> (module Prio.Random_unseen_then_random) @@ -65,7 +65,8 @@ end type t = { unsafe : bool - ; workers : int + ; workers : Int.t Option.t + ; no_worker_isolation : Bool.t ; no_stop_at_failure : bool ; no_value : bool ; no_assert_failure_expression_printing : bool diff --git a/src/symbolic/symbolic_parameters.mli b/src/symbolic/symbolic_parameters.mli index e433e5df7..dd07c9fc0 100644 --- a/src/symbolic/symbolic_parameters.mli +++ b/src/symbolic/symbolic_parameters.mli @@ -25,7 +25,8 @@ end type t = { unsafe : bool - ; workers : int + ; workers : Int.t Option.t + ; no_worker_isolation : Bool.t ; no_stop_at_failure : bool ; no_value : bool ; no_assert_failure_expression_printing : bool