From 3ee159f6a6260605d14e9ed062447095e7fb08d8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 8 Feb 2021 16:40:09 +0100
Subject: [PATCH] [wp] refactor function-body
---
src/plugins/wp/cfgCalculus.ml | 34 ++++++++--------
src/plugins/wp/cfgInfos.ml | 77 ++++++++++++++++++-----------------
src/plugins/wp/cfgInfos.mli | 3 +-
3 files changed, 59 insertions(+), 55 deletions(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index e12ad3ebe43..d418ba2488d 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -129,7 +129,8 @@ struct
type env = {
mode: mode;
props: props;
- cfg: Cfg.automaton option;
+ body: Cfg.automaton option;
+ succ: Cfg.vertex -> Cfg.G.edge list;
we: W.t_env;
wp: W.t_prop option Vhash.t; (* None is used for non-dag detection *)
mutable wk: W.t_prop; (* end point *)
@@ -179,8 +180,6 @@ struct
exception NonNaturalLoop
- let succ env a = G.succ_e (Option.get env.cfg).graph a
-
let rec wp (env:env) (a:vertex) : W.t_prop =
match Vhash.find env.wp a with
| None -> raise NonNaturalLoop
@@ -240,7 +239,7 @@ struct
W.merge env.we established presersed
(* Merge transitions *)
- and successors env (a : vertex) = transitions env (succ env a)
+ and successors env (a : vertex) = transitions env (env.succ a)
and transitions env (es : G.edge list) = fmerge env (transition env) es
and transition env (_,edge,dst) : W.t_prop =
let p = wp env dst in
@@ -355,21 +354,26 @@ struct
List.fold_right (prove_property env) b.bhv_exits @@
prove_assigns env b.bhv_exit_assigns w
- let do_funbehavior env ~formals (b : CfgAnnot.behavior) w =
- let cfg = Option.get env.cfg in
- let wpost = do_post env ~formals b w in
- let wexit = do_exit env ~formals b w in
- Vhash.add env.wp cfg.return_point (Some wpost) ;
- env.wk <- wexit ;
- wp env cfg.entry_point
+ let do_funbehavior env ~formals (b:CfgAnnot.behavior) w =
+ match env.body with
+ | None -> w
+ | Some cfg ->
+ let wpost = do_post env ~formals b w in
+ let wexit = do_exit env ~formals b w in
+ Vhash.add env.wp cfg.return_point (Some wpost) ;
+ env.wk <- wexit ;
+ wp env cfg.entry_point
(* Putting everything together *)
let compute ~mode ~props =
let kf = mode.kf in
let infos = mode.infos in
- let cfg = CfgInfos.cfg infos in
+ let body = CfgInfos.body infos in
+ let succ = match body with
+ | None -> (fun _ -> [])
+ | Some cfg -> Cfg.G.succ_e cfg.graph in
let env = {
- mode ; props ; cfg ;
+ mode ; props ; body ; succ ;
we = W.new_env kf ;
wp = Vhash.create 32 ;
wk = W.empty ;
@@ -382,9 +386,7 @@ struct
do_global_init env @@
do_preconditions env ~formals bhv @@
do_complete_disjoint env @@
- (if Kernel_function.has_definition kf
- then do_funbehavior env ~formals bhv
- else Extlib.id) @@
+ do_funbehavior env ~formals bhv @@
W.empty
end
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 013e77df4fc..ac9c245b0ad 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -31,7 +31,7 @@ module Shash = Cil_datatype.Stmt.Hashtbl
module Reachability = Graph.Path.Check(Cfg.G)
type t = {
- cfg : Cfg.automaton option ;
+ body : Cfg.automaton option ;
reachability : Reachability.path_checker option ;
mutable annots : bool; (* has goals to prove *)
mutable doomed : WpPropId.prop_id Bag.t;
@@ -42,15 +42,17 @@ type t = {
(* --- Getters --- *)
(* -------------------------------------------------------------------------- *)
-let cfg infos = infos.cfg
+let body infos = infos.body
let calls infos = infos.calls
let annots infos = infos.annots
let doomed infos = infos.doomed
let unreachable infos v =
- let reachability = Option.get infos.reachability in
- let entry = (Option.get infos.cfg).entry_point in
- not @@ Reachability.check_path reachability entry v
+ match infos.body, infos.reachability with
+ | Some cfg , Some reach ->
+ let entry = cfg.entry_point in
+ not @@ Reachability.check_path reach entry v
+ | _ -> true
(* -------------------------------------------------------------------------- *)
(* --- Selected Properties --- *)
@@ -191,51 +193,52 @@ let loop_contract_pids kf stmt =
| _ -> []
let compile Key.{ kf ; bhv ; prop } =
- let cfg, reachability =
+ let body, reachability =
if Kernel_function.has_definition kf then
let cfg = Cfg.get_automaton kf in
Some cfg, Some (Reachability.create cfg.graph)
else None, None
in
let infos = {
- cfg ;
+ body ;
annots = false ;
doomed = Bag.empty ;
calls = Fset.empty ;
- reachability
+ reachability ;
} in
let behaviors = Annotations.behaviors kf in
+ (* Inits *)
if WpStrategy.is_main_init kf then
infos.annots <- List.exists (selected_main_bhv ~bhv ~prop) behaviors ;
-
- if Kernel_function.has_definition kf then begin
- let cfg = Option.get cfg in
- (* Spec Iteration *)
- if selected_disjoint_complete kf ~bhv ~prop ||
- (List.exists (selected_bhv ~bhv ~prop) behaviors)
- then infos.annots <- true ;
- (* Stmt Iteration *)
- Shash.iter
- (fun stmt (src,_) ->
- let fs = collect_calls ~bhv stmt in
- let dead = unreachable infos src in
- let ca = CfgAnnot.get_code_assertions kf stmt in
- let ca_pids = List.map fst ca.code_verified in
- let loop_pids = loop_contract_pids kf stmt in
- if dead then begin
- infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
- infos.doomed <- Bag.concat infos.doomed (Bag.list loop_pids) ;
- end else
- begin
- if not infos.annots &&
- ( List.exists (selected ~bhv ~prop) ca_pids ||
- List.exists (selected ~bhv ~prop) loop_pids ||
- Fset.exists (selected_call ~bhv ~prop) fs )
- then infos.annots <- true ;
- infos.calls <- Fset.union fs infos.calls ;
- end
- ) cfg.stmt_table ;
- end ;
+ (* Function Body *)
+ Option.iter
+ begin fun (cfg : Cfg.automaton) ->
+ (* Spec Iteration *)
+ if selected_disjoint_complete kf ~bhv ~prop ||
+ (List.exists (selected_bhv ~bhv ~prop) behaviors)
+ then infos.annots <- true ;
+ (* Stmt Iteration *)
+ Shash.iter
+ (fun stmt (src,_) ->
+ let fs = collect_calls ~bhv stmt in
+ let dead = unreachable infos src in
+ let ca = CfgAnnot.get_code_assertions kf stmt in
+ let ca_pids = List.map fst ca.code_verified in
+ let loop_pids = loop_contract_pids kf stmt in
+ if dead then begin
+ infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
+ infos.doomed <- Bag.concat infos.doomed (Bag.list loop_pids) ;
+ end else
+ begin
+ if not infos.annots &&
+ ( List.exists (selected ~bhv ~prop) ca_pids ||
+ List.exists (selected ~bhv ~prop) loop_pids ||
+ Fset.exists (selected_call ~bhv ~prop) fs )
+ then infos.annots <- true ;
+ infos.calls <- Fset.union fs infos.calls ;
+ end
+ ) cfg.stmt_table ;
+ end body ;
(* Collected Infos *)
infos
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
index b5420e9ffe8..89ff00c7da7 100644
--- a/src/plugins/wp/cfgInfos.mli
+++ b/src/plugins/wp/cfgInfos.mli
@@ -29,10 +29,9 @@ module Cfg = Interpreted_automata
(** Memoized *)
val get : Kernel_function.t -> ?bhv:string list -> ?prop:string list ->
unit -> t
-
val clear : unit -> unit
-val cfg : t -> Cfg.automaton option
+val body : t -> Cfg.automaton option
val annots : t -> bool
val doomed : t -> WpPropId.prop_id Bag.t
val calls : t -> Kernel_function.Set.t
--
GitLab