From 699c1f843a3c9c854c769674a94e16812e5fd030 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 8 Feb 2021 09:48:19 +0100
Subject: [PATCH] [wp] Do not ignore main declaration
---
src/plugins/wp/cfgCalculus.ml | 13 +++---
src/plugins/wp/cfgGenerator.ml | 11 +++--
src/plugins/wp/cfgInfos.ml | 77 +++++++++++++++++++---------------
src/plugins/wp/cfgInfos.mli | 2 +-
4 files changed, 58 insertions(+), 45 deletions(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 6b6a404b943..e12ad3ebe43 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -129,7 +129,7 @@ struct
type env = {
mode: mode;
props: props;
- cfg: Cfg.automaton;
+ cfg: Cfg.automaton option;
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,7 +179,7 @@ struct
exception NonNaturalLoop
- let succ env a = G.succ_e env.cfg.graph a
+ 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
@@ -356,11 +356,12 @@ struct
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 env.cfg.return_point (Some wpost) ;
+ Vhash.add env.wp cfg.return_point (Some wpost) ;
env.wk <- wexit ;
- wp env env.cfg.entry_point
+ wp env cfg.entry_point
(* Putting everything together *)
let compute ~mode ~props =
@@ -381,7 +382,9 @@ struct
do_global_init env @@
do_preconditions env ~formals bhv @@
do_complete_disjoint env @@
- do_funbehavior env ~formals bhv @@
+ (if Kernel_function.has_definition kf
+ then do_funbehavior env ~formals bhv
+ else Extlib.id) @@
W.empty
end
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index c9c999726e8..d781ebb00f4 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -162,12 +162,11 @@ let strategy_main model task ?(fct=Fct_all) ?(bhv=[]) ?(prop=[]) () =
LogicUsage.iter_lemmas (lemma task ~prop) ;
Wp_parameters.iter_fct
(fun kf ->
- if Kernel_function.has_definition kf then
- let infos = get_kf_infos model kf ~bhv ~prop () in
- if CfgInfos.annots infos then
- if bhv=[]
- then apply model task ~infos ~kf ()
- else apply model task ~infos ~kf ~bhvs:(select kf bhv) ()
+ let infos = get_kf_infos model kf ~bhv ~prop () in
+ if CfgInfos.annots infos then
+ if bhv=[]
+ then apply model task ~infos ~kf ()
+ else apply model task ~infos ~kf ~bhvs:(select kf bhv) ()
) fct ;
task.props <- (if prop=[] then `All else `Names prop);
end
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 959fcb2b028..3b9ca175fec 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -30,7 +30,7 @@ module Shash = Cil_datatype.Stmt.Hashtbl
(* -------------------------------------------------------------------------- *)
type t = {
- cfg : Cfg.automaton;
+ cfg : Cfg.automaton option;
mutable annots : bool; (* has goals to prove *)
mutable doomed : WpPropId.prop_id Bag.t;
mutable calls : Kernel_function.Set.t;
@@ -60,7 +60,7 @@ let fixpoint h d f =
in phi
let unreachable infos =
- let pred = Cfg.G.pred infos.cfg.graph in
+ let pred = Cfg.G.pred (Option.get infos.cfg).graph in
fixpoint infos.unreachable true
begin fun phi v -> List.for_all phi (pred v) end
@@ -120,6 +120,9 @@ let selected_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
(List.exists (selected_postcond ~prop) b.b_post_cond)
end
+let selected_main_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
+ (bhv = [] || List.mem b.b_name bhv) && (selected_requires ~prop) b
+
(* -------------------------------------------------------------------------- *)
(* --- Calls --- *)
(* -------------------------------------------------------------------------- *)
@@ -194,7 +197,10 @@ let loop_contract_pids kf stmt =
| _ -> []
let compile Key.{ kf ; bhv ; prop } =
- let cfg = Cfg.get_automaton kf in
+ let cfg =
+ if Kernel_function.has_definition kf then Some (Cfg.get_automaton kf)
+ else None
+ in
let infos = {
cfg ;
annots = false ;
@@ -202,36 +208,41 @@ let compile Key.{ kf ; bhv ; prop } =
calls = Fset.empty ;
unreachable = Vhash.create 32 ;
} in
- (* Root Reachability *)
- let v0 = cfg.entry_point in
- Vhash.add infos.unreachable v0 false ;
- (* Spec Iteration *)
- if selected_disjoint_complete kf ~bhv ~prop ||
- List.exists
- (selected_bhv ~bhv ~prop)
- (Annotations.behaviors kf)
- 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 ;
+ let behaviors = Annotations.behaviors kf in
+ 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
+ (* Root Reachability *)
+ let v0 = cfg.entry_point in
+ Vhash.add infos.unreachable v0 false ;
+ (* 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 ;
(* Collected Infos *)
infos
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
index e90e360797a..b94ab3471ef 100644
--- a/src/plugins/wp/cfgInfos.mli
+++ b/src/plugins/wp/cfgInfos.mli
@@ -30,7 +30,7 @@ module Cfg = Interpreted_automata
val get : Kernel_function.t -> ?bhv:string list -> ?prop:string list ->
unit -> t
-val cfg : t -> Cfg.automaton
+val cfg : t -> Cfg.automaton option
val annots : t -> bool
val doomed : t -> WpPropId.prop_id Bag.t
val calls : t -> Kernel_function.Set.t
--
GitLab