From 69262e6a30d8127eb6f6cd3b874c2ed8c9da2de2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 9 Feb 2021 11:03:06 +0100
Subject: [PATCH] [wp] smoke unreachable stmt
---
src/plugins/wp/cfgAnnot.ml | 16 ++++-----
src/plugins/wp/cfgAnnot.mli | 5 +--
src/plugins/wp/cfgCalculus.ml | 11 +++---
src/plugins/wp/cfgGenerator.ml | 5 ++-
src/plugins/wp/cfgInfos.ml | 61 +++++++++++++++++++++++-----------
src/plugins/wp/cfgInfos.mli | 4 ++-
6 files changed, 66 insertions(+), 36 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 454dba14289..2db21013e62 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -29,6 +29,9 @@ open Cil_types
let smoke kf ~id ?doomed ?unreachable () =
WpPropId.mk_smoke kf ~id ?doomed ?unreachable () , Logic_const.pfalse
+let get_unreachable kf stmt =
+ WpPropId.mk_smoke kf ~id:"unreachabled" ~unreachable:stmt ()
+
(* -------------------------------------------------------------------------- *)
(* --- Memoization --- *)
(* -------------------------------------------------------------------------- *)
@@ -313,15 +316,12 @@ module CodeAssertions = WpContext.StaticGenerator(CodeKey)
}
end)
-let get_code_assertions ?smoking kf stmt =
+let get_code_assertions ?(smoking=false) kf stmt =
let ca = CodeAssertions.get (kf,stmt) in
- match smoking with
- | None -> ca
- | Some r ->
- if WpReached.smoking r stmt then
- let s = smoke kf ~id:"dead_code" ~unreachable:stmt () in
- { ca with code_verified = s :: ca.code_verified }
- else ca
+ if smoking then
+ let s = smoke kf ~id:"dead_code" ~unreachable:stmt () in
+ { ca with code_verified = s :: ca.code_verified }
+ else ca
(* -------------------------------------------------------------------------- *)
(* --- Loop Invariants --- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index a2f997986a8..b7c640af513 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -63,8 +63,9 @@ type code_assertions = {
}
val get_code_assertions :
- ?smoking:WpReached.reachability ->
- kernel_function -> stmt -> code_assertions
+ ?smoking:bool -> kernel_function -> stmt -> code_assertions
+
+val get_unreachable : kernel_function -> stmt -> WpPropId.prop_id
(* -------------------------------------------------------------------------- *)
(* --- Property Accessors : Loop Contracts --- *)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 10e8f52ca38..514b05e8f4d 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -132,7 +132,7 @@ struct
props: props;
body: Cfg.automaton option;
succ: Cfg.vertex -> Cfg.G.edge list;
- dead: WpReached.reachability option;
+ dead: stmt -> bool ;
we: W.t_env;
wp: W.t_prop option Vhash.t; (* None is used for non-dag detection *)
mutable wk: W.t_prop; (* end point *)
@@ -200,8 +200,8 @@ struct
try
Cil.CurrentLoc.set (Stmt.loc s) ;
let smoking =
- if is_default_bhv env.mode then env.dead else None in
- let ca = CfgAnnot.get_code_assertions ?smoking env.mode.kf s in
+ is_default_bhv env.mode && env.dead s in
+ let ca = CfgAnnot.get_code_assertions ~smoking env.mode.kf s in
let pi =
W.label env.we (Some s) (Clabels.stmt s) @@
List.fold_right (prove_property env) ca.code_verified @@
@@ -391,9 +391,10 @@ struct
is_default_bhv mode &&
WpLog.SmokeTests.get () &&
WpLog.SmokeDeadcode.get ()
- then Some (WpReached.reachability kf) else None in
+ then CfgInfos.smoking infos else (fun _ -> false) in
let env = {
- mode ; props ; body ; succ ; dead ;
+ mode ; props ; body ;
+ succ ; dead ;
we = W.new_env kf ;
wp = Vhash.create 32 ;
wk = W.empty ;
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index c6872377e71..d67d5176378 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -50,7 +50,10 @@ let get_kf_infos model kf ?bhv ?prop () =
Wp_parameters.warning ~current:false ~once:true "Missing RTE guards"
else if Wp_parameters.RTE.get () then
WpRTE.generate model kf ;
- CfgInfos.get kf ?bhv ?prop ()
+ let smoking =
+ Wp_parameters.SmokeTests.get () &&
+ Wp_parameters.SmokeDeadcode.get () in
+ CfgInfos.get kf ~smoking ?bhv ?prop ()
let empty_default_behavior : funbehavior = {
b_name = Cil.default_behavior_name ;
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index adcec5bbcc8..342ba0fa450 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -28,11 +28,12 @@ module Shash = Cil_datatype.Stmt.Hashtbl
(* --- Compute Kernel-Function & CFG Infos for WP --- *)
(* -------------------------------------------------------------------------- *)
-module Reachability = Graph.Path.Check(Cfg.G)
+module CheckPath = Graph.Path.Check(Cfg.G)
type t = {
body : Cfg.automaton option ;
- reachability : Reachability.path_checker option ;
+ checkpath : CheckPath.path_checker option ;
+ reachability : WpReached.reachability option ;
mutable annots : bool; (* has goals to prove *)
mutable doomed : WpPropId.prop_id Bag.t;
mutable calls : Kernel_function.Set.t;
@@ -47,11 +48,15 @@ let calls infos = infos.calls
let annots infos = infos.annots
let doomed infos = infos.doomed
+let wpreached s = function
+ | None -> false
+ | Some reachability -> WpReached.smoking reachability s
+let smoking infos s = wpreached s infos.reachability
+
let unreachable infos v =
- match infos.body, infos.reachability with
- | Some cfg , Some reach ->
- let entry = cfg.entry_point in
- not @@ Reachability.check_path reach entry v
+ match infos.body, infos.checkpath with
+ | Some cfg , Some checkpath ->
+ not @@ CheckPath.check_path checkpath cfg.entry_point v
| _ -> true
(* -------------------------------------------------------------------------- *)
@@ -108,12 +113,12 @@ let selected_disjoint_complete kf ~bhv ~prop =
( selected_clause ~prop "@complete_behaviors" Annotations.complete kf ||
selected_clause ~prop "@disjoint_behaviors" Annotations.disjoint kf )
-let selected_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
+let selected_bhv ~smoking ~bhv ~prop (b : Cil_types.funbehavior) =
(bhv = [] || List.mem b.b_name bhv) &&
begin
(selected_assigns ~prop b.b_assigns) ||
(selected_allocates ~prop b.b_allocation) ||
- (Wp_parameters.SmokeTests.get () && b.b_requires <> []) ||
+ (smoking && b.b_requires <> []) ||
(List.exists (selected_postcond ~prop) b.b_post_cond)
end
@@ -154,25 +159,37 @@ let collect_calls ~bhv stmt =
module Key =
struct
- type t = { kf: Kernel_function.t ; bhv : string list ; prop : string list }
+ type t = {
+ kf: Kernel_function.t ;
+ smoking: bool ;
+ bhv : string list ;
+ prop : string list ;
+ }
+
let compare a b =
let cmp = Kernel_function.compare a.kf b.kf in
if cmp <> 0 then cmp else
- let cmp = Stdlib.compare a.bhv b.bhv in
+ let cmp = Stdlib.compare a.smoking b.smoking in
if cmp <> 0 then cmp else
- Stdlib.compare a.prop b.prop
+ let cmp = Stdlib.compare a.bhv b.bhv in
+ if cmp <> 0 then cmp else
+ Stdlib.compare a.prop b.prop
+
let pp_filter kind fmt xs =
match xs with
| [] -> ()
| x::xs ->
Format.fprintf fmt "~%s:%s" kind x ;
List.iter (Format.fprintf fmt ",%s") xs
+
let pretty fmt k =
begin
Kernel_function.pretty fmt k.kf ;
+ pp_filter "smoking" fmt (if k.smoking then ["true"] else []) ;
pp_filter "bhv" fmt k.bhv ;
pp_filter "prop" fmt k.prop ;
end
+
end
(* -------------------------------------------------------------------------- *)
@@ -193,19 +210,20 @@ let loop_contract_pids kf stmt =
List.fold_right add_assigns invs.loop_assigns []
| _ -> []
-let compile Key.{ kf ; bhv ; prop } =
- let body, reachability =
+let compile Key.{ kf ; smoking ; bhv ; prop } =
+ let body, checkpath, reachability =
if Kernel_function.has_definition kf then
let cfg = Cfg.get_automaton kf in
- Some cfg, Some (Reachability.create cfg.graph)
- else None, None
+ Some cfg,
+ Some (CheckPath.create cfg.graph),
+ if smoking then Some (WpReached.reachability kf) else None
+ else None, None, None
in
let infos = {
- body ;
+ body ; checkpath ; reachability ;
annots = false ;
doomed = Bag.empty ;
calls = Fset.empty ;
- reachability ;
} in
let behaviors = Annotations.behaviors kf in
(* Inits *)
@@ -216,7 +234,7 @@ let compile Key.{ kf ; bhv ; prop } =
begin fun (cfg : Cfg.automaton) ->
(* Spec Iteration *)
if selected_disjoint_complete kf ~bhv ~prop ||
- (List.exists (selected_bhv ~bhv ~prop) behaviors)
+ (List.exists (selected_bhv ~smoking ~bhv ~prop) behaviors)
then infos.annots <- true ;
(* Stmt Iteration *)
Shash.iter
@@ -228,6 +246,9 @@ let compile Key.{ kf ; bhv ; prop } =
let loop_pids = loop_contract_pids kf stmt in
if dead then
begin
+ if wpreached stmt reachability then
+ (let p = CfgAnnot.get_unreachable kf stmt in
+ infos.doomed <- Bag.append infos.doomed p) ;
infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
infos.doomed <- Bag.concat infos.doomed (Bag.list loop_pids) ;
end
@@ -259,7 +280,9 @@ module Generator = WpContext.StaticGenerator(Key)
let compile = compile
end)
-let get kf ?(bhv=[]) ?(prop=[]) () = Generator.get { kf ; bhv ; prop }
+let get kf ?(smoking=false) ?(bhv=[]) ?(prop=[]) () =
+ Generator.get { kf ; smoking ; bhv ; prop }
+
let clear () = Generator.clear ()
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
index 89ff00c7da7..3363925581f 100644
--- a/src/plugins/wp/cfgInfos.mli
+++ b/src/plugins/wp/cfgInfos.mli
@@ -27,7 +27,8 @@ type t
module Cfg = Interpreted_automata
(** Memoized *)
-val get : Kernel_function.t -> ?bhv:string list -> ?prop:string list ->
+val get : Kernel_function.t ->
+ ?smoking:bool -> ?bhv:string list -> ?prop:string list ->
unit -> t
val clear : unit -> unit
@@ -35,6 +36,7 @@ val body : t -> Cfg.automaton option
val annots : t -> bool
val doomed : t -> WpPropId.prop_id Bag.t
val calls : t -> Kernel_function.Set.t
+val smoking : t -> Cil_types.stmt -> bool
val unreachable : t -> Cfg.vertex -> bool
(**************************************************************************)
--
GitLab