Commit 1278abbe authored by MARCHE Claude's avatar MARCHE Claude

add stats into the info command of why3session

parent a93bf9ba
......@@ -680,7 +680,8 @@ install_local: bin/why3replayer
###############
SESSION_FILES = why3session_lib why3session_copy why3session_info \
why3session_latex why3session_html why3session_rm why3session
why3session_latex why3session_html why3session_rm \
why3session
SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
......
......@@ -76,53 +76,6 @@ replace by the input file and '%o' which will be replaced by the output file.")
" same as '--add_pp .v \"coqdoc --no-index --html -o %o %i\" .html'") ::
common_options
(*
let version_msg = sprintf
"Why3 html session output, version %s (build date: %s)"
Config.version Config.builddate
let usage_str = sprintf
"Usage: %s [options] [<file.why>|<project directory>] ... "
(Filename.basename Sys.argv.(0))
let set_file f = Queue.push f files
let () = Arg.parse spec set_file usage_str
let () =
if !opt_version then begin
printf "%s@." version_msg;
exit 0
end
*)
(* let () = *)
(* List.iter (fun (in_,(cmd,out)) -> *)
(* printf "in : %s, cmd : %s, out : %s@." in_ cmd out) !opt_pp *)
(*
let () =
Debug.Opt.set_flags_selected ();
if Debug.Opt.option_list () then exit 0
*)
(*
let output_dir =
match !output_dir with
| "" ->
printf "Error: output_dir must be set@.";
exit 1
| "-" when !opt_context ->
printf
"Error: context and stdout output can't be set at the same time@.";
exit 1
| _ -> !output_dir
let edited_dst = Filename.concat output_dir "edited"
let whyconf = Whyconf.read_config !opt_config
*)
open Session
open Util
......
......@@ -17,16 +17,22 @@
(* *)
(**************************************************************************)
(**************************************************************************)
(* Specific source code for computing statistics is a contribution by *)
(* David MENTRE <dmentre@linux-france.org>, 2011 *)
(**************************************************************************)
open Why3
open Why3session_lib
open Whyconf
open Format
module S = Session
open Session
open Util
let opt_print_provers = ref false
let opt_print_edited = ref false
let opt_tree_print = ref false
let opt_stats_print = ref false
let opt_project_dir = ref false
let opt_print0 = ref false
......@@ -35,6 +41,8 @@ let spec =
" the prover used in the session are listed" ) ::
("--edited-files", Arg.Set opt_print_edited,
" the edited files used in the session are listed" ) ::
("--stats", Arg.Set opt_stats_print,
" prints provers statistics" ) ::
("--tree", Arg.Set opt_tree_print,
" the session is pretty printed in an ascii tree format" ) ::
("--dir", Arg.Set opt_project_dir,
......@@ -44,6 +52,168 @@ let spec =
--provers and --edited-files" ) ::
common_options
type proof_stats =
{ mutable no_proof : Sstr.t;
mutable only_one_proof : Sstr.t;
prover_min_time : float Hprover.t;
prover_avg_time : float Hprover.t;
prover_max_time : float Hprover.t;
prover_num_proofs : int Hprover.t;
prover_data : (string) Hprover.t
}
let new_proof_stats () =
{ no_proof = Sstr.empty;
only_one_proof = Sstr.empty;
prover_min_time = Hprover.create 3;
prover_avg_time = Hprover.create 3;
prover_max_time = Hprover.create 3;
prover_num_proofs = Hprover.create 3;
prover_data = Hprover.create 3 }
let apply_f_on_hashtbl_entry ~tbl ~f ~name =
try
let cur_time = Hprover.find tbl name in
Hprover.replace tbl name (f (Some cur_time))
with Not_found ->
Hprover.add tbl name (f None)
let update_min_time tbl (prover, time) =
apply_f_on_hashtbl_entry
~tbl
~f:(function
| Some cur_time -> if time < cur_time then time else cur_time
| None -> time)
~name:prover
let update_max_time tbl (prover, time) =
apply_f_on_hashtbl_entry
~tbl
~f:(function
| Some cur_time -> if time > cur_time then time else cur_time
| None -> time)
~name:prover
let update_avg_time tbl (prover, time) =
apply_f_on_hashtbl_entry
~tbl
~f:(function
| Some cur_time -> cur_time +. time
| None -> time)
~name:prover
let update_count tbl (prover, _time) =
apply_f_on_hashtbl_entry
~tbl
~f:(function
| Some n -> n + 1
| None -> 1)
~name:prover
let update_perf_stats stats prover_and_time =
update_min_time stats.prover_min_time prover_and_time;
update_max_time stats.prover_max_time prover_and_time;
update_avg_time stats.prover_avg_time prover_and_time;
update_count stats.prover_num_proofs prover_and_time
let string_of_prover p = Pp.string_of_wnl print_prover p
let rec stats_of_goal prefix_name stats goal =
let ext_proofs = goal.goal_external_proofs in
let proof_id = prefix_name ^ goal.goal_name.Ident.id_string in
let proof_list =
PHprover.fold
(fun prover proof_attempt acc ->
match proof_attempt.proof_state with
| Done result ->
begin
match result.Call_provers.pr_answer with
| Call_provers.Valid ->
(prover, result.Call_provers.pr_time) :: acc
| _ ->
acc
end
| _ -> acc)
ext_proofs
[] in
let no_transf = PHstr.length goal.goal_transformations = 0 in
begin match proof_list with
| [] when no_transf ->
stats.no_proof <- Sstr.add proof_id stats.no_proof
| [ (prover, time) ] when no_transf ->
stats.only_one_proof <-
Sstr.add
(proof_id ^ " : " ^ (string_of_prover prover))
stats.only_one_proof;
update_perf_stats stats (prover, time)
| _ ->
List.iter (update_perf_stats stats) proof_list end;
PHstr.iter (stats_of_transf prefix_name stats) goal.goal_transformations
and stats_of_transf prefix_name stats _ transf =
let prefix_name = prefix_name ^ transf.transf_name ^ " / " in
List.iter (stats_of_goal prefix_name stats) transf.transf_goals
let stats_of_theory file stats theory =
let goals = theory.theory_goals in
let prefix_name = file.file_name ^ " / " ^ theory.theory_name.Ident.id_string
^ " / " in
List.iter (stats_of_goal prefix_name stats) goals
let stats_of_file stats _ file =
let theories = file.file_theories in
List.iter (stats_of_theory file stats) theories
let fill_prover_data stats session =
Sprover.iter
(fun prover ->
Hprover.add stats.prover_data prover
(prover.prover_name ^ " " ^ prover.prover_version))
(get_used_provers session)
let finalize_stats stats =
Hprover.iter
(fun prover time ->
let n = Hprover.find stats.prover_num_proofs prover in
Hprover.replace stats.prover_avg_time prover
(time /. (float_of_int n)))
stats.prover_avg_time
let print_stats stats =
printf "== Goals not proved ==@\n @[";
Sstr.iter (fun s -> printf "%s@\n" s) stats.no_proof;
printf "@]@\n";
printf "== Goals proved by only one prover ==@\n @[";
Sstr.iter (fun s -> printf "%s@\n" s) stats.only_one_proof;
printf "@]@\n";
printf "== Number of proofs per prover ==@\n @[";
Hprover.iter (fun prover n -> printf "%-10s: %d@\n"
(string_of_prover prover) n)
stats.prover_num_proofs;
printf "@]@\n";
printf "== Minimum time per prover ==@\n @[";
Hprover.iter (fun prover time -> printf "%-10s : %.3f s@\n"
(string_of_prover prover) time)
stats.prover_min_time;
printf "@]@\n";
printf "== Maximum time per prover ==@\n @[";
Hprover.iter (fun prover time -> printf "%-10s : %.3f s@\n"
(string_of_prover prover) time)
stats.prover_max_time;
printf "@]@\n";
printf "== Average time per prover ==@\n @[";
Hprover.iter (fun prover time -> printf "%-10s : %.3f s@\n"
(string_of_prover prover) time)
stats.prover_avg_time;
printf "@]@\n"
let run_one fname =
let project_dir = Session.get_project_dir fname in
if !opt_project_dir then printf "%s@." project_dir;
......@@ -52,15 +222,24 @@ let run_one fname =
if !opt_print_provers then
printf "%a@."
(Pp.print_iter1 Sprover.iter sep print_prover)
(S.get_used_provers session);
(get_used_provers session);
if !opt_print_edited then
S.session_iter_proof_attempt
session_iter_proof_attempt
(fun pr ->
Util.option_iter (fun s -> printf "%s%a" s sep ())
(S.get_edited_as_abs session pr))
(get_edited_as_abs session pr))
session;
if !opt_tree_print then
printf "%a@." S.print_session session
printf "%a@." print_session session;
if !opt_stats_print then
begin
let stats = new_proof_stats () in
fill_prover_data stats session;
PHstr.iter (stats_of_file stats) session.session_files;
finalize_stats stats;
print_stats stats
end
let run () =
let _,_,should_exit1 = read_env_spec () in
......@@ -74,3 +253,10 @@ let cmd =
cmd_name = "info";
cmd_run = run;
}
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3session.byte"
End:
*)
(**************************************************************************)
(* *)
(* copyright 2011 David MENTRE <dmentre@linux-france.org> *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Format
open Why3
open Util
module C = Whyconf
open Session
let includes = ref []
let files = Queue.create ()
let opt_version = ref false
let opt_stats = ref true
let opt_config = ref None
let allow_obsolete = ref true
let spec = Arg.align [
("-I",
Arg.String (fun s -> includes := s :: !includes),
"<s> add s to loadpath") ;
"-C", Arg.String (fun s -> opt_config := Some s),
"<file> Read configuration from <file>";
"--config", Arg.String (fun s -> opt_config := Some s),
" Same as -C";
("--strict",
Arg.Clear allow_obsolete,
" Forbid obsolete session");
("-v",
Arg.Set opt_version,
" print version information") ;
Debug.Opt.desc_debug_list;
Debug.Opt.desc_debug_all;
Debug.Opt.desc_debug;
]
let version_msg = Format.sprintf "Why3 statistics, version 0.1"
let usage_str = Format.sprintf
"Usage: %s [options] [<file.why>|<project directory>]"
(Filename.basename Sys.argv.(0))
let set_file f = Queue.add f files
let () = Arg.parse spec set_file usage_str
let () =
if !opt_version then begin
Format.printf "%s@." version_msg;
exit 0
end
let allow_obsolete = !allow_obsolete
let () =
Debug.Opt.set_flags_selected ();
if Debug.Opt.option_list () then exit 0
let string_of_prover p = Pp.string_of_wnl C.print_prover p
type proof_stats =
{ mutable no_proof : Sstr.t;
mutable only_one_proof : Sstr.t;
prover_min_time : float C.Hprover.t;
prover_avg_time : float C.Hprover.t;
prover_max_time : float C.Hprover.t;
prover_num_proofs : int C.Hprover.t;
prover_data : (string) C.Hprover.t
}
let new_proof_stats () =
{ no_proof = Sstr.empty;
only_one_proof = Sstr.empty;
prover_min_time = C.Hprover.create 3;
prover_avg_time = C.Hprover.create 3;
prover_max_time = C.Hprover.create 3;
prover_num_proofs = C.Hprover.create 3;
prover_data = C.Hprover.create 3 }
let apply_f_on_hashtbl_entry ~tbl ~f ~name =
try
let cur_time = C.Hprover.find tbl name in
C.Hprover.replace tbl name (f (Some cur_time))
with Not_found ->
C.Hprover.add tbl name (f None)
let update_min_time tbl (prover, time) =
apply_f_on_hashtbl_entry
~tbl
~f:(function
| Some cur_time -> if time < cur_time then time else cur_time
| None -> time)
~name:prover
let update_max_time tbl (prover, time) =
apply_f_on_hashtbl_entry
~tbl
~f:(function
| Some cur_time -> if time > cur_time then time else cur_time
| None -> time)
~name:prover
let update_avg_time tbl (prover, time) =
apply_f_on_hashtbl_entry
~tbl
~f:(function
| Some cur_time -> cur_time +. time
| None -> time)
~name:prover
let update_count tbl (prover, _time) =
apply_f_on_hashtbl_entry
~tbl
~f:(function
| Some n -> n + 1
| None -> 1)
~name:prover
let update_perf_stats stats prover_and_time =
update_min_time stats.prover_min_time prover_and_time;
update_max_time stats.prover_max_time prover_and_time;
update_avg_time stats.prover_avg_time prover_and_time;
update_count stats.prover_num_proofs prover_and_time
let rec stats_of_goal prefix_name stats goal =
let ext_proofs = goal.goal_external_proofs in
let proof_id = prefix_name ^ goal.goal_name.Ident.id_string in
let proof_list =
PHprover.fold
(fun prover proof_attempt acc ->
match proof_attempt.proof_state with
| Done result ->
begin
match result.Call_provers.pr_answer with
| Call_provers.Valid ->
(prover, result.Call_provers.pr_time) :: acc
| _ ->
acc
end
| _ -> acc)
ext_proofs
[] in
let no_transf = PHstr.length goal.goal_transformations = 0 in
begin match proof_list with
| [] when no_transf ->
stats.no_proof <- Sstr.add proof_id stats.no_proof
| [ (prover, time) ] when no_transf ->
stats.only_one_proof <-
Sstr.add
(proof_id ^ " : " ^ (string_of_prover prover))
stats.only_one_proof;
update_perf_stats stats (prover, time)
| _ ->
List.iter (update_perf_stats stats) proof_list end;
PHstr.iter (stats_of_transf prefix_name stats) goal.goal_transformations
and stats_of_transf prefix_name stats _ transf =
let prefix_name = prefix_name ^ transf.transf_name ^ " / " in
List.iter (stats_of_goal prefix_name stats) transf.transf_goals
let stats_of_theory file stats theory =
let goals = theory.theory_goals in
let prefix_name = file.file_name ^ " / " ^ theory.theory_name.Ident.id_string
^ " / " in
List.iter (stats_of_goal prefix_name stats) goals
let stats_of_file stats _ file =
let theories = file.file_theories in
List.iter (stats_of_theory file stats) theories
let fill_prover_data stats session =
C.Sprover.iter
(fun prover ->
C.Hprover.add stats.prover_data prover
(prover.C.prover_name ^ " " ^ prover.C.prover_version))
(get_used_provers session)
let extract_stats_from_file stats fname =
let project_dir = get_project_dir fname in
try
let session = read_session project_dir in
fill_prover_data stats session;
PHstr.iter (stats_of_file stats) session.session_files
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "Error while opening session with database '%s' : %a@." project_dir
Exn_printer.exn_printer e;
eprintf "Aborting...@.";
exit 1
let finalize_stats stats =
C.Hprover.iter
(fun prover time ->
let n = C.Hprover.find stats.prover_num_proofs prover in
C.Hprover.replace stats.prover_avg_time prover
(time /. (float_of_int n)))
stats.prover_avg_time
let print_stats stats =
printf "== Provers available ==@\n @[";
C.Hprover.iter (fun prover data -> printf "%-10s: %s@\n"
(string_of_prover prover) data)
stats.prover_data;
printf "@]@\n";
printf "== Goals not proved ==@\n @[";
Sstr.iter (fun s -> printf "%s@\n" s) stats.no_proof;
printf "@]@\n";
printf "== Goals proved by only one prover ==@\n @[";
Sstr.iter (fun s -> printf "%s@\n" s) stats.only_one_proof;
printf "@]@\n";
printf "== Number of proofs per prover ==@\n @[";
C.Hprover.iter (fun prover n -> printf "%-10s: %d@\n"
(string_of_prover prover) n)
stats.prover_num_proofs;
printf "@]@\n";
printf "== Minimum time per prover ==@\n @[";
C.Hprover.iter (fun prover time -> printf "%-10s : %.3f s@\n"
(string_of_prover prover) time)
stats.prover_min_time;
printf "@]@\n";
printf "== Maximum time per prover ==@\n @[";
C.Hprover.iter (fun prover time -> printf "%-10s : %.3f s@\n"
(string_of_prover prover) time)
stats.prover_max_time;
printf "@]@\n";
printf "== Average time per prover ==@\n @[";
C.Hprover.iter (fun prover time -> printf "%-10s : %.3f s@\n"
(string_of_prover prover) time)
stats.prover_avg_time;
printf "@]@\n"
let () =
Queue.iter (fun fname ->
let stats = new_proof_stats () in
let _ = extract_stats_from_file stats fname in
finalize_stats stats;
print_stats stats) files
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment