From 722e71ed3deb5430d2e03f56793ea42028d966f1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 8 Jul 2022 21:53:53 +0200
Subject: [PATCH] [wp] printing stats wrt various modes
---
src/plugins/wp/ProverWhy3.ml | 2 +-
src/plugins/wp/Stats.ml | 35 ++++++++++++++++++++--------------
src/plugins/wp/Stats.mli | 4 ++--
src/plugins/wp/VCS.ml | 15 ++++++---------
src/plugins/wp/Why3Provers.ml | 9 +++++----
src/plugins/wp/Why3Provers.mli | 7 +++----
src/plugins/wp/register.ml | 2 +-
7 files changed, 39 insertions(+), 35 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 212fe6f8bab..307d9dc45c1 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1247,7 +1247,7 @@ let digest wpo drv prover task =
let _ = Command.print_file file
begin fun fmt ->
Format.fprintf fmt "(* WP Task for Prover %s *)@\n"
- (Why3Provers.print_why3 prover) ;
+ (Why3Provers.ident_why3 prover) ;
Why3.Driver.print_task_prepared drv fmt task ;
end
in Digest.file file |> Digest.to_hex
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index de3d5cee53e..32e6fb46c18 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -124,16 +124,14 @@ let consolidated ~smoke = function
r.verdict,
(if cached then 1 else 0),
if p = Qed then [Qed,pqed r]
- else
- if VCS.is_valid r
- then pmerge [Qed,psolver r] [p,if smoke then psmoke r else presult r]
- else []
+ else pmerge [Qed,psolver r] [p,if smoke then psmoke r else presult r]
let smoked_result (p,r) = p, { r with verdict = VCS.smoked r.verdict }
let results ~smoke prs =
let prs = if smoke then List.map smoked_result prs else prs in
let verdict, cached, provers = consolidated ~smoke prs in
+ verdict,
match verdict with
| Valid ->
{ zero with provers ; cached ; proved = 1 }
@@ -194,7 +192,7 @@ let pp_pstats fmt p =
Rformat.pp_time mean
Rformat.pp_time p.tmax
-let pp_stats fmt s =
+let pp_stats ~shell ~updating fmt s =
let vp = s.proved in
let np = proofs s in
if vp < np && np > 1 then
@@ -203,21 +201,30 @@ let pp_stats fmt s =
Format.fprintf fmt " (Tactics %d)" s.tactics
else if np <= 1 && s.tactics = 1 then
Format.fprintf fmt " (Tactic)" ;
- let shell = Wp_parameters.has_dkey dkey_shell in
+ let perfo = not shell || (not updating && s.cached < vp) in
+ let only_qed = match s.provers with [Qed,_] -> true | _ -> false in
List.iter
(fun (p,pr) ->
let success = truncate pr.success in
- let title = VCS.title_of_prover ~version:false p in
- Format.fprintf fmt " (%s" title ;
- if success > 0 && np > 1 then
- Format.fprintf fmt " %d/%d" success np ;
- if not shell && pr.time > Rformat.epsilon then
- Format.fprintf fmt " %a" Rformat.pp_time pr.time ;
- Format.fprintf fmt ")"
+ let print_perfo = perfo && pr.time > Rformat.epsilon in
+ let print_proofs = success > 0 && np > 1 in
+ if p != Qed || only_qed || print_perfo || print_proofs then
+ begin
+ let title = VCS.title_of_prover ~version:false p in
+ Format.fprintf fmt " (%s" title ;
+ if print_proofs then
+ Format.fprintf fmt " %d/%d" success np ;
+ if print_perfo then
+ Format.fprintf fmt " %a" Rformat.pp_time pr.time ;
+ Format.fprintf fmt ")"
+ end
) s.provers ;
if 0 < s.cached then
- if s.cached = np then
+ if s.cached = vp || updating then
Format.fprintf fmt " (Cached)"
+ else
+ if shell then
+ Format.fprintf fmt " (Cache miss %d)" (np - s.cached)
else
Format.fprintf fmt " (Cached %d/%d)" s.cached np
diff --git a/src/plugins/wp/Stats.mli b/src/plugins/wp/Stats.mli
index 0a2023db5fc..c1ced421667 100644
--- a/src/plugins/wp/Stats.mli
+++ b/src/plugins/wp/Stats.mli
@@ -47,9 +47,9 @@ type stats = {
}
val pp_pstats : Format.formatter -> pstats -> unit
-val pp_stats : Format.formatter -> stats -> unit
+val pp_stats : shell:bool -> updating:bool -> Format.formatter -> stats -> unit
-val results : smoke:bool -> (VCS.prover * VCS.result) list -> stats
+val results : smoke:bool -> (VCS.prover * VCS.result) list -> VCS.verdict * stats
val tactical : qed:float -> stats list -> stats
val proofs : stats -> int
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index a280067c96a..3a94da3f3fc 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -55,7 +55,7 @@ let parse_prover = function
| Fallback p ->
Wp_parameters.warning ~current:false ~once:true
"Prover '%s' not found, fallback to '%s'"
- (String.concat ":" prv) (Why3Provers.print_wp p) ;
+ (String.concat ":" prv) (Why3Provers.ident_wp p) ;
Some (Why3 p)
| NotFound ->
Wp_parameters.error ~once:true
@@ -75,18 +75,15 @@ let parse_mode m =
Batch
let name_of_prover = function
- | Why3 s -> Why3Provers.print_wp s
+ | Why3 s -> Why3Provers.ident_wp s
| Qed -> "qed"
| Tactical -> "script"
let title_of_prover ?version = function
| Why3 s ->
- let v = match version with Some v -> v | None ->
- Wp_parameters.has_dkey dkey_shell
- in
- if v
- then Why3Provers.name s
- else Why3Provers.title s
+ let version = match version with Some v -> v | None ->
+ not (Wp_parameters.has_dkey dkey_shell)
+ in Why3Provers.title ~version s
| Qed -> "Qed"
| Tactical -> "Script"
@@ -112,7 +109,7 @@ let sanitize_why3 s =
Buffer.contents buffer
let filename_for_prover = function
- | Why3 s -> sanitize_why3 (Why3Provers.print_wp s)
+ | Why3 s -> sanitize_why3 (Why3Provers.ident_wp s)
| Qed -> "Qed"
| Tactical -> "Tactical"
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 167dc3e1370..0d2e6511ac8 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -87,14 +87,15 @@ let find_fallback name =
end
| _ -> NotFound
-let print_why3 = Why3.Whyconf.prover_parseable_format
-let print_wp s =
+let ident_why3 = Why3.Whyconf.prover_parseable_format
+let ident_wp s =
let name = Why3.Whyconf.prover_parseable_format s in
let prv = String.split_on_char ',' name in
String.concat ":" prv
-let title p = Pretty_utils.to_string Why3.Whyconf.print_prover p
-let name p = p.Why3.Whyconf.prover_name
+let title ?(version=true) p =
+ if version then Pretty_utils.to_string Why3.Whyconf.print_prover p
+ else p.Why3.Whyconf.prover_name
let compare = Why3.Whyconf.Prover.compare
let is_mainstream p = p.Why3.Whyconf.prover_altern = ""
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
index 5463b35fa48..13f9ef446de 100644
--- a/src/plugins/wp/Why3Provers.mli
+++ b/src/plugins/wp/Why3Provers.mli
@@ -32,10 +32,9 @@ val find_opt : string -> t option
type fallback = Exact of t | Fallback of t | NotFound
val find_fallback : string -> fallback
-val print_why3 : t -> string
-val print_wp : t -> string
-val title : t -> string
-val name : t -> string
+val ident_why3 : t -> string
+val ident_wp : t -> string
+val title : ?version:bool -> t -> string
val compare : t -> t -> int
val provers : unit -> t list
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 8952be0b750..99bd498c8a5 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -873,7 +873,7 @@ let do_prover_detect () =
Wp_parameters.result "Prover %10s %-6s [%a%s]"
p.prover_name p.prover_version
print_prover_shortcuts_for p
- (Why3Provers.print_wp p)
+ (Why3Provers.ident_wp p)
) provers
(* ------------------------------------------------------------------------ *)
--
GitLab