From b11129ba99a31b9757881a60e5bb7f8aaa5c6e5a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 11 Sep 2019 15:40:08 +0200
Subject: [PATCH] [wp/cache] fix cleanup mode
---
src/plugins/wp/ProverWhy3.ml | 48 ++++++++-----------
src/plugins/wp/ProverWhy3.mli | 2 -
src/plugins/wp/register.ml | 39 ++-------------
src/plugins/wp/tests/wp_plugin/convert.i | 5 +-
src/plugins/wp/tests/wp_plugin/model.i | 3 +-
.../tests/wp_plugin/oracle/model.res.oracle | 8 ++--
.../oracle_qualif/convert.0.res.oracle | 6 ++-
.../41595c57ce7e98269d53becbfeb7bcb3.json | 2 +
.../997da10e0a56b9a3ff392e4d0e7b52b7.json | 2 +
.../oracle_qualif/convert.1.res.oracle | 21 +++++---
.../wp_plugin/oracle_qualif/model.res.oracle | 20 ++++++--
.../4dc341b2d4deefe644f427eea94616b0.json | 1 +
src/plugins/wp/tests/wp_plugin/removed.i | 2 +-
13 files changed, 74 insertions(+), 85 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/41595c57ce7e98269d53becbfeb7bcb3.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/997da10e0a56b9a3ff392e4d0e7b52b7.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.0.session/cache/4dc341b2d4deefe644f427eea94616b0.json
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 909e27a9e3a..8e212b42b0c 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1090,15 +1090,8 @@ type mode = NoCache | Update | Replay | Rebuild | Offline | Cleanup
let hits = ref 0
let miss = ref 0
let removed = ref 0
-let cleanup = Hashtbl.create 0 (* used entries *)
-
-let reset () =
- begin
- hits := 0 ;
- miss := 0 ;
- removed := 0 ;
- Hashtbl.clear cleanup ;
- end
+let cleanup = Hashtbl.create 0
+(* used entries, never to be reset since cleanup is performed at exit *)
let get_hits () = !hits
let get_miss () = !miss
@@ -1108,7 +1101,7 @@ let mark_cache ~mode hash =
if mode = Cleanup then Hashtbl.replace cleanup hash ()
let cleanup_cache ~mode =
- if mode = Cleanup then
+ if mode = Cleanup && (!hits > 0 || !miss > 0) then
let dir = Wp_parameters.get_session_dir "cache" in
try
if Sys.is_directory dir then
@@ -1181,38 +1174,41 @@ let task_hash wpo drv prover task =
let time_fits time = function
| None | Some 0 -> true
- | Some limit ->
- time < float limit
+ | Some limit -> time <= float limit
-let step_fits steps = function
+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.Checked -> VCS.no_result
| VCS.Failed -> res
| VCS.Invalid | VCS.Valid | VCS.Unknown ->
- if not (step_fits res.prover_steps steplimit) then
+ 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
- | Timeout ->
- if not (step_fits res.prover_steps steplimit) then
+ | VCS.Timeout | VCS.Stepout ->
+ if steps_seized res.prover_steps steplimit then
{ res with verdict = Stepout }
else
- if time_fits res.prover_time timeout then
- VCS.no_result
- else res
- | Stepout ->
- if step_fits res.prover_steps steplimit then
- VCS.no_result
- else
- if not (time_fits res.prover_time timeout) then
+ if time_seized res.prover_time timeout then
{ res with verdict = Timeout }
- else res
+ else (* can be run a longer time or widely *)
+ VCS.no_result
let get_cache_result ~mode hash =
match mode with
@@ -1288,8 +1284,6 @@ let prove ?timeout ?steplimit ~prover wpo =
then
begin
incr hits ;
- if mode = Cleanup then
- set_cache_result ~mode hash prover result ;
Task.return result
end
else
diff --git a/src/plugins/wp/ProverWhy3.mli b/src/plugins/wp/ProverWhy3.mli
index 70df0ed53b7..e107c669a15 100644
--- a/src/plugins/wp/ProverWhy3.mli
+++ b/src/plugins/wp/ProverWhy3.mli
@@ -32,8 +32,6 @@ val prove : ?timeout:int -> ?steplimit:int -> prover:Why3Provers.t ->
type mode = NoCache | Update | Replay | Rebuild | Offline | Cleanup
val get_mode : unit -> mode
-
-val reset : unit -> unit (** Reset cache statistics *)
val get_hits : unit -> int
val get_miss : unit -> int
val get_removed : unit -> int
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index df7d9606a5f..8b30fba2dd6 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -230,7 +230,6 @@ let clear_scheduled () =
exercised := 0 ;
proved := GOALS.empty ;
provers := PM.empty ;
- ProverWhy3.reset () ;
end
let get_pstat p =
@@ -502,6 +501,7 @@ let do_report_cache_usage mode =
Format.pp_print_newline fmt () ;
end
+(* registered at frama-c (normal) exit *)
let do_cache_cleanup () =
begin
let mode = ProverWhy3.get_mode () in
@@ -680,7 +680,6 @@ let do_wp_proofs_iter iter =
begin
if spawned then do_list_scheduled iter ;
spawn_wp_proofs_iter ~mode iter ;
- do_cache_cleanup () ;
if spawned then
begin
do_list_scheduled_result () ;
@@ -916,40 +915,9 @@ let do_prover_detect () =
) provers
(* ------------------------------------------------------------------------ *)
-(* --- Main Entry Point --- *)
+(* --- Main Entry Points --- *)
(* ------------------------------------------------------------------------ *)
-(*
-(* This filter can be changed to make exceptions interrupting
- the sequence immediately *)
-let catch_exn (_:exn) =
- not (Wp_parameters.has_dkey "raised")
-
-(* This order can be changed *)
-let reraised_exn (first:exn) (_last:exn) = Some first
-
-(* Don't use Extlib.try_finally:
- No exception is used for control here.
- Backtrace is dumped here for debugging purpose.
- We just record one of the raised exceptions (to be raised again),
- while ensuring all tasks are finally executed. *)
-let protect err job =
- try job ()
- with e when catch_exn e ->
- let b = Printexc.get_raw_backtrace () in
- Wp_parameters.failure "%s@\n%s"
- (Printexc.to_string e)
- (Printexc.raw_backtrace_to_string b) ;
- match !err with
- | None -> err := Some e
- | Some previous -> err := reraised_exn previous e
-
-let sequence jobs =
- let err = ref None in
- List.iter (protect err) jobs ;
- match !err with None -> () | Some e -> raise e
-*)
-
let rec try_sequence jobs () = match jobs with
| [] -> ()
| head :: tail ->
@@ -980,4 +948,7 @@ let main = sequence [
(fun () -> Wp_parameters.debug ~dkey:job_key "Stop WP plugin...@.") ;
]
+let () = Cmdline.at_normal_exit do_cache_cleanup
let () = Db.Main.extend main
+
+(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/tests/wp_plugin/convert.i b/src/plugins/wp/tests/wp_plugin/convert.i
index 380f6dc6405..630c406f967 100644
--- a/src/plugins/wp/tests/wp_plugin/convert.i
+++ b/src/plugins/wp/tests/wp_plugin/convert.i
@@ -3,9 +3,8 @@
*/
/* run.config_qualif
- CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-timeout 100 -wp-steps 500 -wp-share ./share -wp-msg-key shell,success-only -wp-out @PTEST_FILE@.@PTEST_NUMBER@.out @PTEST_FILE@
- OPT: -wp-prover alt-ergo -wp-report=tests/qualif.report
- OPT: -wp-prover why3:alt-ergo -wp-report=tests/qualif-why3.report
+ OPT:
+ OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report
*/
// --------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/model.i b/src/plugins/wp/tests/wp_plugin/model.i
index 226489bb68d..0f90c5deb36 100644
--- a/src/plugins/wp/tests/wp_plugin/model.i
+++ b/src/plugins/wp/tests/wp_plugin/model.i
@@ -4,8 +4,7 @@
*/
/* run.config_qualif
- CMD: @frama-c@ -wp-share ./share -wp-msg-key cluster,shell -wp-par 1 -wp-timeout 100 -wp-steps 500
- OPT: -wp-model Typed -wp -wp-check -then -wp-model Typed+ref -wp -wp-check
+ OPT: -wp-msg-key cluster -wp-model Typed -wp-check -then -wp -wp-model Typed+ref -wp-check
*/
//@ predicate P(integer a);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
index 521d7599837..32436320567 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/model.i (no preprocessing)
-[kernel] tests/wp_plugin/model.i:11: Warning:
+[kernel] tests/wp_plugin/model.i:10: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
@@ -82,7 +82,7 @@ end
Function f
------------------------------------------------------------
-Goal Post-condition (file tests/wp_plugin/model.i, line 13) in 'f':
+Goal Post-condition (file tests/wp_plugin/model.i, line 12) in 'f':
Let x = Mint_0[shift_sint32(p, k)].
Assume {
Type: is_sint32(k) /\ is_sint32(x).
@@ -199,7 +199,7 @@ end
Function f
------------------------------------------------------------
-Goal Post-condition (file tests/wp_plugin/model.i, line 13) in 'f':
+Goal Post-condition (file tests/wp_plugin/model.i, line 12) in 'f':
Let x = Mint_0[shift_sint32(p, k)].
Assume {
Type: is_sint32(k) /\ is_sint32(x).
@@ -210,7 +210,7 @@ Prove: P_P(x).
------------------------------------------------------------
-Goal Post-condition (file tests/wp_plugin/model.i, line 13) in 'f':
+Goal Post-condition (file tests/wp_plugin/model.i, line 12) in 'f':
Let x = Mint_0[shift_sint32(p, k)].
Assume {
Type: is_sint32(k) /\ is_sint32(x).
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle
index 1174aab5945..005e353f364 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-timeout 100 -wp-steps 500 [...]
+# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/convert.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
@@ -8,7 +8,9 @@
[wp] Proved goals: 2 / 2
Qed: 0
Alt-Ergo 2.0.0: 2
+[wp] Report in: 'tests/wp_plugin/oracle_qualif/convert.0.report.json'
+[wp] Report out: 'tests/wp_plugin/result_qualif/convert.0.report.json'
-------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
-Lemma - 2 2 100%
+Lemma - 2 (1..12) 2 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/41595c57ce7e98269d53becbfeb7bcb3.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/41595c57ce7e98269d53becbfeb7bcb3.json
new file mode 100644
index 00000000000..5f72202be45
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/41595c57ce7e98269d53becbfeb7bcb3.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0062,
+ "steps": 7 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/997da10e0a56b9a3ff392e4d0e7b52b7.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/997da10e0a56b9a3ff392e4d0e7b52b7.json
new file mode 100644
index 00000000000..9c4815d94cd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/997da10e0a56b9a3ff392e4d0e7b52b7.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0087,
+ "steps": 7 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
index cf1e24e7a66..3dd881b83a0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
@@ -1,11 +1,20 @@
-# frama-c -wp -wp-timeout 100 -wp-steps 500 [...]
+# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/convert.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] 2 goals scheduled
-[wp] [Alt-Ergo 2.0.0] Goal typed_lemma_ceil : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_lemma_floor : Valid
+[wp] [Alt-Ergo (Native)] Goal typed_lemma_ceil : Valid
+[wp] [Alt-Ergo (Native)] Goal typed_lemma_floor : Valid
[wp] Proved goals: 2 / 2
- Qed: 0
- Alt-Ergo 2.0.0: 2
-[kernel] System error: tests/qualif-why3.report: No such file or directory
+ Qed: 0
+ Alt-Ergo: 2
+[wp] Report in: 'tests/wp_plugin/oracle_qualif/convert.1.report.json'
+[wp] Report out: 'tests/wp_plugin/result_qualif/convert.1.report.json'
+-------------------------------------------------------------
+Axiomatics WP Alt-Ergo Total Success
+Lemma - - (20..32) 2 100%
+-------------------------------------------------------------
+-------------------------------------------------------------
+Axiomatics WP Alt-Ergo (Native) Total Success
+Lemma - 2 (20..32) 2 100%
+-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
index a86ad7dc115..8569ce3a25e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
@@ -1,6 +1,6 @@
-# frama-c -wp -wp-timeout 100 -wp-steps 500 [...]
+# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/model.i (no preprocessing)
-[kernel] tests/wp_plugin/model.i:11: Warning:
+[kernel] tests/wp_plugin/model.i:10: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
@@ -50,7 +50,13 @@ theory Axiomatic
end
[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures : Typechecked
[wp] Proved goals: 0 / 1
- Alt-Ergo 2.0.0: 0 (unknown: 1)
+ Alt-Ergo 2.0.0: 0 (unsuccess: 1)
+[wp] Report in: 'tests/wp_plugin/oracle_qualif/model.0.report.json'
+[wp] Report out: 'tests/wp_plugin/result_qualif/model.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+f - - 1 0.0%
+-------------------------------------------------------------
[wp] Running WP plugin...
[wp] 2 goals scheduled
[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures : Typechecked
@@ -98,4 +104,10 @@ theory Axiomatic1
end
[wp] [Alt-Ergo 2.0.0] Goal typed_ref_f_ensures : Typechecked
[wp] Proved goals: 0 / 2
- Alt-Ergo 2.0.0: 0 (unknown: 2)
+ Alt-Ergo 2.0.0: 0 (unsuccess: 2)
+[wp] Report in: 'tests/wp_plugin/oracle_qualif/model.0.report.json'
+[wp] Report out: 'tests/wp_plugin/result_qualif/model.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+f - - 2 0.0%
+-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.0.session/cache/4dc341b2d4deefe644f427eea94616b0.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.0.session/cache/4dc341b2d4deefe644f427eea94616b0.json
new file mode 100644
index 00000000000..16d19ceb388
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.0.session/cache/4dc341b2d4deefe644f427eea94616b0.json
@@ -0,0 +1 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_plugin/removed.i b/src/plugins/wp/tests/wp_plugin/removed.i
index e865b65ae68..dadeb120b00 100644
--- a/src/plugins/wp/tests/wp_plugin/removed.i
+++ b/src/plugins/wp/tests/wp_plugin/removed.i
@@ -1,5 +1,5 @@
/* run.config_qualif
- CMD: @frama-c@ -wp-share ./share -wp-msg-key success-only -wp-par 1 -wp-timeout 100 -wp-steps 500
+ CMD: @frama-c@ -wp-share ./share -wp-msg-key success-only -wp-par 1 -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache offline
OPT: -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
*/
--
GitLab