Added a few features in bench_stats

This commit is contained in:
Guillaume Bury 2014-11-17 17:07:40 +01:00
parent b992794a77
commit 5bcb8ae99f
4 changed files with 28 additions and 14 deletions

View file

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

View file

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

View file

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

View file

@ -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; }