From 6a90eb30e7331a575a1800c14f72849eb77af063 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 2 Feb 2021 11:12:19 +0100
Subject: [PATCH] [wp] take into accounts unreachable in final count
---
src/plugins/wp/register.ml | 43 ++++++++-------
.../oracle_qualif/nupw-bcl-bts1120.res.oracle | 2 +-
.../oracle_qualif/string-compare.res.oracle | 2 +-
.../wp/tests/wp_plugin/oracle_qualif/stmt.log | 1 +
.../wp_plugin/oracle_qualif/stmt.res.oracle | 2 +-
.../oracle_qualif/user_init.0.res.oracle | 2 +-
.../oracle_qualif/user_init.1.res.oracle | 2 +-
.../oracle_qualif/user_init.2.res.oracle | 2 +-
src/plugins/wp/wpAnnot.ml | 54 +++++++++++--------
src/plugins/wp/wpAnnot.mli | 3 ++
src/plugins/wp/wpReached.ml | 25 +++++++++
src/plugins/wp/wpReached.mli | 2 +
src/plugins/wp/wpo.ml | 24 +--------
13 files changed, 94 insertions(+), 70 deletions(-)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 206b3d7609d..89998c9ea08 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -225,6 +225,8 @@ let clear_scheduled () =
exercised := 0 ;
session := GOALS.empty ;
provers := PM.empty ;
+ WpAnnot.unreachable_proved := 0 ;
+ WpAnnot.unreachable_failed := 0 ;
end
let get_pstat p =
@@ -255,7 +257,6 @@ let add_time s t =
end
let do_list_scheduled goals =
- clear_scheduled () ;
Bag.iter
(fun goal ->
begin
@@ -503,25 +504,27 @@ let do_report_scheduled () =
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 passed = GOALS.fold
- (fun g n ->
- if Wpo.is_passed g then succ n else n
- ) !session 0 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" passed !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 total =
+ !scheduled + !WpAnnot.unreachable_failed + !WpAnnot.unreachable_proved in
+ if total > 0 then
+ begin
+ let passed = GOALS.fold
+ (fun g n ->
+ if Wpo.is_passed g then succ n else n
+ ) !session !WpAnnot.unreachable_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" passed total ;
+ 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
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
index 164271bc40a..b7eb301f118 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
@@ -17,7 +17,7 @@
[wp] [Qed] Goal typed_g_assigns_normal_part3 : Valid
[wp] [Qed] Goal typed_unreachable_smt_with_contract_ensures_ok_2 : Valid
[wp] [Qed] Goal typed_unreachable_smt_with_contract_call_f_with_precond_2_requires_ok : Valid
-[wp] Proved goals: 8 / 8
+[wp] Proved goals: 14 / 14
Qed: 8
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
index 48ad48fb860..98114b8eb47 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
@@ -56,7 +56,7 @@
[wp] [Qed] Goal typed_main_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_main_assigns_normal_part2 : Valid
[wp] [Alt-Ergo] Goal typed_main_call_stringCompare_requires_validStrings : Valid
-[wp] Proved goals: 51 / 51
+[wp] Proved goals: 53 / 53
Qed: 33
Alt-Ergo: 18
------------------------------------------------------------
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 583f4d36f08..54fa701c499 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
@@ -19,3 +19,4 @@
[wp] CFG f -> f
[wp] CFG f -> f_default_for_stmt_2
[wp] Warning: No goal generated
+[wp] Proved goals: 9 / 9
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
index 3a74fac104c..0d904ff5c08 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
@@ -22,7 +22,7 @@
[wp] [Qed] Goal typed_h_ensures_2 : Valid
[wp] [Qed] Goal typed_h_assert : Valid
[wp] [Qed] Goal typed_h_assert_2 : Valid
-[wp] Proved goals: 10 / 10
+[wp] Proved goals: 19 / 19
Qed: 10
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
index 3945dd8f3a6..890545f1a90 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
@@ -100,7 +100,7 @@
[wp] [Qed] Goal typed_init_t2_bis_v2_loop_variant_positive : Valid
[wp] [Qed] Goal typed_init_t2_bis_v2_call_init_requires : Valid
[wp] [Qed] Goal typed_init_t2_bis_v2_call_init_requires_2 : Valid
-[wp] Proved goals: 92 / 92
+[wp] Proved goals: 97 / 97
Qed: 52
Alt-Ergo: 40
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
index f9f0f2c2198..71a1c37ecc6 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
@@ -31,7 +31,7 @@
[wp] [Qed] Goal typed_init_t2_bis_v2_assigns_exit_part3 : Valid
[wp] [Qed] Goal typed_init_t2_bis_v2_assigns_normal_part1 : Valid
[wp] [Script] Goal typed_init_t2_bis_v2_assigns_normal_part2 : Valid
-[wp] Proved goals: 23 / 23
+[wp] Proved goals: 28 / 28
Qed: 11
Script: 12
Alt-Ergo: 0 (unsuccess: 12)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
index 41f563dd7bf..73b6604f313 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
@@ -24,7 +24,7 @@
[wp] [Qed] Goal typed_init_t2_bis_v1_assigns_exit_part3 : Valid
[wp] [Qed] Goal typed_init_t2_bis_v1_assigns_normal_part1 : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_assigns_normal_part2 : Unsuccess
-[wp] Proved goals: 7 / 16
+[wp] Proved goals: 12 / 21
Qed: 7
Alt-Ergo: 0 (unsuccess: 9)
------------------------------------------------------------
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 2a3326280b0..ad7739a5143 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -68,6 +68,9 @@ let get_called_assigns kf =
(* --- Status of Unreachable Annotations --- *)
(* -------------------------------------------------------------------------- *)
+let unreachable_proved = ref 0
+let unreachable_failed = ref 0
+
let wp_unreachable =
Emitter.create
"Unreachable Annotations"
@@ -76,27 +79,36 @@ let wp_unreachable =
~tuning:[] (* TBC *)
let set_unreachable pid =
- let open Property in
- let emit = function
- | IPPredicate {ip_kind = PKAssumes _} -> ()
- | p ->
- debug "unreachable annotation %a@." Property.pretty p;
- Property_status.emit wp_unreachable ~hyps:[] p Property_status.True
- in
- let pids = match WpPropId.property_of_id pid with
- | IPPredicate {ip_kind = PKAssumes _} -> []
- | IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv} ->
- let active = Datatype.String.Set.elements ib_active in
- (ip_post_cond_of_behavior ib_kf ib_kinstr active ib_bhv) @
- (ip_requires_of_behavior ib_kf ib_kinstr ib_bhv)
- | IPExtended _ -> []
- (* Extended clauses might concern anything. Don't validate them
- unless we know exactly what is going on. *)
- | p ->
- Wp_parameters.result "[CFG] Goal %a : Valid (Unreachable)"
- WpPropId.pp_propid pid ; [p]
- in
- List.iter emit pids
+ if WpPropId.is_smoke_test pid then
+ begin
+ let source = WpPropId.source_of_id pid in
+ WpReached.set_doomed wp_unreachable pid ;
+ incr unreachable_failed ;
+ Wp_parameters.warning ~source "Failed smoke-test"
+ end
+ else
+ let open Property in
+ let emit = function
+ | IPPredicate {ip_kind = PKAssumes _} -> ()
+ | p ->
+ debug "unreachable annotation %a@." Property.pretty p;
+ Property_status.emit wp_unreachable ~hyps:[] p Property_status.True
+ in
+ let pids = match WpPropId.property_of_id pid with
+ | IPPredicate {ip_kind = PKAssumes _} -> []
+ | IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv} ->
+ let active = Datatype.String.Set.elements ib_active in
+ (ip_post_cond_of_behavior ib_kf ib_kinstr active ib_bhv) @
+ (ip_requires_of_behavior ib_kf ib_kinstr ib_bhv)
+ | IPExtended _ -> []
+ (* Extended clauses might concern anything. Don't validate them
+ unless we know exactly what is going on. *)
+ | p ->
+ incr unreachable_proved ;
+ Wp_parameters.result "[CFG] Goal %a : Valid (Unreachable)"
+ WpPropId.pp_propid pid ; [p]
+ in
+ List.iter emit pids
(*----------------------------------------------------------------------------*)
(* Proofs *)
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index fdd66f1de80..a005a5d2c36 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -56,6 +56,9 @@ val filter_status : WpPropId.prop_id -> bool
(*----------------------------------------------------------------------------*)
+val unreachable_proved : int ref
+val unreachable_failed : int ref
+
val get_called_preconditions_at : kernel_function -> stmt -> Property.t list
val get_called_post_conditions : kernel_function -> Property.t list
val get_called_exit_conditions : kernel_function -> Property.t list
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index 3ef23a0bdbf..faa8f4fa173 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -314,3 +314,28 @@ let reachability = FRmap.memo
end
(* -------------------------------------------------------------------------- *)
+(* --- Doome Status --- *)
+(* -------------------------------------------------------------------------- *)
+
+let set_invalid emitter tgt =
+ Property_status.emit emitter ~hyps:[] tgt Property_status.False_if_reachable
+
+let set_doomed emitter pid =
+ List.iter (set_invalid emitter) (WpPropId.doomed_if_valid pid) ;
+ match WpPropId.unreachable_if_valid pid with
+ | Property.OLStmt(kf,stmt) ->
+ let ca =
+ match Annotations.code_annot ~emitter ~filter:is_dead_annot stmt with
+ | ca::_ -> ca
+ | [] ->
+ let pred_loc = Stmt.loc stmt in
+ let pred_name = [ "Wp" ; "SmokeTest" ] in
+ let pf = { Logic_const.pfalse with pred_loc ; pred_name } in
+ let pf = Logic_const.toplevel_predicate pf in
+ let ca = Logic_const.new_code_annotation (AAssert ([],pf)) in
+ Annotations.add_code_annot emitter ~kf stmt ca ; ca
+ in
+ List.iter (set_invalid emitter) (Property.ip_of_code_annot kf stmt ca)
+ | Property.OLGlob _ | Property.OLContract _ -> ()
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpReached.mli b/src/plugins/wp/wpReached.mli
index 0c9c6f46ee4..2ef8a243c65 100644
--- a/src/plugins/wp/wpReached.mli
+++ b/src/plugins/wp/wpReached.mli
@@ -49,4 +49,6 @@ val smoking : reachability -> Cil_types.stmt -> bool
val dump : dir:Datatype.Filepath.t -> Kernel_function.t -> reachability -> unit
+val set_doomed : Emitter.t -> WpPropId.prop_id -> unit
+
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index e5459e75b89..bed4b06b77b 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -715,28 +715,6 @@ let get_proof g =
with Not_found -> `Unknown
in status , target
-let set_invalid emitter tgt =
- Property_status.emit emitter ~hyps:[] tgt Property_status.False_if_reachable
-
-let set_doomed emitter pid =
- List.iter (set_invalid emitter) (WpPropId.doomed_if_valid pid) ;
- match WpPropId.unreachable_if_valid pid with
- | Property.OLStmt(kf,stmt) ->
- let ca =
- let filter = WpReached.is_dead_annot in
- match Annotations.code_annot ~emitter ~filter stmt with
- | ca::_ -> ca
- | [] ->
- let pred_loc = Stmt.loc stmt in
- let pred_name = [ "Wp" ; "SmokeTest" ] in
- let pf = { Logic_const.pfalse with pred_loc ; pred_name } in
- let pf = Logic_const.toplevel_predicate pf in
- let ca = Logic_const.new_code_annotation (AAssert ([],pf)) in
- Annotations.add_code_annot emitter ~kf stmt ca ; ca
- in
- List.iter (set_invalid emitter) (Property.ip_of_code_annot kf stmt ca)
- | Property.OLGlob _ | Property.OLContract _ -> ()
-
let find_proof system g =
let pi = proof g (WpPropId.property_of_id g.po_pid) in
try Hproof.find system.proofs pi
@@ -789,7 +767,7 @@ let set_result g p r =
in
let hyps = if smoke then [] else WpAnnot.dependencies proof in
Property_status.emit emitter ~hyps target status ;
- if smoke && unproved && proved then set_doomed emitter g.po_pid ;
+ if smoke && unproved && proved then WpReached.set_doomed emitter g.po_pid ;
end
let has_verdict g p =
--
GitLab