Commit 2f4c41f1 authored by François Bobot's avatar François Bobot

why3session add csv output that can also be used for gnuplot

parent b94526e7
......@@ -611,7 +611,8 @@ install_local: bin/why3replayer
SESSION_FILES = why3session_lib why3session_copy why3session_info \
why3session_latex why3session_html why3session_rm \
why3session_output why3session_run why3session
why3session_output why3session_run why3session_csv \
why3session
SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
......
......@@ -522,6 +522,12 @@ let mk_filter_prover ?version ?altern name =
filter_altern = Opt.map mk_regexp altern;
}
let filter_from_prover pr =
{ filter_name = mk_regexp pr.prover_name ;
filter_version = Some (mk_regexp pr.prover_version);
filter_altern = Some (mk_regexp pr.prover_altern);
}
let print_filter_prover fmt fp =
match fp.filter_version, fp.filter_altern with
| None , None -> fprintf fmt "%s" fp.filter_name.desc
......@@ -549,19 +555,18 @@ let filter_prover fp p =
&& Opt.fold (fun _ -> check p.prover_version) true fp.filter_version
&& Opt.fold (fun _ -> check p.prover_altern) true fp.filter_altern
let filter_provers whyconf fp =
try
if fp.filter_version = None && fp.filter_altern = None then
let filter_prover_with_shortcut whyconf fp =
if fp.filter_version = None && fp.filter_altern = None then
try
let prover = (Mstr.find fp.filter_name.desc whyconf.prover_shortcuts) in
try
let prover_config = Mprover.find prover whyconf.provers in
Mprover.singleton prover prover_config
with Not_found ->
(** shortcut send to nothing *)
Mprover.empty
else raise Not_found
with Not_found ->
Mprover.filter (fun p _ -> filter_prover fp p) whyconf.provers
filter_from_prover prover
with Not_found -> fp
else fp
let filter_provers whyconf fp =
let fp = filter_prover_with_shortcut whyconf fp in
Mprover.filter (fun p _ -> filter_prover fp p) whyconf.provers
let filter_one_prover whyconf fp =
let provers = filter_provers whyconf fp in
......@@ -572,6 +577,7 @@ let filter_one_prover whyconf fp =
else
raise (ProverAmbiguity (whyconf,fp,provers))
(** merge config *)
let merge_config config filename =
......
......@@ -197,11 +197,14 @@ val parse_filter_prover : string -> filter_prover
regexp must start with ^. Partial match will be used.
*)
val filter_prover_with_shortcut : config -> filter_prover -> filter_prover
(** resolve prover shortcut in filter *)
val filter_prover : filter_prover -> prover -> bool
(** test if the prover match the filter prover *)
val filter_provers : config -> filter_prover -> config_prover Mprover.t
(** test if the prover match the filter prover *)
(** Get all the provers that match this filter *)
exception ProverNotFound of config * filter_prover
exception ProverAmbiguity of config * filter_prover * config_prover Mprover.t
......
......@@ -96,13 +96,17 @@ let rparen fmt () = fprintf fmt ")"
let lchevron fmt () = fprintf fmt "<"
let rchevron fmt () = fprintf fmt ">"
let nothing _fmt _ = ()
let string fmt s = fprintf fmt "%s" s
let string = pp_print_string
let float = pp_print_float
let int = pp_print_int
let constant_string s fmt () = string fmt s
let formatted fmt x = Format.fprintf fmt "%( %)" x
let constant_formatted f fmt () = formatted fmt f
let print0 fmt () = pp_print_string fmt "\000"
let add_flush sep fmt x = sep fmt x; pp_print_flush fmt ()
let asd f fmt x = fprintf fmt "\"%a\"" f x
let print_pair pr1 = print_pair_delim lparen comma rparen pr1
let hov n f fmt x = pp_open_hovbox fmt n; f fmt x; pp_close_box fmt ()
......
......@@ -98,6 +98,8 @@ val lchevron : formatter -> unit -> unit
val rchevron : formatter -> unit -> unit
val nothing : formatter -> 'a -> unit
val string : formatter -> string -> unit
val float : formatter -> float -> unit
val int : formatter -> int -> unit
val constant_string : string -> formatter -> unit -> unit
val formatted : formatter -> formatted -> unit
val constant_formatted : formatted -> formatter -> unit -> unit
......@@ -108,6 +110,9 @@ val indent : int -> (formatter -> 'a -> unit) -> formatter -> 'a -> unit
val add_flush : (formatter -> 'a -> unit) -> formatter -> 'a -> unit
val asd : (formatter -> 'a -> unit) -> (formatter -> 'a -> unit)
(** add string delimiter " " *)
val open_formatter : ?margin:int -> out_channel -> formatter
val close_formatter : formatter -> unit
val open_file_and_formatter : ?margin:int -> string -> out_channel * formatter
......
......@@ -16,9 +16,9 @@ module XHashtbl = Exthtbl.Hashtbl
module Int = struct
type t = int
let compare = Pervasives.compare
let equal x y = x = y
let hash x = x
let compare (x : int) y = Pervasives.compare x y
let equal (x : int) y = x = y
let hash (x : int) = x
end
module Mint = Map.Make(Int)
......@@ -34,6 +34,19 @@ module Hstr = XHashtbl.Make
let equal = ((=) : string -> string -> bool)
end)
module Float = struct
type t = float
let compare (x : float) y = Pervasives.compare x y
let equal (x : float) y = x = y
let hash (x : float) = XHashtbl.hash x
end
module Mfloat = Map.Make(Float)
module Sfloat = Mfloat.Set
module Hfloat = XHashtbl.Make(Float)
(* Set, Map, Hashtbl on structures with a unique tag *)
module type TaggedType =
......
......@@ -22,6 +22,10 @@ module Mstr : Map.S with type key = string
module Sstr : Mstr.Set
module Hstr : XHashtbl.S with type key = string
module Mfloat : Map.S with type key = float
module Sfloat : Mfloat.Set
module Hfloat : XHashtbl.S with type key = float
(* Set, Map, Hashtbl on structures with a unique tag *)
module type TaggedType =
......
......@@ -18,6 +18,7 @@ let cmds =
Why3session_info.cmd;
Why3session_latex.cmd;
Why3session_html.cmd;
Why3session_csv.cmd;
Why3session_copy.cmd_mod;
Why3session_copy.cmd_copy;
Why3session_copy.cmd_archive;
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2012 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open Why3
open Why3session_lib
open Format
module Hprover = Whyconf.Hprover
module S = Session
let opt_output_dir = ref ""
let opt_provers = ref []
let opt_aggregate = ref false
let simple_read_opt_prover s =
try
Whyconf.parse_filter_prover s
with Whyconf.ParseFilterProver _ ->
raise (Arg.Bad
"--filter-prover name[,version[,alternative]|,,alternative] \
regexp must start with ^")
let opt_value_not_valid = ref "-1."
let opt_gnuplot = false
type style =
| Normal
| By_Time
let opt_style = ref Normal
let set_style s =
match s with
| "normal" -> opt_style := Normal
| "by_time" -> opt_style := By_Time
| _ -> assert false
(* TODO *)
let print_gnuplot =
"set datafile separator \",\"
set key autotitle columnhead
set term png
set logscale xy 10
set object rectangle from screen 0,0 to screen 1,1 behind
set output \"%s\"
set xlabel \"%a\"
max(x,y) = x > y ? x : y
plot \"aggregate.csv\" using (max($4,0.001)):(max($3,0.001))
"
let spec =
("-o",
Arg.Set_string opt_output_dir,
"<dir> where to produce LaTeX files (default: session dir)") ::
("--filter-prover",
Arg.String (fun s ->
opt_provers := (simple_read_opt_prover s)::!opt_provers),
" select the provers")::
("--aggregate", Arg.Set opt_aggregate,
" aggregate all the input into one")::
("--value-not-valid", Arg.Set_string opt_value_not_valid,
" value used when the external proof is not valid")::
("--style", Arg.Symbol (["normal";"by_time"],set_style)," set the style")
:: (common_options)
(** Normal *)
let print_cell fmt pa =
match pa.Session.proof_state with
| Session.Done {Call_provers.pr_answer = Call_provers.Valid;
pr_time = time} -> fprintf fmt "%f" time
| _ -> fprintf fmt "%s" !opt_value_not_valid
let rec print_line fmt provers a =
begin match a with
| Session.Goal a ->
fprintf fmt "\"%s\"" a.Session.goal_name.Ident.id_string;
Whyconf.Sprover.iter (fun p ->
try
let pa = Session.PHprover.find a.Session.goal_external_proofs p in
fprintf fmt ",%a" print_cell pa
with Not_found ->
fprintf fmt ",") provers;
fprintf fmt "\n@?" (** no @\n since we use Pp.wnl *)
| _ -> () end;
Session.iter (print_line fmt provers) a
let run_one_normal filter_provers fmt fname =
let project_dir = Session.get_project_dir fname in
let session = Session.read_session project_dir in
let provers = Session.get_used_provers session in
let provers =
match filter_provers with
| [] -> provers
| _ ->
Whyconf.Sprover.filter
(fun p ->
List.exists
(fun f -> Whyconf.filter_prover f p) filter_provers) provers in
fprintf fmt ",%a\n@?"
(Pp.print_iter1 Whyconf.Sprover.iter Pp.comma (Pp.asd Whyconf.print_prover))
provers;
Session.session_iter (print_line fmt provers) session
let run_normal dir filter_provers =
if !opt_aggregate then
let out = open_out (Filename.concat dir "aggregate.csv") in
let fmt = formatter_of_out_channel out in
Pp.wnl fmt;
iter_files (run_one_normal filter_provers fmt);
close_out out
else
iter_files (fun fname ->
let out = open_out
(Filename.concat dir
((try Filename.chop_extension fname with _ -> fname)^".csv")) in
let fmt = formatter_of_out_channel out in
Pp.wnl fmt;
run_one_normal filter_provers fmt fname;
close_out out)
(** By time *)
let print_float_list =
Pp.print_list_delim ~start:Pp.lsquare ~stop:Pp.rsquare ~sep:Pp.semi Pp.float
let rec grab_valid_time provers_time provers pa =
let prover = pa.Session.proof_prover in
if Whyconf.Sprover.mem prover provers then
match pa.Session.proof_state with
| Session.Done {Call_provers.pr_answer = Call_provers.Valid;
pr_time = time} ->
let l = Whyconf.Hprover.find_def provers_time [] prover in
Whyconf.Hprover.replace provers_time prover (time::l)
| _ -> ()
let run_one_by_time provers_time filter_provers fname =
let project_dir = Session.get_project_dir fname in
let session = Session.read_session project_dir in
let provers = Session.get_used_provers session in
let provers =
match filter_provers with
| [] -> provers
| _ ->
Whyconf.Sprover.filter
(fun p ->
List.exists
(fun f -> Whyconf.filter_prover f p) filter_provers) provers in
Session.session_iter_proof_attempt
(grab_valid_time provers_time provers) session
let print_provers_time (provers_time : float list Whyconf.Hprover.t) fmt =
let provers_time =
Whyconf.Hprover.fold (fun p e acc -> Whyconf.Mprover.add p e acc)
provers_time Whyconf.Mprover.empty in
fprintf fmt ",%a\n@?"
(Pp.print_iter2 Whyconf.Mprover.iter Pp.comma Pp.nothing
(Pp.asd Whyconf.print_prover) Pp.nothing)
provers_time;
let l = Whyconf.Mprover.values provers_time in
let l = List.map (fun l ->
let sorted = List.fast_sort Pervasives.compare l in
(ref sorted,ref 0)) l in
let rec print_line (l : (float list ref * int ref) list) =
(** get the minimum *)
let lmin = List.fold_left (fun acc (e,_) ->
match !e with
| [] -> acc
| a::_ -> min a acc) max_float l in
if lmin = max_float then () (** finished *)
else begin
(** remove the minimum and increase the number of proved *)
let rec remove nb = function
| [] -> []
| a::e when a = lmin -> incr nb; remove nb e
| e -> e in
List.iter (fun (e,nb) -> e:=remove nb !e) l;
(** Print the current number of proved *)
fprintf fmt "%f,%a\n@?" lmin
(Pp.print_list Pp.comma (fun fmt (_,nb) -> pp_print_int fmt (!nb)))
l;
print_line l end in
print_line l
let run_by_time dir filter_provers =
if !opt_aggregate then
let out = open_out (Filename.concat dir "aggregate.csv") in
let fmt = formatter_of_out_channel out in
Pp.wnl fmt;
let provers_time = Whyconf.Hprover.create 5 in
iter_files (run_one_by_time provers_time filter_provers);
print_provers_time provers_time fmt;
close_out out
else
iter_files (fun fname ->
let out = open_out
(Filename.concat dir
((try Filename.chop_extension fname with _ -> fname)^".csv")) in
let fmt = formatter_of_out_channel out in
Pp.wnl fmt;
let provers_time = Whyconf.Hprover.create 5 in
run_one_by_time provers_time filter_provers fname;
print_provers_time provers_time fmt;
close_out out)
(* Common *)
let run () =
let _,whyconf,should_exit1 = read_env_spec () in
if should_exit1 then exit 1;
let filter_provers =
List.map (Whyconf.filter_prover_with_shortcut whyconf) !opt_provers in
let dir = !opt_output_dir in
match !opt_style with
| Normal -> run_normal dir filter_provers
| By_Time -> run_by_time dir filter_provers
let cmd =
{ cmd_spec = spec;
cmd_desc = "output session as a table for simple processing.";
cmd_name = "csv";
cmd_run = run;
}
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