why3session_info.ml 14.2 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11

12
13
14
15
16
(**************************************************************************)
(* Specific source code for computing statistics is a contribution by     *)
(* David MENTRE <dmentre@linux-france.org>, 2011                          *)
(**************************************************************************)

17
18
19
20
open Why3
open Why3session_lib
open Whyconf
open Format
21
open Session
22
open Stdlib
23
24

let opt_print_provers = ref false
25
let opt_print_edited = ref false
26
let opt_tree_print = ref false
27
let opt_stats_print = ref false
28
let opt_hist_print = ref false
29
let opt_project_dir = ref false
30
let opt_print0 = ref false
31
32
33

let spec =
  ("--provers", Arg.Set opt_print_provers,
MARCHE Claude's avatar
MARCHE Claude committed
34
   " provers used in the session" ) ::
35
  ("--edited-files", Arg.Set opt_print_edited,
MARCHE Claude's avatar
MARCHE Claude committed
36
   " edited proof scripts in the session" ) ::
37
  ("--stats", Arg.Set opt_stats_print,
38
   " print various proofs statistics" ) ::
39
  ("--graph", Arg.Set opt_hist_print,
40
   " print a graph of the total time needed for \
41
     proving a given number of goals for each provers" ) ::
42
  ("--tree", Arg.Set opt_tree_print,
MARCHE Claude's avatar
MARCHE Claude committed
43
   " session contents as a tree in textual format" ) ::
44
  ("--dir", Arg.Set opt_project_dir,
45
   " print the directory of the session" ) ::
46
  ("--print0", Arg.Set opt_print0,
MARCHE Claude's avatar
MARCHE Claude committed
47
   " use the null character instead of newline" ) ::
48
49
50
51
    common_options


type proof_stats =
52
53
    { mutable nb_root_goals : int;
      mutable nb_sub_goals : int;
54
      mutable max_time : float;
55
56
      mutable nb_proved_root_goals : int;
      mutable nb_proved_sub_goals : int;
57
      mutable no_proof : Sstr.t;
58
      mutable only_one_proof : Sstr.t;
59
      prover_hist : int Mfloat.t Hprover.t;
60
      prover_min_time : float Hprover.t;
MARCHE Claude's avatar
MARCHE Claude committed
61
      prover_sum_time : float Hprover.t;
62
63
      prover_max_time : float Hprover.t;
      prover_num_proofs : int Hprover.t;
MARCHE Claude's avatar
MARCHE Claude committed
64
      (* prover_data : (string) Hprover.t *)
65
66
67
    }

let new_proof_stats () =
68
69
  { nb_root_goals = 0;
    nb_sub_goals = 0;
70
    max_time = 0.0;
71
72
    nb_proved_root_goals = 0;
    nb_proved_sub_goals = 0;
73
    no_proof = Sstr.empty;
74
    only_one_proof = Sstr.empty;
75
    prover_hist = Hprover.create 3;
76
    prover_min_time = Hprover.create 3;
MARCHE Claude's avatar
MARCHE Claude committed
77
    prover_sum_time = Hprover.create 3;
78
79
    prover_max_time = Hprover.create 3;
    prover_num_proofs =  Hprover.create 3;
MARCHE Claude's avatar
MARCHE Claude committed
80
    (* prover_data = Hprover.create 3  *)}
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104

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

MARCHE Claude's avatar
MARCHE Claude committed
105
let update_sum_time tbl (prover, time) =
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
  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

121
122
123
124
125
126
127
128
129
130
131
132
133
let update_hist tbl (prover, time) =
  let h =
    try Hprover.find tbl prover
    with Not_found -> Mfloat.empty
  in
  let h =
    try
      let c = Mfloat.find time h in
      Mfloat.add time (succ c) h
    with Not_found ->
      Mfloat.add time 1 h
  in
  Hprover.replace tbl prover h
134

135
136
let update_perf_stats stats ((_,t) as prover_and_time) =
  if t > stats.max_time then stats.max_time <- t;
137
138
  update_min_time stats.prover_min_time prover_and_time;
  update_max_time stats.prover_max_time prover_and_time;
MARCHE Claude's avatar
MARCHE Claude committed
139
  update_sum_time stats.prover_sum_time prover_and_time;
140
141
  update_count stats.prover_num_proofs prover_and_time;
  update_hist stats.prover_hist prover_and_time
142
143
144

let string_of_prover p = Pp.string_of_wnl print_prover p

145
146
147
148
let rec stats_of_goal ~root prefix_name stats goal =
  if root
  then stats.nb_root_goals <- stats.nb_root_goals + 1
  else stats.nb_sub_goals <- stats.nb_sub_goals + 1;
149
150
151
152
153
154
155
156
157
158
159
160
161
  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)
