From a8067c4bf17e3881490dd34986b2717af422a007 Mon Sep 17 00:00:00 2001 From: Arthur Carcano Date: Mon, 24 Jun 2024 18:05:01 +0200 Subject: [PATCH] wip --- src/bin/owi.ml | 8 +- src/cmd/cmd_c.ml | 7 +- src/cmd/cmd_c.mli | 1 + src/cmd/cmd_conc.ml | 5 +- src/cmd/cmd_conc.mli | 1 + src/cmd/cmd_sym.ml | 5 +- src/cmd/cmd_sym.mli | 1 + src/dune | 1 + src/symbolic/solver.ml | 16 +++- src/symbolic/symbolic_choice.ml | 15 +++- src/utils/stats.ml | 131 ++++++++++++++++++++++++++++++++ 11 files changed, 179 insertions(+), 12 deletions(-) create mode 100644 src/utils/stats.ml diff --git a/src/bin/owi.ml b/src/bin/owi.ml index b7b50dc21..78d95ba5d 100644 --- a/src/bin/owi.ml +++ b/src/bin/owi.ml @@ -66,6 +66,8 @@ let solver = & opt solver_conv Smtml.Solver_dispatcher.Z3_solver & info [ "solver"; "s" ] ~doc ) +let profile = Cmdliner.Term.const @@ Some (Fpath.v "profile.json") + let unsafe = let doc = "skip typechecking pass" in Cmdliner.Arg.(value & flag & info [ "unsafe"; "u" ] ~doc) @@ -136,7 +138,7 @@ let c_cmd = 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 - $ solver ) + $ solver $ profile ) let fmt_cmd = let open Cmdliner in @@ -202,7 +204,7 @@ let sym_cmd = Term.( const Cmd_sym.cmd $ profiling $ debug $ unsafe $ optimize $ workers $ no_stop_at_failure $ no_values $ deterministic_result_order $ workspace - $ solver $ files ) + $ solver $ profile $ files ) let conc_cmd = let open Cmdliner in @@ -215,7 +217,7 @@ let conc_cmd = Term.( const Cmd_conc.cmd $ profiling $ debug $ unsafe $ optimize $ workers $ no_stop_at_failure $ no_values $ deterministic_result_order $ workspace - $ solver $ files ) + $ solver $ profile $ files ) let wasm2wat_cmd = let open Cmdliner in diff --git a/src/cmd/cmd_c.ml b/src/cmd/cmd_c.ml index 77b4a265c..48afc3f3a 100644 --- a/src/cmd/cmd_c.ml +++ b/src/cmd/cmd_c.ml @@ -120,7 +120,10 @@ let metadata ~workspace arch property files : unit Result.t = 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 solver : unit Result.t = + deterministic_result_order concolic solver profile : unit Result.t = + begin + match profile with None -> () | Some f -> Stats.init_logger_to_file f + end; if debug then Logs.set_level (Some Debug); let workspace = Fpath.v workspace in let includes = libc_location @ includes in @@ -131,4 +134,4 @@ let cmd debug arch property _testcomp workspace workers opt_lvl includes files 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 solver files + deterministic_result_order workspace solver None files diff --git a/src/cmd/cmd_c.mli b/src/cmd/cmd_c.mli index 2a2b73d17..b58e84bde 100644 --- a/src/cmd/cmd_c.mli +++ b/src/cmd/cmd_c.mli @@ -20,4 +20,5 @@ val cmd : -> bool -> bool -> Smtml.Solver_dispatcher.solver_type + -> Fpath.t option -> unit Result.t diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml index 0b2867bff..108f9d8b3 100644 --- a/src/cmd/cmd_conc.ml +++ b/src/cmd/cmd_conc.ml @@ -403,7 +403,10 @@ let launch solver tree link_state modules_to_run = which are handled here. Most of the computations are done in the Result monad, hence the let*. *) let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values - deterministic_result_order (workspace : Fpath.t) solver files = + deterministic_result_order (workspace : Fpath.t) solver profile files = + begin + match profile with None -> () | Some f -> Stats.init_logger_to_file f + end; ignore (workers, no_stop_at_failure, deterministic_result_order, workspace); if profiling then Log.profiling_on := true; diff --git a/src/cmd/cmd_conc.mli b/src/cmd/cmd_conc.mli index 2a258b383..d6e0e04fa 100644 --- a/src/cmd/cmd_conc.mli +++ b/src/cmd/cmd_conc.mli @@ -13,5 +13,6 @@ val cmd : -> bool -> Fpath.t -> Smtml.Solver_dispatcher.solver_type + -> Fpath.t option -> Fpath.t list -> unit Result.t diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index 1c916a308..bee253685 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -50,7 +50,10 @@ let run_file ~unsafe ~optimize pc filename = which are handled here. Most of the computations are done in the Result monad, hence the let*. *) let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values - deterministic_result_order (workspace : Fpath.t) solver files = + deterministic_result_order (workspace : Fpath.t) solver profile files = + begin + match profile with None -> () | Some f -> Stats.init_logger_to_file f + end; if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; (* deterministic_result_order implies no_stop_at_failure *) diff --git a/src/cmd/cmd_sym.mli b/src/cmd/cmd_sym.mli index 2a258b383..d6e0e04fa 100644 --- a/src/cmd/cmd_sym.mli +++ b/src/cmd/cmd_sym.mli @@ -13,5 +13,6 @@ val cmd : -> bool -> Fpath.t -> Smtml.Solver_dispatcher.solver_type + -> Fpath.t option -> Fpath.t list -> unit Result.t diff --git a/src/dune b/src/dune index 738236bb2..08260c648 100644 --- a/src/dune +++ b/src/dune @@ -69,6 +69,7 @@ symbolic_wasm_ffi spectest stack + stats string_map syntax text diff --git a/src/symbolic/solver.ml b/src/symbolic/solver.ml index 76316f5f6..1c2e82a3e 100644 --- a/src/symbolic/solver.ml +++ b/src/symbolic/solver.ml @@ -15,12 +15,20 @@ let fresh solver () = S ((module Batch), solver) let check (S (solver_module, s)) pc = + Stats.start_span "check" "solver"; let module Solver = (val solver_module) in - Solver.check s pc + let res = Solver.check s pc in + Stats.close_span (); + res let model (S (solver_module, s)) ~symbols ~pc = + Stats.start_span "model" "solver"; let module Solver = (val solver_module) in assert (Solver.check s pc = `Sat); - match Solver.model ?symbols s with - | None -> assert false - | Some model -> model + let res = + match Solver.model ?symbols s with + | None -> assert false + | Some model -> model + in + Stats.close_span (); + res diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index 46e286d48..2447d4e3a 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -48,6 +48,8 @@ module CoreImpl : sig val with_thread : (Thread.t -> 'a) -> 'a t + val lazily : (unit -> 'a) -> 'a t + val set_thread : Thread.t -> unit t val modify_thread : (Thread.t -> Thread.t) -> unit t @@ -270,6 +272,8 @@ end = struct let with_thread f = lift (State.with_state (fun st -> (f st, st))) + let lazily f = with_thread (fun _th -> f ()) + let thread = with_thread Fun.id let modify_thread f = lift (State.modify_state f) @@ -386,12 +390,20 @@ let select_inner ~explore_first (cond : Symbolic_value.vbool) = let true_branch = let* () = add_pc v in let* () = add_breadcrumb 1l in + let* () = + lazily (fun () -> + Stats.event "check true branch reachability" "branches" ) + 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* () = + lazily (fun () -> + Stats.event "check true branch reachability" "branches" ) + in let+ () = check_reachability in false in @@ -444,7 +456,8 @@ let select_i32 (i : Symbolic_value.int32) = in let this_val_branch = let* () = add_breadcrumb i in - let+ () = add_pc this_value_cond in + let* () = add_pc this_value_cond in + let+ () = lazily (fun () -> Stats.event "selected n" "branches") in i in let not_this_val_branch = diff --git a/src/utils/stats.ml b/src/utils/stats.ml new file mode 100644 index 000000000..bd49704db --- /dev/null +++ b/src/utils/stats.ml @@ -0,0 +1,131 @@ +type logger = + { channel : out_channel + ; mutex : Mutex.t + } + +let global_stats_logger : logger option ref = ref None + +let init_logger_to_file f = + let logger = + { channel = Out_channel.open_text (Fpath.to_string f) + ; mutex = Mutex.create () + } + in + Out_channel.output_char logger.channel '['; + global_stats_logger := Some logger + +(* Be careful that f will be run in the critical section + so should be kept small *) +let on_logger f = + match !global_stats_logger with + | None -> () + | Some logger -> begin + Mutex.protect logger.mutex (fun () -> f logger.channel) + end + +(* assumes that v does not need escaping*) +let emit_key_val_s ch ?(end_comma = true) k v = + Out_channel.output_char ch '"'; + Out_channel.output_string ch k; + Out_channel.output_char ch '"'; + Out_channel.output_string ch {|:"|}; + Out_channel.output_string ch v; + Out_channel.output_char ch '"'; + if end_comma then Out_channel.output_char ch ',' + +(* assumes that v does not need escaping*) +let emit_key_val_i ch ?(end_comma = true) k v = + Out_channel.output_char ch '"'; + Out_channel.output_string ch k; + Out_channel.output_char ch '"'; + Out_channel.output_char ch ':'; + Out_channel.output_string ch @@ Int.to_string v; + if end_comma then Out_channel.output_char ch ',' + +type scope = + | Global + | Process + | Thread + +let event ?(scope = Thread) ?(arg_writter = None) name cat = + let pid = Unix.getpid () in + let tid = (Domain.self () :> int) in + let ts = Int.of_float (Unix.gettimeofday () *. 1e6) in + let scope = + match scope with Global -> "g" | Process -> "p" | Thread -> "t" + in + on_logger (fun ch -> + begin + Out_channel.output_string ch "{"; + emit_key_val_s ch "name" name; + emit_key_val_s ch "cat" cat; + emit_key_val_s ch "ph" "i"; + emit_key_val_i ch "ts" ts; + emit_key_val_i ch "pid" pid; + emit_key_val_i ch "tid" tid; + emit_key_val_s ch "s" scope ~end_comma:false; + begin + match arg_writter with + | None -> () + | Some arg_writter -> begin + Out_channel.output_string ch {|,"args":{|}; + arg_writter ch; + Out_channel.output_char ch '}' + end + end; + Out_channel.output_string ch "}," + end ) + +let start_span ?(arg_writter = None) name cat = + let pid = Unix.getpid () in + let tid = (Domain.self () :> int) in + let ts = Int.of_float (Unix.gettimeofday () *. 1e6) in + on_logger (fun ch -> + begin + Out_channel.output_string ch "{"; + emit_key_val_s ch "name" name; + emit_key_val_s ch "cat" cat; + emit_key_val_s ch "ph" "B"; + emit_key_val_i ch "ts" ts; + emit_key_val_i ch "pid" pid; + emit_key_val_i ch "tid" tid ~end_comma:false; + begin + match arg_writter with + | None -> () + | Some arg_writter -> begin + Out_channel.output_string ch {|,"args":{|}; + arg_writter ch; + Out_channel.output_char ch '}' + end + end; + Out_channel.output_string ch "}," + end ) + +let close_span () = + let pid = Unix.getpid () in + let tid = (Domain.self () :> int) in + let ts = Int.of_float (Unix.gettimeofday () *. 1e6) in + on_logger (fun ch -> + begin + Out_channel.output_string ch "{"; + emit_key_val_s ch "ph" "E"; + emit_key_val_i ch "ts" ts; + emit_key_val_i ch "pid" pid; + emit_key_val_i ch "tid" tid ~end_comma:false; + Out_channel.output_string ch "}," + end ) + +(* { + "name": "myName", + "cat": "category,list", + "ph": "B", + "ts": 12345, + "pid": 123, + "tid": 456, + "args": { + "someArg": 1, + "anotherArg": { + "value": "my value" + } + } *) +(* } *)