From 5bcb8ae99f59454e406197bfe196a37c38409895 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 17 Nov 2014 17:07:40 +0100 Subject: [PATCH] Added a few features in bench_stats --- Makefile | 4 ++-- util/bench_stats.ml | 19 +++++++++++++------ util/parselog.ml | 16 +++++++++++----- util/parselog.mli | 3 ++- 4 files changed, 28 insertions(+), 14 deletions(-) diff --git a/Makefile b/Makefile index ab950931..61a1a203 100644 --- a/Makefile +++ b/Makefile @@ -28,8 +28,8 @@ $(TEST): $(LIB) bench: $(TEST) cd bench && $(MAKE) -stats: $(TEST) - ./bench_stats.native `git rev-parse HEAD` +stats: + ./bench_stats.native log: cat _build/$(LOG) || true diff --git a/util/bench_stats.ml b/util/bench_stats.ml index 6d10db05..632235e2 100644 --- a/util/bench_stats.ml +++ b/util/bench_stats.ml @@ -8,13 +8,16 @@ exception Commit_not_found exception Commit_ambiguous (* Arguments parsing *) -let usage = "Usage : ./bench_stats [options] commit1 [commit2]" +let usage = "Usage : ./bench_stats [options] [commit1 [commit2]]" let arg_commit = ref [] let anon s = arg_commit := s :: !arg_commit +let info_commit = ref false let long_diff = ref false let args = Arg.align [ + "-info", Arg.Set info_commit, + " Adds info on the commit when printing stats"; "-long", Arg.Set long_diff, " Print a long diff instead of a short one"; ] @@ -114,8 +117,8 @@ let diff h h' = let print_stats s = let sha, h = get_commit s in let st = get_stats h in - Format.printf "Average time : %f (%d / %d)@\nTimeouts : %d@\nSpaceouts : %d@." - st.avg_time (st.nb_sat + st.nb_unsat) + Format.printf "%s@\nAverage time : %f (%d / %d)@\nTimeouts : %d@\nSpaceouts : %d@." + (if !info_commit then Parselog.commit_info sha else sha) st.avg_time (st.nb_sat + st.nb_unsat) (st.nb_sat + st.nb_unsat + st.nb_timeout + st.nb_spaceout) st.nb_timeout st.nb_spaceout let print_diff_short s1 s2 = @@ -135,16 +138,20 @@ let print_diff_short s1 s2 = (* Main function *) let main () = Arg.parse args anon usage; - (* Warning : the 'anon' function reverses the order of the arguments *) - match !arg_commit with + match List.rev (!arg_commit) with + | [] -> print_stats (Parselog.last_commit ()) | [c] -> print_stats c - | [c1; c2] -> print_diff_short c2 c1 + | [c1; c2] -> print_diff_short c1 c2 | _ -> Arg.usage args usage ;; try main () with +| Parselog.Unknown_status (f, l) -> + Format.printf "For file '%s' : unknown return string :@\n" f; + List.iter (fun s -> Format.printf "%s@." s) l; + exit 3 | Commit_not_found -> Format.printf "No such commit found@."; exit 2 diff --git a/util/parselog.ml b/util/parselog.ml index 1762021c..03480e44 100644 --- a/util/parselog.ml +++ b/util/parselog.ml @@ -45,9 +45,15 @@ let commit_info sha = ignore (Unix.close_process_in ch); String.concat "\n" (List.rev l) +let last_commit () = + let ch = Unix.open_process_in "git rev-parse HEAD" in + let s = input_line ch in + ignore (Unix.close_process_in ch); + s + (* Raw log file parsing *) exception Empty_raw of string -exception Unknown_status of string list +exception Unknown_status of string * string list type status = | Sat @@ -61,12 +67,12 @@ type pb = { pb_time : float; } -let status_of_lines = function +let status_of_lines f = function | ["Sat"] -> Sat | ["Unsat"] -> Unsat | ["Time limit exceeded"; _] -> Timeout | ["Size limit exceeded"; _] -> Spaceout - | l -> raise (Unknown_status l) + | l -> raise (Unknown_status (f, l)) let parse_raw f = let f_in = open_in f in @@ -82,12 +88,12 @@ let parse_raw f = match !f_lines with | [] -> raise (Empty_raw f) | s :: r -> - let st = status_of_lines (List.rev r) in + let st = status_of_lines f (List.rev r) in { pb_name = f; pb_st = st; pb_time = float_of_string s } let parse_commit root = let l = list_dir_files_rec (Filename.concat root "raw") in let res = Hashtbl.create (List.length l) in - List.iter (fun f -> Hashtbl.add res f (parse_raw f)) l; + List.iter (fun f -> try Hashtbl.add res f (parse_raw f) with Empty_raw _ -> ()) l; res diff --git a/util/parselog.mli b/util/parselog.mli index 7088ce52..50c70fbf 100644 --- a/util/parselog.mli +++ b/util/parselog.mli @@ -5,10 +5,11 @@ Copyright 2014 Simon Cruanes *) exception Empty_raw of string -exception Unknown_status of string list +exception Unknown_status of string * string list val complete : string -> string -> string list val commit_info : string -> string +val last_commit : unit -> string type status = Sat | Unsat | Timeout | Spaceout type pb = { pb_name : string; pb_st : status; pb_time : float; }