why3session_csv.ml 12 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
10 11 12 13 14 15 16 17 18
(********************************************************************)

open Why3
open Why3session_lib
open Format

module Hprover = Whyconf.Hprover
module S = Session

19 20 21
let orig_dir = Sys.getcwd ()

let opt_output_dir = ref "./"
22 23 24

let opt_provers = ref []
let opt_aggregate = ref false
25
let opt_print_csv = ref false
26 27 28 29 30 31 32 33 34 35 36

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."
37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
type gnuplot =
  | PDF
  | PNG
  | SVG
  | QT
  | GP

let opt_gnuplot = ref []
let select_gnuplot = function
  | "pdf" -> opt_gnuplot := PDF::!opt_gnuplot
  | "png" -> opt_gnuplot := PNG::!opt_gnuplot
  | "svg" -> opt_gnuplot := SVG::!opt_gnuplot
  | "qt"  -> opt_gnuplot := QT::!opt_gnuplot
  | "gp" -> opt_gnuplot := GP::!opt_gnuplot
  | _ -> assert false (** absurd: Arg already filtered bad cases *)

53 54 55 56 57 58 59 60 61 62 63 64
type gnuplot_x =
  | Xtime
  | Xgoals

let opt_gnuplot_x = ref Xtime

let select_gnuplot_x = function
  | "time" -> opt_gnuplot_x := Xtime
  | "goals" -> opt_gnuplot_x := Xgoals
  | _ -> assert false (** absurd: Arg already filtered bad cases *)


65 66
let opt_data = ref false
let opt_by_time = ref false
67 68 69 70

let spec =
  ("-o",
   Arg.Set_string opt_output_dir,
71
   "<dir> where to produce files (default: session dir)") ::
72 73 74 75
  ("--filter-prover",
   Arg.String (fun s ->
     opt_provers := (simple_read_opt_prover s)::!opt_provers),
   " select the provers")::
76
    ("--data", Arg.Set opt_data,
77
     " for all the goals give the time taken by each provers that proved it")::
78
    ("--aggregate", Arg.Set opt_aggregate,
79 80
     " aggregate all the input into one file named \
       aggregate_data.* and aggregate.*")::
