From 5da46e2c9836b94ca8c1ffef447964903b51f098 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 22 Oct 2021 10:29:06 +0200
Subject: [PATCH] [wp] Register dependencies for terminates
---
src/plugins/wp/cfgCalculus.ml | 16 +++++++++--
src/plugins/wp/cfgDump.ml | 3 +-
src/plugins/wp/cfgInfos.ml | 52 +++++++++++++++++++++++++----------
src/plugins/wp/cfgInfos.mli | 1 +
src/plugins/wp/cfgWP.ml | 9 +++---
src/plugins/wp/mcfg.mli | 2 +-
src/plugins/wp/wpAnnot.ml | 5 ++--
src/plugins/wp/wpAnnot.mli | 2 +-
8 files changed, 63 insertions(+), 27 deletions(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 41c62992ab8..b3553ec3aeb 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -187,9 +187,9 @@ struct
let prove_property env (p : WpPropId.pred_info) w =
if is_selected ~goal:true env p then W.add_goal env.we p w else w
- let prove_subproperty env (p : WpPropId.pred_info) prop stmt source w =
+ let prove_subproperty env (p : WpPropId.pred_info) ?deps prop stmt source w =
if is_selected ~goal:true env p
- then W.add_subgoal env.we p prop stmt source w
+ then W.add_subgoal env.we ?deps p prop stmt source w
else w
(* --- Decomposition of WP Rules --- *)
@@ -355,6 +355,16 @@ struct
List.fold_right (prove_property env) complete @@
List.fold_right (prove_property env) disjoint w
+ let do_terminates env w =
+ let deps = CfgInfos.terminates_deps env.mode.infos in
+ match env.terminates with
+ | Some t
+ when is_default_bhv env.mode && is_selected ~goal:true env t &&
+ not @@ Property.Set.is_empty deps ->
+ let return = Kernel_function.find_return env.mode.kf in
+ prove_subproperty env t ~deps Logic_const.ptrue return FromReturn w
+ | _ -> w
+
let do_global_init env w =
I.process_global_init env.we env.mode.kf @@
W.scope env.we [] SC_Global w
@@ -378,7 +388,6 @@ struct
(* frame-in *)
W.scope env.we formals SC_Frame_in w
-
let do_post env ~formals (b : CfgAnnot.behavior) w =
W.label env.we None Clabels.post @@
W.scope env.we formals SC_Frame_out @@
@@ -428,6 +437,7 @@ struct
let bhv = CfgAnnot.get_behavior_goals kf ~smoking ~exits mode.bhv in
begin
W.close env.we @@
+ do_terminates env @@
do_global_init env @@
do_preconditions env ~formals bhv @@
do_complete_disjoint env @@
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index a7592df0bfb..c15ac2a858f 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/src/plugins/wp/cfgDump.ml
@@ -106,7 +106,8 @@ let add_goal env (pid,pred) k =
Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
-let add_subgoal env (pid, t_pred) prop stmt _source k =
+let add_subgoal env (pid, t_pred) ?deps prop stmt _source k =
+ ignore deps ;
let u = node () in
if Wp_parameters.debug_atleast 1 then
Format.fprintf !out " %a [ color=red , label=\"Prove %a @@ %a (%a)\" ] ;@."
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 2fc2e6b4a4f..f45fdfba450 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -23,6 +23,7 @@
module Cfg = Interpreted_automata
module Fset = Kernel_function.Set
module Sset = Cil_datatype.Stmt.Set
+module Pset = Property.Set
module Shash = Cil_datatype.Stmt.Hashtbl
(* -------------------------------------------------------------------------- *)
@@ -39,6 +40,7 @@ type t = {
mutable doomed : WpPropId.prop_id Bag.t;
mutable calls : Kernel_function.Set.t;
mutable no_variant_loops : Sset.t;
+ mutable terminates_deps : Pset.t;
}
(* -------------------------------------------------------------------------- *)
@@ -61,6 +63,8 @@ let unreachable infos v =
not @@ CheckPath.check_path checkpath cfg.entry_point v
| _ -> true
+let terminates_deps infos = infos.terminates_deps
+
(* -------------------------------------------------------------------------- *)
(* --- Selected Properties --- *)
(* -------------------------------------------------------------------------- *)
@@ -171,17 +175,26 @@ let collect_calls ~bhv kf stmt =
(* --- No variant loops --- *)
(* -------------------------------------------------------------------------- *)
-let collect_loops_no_variant stmt =
+let collect_loops_no_variant kf stmt =
let open Cil_types in
let fold_no_variant _ = function
- | { annot_content = AVariant _ } -> (&&) false
- | _ -> (&&) true
+ | { annot_content = AVariant v } as ca -> fun _ -> Some (ca, v)
+ | _ -> Extlib.id
+ in
+ let props_of_v ca v =
+ let (d, _), (p, _) = WpStrategy.mk_variant_properties kf stmt ca v in
+ Pset.union
+ (Pset.singleton @@ WpPropId.property_of_id d)
+ (Pset.singleton @@ WpPropId.property_of_id p)
in
match stmt.skind with
- | Loop _ when Annotations.fold_code_annot fold_no_variant stmt true ->
- Sset.singleton stmt
+ | Loop _ ->
+ begin match Annotations.fold_code_annot fold_no_variant stmt None with
+ | None -> Sset.singleton stmt, Pset.empty
+ | Some (ca, v) -> Sset.empty, props_of_v ca (fst v)
+ end
| _ ->
- Sset.empty
+ Sset.empty, Pset.empty
(* -------------------------------------------------------------------------- *)
(* --- Memoization Key --- *)
@@ -265,7 +278,8 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
annots = false ;
doomed = Bag.empty ;
calls = Fset.empty ;
- no_variant_loops = Sset.empty
+ no_variant_loops = Sset.empty ;
+ terminates_deps = Pset.empty ;
} in
let behaviors = Annotations.behaviors kf in
(* Inits *)
@@ -283,7 +297,7 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
Shash.iter
(fun stmt (src,_) ->
let fs = collect_calls ~bhv kf stmt in
- let nv_loops = collect_loops_no_variant stmt in
+ let nv_loops, term_deps = collect_loops_no_variant kf stmt in
let dead = unreachable infos src in
let ca = CfgAnnot.get_code_assertions kf stmt in
let ca_pids = List.map fst ca.code_verified in
@@ -306,6 +320,8 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
infos.calls <- Fset.union fs infos.calls ;
infos.no_variant_loops <-
Sset.union nv_loops infos.no_variant_loops ;
+ infos.terminates_deps <-
+ Pset.union term_deps infos.terminates_deps
end
) cfg.stmt_table ;
(* Dead Post Conditions *)
@@ -328,15 +344,21 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
(fun p -> if WpPropId.filter_status p then WpAnnot.set_unreachable p)
infos.doomed ;
(* Trivial terminates *)
- if Kernel_function.is_definition kf then
- begin match CfgAnnot.get_terminates_goal kf with
- | Some (id, _t)
- when selected_terminates ~prop kf
+ let infos =
+ if Kernel_function.is_definition kf then
+ match CfgAnnot.get_terminates_goal kf with
+ | Some (id, _)
+ when
+ selected_terminates ~prop kf
&& infos.calls = Fset.empty
&& infos.no_variant_loops = Sset.empty ->
- WpAnnot.set_trivially_terminates id
- | _ -> ()
- end ;
+ WpAnnot.set_trivially_terminates id infos.terminates_deps ;
+ (* Drop dependencies for this terminates, we've used it. *)
+ { infos with terminates_deps = Pset.empty }
+ | _ ->
+ infos
+ else infos
+ in
(* Collected Infos *)
infos
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
index 472a321933a..ad6f782ba06 100644
--- a/src/plugins/wp/cfgInfos.mli
+++ b/src/plugins/wp/cfgInfos.mli
@@ -38,5 +38,6 @@ 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
+val terminates_deps : t -> Property.Set.t
(**************************************************************************)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 869a3f39158..7c5edf076e1 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -438,10 +438,11 @@ struct
(F.varsp goal) hs
in xs , hs , goal
- let add_vc target ?(warn=Warning.Set.empty) pred vcs =
+ let add_vc
+ target ?(warn=Warning.Set.empty) ?(deps=Property.Set.empty) pred vcs =
let xs , hs , goal = introduction pred in
let hyps = Conditions.intros hs Conditions.nil in
- let vc = { empty_vc with goal=goal ; vars=xs ; hyps=hyps ; warn=warn } in
+ let vc = { empty_vc with goal ; vars=xs ; hyps ; warn ; deps } in
Gmap.add target (Splitter.singleton vc) vcs
(* ------------------------------------------------------------------------ *)
@@ -507,7 +508,7 @@ struct
let vcs = add_vc (Gprop gpid) ~warn goal wp.vcs in
{ wp with vcs = vcs })
- let add_subgoal wenv (gpid, _) predicate stmt source wp = in_wenv wenv wp
+ let add_subgoal wenv (gpid,_) ?deps predicate stmt src wp = in_wenv wenv wp
(fun env wp ->
let outcome = Warning.catch
~severe:true ~effect:"Degenerated goal"
@@ -516,7 +517,7 @@ struct
| Warning.Result(warn,goal) -> warn,goal
| Warning.Failed warn -> warn,F.p_false
in
- let vcs = add_vc (Gsource(gpid, stmt, source)) ~warn goal wp.vcs in
+ let vcs = add_vc (Gsource(gpid, stmt, src)) ~warn ?deps goal wp.vcs in
{ wp with vcs = vcs })
let add_assigns wenv (gpid,ainfo) wp = in_wenv wenv wp
diff --git a/src/plugins/wp/mcfg.mli b/src/plugins/wp/mcfg.mli
index 15905e4eab2..3ecd5a5f9a2 100644
--- a/src/plugins/wp/mcfg.mli
+++ b/src/plugins/wp/mcfg.mli
@@ -67,7 +67,7 @@ module type S = sig
val add_axiom : WpPropId.prop_id -> LogicUsage.logic_lemma -> unit
val add_hyp : t_env -> WpPropId.pred_info -> t_prop -> t_prop
val add_goal : t_env -> WpPropId.pred_info -> t_prop -> t_prop
- val add_subgoal : t_env -> WpPropId.pred_info ->
+ val add_subgoal : t_env -> WpPropId.pred_info -> ?deps:Property.Set.t ->
predicate -> stmt -> WpPropId.effect_source -> t_prop -> t_prop
val add_assigns : t_env -> WpPropId.assigns_info -> t_prop -> t_prop
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 7f6b34561c7..7a0dc8f3971 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -89,11 +89,12 @@ let wp_trivially_terminates =
~correctness:[] (* TBC *)
~tuning:[] (* TBC *)
-let set_trivially_terminates p =
+let set_trivially_terminates p hyps =
incr trivial_terminates ;
Wp_parameters.result "[CFG] Goal %a : Valid (Trivial)" WpPropId.pp_propid p ;
let pid = WpPropId.property_of_id p in
- Property_status.emit wp_trivially_terminates ~hyps:[] pid Property_status.True
+ let hyps = Property.Set.elements hyps in
+ Property_status.emit wp_trivially_terminates ~hyps pid Property_status.True
(* -------------------------------------------------------------------------- *)
(* --- Preconditions at Callsites --- *)
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index 171a83e4299..a2b4ebcf851 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -36,7 +36,7 @@ val unreachable_proved : int ref
val unreachable_failed : int ref
val trivial_terminates : int ref
val set_unreachable : WpPropId.prop_id -> unit
-val set_trivially_terminates : WpPropId.prop_id -> unit
+val set_trivially_terminates : WpPropId.prop_id -> Property.Set.t -> unit
type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns
--
GitLab