diff --git a/bin/wp-qualif.sh b/bin/wp-qualif.sh
index 26d743608360c8676a6801e0b70459332e64caea..ae239fbadbe2bcd440bac1a4cd149dcc391e1d13 100644
--- a/bin/wp-qualif.sh
+++ b/bin/wp-qualif.sh
@@ -1,2 +1,2 @@
export FRAMAC_WP_CACHE=update
-export FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE)
+export FRAMAC_WP_CACHEDIR=$WP_QUALIF_CACHE
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index a8437b5bd42c4ad9d51a59deff3c1dbac6e31fa2..0410e84facbd9940996a8d375593a164a05f0622 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1451,6 +1451,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/report/tests/report/classify.c b/src/plugins/report/tests/report/classify.c
index 050fe0fd4bcd1497c4d4cab535dcece5fe5d90b6..3ee8df0b80ad14afc530a3013f7067df128c4ec8 100644
--- a/src/plugins/report/tests/report/classify.c
+++ b/src/plugins/report/tests/report/classify.c
@@ -1,5 +1,5 @@
/* run.config
- CMD: @frama-c@ -kernel-warn-key=annot-error=active -no-autoload-plugins -load-module wp,report -report-output @PTEST_RESULT@/classified.@PTEST_NUMBER@.json -wp -wp-msg-key no-time-info
+ CMD: @frama-c@ -kernel-warn-key=annot-error=active -no-autoload-plugins -load-module wp,report -report-output @PTEST_RESULT@/classified.@PTEST_NUMBER@.json -wp -wp-msg-key shell
LOG: classified.@PTEST_NUMBER@.json
OPT: -wp-prover qed -report-unclassified-untried REVIEW -then -report-classify
LOG: classified.@PTEST_NUMBER@.json
diff --git a/src/plugins/report/tests/report/oracle/classify.0.res.oracle b/src/plugins/report/tests/report/oracle/classify.0.res.oracle
index 2d9f271aea5752a9bbc3037c9c42b90aac05b38e..e19a301288f31daaee5a84de423e34be38e9a539 100644
--- a/src/plugins/report/tests/report/oracle/classify.0.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.0.res.oracle
@@ -1,3 +1,4 @@
+# frama-c -wp [...]
[kernel] Parsing tests/report/classify.c (with preprocessing)
[kernel:annot-error] tests/report/classify.c:27: Warning:
unbound logic variable ignored. Ignoring code annotation
diff --git a/src/plugins/report/tests/report/oracle/classify.1.res.oracle b/src/plugins/report/tests/report/oracle/classify.1.res.oracle
index 9266851bb999c61aaf138053b920459d475fb73d..442bb8d3b8ce3649bef6678accea16e983d104d3 100644
--- a/src/plugins/report/tests/report/oracle/classify.1.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.1.res.oracle
@@ -1,4 +1,5 @@
[report] Monitoring events
+# frama-c -wp [...]
[kernel] Parsing tests/report/classify.c (with preprocessing)
[kernel:annot-error] tests/report/classify.c:27: Warning:
unbound logic variable ignored. Ignoring code annotation
diff --git a/src/plugins/report/tests/report/oracle/classify.2.res.oracle b/src/plugins/report/tests/report/oracle/classify.2.res.oracle
index 8e0f90163361e74984979077ddaa1a85702be12e..974d340981d9d583ddecf5a335ebfbe03c3002a9 100644
--- a/src/plugins/report/tests/report/oracle/classify.2.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.2.res.oracle
@@ -1,4 +1,5 @@
[report] Monitoring events
+# frama-c -wp [...]
[kernel] Parsing tests/report/classify.c (with preprocessing)
[kernel:annot-error] tests/report/classify.c:27: Warning:
unbound logic variable ignored. Ignoring code annotation
diff --git a/src/plugins/report/tests/report/oracle/classify.3.res.oracle b/src/plugins/report/tests/report/oracle/classify.3.res.oracle
index 5fab349a04e38664af8b21b15febbb573588c6c7..91bb8b30a52c6ab24b75cf1c04a53d3cc15534d7 100644
--- a/src/plugins/report/tests/report/oracle/classify.3.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.3.res.oracle
@@ -1,5 +1,6 @@
[report] Monitoring events
[report] Loading 'tests/report/classify.json'
+# frama-c -wp [...]
[kernel] Parsing tests/report/classify.c (with preprocessing)
[kernel:annot-error] tests/report/classify.c:27: Warning:
unbound logic variable ignored. Ignoring code annotation
diff --git a/src/plugins/report/tests/report/oracle/classify.4.res.oracle b/src/plugins/report/tests/report/oracle/classify.4.res.oracle
index 4fe970e76ac2d9a5d2c965d22a6f185ebaeb2f95..ab13ead4ecb87d3507d41418ee453bf3a16f4fde 100644
--- a/src/plugins/report/tests/report/oracle/classify.4.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.4.res.oracle
@@ -1,5 +1,6 @@
[report] Monitoring events
[report] Loading 'tests/report/classify.json'
+# frama-c -wp [...]
[kernel] Parsing tests/report/classify.c (with preprocessing)
[kernel:annot-error] tests/report/classify.c:27: Warning:
unbound logic variable ignored. Ignoring code annotation
diff --git a/src/plugins/report/tests/report/oracle/classify.5.res.oracle b/src/plugins/report/tests/report/oracle/classify.5.res.oracle
index fe7d84466c0e64effca171af82723994cecf7759..bab75d5f591e203476328215f076bf5d0ad61a7a 100644
--- a/src/plugins/report/tests/report/oracle/classify.5.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.5.res.oracle
@@ -1,5 +1,6 @@
[report] Monitoring events
[report] Loading 'tests/report/classify.json'
+# frama-c -wp [...]
[kernel] Parsing tests/report/classify.c (with preprocessing)
[kernel:annot-error] tests/report/classify.c:27: Warning:
unbound logic variable ignored. Ignoring code annotation
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
new file mode 100644
index 0000000000000000000000000000000000000000..d08034e93ca7bd84a44ba06bb4d5b340ad474e75
--- /dev/null
+++ b/src/plugins/wp/Cache.ml
@@ -0,0 +1,288 @@
+(**************************************************************************)
+(* *)
+(* 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_dir () = (CACHEDIR.get () :> string)
+
+let is_session_dir path =
+ 0 = Filepath.Normalized.compare
+ path (Wp_parameters.get_session_dir ~force:false "cache")
+
+let get_usable_dir ?(make=false) () =
+ let path = CACHEDIR.get () in
+ let parents = is_session_dir path in
+ let path = (path :> string) in
+ if not (Sys.file_exists path) && make then
+ Extlib.mkdir ~parents path 0o755 ;
+ if not (Sys.is_directory path) then begin
+ Wp_parameters.warning ~current:false ~once:true
+ "Cache path is not a directory" ;
+ raise Not_found
+ end ;
+ path
+
+let has_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_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 ->
+ try
+ let dir = get_usable_dir ~make:true () 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.warning ~current:false ~once:true
+ "invalid cache entry (%s)" (Printexc.to_string err) ;
+ VCS.no_result
+ with Not_found -> VCS.no_result
+
+let set_cache_result ~mode hash prover result =
+ match mode with
+ | NoCache | Replay | Offline -> ()
+ | Rebuild | Update | Cleanup ->
+ let hash = Lazy.force hash in
+ try
+ let dir = get_usable_dir ~make:true () in
+ let file = Printf.sprintf "%s/%s.json" dir hash in
+ 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
+ try
+ let dir = get_usable_dir () in
+ if is_global_cache () then
+ Wp_parameters.warning ~current:false ~once:true
+ "Cleanup mode deactivated with global cache."
+ else
+ 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)
+ | Not_found ->
+ Wp_parameters.warning ~current:false
+ "Cannot cleanup cache"
+
+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..39af510514147e3d227b1a69b7b02ca38789e2b9
--- /dev/null
+++ b/src/plugins/wp/Cache.mli
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(* *)
+(* 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 get_dir : unit -> string
+
+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/Changelog b/src/plugins/wp/Changelog
index 33d00e5c2bc3331d2648273f5dd6979ecebd4099..7f362c7148689ecbbdda1696585c2a3fd53b0e65 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,7 +24,10 @@
Plugin WP <next-release>
#########################
-- WP [2020-06-12] Supports the \initialized ACSL predicate
+- WP [2020-07-06] Removed debug keys "no-xxx-info" (subsumed by "shell")
+- WP [2020-07-06] Option -wp-cache-env now defaults to false
+- WP [2020-07-06] New option -wp-cache-print
+- WP [2020-06-12] Supports the \initialized ACSL predicate
#########################
Plugin WP 21.1 (Scandium)
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..dc8b2c99ecea03e5415df621ca826a3db8c40aeb 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 \
@@ -169,15 +169,23 @@ $(Wp_DIR)/Makefile: $(WP_CONFIGURE_MAKEFILE)
WP_QUALIF_CACHE?=$(abspath $(Wp_DIR)/../wp-cache)
WP_QUALIF_ENTRIES=git -C $(WP_QUALIF_CACHE) ls-files --others --exclude-standard | wc -l
+WP_CHECKOUT_CACHE=\
+ echo "[CACHE] repo: $(WP_QUALIF_CACHE)" && \
+ git -C $(WP_QUALIF_CACHE) checkout master
+
wp-qualif: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
+ $(WP_CHECKOUT_CACHE)
FRAMAC_WP_CACHE=replay \
FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE) \
./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
-wp-qualif-update: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
- @echo "[CACHE] pull cache"
- @echo "[CACHE] $(WP_QUALIF_CACHE)"
+WP_PULL_CACHE=\
+ echo "[CACHE] pull cache" && \
+ $(WP_CHECKOUT_CACHE) && \
git -C $(WP_QUALIF_CACHE) pull --rebase --prune
+
+wp-qualif-update: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
+ $(WP_PULL_CACHE)
@echo "[TESTS] updating wp-qualif"
FRAMAC_WP_CACHE=update \
FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE) \
@@ -187,9 +195,7 @@ wp-qualif-update: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
@echo "New entries: `$(WP_QUALIF_ENTRIES)`"
wp-qualif-upgrade: ./bin/toplevel.opt ./bin/ptests.opt
- @echo "[CACHE] pull cache"
- @echo "[CACHE] repo: $(WP_QUALIF_CACHE)"
- git -C $(WP_QUALIF_CACHE) pull --rebase --prune
+ $(WP_PULL_CACHE)
@echo "[TESTS] upgrading wp-qualif (cache & scripts)"
FRAMAC_WP_CACHE=update \
FRAMAC_WP_SCRIPT=update \
@@ -201,14 +207,14 @@ wp-qualif-upgrade: ./bin/toplevel.opt ./bin/ptests.opt
wp-qualif-push:
@echo "[CACHE] pushing updates"
- @echo "[CACHE] repo: $(WP_QUALIF_CACHE)"
+ $(WP_CHECKOUT_CACHE)
git -C $(WP_QUALIF_CACHE) add -A
git -C $(WP_QUALIF_CACHE) commit -m "[wp] cache updates"
git -C $(WP_QUALIF_CACHE) push -f
wp-qualif-status:
@echo "[CACHE] status"
- @echo "[CACHE] repo: $(WP_QUALIF_CACHE)"
+ $(WP_CHECKOUT_CACHE)
git -C $(WP_QUALIF_CACHE) status -s -b -u no
@echo "New entries: `$(WP_QUALIF_ENTRIES)`"
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/VCS.ml b/src/plugins/wp/VCS.ml
index 5d8d33d6c3742de548535a7581d8a835674097b1..c92b0ca59fb985c1a5b76353ce52de64594e1ba7 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -24,11 +24,7 @@
(* --- Prover Results --- *)
(* -------------------------------------------------------------------------- *)
-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"
+let dkey_shell = Wp_parameters.register_category "shell"
type prover =
| Why3 of Why3Provers.t (* Prover via WHY *)
@@ -91,7 +87,7 @@ let name_of_prover = function
let title_of_prover = function
| Why3 s ->
- if Wp_parameters.has_dkey dkey_success_only
+ if Wp_parameters.has_dkey dkey_shell
then Why3Provers.name s
else Why3Provers.title s
| NativeAltErgo -> "Alt-Ergo (native)"
@@ -298,15 +294,15 @@ let perfo dkey = not (Wp_parameters.has_dkey dkey)
let pp_perf fmt r =
begin
let t = r.solver_time in
- if t > Rformat.epsilon && perfo dkey_no_time_info
+ if t > Rformat.epsilon && perfo dkey_shell
then Format.fprintf fmt " (Qed:%a)" Rformat.pp_time t ;
let t = r.prover_time in
- if t > Rformat.epsilon && perfo dkey_no_time_info
+ if t > Rformat.epsilon && perfo dkey_shell
then Format.fprintf fmt " (%a)" Rformat.pp_time t ;
let s = r.prover_steps in
- if s > 0 && perfo dkey_no_step_info
+ if s > 0 && perfo dkey_shell
then Format.fprintf fmt " (%d)" s ;
- if r.cached && perfo dkey_no_cache_info
+ if r.cached && perfo dkey_shell
then Format.fprintf fmt " (cached)" ;
end
@@ -328,13 +324,13 @@ let pp_cache_miss fmt st prover r =
| NativeAltErgo | NativeCoq -> r.verdict <> Timeout
| Why3 _ -> r.cached || r.prover_time < Rformat.epsilon
in
- if qualified then
- Format.pp_print_string fmt (if is_valid r then "Valid" else "Unsuccess")
- else
+ if not qualified && Wp_parameters.has_dkey dkey_shell then
Format.fprintf fmt "%s%a (unqualified)" st pp_perf r
+ else
+ Format.pp_print_string fmt (if is_valid r then "Valid" else "Unsuccess")
let pp_result_qualif prover fmt r =
- if Wp_parameters.has_dkey dkey_success_only then
+ if Wp_parameters.has_dkey dkey_shell then
match r.verdict with
| NoResult -> Format.pp_print_string fmt "No Result"
| Computing _ -> Format.pp_print_string fmt "Computing"
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 87b2a3fb7a726999ee54f33b9bc10d7e53f70c1f..0e869ebea1458ef899c8e8ea6ff4b563cf224644 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -126,8 +126,4 @@ val merge : result -> result -> result
val choose : result -> result -> result
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
+val dkey_shell: Wp_parameters.category
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index c8b8b89130d3bc301d2b89a9aa88880de8598c85..650b869af3ec4b4989e7e1e3333dc3833c965ceb 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1290,12 +1290,17 @@ There are different ways of using the cache, depending on your precise needs.
The main option to control cache usage is \verb+-wp-cache+, documented below:
\begin{description}
-\item[\tt -wp-session <dir>] select the directory where cached results and proof scripts
- are stored. If the local directory \verb+'.frama-c'+ already exists, the default session
- directory \verb+'.frama-c/wp'+ will be used to setup the \textsf{WP} session.
-\item[\tt -wp-cache <mode>] selects the cache mode to use with \textsf{Why-3} provers. The default mode is \verb'update'
- if a \textsf{WP} session is set, and \verb+none+ otherwise. The cache entries are stored in the session directory,
- which is \verb+./.frama-c/wp/cache+ by default.
+\item[\tt -wp-cache <mode>] selects the cache mode to use with \textsf{Why-3}
+ provers. The default mode is \verb'update' if there is \textsf{WP} session
+ available, and \verb+none+ otherwise. You can also use the environment
+ variable \texttt{FRAMAC\_WP\_CACHE} instead.
+\item[\tt -wp-cache-dir <dir>] select the directory where cached results are
+ stored. By default, the cache is store in the \textsf{WP} session
+ directory, when available.
+ You can also use the environment variable
+ \texttt{FRAMAC\_WP\_CACHEDIR} instead.
+\item[\tt -wp-cache-env] gives environment variables the precedence over command line options.
+ By default, the command line options take precedence, as usual.
\end{description}
The available cache modes are described below:
@@ -1309,7 +1314,6 @@ The available cache modes are described below:
\end{description}
When using cache with a non-\verb+offline+ mode, time and steps limits recorded in the cache are compared to the command line settings to produce meaningful and consistent results. Hence, if you provide more time or more steps from the command line than before, the prover would be run again. If you provide less or equal limits, the cache entries are reused, but \textsf{WP} still report the cached time and step limits to inform you of your previous attempts. For instance, if you have in the cache a « Valid » entry with time 12.4s and re-run it with a timeout of 5s, you will have a « Timeout » result with time 12.4s printed on the console.
-Cached usage is indicated on the standard output, unless you specify \verb+-wp-msg-key no-cache-info+.
\section{Plug-in Developer Interface}
\label{wp-api}
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index ccba10093be6cb8ecd8219de1164529489d2545c..c350f0f5779d5de2272bee29683161bf140e4290 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -24,7 +24,6 @@ open Factory
let dkey_main = Wp_parameters.register_category "main"
let dkey_raised = Wp_parameters.register_category "raised"
-let dkey_shell = Wp_parameters.register_category "shell"
let wkey_smoke = Wp_parameters.register_warn_category "smoke"
(* --------- Command Line ------------------- *)
@@ -264,20 +263,17 @@ let add_time s t =
end
let do_list_scheduled iter_on_goals =
- if not (Wp_parameters.has_dkey VCS.dkey_no_goals_info) then
- begin
- clear_scheduled () ;
- iter_on_goals
- (fun goal ->
- begin
- incr scheduled ;
- if !spy then session := GOALS.add goal !session ;
- end) ;
- match !scheduled with
- | 0 -> Wp_parameters.warning ~current:false "No goal generated"
- | 1 -> Wp_parameters.feedback "1 goal scheduled"
- | n -> Wp_parameters.feedback "%d goals scheduled" n
- end
+ clear_scheduled () ;
+ iter_on_goals
+ (fun goal ->
+ begin
+ incr scheduled ;
+ if !spy then session := GOALS.add goal !session ;
+ end) ;
+ match !scheduled with
+ | 0 -> Wp_parameters.warning ~current:false "No goal generated"
+ | 1 -> Wp_parameters.feedback "1 goal scheduled"
+ | n -> Wp_parameters.feedback "%d goals scheduled" n
let dkey_prover = Wp_parameters.register_category "prover"
@@ -306,11 +302,10 @@ let do_progress goal msg =
let do_report_cache_usage mode =
if !exercised > 0 &&
- not (Wp_parameters.has_dkey dkey_shell) &&
- not (Wp_parameters.has_dkey VCS.dkey_no_cache_info)
+ not (Wp_parameters.has_dkey VCS.dkey_shell)
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 +316,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 () ;
@@ -451,8 +446,7 @@ let do_report_time fmt s =
begin
if s.n_time > 0 &&
s.u_time > Rformat.epsilon &&
- not (Wp_parameters.has_dkey VCS.dkey_no_time_info) &&
- not (Wp_parameters.has_dkey VCS.dkey_success_only)
+ not (Wp_parameters.has_dkey VCS.dkey_shell)
then
let mean = s.a_time /. float s.n_time in
let epsilon = 0.05 *. mean in
@@ -475,14 +469,13 @@ let do_report_time fmt s =
let do_report_steps fmt s =
begin
if s.steps > 0 &&
- not (Wp_parameters.has_dkey VCS.dkey_no_step_info) &&
- not (Wp_parameters.has_dkey VCS.dkey_success_only)
+ not (Wp_parameters.has_dkey VCS.dkey_shell)
then
Format.fprintf fmt " (%d)" s.steps ;
end
let do_report_stopped fmt s =
- if Wp_parameters.has_dkey VCS.dkey_success_only then
+ if Wp_parameters.has_dkey VCS.dkey_shell then
begin
let n = s.interrupted + s.unknown in
if n > 0 then
@@ -511,27 +504,26 @@ let do_report_prover_stats pp_prover fmt (p,s) =
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
- 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 ;
- 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 ;
- end
+ 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
+ if !scheduled > 0 then
+ begin
+ let proved = GOALS.cardinal !proved in
+ 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 ;
+ 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 ;
+ end
let do_list_scheduled_result () =
begin
@@ -736,12 +728,10 @@ 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)
+ not (Wp_parameters.has_dkey VCS.dkey_shell)
then
Wp_parameters.result "[Cache] removed:%d" removed
end
@@ -812,6 +802,8 @@ let cmdline_run () =
end ;
Generator.compute_selection computer ~fct ~bhv ~prop ()
in
+ if Wp_parameters.CachePrint.get () then
+ Kernel.feedback "Cache directory: %s" (Cache.get_dir ()) ;
let fct = Wp_parameters.get_wp () in
match fct with
| Wp_parameters.Fct_none -> ()
@@ -905,7 +897,10 @@ let pp_wp_parameters fmt =
if Wp_parameters.RTE.get () then Format.pp_print_string fmt " -wp-rte" ;
let spec = Wp_parameters.Model.get () in
if spec <> [] && spec <> ["Typed"] then
- ( let descr = Factory.descr (Factory.parse spec) in
+ ( let descr =
+ if spec = ["Dump"] then "Dump"
+ else Factory.descr (Factory.parse spec)
+ in
Format.fprintf fmt " -wp-model '%s'" descr ) ;
if not (Wp_parameters.Let.get ()) then Format.pp_print_string fmt
" -wp-no-let" ;
@@ -932,7 +927,7 @@ let pp_wp_parameters fmt =
let () = Cmdline.run_after_setting_files
(fun _ ->
- if Wp_parameters.has_dkey dkey_shell then
+ if Wp_parameters.has_dkey VCS.dkey_shell then
Log.print_on_output pp_wp_parameters)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/tests/README.md b/src/plugins/wp/tests/README.md
index 2eb7d3d587b555af4b14c9f791c20376a97d2b5c..68134928bbc16a587fa10b91746e0fbadd61da20 100644
--- a/src/plugins/wp/tests/README.md
+++ b/src/plugins/wp/tests/README.md
@@ -59,11 +59,16 @@ doing so would causing WP to add new cache entries to the global « qualif » ca
from all your projects around. Consult the section « Global WP Cache Setup »
below for details.
+Note that this cache is meant to be global, including for the different merge
+requests. Thus, when working on a new merge request for WP, **do not** create a
+branch (and MR) on the WP-cache repository: just push the new cache entries into
+the global cache using `make wp-qualif-push`.
+
# Qualified Test Results
To be accepted by Frama-CI, tests in « qualif » configuration must be easily
reproducible on any platform. This is checked by running WP with flag
-`-wp-msg-key success-only` which is set by the default in the qualif test
+`-wp-msg-key shell` which is set by the default in the qualif test
configuration. Hence, a qualified test result only contains proof status that
are either:
- failed
@@ -75,7 +80,7 @@ are either:
This excludes any timeout with native Alt-Ergo, which must be turned into some
reproducible stepout by setting `-wp-steps` and `-wp-timeout` options
accordingly. Please choose a step limit that makes large enough to ensure the
-goal is not provable, but small enough to make alt-ergo decide quickly.
+goal is provable, but small enough to make alt-ergo decide quickly.
# Global WP Cache Setup (for wp-qualif)
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 2fb225cf969783f35136d70c84351eb7ff294699..82ac23797226aae576338c46106f95e16f40b717 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,2 +1,2 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell,success-only -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
+CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
OPT:
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.i b/src/plugins/wp/tests/wp/stmtcompiler_test.i
index 264b9e58d48e6401b1c73564a7755720598f2b97..c610d54549272ce23c3610a5e58846880fcd5b00 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.i
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.i
@@ -1,5 +1,5 @@
/* run.config
- OPT: -load-script tests/wp/stmtcompiler_test.ml -wp-msg-key success-only
+ OPT: -load-script tests/wp/stmtcompiler_test.ml -wp-msg-key shell
*/
int empty (int c){
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
index 4dafe25db11100c8549fc7f6291914f0a31f9df0..b206efad0519db1f347ae4a6b79e5221ff611f9d 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
@@ -1,5 +1,5 @@
/* run.config_qualif
- OPT: -load-script tests/wp/stmtcompiler_test_rela.ml -wp-msg-key success-only
+ OPT: -load-script tests/wp/stmtcompiler_test_rela.ml -wp-msg-key shell
*/
int empty (int c){
diff --git a/src/plugins/wp/tests/wp/wp_strategy.c b/src/plugins/wp/tests/wp/wp_strategy.c
index 0afd35c132005b5dc32d047c4d9847b410013b91..c514347a72a233922e656c26095d63647feea376 100644
--- a/src/plugins/wp/tests/wp/wp_strategy.c
+++ b/src/plugins/wp/tests/wp/wp_strategy.c
@@ -4,7 +4,7 @@ OPT: -journal-disable -wp-model Typed -wp-verbose 2 -wp-prop @assigns
*/
/* run.config_qualif
-OPT: -journal-disable -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key "success-only"
+OPT: -journal-disable -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key shell
*/
/*----------------------------------------------------------------------------*/
@@ -89,7 +89,7 @@ int default_behaviors (int c, int x) {
int y;
//@ ensures qed_ok: stmt_p: x > 0; assigns qed_ok: x;
- if (c) x = 1;
+ if (c) x = 1;
else {
//@ assert qed_ok: x >= 0;
x++;
diff --git a/src/plugins/wp/tests/wp_acsl/boolean.i b/src/plugins/wp/tests/wp_acsl/boolean.i
index f8e7f458b4f55d82f878bfed3a4a83f71dd3352e..79f94c24a8a358a23922d03fee6157f4d6f03ad1 100644
--- a/src/plugins/wp/tests/wp_acsl/boolean.i
+++ b/src/plugins/wp/tests/wp_acsl/boolean.i
@@ -1,5 +1,5 @@
/* run.config
-OPT: -wp-gen -wp-prover why3 -wp-msg-key success-only
+OPT: -wp-gen -wp-prover why3 -wp-msg-key shell
*/
/*@
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
index 40c0c6de692e62b8846b7a62e3bc02b1dcfb564c..979b8b88f24de686b3269c1c829b0bf3c69cf033 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
@@ -305,4 +305,4 @@
Functions WP Alt-Ergo Total Success
f 12 31 43 100%
------------------------------------------------------------
-[wp] Logging keys: success-only,shell,cnf.
+[wp] Logging keys: shell,cnf.
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
index 00a8df49e163c00104c97b7203e10f9e6f4accfa..064dce264b9e7e20ae5c3d9799927e9b346ed87c 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
@@ -8,7 +8,6 @@
[rte] annotating function init
[rte] annotating function mem_binding
[rte] annotating function size
-[wp] Computing [100 goals...]
[wp] Goal typed_add_complete_full_nominal : not tried
[wp] Goal typed_add_disjoint_full_nominal : not tried
[wp] Goal typed_add_assert_rte_index_bound : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
index 6e3fc54c35c0210277228789814f49736f648f08..8e5320587c9157e2971dc28f9078d3d860dbfd28 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
@@ -3,7 +3,6 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] Computing [100 goals...]
[wp] 102 goals scheduled
[wp] [Alt-Ergo] Goal typed_add_complete_full_nominal : Valid
[wp] [Alt-Ergo] Goal typed_add_disjoint_full_nominal : Valid
diff --git a/src/plugins/wp/tests/wp_manual/manual.i b/src/plugins/wp/tests/wp_manual/manual.i
index 7cd72107d4ca6d53372e573288e68d42ab88786c..11a04e0783ab7854b9dcb873766eaa739de19bfa 100644
--- a/src/plugins/wp/tests/wp_manual/manual.i
+++ b/src/plugins/wp/tests/wp_manual/manual.i
@@ -2,8 +2,8 @@
DONTRUN:
*/
/* run.config_qualif
- OPT: -wp-msg-key no-time-info @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap1.h
- OPT: -wp-msg-key no-time-info -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h
- OPT: -load-module report -kernel-verbose 0 -wp-msg-key no-time-info -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h -wp-verbose 0 -then -no-unicode -report
+ OPT: -wp-msg-key shell @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap1.h
+ OPT: -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h
+ OPT: -load-module report -kernel-verbose 0 -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h -wp-verbose 0 -then -no-unicode -report
*/
void look_at_working_dir(void);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
index 98b421111a0747310342b30ae27213ef61a1adc8..b622a45a0f7a2daa0c28f30d33096e4fde0e5d6c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
@@ -1,10 +1,11 @@
+# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/removed.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/wp_plugin/removed.i:10: Warning:
+[eva:alarm] tests/wp_plugin/removed.i:9: Warning:
signed overflow. assert 1 + i ≤ 2147483647;
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -17,5 +18,10 @@
[wp] [Alt-Ergo] Goal typed_main_assert_Eva_signed_overflow : Unsuccess
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unsuccess: 1)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ main - - 1 0.0%
+------------------------------------------------------------
[wp] Running WP plugin...
[wp] Warning: No goal generated
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
index efc57b6183b5975f7b8605af6ecacb8409e2fa88..583f4d36f0886bdb9e400a01be8bc0d7723ec389 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
@@ -1,3 +1,4 @@
+# frama-c -wp -wp-model 'Dump' [...]
[kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing)
[wp] Running WP plugin...
[wp] [CFG] Goal f_exits : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_plugin/removed.i b/src/plugins/wp/tests/wp_plugin/removed.i
index f27fb0df1d6386f8b02e3954f7cf1cab1d922897..9a4824f460e97fc22bacd03aae895c0e4c6147eb 100644
--- a/src/plugins/wp/tests/wp_plugin/removed.i
+++ b/src/plugins/wp/tests/wp_plugin/removed.i
@@ -1,6 +1,5 @@
/* run.config_qualif
- CMD: @frama-c@ -wp-share ./share -wp-msg-key no-cache-info,success-only -wp-par 1 -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache replay -wp-cache-dir ./cache
- OPT: -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
+ OPT: -load-module eva,scope -no-wp -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
*/
/* run.config
diff --git a/src/plugins/wp/tests/wp_plugin/stmt.c b/src/plugins/wp/tests/wp_plugin/stmt.c
index 02e1eddff383cc8b84a70ba560c0f62f60cd4d4d..58e04b9d85fccbba9f6eb09c1738dffc0c98768c 100644
--- a/src/plugins/wp/tests/wp_plugin/stmt.c
+++ b/src/plugins/wp/tests/wp_plugin/stmt.c
@@ -4,7 +4,7 @@
/* run.config_qualif
OPT: -load-module report -then -report
- EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-model Dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key no-cache-info @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
+ EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-model Dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key shell @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
*/
/*@ ensures a > 0 ==> \result == a + b;
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index 999fd9b742431831e08595ee7463dfe6d0469cd4..e8e6e13bc582dde43cd57df852ee32ea1fc163ed 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -8,7 +8,6 @@
[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
-[wp] Computing [100 goals...]
------------------------------------------------------------
Function init
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index e6996907f9367101bc6353be0b7ae906cb568ba9..aa1fcfbc2ff78b19adb1a83efb7a8576a3e8bf19 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -8,7 +8,6 @@
[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
-[wp] Computing [100 goals...]
------------------------------------------------------------
Function init
------------------------------------------------------------
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 47bb5721b38c1de4331503410072ae87c26c7265..448ff335f59df0604294f560f9f87b957e69a5ae 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -639,18 +639,18 @@ module Cache = String
- 'replay': update mode with no cache update\n\
- 'rebuild': always run provers and update cache\n\
- 'offline': use cache but never run provers\n\
- This option is overriden by environment variable FRAMAC_WP_CACHE,\
- unless -wp-no-cache-env is used."
+ You can also use the environment variable FRAMAC_WP_CACHE instead."
end)
let () = Parameter_customize.set_group wp_prover
-module CacheEnv = True
+module CacheEnv = False
(struct
let option_name = "-wp-cache-env"
- let help = "Use environment variables for cache.\n\
+ let help = "Gives environment variables precedence over command line\n\
+ for cache management:\n\
- FRAMAC_WP_CACHE overrides -wp-cache\n\
- FRAMAC_WP_CACHEDIR overrides -wp-cache-dir\n\
- This is the behavior by default."
+ Disabled by default."
end)
let () = Parameter_customize.set_group wp_prover
@@ -661,8 +661,15 @@ module CacheDir = String
let default = ""
let help =
"Specify global cache directory (no cleanup mode).\n\
- This option is overriden by environment variable FRAMAC_WP_CACHEDIR,\
- unless -wp-no-cache-env is used."
+ By default, cache entries are stored in the WP session directory.\n\
+ You can also use the environment variable FRAMAC_WP_CACHEDIR instead."
+ end)
+
+let () = Parameter_customize.set_group wp_prover
+module CachePrint = False
+ (struct
+ let option_name = "-wp-cache-print"
+ let help = "Show cache directory"
end)
let () = Parameter_customize.set_group wp_prover
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index e1fd65d39590ff076d0f33ec8c496d5af590f9bf..f998977a9af312b4433ba49926a80b811f21a275 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -112,6 +112,7 @@ module RunAllProvers: Parameter_sig.Bool
module Cache: Parameter_sig.String
module CacheEnv: Parameter_sig.Bool
module CacheDir: Parameter_sig.String
+module CachePrint: Parameter_sig.Bool
module Drivers: Parameter_sig.String_list
module Script: Parameter_sig.String
module UpdateScript: Parameter_sig.Bool
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 4f85fe8851bc0fa7025f2cffd3fb2d1ca71b67bc..1d6649a3de7511c3c8a26c798fa5d9a90c25877d 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -659,7 +659,7 @@ let add g =
Gmap.iter
(fun _ ws -> WPOset.iter (fun _ -> incr added) ws)
system.wpo_idx ;
- if not (Wp_parameters.has_dkey VCS.dkey_no_goals_info) then
+ if not (Wp_parameters.has_dkey VCS.dkey_shell) then
Wp_parameters.feedback ~ontty:`Feedback "Computing [%d goals...]" !added ;
added := 0 ;
end ;