From dc54bea118ab8ca4191ef86cc3f8fe04cff024d1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 28 Jan 2021 19:23:20 +0100
Subject: [PATCH] [wp] complete & disjoint & side conditions
---
src/kernel_services/ast_queries/ast_info.ml | 8 ++--
src/kernel_services/ast_queries/ast_info.mli | 6 ++-
.../ast_queries/logic_const.ml | 6 ++-
.../ast_queries/logic_const.mli | 6 ++-
src/plugins/wp/cfgAnnot.ml | 42 +++++++++++++++++--
src/plugins/wp/cfgAnnot.mli | 4 ++
src/plugins/wp/cfgCalculus.ml | 33 +++++++++++----
7 files changed, 84 insertions(+), 21 deletions(-)
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index b2830548195..90397e1a578 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -117,15 +117,15 @@ let behavior_postcondition b k =
in
Logic_const.pimplies (assumes,postcondition)
-let behavior_precondition b =
+let behavior_precondition ?check b =
let assumes = behavior_assumes b in
let requires = Logic_const.pands
- (List.rev_map Logic_const.pred_of_id_pred b.b_requires)
+ (List.rev_map (Logic_const.pred_of_id_pred ?check) b.b_requires)
in
Logic_const.pimplies (assumes,requires)
-let precondition spec =
- Logic_const.pands (List.map behavior_precondition spec.spec_behavior)
+let precondition ?check spec =
+ Logic_const.pands (List.map (behavior_precondition ?check) spec.spec_behavior)
(** find the behavior named [name] in the list *)
let get_named_bhv bhv_list name =
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index 22cef1f7030..cce23bff9a1 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -65,16 +65,18 @@ val term_lvals_of_term: term -> term_lval list
(** @return the list of all the term lvals of a given term.
Purely syntactic function. *)
-val precondition : funspec -> predicate
+val precondition : ?check:bool -> funspec -> predicate
(** Builds the precondition from [b_assumes] and [b_requires] clauses.
+ If [~check:false] is specified, check-only requires are skipped.
@since Carbon-20101201 *)
val behavior_assumes : funbehavior -> predicate
(** Builds the conjunction of the [b_assumes].
@since Nitrogen-20111001 *)
-val behavior_precondition : funbehavior -> predicate
+val behavior_precondition : ?check:bool -> funbehavior -> predicate
(** Builds the precondition from [b_assumes] and [b_requires] clauses.
+ If [~check:false] is specified, check-only requires are skipped.
@since Carbon-20101201 *)
val behavior_postcondition : funbehavior -> termination_kind -> predicate
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index e53a0d86219..36830964006 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -51,8 +51,6 @@ let new_predicate ?only_check p =
let fresh_predicate_id = PredicateId.next
-let pred_of_id_pred p = p.ip_content.tp_statement
-
let refresh_predicate p = { p with ip_id = PredicateId.next () }
let new_identified_term t =
@@ -342,6 +340,10 @@ let unamed ?(loc=Cil_datatype.Location.unknown) p =
let ptrue = unamed Ptrue
let pfalse = unamed Pfalse
+let pred_of_id_pred ?(check=true) p =
+ let tp = p.ip_content in
+ if tp.tp_only_check && not check then ptrue else tp.tp_statement
+
let pold ?(loc=Cil_datatype.Location.unknown) p = match p.pred_content with
| Ptrue | Pfalse -> p
| _ -> {p with pred_content = Pat(p, old_label); pred_loc = loc}
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index 2c2ebd716d2..fadbb859a37 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -75,8 +75,10 @@ val refresh_predicate: identified_predicate -> identified_predicate
(** @return a fresh id for predicates *)
val fresh_predicate_id: unit -> int
-(** extract a named predicate for an identified predicate. *)
-val pred_of_id_pred: identified_predicate -> predicate
+(** extract a named predicate for an identified predicate.
+ When [~check:false] is specified, check-only predicate
+ returns a [ptrue] condition. *)
+val pred_of_id_pred: ?check:bool -> identified_predicate -> predicate
(** creates a new identified term with a fresh id*)
val new_identified_term: term -> identified_term
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index c6579e0f850..6bc07d26997 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -104,6 +104,43 @@ let get_behavior kf ki ~active bhv =
bhv_assigns = assigns ;
}
+(* -------------------------------------------------------------------------- *)
+(* --- Side Behavior Requires --- *)
+(* -------------------------------------------------------------------------- *)
+
+let get_assumes kf bhv =
+ normalize_assumes kf Kglobal (Ast_info.behavior_assumes bhv)
+
+let get_preconditions kf =
+ (*TODO use this code instead! *)
+ (*
+ let assumes = get_assumes kf bhv in
+ List.map (normalize_pre kf Kglobal ~assumes bhv) bhv.b_requires
+ *)
+ List.map
+ (fun bhv ->
+ let p = Ast_info.behavior_precondition ~check:false bhv in
+ normalize_pre kf Kglobal bhv (Logic_const.new_predicate p)
+ ) (Annotations.behaviors kf)
+
+let get_complete_behaviors kf =
+ let spec = Annotations.funspec kf in
+ let module L = NormAtLabels in
+ List.map
+ (fun bs ->
+ WpPropId.mk_compl_bhv_id (kf,Kglobal,[],bs) ,
+ L.preproc_annot L.labels_fct_pre @@ Ast_info.complete_behaviors spec bs
+ ) spec.spec_complete_behaviors
+
+let get_disjoint_behaviors kf =
+ let spec = Annotations.funspec kf in
+ let module L = NormAtLabels in
+ List.map
+ (fun bs ->
+ WpPropId.mk_disj_bhv_id (kf,Kglobal,[],bs) ,
+ L.preproc_annot L.labels_fct_pre @@ Ast_info.disjoint_behaviors spec bs
+ ) spec.spec_disjoint_behaviors
+
(* -------------------------------------------------------------------------- *)
(* --- Called Contract --- *)
(* -------------------------------------------------------------------------- *)
@@ -112,7 +149,7 @@ let get_behavior kf ki ~active bhv =
module AllPrecondStatus =
State_builder.Hashtbl(Kernel_function.Hashtbl)(Datatype.Unit)
(struct
- let name = "Call Preconditions Proxy Generated"
+ let name = "Wp.CfgAnnot.AllPrecondStatus"
let dependencies = [Ast.self]
let size = 32
end)
@@ -164,8 +201,7 @@ let get_call_contract kf =
setup_preconditions kf ;
List.iter
begin fun bhv ->
- let assumes =
- normalize_assumes kf Kglobal (Ast_info.behavior_assumes bhv) in
+ let assumes = get_assumes kf bhv in
let mk_pre = normalize_pre kf Kglobal bhv ~assumes in
let mk_post = normalize_post kf Kglobal bhv ~assumes in
List.iter (add cpre @@ mk_pre) bhv.b_requires ;
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 5da0e8ab665..44a71ff4ed8 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -44,6 +44,10 @@ val get_requires : kernel_function -> kinstr -> funbehavior -> pred_info list
val get_behavior : kernel_function -> kinstr -> active:string list ->
funbehavior -> behavior
+val get_preconditions : kernel_function -> pred_info list
+val get_complete_behaviors : kernel_function -> pred_info list
+val get_disjoint_behaviors : kernel_function -> pred_info list
+
(* -------------------------------------------------------------------------- *)
(* --- Property Accessors : Assertions --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 32afaa6c367..8a1ef560ed0 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -146,7 +146,7 @@ struct
is_active_mode ~mode pi &&
( not goal || is_selected_props props ~pi pid )
- let is_selected_precond { props } (pid,_) =
+ let is_selected_callpre { props } (pid,_) =
is_selected_props props pid
let use_assigns env (a : assigns) w =
@@ -296,13 +296,25 @@ struct
if is_default_bhv env.mode then
let pre =
List.filter_map (fun p ->
- if is_selected_precond env p then
+ if is_selected_callpre env p then
Some (CfgAnnot.get_precond_at kf s p)
else None
) c.call_pre
in W.call_goal_precond env.we s kf es ~pre w_call
else w_call
+ let behaviors kf =
+ if WpStrategy.is_main_init kf || WpLog.PrecondWeakening.get () then []
+ else CfgAnnot.get_preconditions kf
+
+ let complete mode kf =
+ if not (is_default_bhv mode) then []
+ else CfgAnnot.get_complete_behaviors kf
+
+ let disjoint mode kf =
+ if not (is_default_bhv mode) then []
+ else CfgAnnot.get_disjoint_behaviors kf
+
let body env ~ensures ~exits w =
let rw = List.fold_right (prove_property env) ensures w in
let rk = List.fold_right (prove_property env) exits w in
@@ -312,26 +324,31 @@ struct
(* Putting everything together *)
let compute ~mode ~props =
+ let kf = mode.kf in
let env = {
mode ; props ;
- cfg = Cfg.get_automaton mode.kf ;
- we = W.new_env mode.kf ;
+ cfg = Cfg.get_automaton kf ;
+ we = W.new_env kf ;
wp = Vhash.create 32 ;
wk = W.empty ;
} in
- let xs = Kernel_function.get_formals mode.kf in
- let req = default_requires mode mode.kf in
- let bhv = CfgAnnot.get_behavior mode.kf Kglobal ~active:[] mode.bhv in
+ let xs = Kernel_function.get_formals kf in
+ let req = default_requires mode kf in
+ let bhv = CfgAnnot.get_behavior kf Kglobal ~active:[] mode.bhv in
+
env.we ,
(* global init *)
W.close env.we @@
- I.process_global_init env.we mode.kf @@
+ I.process_global_init env.we kf @@
W.scope env.we [] SC_Global @@
(* pre-state *)
W.label env.we None Clabels.pre @@
List.fold_right (use_property env) req @@
List.fold_right (use_property env) bhv.bhv_assumes @@
List.fold_right (use_property env) bhv.bhv_requires @@
+ List.fold_right (use_property env) (behaviors kf) @@
+ List.fold_right (use_property env) (complete mode kf) @@
+ List.fold_right (use_property env) (disjoint mode kf) @@
(* frame-in *)
W.scope env.we xs SC_Frame_in @@
(* function body *)
--
GitLab