81
    ("--value-not-valid", Arg.Set_string opt_value_not_valid,
82 83
     " value used when the external proof is not valid (only for --data)")::
    ("--valid_by_time", Arg.Set opt_by_time,
84
     " give the evolution of the number of goal proved \
85 86
      for each provers (default)")::
    ("--gnuplot", Arg.Symbol (["pdf";"png";"svg";"qt";"gp"],select_gnuplot),
87
     " run gnuplot on the produced file (currently only with --valid_by_time)\
88
      (gp write the gnuplot script used for generating the other case)")::
89
    ("--gnuplot-x", Arg.Symbol (["time";"goals"],select_gnuplot_x),
90
     " select the data used for the x axes time or number of goal proved \
91
      (default time)")::
92
    ("--output-csv", Arg.Set opt_print_csv,
93
     " print the csv, set by default when --gnuplot is not set")::
94
    common_options
95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113

(** 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;
114
    fprintf fmt "\n@?" (* no @\n since we use Pp.wnl *)
115 116 117 118 119
  | _ -> () 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
120
  let session,_use_shapes = Session.read_session project_dir in
121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137
  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
138
    let out = open_out (Filename.concat dir "aggregate_data.csv") in
139 140 141 142 143 144 145 146
    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
147
           ((try Filename.chop_extension fname with _ -> fname)^"_data.csv")) in
148 149 150 151 152 153 154 155 156 157 158
      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

159
let grab_valid_time provers_time provers pa =
160 161 162 163 164 165 166 167 168 169 170
  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
171
  let session,_use_shapes = Session.read_session project_dir in
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197
  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) =
198
    (* get the minimum *)
199 200 201 202
    let lmin = List.fold_left (fun acc (e,_) ->
      match !e with
      | [] -> acc
      | a::_ -> min a acc) max_float l in
203
    if lmin = max_float then () (* finished *)
204
    else begin
205
      (* remove the minimum and increase the number of proved *)
206 207 208 209 210
      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;
211
      (* Print the current number of proved *)
212 213 214 215 216 217
      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

218
let create_gnuplot_by_time nb_provers fmt =
219 220 221
  let timeaxe, goalsaxe =
    match !opt_gnuplot_x with | Xtime -> "x","y" | Xgoals -> "y","x"
  in
222 223 224 225 226
  Format.pp_print_string fmt
"\
set datafile separator \",\"\n\
set key autotitle columnhead\n\
set object rectangle from screen 0,0 to screen 1,1 behind\n\
227 228 229 230 231
set key rmargin width -4 samplen 2\n";
  Format.fprintf fmt "set logscale %s 10\n" timeaxe;
  Format.fprintf fmt "set %slabel \"time(s)\"\n" timeaxe;
  Format.fprintf fmt "set %slabel \"number of solved goals\"\n\n" goalsaxe;
  Format.pp_print_string fmt "plot \\\n";
232
  for i=1 to nb_provers do
233 234 235 236 237 238 239 240 241 242
    begin match !opt_gnuplot_x with
    | Xtime ->
      Format.fprintf fmt
        "data_filename using ($1):($%i) with steps title columnhead(%i)"
        (i+1) (i+1)
    | Xgoals ->
      Format.fprintf fmt
        "data_filename using ($%i):($1) with fsteps title columnhead(%i)"
        (i+1) (i+1)
    end;
243 244 245 246
    if i <> nb_provers then Format.pp_print_string fmt ",\\\n";
  done

let print_file out f : unit =
247 248
    let fmt = formatter_of_out_channel out in
    Pp.wnl fmt;
249
    f fmt;
250
    close_out out
251 252 253

let print_args fmt args =
  (Pp.print_iter1 Array.iter
254
     (fun fmt () -> Format.pp_print_string fmt " ") (* no @\n *)
255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273
     (fun fmt -> Format.fprintf fmt "%S"))
   fmt args

let call_gnuplot arg1 arg2 csv_file gp_file =
  let args =
    [| "gnuplot"; "-e"; arg1; "-e"; arg2;
       "-e"; Printf.sprintf "data_filename = \"%s\"" (Opt.get csv_file);
       Opt.get gp_file |] in
  Debug.dprintf verbose "exec:%a@." print_args args;
  let pid = Unix.create_process "gnuplot" args
      Unix.stdin Unix.stdout Unix.stderr  in
  match Unix.waitpid [] pid with
  | _, Unix.WEXITED 0 -> ()
  | _ -> Format.eprintf "Command failed:%a@." print_args args


let run_by_time_gen dir canonical_name iter =
  let to_remove = Stack.create () in
  let canonical_name = Filename.concat dir canonical_name in
274
  (* compute stats *)
275 276
  let provers_time = Whyconf.Hprover.create 5 in
  iter provers_time;
277
  (* print .csv if necessary *)
278 279 280 281 282 283 284 285 286 287 288 289 290 291 292
  let csv_file =
     if !opt_gnuplot = [] || !opt_print_csv then
       let fname = canonical_name ^ ".csv" in
       print_file (open_out fname)
         (fun fmt -> print_provers_time provers_time fmt);
       Some fname
     else if !opt_gnuplot <> [] then
       let fname,ch = Filename.open_temp_file "why3session" ".csv" in
       Stack.push fname to_remove;
       print_file ch
         (fun fmt -> print_provers_time provers_time fmt);
       Some fname
     else None
  in

293
  (* create .gp if necessary *)
294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309
  let nb_provers = Whyconf.Hprover.length provers_time in
  let gp_file =
    if List.mem GP !opt_gnuplot
    then let fname = canonical_name ^ ".gp" in
      print_file (open_out fname)
        (fun fmt -> create_gnuplot_by_time nb_provers fmt);
      Some fname
    else if !opt_gnuplot <> [] then
      let fname,ch = Filename.open_temp_file "why3session" ".gp" in
      Stack.push fname to_remove;
      print_file ch
        (fun fmt -> create_gnuplot_by_time nb_provers fmt);
      Some fname
    else None
  in

310
  (* output .png, .pdf, .csv and run .qt if necessary *)
311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330
  if List.mem PNG !opt_gnuplot then
    call_gnuplot
      "set terminal pngcairo size 600, 400"
      (Printf.sprintf "set output \"%s.png\"" canonical_name)
      csv_file gp_file;
  if List.mem PDF !opt_gnuplot then
    call_gnuplot
      "set terminal pdfcairo"
      (Printf.sprintf "set output \"%s.pdf\"" canonical_name)
      csv_file gp_file;
  if List.mem SVG !opt_gnuplot then
    call_gnuplot
      "set terminal svg"
      (Printf.sprintf "set output \"%s.svg\"" canonical_name)
      csv_file gp_file;
  if List.mem QT !opt_gnuplot then
    call_gnuplot
      "set terminal qt persist"
      ""
      csv_file gp_file;
331
  (* Clean up temporary files *)
332 333 334 335 336 337 338 339
  Stack.iter Sys.remove to_remove


let run_by_time dir filter_provers =
  if !opt_aggregate then
    run_by_time_gen dir "aggregate.csv"
      (fun provers_time ->
         iter_files (run_one_by_time provers_time filter_provers))
340 341
  else
    iter_files (fun fname ->
342 343 344 345
        run_by_time_gen dir (try Filename.chop_extension fname with _ -> fname)
          (fun provers_time ->
             run_one_by_time provers_time filter_provers fname)
      )
346 347 348 349 350 351 352 353

(* 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
354 355 356
  let dir = Sysutil.absolutize_filename orig_dir (!opt_output_dir) in
  if !opt_data then run_normal dir filter_provers;
  if !opt_by_time || not (!opt_data) then run_by_time dir filter_provers
357 358 359

let cmd =
  { cmd_spec = spec;
360
    cmd_desc =
361
      "output session as a table or graph for simple processing or viewing";
362 363 364
    cmd_name = "csv";
    cmd_run  = run;
  }