Commit dcef90ff authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'master' into feature/server/generate-api

parents a4714f32 21864645
export FRAMAC_WP_CACHE=update
export FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE)
export FRAMAC_WP_CACHEDIR=$WP_QUALIF_CACHE
......@@ -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
......
/* 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
......
# 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
......
[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
......
[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
......
[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
......
[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
......
[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
......
(**************************************************************************)
(* *)
(* 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
(**************************************************************************)
(* *)
(* 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
......@@ -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)
......
......@@ -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
......
......@@ -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)`"
......
......@@ -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"