[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

@@ -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 =

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 rename r s =
-let or_ us r s = wrap (fun () -> or_ us r s) (fun () -> Or_ (us, r, s))
+  wrap rename_tmr (fun () -> rename r s) (fun () -> Rename (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 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))

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

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

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 <spec>]         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 <spec>]         enable debug tracing
   [-help]                 print this help text and exit
                           (alias: -?)
@@ -197,6 +199,7 @@ The <input> file must be binary LLAIR, such as produced by `sledge translate`.
   [-margin <cols>]       wrap debug tracing at <cols> 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 <spec>]        enable debug tracing
   [-help]                print this help text and exit
                          (alias: -?)