From 7e00d91d25fd6da1f60ec60c33a0dcedea09e052 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 18 Jan 2021 16:24:18 +0100
Subject: [PATCH] [wp] process behavior
---
src/plugins/wp/clabels.ml | 1 +
src/plugins/wp/clabels.mli | 1 +
src/plugins/wp/normAtLabels.ml | 16 ++++++++++--
src/plugins/wp/normAtLabels.mli | 6 +++--
src/plugins/wp/wpAnnot.ml | 43 ++++++++++++++++++++++++++++++++-
src/plugins/wp/wpAnnot.mli | 16 ++++++++++++
src/plugins/wp/wpPropId.ml | 3 +++
src/plugins/wp/wpPropId.mli | 3 +++
src/plugins/wp/wpStrategy.ml | 6 ++---
9 files changed, 87 insertions(+), 8 deletions(-)
diff --git a/src/plugins/wp/clabels.ml b/src/plugins/wp/clabels.ml
index f9e26a0db02..6f20a911f5e 100644
--- a/src/plugins/wp/clabels.ml
+++ b/src/plugins/wp/clabels.ml
@@ -59,6 +59,7 @@ let mem l lbl = List.mem l lbl
let case n = "wp:case" ^ Int64.to_string n
let stmt s = "wp:sid" ^ string_of_int s.sid
+let stmt_post s = "wp:sid:post:" ^ string_of_int s.sid
let loop_entry s = stmt s (* same point *)
let loop_current s = "wp:head" ^ string_of_int s.sid
diff --git a/src/plugins/wp/clabels.mli b/src/plugins/wp/clabels.mli
index 33812ec5f13..4014aab7f58 100644
--- a/src/plugins/wp/clabels.mli
+++ b/src/plugins/wp/clabels.mli
@@ -56,6 +56,7 @@ val formal : string -> c_label
val case : int64 -> c_label
val stmt : Cil_types.stmt -> c_label
+val stmt_post : Cil_types.stmt -> c_label
val loop_entry : Cil_types.stmt -> c_label
val loop_current : Cil_types.stmt -> c_label
diff --git a/src/plugins/wp/normAtLabels.ml b/src/plugins/wp/normAtLabels.ml
index 197b12f9685..fb30f63eadd 100644
--- a/src/plugins/wp/normAtLabels.ml
+++ b/src/plugins/wp/normAtLabels.ml
@@ -153,12 +153,24 @@ let labels_stmt_pre ~kf s = function
| BuiltinLabel Here -> Clabels.stmt s
| l -> labels_fct ~kf ~at:s l
-let labels_stmt_post ~kf s l_post = function
+let labels_stmt_post ~kf s = function
+ | BuiltinLabel Old -> Clabels.stmt s
+ | BuiltinLabel (Here | Post) -> Clabels.stmt_post s
+ | l -> labels_fct ~kf ~at:s l
+
+let labels_stmt_assigns ~kf s = function
+ | BuiltinLabel (Here | Old) -> Clabels.stmt s
+ | BuiltinLabel Post -> Clabels.stmt_post s
+ | l -> labels_fct ~kf ~at:s l
+
+(* LEGACY *)
+let labels_stmt_post_l ~kf s l_post = function
| BuiltinLabel Old -> Clabels.stmt s
| BuiltinLabel (Here | Post) as l -> option l l_post
| l -> labels_fct ~kf ~at:s l
-let labels_stmt_assigns ~kf s l_post = function
+(* LEGACY *)
+let labels_stmt_assigns_l ~kf s l_post = function
| BuiltinLabel (Here | Old) -> Clabels.stmt s
| BuiltinLabel Post as l -> option l l_post
| l -> labels_fct ~kf ~at:s l
diff --git a/src/plugins/wp/normAtLabels.mli b/src/plugins/wp/normAtLabels.mli
index 0dd24f82545..2becd6c715a 100644
--- a/src/plugins/wp/normAtLabels.mli
+++ b/src/plugins/wp/normAtLabels.mli
@@ -36,8 +36,10 @@ val labels_assert_before : kf:kernel_function -> stmt -> label_mapping
val labels_assert_after : kf:kernel_function -> stmt -> c_label option -> label_mapping
val labels_loop : stmt -> label_mapping
val labels_stmt_pre : kf:kernel_function -> stmt -> label_mapping
-val labels_stmt_post : kf:kernel_function -> stmt -> c_label option -> label_mapping
-val labels_stmt_assigns : kf:kernel_function -> stmt -> c_label option -> label_mapping
+val labels_stmt_post : kf:kernel_function -> stmt -> label_mapping
+val labels_stmt_assigns : kf:kernel_function -> stmt -> label_mapping
+val labels_stmt_post_l : kf:kernel_function -> stmt -> c_label option -> label_mapping
+val labels_stmt_assigns_l : kf:kernel_function -> stmt -> c_label option -> label_mapping
val labels_predicate : (logic_label * logic_label) list -> label_mapping
val labels_axiom : label_mapping
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 88708e985e5..63b38897149 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -188,6 +188,47 @@ let preconditions_at_call s = function
let get_called_preconditions_at kf stmt =
List.map snd (call_preconditions kf stmt)
+(* -------------------------------------------------------------------------- *)
+(* --- Property Accessors : Behaviors --- *)
+(* -------------------------------------------------------------------------- *)
+
+type behavior = {
+ bhv_assumes: WpPropId.pred_info list ;
+ bhv_requires: WpPropId.pred_info list ;
+ bhv_ensures: WpPropId.pred_info list ;
+ bhv_exits: WpPropId.pred_info list ;
+ bhv_assigns: WpPropId.assigns_full_info list ;
+}
+
+let get_behavior kf ki bhv =
+ let module L = NormAtLabels in
+ let normalize_pre ip =
+ let labels =
+ match ki with
+ | Kglobal -> L.labels_fct_pre
+ | Kstmt s -> L.labels_stmt_pre kf s in
+ WpPropId.mk_pre_id kf ki bhv ip ,
+ L.preproc_annot labels ip.ip_content.tp_statement
+ in
+ let normalize_post tk ip =
+ let labels =
+ match ki with
+ | Kglobal -> L.labels_fct_pre
+ | Kstmt s -> L.labels_stmt_post kf s in
+ WpPropId.mk_post_id kf ki bhv (tk,ip) ,
+ L.preproc_annot labels ip.ip_content.tp_statement
+ in
+ let post_cond tk = List.filter_map (fun (kind,ip) ->
+ if kind = tk then Some (normalize_post tk ip) else None
+ ) bhv.b_post_cond
+ in {
+ bhv_assumes = List.map normalize_pre bhv.b_assumes;
+ bhv_requires = List.map normalize_pre bhv.b_requires;
+ bhv_ensures = post_cond Normal ;
+ bhv_exits = post_cond Exits ;
+ bhv_assigns = [];
+ }
+
(* -------------------------------------------------------------------------- *)
(* --- Code Assertions --- *)
(* -------------------------------------------------------------------------- *)
@@ -517,7 +558,7 @@ let add_stmt_assigns_goal config s active acc b l_post = match b.b_assigns with
| Some id ->
if goal_to_select config id then
let kf = config.kf in
- let labels = NormAtLabels.labels_stmt_assigns ~kf s l_post in
+ let labels = NormAtLabels.labels_stmt_assigns_l ~kf s l_post in
let assigns = NormAtLabels.preproc_assigns labels assigns in
let a_desc = WpPropId.mk_stmt_assigns_desc s assigns in
WpStrategy.add_assigns acc WpStrategy.Agoal id a_desc
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index daaf415162e..38d2dcbdcfa 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -63,6 +63,20 @@ val get_called_post_conditions : kernel_function -> Property.t list
val get_called_exit_conditions : kernel_function -> Property.t list
val get_called_assigns : kernel_function -> Property.t list
+(* -------------------------------------------------------------------------- *)
+(* --- Property Accessors : Behaviors --- *)
+(* -------------------------------------------------------------------------- *)
+
+type behavior = {
+ bhv_assumes: WpPropId.pred_info list ;
+ bhv_requires: WpPropId.pred_info list ;
+ bhv_ensures: WpPropId.pred_info list ;
+ bhv_exits: WpPropId.pred_info list ;
+ bhv_assigns: WpPropId.assigns_full_info list;
+}
+
+val get_behavior : kernel_function -> kinstr -> funbehavior -> behavior
+
(* -------------------------------------------------------------------------- *)
(* --- Property Accessors : Assertions --- *)
(* -------------------------------------------------------------------------- *)
@@ -91,6 +105,8 @@ type loop_contract = {
val get_loop_contract : kernel_function -> stmt -> loop_contract
+(* -------------------------------------------------------------------------- *)
+
(* ########################################################################## *)
(* ### WARNING: DEPRECATED API BELOW THIS LINE ### *)
(* ########################################################################## *)
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index a95b4a86490..9097438fdcb 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -169,6 +169,9 @@ let mk_fct_assigns_id kf b tkind a =
let mk_pre_id kf ki b p =
mk_prop PKProp (Property.ip_of_requires kf ki b p)
+let mk_post_id kf ki b p =
+ mk_prop PKProp (Property.ip_of_ensures kf ki b p)
+
let mk_stmt_post_id kf s b p =
mk_prop PKProp (Property.ip_of_ensures kf (Kstmt s) b p)
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 29098180bbe..c3adc45404b 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -183,6 +183,9 @@ val mk_fct_assigns_id : kernel_function -> funbehavior ->
val mk_pre_id : kernel_function -> kinstr -> funbehavior ->
identified_predicate -> prop_id
+val mk_post_id : kernel_function -> kinstr -> funbehavior ->
+ termination_kind * identified_predicate -> prop_id
+
val mk_stmt_post_id : kernel_function -> stmt -> funbehavior ->
termination_kind * identified_predicate -> prop_id
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index 7026d240203..195affa7997 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -228,7 +228,7 @@ let add_prop_stmt_spec_pre acc kind kf s spec =
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 labels = NormAtLabels.labels_stmt_post_l ~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
@@ -403,7 +403,7 @@ let add_stmt_spec_assigns_hyp acc kf s l_post spec =
| None -> add_assigns_any acc Ahyp
(WpPropId.mk_stmt_any_assigns_info s)
| Some id ->
- let labels = NormAtLabels.labels_stmt_assigns ~kf s l_post in
+ let labels = NormAtLabels.labels_stmt_assigns_l ~kf s l_post in
let assigns = NormAtLabels.preproc_assigns labels assigns in
let a_desc = WpPropId.mk_stmt_assigns_desc s assigns in
add_assigns acc Ahyp id a_desc
@@ -432,7 +432,7 @@ let add_call_assigns_hyp acc kf_caller s ~called_kf l_post spec_opt =
add_assigns_any acc (AcallHyp called_kf) asgn
| Some pid ->
let kf = kf_caller in
- let labels = NormAtLabels.labels_stmt_assigns ~kf s l_post in
+ let labels = NormAtLabels.labels_stmt_assigns_l ~kf s l_post in
let assigns = NormAtLabels.preproc_assigns labels assigns in
let a_desc = WpPropId.mk_stmt_assigns_desc s assigns in
add_assigns acc (AcallHyp called_kf) pid a_desc
--
GitLab