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

@@ -69,6 +69,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
@@ -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 =

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