162
163
164
165
166
      goal.goal_external_proofs
      []
  in
  List.iter (update_perf_stats stats) proof_list;
  PHstr.iter (stats_of_transf prefix_name stats) goal.goal_transformations;
167
  if not (Opt.inhabited goal.goal_verified) then
168
169
170
171
    let goal_name = prefix_name ^ goal.goal_name.Ident.id_string in
    stats.no_proof <- Sstr.add goal_name stats.no_proof
  else
    begin
172
173
174
175
      if root then
        stats.nb_proved_root_goals <- stats.nb_proved_root_goals + 1
      else
        stats.nb_proved_sub_goals <- stats.nb_proved_sub_goals + 1;
176
177
178
179
180
181
182
183
184
      match proof_list with
      | [ (prover, _) ] ->
        let goal_name = prefix_name ^ goal.goal_name.Ident.id_string in
        stats.only_one_proof <-
          Sstr.add
          (goal_name ^ " : " ^ (string_of_prover prover))
          stats.only_one_proof
      | _ -> ()
    end
185
186
187

and stats_of_transf prefix_name stats _ transf =
  let prefix_name = prefix_name ^ transf.transf_name  ^ " / " in
188
  List.iter (stats_of_goal ~root:false prefix_name stats) transf.transf_goals
189
190
191
192
193

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
194
  List.iter (stats_of_goal ~root:true prefix_name stats) goals
195
196
197
198
199

let stats_of_file stats _ file =
  let theories = file.file_theories in
  List.iter (stats_of_theory file stats) theories

MARCHE Claude's avatar
MARCHE Claude committed
200
201
202
203
204
205


