From e7cecff76e6c1352d0e71132d59017f8283ea6e9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 21 Jan 2021 18:34:29 +0100
Subject: [PATCH] [wp] compute modes for new calculus
---
src/libraries/utils/bag.mli | 1 +
src/plugins/wp/Generator.ml | 26 ++---
src/plugins/wp/cfgCalculus.ml | 61 +++---------
src/plugins/wp/cfgCalculus.mli | 10 +-
src/plugins/wp/cfgGenerator.ml | 176 +++++++++++++++++++++++++++++++--
5 files changed, 201 insertions(+), 73 deletions(-)
diff --git a/src/libraries/utils/bag.mli b/src/libraries/utils/bag.mli
index 1e466b2e6e2..ef515cb71fc 100644
--- a/src/libraries/utils/bag.mli
+++ b/src/libraries/utils/bag.mli
@@ -36,6 +36,7 @@ val concat : 'a t -> 'a t -> 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
val umap : ('a -> 'b t) -> 'a t -> 'b t
+val umap_list : ('a -> 'b t) -> 'a list -> 'b t
val iter : ('a -> unit) -> 'a t -> unit
val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml
index dbe19558090..2af03b61f95 100644
--- a/src/plugins/wp/Generator.ml
+++ b/src/plugins/wp/Generator.ml
@@ -67,17 +67,19 @@ let create
let legacy = default Wp_parameters.Dump.get legacy in
let driver = default Driver.load_driver driver in
let setup = default user_setup setup in
- ignore legacy ;
- let cc =
- if dump
- then WpGenerator.dumper ()
- else WpGenerator.computer setup driver in
- let the_model = cc#model in
- object
- method model = the_model
- method compute_ip = WpGenerator.compute_ip cc
- method compute_call = WpGenerator.compute_call cc
- method compute_main = WpGenerator.compute_selection cc
- end
+ if legacy then
+ let cc =
+ if dump
+ then WpGenerator.dumper ()
+ else WpGenerator.computer setup driver in
+ let the_model = cc#model in
+ object
+ method model = the_model
+ method compute_ip = WpGenerator.compute_ip cc
+ method compute_call = WpGenerator.compute_call cc
+ method compute_main = WpGenerator.compute_selection cc
+ end
+ else
+ CfgGenerator.generator setup driver
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index eb8175580fd..9205c53e4fe 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -40,37 +40,12 @@ type assigns = WpPropId.assigns_full_info
(* -------------------------------------------------------------------------- *)
type mode = {
+ kf: kernel_function;
bhv : funbehavior ; (* Selected behavior (None is default) *)
- stmt : stmt option ; (* Stmt contract under proof *)
}
type props = [ `All | `Names of string list | `PropId of Property.t ]
-module MODES = WpContext.StaticGenerator(Kernel_function)
- (struct
- type key = kernel_function
- type data = mode list
- let name = "Wp.CfgCalculus.Modes"
- let compile kf =
- Annotations.fold_behaviors
- (fun _emitter bhv ms -> { bhv ; stmt = None } :: ms)
- kf @@
- List.fold_right
- (fun stmt ms ->
- Annotations.fold_code_annot (fun _emitter ca ms ->
- match ca.annot_content with
- | AStmtSpec(_, { spec_behavior = bs } ) ->
- List.fold_right (fun bhv ms -> {
- bhv ;
- stmt = Some stmt ;
- }::ms) bs ms
- | _ -> ms
- ) stmt ms
- ) (Kernel_function.get_definition kf).sallstmts []
- end)
-
-let modes = MODES.get
-
let default_requires mode kf =
if Cil.is_default_behavior mode.bhv then [] else
try
@@ -139,10 +114,8 @@ struct
(* --- Traversal Environment --- *)
type env = {
- kf: kernel_function;
mode: mode;
props: props;
- mutable ki: kinstr; (* Current localisation *)
cfg: Cfg.automaton;
we: W.t_env;
wp: W.t_prop option Vhash.t; (* None is used for non-dag detection *)
@@ -189,13 +162,13 @@ struct
(* --- Decomposition of WP Rules --- *)
- exception NonNaturalLoop of kernel_function * kinstr
+ exception NonNaturalLoop
let succ env a = G.succ_e env.cfg.graph a
let rec wp (env:env) (a:vertex) : W.t_prop =
match Vhash.find env.wp a with
- | None -> raise (NonNaturalLoop(env.kf,env.ki))
+ | None -> raise NonNaturalLoop
| Some pi -> pi
| exception Not_found ->
(* cut circularities *)
@@ -207,23 +180,19 @@ struct
(* Compute a stmt node *)
and stmt env a (s: stmt) : W.t_prop =
- let ki = env.ki in
let kl = Cil.CurrentLoc.get () in
try
- env.ki <- Kstmt s ;
Cil.CurrentLoc.set (Stmt.loc s) ;
- let ca = CfgAnnot.get_code_assertions env.kf s in
+ let ca = CfgAnnot.get_code_assertions env.mode.kf s in
let pi =
W.label env.we (Some s) (Clabels.stmt s) @@
List.fold_right (prove_property env) ca.code_verified @@
List.fold_right (use_property env) ca.code_admitted @@
control env a s
in
- Cil.CurrentLoc.set kl ;
- env.ki <- ki ; pi
+ Cil.CurrentLoc.set kl ; pi
with err ->
- Cil.CurrentLoc.set kl ;
- env.ki <- ki ; raise err
+ Cil.CurrentLoc.set kl ; raise err
(* Branching wrt control-flow *)
and control env a s : W.t_prop =
@@ -234,7 +203,7 @@ struct
W.switch env.we s value
(List.map (fun (e,v) -> [e], wp env v) cases)
(wp env default)
- | Loop _ -> loop env a s (CfgAnnot.get_loop_contract env.kf s)
+ | Loop _ -> loop env a s (CfgAnnot.get_loop_contract env.mode.kf s)
| Edges -> successors env a
(* Compute loops *)
@@ -322,21 +291,21 @@ struct
wp env env.cfg.entry_point
(* Putting everything together *)
- let compute ~mode ~props kf =
+ let compute ~mode ~props =
let env = {
- kf ; ki = Kglobal ; mode ; props ;
- cfg = Cfg.get_automaton kf ;
- we = W.new_env kf ;
+ mode ; props ;
+ cfg = Cfg.get_automaton mode.kf ;
+ we = W.new_env mode.kf ;
wp = Vhash.create 32 ;
wk = W.empty ;
} 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
+ 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
env.we ,
(* global init *)
W.close env.we @@
- I.process_global_init env.we kf @@
+ I.process_global_init env.we mode.kf @@
W.scope env.we [] SC_Global @@
(* pre-state *)
W.label env.we None Clabels.pre @@
diff --git a/src/plugins/wp/cfgCalculus.mli b/src/plugins/wp/cfgCalculus.mli
index 6e7ec0f5ef0..e49d6dd72a9 100644
--- a/src/plugins/wp/cfgCalculus.mli
+++ b/src/plugins/wp/cfgCalculus.mli
@@ -27,20 +27,16 @@ open Cil_types
(* -------------------------------------------------------------------------- *)
type mode = {
- bhv : funbehavior ; (* Selected behavior (None is default) *)
- stmt : stmt option ; (* Stmt contract under proof *)
+ kf : kernel_function ; (* Selected function *)
+ bhv : funbehavior ; (* Selected behavior *)
}
type props = [ `All | `Names of string list | `PropId of Property.t ]
-(* Memoized *)
-val modes : kernel_function -> mode list
-
module Make(W : Mcfg.S) :
sig
- val compute : mode:mode -> props:props -> kernel_function ->
- W.t_env * W.t_prop
+ val compute : mode:mode -> props:props -> W.t_env * W.t_prop
end
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index 0350785f987..e9cd98fec7e 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -20,6 +20,170 @@
(* *)
(**************************************************************************)
+open Cil_types
+open Wp_parameters
+
+(* -------------------------------------------------------------------------- *)
+(* --- Task Manager --- *)
+(* -------------------------------------------------------------------------- *)
+
+type task = {
+ mutable lemmas: LogicUsage.logic_lemma list ;
+ mutable modes: CfgCalculus.mode list ;
+ mutable props: CfgCalculus.props ;
+}
+
+let empty () = {
+ lemmas = [];
+ modes = [];
+ props = `All ;
+}
+
+(* -------------------------------------------------------------------------- *)
+(* --- Property Guided Selection --- *)
+(* -------------------------------------------------------------------------- *)
+
+let default kf =
+ List.filter
+ Cil.is_default_behavior
+ (Annotations.behaviors kf)
+
+let select kf bnames =
+ List.filter
+ (fun b -> List.mem b.b_name bnames)
+ (Annotations.behaviors kf)
+
+let apply task ~kf ?bhvs ?prop () =
+ begin
+ let bhvs = match bhvs with
+ | None -> Annotations.behaviors kf
+ | Some bhvs -> bhvs in
+ List.iter (fun bhv ->
+ task.modes <- { kf ; bhv } :: task.modes
+ ) bhvs ;
+ Extlib.may (fun ip -> task.props <- `PropId ip) prop ;
+ end
+
+let notyet prop =
+ Wp_parameters.warning ~once:true
+ "Not yet implemented wp for '%a'" Property.pretty prop
+
+let rec strategy task prop =
+ let open Property in
+ match prop with
+ | IPLemma { il_name } ->
+ let l = LogicUsage.logic_lemma il_name in
+ task.lemmas <- l :: task.lemmas
+ | IPAxiomatic { iax_props } ->
+ List.iter (strategy task) iax_props
+ | IPBehavior { ib_kf = kf ; ib_bhv = bhv } ->
+ apply task ~kf ~bhvs:[bhv] ()
+ | IPPredicate { ip_kf = kf ; ip_kind ; ip_kinstr = ki } ->
+ begin match ip_kind with
+ | PKAssumes _ -> ()
+ | PKRequires bhv ->
+ begin
+ match ki with
+ | Kglobal -> (*TODO*) notyet prop
+ | Kstmt _ -> apply task ~kf ~bhvs:[bhv] ~prop ()
+ end
+ | PKEnsures(bhv,_) ->
+ apply task ~kf ~bhvs:[bhv] ~prop ()
+ | PKTerminates ->
+ apply task ~kf ~bhvs:(default kf) ~prop ()
+ end
+ | IPDecrease { id_kf = kf } ->
+ apply task ~kf ~bhvs:(default kf) ~prop ()
+ | IPAssigns { ias_kf=kf ; ias_bhv=Id_loop ca }
+ | IPAllocation { ial_kf=kf ; ial_bhv=Id_loop ca } ->
+ let bhvs = match ca.annot_content with
+ | AAssigns(bhvs,_) | AAllocation(bhvs,_) -> bhvs
+ | _ -> [] in
+ apply task ~kf ~bhvs:(select kf bhvs) ~prop ()
+ | IPAssigns { ias_kf=kf ; ias_bhv=Id_contract(_,bhv) }
+ | IPAllocation { ial_kf=kf ; ial_bhv=Id_contract(_,bhv) }
+ -> apply task ~kf ~bhvs:[bhv] ~prop ()
+ | IPCodeAnnot { ica_kf = kf ; ica_ca = ca } ->
+ begin match ca.annot_content with
+ | AExtended _ | APragma _ -> ()
+ | AStmtSpec(fors,_) ->
+ (*TODO*) notyet prop ;
+ apply task ~kf ~bhvs:(select kf fors) ()
+ | AVariant _ ->
+ apply task ~kf ~prop ()
+ | AAssert(fors, _)
+ | AInvariant(fors, _, _)
+ | AAssigns(fors, _)
+ | AAllocation(fors, _) ->
+ apply task ~kf ~bhvs:(select kf fors) ~prop ()
+ end
+ | IPComplete _ -> (*TODO*) notyet prop
+ | IPDisjoint _ -> (*TODO*) notyet prop
+ | IPFrom _ | IPReachable _ | IPTypeInvariant _ | IPGlobalInvariant _
+ | IPPropertyInstance _ -> notyet prop (* ? *)
+ | IPExtended _ | IPAxiom _ | IPOther _ -> ()
+
+(* -------------------------------------------------------------------------- *)
+(* --- Compute All Tasks --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Make(VCG : CfgWP.VCgen) =
+struct
+
+ module WP = CfgCalculus.Make(VCG)
+
+ let compute model task =
+ begin
+ let collection = ref Bag.empty in
+ Lang.F.release () ;
+ if task.lemmas <> [] then
+ WpContext.on_context (model,WpContext.Global)
+ begin fun () ->
+ LogicUsage.iter_lemmas VCG.register_lemma ;
+ List.iter (fun l ->
+ let wpo = VCG.compile_lemma l in
+ collection := Bag.add wpo !collection
+ ) task.lemmas ;
+ end () ;
+ List.iter
+ (fun (mode : CfgCalculus.mode) ->
+ WpContext.on_context (model,WpContext.Kf mode.kf)
+ begin fun () ->
+ let wp = snd @@ WP.compute ~mode ~props:task.props in
+ let bhv =
+ if Cil.is_default_behavior mode.bhv then None
+ else Some mode.bhv.b_name in
+ let index = Wpo.Function(mode.kf,bhv) in
+ let wcs = VCG.compile_wp index wp in
+ collection := Bag.concat !collection wcs
+ end ()
+ ) task.modes ;
+ !collection
+ end
+
+ let compute_ip model ip =
+ let task = empty () in
+ strategy task ip ;
+ compute model task
+
+ let compute_call _model _stmt =
+ Wp_parameters.warning
+ ~once:true "Not yet implemented call preconds" ;
+ Bag.empty
+
+ let compute_main model ?(fct=Fct_all) ?bhv ?prop () =
+ let task = empty () in
+ Wp_parameters.iter_fct
+ (fun kf ->
+ match bhv with
+ | None -> apply task ~kf ()
+ | Some bs -> apply task ~kf ~bhvs:(select kf bs) ()
+ ) fct ;
+ task.props <- (match prop with None -> `All | Some ps -> `Names ps) ;
+ compute model task
+
+end
+
(* -------------------------------------------------------------------------- *)
(* --- New WP Computer (main entry points) --- *)
(* -------------------------------------------------------------------------- *)
@@ -31,17 +195,13 @@ let generator setup driver =
try WpContext.MINDEX.find generators model
with Not_found ->
let module VCG = (val CfgWP.vcgen setup driver) in
- let module WP = CfgCalculus.Make(VCG) in
+ let module CC = Make(VCG) in
let generator : Wpo.generator =
object
method model = model
- method compute_ip _ = Bag.empty
- method compute_call _ = Bag.empty
- method compute_main ?fct ?bhv ?prop () =
- ignore fct ;
- ignore bhv ;
- ignore prop ;
- Bag.empty
+ method compute_ip = CC.compute_ip model
+ method compute_call = CC.compute_call model
+ method compute_main = CC.compute_main model
end in
WpContext.MINDEX.add generators model generator ;
generator
--
GitLab