From 68fb5f9f4157bb66bd97a75c12b461fde670702a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 10 Sep 2019 12:16:47 +0200
Subject: [PATCH] [wp/cache] collect cache info
---
src/plugins/wp/ProverWhy3.ml | 42 +++++++++-----
src/plugins/wp/ProverWhy3.mli | 8 +++
src/plugins/wp/VCS.ml | 15 ++++-
src/plugins/wp/VCS.mli | 6 +-
src/plugins/wp/register.ml | 106 ++++++++++++++++++++++++----------
5 files changed, 129 insertions(+), 48 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 9d4aad3d212..ce30da10799 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -24,7 +24,6 @@
let dkey = Wp_parameters.register_category "prover"
let dkey_api = Wp_parameters.register_category "why3_api"
-let dkey_cache = Wp_parameters.register_category "cache"
let option_file = LogicBuiltins.create_option
(fun ~driver_dir x -> Filename.concat driver_dir x)
@@ -1088,6 +1087,13 @@ let call_prover ~timeout ~steplimit drv prover prover_config task =
type mode = NoCache | Update | Replay | Rebuild | Offline | Markup
+let hits = ref 0
+let miss = ref 0
+
+let reset () = hits := 0 ; miss := 0
+let get_hits () = !hits
+let get_miss () = !miss
+
let get_mode () =
match Wp_parameters.Cache.get () with
| "none" -> NoCache
@@ -1097,7 +1103,9 @@ let get_mode () =
| "offline" -> Offline
| "markup" -> Markup
| m -> Wp_parameters.error
- "Unknown -wp-cache %S (use 'none' instead)" m ; NoCache
+ ~once:true
+ "Unknown -wp-cache %S (use 'none' instead)" m ;
+ NoCache
let task_hash wpo drv prover task =
lazy
@@ -1117,7 +1125,8 @@ let task_hash wpo drv prover task =
let time_fits time = function
| None | Some 0 -> true
- | Some limit -> time <= float limit
+ | Some limit ->
+ time < float limit
let step_fits steps = function
| None | Some 0 -> true
@@ -1202,24 +1211,31 @@ let prove ?timeout ?steplimit ~prover wpo =
call_prover ~timeout ~steplimit drv prover config task
| Offline ->
let hash = task_hash wpo drv prover task in
- Task.return (get_cache_result ~mode hash)
+ let result = get_cache_result ~mode hash |> VCS.cached in
+ Task.return result
| Update | Replay | Rebuild | Markup ->
let hash = task_hash wpo drv prover task in
let result =
get_cache_result ~mode hash
- |> promote ~timeout ~steplimit in
+ |> promote ~timeout ~steplimit |> VCS.cached in
if VCS.is_verdict result
then
- ( if mode = Markup then
+ begin
+ incr hits ;
+ if mode = Markup then
set_cache_result ~mode hash prover result ;
- Task.return result )
+ Task.return result
+ end
else
- Task.finally
- (call_prover ~timeout ~steplimit drv prover config task)
- (function
- | Task.Result result when VCS.is_verdict result ->
- set_cache_result ~mode hash prover result
- | _ -> ())
+ begin
+ incr miss ;
+ Task.finally
+ (call_prover ~timeout ~steplimit drv prover config task)
+ (function
+ | Task.Result result when VCS.is_verdict result ->
+ set_cache_result ~mode hash prover result
+ | _ -> ())
+ end
end ()
with exn ->
let bt = Printexc.get_raw_backtrace () in
diff --git a/src/plugins/wp/ProverWhy3.mli b/src/plugins/wp/ProverWhy3.mli
index f2f10c93d0c..47f63870138 100644
--- a/src/plugins/wp/ProverWhy3.mli
+++ b/src/plugins/wp/ProverWhy3.mli
@@ -29,3 +29,11 @@ val add_specific_equality:
val prove : ?timeout:int -> ?steplimit:int -> prover:Why3Provers.t ->
Wpo.t -> VCS.result Task.task
(** Return NoResult if it is already proved by Qed *)
+
+type mode = NoCache | Update | Replay | Rebuild | Offline | Markup
+val get_mode : unit -> mode
+
+val reset : unit -> unit (** Reset cache statistics *)
+val get_hits : unit -> int
+val get_miss : unit -> int
+
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 98aa0f4d3f1..87f7bc0053f 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -27,6 +27,7 @@
let dkey_no_time_info = Wp_parameters.register_category "no-time-info"
let dkey_no_step_info = Wp_parameters.register_category "no-step-info"
let dkey_no_goals_info = Wp_parameters.register_category "no-goals-info"
+let dkey_no_cache_info = Wp_parameters.register_category "no-cache-info"
let dkey_success_only = Wp_parameters.register_category "success-only"
type prover =
@@ -214,6 +215,7 @@ type verdict =
type result = {
verdict : verdict ;
+ cached : bool ;
solver_time : float ;
prover_time : float ;
prover_steps : int ;
@@ -276,9 +278,10 @@ let autofit r =
step_fits r.prover_steps &&
depth_fits r.prover_depth
-let result ?(solver=0.0) ?(time=0.0) ?(steps=0) ?(depth=0) verdict =
+let result ?(cached=false) ?(solver=0.0) ?(time=0.0) ?(steps=0) ?(depth=0) verdict =
{
verdict ;
+ cached = cached ;
solver_time = solver ;
prover_time = time ;
prover_steps = steps ;
@@ -297,6 +300,7 @@ let stepout n = result ~steps:n Stepout
let computing kill = result (Computing kill)
let failed ?pos msg = {
verdict = Failed ;
+ cached = false ;
solver_time = 0.0 ;
prover_time = 0.0 ;
prover_steps = 0 ;
@@ -305,6 +309,8 @@ let failed ?pos msg = {
prover_errmsg = msg ;
}
+let cached r = if is_verdict r then { r with cached=true } else r
+
let kfailed ?pos msg = Pretty_utils.ksfprintf (failed ?pos) msg
let perfo extended dkey = extended || not (Wp_parameters.has_dkey dkey)
@@ -319,15 +325,17 @@ let pp_perf ~extended fmt r =
then Format.fprintf fmt " (%a)" Rformat.pp_time t ;
let s = r.prover_steps in
if s > 0 && perfo extended dkey_no_step_info
- then Format.fprintf fmt " (%d)" s
+ then Format.fprintf fmt " (%d)" s ;
+ if r.cached && perfo extended dkey_no_cache_info
+ then Format.fprintf fmt " (cached)" ;
end
let pp_res ~extended fmt r =
match r.verdict with
| NoResult -> Format.pp_print_string fmt (if extended then "No Result" else "-")
- | Invalid -> Format.pp_print_string fmt "Invalid"
| Computing _ -> Format.pp_print_string fmt "Computing"
| Checked -> Format.fprintf fmt "Typechecked"
+ | Invalid -> Format.pp_print_string fmt "Invalid"
| Valid when Wp_parameters.has_dkey dkey_success_only ->
Format.pp_print_string fmt "Valid"
| (Timeout|Stepout|Unknown) when Wp_parameters.has_dkey dkey_success_only ->
@@ -372,6 +380,7 @@ let merge r1 r2 =
let err = if r1.prover_errmsg <> "" then r1 else r2 in
{
verdict = combine r1.verdict r2.verdict ;
+ cached = r1.cached && r2.cached ;
solver_time = max r1.solver_time r2.solver_time ;
prover_time = max r1.prover_time r2.prover_time ;
prover_steps = max r1.prover_steps r2.prover_steps ;
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 14a1db16681..0b5436bc7dc 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -96,6 +96,7 @@ type verdict =
type result = {
verdict : verdict ;
+ cached : bool ;
solver_time : float ;
prover_time : float ;
prover_steps : int ;
@@ -114,7 +115,9 @@ val timeout : int -> result
val computing : (unit -> unit) -> result
val failed : ?pos:Lexing.position -> string -> result
val kfailed : ?pos:Lexing.position -> ('a,Format.formatter,unit,result) format4 -> 'a
-val result : ?solver:float -> ?time:float -> ?steps:int -> ?depth:int -> verdict -> result
+val cached : result -> result (** only for true verdicts *)
+
+val result : ?cached:bool -> ?solver:float -> ?time:float -> ?steps:int -> ?depth:int -> verdict -> result
val is_auto : prover -> bool
val is_verdict : result -> bool
@@ -133,4 +136,5 @@ val best : result list -> result
val dkey_no_time_info: Wp_parameters.category
val dkey_no_step_info: Wp_parameters.category
val dkey_no_goals_info: Wp_parameters.category
+val dkey_no_cache_info: Wp_parameters.category
val dkey_success_only: Wp_parameters.category
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 5e271cc24ee..43ba83d815c 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -201,6 +201,7 @@ type pstat = {
mutable proved : int ;
mutable unknown : int ;
mutable interrupted : int ;
+ mutable incache : int ;
mutable failed : int ;
mutable n_time : int ; (* nbr of measured times *)
mutable a_time : float ; (* sum of measured times *)
@@ -229,6 +230,7 @@ let clear_scheduled () =
exercised := 0 ;
proved := GOALS.empty ;
provers := PM.empty ;
+ ProverWhy3.reset () ;
end
let get_pstat p =
@@ -239,6 +241,7 @@ let get_pstat p =
interrupted = 0 ;
failed = 0 ;
steps = 0 ;
+ incache = 0 ;
n_time = 0 ;
a_time = 0.0 ;
u_time = 0.0 ;
@@ -297,6 +300,7 @@ let do_progress goal msg =
let do_wpo_stat goal prover res =
let s = get_pstat prover in
let open VCS in
+ if res.cached then s.incache <- succ s.incache ;
match res.verdict with
| Checked | NoResult | Computing _ | Invalid | Unknown ->
s.unknown <- succ s.unknown
@@ -329,23 +333,17 @@ let do_wpo_result goal prover res =
do_wpo_stat goal prover res ;
end
-let do_why3_result goal prover res =
- if VCS.is_verdict res then
- begin
- do_wpo_stat goal prover res ;
- let open VCS in
- if res.verdict <> Valid then
- Wp_parameters.result
- "[%a] Goal %s : %a"
- VCS.pp_prover prover (Wpo.get_gid goal)
- VCS.pp_result res ;
- end
-
let do_wpo_success goal s =
if not (Wp_parameters.Check.get ()) then
- match s with
- | None ->
- if not (Wp_parameters.Generate.get ()) then
+ if Wp_parameters.Generate.get () then
+ match s with
+ | None -> ()
+ | Some prover ->
+ Wp_parameters.feedback ~ontty:`Silent
+ "[%a] Goal %s : Valid" VCS.pp_prover prover (Wpo.get_gid goal)
+ else
+ match s with
+ | None ->
begin
match Wpo.get_results goal with
| [p,r] ->
@@ -363,9 +361,12 @@ let do_wpo_success goal s =
) pres ;
end
end
- | Some prover ->
- Wp_parameters.feedback ~ontty:`Silent
- "[%a] Goal %s : Valid" VCS.pp_prover prover (Wpo.get_gid goal)
+ | Some p ->
+ let r = Wpo.get_result goal p in
+ Wp_parameters.feedback ~ontty:`Silent
+ "[%a] Goal %s : %a%a"
+ VCS.pp_prover p (Wpo.get_gid goal)
+ VCS.pp_result r pp_warnings goal
let do_report_time fmt s =
begin
@@ -411,9 +412,11 @@ let do_report_stopped fmt s =
else
begin
if s.interrupted > 0 then
- Format.fprintf fmt " (interrupted: %d)" s.interrupted ;
+ Format.fprintf fmt " (stopped: %d)" s.interrupted ;
if s.unknown > 0 then
Format.fprintf fmt " (unknown: %d)" s.unknown ;
+ if s.incache > 0 then
+ Format.fprintf fmt " (cached: %d)" s.incache ;
end
let do_report_prover_stats pp_prover fmt (p,s) =
@@ -428,27 +431,68 @@ let do_report_prover_stats pp_prover fmt (p,s) =
Format.fprintf fmt "@\n" ;
end
+let dkey_cache = Wp_parameters.register_category "cache"
+
+let do_report_cache_usage () =
+ if Wp_parameters.has_dkey dkey_cache
+ then
+ let hits = ProverWhy3.get_hits () in
+ let miss = ProverWhy3.get_miss () in
+ if hits <= 0 && miss <= 0 then
+ Wp_parameters.result "[Cache] not used"
+ else
+ let mode = ProverWhy3.get_mode () in
+ Wp_parameters.result "[Cache]%t"
+ begin fun fmt ->
+ let sep = ref " " in
+ let pp_cache fmt n job =
+ if n > 0 then
+ ( Format.fprintf fmt "%s%s:%d" !sep job n ; sep := ", " ) in
+ match mode with
+ | ProverWhy3.NoCache -> ()
+ | ProverWhy3.Replay ->
+ pp_cache fmt hits "found" ;
+ pp_cache fmt miss "missed" ;
+ Format.pp_print_newline fmt () ;
+ | ProverWhy3.Offline ->
+ pp_cache fmt hits "found" ;
+ pp_cache fmt miss "failed" ;
+ Format.pp_print_newline fmt () ;
+ | ProverWhy3.Update ->
+ pp_cache fmt hits "found" ;
+ pp_cache fmt miss "updated" ;
+ Format.pp_print_newline fmt () ;
+ | ProverWhy3.Markup ->
+ pp_cache fmt hits "found" ;
+ pp_cache fmt miss "missed" ;
+ pp_cache fmt (hits+miss) "updated" ;
+ Format.pp_print_newline fmt () ;
+ | ProverWhy3.Rebuild ->
+ pp_cache fmt (hits+miss) "updated" ;
+ Format.pp_print_newline fmt () ;
+ end
+
let do_report_scheduled () =
if not (Wp_parameters.has_dkey VCS.dkey_no_goals_info) then
if Wp_parameters.Generate.get () then
let plural = if !exercised > 1 then "s" else "" in
Wp_parameters.result "%d goal%s generated" !exercised plural
else
- begin
- let proved = GOALS.cardinal !proved in
- Wp_parameters.result "%t"
- (fun fmt ->
- Format.fprintf fmt "Proved goals: %4d / %d@\n" proved !scheduled ;
- Pretty_utils.pp_items
- ~min:12 ~align:`Left
- ~title:(fun (prover,_) -> VCS.title_of_prover prover)
- ~iter:(fun f -> PM.iter (fun p s -> f (p,s)) !provers)
- ~pp_title:(fun fmt a -> Format.fprintf fmt "%s:" a)
- ~pp_item:do_report_prover_stats fmt) ;
- end
+ let proved = GOALS.cardinal !proved in
+ Wp_parameters.result "%t"
+ begin fun fmt ->
+ Format.fprintf fmt "Proved goals: %4d / %d@\n" proved !scheduled ;
+ Pretty_utils.pp_items
+ ~min:12 ~align:`Left
+ ~title:(fun (prover,_) -> VCS.title_of_prover prover)
+ ~iter:(fun f -> PM.iter (fun p s -> f (p,s)) !provers)
+ ~pp_title:(fun fmt a -> Format.fprintf fmt "%s:" a)
+ ~pp_item:do_report_prover_stats fmt ;
+ end
let do_list_scheduled_result () =
begin
+ do_report_cache_usage () ;
do_report_scheduled () ;
clear_scheduled () ;
end
--
GitLab