diff options
Diffstat (limited to 'ltac/profile_ltac.ml')
| -rw-r--r-- | ltac/profile_ltac.ml | 323 |
1 files changed, 323 insertions, 0 deletions
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml new file mode 100644 index 000000000..7a8ef32c3 --- /dev/null +++ b/ltac/profile_ltac.ml @@ -0,0 +1,323 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Unicode +open Pp +open Printer +open Util + +(** [is_profiling] and the profiling info ([stack]) should be synchronized with + the document; the rest of the ref cells are either local to individual + tactic invocations, or global flags, and need not be synchronized, since no + document-level backtracking happens within tactics. We synchronize + is_profiling via an option. *) +let is_profiling = Flags.profile_ltac + +let set_profiling b = is_profiling := b +let get_profiling () = !is_profiling + +let new_call = ref false +let entered_call () = new_call := true +let is_new_call () = let b = !new_call in new_call := false; b + +(** LtacProf cannot yet handle backtracking into multi-success tactics. + To properly support this, we'd have to somehow recreate our location in the + call-stack, and stop/restart the intervening timers. This is tricky and + possibly expensive, so instead we currently just emit a warning that + profiling results will be off. *) +let encountered_multi_success_backtracking = ref false + +let warn_encountered_multi_success_backtracking () = + if !encountered_multi_success_backtracking then + Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking \ + into multi-success tactics; profiling results may be wildly inaccurate.") + +let encounter_multi_success_backtracking () = + if not !encountered_multi_success_backtracking + then begin + encountered_multi_success_backtracking := true; + warn_encountered_multi_success_backtracking () + end + +type entry = { + mutable total : float; + mutable local : float; + mutable ncalls : int; + mutable max_total : float +} + +let empty_entry () = { total = 0.; local = 0.; ncalls = 0; max_total = 0. } + +let add_entry e add_total { total; local; ncalls; max_total } = + if add_total then e.total <- e.total +. total; + e.local <- e.local +. local; + e.ncalls <- e.ncalls + ncalls; + if add_total then e.max_total <- max e.max_total max_total + +type treenode = { + entry : entry; + children : (string, treenode) Hashtbl.t +} + +let empty_treenode n = { entry = empty_entry (); children = Hashtbl.create n } + +(** Tobias Tebbi wrote some tricky code involving mutation. Rather than + rewriting it in a functional style, we simply freeze the state when we need + to by issuing a deep copy of the profiling data. *) +(** TODO: rewrite me in purely functional style *) +let deepcopy_entry { total; local; ncalls; max_total } = + { total; local; ncalls; max_total } + +let rec deepcopy_treenode { entry; children } = + let children' = Hashtbl.create (Hashtbl.length children) in + let iter key subtree = Hashtbl.add children' key (deepcopy_treenode subtree) in + let () = Hashtbl.iter iter children in + { entry = deepcopy_entry entry; children = children' } + +let stack = + let freeze _ = List.map deepcopy_treenode in + Summary.ref ~freeze [empty_treenode 20] ~name:"LtacProf-stack" + +let on_stack = Hashtbl.create 5 + +let get_node c table = + try Hashtbl.find table c + with Not_found -> + let new_node = empty_treenode 5 in + Hashtbl.add table c new_node; + new_node + +let rec add_node node node' = + add_entry node.entry true node'.entry; + Hashtbl.iter + (fun s node' -> add_node (get_node s node.children) node') + node'.children + +let time () = + let times = Unix.times () in + times.Unix.tms_utime +. times.Unix.tms_stime + +(* +let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) +let msgnl strm = msgnl_with !Pp_control.std_ft strm + +let rec print_treenode indent (tn : treenode) = + msgnl (str (indent^"{ entry = {")); + Feedback.msg_notice (str (indent^"total = ")); + msgnl (str (indent^(string_of_float (tn.entry.total)))); + Feedback.msg_notice (str (indent^"local = ")); + msgnl (str (indent^(string_of_float tn.entry.local))); + Feedback.msg_notice (str (indent^"ncalls = ")); + msgnl (str (indent^(string_of_int tn.entry.ncalls))); + Feedback.msg_notice (str (indent^"max_total = ")); + msgnl (str (indent^(string_of_float tn.entry.max_total))); + msgnl (str (indent^"}")); + msgnl (str (indent^"children = {")); + Hashtbl.iter + (fun s node -> + msgnl (str (indent^" "^s^" |-> ")); + print_treenode (indent^" ") node + ) + tn.children; + msgnl (str (indent^"} }")) + +let rec print_stack (st : treenode list) = match st with +| [] -> msgnl (str "[]") +| x :: xs -> print_treenode "" x; msgnl (str ("::")); print_stack xs +*) + +let string_of_call ck = + let s = + string_of_ppcmds + (match ck with + | Tacexpr.LtacNotationCall s -> Names.KerName.print s + | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst + | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id + | Tacexpr.LtacAtomCall te -> + (Pptactic.pr_glob_tactic (Global.env ()) + (Tacexpr.TacAtom (Loc.ghost, te))) + | Tacexpr.LtacConstrInterp (c, _) -> + pr_glob_constr_env (Global.env ()) c + | Tacexpr.LtacMLCall te -> + (Pptactic.pr_glob_tactic (Global.env ()) + te) + ) in + for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done; + let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in + CString.strip s + +let exit_tactic start_time add_total c = match !stack with +| [] | [_] -> + (* oops, our stack is invalid *) + encounter_multi_success_backtracking () +| node :: (parent :: _ as stack') -> + stack := stack'; + if add_total then Hashtbl.remove on_stack (string_of_call c); + let diff = time () -. start_time in + parent.entry.local <- parent.entry.local -. diff; + let node' = { total = diff; local = diff; ncalls = 1; max_total = diff } in + add_entry node.entry add_total node' + +let tclFINALLY tac (finally : unit Proofview.tactic) = + let open Proofview.Notations in + Proofview.tclIFCATCH + tac + (fun v -> finally <*> Proofview.tclUNIT v) + (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn) + +let do_profile s call_trace tac = + let open Proofview.Notations in + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + if !is_profiling && is_new_call () then + match call_trace with + | (_, c) :: _ -> + let s = string_of_call c in + let parent = List.hd !stack in + let node, add_total = try Hashtbl.find on_stack s, false + with Not_found -> + let node = get_node s parent.children in + Hashtbl.add on_stack s node; + node, true + in + if not add_total && node = List.hd !stack then None else ( + stack := node :: !stack; + let start_time = time () in + Some (start_time, add_total) + ) + | [] -> None + else None)) >>= function + | Some (start_time, add_total) -> + tclFINALLY + tac + (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + (match call_trace with + | (_, c) :: _ -> + exit_tactic start_time add_total c + | [] -> ())))) + | None -> tac + + + +let format_sec x = (Printf.sprintf "%.3fs" x) +let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x)) +let padl n s = ws (max 0 (n - utf8_length s)) ++ str s +let padr n s = str s ++ ws (max 0 (n - utf8_length s)) +let padr_with c n s = + let ulength = utf8_length s in + str (utf8_sub s 0 n) ++ str (String.make (max 0 (n - ulength)) c) + +let rec list_iter_is_last f = function + | [] -> [] + | [x] -> [f true x] + | x :: xs -> f false x :: list_iter_is_last f xs + +let header = + str " tactic self total calls max" ++ + fnl () ++ + str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘" + +let rec print_node all_total indent prefix (s, n) = + let e = n.entry in + h 0 ( + padr_with '-' 40 (prefix ^ s ^ " ") + ++ padl 7 (format_ratio (e.local /. all_total)) + ++ padl 7 (format_ratio (e.total /. all_total)) + ++ padl 8 (string_of_int e.ncalls) + ++ padl 10 (format_sec (e.max_total)) + ) ++ + print_table all_total indent false n.children + +and print_table all_total indent first_level table = + let fold s n l = if n.entry.total /. all_total < 0.02 then l else (s, n) :: l in + let ls = Hashtbl.fold fold table [] in + match ls with + | [s, n] when not first_level -> + print_node all_total indent (indent ^ "└") (s, n) + | _ -> + let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in + let iter is_last = + let sep0 = if first_level then "" else if is_last then " " else " │" in + let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in + print_node all_total (indent ^ sep0) (indent ^ sep1) + in + prlist_with_sep fnl (fun pr -> pr) (list_iter_is_last iter ls) + +let print_results () = + let tree = (List.hd !stack).children in + let all_total = -. (List.hd !stack).entry.local in + let global = Hashtbl.create 20 in + let rec cumulate table = + let iter s node = + let node' = get_node s global in + add_entry node'.entry true node.entry; + cumulate node.children + in + Hashtbl.iter iter table + in + cumulate tree; + warn_encountered_multi_success_backtracking (); + let msg = + h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++ + fnl () ++ + header ++ + print_table all_total "" true global ++ + fnl () ++ + header ++ + print_table all_total "" true tree + in + Feedback.msg_notice msg + (* FOR DEBUGGING *) + (* ; + msgnl (str""); + print_stack (!stack) + *) + +let print_results_tactic tactic = + let tree = (List.hd !stack).children in + let table_tactic = Hashtbl.create 20 in + let rec cumulate table = + let iter s node = + if String.sub (s ^ ".") 0 (min (1 + String.length s) (String.length tactic)) = tactic + then add_node (get_node s table_tactic) node + else cumulate node.children + in + Hashtbl.iter iter table + in + cumulate tree; + let all_total = -. (List.hd !stack).entry.local in + let tactic_total = + Hashtbl.fold + (fun _ node all_total -> node.entry.total +. all_total) + table_tactic 0. in + warn_encountered_multi_success_backtracking (); + let msg = + h 0 (str"total time: " ++ padl 11 (format_sec (all_total))) ++ + h 0 (str"time spent in tactic: " ++ padl 11 (format_sec (tactic_total))) ++ + fnl () ++ + header ++ + print_table tactic_total "" true table_tactic + in + Feedback.msg_notice msg + +let reset_profile () = + stack := [empty_treenode 20]; + encountered_multi_success_backtracking := false + +let do_print_results_at_close () = if get_profiling () then print_results () + +let _ = Declaremods.append_end_library_hook do_print_results_at_close + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "Ltac Profiling"; + optkey = ["Ltac"; "Profiling"]; + optread = get_profiling; + optwrite = set_profiling } |