type 'a goal_stat =
  | No of ('a transf * ('a goal * 'a goal_stat) list) list
  | Yes of (prover * float) list * ('a transf * ('a goal * 'a goal_stat) list) list

206
let rec stats2_of_goal ~nb_proofs g : 'a goal_stat =
MARCHE Claude's avatar
MARCHE Claude committed
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
  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)
      g.goal_external_proofs
      []
  in
  let l =
    PHstr.fold
      (fun _ tr acc ->
        match stats2_of_transf ~nb_proofs tr with
          | [] -> acc
          | r -> (tr,List.rev r)::acc)
      g.goal_transformations
      []
  in
  if match nb_proofs with
233
    | 0 -> not (Opt.inhabited g.goal_verified)
MARCHE Claude's avatar
MARCHE Claude committed
234
235
236
237
    | 1 -> List.length proof_list = 1
    | _ -> assert false
      then Yes(proof_list,l) else No(l)

238
and stats2_of_transf ~nb_proofs tr : ('a goal * 'a goal_stat) list =
MARCHE Claude's avatar
MARCHE Claude committed
239
240
241
242
243
244
245
  List.fold_left
    (fun acc g ->
      match stats2_of_goal ~nb_proofs g with
        | No [] -> acc
        | r -> (g,r)::acc)
    [] tr.transf_goals

MARCHE Claude's avatar
MARCHE Claude committed
246
let print_res ~time fmt (p,t) =
MARCHE Claude's avatar
MARCHE Claude committed
247
248
  fprintf fmt "%a" print_prover p;
  if time then fprintf fmt " (%.2f)" t
MARCHE Claude's avatar
MARCHE Claude committed
249

MARCHE Claude's avatar
MARCHE Claude committed
250
let rec print_goal_stats ~time depth (g,l) =
251
  for _i=1 to depth do printf "  " done;
MARCHE Claude's avatar
MARCHE Claude committed
252
253
254
255
  printf "+-- goal %s" g.goal_name.Ident.id_string;
  match l with
    | No l ->
      printf "@\n";
MARCHE Claude's avatar
MARCHE Claude committed
256
      List.iter (print_transf_stats ~time (depth+1)) l
MARCHE Claude's avatar
MARCHE Claude committed
257
258
259
260
    | Yes(pl,l) ->
      begin
        match pl with
          | [] -> printf "@\n"
MARCHE Claude's avatar
MARCHE Claude committed
261
          | _ -> printf ": %a@\n"
MARCHE Claude's avatar
MARCHE Claude committed
262
            (Pp.print_list pp_print_space (print_res ~time)) pl
MARCHE Claude's avatar
MARCHE Claude committed
263
      end;
MARCHE Claude's avatar
MARCHE Claude committed
264
      List.iter (print_transf_stats ~time (depth+1)) l
MARCHE Claude's avatar
MARCHE Claude committed
265

MARCHE Claude's avatar
MARCHE Claude committed
266
and print_transf_stats ~time depth (tr,l) =
267
  for _i=1 to depth do printf "  " done;
MARCHE Claude's avatar
MARCHE Claude committed
268
  printf "+-- transformation %s@\n" tr.transf_name;
MARCHE Claude's avatar
MARCHE Claude committed
269
  List.iter (print_goal_stats ~time (depth+1)) l
MARCHE Claude's avatar
MARCHE Claude committed
270
271
272
273
274
275
276
277
278

let stats2_of_theory ~nb_proofs th =
  List.fold_left
    (fun acc g ->
      match stats2_of_goal ~nb_proofs g with
        | No [] -> acc
        | r -> (g,r)::acc)
    [] th.theory_goals

MARCHE Claude's avatar
MARCHE Claude committed
279
let print_theory_stats ~time (th,r) =
MARCHE Claude's avatar
MARCHE Claude committed
280
  printf "  +-- theory %s@\n" th.theory_name.Ident.id_string;
MARCHE Claude's avatar
MARCHE Claude committed
281
  List.iter (print_goal_stats ~time 2) r
MARCHE Claude's avatar
MARCHE Claude committed
282
283
284
285
286
287
288
289
290

let stats2_of_file ~nb_proofs file =
  List.fold_left
    (fun acc th ->
      match stats2_of_theory ~nb_proofs th with
        | [] -> acc
        | r -> (th,List.rev r)::acc)
    [] file.file_theories

291
let stats2_of_session ~nb_proofs s acc =
MARCHE Claude's avatar
MARCHE Claude committed
292
293
294
295
296
  PHstr.fold
    (fun _ f acc ->
      match stats2_of_file ~nb_proofs f with
        | [] -> acc
        | r -> (f,List.rev r)::acc)
297
    s.session_files acc
MARCHE Claude's avatar
MARCHE Claude committed
298

MARCHE Claude's avatar
MARCHE Claude committed
299
let print_file_stats ~time (f,r) =
MARCHE Claude's avatar
MARCHE Claude committed
300
  printf "+-- file %s@\n" f.file_name;
MARCHE Claude's avatar
MARCHE Claude committed
301
  List.iter (print_theory_stats ~time) r
MARCHE Claude's avatar
MARCHE Claude committed
302

MARCHE Claude's avatar
MARCHE Claude committed
303
let print_session_stats ~time = List.iter (print_file_stats ~time)
MARCHE Claude's avatar
MARCHE Claude committed
304
305
306


(*
307
308
309
310
let fill_prover_data stats session =
  Sprover.iter
    (fun prover ->
      Hprover.add stats.prover_data prover
MARCHE Claude's avatar
MARCHE Claude committed
311
        (string_of_prover prover))
312
    (get_used_provers session)
MARCHE Claude's avatar
MARCHE Claude committed
313
*)
314

MARCHE Claude's avatar
MARCHE Claude committed
315
(*
316
317
318
319
320
321
322
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
MARCHE Claude's avatar
MARCHE Claude committed
323
*)
324

MARCHE Claude's avatar
MARCHE Claude committed
325
let print_stats r0 r1 stats =
326
327
328
329
330
  printf "== Number of root goals ==@\n  total: %d  proved: %d@\n@\n"
    stats.nb_root_goals stats.nb_proved_root_goals;

  printf "== Number of sub goals ==@\n  total: %d  proved: %d@\n@\n"
    stats.nb_sub_goals stats.nb_proved_sub_goals;
331

332
  printf "== Goals not proved ==@\n  @[";
MARCHE Claude's avatar
MARCHE Claude committed
333
  print_session_stats ~time:false r0;
MARCHE Claude's avatar
MARCHE Claude committed
334
  (* Sstr.iter (fun s -> printf "%s@\n" s) stats.no_proof; *)
335
336
337
  printf "@]@\n";

  printf "== Goals proved by only one prover ==@\n  @[";
MARCHE Claude's avatar
MARCHE Claude committed
338
  print_session_stats ~time:false r1;
MARCHE Claude's avatar
MARCHE Claude committed
339
  (* Sstr.iter (fun s -> printf "%s@\n" s) stats.only_one_proof; *)
340
341
  printf "@]@\n";

MARCHE Claude's avatar
MARCHE Claude committed
342
  printf "== Statistics per prover: number of proofs, time (minimum/maximum/average) in seconds ==@\n  @[";
MARCHE Claude's avatar
MARCHE Claude committed
343
344
345
346
347
348
349
  Hprover.iter (fun prover n ->
    let sum_times = Hprover.find stats.prover_sum_time prover in
    printf "%-20s : %3d %6.2f %6.2f %6.2f@\n"
      (string_of_prover prover) n
      (Hprover.find stats.prover_min_time prover)
      (Hprover.find stats.prover_max_time prover)
      (sum_times /. (float_of_int n)))
350
351
    stats.prover_num_proofs;
  printf "@]@\n"
352

MARCHE Claude's avatar
MARCHE Claude committed
353

354
let run_one stats r0 r1 fname =
355
356
  let project_dir = Session.get_project_dir fname in
  if !opt_project_dir then printf "%s@." project_dir;
357
  let session,_use_shapes = Session.read_session project_dir in
358
  let sep = if !opt_print0 then Pp.print0 else Pp.newline in
359
360
  if !opt_print_provers then
    printf "%a@."
361
      (Pp.print_iter1 Sprover.iter sep print_prover)
362
      (get_used_provers session);
363
  if !opt_print_edited then
364
    session_iter_proof_attempt
365
      (fun pr ->
366
        Opt.iter (fun s -> printf "%s%a" s sep ())
367
          (get_edited_as_abs session pr))
368
      session;
369
  if !opt_tree_print then
370
    printf "%a@." print_session session;
371
  if !opt_stats_print || !opt_hist_print then
372
    begin
MARCHE Claude's avatar
MARCHE Claude committed
373
      (* fill_prover_data stats session; *)
374
      PHstr.iter (stats_of_file stats) session.session_files;
375
376
      r0 := stats2_of_session ~nb_proofs:0 session !r0;
      r1 := stats2_of_session ~nb_proofs:1 session !r1
377
    end
378

379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
(**** print histograms ******)

let print_hist stats =
  let main_file,main_ch =
    Filename.open_temp_file "why3session" ".gnuplot"
  in
  let main_fmt = formatter_of_out_channel main_ch in
  fprintf main_fmt "set logscale y@\n";
  fprintf main_fmt "set key rmargin@\n";
  let max_sum_times =
    Hprover.fold
      (fun _ s acc -> max s acc)
      stats.prover_sum_time 0.0
  in
  let (_:int) =
  Hprover.fold
    (fun p h acc ->
      let pf,ch = Filename.open_temp_file "why3session" ".data" in
      if acc = 1 then
398
        fprintf main_fmt "plot [0:%d] [0.1:%.2f] "
399
400
401
402
403
404
405
406
          (stats.nb_proved_sub_goals + stats.nb_proved_root_goals)
          max_sum_times
      else
        fprintf main_fmt "replot";
      fprintf main_fmt
        " \"%s\" using 2:1 title \"%s\" with linespoints ps 0.2@\n"
        pf (string_of_prover p);
      let fmt = formatter_of_out_channel ch in
407
      (* The time is also accumulated in order to obtain the total cpu time
408
          taken to reach the given number of proved goal *)
409
      fprintf fmt "0.1 0@\n";
410
      let (_ : float * int) =
411
        Mfloat.fold
412
          (fun t c (acct,accc) ->
413
            let accc = c + accc in
414
            let acct = (float c) *. t +. acct in
415
416
            fprintf fmt "%.2f %d@\n" acct accc;
            (acct,accc))
417
          h (0.1,0)
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
      in
      fprintf fmt "@.";
      close_out ch;
      acc+1)
    stats.prover_hist 1
  in
  fprintf main_fmt "pause -1 \"Press any key\"@\n";
  fprintf main_fmt "set terminal pdfcairo@\n";
  fprintf main_fmt "set output \"why3session.pdf\"@\n";
  fprintf main_fmt "replot@.";
  close_out main_ch;
  let cmd = "gnuplot " ^ main_file in
  eprintf "Running command %s@." cmd;
  let ret = Sys.command cmd in
  if ret <> 0 then
    eprintf "Command %s failed@." cmd
  else
    eprintf "See also results in file why3session.pdf@."

437
(****** run on all files  ******)
438
439

let run () =
MARCHE Claude's avatar
MARCHE Claude committed
440
  let _,_,should_exit1 = read_env_spec () in
441
  if should_exit1 then exit 1;
442
443
444
  let stats = new_proof_stats () in
  let r0 = ref [] and r1 = ref [] in
  iter_files (run_one stats r0 r1);
445
446
  if !opt_stats_print then
    begin
MARCHE Claude's avatar
MARCHE Claude committed
447
      (* finalize_stats stats; *)
448
      print_stats !r0 !r1 stats
449
450
    end;
  if !opt_hist_print then print_hist stats
451
452
453
454


let cmd =
  { cmd_spec = spec;
455
    cmd_desc = "print informations and statistics about a session";
456
457
458
    cmd_name = "info";
    cmd_run  = run;
  }
459
460
461
462
463
464
465


(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3session.byte"
End:
*)