diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 206b3d7609d9d16496e2d701dc64c5dabf1ea3e0..89998c9ea08bb99f08e0d3fa2a4d45ff8d4359bf 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 164271bc40ab026c97fa2a3ab4579fcb40c49bda..b7eb301f1182c82ee5e56750240487d8a1b2d157 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 48ad48fb860195d2301df4b58092b1e8086305dc..98114b8eb4713eda59a07effdbde20813a2eea86 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/doomed_dead.i b/src/plugins/wp/tests/wp_plugin/doomed_dead.i
index 5cba4b4ae13d297cf591afaa08431a1c45694e41..8d0d1b2c50fc6f8e06c5e79012073da85f98f6b9 100644
--- a/src/plugins/wp/tests/wp_plugin/doomed_dead.i
+++ b/src/plugins/wp/tests/wp_plugin/doomed_dead.i
@@ -3,8 +3,8 @@
*/
/* run.config_qualif
- OPT: -wp-smoke-tests
- OPT: -wp-smoke-tests -wp-split
+ OPT: -wp-smoke-tests -wp-steps 100
+ OPT: -wp-smoke-tests -wp-steps 100 -wp-split
*/
//@ assigns \nothing ;
diff --git a/src/plugins/wp/tests/wp_plugin/doomed_unreach.i b/src/plugins/wp/tests/wp_plugin/doomed_unreach.i
new file mode 100644
index 0000000000000000000000000000000000000000..6327fad4ec08aa62ba356fd50696547c3400b4c9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/doomed_unreach.i
@@ -0,0 +1,24 @@
+/* run.config
+ DONTRUN:
+ */
+
+/* run.config_qualif
+ OPT: -wp-smoke-tests -wp-steps 100
+*/
+
+//@ assigns \result;
+int job(int x) {
+ switch(x) {
+ return 42;
+ case 0:
+ return 0;
+ case 1:
+ return 1;
+ x = 42;
+ return 42;
+ default:
+ return 3;
+ }
+ x = 42;
+ return 42;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
index 0b349526c40d14e9bc6ee38bd5e6574999977b81..882ac924345c75bfbe007ec974f073762e8e6381 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp [...]
+# frama-c -wp -wp-steps 100 [...]
[kernel] Parsing tests/wp_plugin/doomed_dead.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
index fd8fae824785bcd829b66d0b40756567adba02b3..f3a71acd41e49cfc63ac7dcd2803443c07296812 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-split [...]
+# frama-c -wp -wp-split -wp-steps 100 [...]
[kernel] Parsing tests/wp_plugin/doomed_dead.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7140362d3548372aa5cbc7e8ff1bc89cf34acbf4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle
@@ -0,0 +1,21 @@
+# frama-c -wp -wp-steps 100 [...]
+[kernel] Parsing tests/wp_plugin/doomed_unreach.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] tests/wp_plugin/doomed_unreach.i:12: Warning: Failed smoke-test
+[wp] tests/wp_plugin/doomed_unreach.i:17: Warning: Failed smoke-test
+[wp] tests/wp_plugin/doomed_unreach.i:22: Warning: Failed smoke-test
+[wp] Warning: Missing RTE guards
+[wp] 6 goals scheduled
+[wp] [Passed] Smoke-test typed_job_wp_smoke_dead_code_s4
+[wp] [Passed] Smoke-test typed_job_wp_smoke_dead_code_s5
+[wp] [Passed] Smoke-test typed_job_wp_smoke_dead_code_s8
+[wp] [Qed] Goal typed_job_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job_assigns_part2 : Valid
+[wp] [Qed] Goal typed_job_assigns_part3 : Valid
+[wp] Proved goals: 6 / 9
+ Qed: 3
+ Alt-Ergo: 3
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job 3 3 6 100%
+------------------------------------------------------------
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 583f4d36f0886bdb9e400a01be8bc0d7723ec389..54fa701c499fd123bd6160f72a022ee8b5fd21de 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 3a74fac104c542c05e02bcaa5acab1560cebf58a..0d904ff5c08035bbca30031d490eb15e6ffdf0f0 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 3945dd8f3a65ec11fffa0303fe8300c4c4e63a66..890545f1a901bbb0eaec681155b688d75658e609 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 f9f0f2c219867828a57bba71fbce2fade387cf24..71a1c37ecc6fac5af4a88d1151b8798d141a3ca8 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 41f563dd7bf77dbfd732205c343f841b0bad0caf..73b6604f313f1b3c18ba90b8824a3f4c14e24982 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 c27e5f587c1c40a375e52e7aed7d072cc4565844..4a8f6ea3aeadb06a0fde85baa9c1bc075daec05b 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 *)
@@ -238,7 +250,7 @@ module HdefAnnotBhv = Cil2cfg.HE (struct type t = (stmt * int) end)
type strategy_info = {
kf : Kernel_function.t;
cfg : Cil2cfg.t;
- reached : WpReached.reached option ;
+ reachability : WpReached.reachability option ;
cur_bhv : asked_bhv;
asked_bhvs : asked_bhv list;
asked_prop : asked_prop;
@@ -915,7 +927,7 @@ let get_loop_annots config vloop s =
let add_stmt_deadcode_smoke config acc s =
if cur_fct_default_bhv config
then
- match config.reached with
+ match config.reachability with
| Some r when WpReached.smoking r s ->
WpStrategy.add_prop_dead_code acc config.kf s
| _ -> acc
@@ -1282,7 +1294,7 @@ class vexit kf acc =
Cil.DoChildren
end
-let process_unreached_annots cfg =
+let process_unreached_annots cfg reachability =
debug "collecting unreachable annotations@.";
let unreached = Cil2cfg.unreachable_nodes cfg in
let kf = Cil2cfg.cfg_kf cfg in
@@ -1298,6 +1310,16 @@ let process_unreached_annots cfg =
let do_annot s _ a acc =
List.fold_left add_id acc (WpPropId.mk_code_annot_ids kf s a)
in
+ let do_stmt s acc =
+ let acc =
+ match reachability with
+ | None -> acc
+ | Some r ->
+ if WpReached.smoking r s then
+ WpPropId.mk_smoke kf ~id:"unreachable" ~unreachable:s () :: acc
+ else acc
+ in Annotations.fold_code_annot (do_annot s) s acc
+ in
let do_node acc n =
debug
"process annotations of unreachable node %a@."
@@ -1312,13 +1334,13 @@ let process_unreached_annots cfg =
ignore Visitor.(visitFramacKf (visitor :> frama_c_visitor) kf) ;
visitor#acc
| Cil2cfg.Vcall (s, _, call, _) ->
- Annotations.fold_code_annot (do_annot s) s acc @
+ do_stmt s acc @
preconditions_at_call s call
| Cil2cfg.Vstmt s
| Cil2cfg.VblkIn (Cil2cfg.Bstmt s, _)
| Cil2cfg.VblkOut (Cil2cfg.Bstmt s, _)
| Cil2cfg.Vtest (true, s, _) | Cil2cfg.Vloop (_, s) | Cil2cfg.Vswitch (s,_)
- -> Annotations.fold_code_annot (do_annot s) s acc
+ -> do_stmt s acc
| Cil2cfg.Vtest (false, _, _) | Cil2cfg.Vloop2 _
| Cil2cfg.VblkIn _ | Cil2cfg.VblkOut _ | Cil2cfg.Vend -> acc
in
@@ -1330,11 +1352,6 @@ let process_unreached_annots cfg =
(* Everything must go through here. *)
(*----------------------------------------------------------------------------*)
-let get_cfg kf model =
- if Wp_parameters.RTE.get () then WpRTE.generate model kf ;
- let cfg = Cil2cfg.get kf in
- let _ = process_unreached_annots cfg in cfg
-
let build_configs assigns kf model behaviors ki property =
debug "[get_strategies] for behaviors names: %a@."
(Wp_error.pp_string_list ~sep:" " ~empty:"<none>")
@@ -1348,16 +1365,18 @@ let build_configs assigns kf model behaviors ki property =
debug
"[get_strategies] select stmt %d properties@." s.sid
in
- let cfg = get_cfg kf model in
- let reached =
+ if Wp_parameters.RTE.get () then WpRTE.generate model kf ;
+ let cfg = Cil2cfg.get kf in
+ let reachability =
if Wp_parameters.SmokeTests.get ()
&& Wp_parameters.SmokeDeadcode.get ()
- then Some (WpReached.reached kf)
+ then Some (WpReached.reachability kf)
else None in
+ process_unreached_annots cfg reachability ;
let def_annot_bhv, bhvs = find_behaviors kf cfg ki behaviors in
if bhvs <> [] then debug "[get_strategies] %d behaviors" (List.length bhvs);
let mk_bhv_config bhv = {
- kf; reached; cfg;
+ kf; reachability; cfg;
cur_bhv = bhv;
asked_prop = property;
asked_bhvs = bhvs;
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index fdd66f1de807146ead86fec1bf891ca75b0ebd5c..a005a5d2c36b54c29e3921a894615094f3333242 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 b21fa463f9fdd3b9aae169f4c37799a80600c8d0..60fe40d175ef9651652217627cc829397fddd8c9 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -40,14 +40,20 @@ type node = {
id : int ;
mutable flow : flow ;
mutable prev : node list ;
- mutable reached : bool option ;
+ mutable protected : bool option ;
+ (* whether the node is dominated by unreachable node or by a smoke test *)
+ mutable unreachable : bool option ;
+ (* whether the node is unreachable from the entry point *)
}
let kid = ref 0
let node () =
incr kid ;
- { id = !kid ; prev = [] ; reached = None ; flow = F_goto }
+ { id = !kid ; prev = [] ;
+ protected = None ;
+ unreachable = None ;
+ flow = F_goto }
(* -------------------------------------------------------------------------- *)
(* --- Unrolled Loop --- *)
@@ -83,7 +89,7 @@ let rec is_predicate cond p =
let is_dead_annot ca =
match ca.annot_content with
| APragma (Loop_pragma (Unroll_specs [ spec ; _ ])) ->
- false && is_unrolled_completely spec
+ is_unrolled_completely spec
| AAssert([],p)
| AInvariant([],_,p) ->
not p.tp_only_check && is_predicate false p.tp_statement
@@ -102,8 +108,8 @@ let is_dead_code stmt =
(* --- Compute CFG --- *)
(* -------------------------------------------------------------------------- *)
-type reached = node Stmt.Map.t
-type cfg = reached ref
+type reachability = node Stmt.Map.t
+type cfg = reachability ref (* working cfg during compilation *)
let of_stmt cfg s =
try Stmt.Map.find s !cfg with Not_found ->
@@ -133,11 +139,8 @@ type env = {
let rec stmt env s b =
let a = of_stmt env.cfg s in
- if is_dead_code s then
- a.flow <- F_dead
- else
- a.flow <- skind env a b s.skind ;
- a
+ let f = skind env a b s.skind in
+ a.flow <- if is_dead_code s then F_dead else f ; a
and skind env a b = function
| Instr i -> flow i (goto a b)
@@ -177,29 +180,46 @@ and sequence env seq b = match seq with
(* --- Compute Reachability --- *)
(* -------------------------------------------------------------------------- *)
-let rec reached node =
- match node.reached with
+let rec unreachable node =
+ match node.unreachable with
| Some r -> r
| None ->
- node.reached <- Some true ; (* cut loops *)
- let r = List.for_all reached_after node.prev in
- node.reached <- Some r ; r
-
-and reached_after node =
- match node.flow with
- | F_goto -> reached node
- | F_effect | F_entry | F_dead -> true
- | F_return | F_branch | F_call -> false
+ node.unreachable <- Some true ; (* cut loops *)
+ let r =
+ match node.flow with
+ | F_dead -> true
+ | F_entry -> false
+ | F_goto | F_effect | F_return | F_branch | F_call ->
+ List.for_all unreachable node.prev
+ in node.unreachable <- Some r ; r
+
+let rec protected node =
+ match node.protected with
+ | Some r -> r
+ | None ->
+ node.protected <- Some false ; (* cut loops *)
+ let r =
+ match node.flow with
+ | F_dead | F_entry -> true
+ | F_goto | F_effect | F_return | F_branch | F_call ->
+ node.prev <> [] && List.for_all protected_by node.prev
+ in node.protected <- Some r ; r
+
+and protected_by prev =
+ match prev.flow with
+ | F_dead | F_entry | F_effect -> true
+ | F_goto -> protected prev
+ | F_call | F_branch | F_return -> unreachable prev
let smoking_node n =
match n.flow with
- | F_effect | F_call | F_return -> not (reached n)
+ | F_effect | F_call | F_return -> not (protected n)
| F_goto | F_branch | F_entry | F_dead -> false
(* returns true if the stmt requires a reachability smoke test *)
-let smoking nodes stmt =
- try Stmt.Map.find stmt nodes |> smoking_node
- with Not_found -> false
+let smoking reachability stmt =
+ try Stmt.Map.find stmt reachability |> smoking_node
+ with Not_found -> true
let compute kf =
try
@@ -230,14 +250,10 @@ let dump ~dir kf reached =
N.define dot
(fun a na ->
let attr =
- if smoking_node a
- then [`Filled;`Fillcolor "orange"]
- else
- match a.flow with
- | F_entry | F_effect | F_return | F_call ->
- [`Filled;`Fillcolor "green"]
- | F_dead -> [`Filled;`Fillcolor "red"]
- | F_branch | F_goto -> []
+ if smoking_node a then [`Filled;`Fillcolor "orange"]
+ else if protected a then [`Filled;`Fillcolor "green"]
+ else if unreachable a then [`Filled;`Fillcolor "red"]
+ else []
in G.node dot na attr ;
List.iter
(fun b ->
@@ -262,7 +278,8 @@ let dump ~dir kf reached =
| UnspecifiedSequence _ -> Printf.sprintf "Seq. s%d" s.sid
| Throw _ | TryExcept _ | TryCatch _ | TryFinally _ ->
Printf.sprintf "Exn. s%d" s.sid
- in G.node dot (N.get n) [`Box;`Label label])
+ in G.node dot (N.get n)
+ [`Box;`Label (Printf.sprintf "s%d n%d: %s" s.sid n.id label)])
reached ;
G.run dot ;
G.close dot ;
@@ -276,7 +293,7 @@ let dump ~dir kf reached =
module FRmap = Kernel_function.Make_Table
(Datatype.Make
(struct
- type t = reached
+ type t = reachability
include Datatype.Serializable_undefined
let reprs = [Stmt.Map.empty]
let name = "WpReachable.reached"
@@ -289,7 +306,7 @@ module FRmap = Kernel_function.Make_Table
let dkey = Wp_parameters.register_category "reached"
-let reached = FRmap.memo
+let reachability = FRmap.memo
begin fun kf ->
let r = compute kf in
(if Wp_parameters.has_dkey dkey then
@@ -298,3 +315,28 @@ let reached = 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 2f7bc0283bc0c5cc24c0cdd7d6984cf1c3d40c95..2ef8a243c65a83a8e890e6eeed02a99c213cdbb4 100644
--- a/src/plugins/wp/wpReached.mli
+++ b/src/plugins/wp/wpReached.mli
@@ -26,7 +26,7 @@
open Cil_types
-type reached
+type reachability
(** control flow graph dedicated to smoke tests *)
val is_predicate : bool -> predicate -> bool
@@ -39,14 +39,16 @@ val is_dead_annot : code_annotation -> bool
val is_dead_code : stmt -> bool
(** Checks whether the stmt has a dead-code annotation. *)
-val reached : Kernel_function.t -> reached
+val reachability : Kernel_function.t -> reachability
(** memoized reached cfg for function *)
-val smoking : reached -> Cil_types.stmt -> bool
+val smoking : reachability -> Cil_types.stmt -> bool
(** Returns whether a stmt need a smoke tests to avoid being unreachable.
This is restricted to assignments, returns and calls not dominated
another smoking statement. *)
-val dump : dir:Datatype.Filepath.t -> Kernel_function.t -> reached -> unit
+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 e5459e75b894fda2a88fd783408471bef27d773b..bed4b06b77b25790f7c8b8c259dafcaee4d48878 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 =