From 40c243f9ba8e3491ed39adbc51aa055e25dd2b64 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 11 Feb 2021 10:11:52 +0100
Subject: [PATCH] [wp] refactor contract to prepare stmt
---
src/plugins/wp/cfgAnnot.ml | 76 +++++++++++++++++------------------
src/plugins/wp/cfgAnnot.mli | 14 +++----
src/plugins/wp/cfgCalculus.ml | 17 ++++----
3 files changed, 53 insertions(+), 54 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 8de5afd5be0..401ee6ebaf9 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -180,7 +180,37 @@ let get_disjoint_behaviors kf =
) spec.spec_disjoint_behaviors
(* -------------------------------------------------------------------------- *)
-(* --- Called Contract --- *)
+(* --- Contracts --- *)
+(* -------------------------------------------------------------------------- *)
+
+type contract = {
+ contract_pre : WpPropId.pred_info list ;
+ contract_post : WpPropId.pred_info list ;
+ contract_exit : WpPropId.pred_info list ;
+ contract_smoke : WpPropId.pred_info list ;
+ contract_assigns : Cil_types.assigns ;
+}
+
+let assigns_upper_bound behaviors =
+ let collect_assigns (def, assigns) bhv =
+ (* Default behavior prevails *)
+ if Cil.is_default_behavior bhv then Some bhv.b_assigns, None
+ else if Option.is_some def then def, None
+ else begin
+ (* Note that here, def is None *)
+ match assigns, bhv.b_assigns with
+ | None, a -> None, Some a
+ | Some WritesAny, _ | Some _, WritesAny -> None, Some WritesAny
+ | Some (Writes a), Writes b -> None, Some (Writes (a @ b))
+ end
+ in
+ match List.fold_left collect_assigns (None, None) behaviors with
+ | Some a, _ -> a (* default behavior first *)
+ | _, Some a -> a (* else combined behaviors *)
+ | _ -> WritesAny
+
+(* -------------------------------------------------------------------------- *)
+(* --- Call Contracts --- *)
(* -------------------------------------------------------------------------- *)
(*TODO: put it in Status_by_call ? *)
@@ -199,42 +229,16 @@ let setup_preconditions kf =
Statuses_by_call.setup_all_preconditions_proxies kf ;
end
-type call_contract = {
- call_pre : WpPropId.pred_info list ;
- call_post : WpPropId.pred_info list ;
- call_exit : WpPropId.pred_info list ;
- call_smoke : WpPropId.pred_info list ;
- call_assigns : Cil_types.assigns ;
-}
-
let get_precond_at kf stmt (id,p) =
let pi = WpPropId.property_of_id id in
let pi_at = Statuses_by_call.precondition_at_call kf pi stmt in
let id_at = WpPropId.mk_call_pre_id kf stmt pi pi_at in
id_at , p
-let assigns_upper_bound behaviors =
- let collect_assigns (def, assigns) bhv =
- (* Default behavior prevails *)
- if Cil.is_default_behavior bhv then Some bhv.b_assigns, None
- else if Option.is_some def then def, None
- else begin
- (* Note that here, def is None *)
- match assigns, bhv.b_assigns with
- | None, a -> None, Some a
- | Some WritesAny, _ | Some _, WritesAny -> None, Some WritesAny
- | Some (Writes a), Writes b -> None, Some (Writes (a @ b))
- end
- in
- match List.fold_left collect_assigns (None, None) behaviors with
- | Some a, _ -> a (* default behavior first *)
- | _, Some a -> a (* else combined behaviors *)
- | _ -> WritesAny
-
module CallContract = WpContext.StaticGenerator(Kernel_function)
(struct
type key = kernel_function
- type data = call_contract
+ type data = contract
let name = "Wp.CfgAnnot.CallContract"
let compile kf =
let cpre : WpPropId.pred_info list ref = ref [] in
@@ -255,11 +259,11 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
) bhv.b_post_cond ;
end behaviors ;
{
- call_pre = List.rev !cpre ;
- call_post = List.rev !cpost ;
- call_exit = List.rev !cexit ;
- call_smoke = [] ;
- call_assigns = assigns_upper_bound behaviors
+ contract_pre = List.rev !cpre ;
+ contract_post = List.rev !cpost ;
+ contract_exit = List.rev !cexit ;
+ contract_smoke = [] ;
+ contract_assigns = assigns_upper_bound behaviors
}
end)
@@ -269,11 +273,7 @@ let get_call_contract ?smoking kf =
| None -> cc
| Some s ->
let g = smoke kf ~id:"dead_call" ~unreachable:s () in
- { cc with
- call_smoke = [ g ] ;
- call_post = cc.call_post ;
- call_exit = cc.call_exit ;
- }
+ { cc with contract_smoke = [ g ] }
(* -------------------------------------------------------------------------- *)
(* --- Code Assertions --- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 0a1f6cd81c3..88384ea7f7a 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -91,16 +91,16 @@ val get_loop_contract : ?smoking:bool ->
(* --- Property Accessors : Call Contracts --- *)
(* -------------------------------------------------------------------------- *)
-type call_contract = {
- call_pre : pred_info list ;
- call_post : pred_info list ;
- call_exit : pred_info list ;
- call_smoke : pred_info list ;
- call_assigns : assigns ;
+type contract = {
+ contract_pre : pred_info list ;
+ contract_post : pred_info list ;
+ contract_exit : pred_info list ;
+ contract_smoke : pred_info list ;
+ contract_assigns : assigns ;
}
val get_precond_at : kernel_function -> stmt -> pred_info -> pred_info
-val get_call_contract : ?smoking:stmt -> kernel_function -> call_contract
+val get_call_contract : ?smoking:stmt -> kernel_function -> contract
(* -------------------------------------------------------------------------- *)
(* --- Clear Tablesnts --- *)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 796e211fe48..8cb4e5410e2 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -99,8 +99,7 @@ let is_active_mode ~mode ~goal (p: Property.t) =
| 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
+ | IPFrom _ | IPGlobalInvariant _ | IPTypeInvariant _
| IPAxiomatic _ | IPAxiom _ | IPLemma _
| IPExtended _ | IPBehavior _
| IPReachable _ | IPPropertyInstance _
@@ -304,13 +303,13 @@ struct
WpLog.SmokeDeadcall.get ()
then Some s else None in
let c = CfgAnnot.get_call_contract ?smoking kf in
- let p_post = List.fold_right (prove_property env) c.call_smoke wr in
- let p_exit = List.fold_right (prove_property env) c.call_smoke env.wk in
+ let p_post = List.fold_right (prove_property env) c.contract_smoke wr in
+ let p_exit = List.fold_right (prove_property env) c.contract_smoke env.wk in
let w_call = W.call env.we s r kf es
- ~pre:c.call_pre
- ~post:c.call_post
- ~pexit:c.call_exit
- ~assigns:c.call_assigns
+ ~pre:c.contract_pre
+ ~post:c.contract_post
+ ~pexit:c.contract_exit
+ ~assigns:c.contract_assigns
~p_post ~p_exit in
if is_default_bhv env.mode then
let pre =
@@ -318,7 +317,7 @@ struct
if is_selected_callpre env p then
Some (CfgAnnot.get_precond_at kf s p)
else None
- ) c.call_pre
+ ) c.contract_pre
in W.call_goal_precond env.we s kf es ~pre w_call
else w_call
--
GitLab