From 46ef6f5ec5879b6b552be59af11f4d02a7a6061c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 20 Jan 2021 08:53:55 +0100
Subject: [PATCH] [wp] moving things around regarding strategies
---
src/plugins/wp/Generator.ml | 33 ++----------------------------
src/plugins/wp/cfgWP.ml | 40 ++++++++++++++++++-------------------
src/plugins/wp/wpAnnot.ml | 32 +++++++++++++++++++++++++++++
src/plugins/wp/wpAnnot.mli | 7 +++----
4 files changed, 56 insertions(+), 56 deletions(-)
diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml
index 1f303b5fc34..c5ac01b0f15 100644
--- a/src/plugins/wp/Generator.ml
+++ b/src/plugins/wp/Generator.ml
@@ -48,40 +48,11 @@ let compute_ip cc ip =
| _ -> ()
in iter cc ip ;
cc#compute
-
- | IPBehavior {ib_kf; ib_bhv} ->
- let model = cc#model in
- let bhv = [ib_bhv.Cil_types.b_name] in
- let assigns = WpAnnot.WithAssigns in
- List.iter cc#add_strategy
- (WpAnnot.get_function_strategies ~model ~assigns ~bhv ib_kf) ;
- cc#compute
- | IPComplete _
- | IPDisjoint _
- | IPCodeAnnot _
- | IPAllocation _
- | IPAssigns _
- | IPDecrease _
- | IPPredicate _
- ->
- let model = cc#model in
- let assigns = WpAnnot.WithAssigns in
+ | _ ->
List.iter cc#add_strategy
- (WpAnnot.get_id_prop_strategies ~model ~assigns ip) ;
+ (WpAnnot.get_property_strategies ~model:cc#model ip) ;
cc#compute
- | IPFrom _
- | IPAxiom _
- | IPReachable _
- | IPPropertyInstance _
- | IPOther _
- | IPTypeInvariant _
- | IPGlobalInvariant _
- | IPExtended _
- ->
- Wp_parameters.result "Nothing to compute for '%a'" pretty ip ;
- Bag.empty
-
(* -------------------------------------------------------------------------- *)
(* --- Annotations Entry Point --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index d8d221d9cbd..8165aea5076 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1386,29 +1386,13 @@ struct
end !groups
- let lemma = L.lemma
-
-end
-
-(* -------------------------------------------------------------------------- *)
-(* --- WPO Computer --- *)
-(* -------------------------------------------------------------------------- *)
-
-module KFmap = Kernel_function.Map
-
-module Computer(M : Sigs.Compiler) =
-struct
-
- module VCG = VC(M)
- module WP = Calculus.Cfg(VCG)
-
- let compile_lemma l = ignore (VCG.lemma l)
+ let lemma l = ignore (L.lemma l)
let prove_lemma collection l =
if l.lem_kind <> `Axiom then
begin
let id = WpPropId.mk_lemma_id l in
- let def = VCG.lemma l in
+ let def = L.lemma l in
let model = WpContext.get_model () in
let vca = {
Wpo.VC_Lemma.depends = l.lem_depends ;
@@ -1435,6 +1419,20 @@ struct
collection := Bag.append !collection wpo ;
end
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- WPO Computer --- *)
+(* -------------------------------------------------------------------------- *)
+
+module KFmap = Kernel_function.Map
+
+module Computer(M : Sigs.Compiler) =
+struct
+
+ module VCG = VC(M)
+ module WP = Calculus.Cfg(VCG)
+
let prove_strategy collection model kf strategy =
let cfg = WpStrategy.cfg_of_strategy strategy in
let bhv = WpStrategy.get_bhv strategy in
@@ -1469,14 +1467,14 @@ struct
Lang.F.release () ;
WpContext.on_context (model,WpContext.Global)
begin fun () ->
- LogicUsage.iter_lemmas compile_lemma ;
- Bag.iter (prove_lemma collection) lemmas ;
+ LogicUsage.iter_lemmas VCG.lemma ;
+ Bag.iter (VCG.prove_lemma collection) lemmas ;
end () ;
KFmap.iter
(fun kf strategies ->
WpContext.on_context (model,WpContext.Kf kf)
begin fun () ->
- LogicUsage.iter_lemmas compile_lemma ;
+ LogicUsage.iter_lemmas VCG.lemma ;
Bag.iter (prove_strategy collection model kf) strategies ;
end ()
) annots ;
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 9b3af468c5b..1e0f4006807 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -1344,3 +1344,35 @@ let get_function_strategies ~model
?(assigns=WithAssigns) ?(bhv=[]) ?(prop=[]) kf =
let prop = match prop with [] -> AllProps | _ -> NamedProp prop in
get_strategies assigns kf model bhv None prop
+
+let get_property_strategies ~model ip =
+ let open Property in
+ match ip with
+ | IPBehavior {ib_kf; ib_bhv} ->
+ let bhv = [ib_bhv.Cil_types.b_name] in
+ let assigns = WithAssigns in
+ get_function_strategies ~model ~assigns ~bhv ib_kf
+ | IPComplete _
+ | IPDisjoint _
+ | IPCodeAnnot _
+ | IPAllocation _
+ | IPAssigns _
+ | IPDecrease _
+ | IPPredicate _
+ ->
+ let assigns = WithAssigns in
+ get_id_prop_strategies ~model ~assigns ip
+
+ | IPAxiomatic _
+ | IPLemma _
+ | IPFrom _
+ | IPAxiom _
+ | IPReachable _
+ | IPPropertyInstance _
+ | IPOther _
+ | IPTypeInvariant _
+ | IPGlobalInvariant _
+ | IPExtended _
+ ->
+ Wp_parameters.result "Nothing to compute for '%a'" pretty ip ;
+ []
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index 8155d57820c..835a1e96881 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -34,10 +34,6 @@ open Cil_types
type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns
-val get_id_prop_strategies :
- model:WpContext.model ->
- ?assigns:asked_assigns -> Property.t -> WpStrategy.strategy list
-
val get_call_pre_strategies :
model:WpContext.model ->
stmt -> WpStrategy.strategy list
@@ -49,4 +45,7 @@ val get_function_strategies :
?prop:string list ->
Kernel_function.t -> WpStrategy.strategy list
+val get_property_strategies :
+ model:WpContext.model -> Property.t -> WpStrategy.strategy list
+
(*----------------------------------------------------------------------------*)
--
GitLab