From cb6150a18272fb036b1e920cdc1bfb30e9ead6f9 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 8 Feb 2021 08:54:49 +0100
Subject: [PATCH] [wp] Generate RTE before getting cfg infos
---
src/plugins/wp/cfgGenerator.ml | 53 +++++++++++++++++++---------------
1 file changed, 29 insertions(+), 24 deletions(-)
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index ae509665f23..c9c999726e8 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -45,6 +45,13 @@ let empty () = {
(* --- Property Guided Selection --- *)
(* -------------------------------------------------------------------------- *)
+let get_kf_infos model kf ?bhv ?prop () =
+ if WpRTE.missing_guards model kf then
+ Wp_parameters.warning ~current:false ~once:true "Missing RTE guards"
+ else if Wp_parameters.RTE.get () then
+ WpRTE.generate model kf ;
+ CfgInfos.get kf ?bhv ?prop ()
+
let empty_default_behavior : funbehavior = {
b_name = Cil.default_behavior_name ;
b_requires = [] ;
@@ -73,10 +80,10 @@ 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 ?infos ?bhvs ?target () =
+let apply model task ~kf ?infos ?bhvs ?target () =
let infos = match infos with
| Some infos -> infos
- | None -> CfgInfos.get kf () in
+ | None -> get_kf_infos model kf () in
let bhvs = match bhvs with
| Some bhvs -> bhvs
| None ->
@@ -95,15 +102,15 @@ let notyet prop =
Wp_parameters.warning ~once:true
"Not yet implemented wp for '%a'" Property.pretty prop
-let rec strategy_ip task target =
+let rec strategy_ip model task target =
let open Property in
match target with
| IPLemma { il_name } ->
lemma task (LogicUsage.logic_lemma il_name)
| IPAxiomatic { iax_props } ->
- List.iter (strategy_ip task) iax_props
+ List.iter (strategy_ip model task) iax_props
| IPBehavior { ib_kf = kf ; ib_bhv = bhv } ->
- apply task ~kf ~bhvs:[bhv] ()
+ apply model task ~kf ~bhvs:[bhv] ()
| IPPredicate { ip_kf = kf ; ip_kind ; ip_kinstr = ki } ->
begin match ip_kind with
| PKAssumes _ -> ()
@@ -111,37 +118,37 @@ let rec strategy_ip task target =
begin
match ki with
| Kglobal -> (*TODO*) notyet target
- | Kstmt _ -> apply task ~kf ~bhvs:[bhv] ~target ()
+ | Kstmt _ -> apply model task ~kf ~bhvs:[bhv] ~target ()
end
| PKEnsures(bhv,_) ->
- apply task ~kf ~bhvs:[bhv] ~target ()
+ apply model task ~kf ~bhvs:[bhv] ~target ()
| PKTerminates ->
- apply task ~kf ~bhvs:(default kf) ~target ()
+ apply model task ~kf ~bhvs:(default kf) ~target ()
end
| IPDecrease { id_kf = kf } ->
- apply task ~kf ~bhvs:(default kf) ~target ()
+ apply model 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) ~target ()
+ apply model 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] ~target ()
+ -> apply model task ~kf ~bhvs:[bhv] ~target ()
| IPCodeAnnot { ica_kf = kf ; ica_ca = ca } ->
begin match ca.annot_content with
| AExtended _ | APragma _ -> ()
| AStmtSpec(fors,_) ->
(*TODO*) notyet target ;
- apply task ~kf ~bhvs:(select kf fors) ()
+ apply model task ~kf ~bhvs:(select kf fors) ()
| AVariant _ ->
- apply task ~kf ~target ()
+ apply model task ~kf ~target ()
| AAssert(fors, _)
| AInvariant(fors, _, _)
| AAssigns(fors, _)
| AAllocation(fors, _) ->
- apply task ~kf ~bhvs:(select kf fors) ~target ()
+ apply model task ~kf ~bhvs:(select kf fors) ~target ()
end
| IPComplete _ -> (*TODO*) notyet target
| IPDisjoint _ -> (*TODO*) notyet target
@@ -149,18 +156,18 @@ let rec strategy_ip task target =
| IPPropertyInstance _ -> notyet target (* ? *)
| IPExtended _ | IPAxiom _ | IPOther _ -> ()
-let strategy_main task ?(fct=Fct_all) ?(bhv=[]) ?(prop=[]) () =
+let strategy_main model task ?(fct=Fct_all) ?(bhv=[]) ?(prop=[]) () =
begin
if fct = Fct_all && bhv = [] then
LogicUsage.iter_lemmas (lemma task ~prop) ;
Wp_parameters.iter_fct
(fun kf ->
if Kernel_function.has_definition kf then
- let infos = CfgInfos.get kf ~bhv ~prop () in
+ let infos = get_kf_infos model 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) ()
+ 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
@@ -195,8 +202,6 @@ struct
WpContext.on_context (model,WpContext.Kf mode.kf)
begin fun () ->
LogicUsage.iter_lemmas VCG.register_lemma ;
- if WpRTE.missing_guards model mode.kf then
- warning ~current:false ~once:true "Missing RTE guards" ;
let bhv =
if Cil.is_default_behavior mode.bhv then None
else Some mode.bhv.b_name in
@@ -214,7 +219,7 @@ struct
let compute_ip model ip =
let task = empty () in
- strategy_ip task ip ;
+ strategy_ip model task ip ;
compute model task
let compute_call _model _stmt =
@@ -224,7 +229,7 @@ struct
let compute_main model ?fct ?bhv ?prop () =
let task = empty () in
- strategy_main task ?fct ?bhv ?prop () ;
+ strategy_main model task ?fct ?bhv ?prop () ;
compute model task
end
@@ -283,12 +288,12 @@ let dumper setup driver =
method model = model
method compute_ip ip =
let task = empty () in
- strategy_ip task ip ;
+ strategy_ip model task ip ;
dump task ; Bag.empty
method compute_call _ = Bag.empty
method compute_main ?fct ?bhv ?prop () =
let task = empty () in
- strategy_main task ?fct ?bhv ?prop () ;
+ strategy_main model task ?fct ?bhv ?prop () ;
dump task ; Bag.empty
end
in generator
--
GitLab