From 28b2ccccedd3245686e2e9a4728c425819de1620 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 18 Jan 2021 14:10:37 +0100
Subject: [PATCH] [wp] fix use/verify predicate kinds
---
.../ast_queries/logic_utils.ml | 3 +
.../ast_queries/logic_utils.mli | 9 +++
src/plugins/wp/wpAnnot.ml | 58 +++++++++++--------
src/plugins/wp/wpReached.ml | 2 +-
src/plugins/wp/wpStrategy.ml | 43 ++++++++------
5 files changed, 72 insertions(+), 43 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 13faf94caec..e6b2f808798 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -2229,6 +2229,9 @@ let lhost_c_type thost =
| _ -> assert false)
| TResult ty -> ty
+let use_predicate = function Assert | Admit -> true | Check -> false
+let verify_predicate = function Assert | Check -> true | Admit -> false
+
let is_assert ca =
match ca.annot_content with AAssert (_, p) -> p.tp_kind = Assert | _ -> false
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 71579a36bf0..1e0ddf5ad41 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -444,6 +444,15 @@ val merge_funspec :
val clear_funspec: funspec -> unit
(** {2 Discriminating code_annotations} *)
+
+(** Checks if a predicate kind can be used as an hypothesis or requirement.
+ It is true for `Admit` and `Assert`, and false for `Check`. *)
+val use_predicate : predicate_kind -> bool
+
+(** Checks if a predicate kind shall be put under verification.
+ It is true for `Assert` and `Check`, and false for `Admit`. *)
+val verify_predicate : predicate_kind -> bool
+
(** Functions below allows to test a special kind of code_annotation.
Use them in conjunction with {!Annotations.get_filter} to retrieve
a particular kind of annotations associated to a statement. *)
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index a64dbebde90..c6ff88f1a14 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -28,6 +28,7 @@ let debug fmt = Wp_parameters.debug ~dkey fmt
open Cil_types
open Cil_datatype
+open Logic_utils
(* -------------------------------------------------------------------------- *)
(* --- Selection of relevant assigns and postconditions --- *)
@@ -761,7 +762,7 @@ let add_called_post called_kf termination_kind acc =
let kind = WpStrategy.AcallHyp called_kf in
let assumes = (Ast_info.behavior_assumes b) in
let add_post acc (tk, p) =
- if tk = termination_kind && p.ip_content.tp_kind <> Check
+ if tk = termination_kind && use_predicate p.ip_content.tp_kind
then WpStrategy.add_prop_call_post acc kind called_kf b tk ~assumes p
else acc
in List.fold_left add_post acc b.b_post_cond
@@ -838,7 +839,8 @@ let add_variant_annot config s ca var_exp loop_entry loop_back =
in loop_entry, loop_back
let add_loop_invariant_annot config vloop s ca b_list inv acc =
- let only_check = inv.tp_kind = Check in
+ let hyp = use_predicate inv.tp_kind in
+ let goal = verify_predicate inv.tp_kind in
let inv = inv.tp_statement in
let assigns, loop_entry, loop_back , loop_core = acc in
(* we have to prove that inv is true for each edge that goes
@@ -849,22 +851,29 @@ let add_loop_invariant_annot config vloop s ca b_list inv acc =
| TBRpart (* TODO: PKPartial *)
->
begin
- let loop_entry = add_prop_loop_inv ~established:true config loop_entry
- WpStrategy.Agoal s ca inv in
- let loop_back = add_prop_loop_inv ~established:false config loop_back
- WpStrategy.Agoal s ca inv in
+ let loop_entry =
+ if goal then
+ add_prop_loop_inv ~established:true config loop_entry
+ WpStrategy.Agoal s ca inv
+ else loop_entry in
+ let loop_back =
+ if goal then
+ add_prop_loop_inv ~established:false config loop_back
+ WpStrategy.Agoal s ca inv
+ else loop_back in
let loop_core =
- if only_check then loop_core
- else
+ if hyp then
add_prop_inv_fixpoint config loop_core WpStrategy.Ahyp s ca inv
- in
+ else loop_core in
assigns, loop_entry , loop_back , loop_core
end
- | TBRhyp when not only_check ->
- let kind = WpStrategy.Ahyp in
- let loop_core = add_prop_inv_fixpoint config loop_core kind s ca inv
- in assigns, loop_entry , loop_back , loop_core
- | TBRhyp | TBRno -> acc
+ | TBRhyp ->
+ if hyp then
+ let kind = WpStrategy.Ahyp in
+ let loop_core = add_prop_inv_fixpoint config loop_core kind s ca inv
+ in assigns, loop_entry , loop_back , loop_core
+ else acc
+ | TBRno -> acc
(** Returns the annotations for the three edges of the loop node:
* - loop_entry : goals for the edge entering in the loop
@@ -952,24 +961,25 @@ let get_stmt_annots config v s =
let acc = match is_annot_for_config config v s b_list with
| TBRno -> acc
| TBRhyp ->
- if p.tp_kind = Check then acc
- else
+ if use_predicate p.tp_kind then
let b_acc =
WpStrategy.add_prop_assert
b_acc WpStrategy.Ahyp kf s a p.tp_statement
in (b_acc, (a_acc, e_acc))
+ else acc
| TBRok | TBRpart ->
let id = WpPropId.mk_assert_id config.kf s a in
let goal = goal_to_select config id in
- if p.tp_kind = Check && not goal then acc
- else
- let kind =
- WpStrategy.(if p.tp_kind = Check then Agoal else Aboth goal)
- in
+ let add, kind =
+ match p.tp_kind with
+ | Admit -> true, WpStrategy.Ahyp
+ | Assert -> true, Aboth goal
+ | Check -> goal, Agoal
+ in if add then
let b_acc =
WpStrategy.add_prop_assert b_acc kind kf s a p.tp_statement
- in
- (b_acc, (a_acc, e_acc))
+ in (b_acc, (a_acc, e_acc))
+ else acc
in acc
| AAllocation (_b_list, _frees_allocates) ->
(* [PB] TODO *) acc
@@ -1136,7 +1146,7 @@ let add_global_annotations annots =
linfo.l_var_info.lv_name;
()
| Dlemma (name,_,_,_,p,_,_) ->
- if p.tp_kind <> Check then
+ if use_predicate p.tp_kind then
WpStrategy.add_axiom annots (LogicUsage.logic_lemma name)
and do_globals gs = List.iter do_global gs in
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index af993718983..549725d8cf1 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -92,7 +92,7 @@ let is_dead_annot ca =
is_unrolled_completely spec
| AAssert([],p)
| AInvariant([],_,p) ->
- p.tp_kind <> Check && is_predicate false p.tp_statement
+ Logic_utils.use_predicate p.tp_kind && is_predicate false p.tp_statement
| _ -> false
let is_dead_code stmt =
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index 2488ade0d3f..bace35e939a 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -24,6 +24,7 @@ let dkey = Wp_parameters.register_category "strategy" (* debugging key *)
let debug fmt = Wp_parameters.debug ~dkey fmt
open Cil_types
+open Logic_utils
open LogicUsage
(* -------------------------------------------------------------------------- *)
@@ -171,7 +172,7 @@ let add_prop_fct_pre_bhv acc kind kf bhv =
Logic_const.(pat (p,pre_label))
in
let requires =
- List.filter (fun x -> x.ip_content.tp_kind <> Check) bhv.b_requires
+ List.filter (fun x -> use_predicate x.ip_content.tp_kind) bhv.b_requires
in
let requires = Logic_const.pands (List.map norm_pred requires) in
let assumes = Logic_const.pands (List.map norm_pred bhv.b_assumes) in
@@ -183,21 +184,23 @@ let add_prop_fct_pre_bhv acc kind kf bhv =
add_prop acc kind id p
let add_prop_fct_pre acc kind kf bhv ~assumes pre =
- if pre.ip_content.tp_kind = Check then acc else begin
+ if use_predicate pre.ip_content.tp_kind then begin
let id = WpPropId.mk_pre_id kf Kglobal bhv pre in
let labels = NormAtLabels.labels_fct_pre in
let p = Logic_const.pred_of_id_pred pre in
let p = Logic_const.(pat (p,pre_label)) in
let p = normalize id ?assumes labels p in
add_prop acc kind id p
- end
+ end else acc
let add_prop_fct_post acc kind kf bhv tkind post =
- let id = WpPropId.mk_fct_post_id kf bhv (tkind, post) in
- let labels = NormAtLabels.labels_fct_post in
- let p = Logic_const.pred_of_id_pred post in
- let p = normalize id labels p in
- add_prop acc kind id p
+ if verify_predicate post.ip_content.tp_kind then begin
+ let id = WpPropId.mk_fct_post_id kf bhv (tkind, post) in
+ let labels = NormAtLabels.labels_fct_post in
+ let p = Logic_const.pred_of_id_pred post in
+ let p = normalize id labels p in
+ add_prop acc kind id p
+ end else acc
let add_prop_fct_bhv_pre acc kind kf bhv =
let assumes = None in
@@ -206,11 +209,13 @@ let add_prop_fct_bhv_pre acc kind kf bhv =
List.fold_left add acc bhv.b_assumes
let add_prop_stmt_pre acc kind kf s bhv ~assumes pre =
- let id = WpPropId.mk_pre_id kf (Kstmt s) bhv pre in
- let labels = NormAtLabels.labels_stmt_pre ~kf s in
- let p = Logic_const.pred_of_id_pred pre in
- let p = normalize id labels ?assumes p in
- add_prop acc kind id p
+ if use_predicate pre.ip_content.tp_kind then begin
+ let id = WpPropId.mk_pre_id kf (Kstmt s) bhv pre in
+ let labels = NormAtLabels.labels_stmt_pre ~kf s in
+ let p = Logic_const.pred_of_id_pred pre in
+ let p = normalize id labels ?assumes p in
+ add_prop acc kind id p
+ end else acc
let add_prop_stmt_bhv_requires acc kind kf s bhv ~with_assumes =
let assumes =
@@ -227,11 +232,13 @@ let add_prop_stmt_spec_pre acc kind kf s spec =
in List.fold_left add_bhv_pre acc spec.spec_behavior
let add_prop_stmt_post acc kind kf s bhv tkind l_post ~assumes post =
- let id = WpPropId.mk_stmt_post_id kf s bhv (tkind, post) in
- let labels = NormAtLabels.labels_stmt_post ~kf s l_post in
- let p = Logic_const.pred_of_id_pred post in
- let p = normalize id labels ?assumes p in
- add_prop acc kind id p
+ if verify_predicate post.ip_content.tp_kind then begin
+ let id = WpPropId.mk_stmt_post_id kf s bhv (tkind, post) in
+ let labels = NormAtLabels.labels_stmt_post ~kf s l_post in
+ let p = Logic_const.pred_of_id_pred post in
+ let p = normalize id labels ?assumes p in
+ add_prop acc kind id p
+ end else acc
let update_kind kind pre =
if pre.ip_content.tp_kind = Check then begin
--
GitLab