diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 3375e04b614503585ce7b7c0ee1915763808b8a9..5a83f98a02c057cccf36c05d694f444267629c82 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1085,14 +1085,50 @@ let call_prover ~timeout ~steplimit drv prover prover_config task =
(* --- Cache Management --- *)
(* -------------------------------------------------------------------------- *)
-type mode = NoCache | Update | Replay | Rebuild | Offline | Markup
+type mode = NoCache | Update | Replay | Rebuild | Offline | Cleanup
let hits = ref 0
let miss = ref 0
+let removed = ref 0
+let cleanup = Hashtbl.create 0 (* used entries *)
+
+let reset () =
+ begin
+ hits := 0 ;
+ miss := 0 ;
+ removed := 0 ;
+ Hashtbl.clear cleanup ;
+ end
-let reset () = hits := 0 ; miss := 0
let get_hits () = !hits
let get_miss () = !miss
+let get_removed () = !removed
+
+let mark_cache ~mode hash =
+ if mode = Cleanup then Hashtbl.replace cleanup hash ()
+
+let cleanup_cache ~mode =
+ if mode = Cleanup then
+ let dir = Wp_parameters.get_session_dir "cache" in
+ try
+ if Sys.is_directory dir then
+ Array.iter
+ (fun f ->
+ if Filename.check_suffix f ".json" then
+ let hash = Filename.chop_suffix f ".json" in
+ if not (Hashtbl.mem cleanup hash) then
+ begin
+ incr removed ;
+ Extlib.safe_remove (Printf.sprintf "%s/%s" dir f) ;
+ end
+ ) (Sys.readdir dir) ;
+ with Unix.Unix_error _ as exn ->
+ Wp_parameters.failure "Can not cleanup cache (%s)"
+ (Printexc.to_string exn)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Cache Management --- *)
+(* -------------------------------------------------------------------------- *)
let parse_mode ~origin ~fallback = function
| "none" -> NoCache
@@ -1100,7 +1136,7 @@ let parse_mode ~origin ~fallback = function
| "replay" -> Replay
| "rebuild" -> Rebuild
| "offline" -> Offline
- | "markup" -> Markup
+ | "cleanup" -> Cleanup
| m ->
Wp_parameters.warning ~current:false
"Unknown %s mode %S (use %s instead)" origin m fallback ;
@@ -1179,12 +1215,14 @@ let promote ~timeout ~steplimit (res : VCS.result) =
let get_cache_result ~mode hash =
match mode with
| NoCache | Rebuild -> VCS.no_result
- | Update | Markup | Replay | Offline ->
+ | Update | Cleanup | Replay | Offline ->
let dir = Wp_parameters.get_session_dir "cache" in
- let file = Printf.sprintf "%s/%s.json" dir (Lazy.force hash) in
+ let hash = Lazy.force hash in
+ let file = Printf.sprintf "%s/%s.json" dir hash in
if not (Sys.file_exists file) then VCS.no_result
else
try
+ mark_cache ~mode hash ;
Json.load_file file |> ProofScript.result_of_json
with err ->
Wp_parameters.failure ~once:true "invalid cache entry (%s)"
@@ -1194,10 +1232,12 @@ let get_cache_result ~mode hash =
let set_cache_result ~mode hash prover result =
match mode with
| NoCache | Replay | Offline -> ()
- | Rebuild | Update | Markup ->
+ | Rebuild | Update | Cleanup ->
let dir = Wp_parameters.get_session_dir "cache" in
- let file = Printf.sprintf "%s/%s.json" dir (Lazy.force hash) in
+ let hash = Lazy.force hash in
+ let file = Printf.sprintf "%s/%s.json" dir hash in
try
+ mark_cache ~mode hash ;
ProofScript.json_of_result (VCS.Why3 prover) result
|> Json.save_file file
with err ->
@@ -1235,8 +1275,9 @@ let prove ?timeout ?steplimit ~prover wpo =
| Offline ->
let hash = task_hash wpo drv prover task in
let result = get_cache_result ~mode hash |> VCS.cached in
+ if VCS.is_verdict result then incr hits else incr miss ;
Task.return result
- | Update | Replay | Rebuild | Markup ->
+ | Update | Replay | Rebuild | Cleanup ->
let hash = task_hash wpo drv prover task in
let result =
get_cache_result ~mode hash
@@ -1245,7 +1286,7 @@ let prove ?timeout ?steplimit ~prover wpo =
then
begin
incr hits ;
- if mode = Markup then
+ if mode = Cleanup then
set_cache_result ~mode hash prover result ;
Task.return result
end
diff --git a/src/plugins/wp/ProverWhy3.mli b/src/plugins/wp/ProverWhy3.mli
index 4beeea60d2b11969b2e908db04079f6b13eb532b..70df0ed53b72d95ed503b1ee6a8f1766aa0d1977 100644
--- a/src/plugins/wp/ProverWhy3.mli
+++ b/src/plugins/wp/ProverWhy3.mli
@@ -30,11 +30,14 @@ 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
+type mode = NoCache | Update | Replay | Rebuild | Offline | Cleanup
val get_mode : unit -> mode
val reset : unit -> unit (** Reset cache statistics *)
val get_hits : unit -> int
val get_miss : unit -> int
+val get_removed : unit -> int
+
+val cleanup_cache : mode:mode -> unit
(**************************************************************************)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 25ae43c9da7f7bca2bed0a934d270e4f89814ccf..109e5141899b2d6cd96d18d673642fed92ed2c64 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -435,47 +435,6 @@ 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
@@ -496,11 +455,61 @@ let do_report_scheduled () =
let do_list_scheduled_result () =
begin
- do_report_cache_usage () ;
do_report_scheduled () ;
clear_scheduled () ;
end
+(* ------------------------------------------------------------------------ *)
+(* --- Caching --- *)
+(* ------------------------------------------------------------------------ *)
+
+let dkey_cache = Wp_parameters.register_category "cache"
+
+let do_report_cache_usage mode =
+ let hits = ProverWhy3.get_hits () in
+ let miss = ProverWhy3.get_miss () in
+ let removed = ProverWhy3.get_removed () in
+ if hits <= 0 && miss <= 0 then
+ Wp_parameters.result "[Cache] not used"
+ else
+ 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.Cleanup ->
+ pp_cache fmt hits "found" ;
+ pp_cache fmt miss "missed" ;
+ pp_cache fmt removed "removed" ;
+ Format.pp_print_newline fmt () ;
+ | ProverWhy3.Rebuild ->
+ pp_cache fmt (hits+miss) "updated" ;
+ Format.pp_print_newline fmt () ;
+ end
+
+let do_cache_cleanup () =
+ begin
+ let mode = ProverWhy3.get_mode () in
+ ProverWhy3.cleanup_cache ~mode ;
+ if Wp_parameters.has_dkey dkey_cache
+ then do_report_cache_usage mode ;
+ end
+
(* ------------------------------------------------------------------------ *)
(* --- Proving --- *)
(* ------------------------------------------------------------------------ *)
@@ -672,6 +681,7 @@ let do_wp_proofs_iter iter =
begin
if spawned then do_list_scheduled iter ;
spawn_wp_proofs_iter ~mode iter ;
+ do_cache_cleanup () ;
if spawned then
begin
do_list_scheduled_result () ;