wip

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

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

src/cmd/cmd_c.mli

@@ -20,4 +20,5 @@ val cmd :
  -> bool
  -> bool
  -> Smtml.Solver_dispatcher.solver_type
+ -> Fpath.t option
  -> unit Result.t

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;

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

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 *)

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

src/dune

@@ -67,6 +67,7 @@
  symbolic_wasm_ffi
  spectest
  stack
+ stats
  string_map
  syntax
  text

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

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
@@ -271,6 +273,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)
@@ -380,12 +384,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
@@ -438,7 +450,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 =

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"
+ }
+ } *)
+(* } *)