diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 7fdecae8316b409d5dc49098688c2cf5cd52f1a9..b8846ff518e13dabd06f7308f3a52e79894038c6 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1449,6 +1449,8 @@ src/plugins/wp/.gitignore: .ignore
src/plugins/wp/.ocp-indent: .ignore
src/plugins/wp/Auto.ml: CEA_WP
src/plugins/wp/Auto.mli: CEA_WP
+src/plugins/wp/Cache.ml: CEA_WP
+src/plugins/wp/Cache.mli: CEA_WP
src/plugins/wp/Cfloat.ml: CEA_WP
src/plugins/wp/Cfloat.mli: CEA_WP
src/plugins/wp/Changelog: .ignore
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
new file mode 100644
index 0000000000000000000000000000000000000000..bf270c742cf6c2483c8d1da7b6d01043bd06b09a
--- /dev/null
+++ b/src/plugins/wp/Cache.ml
@@ -0,0 +1,269 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Cache Management --- *)
+(* -------------------------------------------------------------------------- *)
+
+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, never to be reset since cleanup is performed at exit *)
+
+let get_hits () = !hits
+let get_miss () = !miss
+let get_removed () = !removed
+
+let mark_cache ~mode hash =
+ if mode = Cleanup || !Fc_config.is_gui then Hashtbl.replace cleanup hash ()
+
+module CACHEDIR = WpContext.StaticGenerator(Datatype.Unit)
+ (struct
+ type key = unit
+ type data = Filepath.Normalized.t
+ let name = "Wp.Cache.dir"
+ let compile () =
+ try
+ if not (Wp_parameters.CacheEnv.get()) then
+ raise Not_found ;
+ let gdir = Sys.getenv "FRAMAC_WP_CACHEDIR" in
+ if gdir = "" then raise Not_found ;
+ Filepath.Normalized.of_string gdir
+ with Not_found ->
+ try
+ let gdir = Wp_parameters.CacheDir.get() in
+ if gdir = "" then raise Not_found ;
+ Filepath.Normalized.of_string gdir
+ with Not_found ->
+ Wp_parameters.get_session_dir ~force:false "cache"
+ end)
+
+let get_cache_dir () = (CACHEDIR.get () :> string)
+
+let has_cache_dir () =
+ try
+ if not (Wp_parameters.CacheEnv.get()) then
+ raise Not_found ;
+ Sys.getenv "FRAMAC_WP_CACHEDIR" <> ""
+ with Not_found -> Wp_parameters.CacheDir.get () <> ""
+
+let is_global_cache () = Wp_parameters.CacheDir.get () <> ""
+
+(* -------------------------------------------------------------------------- *)
+(* --- Cache Management --- *)
+(* -------------------------------------------------------------------------- *)
+
+let parse_mode ~origin ~fallback = function
+ | "none" -> NoCache
+ | "update" -> Update
+ | "replay" -> Replay
+ | "rebuild" -> Rebuild
+ | "offline" -> Offline
+ | "cleanup" -> Cleanup
+ | "" -> raise Not_found
+ | m ->
+ Wp_parameters.warning ~current:false
+ "Unknown %s mode %S (use %s instead)" origin m fallback ;
+ raise Not_found
+
+let mode_name = function
+ | NoCache -> "none"
+ | Update -> "update"
+ | Replay -> "replay"
+ | Rebuild -> "rebuild"
+ | Offline -> "offline"
+ | Cleanup -> "cleanup"
+
+module MODE = WpContext.StaticGenerator(Datatype.Unit)
+ (struct
+ type key = unit
+ type data = mode
+ let name = "Wp.Cache.mode"
+ let compile () =
+ try
+ if not (Wp_parameters.CacheEnv.get()) then
+ raise Not_found ;
+ let origin = "FRAMAC_WP_CACHE" in
+ parse_mode ~origin ~fallback:"-wp-cache" (Sys.getenv origin)
+ with Not_found ->
+ try
+ let mode = Wp_parameters.Cache.get() in
+ parse_mode ~origin:"-wp-cache" ~fallback:"none" mode
+ with Not_found ->
+ if Wp_parameters.has_session () || has_cache_dir ()
+ then Update else NoCache
+ end)
+
+let get_mode = MODE.get
+let set_mode m = MODE.clear () ; Wp_parameters.Cache.set (mode_name m)
+
+let task_hash wpo drv prover task =
+ lazy
+ begin
+ let file = Wpo.DISK.file_goal
+ ~pid:wpo.Wpo.po_pid
+ ~model:wpo.Wpo.po_model
+ ~prover:(VCS.Why3 prover) in
+ let _ = Command.print_file file
+ begin fun fmt ->
+ Format.fprintf fmt "(* WP Task for Prover %s *)@\n"
+ (Why3Provers.print_why3 prover) ;
+ Why3.Driver.print_task_prepared drv fmt task ;
+ end
+ in Digest.file file |> Digest.to_hex
+ end
+
+let time_fits time = function
+ | None | Some 0 -> true
+ | Some limit -> time <= float limit
+
+let steps_fits steps = function
+ | None | Some 0 -> true
+ | Some limit -> steps <= limit
+
+let time_seized time = function
+ | None | Some 0 -> false
+ | Some limit -> float limit <= time
+
+let steps_seized steps steplimit =
+ steps <> 0 &&
+ match steplimit with
+ | None | Some 0 -> false
+ | Some limit -> limit <= steps
+
+let promote ~timeout ~steplimit (res : VCS.result) =
+ match res.verdict with
+ | VCS.NoResult | VCS.Computing _ -> VCS.no_result
+ | VCS.Failed -> res
+ | VCS.Invalid | VCS.Valid | VCS.Unknown ->
+ if not (steps_fits res.prover_steps steplimit) then
+ { res with verdict = Stepout }
+ else
+ if not (time_fits res.prover_time timeout) then
+ { res with verdict = Timeout }
+ else res
+ | VCS.Timeout | VCS.Stepout ->
+ if steps_seized res.prover_steps steplimit then
+ { res with verdict = Stepout }
+ else
+ if time_seized res.prover_time timeout then
+ { res with verdict = Timeout }
+ else (* can be run a longer time or widely *)
+ VCS.no_result
+
+let get_cache_result ~mode hash =
+ match mode with
+ | NoCache | Rebuild -> VCS.no_result
+ | Update | Cleanup | Replay | Offline ->
+ let dir = get_cache_dir () in
+ if not (Sys.file_exists dir && Sys.is_directory dir) then
+ VCS.no_result
+ else
+ 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.warning ~current:false ~once:true
+ "invalid cache entry (%s)" (Printexc.to_string err) ;
+ VCS.no_result
+
+let set_cache_result ~mode hash prover result =
+ match mode with
+ | NoCache | Replay | Offline -> ()
+ | Rebuild | Update | Cleanup ->
+ let dir = CACHEDIR.get () in
+ let hash = Lazy.force hash in
+ let file = Printf.sprintf "%s/%s.json" (dir :> string) hash in
+ try
+ mark_cache ~mode hash ;
+ ProofScript.json_of_result (VCS.Why3 prover) result
+ |> Json.save_file file
+ with err ->
+ Wp_parameters.warning ~current:false ~once:true
+ "can not update cache (%s)" (Printexc.to_string err)
+
+let cleanup_cache () =
+ let mode = get_mode () in
+ if mode = Cleanup && (!hits > 0 || !miss > 0) then
+ let dir = get_cache_dir () in
+ if is_global_cache () then
+ Wp_parameters.warning ~current:false ~once:true
+ "Cleanup mode deactivated with global cache."
+ else
+ try
+ if Sys.file_exists dir && 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.warning ~current:false
+ "Can not cleanup cache (%s)" (Printexc.to_string exn)
+
+type runner =
+ timeout:int option -> steplimit:int option ->
+ Why3.Driver.driver -> Why3Provers.t -> Why3.Task.task ->
+ VCS.result Task.task
+
+let get_result wpo runner ~timeout ~steplimit drv prover task =
+ let mode = get_mode () in
+ match mode with
+ | NoCache ->
+ runner ~timeout ~steplimit drv prover task
+ | 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 | Cleanup ->
+ let hash = task_hash wpo drv prover task in
+ let result =
+ get_cache_result ~mode hash
+ |> promote ~timeout ~steplimit |> VCS.cached in
+ if VCS.is_verdict result
+ then
+ begin
+ incr hits ;
+ Task.return result
+ end
+ else
+ Task.finally
+ (runner ~timeout ~steplimit drv prover task)
+ begin function
+ | Task.Result result when VCS.is_verdict result ->
+ incr miss ;
+ set_cache_result ~mode hash prover result
+ | _ -> ()
+ end
diff --git a/src/plugins/wp/Cache.mli b/src/plugins/wp/Cache.mli
new file mode 100644
index 0000000000000000000000000000000000000000..53d335826478794c4b2b4907cc90ff668c187da1
--- /dev/null
+++ b/src/plugins/wp/Cache.mli
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+type mode = NoCache | Update | Replay | Rebuild | Offline | Cleanup
+
+val set_mode : mode -> unit
+val get_mode : unit -> mode
+val get_hits : unit -> int
+val get_miss : unit -> int
+val get_removed : unit -> int
+
+val cleanup_cache : unit -> unit
+
+type runner =
+ timeout:int option -> steplimit:int option ->
+ Why3.Driver.driver -> Why3Provers.t -> Why3.Task.task ->
+ VCS.result Task.task
+
+val get_result: Wpo.t -> runner -> runner
diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index 75cda8679784d9b0c40266bd0200fd7cdb72c8c1..b24a0ca165b0113a6afb5761142d6c86f4eb22f2 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/src/plugins/wp/GuiPanel.ml
@@ -224,14 +224,14 @@ let wp_panel
hbox#pack prover_cfg#coerce ;
Gtk_form.menu [
- "No Cache" , ProverWhy3.NoCache ;
- "Update" , ProverWhy3.Update ;
- "Cleanup" , ProverWhy3.Cleanup ;
- "Rebuild" , ProverWhy3.Rebuild ;
- "Replay" , ProverWhy3.Replay ;
- "Offline" , ProverWhy3.Offline ;
+ "No Cache" , Cache.NoCache ;
+ "Update" , Cache.Update ;
+ "Cleanup" , Cache.Cleanup ;
+ "Rebuild" , Cache.Rebuild ;
+ "Replay" , Cache.Replay ;
+ "Offline" , Cache.Offline ;
] ~packing:hbox#pack ~tooltip:"Proof Cache Mode"
- ProverWhy3.get_mode ProverWhy3.set_mode demon ;
+ Cache.get_mode Cache.set_mode demon ;
let pbox = GPack.hbox ~packing ~show:false () in
let progress = GRange.progress_bar ~packing:(pbox#pack ~expand:true ~fill:true) () in
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index c16073091edcdfc27feac50c7b1d236f141e9f46..5f1dd450bceb6d63e9922b879c7cbadff69dc749 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -93,7 +93,7 @@ PLUGIN_CMO:= \
TacCongruence TacOverflow Auto \
ProofSession ProofScript ProofEngine \
ProverTask ProverErgo ProverCoq \
- filter_axioms ProverWhy3 \
+ filter_axioms Cache ProverWhy3 \
driver prover ProverSearch ProverScript \
Generator Factory \
calculus cfgDump cfgWP \
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 07b0ef0257e942702a812436a6d212057a865a3b..2d9a6ce177b2444d77f578b6d09607cfc66524be 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1198,7 +1198,7 @@ let ping_prover_call p =
VCS.pp_result r;
Task.Return (Task.Result r)
-let call_prover ~timeout ~steplimit drv prover prover_config task =
+let call_prover prover_config ~timeout ~steplimit drv prover task =
let steps = match steplimit with Some 0 -> None | _ -> steplimit in
let limit =
let def = Why3.Call_provers.empty_limit in
@@ -1230,217 +1230,6 @@ let call_prover ~timeout ~steplimit drv prover prover_config task =
in
Task.async ping
-(* -------------------------------------------------------------------------- *)
-(* --- Cache Management --- *)
-(* -------------------------------------------------------------------------- *)
-
-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, never to be reset since cleanup is performed at exit *)
-
-let get_hits () = !hits
-let get_miss () = !miss
-let get_removed () = !removed
-
-let mark_cache ~mode hash =
- if mode = Cleanup || !Fc_config.is_gui then Hashtbl.replace cleanup hash ()
-
-module CACHEDIR = WpContext.StaticGenerator(Datatype.Unit)
- (struct
- type key = unit
- type data = Filepath.Normalized.t
- let name = "Wp.Cache.dir"
- let compile () =
- try
- if not (Wp_parameters.CacheEnv.get()) then
- raise Not_found ;
- let gdir = Sys.getenv "FRAMAC_WP_CACHEDIR" in
- if gdir = "" then raise Not_found ;
- Filepath.Normalized.of_string gdir
- with Not_found ->
- try
- let gdir = Wp_parameters.CacheDir.get() in
- if gdir = "" then raise Not_found ;
- Filepath.Normalized.of_string gdir
- with Not_found ->
- Wp_parameters.get_session_dir ~force:false "cache"
- end)
-
-let get_cache_dir () = (CACHEDIR.get () :> string)
-
-let has_cache_dir () =
- try
- if not (Wp_parameters.CacheEnv.get()) then
- raise Not_found ;
- Sys.getenv "FRAMAC_WP_CACHEDIR" <> ""
- with Not_found -> Wp_parameters.CacheDir.get () <> ""
-
-let is_global_cache () = Wp_parameters.CacheDir.get () <> ""
-
-let cleanup_cache ~mode =
- if mode = Cleanup && (!hits > 0 || !miss > 0) then
- let dir = get_cache_dir () in
- if is_global_cache () then
- Wp_parameters.warning ~current:false ~once:true
- "Cleanup mode deactivated with global cache."
- else
- try
- if Sys.file_exists dir && 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.warning ~current:false
- "Can not cleanup cache (%s)" (Printexc.to_string exn)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Cache Management --- *)
-(* -------------------------------------------------------------------------- *)
-
-let parse_mode ~origin ~fallback = function
- | "none" -> NoCache
- | "update" -> Update
- | "replay" -> Replay
- | "rebuild" -> Rebuild
- | "offline" -> Offline
- | "cleanup" -> Cleanup
- | "" -> raise Not_found
- | m ->
- Wp_parameters.warning ~current:false
- "Unknown %s mode %S (use %s instead)" origin m fallback ;
- raise Not_found
-
-let mode_name = function
- | NoCache -> "none"
- | Update -> "update"
- | Replay -> "replay"
- | Rebuild -> "rebuild"
- | Offline -> "offline"
- | Cleanup -> "cleanup"
-
-module MODE = WpContext.StaticGenerator(Datatype.Unit)
- (struct
- type key = unit
- type data = mode
- let name = "Wp.Cache.mode"
- let compile () =
- try
- if not (Wp_parameters.CacheEnv.get()) then
- raise Not_found ;
- let origin = "FRAMAC_WP_CACHE" in
- parse_mode ~origin ~fallback:"-wp-cache" (Sys.getenv origin)
- with Not_found ->
- try
- let mode = Wp_parameters.Cache.get() in
- parse_mode ~origin:"-wp-cache" ~fallback:"none" mode
- with Not_found ->
- if Wp_parameters.has_session () || has_cache_dir ()
- then Update else NoCache
- end)
-
-let get_mode = MODE.get
-let set_mode m = MODE.clear () ; Wp_parameters.Cache.set (mode_name m)
-
-let task_hash wpo drv prover task =
- lazy
- begin
- let file = Wpo.DISK.file_goal
- ~pid:wpo.Wpo.po_pid
- ~model:wpo.Wpo.po_model
- ~prover:(VCS.Why3 prover) in
- let _ = Command.print_file file
- begin fun fmt ->
- Format.fprintf fmt "(* WP Task for Prover %s *)@\n"
- (Why3Provers.print_why3 prover) ;
- Why3.Driver.print_task_prepared drv fmt task ;
- end
- in Digest.file file |> Digest.to_hex
- end
-
-let time_fits time = function
- | None | Some 0 -> true
- | Some limit -> time <= float limit
-
-let steps_fits steps = function
- | None | Some 0 -> true
- | Some limit -> steps <= limit
-
-let time_seized time = function
- | None | Some 0 -> false
- | Some limit -> float limit <= time
-
-let steps_seized steps steplimit =
- steps <> 0 &&
- match steplimit with
- | None | Some 0 -> false
- | Some limit -> limit <= steps
-
-let promote ~timeout ~steplimit (res : VCS.result) =
- match res.verdict with
- | VCS.NoResult | VCS.Computing _ -> VCS.no_result
- | VCS.Failed -> res
- | VCS.Invalid | VCS.Valid | VCS.Unknown ->
- if not (steps_fits res.prover_steps steplimit) then
- { res with verdict = Stepout }
- else
- if not (time_fits res.prover_time timeout) then
- { res with verdict = Timeout }
- else res
- | VCS.Timeout | VCS.Stepout ->
- if steps_seized res.prover_steps steplimit then
- { res with verdict = Stepout }
- else
- if time_seized res.prover_time timeout then
- { res with verdict = Timeout }
- else (* can be run a longer time or widely *)
- VCS.no_result
-
-let get_cache_result ~mode hash =
- match mode with
- | NoCache | Rebuild -> VCS.no_result
- | Update | Cleanup | Replay | Offline ->
- let dir = get_cache_dir () in
- if not (Sys.file_exists dir && Sys.is_directory dir) then
- VCS.no_result
- else
- 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.warning ~current:false ~once:true
- "invalid cache entry (%s)" (Printexc.to_string err) ;
- VCS.no_result
-
-let set_cache_result ~mode hash prover result =
- match mode with
- | NoCache | Replay | Offline -> ()
- | Rebuild | Update | Cleanup ->
- let dir = CACHEDIR.get () in
- let hash = Lazy.force hash in
- let file = Printf.sprintf "%s/%s.json" (dir :> string) hash in
- try
- mark_cache ~mode hash ;
- ProofScript.json_of_result (VCS.Why3 prover) result
- |> Json.save_file file
- with err ->
- Wp_parameters.warning ~current:false ~once:true
- "can not update cache (%s)" (Printexc.to_string err)
-
let is_trivial (t : Why3.Task.task) =
let goal = Why3.Task.task_goal_fmla t in
Why3.Term.t_equal goal Why3.Term.t_true
@@ -1462,35 +1251,8 @@ let build_proof_task ?timeout ?steplimit ~prover wpo () =
if is_trivial task then
Task.return VCS.valid
else
- let mode = get_mode () in
- match mode with
- | NoCache ->
- call_prover ~timeout ~steplimit drv prover config task
- | 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 | Cleanup ->
- let hash = task_hash wpo drv prover task in
- let result =
- get_cache_result ~mode hash
- |> promote ~timeout ~steplimit |> VCS.cached in
- if VCS.is_verdict result
- then
- begin
- incr hits ;
- Task.return result
- end
- else
- Task.finally
- (call_prover ~timeout ~steplimit drv prover config task)
- begin function
- | Task.Result result when VCS.is_verdict result ->
- incr miss ;
- set_cache_result ~mode hash prover result
- | _ -> ()
- end
+ Cache.get_result wpo (call_prover config)
+ ~timeout ~steplimit drv prover task
with exn ->
if Wp_parameters.has_dkey dkey_api then
Wp_parameters.fatal "[Why3 Error] %a@\n%s"
diff --git a/src/plugins/wp/ProverWhy3.mli b/src/plugins/wp/ProverWhy3.mli
index 487eb531c73b2bb1c3906af61d60dcc330ac7a93..ea029e0804bc7aba4a8f25d66b18a043dd0804ea 100644
--- a/src/plugins/wp/ProverWhy3.mli
+++ b/src/plugins/wp/ProverWhy3.mli
@@ -30,14 +30,4 @@ 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 | Cleanup
-
-val set_mode : mode -> unit
-val get_mode : unit -> mode
-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 ccba10093be6cb8ecd8219de1164529489d2545c..443f11f76594a9e5a933d4eba40a7ba64481e1b6 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -309,8 +309,8 @@ let do_report_cache_usage mode =
not (Wp_parameters.has_dkey dkey_shell) &&
not (Wp_parameters.has_dkey VCS.dkey_no_cache_info)
then
- let hits = ProverWhy3.get_hits () in
- let miss = ProverWhy3.get_miss () in
+ let hits = Cache.get_hits () in
+ let miss = Cache.get_miss () in
if hits <= 0 && miss <= 0 then
Wp_parameters.result "[Cache] not used"
else
@@ -321,20 +321,20 @@ let do_report_cache_usage mode =
if n > 0 then
( Format.fprintf fmt "%s%s:%d" !sep job n ; sep := ", " ) in
match mode with
- | ProverWhy3.NoCache -> ()
- | ProverWhy3.Replay ->
+ | Cache.NoCache -> ()
+ | Cache.Replay ->
pp_cache fmt hits "found" ;
pp_cache fmt miss "missed" ;
Format.pp_print_newline fmt () ;
- | ProverWhy3.Offline ->
+ | Cache.Offline ->
pp_cache fmt hits "found" ;
pp_cache fmt miss "failed" ;
Format.pp_print_newline fmt () ;
- | ProverWhy3.Update | ProverWhy3.Cleanup ->
+ | Cache.Update | Cache.Cleanup ->
pp_cache fmt hits "found" ;
pp_cache fmt miss "updated" ;
Format.pp_print_newline fmt () ;
- | ProverWhy3.Rebuild ->
+ | Cache.Rebuild ->
pp_cache fmt hits "replaced" ;
pp_cache fmt miss "updated" ;
Format.pp_print_newline fmt () ;
@@ -519,8 +519,8 @@ let do_report_scheduled () =
if !scheduled > 0 then
begin
let proved = GOALS.cardinal !proved in
- let mode = ProverWhy3.get_mode () in
- if mode <> ProverWhy3.NoCache then do_report_cache_usage mode ;
+ let mode = Cache.get_mode () in
+ if mode <> Cache.NoCache then do_report_cache_usage mode ;
Wp_parameters.result "%t"
begin fun fmt ->
Format.fprintf fmt "Proved goals: %4d / %d@\n" proved !scheduled ;
@@ -736,9 +736,8 @@ let do_wp_proofs_for goals = do_wp_proofs_iter (fun f -> Bag.iter f goals)
(* registered at frama-c (normal) exit *)
let do_cache_cleanup () =
begin
- let mode = ProverWhy3.get_mode () in
- ProverWhy3.cleanup_cache ~mode ;
- let removed = ProverWhy3.get_removed () in
+ Cache.cleanup_cache () ;
+ let removed = Cache.get_removed () in
if removed > 0 &&
not (Wp_parameters.has_dkey dkey_shell) &&
not (Wp_parameters.has_dkey VCS.dkey_no_cache_info)