From dc9ee50f48889a81b2ae4c9f3adfd43836bf9768 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 15 Sep 2020 14:34:50 +0200
Subject: [PATCH] [wp] better feedback for cache miss (wp-qualif)
---
src/plugins/wp/Cache.ml | 5 +++
src/plugins/wp/Cache.mli | 2 +
src/plugins/wp/VCS.ml | 40 ++++++++++---------
src/plugins/wp/VCS.mli | 3 +-
src/plugins/wp/register.ml | 20 ++++++----
src/plugins/wp/tests/wp/stmtcompiler_test.ml | 4 +-
.../wp/tests/wp/stmtcompiler_test_rela.ml | 4 +-
src/plugins/wp/wpo.ml | 8 ++--
8 files changed, 51 insertions(+), 35 deletions(-)
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index d08034e93ca..65da7ca4b52 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -136,6 +136,11 @@ module MODE = WpContext.StaticGenerator(Datatype.Unit)
let get_mode = MODE.get
let set_mode m = MODE.clear () ; Wp_parameters.Cache.set (mode_name m)
+let is_updating () =
+ match MODE.get () with
+ | NoCache | Replay | Offline -> false
+ | Update | Rebuild | Cleanup -> true
+
let task_hash wpo drv prover task =
lazy
begin
diff --git a/src/plugins/wp/Cache.mli b/src/plugins/wp/Cache.mli
index 39af5105141..85130ef5bbf 100644
--- a/src/plugins/wp/Cache.mli
+++ b/src/plugins/wp/Cache.mli
@@ -30,6 +30,8 @@ val get_hits : unit -> int
val get_miss : unit -> int
val get_removed : unit -> int
+val is_updating : unit -> bool
+
val cleanup_cache : unit -> unit
type runner =
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 1a855c3bbbe..50507c33c39 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -317,31 +317,35 @@ let pp_result fmt r =
| Stepout -> Format.fprintf fmt "Step limit%a" pp_perf r
| Timeout -> Format.fprintf fmt "Timeout%a" pp_perf r
-let pp_cache_miss fmt st prover r =
- let qualified =
- match prover with
- | Qed | Tactical -> true
- | NativeAltErgo | NativeCoq -> r.verdict <> Timeout
- | Why3 _ -> r.cached || r.prover_time < Rformat.epsilon
- in
- if not qualified && Wp_parameters.has_dkey dkey_shell then
- Format.fprintf fmt "%s%a (unqualified)" st pp_perf r
+let is_qualified prover result =
+ match prover with
+ | Qed | Tactical -> true
+ | NativeAltErgo | NativeCoq -> result.verdict <> Timeout
+ | Why3 _ -> result.cached || result.prover_time < Rformat.epsilon
+
+let pp_cache_miss fmt st updating prover result =
+ if not updating
+ && not (is_qualified prover result)
+ && Wp_parameters.has_dkey dkey_shell
+ then
+ Format.fprintf fmt "%s%a (missing cache)" st pp_perf result
else
- Format.pp_print_string fmt (if is_valid r then "Valid" else "Unsuccess")
+ Format.pp_print_string fmt @@
+ if is_valid result then "Valid" else "Unsuccess"
-let pp_result_qualif prover fmt r =
+let pp_result_qualif ?(updating=true) prover result fmt =
if Wp_parameters.has_dkey dkey_shell then
- match r.verdict with
+ match result.verdict with
| NoResult -> Format.pp_print_string fmt "No Result"
| Computing _ -> Format.pp_print_string fmt "Computing"
| Invalid -> Format.pp_print_string fmt "Invalid"
- | Failed -> Format.fprintf fmt "Failed@ %s" r.prover_errmsg
- | Valid -> pp_cache_miss fmt "Valid" prover r
- | Unknown -> pp_cache_miss fmt "Unsuccess" prover r
- | Timeout -> pp_cache_miss fmt "Timeout" prover r
- | Stepout -> pp_cache_miss fmt "Stepout" prover r
+ | Failed -> Format.fprintf fmt "Failed@ %s" result.prover_errmsg
+ | Valid -> pp_cache_miss fmt "Valid" updating prover result
+ | Unknown -> pp_cache_miss fmt "Unsuccess" updating prover result
+ | Timeout -> pp_cache_miss fmt "Timeout" updating prover result
+ | Stepout -> pp_cache_miss fmt "Stepout" updating prover result
else
- pp_result fmt r
+ pp_result fmt result
let compare p q =
let rank = function
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 0e869ebea14..54b34f23ef8 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -119,7 +119,8 @@ val configure : result -> config
val autofit : result -> bool (** Result that fits the default configuration *)
val pp_result : Format.formatter -> result -> unit
-val pp_result_qualif : prover -> Format.formatter -> result -> unit
+val pp_result_qualif : ?updating:bool -> prover -> result ->
+ Format.formatter -> unit
val compare : result -> result -> int (* best is minimal *)
val merge : result -> result -> result
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 6cb8afbc7c0..58c0b6ab08b 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -391,19 +391,21 @@ let results g =
(Wpo.get_results g)
let do_wpo_failed goal =
+ let updating = Cache.is_updating () in
match results goal with
| [p,r] ->
- Wp_parameters.result "[%a] Goal %s : %a%a"
+ Wp_parameters.result "[%a] Goal %s : %t%a"
VCS.pp_prover p (Wpo.get_gid goal)
- (VCS.pp_result_qualif p) r pp_warnings goal
+ (VCS.pp_result_qualif ~updating p r) pp_warnings goal
| pres ->
Wp_parameters.result "[Failed] Goal %s%t" (Wpo.get_gid goal)
begin fun fmt ->
pp_warnings fmt goal ;
List.iter
(fun (p,r) ->
- Format.fprintf fmt "@\n%8s: @[<hv>%a@]"
- (VCS.title_of_prover p) (VCS.pp_result_qualif p) r
+ Format.fprintf fmt "@\n%8s: @[<hv>%t@]"
+ (VCS.title_of_prover p)
+ (VCS.pp_result_qualif ~updating p r)
) pres ;
end
@@ -416,11 +418,12 @@ let do_wpo_smoke status goal =
(Wpo.get_gid goal)
begin fun fmt ->
pp_warnings fmt goal ;
+ let updating = Cache.is_updating () in
List.iter
(fun (p,r) ->
- Format.fprintf fmt "@\n%8s: @[<hv>%a@]"
+ Format.fprintf fmt "@\n%8s: @[<hv>%t@]"
(VCS.title_of_prover p)
- (VCS.pp_result_qualif p) r
+ (VCS.pp_result_qualif ~updating p r)
) (results goal) ;
end
@@ -453,10 +456,11 @@ let do_wpo_success goal s =
VCS.pp_prover script (Wpo.get_gid goal)
| Some prover ->
let result = Wpo.get_result goal prover in
+ let updating = Cache.is_updating () in
Wp_parameters.feedback ~ontty:`Silent
- "[%a] Goal %s : %a"
+ "[%a] Goal %s : %t"
VCS.pp_prover prover (Wpo.get_gid goal)
- (VCS.pp_result_qualif prover) result
+ (VCS.pp_result_qualif ~updating prover result)
end
let do_report_time fmt s =
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.ml b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
index 7d61b014274..07e77bf2309 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
@@ -28,8 +28,8 @@ let run () =
let spawn goal =
let result _ prv res =
- Format.printf "[%a] %a@.@\n"
- VCS.pp_prover prv (VCS.pp_result_qualif prv) res
+ Format.printf "[%a] %t@.@\n"
+ VCS.pp_prover prv (VCS.pp_result_qualif prv res)
in
let server = ProverTask.server () in
Prover.spawn goal ~delayed:true ~result provers;
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index 513c205deea..f38450c4501 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -27,8 +27,8 @@ let run () =
let spawn goal =
let result _ prv res =
- Format.printf "[%a] %a@.@\n"
- VCS.pp_prover prv (VCS.pp_result_qualif prv) res
+ Format.printf "[%a] %t@.@\n"
+ VCS.pp_prover prv (VCS.pp_result_qualif prv res)
in
let server = ProverTask.server () in
Prover.spawn goal ~delayed:true ~result provers;
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 1e5cc14b71b..0574facb577 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -283,8 +283,8 @@ struct
List.iter
(fun (prover,result) ->
if result.verdict <> NoResult then
- Format.fprintf fmt "Prover %a returns %a@\n"
- pp_prover prover (pp_result_qualif prover) result
+ Format.fprintf fmt "Prover %a returns %t@\n"
+ pp_prover prover (pp_result_qualif prover result)
) results ;
end
@@ -347,9 +347,9 @@ struct
List.iter
(fun (prover,result) ->
if result.verdict <> NoResult then
- Format.fprintf fmt "Prover %a returns %a@\n"
+ Format.fprintf fmt "Prover %a returns %t@\n"
pp_prover prover
- (pp_result_qualif prover) result
+ (pp_result_qualif prover result)
) results ;
end
--
GitLab