From 448ae659b469b042b41ee0198ec5113bcb30499c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 5 Feb 2021 18:26:08 +0100
Subject: [PATCH] [wp] fix cfg-infos annots
---
src/plugins/wp/cfgCalculus.ml | 5 +++-
src/plugins/wp/cfgInfos.ml | 53 ++++++++++++++++++++++++++++++++++-
src/plugins/wp/wpPropId.ml | 12 ++++----
src/plugins/wp/wpPropId.mli | 1 +
4 files changed, 63 insertions(+), 8 deletions(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 7305217ee55..6b6a404b943 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -277,7 +277,10 @@ struct
| None ->
match Dyncall.get ~bhv:env.mode.bhv.b_name s with
| None ->
- WpLog.warning ~once:true "Missing dynamic-call infos." ;
+ WpLog.warning ~once:true "Missing 'calls' for %s"
+ (if Cil.is_default_behavior env.mode.bhv
+ then "default behavior"
+ else env.mode.bhv.b_name) ;
let any = WpPropId.mk_stmt_assigns_any_desc s in
W.use_assigns env.we None any (W.merge env.we w env.wk)
| Some(prop,kfs) ->
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 4d0503a4dfc..69477a06938 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -72,6 +72,51 @@ let selected ~bhv ~prop pid =
(prop = [] || WpPropId.select_by_name prop pid) &&
(bhv = [] || WpPropId.select_for_behaviors bhv pid)
+let selected_default ~bhv =
+ bhv=[] || List.mem Cil.default_behavior_name bhv
+
+let selected_name ~prop name =
+ prop=[] || WpPropId.are_selected_names prop [name]
+
+let selected_assigns ~prop = function
+ | Cil_types.WritesAny -> false
+ | _ -> selected_name ~prop "@assigns"
+
+let selected_allocates ~prop = function
+ | Cil_types.FreeAllocAny -> false
+ | _ -> (selected_name ~prop "@allocates" || selected_name ~prop "@frees")
+
+let selected_precond ~prop ip =
+ prop = [] ||
+ let tk_name = "@ensures" in
+ let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
+ WpPropId.are_selected_names prop (tk_name :: tp_names)
+
+let selected_postcond ~prop (tk,ip) =
+ prop = [] ||
+ let tk_name = "@" ^ WpPropId.string_of_termination_kind tk in
+ let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
+ WpPropId.are_selected_names prop (tk_name :: tp_names)
+
+let selected_requires ~prop (b : Cil_types.funbehavior) =
+ List.exists (selected_precond ~prop) b.b_requires
+
+let selected_call ~bhv ~prop kf =
+ bhv = [] && List.exists (selected_requires ~prop) (Annotations.behaviors kf)
+
+let selected_disjoint_complete ~bhv ~prop =
+ selected_default ~bhv &&
+ ( selected_name ~prop "@disjoint_behaviors" ||
+ selected_name ~prop "@disjoint_behaviors" )
+
+let selected_bhv ~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) ||
+ (List.exists (selected_postcond ~prop) b.b_post_cond)
+ end
+
(* -------------------------------------------------------------------------- *)
(* --- Calls --- *)
(* -------------------------------------------------------------------------- *)
@@ -143,6 +188,10 @@ let compile Key.{ kf ; bhv ; prop } =
(* Root Reachability *)
let v0 = cfg.entry_point in
Vhash.add infos.unreachable v0 false ;
+ (* Spec Iteration *)
+ if selected_disjoint_complete ~bhv ~prop ||
+ List.exists (selected_bhv ~bhv ~prop) (Annotations.behaviors kf)
+ then infos.annots <- true ;
(* Stmt Iteration *)
Shash.iter
(fun stmt (src,_) ->
@@ -154,7 +203,9 @@ let compile Key.{ kf ; bhv ; prop } =
infos.doomed <- Bag.concat infos.doomed (Bag.list pids)
else
begin
- if List.exists (selected ~bhv ~prop) pids
+ if not infos.annots &&
+ ( List.exists (selected ~bhv ~prop) pids ||
+ Fset.exists (selected_call ~bhv ~prop) fs )
then infos.annots <- true ;
infos.calls <- Fset.union fs infos.calls ;
end
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 7e4772e1af3..35df2f49a47 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -476,13 +476,13 @@ let ident_names names =
List.filter (function "" -> true
| _ as n -> '\"' <> (String.get n 0) ) names
-let pred_names p =
+let user_pred_names p =
let p_names = ident_names p.tp_statement.pred_name in
if p.tp_kind = Check then "@check"::p_names else p_names
let code_annot_names ca = match ca.annot_content with
- | AAssert (_, pred) -> "@assert" :: pred_names pred
- | AInvariant (_,_,pred) -> "@invariant":: pred_names pred
+ | AAssert (_, pred) -> "@assert" :: user_pred_names pred
+ | AInvariant (_,_,pred) -> "@invariant":: user_pred_names pred
| AVariant (term, _) -> "@variant"::(ident_names term.term_name)
| AExtended(_,_,{ext_name}) -> [Printf.sprintf "@%s" ext_name]
| _ -> [] (* TODO : add some more names ? *)
@@ -493,7 +493,7 @@ let user_prop_names p =
let open Property in match p with
| IPPredicate {ip_kind; ip_pred} ->
Format.asprintf "@@%a" Property.pretty_predicate_kind ip_kind ::
- pred_names ip_pred.ip_content
+ user_pred_names ip_pred.ip_content
| IPExtended {ie_ext={ext_name}} -> [ Printf.sprintf "@%s" ext_name ]
| IPCodeAnnot {ica_ca} -> code_annot_names ica_ca
| IPComplete {ic_bhvs} ->
@@ -511,7 +511,7 @@ let user_prop_names p =
| IPDecrease {id_ca=Some ca} -> "@decreases"::code_annot_names ca
| IPDecrease _ -> [ "@decreases" ]
| IPLemma {il_name = a; il_pred = l} ->
- let names = "@lemma"::a::pred_names l in
+ let names = "@lemma"::a::user_pred_names l in
begin
match LogicUsage.section_of_lemma a with
| LogicUsage.Toplevel _ -> names
@@ -546,7 +546,7 @@ let user_bhv_names p =
in Option.fold ~none:fors ~some:(fun b -> b.b_name :: fors) (get_behavior p)
let string_of_termination_kind = function
- Normal -> "post"
+ Normal -> "ensures"
| Exits -> "exits"
| Breaks -> "breaks"
| Continues -> "continues"
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index de80d8445d0..45d5c451922 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -79,6 +79,7 @@ val get_propid : prop_id -> string (** Unique identifier of [prop_id] *)
val get_legacy : prop_id -> string (** Unique legacy identifier of [prop_id] *)
val pp_propid : Format.formatter -> prop_id -> unit (** Print unique id of [prop_id] *)
+val user_pred_names: toplevel_predicate -> string list
val user_bhv_names: Property.identified_property -> string list
val user_prop_names: Property.identified_property -> string list
val are_selected_names: string list -> string list -> bool
--
GitLab