From c8e75e3b829c94e789c3684b355e474d5a9508a8 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 16 Apr 2020 03:37:12 -0700 Subject: [PATCH] [sledge] Dump perf diagnostics and replays for slow queries to stderr Summary: Generate output on stderr containing lines such as: ``` solve_for_vars time: 0.105 ms 0.871 ms 79 calls ``` which indicates that the current maximal time of a single `solve_for_vars` query is `0.105 ms` and so far the total time spent in `solve_for_vars` over `79` queries is `0.871 ms`. At program exit, there is also a line for each timer indicating the max query time and final accumulated duration and number of queries: ``` solve_for_vars time: 0.173 ms 17.242 ms 1108 calls ``` Additionally, replay sexp are dumped interactively. A query exceeding 1 sec is dumped, then one exceeding 2 sec, then 4 sec, etc. Reviewed By: jvillard Differential Revision: D20852160 fbshipit-source-id: 0a316891e --- sledge/bin/sledge_cli.ml | 3 ++ sledge/lib/equality.ml | 64 +++++++++++++++++++++++++++++++------ sledge/lib/timer.ml | 68 ++++++++++++++++++++++++++++++++++++++++ sledge/lib/timer.mli | 53 +++++++++++++++++++++++++++++++ sledge/sledge-help.txt | 3 ++ 5 files changed, 182 insertions(+), 9 deletions(-) create mode 100644 sledge/lib/timer.ml create mode 100644 sledge/lib/timer.mli diff --git a/sledge/bin/sledge_cli.ml b/sledge/bin/sledge_cli.ml index 8effdf035..92a777d73 100644 --- a/sledge/bin/sledge_cli.ml +++ b/sledge/bin/sledge_cli.ml @@ -115,6 +115,8 @@ let analyze = and no_simplify_states = flag "no-simplify-states" no_arg ~doc:"do not simplify states during symbolic execution" + and stats = + flag "stats" no_arg ~doc:"output performance statistics to stderr" in fun program () -> let pgm = program () in @@ -122,6 +124,7 @@ let analyze = let entry_points = Config.find_list "entry-points" in let skip_throw = not exceptions in Domain_sh.simplify_states := not no_simplify_states ; + Timer.enabled := stats ; exec {bound; skip_throw; function_summaries; entry_points; globals} pgm let analyze_cmd = diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml index 84b0de9fa..835762e0f 100644 --- a/sledge/lib/equality.ml +++ b/sledge/lib/equality.ml @@ -1019,6 +1019,7 @@ let solve_for_vars vss r = (* Replay debugging *) type call = + | Normalize of t * Term.t | And_eq of Var.Set.t * Term.t * Term.t * t | And_term of Var.Set.t * Term.t * t | And_ of Var.Set.t * t * t @@ -1031,6 +1032,7 @@ type call = let replay c = match call_of_sexp (Sexp.of_string c) with + | Normalize (r, e) -> normalize r e |> ignore | And_eq (us, a, b, r) -> and_eq us a b r |> ignore | And_term (us, e, r) -> and_term us e r |> ignore | And_ (us, r, s) -> and_ us r s |> ignore @@ -1042,24 +1044,68 @@ let replay c = (* Debug wrappers *) -let wrap f call = +let report ~name ~elapsed ~aggregate ~count = + Format.eprintf "%15s time: %12.3f ms %12.3f ms %12d calls@." name + elapsed aggregate count + +let dump_threshold = ref 1000. + +let wrap tmr f call = + let f () = + Timer.start tmr ; + let r = f () in + Timer.stop_report tmr (fun ~name ~elapsed ~aggregate ~count -> + report ~name ~elapsed ~aggregate ~count ; + if Float.(elapsed > !dump_threshold) then ( + dump_threshold := 2. *. !dump_threshold ; + Format.eprintf "@\n%a@\n@." Sexp.pp_hum (sexp_of_call (call ())) ) + ) ; + r + in if not [%debug] then f () else try f () with exn -> raise_s ([%sexp_of: exn * call] (exn, call ())) +let normalize_tmr = Timer.create "normalize" ~at_exit:report +let and_eq_tmr = Timer.create "and_eq" ~at_exit:report +let and_term_tmr = Timer.create "and_term" ~at_exit:report +let and_tmr = Timer.create "and_" ~at_exit:report +let or_tmr = Timer.create "or_" ~at_exit:report +let orN_tmr = Timer.create "orN" ~at_exit:report +let rename_tmr = Timer.create "rename" ~at_exit:report +let apply_subst_tmr = Timer.create "apply_subst" ~at_exit:report +let solve_for_vars_tmr = Timer.create "solve_for_vars" ~at_exit:report + +let normalize r e = + wrap normalize_tmr (fun () -> normalize r e) (fun () -> Normalize (r, e)) + let and_eq us a b r = - wrap (fun () -> and_eq us a b r) (fun () -> And_eq (us, a, b, r)) + wrap and_eq_tmr + (fun () -> and_eq us a b r) + (fun () -> And_eq (us, a, b, r)) let and_term us e r = - wrap (fun () -> and_term us e r) (fun () -> And_term (us, e, r)) + wrap and_term_tmr + (fun () -> and_term us e r) + (fun () -> And_term (us, e, r)) + +let and_ us r s = + wrap and_tmr (fun () -> and_ us r s) (fun () -> And_ (us, r, s)) + +let or_ us r s = + wrap or_tmr (fun () -> or_ us r s) (fun () -> Or_ (us, r, s)) + +let orN us rs = wrap orN_tmr (fun () -> orN us rs) (fun () -> OrN (us, rs)) -let and_ us r s = wrap (fun () -> and_ us r s) (fun () -> And_ (us, r, s)) -let or_ us r s = wrap (fun () -> or_ us r s) (fun () -> Or_ (us, r, s)) -let orN us rs = wrap (fun () -> orN us rs) (fun () -> OrN (us, rs)) -let rename r s = wrap (fun () -> rename r s) (fun () -> Rename (r, s)) +let rename r s = + wrap rename_tmr (fun () -> rename r s) (fun () -> Rename (r, s)) let apply_subst us s r = - wrap (fun () -> apply_subst us s r) (fun () -> Apply_subst (us, s, r)) + wrap apply_subst_tmr + (fun () -> apply_subst us s r) + (fun () -> Apply_subst (us, s, r)) let solve_for_vars vss r = - wrap (fun () -> solve_for_vars vss r) (fun () -> Solve_for_vars (vss, r)) + wrap solve_for_vars_tmr + (fun () -> solve_for_vars vss r) + (fun () -> Solve_for_vars (vss, r)) diff --git a/sledge/lib/timer.ml b/sledge/lib/timer.ml new file mode 100644 index 000000000..4f32ea7d4 --- /dev/null +++ b/sledge/lib/timer.ml @@ -0,0 +1,68 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Timers for runtime statistics *) + +type t = + { mutable ustart: float + ; mutable sstart: float + ; mutable uaggregate: float + ; mutable saggregate: float + ; mutable count: int + ; mutable max: float + ; mutable threshold: float + ; name: string } + +let enabled = ref false + +let start t = + if !enabled then ( + let {Unix.tms_utime; tms_stime} = Unix.times () in + t.ustart <- tms_utime ; + t.sstart <- tms_stime ) + +let stop_ t = + let {Unix.tms_utime; tms_stime} = Unix.times () in + let ud = tms_utime -. t.ustart in + let sd = tms_stime -. t.sstart in + t.uaggregate <- t.uaggregate +. ud ; + t.saggregate <- t.saggregate +. sd ; + let usd = ud +. sd in + if Float.(t.max < usd) then t.max <- usd ; + t.count <- t.count + 1 ; + (tms_utime, tms_stime) + +let stop t = if !enabled then stop_ t |> (ignore : float * float -> unit) + +let stop_report t report = + if !enabled then + let tms_utime, tms_stime = stop_ t in + let elapsed = tms_utime +. tms_stime -. (t.ustart +. t.sstart) in + if Float.(elapsed > t.threshold) then ( + t.threshold <- elapsed ; + report ~name:t.name ~elapsed:(elapsed *. 1000.) + ~aggregate:((t.uaggregate +. t.saggregate) *. 1000.) + ~count:t.count ) + +let create ?at_exit:printf name = + let t = + { ustart= 0. + ; uaggregate= 0. + ; sstart= 0. + ; saggregate= 0. + ; count= 0 + ; max= 0. + ; threshold= 0. + ; name } + in + Option.iter printf ~f:(fun report -> + at_exit (fun () -> + if !enabled then + report ~name:t.name ~elapsed:(t.max *. 1000.) + ~aggregate:((t.uaggregate +. t.saggregate) *. 1000.) + ~count:t.count ) ) ; + t diff --git a/sledge/lib/timer.mli b/sledge/lib/timer.mli new file mode 100644 index 000000000..7d632f039 --- /dev/null +++ b/sledge/lib/timer.mli @@ -0,0 +1,53 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Timers for runtime statistics *) + +type t = private + { mutable ustart: float + ; mutable sstart: float + ; mutable uaggregate: float + ; mutable saggregate: float + ; mutable count: int + ; mutable max: float + ; mutable threshold: float + ; name: string } + +val create : + ?at_exit: + ( name:string + -> elapsed:float + -> aggregate:float + -> count:int + -> unit) + -> string + -> t +(** Construct a timer with the given name and register the given function to + run at exit. The [at_exit] function receives [name]: the name of the + timer passed to [create], [elapsed]: the number of milliseconds between + the longest single [start]-[stop] pair, [aggregate]: the sum of the time + that elapsed while the named timer was running, [count]: the number of + times [stop] was called on the timer. *) + +val start : t -> unit +(** Start a timer. *) + +val stop : t -> unit +(** Stop a timer. *) + +val stop_report : + t + -> (name:string -> elapsed:float -> aggregate:float -> count:int -> unit) + -> unit +(** Stop a timer and report using the given function, which receives [name]: + the name of the timer passed to [create], [elapsed]: the number of + milliseconds since [start] was called, [aggregate]: the sum of the time + that has elapsed while the timer was running, [count]: the number of + times [stop] has been called on the timer. *) + +val enabled : bool ref +(** Timers do nothing unless [enabled] is set. *) diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt index 7a745e09e..c4986bc85 100644 --- a/sledge/sledge-help.txt +++ b/sledge/sledge-help.txt @@ -63,6 +63,7 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s libraries [-no-simplify-states] do not simplify states during symbolic execution [-preanalyze-globals] pre-analyze global variables used by each function + [-stats] output performance statistics to stderr [-trace ] enable debug tracing [-help] print this help text and exit (alias: -?) @@ -149,6 +150,7 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo libraries [-no-simplify-states] do not simplify states during symbolic execution [-preanalyze-globals] pre-analyze global variables used by each function + [-stats] output performance statistics to stderr [-trace ] enable debug tracing [-help] print this help text and exit (alias: -?) @@ -197,6 +199,7 @@ The file must be binary LLAIR, such as produced by `sledge translate`. [-margin ] wrap debug tracing at columns [-no-simplify-states] do not simplify states during symbolic execution [-preanalyze-globals] pre-analyze global variables used by each function + [-stats] output performance statistics to stderr [-trace ] enable debug tracing [-help] print this help text and exit (alias: -?)