From 64c8febbee372a576383a23daf0206bc7b346b30 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 8 Feb 2021 19:13:39 +0100
Subject: [PATCH] [wp] (some) smoke fixes
---
src/plugins/wp/cfgAnnot.ml | 26 +++++++++++++++++---------
src/plugins/wp/cfgAnnot.mli | 13 ++++++++-----
src/plugins/wp/cfgCalculus.ml | 14 +++++++++++---
src/plugins/wp/cfgInfos.ml | 15 ++++++++++-----
src/plugins/wp/wpAnnot.mli | 1 +
5 files changed, 47 insertions(+), 22 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 3ed9641b471..454dba14289 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -126,13 +126,12 @@ let get_behavior kf
let p_asgn, e_asgn =
normalize_assigns kf ki exits bhv ~active bhv.b_assigns in
let smokes =
- if smoking then
- if bhv.b_assumes = [] && bhv.b_requires = [] then [] else
- let bname =
- if Cil.is_default_behavior bhv then "default" else bhv.b_name in
- let id = bname ^ "_requires" in
- let doomed = Property.ip_requires_of_behavior kf Kglobal bhv in
- [smoke kf ~id ~doomed ()]
+ if smoking && bhv.b_requires <> [] then
+ let bname =
+ if Cil.is_default_behavior bhv then "default" else bhv.b_name in
+ let id = bname ^ "_requires" in
+ let doomed = Property.ip_requires_of_behavior kf Kglobal bhv in
+ [smoke kf ~id ~doomed ()]
else []
in
{
@@ -320,7 +319,7 @@ let get_code_assertions ?smoking kf stmt =
| None -> ca
| Some r ->
if WpReached.smoking r stmt then
- let s = smoke kf ~id:"deadcode" ~unreachable:stmt () in
+ let s = smoke kf ~id:"dead_code" ~unreachable:stmt () in
{ ca with code_verified = s :: ca.code_verified }
else ca
@@ -333,6 +332,8 @@ type loop_contract = {
loop_established: WpPropId.pred_info list;
(* to be assumed for loop current *)
loop_invariants: WpPropId.pred_info list;
+ (* to be proved after loop invariants *)
+ loop_smoke: WpPropId.pred_info list;
(* to be verified after loop body *)
loop_preserved: WpPropId.pred_info list;
(* assigned by loop body *)
@@ -344,6 +345,7 @@ let reverse_loop_contract l = {
loop_invariants = List.rev l.loop_invariants ;
loop_preserved = List.rev l.loop_preserved ;
loop_assigns = List.rev l.loop_assigns ;
+ loop_smoke = List.rev l.loop_smoke ;
}
let default_assigns stmt l =
@@ -403,11 +405,17 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
loop_established = [] ;
loop_invariants = [] ;
loop_preserved = [] ;
+ loop_smoke = [] ;
loop_assigns = [] ;
}
end)
-let get_loop_contract kf stmt = LoopContract.get (kf,stmt)
+let get_loop_contract ?(smoking=false) kf stmt =
+ let lc = LoopContract.get (kf,stmt) in
+ if smoking && not (WpReached.is_dead_code stmt) then
+ let g = smoke kf ~id:"dead_loop" ~unreachable:stmt () in
+ { lc with loop_smoke = g :: lc.loop_smoke }
+ else lc
(* -------------------------------------------------------------------------- *)
(* --- Clear Tablesnts --- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 9ba615b4305..a2f997986a8 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -72,16 +72,19 @@ val get_code_assertions :
type loop_contract = {
(** to be verified at loop entry *)
- loop_established: pred_info list;
+ loop_established: WpPropId.pred_info list;
(** to be assumed for loop current *)
- loop_invariants: pred_info list;
+ loop_invariants: WpPropId.pred_info list;
+ (** to be proved after loop invariants *)
+ loop_smoke: WpPropId.pred_info list;
(** to be verified after loop body *)
- loop_preserved: pred_info list;
+ loop_preserved: WpPropId.pred_info list;
(** assigned by loop body *)
- loop_assigns: assigns_full_info list;
+ loop_assigns: WpPropId.assigns_full_info list;
}
-val get_loop_contract : kernel_function -> stmt -> loop_contract
+val get_loop_contract : ?smoking:bool ->
+ kernel_function -> stmt -> loop_contract
(* -------------------------------------------------------------------------- *)
(* --- Property Accessors : Call Contracts --- *)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 431b3df41f3..10e8f52ca38 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -98,10 +98,11 @@ let is_active_mode ~mode ~goal (p: Property.t) =
| IPDecrease { id_ca = None } -> is_default_bhv mode
| IPDecrease { id_ca = Some ca } -> is_selected_ca mode ~goal ca
| IPComplete _ | IPDisjoint _ -> is_default_bhv mode
+ | IPOther _ -> true
| IPFrom _ | IPGlobalInvariant _ | IPTypeInvariant _ ->
(*TODO: is it in pass or not ? *) assert false
| IPAxiomatic _ | IPAxiom _ | IPLemma _
- | IPOther _ | IPExtended _ | IPBehavior _
+ | IPExtended _ | IPBehavior _
| IPReachable _ | IPPropertyInstance _
-> assert false (* n/a *)
@@ -220,7 +221,13 @@ struct
W.switch env.we s value
(List.map (fun (e,v) -> [e], wp env v) cases)
(wp env default)
- | Loop _ -> loop env a s (CfgAnnot.get_loop_contract env.mode.kf s)
+ | Loop _ ->
+ let m = env.mode in
+ let smoking =
+ is_default_bhv m &&
+ WpLog.SmokeTests.get () &&
+ WpLog.SmokeDeadloop.get () in
+ loop env a s (CfgAnnot.get_loop_contract ~smoking m.kf s)
| Edges -> successors env a
(* Compute loops *)
@@ -233,6 +240,7 @@ struct
List.fold_right (use_assigns env) lc.loop_assigns @@
W.label env.we None loop_current @@
List.fold_right (use_property env) lc.loop_invariants @@
+ List.fold_right (prove_property env) lc.loop_smoke @@
let q =
List.fold_right (prove_property env) lc.loop_preserved @@
List.fold_right (prove_assigns env) lc.loop_assigns @@
@@ -382,7 +390,7 @@ struct
if body <> None &&
is_default_bhv mode &&
WpLog.SmokeTests.get () &&
- WpLog.SmokeDeadcall.get ()
+ WpLog.SmokeDeadcode.get ()
then Some (WpReached.reachability kf) else None in
let env = {
mode ; props ; body ; succ ; dead ;
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index ac9c245b0ad..adcec5bbcc8 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -113,11 +113,12 @@ let selected_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
begin
(selected_assigns ~prop b.b_assigns) ||
(selected_allocates ~prop b.b_allocation) ||
+ (Wp_parameters.SmokeTests.get () && b.b_requires <> []) ||
(List.exists (selected_postcond ~prop) b.b_post_cond)
end
let selected_main_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
- (bhv = [] || List.mem b.b_name bhv) && (selected_requires ~prop) b
+ (bhv = [] || List.mem b.b_name bhv) && (selected_requires ~prop b)
(* -------------------------------------------------------------------------- *)
(* --- Calls --- *)
@@ -225,10 +226,12 @@ let compile Key.{ kf ; bhv ; prop } =
let ca = CfgAnnot.get_code_assertions kf stmt in
let ca_pids = List.map fst ca.code_verified in
let loop_pids = loop_contract_pids kf stmt in
- if dead then begin
- infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
- infos.doomed <- Bag.concat infos.doomed (Bag.list loop_pids) ;
- end else
+ if dead then
+ begin
+ infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
+ infos.doomed <- Bag.concat infos.doomed (Bag.list loop_pids) ;
+ end
+ else
begin
if not infos.annots &&
( List.exists (selected ~bhv ~prop) ca_pids ||
@@ -239,6 +242,8 @@ let compile Key.{ kf ; bhv ; prop } =
end
) cfg.stmt_table ;
end body ;
+ (* Doomed *)
+ Bag.iter WpAnnot.set_unreachable infos.doomed ;
(* Collected Infos *)
infos
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index 211c0ee80a7..1faa344c267 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -34,6 +34,7 @@ open Cil_types
val unreachable_proved : int ref
val unreachable_failed : int ref
+val set_unreachable : WpPropId.prop_id -> unit
type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns
--
GitLab