diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index af9599cde0f054ddcc080d9e34c43a1b31ad6358..5944017b75c270cceee4140b80ec2a5b5dac58d5 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -110,12 +110,12 @@ let normalize_assigns kf ki has_exit bhv ~active = function
let get_requires kf ki bhv =
List.map (normalize_pre kf ki bhv) bhv.b_requires
-let get_behavior kf ki has_exit ~active bhv =
+let get_behavior kf ki ~exits ~active bhv =
let pre_cond = normalize_pre kf ki bhv in
let post_cond tk (kind,ip) =
if kind = tk then Some (normalize_post kf ki bhv tk ip) else None in
let p_asgn, e_asgn =
- normalize_assigns kf ki has_exit bhv ~active bhv.b_assigns
+ normalize_assigns kf ki exits bhv ~active bhv.b_assigns
in
{
bhv_assumes = List.map pre_cond bhv.b_assumes;
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index a3330628d2f4e53e14191d88e67d7c236fe874c6..302d1b08ba7ee314cb4a7e91ad8689df81d1cb6d 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -43,8 +43,8 @@ type behavior = {
val get_requires : kernel_function -> kinstr -> funbehavior -> pred_info list
val get_behavior :
- kernel_function -> kinstr -> bool -> active:string list -> funbehavior ->
- behavior
+ kernel_function -> kinstr -> exits:bool -> active:string list ->
+ funbehavior -> behavior
val get_preconditions : goal:bool ->kernel_function -> pred_info list
val get_complete_behaviors : kernel_function -> pred_info list
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 6c473581c298d5a384284263233bbb6c60996563..7305217ee55228f9a96c6e7aef65a7a0019d3e3e 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -28,6 +28,7 @@ open Cil_datatype
(* -------------------------------------------------------------------------- *)
module WpLog = Wp_parameters
+module Kf = Kernel_function
module Cfg = Interpreted_automata
module G = Cfg.G
module V = Cfg.Vertex
@@ -42,6 +43,7 @@ type assigns = WpPropId.assigns_full_info
type mode = {
kf: kernel_function;
bhv : funbehavior ;
+ infos : CfgInfos.t ;
}
type props = [ `All | `Names of string list | `PropId of Property.t ]
@@ -122,37 +124,6 @@ struct
module I = CfgInit.Make(W)
- module Reachable_call : sig
- val has_reachable_call: Cfg.automaton -> vertex -> bool
- end
- =
- struct
- exception Found_call
-
- type reachability_env = {
- table: unit Vhash.t ;
- cfg: Cfg.automaton ;
- }
-
- let rec reachable_call_by_cfg env a =
- try Vhash.find env.table a
- with Not_found ->
- Vhash.add env.table a () ;
- List.iter (transition env) (G.succ_e env.cfg.graph a)
-
- and transition env (_,edge,dst) =
- reachable_call_by_cfg env dst ;
- match edge.edge_transition with
- | Instr ((Local_init(_,ConsInit _, _)| Call _), _) -> raise Found_call
- | _ -> ()
-
- let has_reachable_call cfg v =
- let env = { table = Vhash.create 32 ; cfg } in
- try reachable_call_by_cfg env v ; false
- with Found_call -> true
-
- end
-
(* --- Traversal Environment --- *)
type env = {
@@ -291,7 +262,7 @@ struct
| Local_init(x,ConsInit (vf, args, kind), loc) ->
Cil.treat_constructor_as_func
begin fun r fct args _loc ->
- match Kernel_function.get_called fct with
+ match Kf.get_called fct with
| Some kf -> call env s r kf args w
| None ->
WpLog.warning ~once:true "No function for constructor '%s'"
@@ -301,7 +272,7 @@ struct
end x vf args kind loc
| Call(res,fct,args,_loc) ->
begin
- match Kernel_function.get_called fct with
+ match Kf.get_called fct with
| Some kf -> call env s res kf args w
| None ->
match Dyncall.get ~bhv:env.mode.bhv.b_name s with
@@ -335,27 +306,28 @@ struct
in W.call_goal_precond env.we s kf es ~pre w_call
else w_call
- 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 do_complete_disjoint env w =
+ if not (is_default_bhv env.mode) then w
+ else
+ let kf = env.mode.kf in
+ let complete = CfgAnnot.get_complete_behaviors kf in
+ let disjoint = CfgAnnot.get_disjoint_behaviors kf in
+ List.fold_right (prove_property env) complete @@
+ List.fold_right (prove_property env) disjoint w
let do_global_init env w =
I.process_global_init env.we env.mode.kf @@
W.scope env.we [] SC_Global w
- let do_preconditions env ~main ~formals bhvs w =
+ let do_preconditions env ~formals bhvs w =
let kf = env.mode.kf in
- let prove_if_main ps w =
- if main then List.fold_right (prove_property env) ps w else w in
+ let init = WpStrategy.is_main_init kf in
let behaviors =
- if main || WpLog.PrecondWeakening.get () then []
+ if init || WpLog.PrecondWeakening.get () then []
else CfgAnnot.get_preconditions ~goal:false kf in
let defaults = default_requires env.mode kf in
let requires = bhvs.CfgAnnot.bhv_requires in
+ let initreqs = if init then requires else [] in
let assumes = bhvs.CfgAnnot.bhv_assumes in
(* pre-state *)
W.label env.we None Clabels.pre @@
@@ -364,14 +336,10 @@ struct
(* pre-conditions *)
List.fold_right (use_property env) defaults @@
List.fold_right (use_property env) assumes @@
- prove_if_main requires @@
+ List.fold_right (prove_property env) initreqs @@
List.fold_right (use_property env) requires @@
List.fold_right (use_property env) behaviors w
- let do_complete_disjoint env ~complete ~disjoint w =
- List.fold_right (prove_property env) complete @@
- List.fold_right (prove_property env) disjoint w
-
let do_post env ~formals (b : CfgAnnot.behavior) w =
W.scope env.we formals SC_Frame_out @@
W.label env.we None Clabels.post @@
@@ -384,7 +352,7 @@ struct
List.fold_right (prove_property env) b.bhv_exits @@
prove_assigns env b.bhv_exit_assigns w
- let do_body env ~formals (b : CfgAnnot.behavior) w =
+ let do_funbehavior env ~formals (b : CfgAnnot.behavior) w =
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) ;
@@ -394,27 +362,25 @@ struct
(* Putting everything together *)
let compute ~mode ~props =
let kf = mode.kf in
- let cfg = Cfg.get_automaton kf in
+ let infos = mode.infos in
+ let cfg = CfgInfos.cfg infos in
let env = {
- mode ; props ;
- cfg ;
+ mode ; props ; cfg ;
we = W.new_env kf ;
wp = Vhash.create 32 ;
wk = W.empty ;
} in
- let main = WpStrategy.is_main_init kf in
- let formals = Kernel_function.get_formals kf in
- let complete = complete mode kf in
- let disjoint = disjoint mode kf in
- let has_exit = Reachable_call.has_reachable_call cfg (cfg.entry_point) in
- let bhv = CfgAnnot.get_behavior kf Kglobal has_exit ~active:[] mode.bhv in
- env.we ,
- W.close env.we @@
- do_global_init env @@
- do_preconditions env ~main ~formals bhv @@
- do_complete_disjoint env ~complete ~disjoint @@
- do_body env ~formals bhv @@
- W.empty
+ let formals = Kf.get_formals kf in
+ let exits = not @@ Kf.Set.is_empty @@ CfgInfos.calls infos in
+ let bhv = CfgAnnot.get_behavior kf Kglobal ~exits ~active:[] mode.bhv in
+ begin
+ W.close env.we @@
+ do_global_init env @@
+ do_preconditions env ~formals bhv @@
+ do_complete_disjoint env @@
+ do_funbehavior env ~formals bhv @@
+ W.empty
+ end
end
diff --git a/src/plugins/wp/cfgCalculus.mli b/src/plugins/wp/cfgCalculus.mli
index e49d6dd72a9cabe425e173590782f08e70136268..16a6e66cd28a83dbbb64c463af59dddc74a8ee51 100644
--- a/src/plugins/wp/cfgCalculus.mli
+++ b/src/plugins/wp/cfgCalculus.mli
@@ -29,15 +29,14 @@ open Cil_types
type mode = {
kf : kernel_function ; (* Selected function *)
bhv : funbehavior ; (* Selected behavior *)
+ infos : CfgInfos.t ; (* Associated infos *)
}
type props = [ `All | `Names of string list | `PropId of Property.t ]
module Make(W : Mcfg.S) :
sig
-
- val compute : mode:mode -> props:props -> W.t_env * W.t_prop
-
+ val compute : mode:mode -> props:props -> W.t_prop
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index 9ee671a972993145de26d2f4dcb493d309562e6d..ae509665f232ec2ee905be19492084f50de8c79a 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -30,15 +30,15 @@ open Wp_parameters
module KFmap = Kernel_function.Map
type task = {
- mutable lemmas: LogicUsage.logic_lemma list ;
- mutable modes: CfgCalculus.mode list KFmap.t ; (** TODO: when New CFG is validated, use list *)
+ mutable modes: CfgCalculus.mode list KFmap.t ;
mutable props: CfgCalculus.props ;
+ mutable lemmas: LogicUsage.logic_lemma list ;
}
let empty () = {
lemmas = [];
modes = KFmap.empty;
- props = `All ;
+ props = `All;
}
(* -------------------------------------------------------------------------- *)
@@ -73,34 +73,31 @@ let lemma task ?(prop=[]) l =
(prop=[] || WpPropId.select_by_name prop (WpPropId.mk_lemma_id l))
then task.lemmas <- l :: task.lemmas
-let apply task ~kf ?bhvs ?prop () =
+let apply task ~kf ?infos ?bhvs ?target () =
+ let infos = match infos with
+ | Some infos -> infos
+ | None -> CfgInfos.get kf () in
+ let bhvs = match bhvs with
+ | Some bhvs -> bhvs
+ | None ->
+ let bhvs = Annotations.behaviors kf in
+ if List.exists (Cil.is_default_behavior) bhvs then bhvs
+ else empty_default_behavior :: bhvs in
+ let add_mode kf m =
+ let ms = try KFmap.find kf task.modes with Not_found -> [] in
+ task.modes <- KFmap.add kf (m :: ms) task.modes in
begin
- let bhvs = match bhvs with
- | Some bhvs -> bhvs
- | None ->
- let bhvs = Annotations.behaviors kf in
- if List.exists (Cil.is_default_behavior) bhvs then bhvs
- else empty_default_behavior :: bhvs
- in
- let add_mode kf m =
- let modes =
- match KFmap.find_opt kf task.modes with
- | None -> []
- | Some modes -> modes
- in
- task.modes <- KFmap.add kf (m :: modes) task.modes
- in
- List.iter (fun bhv -> add_mode kf { CfgCalculus.kf ; bhv }) bhvs ;
- Option.iter (fun ip -> task.props <- `PropId ip) prop ;
+ List.iter (fun bhv -> add_mode kf CfgCalculus.{ infos ; kf ; bhv }) bhvs ;
+ Option.iter (fun ip -> task.props <- `PropId ip) target ;
end
let notyet prop =
Wp_parameters.warning ~once:true
"Not yet implemented wp for '%a'" Property.pretty prop
-let rec strategy_ip task prop =
+let rec strategy_ip task target =
let open Property in
- match prop with
+ match target with
| IPLemma { il_name } ->
lemma task (LogicUsage.logic_lemma il_name)
| IPAxiomatic { iax_props } ->
@@ -113,43 +110,43 @@ let rec strategy_ip task prop =
| PKRequires bhv ->
begin
match ki with
- | Kglobal -> (*TODO*) notyet prop
- | Kstmt _ -> apply task ~kf ~bhvs:[bhv] ~prop ()
+ | Kglobal -> (*TODO*) notyet target
+ | Kstmt _ -> apply task ~kf ~bhvs:[bhv] ~target ()
end
| PKEnsures(bhv,_) ->
- apply task ~kf ~bhvs:[bhv] ~prop ()
+ apply task ~kf ~bhvs:[bhv] ~target ()
| PKTerminates ->
- apply task ~kf ~bhvs:(default kf) ~prop ()
+ apply task ~kf ~bhvs:(default kf) ~target ()
end
| IPDecrease { id_kf = kf } ->
- apply task ~kf ~bhvs:(default kf) ~prop ()
+ apply task ~kf ~bhvs:(default kf) ~target ()
| 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 ()
+ apply task ~kf ~bhvs:(select kf bhvs) ~target ()
| IPAssigns { ias_kf=kf ; ias_bhv=Id_contract(_,bhv) }
| IPAllocation { ial_kf=kf ; ial_bhv=Id_contract(_,bhv) }
- -> apply task ~kf ~bhvs:[bhv] ~prop ()
+ -> apply task ~kf ~bhvs:[bhv] ~target ()
| IPCodeAnnot { ica_kf = kf ; ica_ca = ca } ->
begin match ca.annot_content with
| AExtended _ | APragma _ -> ()
| AStmtSpec(fors,_) ->
- (*TODO*) notyet prop ;
+ (*TODO*) notyet target ;
apply task ~kf ~bhvs:(select kf fors) ()
| AVariant _ ->
- apply task ~kf ~prop ()
+ apply task ~kf ~target ()
| AAssert(fors, _)
| AInvariant(fors, _, _)
| AAssigns(fors, _)
| AAllocation(fors, _) ->
- apply task ~kf ~bhvs:(select kf fors) ~prop ()
+ apply task ~kf ~bhvs:(select kf fors) ~target ()
end
- | IPComplete _ -> (*TODO*) notyet prop
- | IPDisjoint _ -> (*TODO*) notyet prop
+ | IPComplete _ -> (*TODO*) notyet target
+ | IPDisjoint _ -> (*TODO*) notyet target
| IPFrom _ | IPReachable _ | IPTypeInvariant _ | IPGlobalInvariant _
- | IPPropertyInstance _ -> notyet prop (* ? *)
+ | IPPropertyInstance _ -> notyet target (* ? *)
| IPExtended _ | IPAxiom _ | IPOther _ -> ()
let strategy_main task ?(fct=Fct_all) ?(bhv=[]) ?(prop=[]) () =
@@ -159,9 +156,11 @@ let strategy_main task ?(fct=Fct_all) ?(bhv=[]) ?(prop=[]) () =
Wp_parameters.iter_fct
(fun kf ->
if Kernel_function.has_definition kf then
- if bhv=[]
- then apply task ~kf ()
- else apply task ~kf ~bhvs:(select kf bhv) ()
+ let infos = CfgInfos.get kf ~bhv ~prop () in
+ if CfgInfos.annots infos then
+ if bhv=[]
+ then apply task ~infos ~kf ()
+ else apply task ~infos ~kf ~bhvs:(select kf bhv) ()
) fct ;
task.props <- (if prop=[] then `All else `Names prop);
end
@@ -202,7 +201,8 @@ struct
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 wp = snd @@ WP.compute ~mode ~props:task.props in
+ let props = task.props in
+ let wp = WP.compute ~mode ~props in
let wcs = VCG.compile_wp index wp in
collection := Bag.concat !collection wcs
end ()
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 88d853e711713b55f8710cee0bbe54806fc842d6..4d0503a4dfcaffde9633f0c573b292f3c0f8e75c 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -41,6 +41,7 @@ type t = {
(* --- Getters --- *)
(* -------------------------------------------------------------------------- *)
+let cfg infos = infos.cfg
let calls infos = infos.calls
let annots infos = infos.annots
let doomed infos = infos.doomed
@@ -173,7 +174,6 @@ module Generator = WpContext.StaticGenerator(Key)
let compile = compile
end)
-let collect kf ?(bhv=[]) ?(prop=[]) () =
- Generator.get { kf ; bhv ; prop }
+let get kf ?(bhv=[]) ?(prop=[]) () = Generator.get { kf ; bhv ; prop }
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
index 355a3efcffd97d244a7f8262f5568638564ce9b3..e90e360797a80f1b152ec285aedabab39f4c0a45 100644
--- a/src/plugins/wp/cfgInfos.mli
+++ b/src/plugins/wp/cfgInfos.mli
@@ -27,9 +27,10 @@ type t
module Cfg = Interpreted_automata
(** Memoized *)
-val collect :
- Kernel_function.t -> ?bhv:string list -> ?prop:string list -> unit -> t
+val get : Kernel_function.t -> ?bhv:string list -> ?prop:string list ->
+ unit -> t
+val cfg : t -> Cfg.automaton
val annots : t -> bool
val doomed : t -> WpPropId.prop_id Bag.t
val calls : t -> Kernel_function.Set.t