Skip to content
Snippets Groups Projects
Commit 55565c87 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] refactor API generators

parent 251a7786
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 379 additions and 364 deletions
src/plugins/wp/Generator.ml
+ 2
− 2
View file @ 55565c87
......@@ -85,8 +85,8 @@ let create
ignore legacy ;
let cc =
if dump
then CfgDump.create ()
else CfgWP.computer setup driver in
then WpGenerator.dumper ()
else WpGenerator.computer setup driver in
let the_model = cc#model in
object
method model = the_model
......
src/plugins/wp/Makefile.in
+ 2
− 1
View file @ 55565c87
......@@ -96,9 +96,10 @@ PLUGIN_CMO:= \
ProverTask ProverErgo ProverCoq \
filter_axioms Cache ProverWhy3 \
driver prover ProverSearch ProverScript \
wpGenerator Factory \
Factory \
cfgInit cfgAnnot cfgCalculus \
calculus cfgDump cfgWP \
wpGenerator \
Generator register VC
PLUGIN_CMI:=
......
src/plugins/wp/cfgDump.ml
+ 224
− 269
View file @ 55565c87
......@@ -20,283 +20,238 @@
(* *)
(**************************************************************************)
(* *)
(**************************************************************************)
let _dkey = "cfgdump" (* debugging key *)
module VC =
struct
let fc = ref None
let out = ref Format.std_formatter
let knode = ref 0
let node () = incr knode ; !knode
let create kf bhv =
begin
let name =
match bhv with
| None -> Kernel_function.get_name kf
| Some bname -> Kernel_function.get_name kf ^ "_" ^ bname
in
let file = Filename.concat (Wp_parameters.get_output () :> string) name in
Wp_parameters.feedback "CFG %a -> %s@." Kernel_function.pretty kf name ;
let fout = open_out (file ^ ".dot") in
fc := Some (fout,file) ;
out := Format.formatter_of_out_channel fout ;
Format.fprintf !out "digraph %a {@\n" Kernel_function.pretty kf ;
Format.fprintf !out " rankdir = TB ;@\n" ;
Format.fprintf !out " node [ style = filled, shape = box ] ;@\n" ;
Format.fprintf !out " N000 [ color = red, shape = circle, label = \"*\" ] ;@\n" ;
end
let flush () =
begin
Format.fprintf !out "}@." ;
out := Format.std_formatter ;
match !fc with
| None -> ()
| Some (fout,file) ->
close_out fout ;
ignore (Sys.command
(Printf.sprintf "dot -Tpdf %s.dot > %s.pdf" file file))
end
(* -------------------------------------------------------------------------- *)
(* --- MCFG Interface --- *)
(* -------------------------------------------------------------------------- *)
type t_prop = int (* current node *)
let pretty fmt k = Format.fprintf fmt "N%03d" k
let link a b =
if b =0
then Format.fprintf !out " %a -> %a [ style=dotted ];@." pretty a pretty b
else Format.fprintf !out " %a -> %a ;@." pretty a pretty b
let merge _env k1 k2 =
if k1=0 then k2 else
if k2=0 then k1 else
let u = node () in
Format.fprintf !out " %a [ label=\"\" , shape=circle ] ;@." pretty u ;
link u k1 ; link u k2 ; u
let empty = 0
let has_init _ = false
type t_env = Kernel_function.t
let new_env ?lvars kf : t_env = ignore lvars ; kf
let add_axiom _p _l = ()
let add_hyp _env (pid,pred) k =
let u = node () in
if Wp_parameters.debug_atleast 1 then
Format.fprintf !out " %a [ color=green , label=\"Assume %a\" ] ;@." pretty u Printer.pp_predicate pred
else
Format.fprintf !out " %a [ color=green , label=\"Assume %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
link u k ; u
let add_goal env (pid,pred) k =
let u = node () in
if Wp_parameters.debug_atleast 1 then
Format.fprintf !out " %a [ color=red , label=\"Prove %a\" ] ;@." pretty u Printer.pp_predicate pred
else
Format.fprintf !out " %a [ color=red , label=\"Prove %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
let pp_assigns fmt = function
| Cil_types.WritesAny -> Format.pp_print_string fmt " \\everything"
| Cil_types.Writes [] -> Format.pp_print_string fmt " \\nothing"
| Cil_types.Writes froms ->
List.iter
(fun (t,_) -> Format.fprintf fmt "@ %a" Printer.pp_identified_term t)
froms
let add_assigns env (pid,_) k =
let u = node () in
Format.fprintf !out " %a [ color=red , label=\"Assigns %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
let use_assigns _env region d k =
let u = node () in
begin match region with
| None ->
Format.fprintf !out " %a [ color=orange , label=\"Havoc All\" ] ;@." pretty u
| Some pid ->
Format.fprintf !out " %a [ color=orange , label=\"Havoc %a:\n@[<hov 2>assigns%a;@]\" ] ;@."
pretty u WpPropId.pp_propid pid
pp_assigns d.WpPropId.a_assigns
end ;
link u k ; u
let label _env stmt label k =
if Clabels.is_here label then k else
let u = node () in
( match stmt with
| None ->
Format.fprintf !out " %a [ label=\"Label %a\" ] ;@." pretty u Clabels.pretty label
| Some s ->
Format.fprintf !out " %a [ label=\"Label %a (Stmt s%d)\" ] ;@." pretty u Clabels.pretty label s.Cil_types.sid
) ;
link u k ; u
let assign _env _stmt x e k =
let u = node () in
Format.fprintf !out " %a [ color=orange , label=\"%a := %a\" ] ;@." pretty u
Printer.pp_lval x Printer.pp_exp e ;
link u k ; u
let return _env _stmt r k =
let u = node () in
begin
match r with
| None ->
Format.fprintf !out " %a [ color=orange , label=\"Return\" ] ;@." pretty u
| Some e ->
Format.fprintf !out " %a [ color=orange , label=\"Return %a\" ] ;@." pretty u
Printer.pp_exp e
end ;
link u k ; u
let test _env _stmt e k1 k2 =
let u = node () in
Format.fprintf !out " %a [ color=cyan , label=\"If %a\" ] ;@." pretty u Printer.pp_exp e ;
link u k1 ; link u k2 ; u
let switch _env _stmt e cases def =
let u = node () in
Format.fprintf !out " %a [ color=cyan , label=\"Switch %a\" ] ;@." pretty u Printer.pp_exp e ;
List.iter (fun (_,k) -> link u k) cases ;
link u def ; u
let const _ x k =
let u = node () in
Format.fprintf !out " %a [ color=orange, label=\"const %a\" ] ;@."
pretty u Printer.pp_lval (Cil.var x) ;
link u k ; u
let init _ x init k =
let u = node () in
let pp_init fmt = function
| None -> Format.pp_print_string fmt "<default>"
| Some init -> Printer.pp_init fmt init
let fc = ref None
let out = ref Format.std_formatter
let knode = ref 0
let node () = incr knode ; !knode
let fopen kf bhv =
begin
let name =
match bhv with
| None -> Kernel_function.get_name kf
| Some bname -> Kernel_function.get_name kf ^ "_" ^ bname
in
Format.fprintf !out " %a [ color=orange, label=\"init %a := %a\" ] ;@."
pretty u Printer.pp_lval (Cil.var x) pp_init init ;
link u k ; u
let tag s k =
let u = node () in
Format.fprintf !out " %a [ color=cyan , label=\"Tag %s\" ] ;@." pretty u s ;
link u k ; u
let loop_entry w = tag "BeforeLoop" w
let loop_step w = tag "InLoop" w
let call_dynamic _env _stmt _pid fct calls =
let u = node () in
Format.fprintf !out " %a [ color=red , label \"CallPtr %a\" ];@." pretty u
Printer.pp_exp fct ;
List.iter (fun (_,k) -> link u k) calls ; u
let call_goal_precond env _stmt kf _es ~pre k =
let u = node () in
Format.fprintf !out " %a [ color=red , label=\"Prove PreCond %a%t\" ] ;@."
pretty u Kernel_function.pretty kf
begin fun fmt ->
if Wp_parameters.debug_atleast 1 then
List.iter
(fun (_,p) -> Format.fprintf fmt "\n@[<hov 2>Requires %a ;@]"
Printer.pp_predicate p) pre
end ;
ignore pre ;
Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
let call env stmt _r kf _es ~pre ~post ~pexit ~assigns ~p_post ~p_exit =
let u_post = List.fold_right (add_hyp env) post p_post in
let u_exit = List.fold_right (add_hyp env) pexit p_exit in
let u = node () in
link u u_post ; link u u_exit ;
Format.fprintf !out
" %a [ color=orange , label=\"Call %a @[<hov 2>(assigns%a)@]\" ] ;@."
pretty u Kernel_function.pretty kf pp_assigns assigns ;
ignore stmt ;
List.fold_right (add_hyp env) pre u
let pp_scope sc fmt xs =
let title = match sc with
| Mcfg.SC_Global -> "Global"
| Mcfg.SC_Frame_in -> "F-in"
| Mcfg.SC_Frame_out -> "F-out"
| Mcfg.SC_Block_in -> "B-in"
| Mcfg.SC_Block_out -> "B-out"
in begin
Format.fprintf fmt "%s {" title ;
List.iter (fun x -> Format.fprintf fmt " %a" Printer.pp_varinfo x) xs ;
Format.fprintf fmt " }" ;
end
let scope _kfenv xs scope k =
let file = Filename.concat (Wp_parameters.get_output () :> string) name in
Wp_parameters.feedback "CFG %a -> %s@." Kernel_function.pretty kf name ;
let fout = open_out (file ^ ".dot") in
fc := Some (fout,file) ;
out := Format.formatter_of_out_channel fout ;
Format.fprintf !out "digraph %a {@\n" Kernel_function.pretty kf ;
Format.fprintf !out " rankdir = TB ;@\n" ;
Format.fprintf !out " node [ style = filled, shape = box ] ;@\n" ;
Format.fprintf !out " N000 [ color = red, shape = circle, label = \"*\" ] ;@\n" ;
end
let flush () =
begin
Format.fprintf !out "}@." ;
out := Format.std_formatter ;
match !fc with
| None -> ()
| Some (fout,file) ->
close_out fout ;
ignore (Sys.command
(Printf.sprintf "dot -Tpdf %s.dot > %s.pdf" file file))
end
(* -------------------------------------------------------------------------- *)
(* --- MCFG Interface --- *)
(* -------------------------------------------------------------------------- *)
type t_prop = int (* current node *)
let pretty fmt k = Format.fprintf fmt "N%03d" k
let link a b =
if b =0
then Format.fprintf !out " %a -> %a [ style=dotted ];@." pretty a pretty b
else Format.fprintf !out " %a -> %a ;@." pretty a pretty b
let merge _env k1 k2 =
if k1=0 then k2 else
if k2=0 then k1 else
let u = node () in
Format.fprintf !out " %a [ color=lightblue , label=\"%a\" ] ;@." pretty u
(pp_scope scope) xs ;
link u k ; u
Format.fprintf !out " %a [ label=\"\" , shape=circle ] ;@." pretty u ;
link u k1 ; link u k2 ; u
let close kfenv k =
let empty = 0
let has_init _ = false
type t_env = Kernel_function.t
let new_env ?lvars kf : t_env = ignore lvars ; kf
let add_axiom _p _l = ()
let add_hyp _env (pid,pred) k =
let u = node () in
if Wp_parameters.debug_atleast 1 then
Format.fprintf !out " %a [ color=green , label=\"Assume %a\" ] ;@." pretty u Printer.pp_predicate pred
else
Format.fprintf !out " %a [ color=green , label=\"Assume %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
link u k ; u
let add_goal env (pid,pred) k =
let u = node () in
if Wp_parameters.debug_atleast 1 then
Format.fprintf !out " %a [ color=red , label=\"Prove %a\" ] ;@." pretty u Printer.pp_predicate pred
else
Format.fprintf !out " %a [ color=red , label=\"Prove %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
let pp_assigns fmt = function
| Cil_types.WritesAny -> Format.pp_print_string fmt " \\everything"
| Cil_types.Writes [] -> Format.pp_print_string fmt " \\nothing"
| Cil_types.Writes froms ->
List.iter
(fun (t,_) -> Format.fprintf fmt "@ %a" Printer.pp_identified_term t)
froms
let add_assigns env (pid,_) k =
let u = node () in
Format.fprintf !out " %a [ color=red , label=\"Assigns %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
let use_assigns _env region d k =
let u = node () in
begin match region with
| None ->
Format.fprintf !out " %a [ color=orange , label=\"Havoc All\" ] ;@." pretty u
| Some pid ->
Format.fprintf !out " %a [ color=orange , label=\"Havoc %a:\n@[<hov 2>assigns%a;@]\" ] ;@."
pretty u WpPropId.pp_propid pid
pp_assigns d.WpPropId.a_assigns
end ;
link u k ; u
let label _env stmt label k =
if Clabels.is_here label then k else
let u = node () in
Format.fprintf !out " %a [ color=cyan , label=\"Function %a\" ] ;@." pretty u
Kernel_function.pretty kfenv ;
( match stmt with
| None ->
Format.fprintf !out " %a [ label=\"Label %a\" ] ;@." pretty u Clabels.pretty label
| Some s ->
Format.fprintf !out " %a [ label=\"Label %a (Stmt s%d)\" ] ;@." pretty u Clabels.pretty label s.Cil_types.sid
) ;
link u k ; u
let build_prop_of_from _env _ps _k = 0
end
module WP = Calculus.Cfg(VC)
(* ------------------------------------------------------------------------ *)
(* --- Proof Obligation Generation --- *)
(* ------------------------------------------------------------------------ *)
class computer () =
let driver = Driver.load_driver () in
let model = Factory.(instance default driver) in
object
val mutable wptasks = []
method model = model
method add_lemma (_ : LogicUsage.logic_lemma) = ()
method add_strategy strategy =
wptasks <- strategy :: wptasks
method compute : Wpo.t Bag.t =
begin
(* Generates Wpos and accumulate exported goals *)
let assign _env _stmt x e k =
let u = node () in
Format.fprintf !out " %a [ color=orange , label=\"%a := %a\" ] ;@." pretty u
Printer.pp_lval x Printer.pp_exp e ;
link u k ; u
let return _env _stmt r k =
let u = node () in
begin
match r with
| None ->
Format.fprintf !out " %a [ color=orange , label=\"Return\" ] ;@." pretty u
| Some e ->
Format.fprintf !out " %a [ color=orange , label=\"Return %a\" ] ;@." pretty u
Printer.pp_exp e
end ;
link u k ; u
let test _env _stmt e k1 k2 =
let u = node () in
Format.fprintf !out " %a [ color=cyan , label=\"If %a\" ] ;@." pretty u Printer.pp_exp e ;
link u k1 ; link u k2 ; u
let switch _env _stmt e cases def =
let u = node () in
Format.fprintf !out " %a [ color=cyan , label=\"Switch %a\" ] ;@." pretty u Printer.pp_exp e ;
List.iter (fun (_,k) -> link u k) cases ;
link u def ; u
let const _ x k =
let u = node () in
Format.fprintf !out " %a [ color=orange, label=\"const %a\" ] ;@."
pretty u Printer.pp_lval (Cil.var x) ;
link u k ; u
let init _ x init k =
let u = node () in
let pp_init fmt = function
| None -> Format.pp_print_string fmt "<default>"
| Some init -> Printer.pp_init fmt init
in
Format.fprintf !out " %a [ color=orange, label=\"init %a := %a\" ] ;@."
pretty u Printer.pp_lval (Cil.var x) pp_init init ;
link u k ; u
let tag s k =
let u = node () in
Format.fprintf !out " %a [ color=cyan , label=\"Tag %s\" ] ;@." pretty u s ;
link u k ; u
let loop_entry w = tag "BeforeLoop" w
let loop_step w = tag "InLoop" w
let call_dynamic _env _stmt _pid fct calls =
let u = node () in
Format.fprintf !out " %a [ color=red , label \"CallPtr %a\" ];@." pretty u
Printer.pp_exp fct ;
List.iter (fun (_,k) -> link u k) calls ; u
let call_goal_precond env _stmt kf _es ~pre k =
let u = node () in
Format.fprintf !out " %a [ color=red , label=\"Prove PreCond %a%t\" ] ;@."
pretty u Kernel_function.pretty kf
begin fun fmt ->
if Wp_parameters.debug_atleast 1 then
List.iter
(fun strategy ->
let cfg = WpStrategy.cfg_of_strategy strategy in
let kf = Cil2cfg.cfg_kf cfg in
let bhv = WpStrategy.behavior_name_of_strategy strategy in
VC.create kf bhv ;
try ignore (WP.compute cfg strategy) ; VC.flush ()
with err -> VC.flush () ; raise err
) wptasks ;
wptasks <- [] ;
Bag.empty
end (* method compute *)
end (* class computer *)
let create () = (new computer () :> WpGenerator.computer)
(fun (_,p) -> Format.fprintf fmt "\n@[<hov 2>Requires %a ;@]"
Printer.pp_predicate p) pre
end ;
ignore pre ;
Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
let call env stmt _r kf _es ~pre ~post ~pexit ~assigns ~p_post ~p_exit =
let u_post = List.fold_right (add_hyp env) post p_post in
let u_exit = List.fold_right (add_hyp env) pexit p_exit in
let u = node () in
link u u_post ; link u u_exit ;
Format.fprintf !out
" %a [ color=orange , label=\"Call %a @[<hov 2>(assigns%a)@]\" ] ;@."
pretty u Kernel_function.pretty kf pp_assigns assigns ;
ignore stmt ;
List.fold_right (add_hyp env) pre u
let pp_scope sc fmt xs =
let title = match sc with
| Mcfg.SC_Global -> "Global"
| Mcfg.SC_Frame_in -> "F-in"
| Mcfg.SC_Frame_out -> "F-out"
| Mcfg.SC_Block_in -> "B-in"
| Mcfg.SC_Block_out -> "B-out"
in begin
Format.fprintf fmt "%s {" title ;
List.iter (fun x -> Format.fprintf fmt " %a" Printer.pp_varinfo x) xs ;
Format.fprintf fmt " }" ;
end
let scope _kfenv xs scope k =
let u = node () in
Format.fprintf !out " %a [ color=lightblue , label=\"%a\" ] ;@." pretty u
(pp_scope scope) xs ;
link u k ; u
let close kfenv k =
let u = node () in
Format.fprintf !out " %a [ color=cyan , label=\"Function %a\" ] ;@." pretty u
Kernel_function.pretty kfenv ;
link u k ; u
let build_prop_of_from _env _ps _k = 0
(* -------------------------------------------------------------------------- *)
src/plugins/wp/cfgDump.mli
+ 9
− 2
View file @ 55565c87
......@@ -20,6 +20,13 @@
(* *)
(**************************************************************************)
(* Produce a CfgProof.computer that dumps a graph of generated PO *)
(* Dump calls to Mcfg into DOT graphs *)
val create : unit -> WpGenerator.computer
open Cil_types
include Mcfg.S
val fopen : kernel_function -> string option -> unit
val flush : unit -> unit
(**************************************************************************)
src/plugins/wp/cfgWP.ml
+ 3
− 88
View file @ 55565c87
......@@ -1434,100 +1434,15 @@ end
(* -------------------------------------------------------------------------- *)
(* Cache by Model Context *)
module CONTEXT = Hashtbl.Make(WpContext.MODEL)
let vcgenerators = CONTEXT.create 1
let vcgenerators = WpContext.MINDEX.create 1
let vcgen setup driver : (module VCgen) =
let model = Factory.instance setup driver in
try CONTEXT.find vcgenerators model
try WpContext.MINDEX.find vcgenerators model
with Not_found ->
let module M = (val Factory.(compiler setup.mheap setup.mvar)) in
let vcgen = (module VC(M) : VCgen) in
CONTEXT.add vcgenerators model vcgen ;
WpContext.MINDEX.add vcgenerators model vcgen ;
vcgen
(* -------------------------------------------------------------------------- *)
(* --- WPO Computer --- *)
(* -------------------------------------------------------------------------- *)
module KFmap = Kernel_function.Map
module Computer(VCG : VCgen) =
struct
module WP = Calculus.Cfg(VCG)
let prove_strategy collection model kf strategy =
let cfg = WpStrategy.cfg_of_strategy strategy in
let bhv = WpStrategy.get_bhv strategy in
let index = Wpo.Function( kf , bhv ) in
if WpRTE.missing_guards model kf then
Wp_parameters.warning ~current:false ~once:true
"Missing RTE guards" ;
try
let (results,_) = WP.compute cfg strategy in
List.iter
(fun wp ->
let wcs = VCG.compile_wp index wp in
collection := Bag.concat !collection wcs
) results
with Warning.Error(source,reason) ->
Wp_parameters.failure
~current:false "From %s: %s" source reason
class wp (model:WpContext.model) =
object
val mutable lemmas : LogicUsage.logic_lemma Bag.t = Bag.empty
val mutable annots : WpStrategy.strategy Bag.t KFmap.t = KFmap.empty
method model = model
method add_lemma lemma = lemmas <- Bag.append lemmas lemma
method add_strategy strategy =
let kf = WpStrategy.get_kf strategy in
let sf = try KFmap.find kf annots with Not_found -> Bag.empty in
annots <- KFmap.add kf (Bag.append sf strategy) annots
method compute : Wpo.t Bag.t =
begin
let collection = ref Bag.empty in
Lang.F.release () ;
WpContext.on_context (model,WpContext.Global)
begin fun () ->
LogicUsage.iter_lemmas VCG.register_lemma ;
Bag.iter (fun l ->
if l.lem_kind <> `Axiom then
let vc = VCG.compile_lemma l in
collection := Bag.append !collection vc
) lemmas ;
end () ;
KFmap.iter
(fun kf strategies ->
WpContext.on_context (model,WpContext.Kf kf)
begin fun () ->
LogicUsage.iter_lemmas VCG.register_lemma ;
Bag.iter (prove_strategy collection model kf) strategies ;
end ()
) annots ;
lemmas <- Bag.empty ;
annots <- KFmap.empty ;
Lang.F.release () ;
!collection
end
end
end
let computers = CONTEXT.create 1
let computer setup driver =
let model = Factory.instance setup driver in
try CONTEXT.find computers model
with Not_found ->
let module VCG = (val vcgen setup driver) in
let module CC = Computer(VCG) in
let computer = (new CC.wp model :> WpGenerator.computer) in
CONTEXT.add computers model computer ; computer
(* -------------------------------------------------------------------------- *)
src/plugins/wp/cfgWP.mli
+ 2
− 2
View file @ 55565c87
......@@ -23,7 +23,7 @@
open LogicUsage
(* -------------------------------------------------------------------------- *)
(* --- WP Calculus --- *)
(* --- VC Generator --- *)
(* -------------------------------------------------------------------------- *)
module type VCgen =
......@@ -36,4 +36,4 @@ end
val vcgen : Factory.setup -> Factory.driver -> (module VCgen)
val computer : Factory.setup -> Factory.driver -> WpGenerator.computer
(* -------------------------------------------------------------------------- *)
src/plugins/wp/wpContext.ml
+ 2
− 0
View file @ 55565c87
......@@ -56,6 +56,8 @@ struct
}
end
module MINDEX = Hashtbl.Make(MODEL)
module MODELS =
struct
......
src/plugins/wp/wpContext.mli
+ 2
− 0
View file @ 55565c87
......@@ -78,6 +78,8 @@ sig
val compare : t -> t -> int
end
module MINDEX : Hashtbl.S with type key = model
val is_defined : unit -> bool
val on_context : context -> ('a -> 'b) -> 'a -> 'b
val get_model : unit -> model
......
src/plugins/wp/wpGenerator.ml
+ 130
− 0
View file @ 55565c87
......@@ -95,3 +95,133 @@ let compute_call cc stmt =
cc#compute
(* -------------------------------------------------------------------------- *)
(* --- WPO Computer --- *)
(* -------------------------------------------------------------------------- *)
module KFmap = Kernel_function.Map
module Computer(VCG : CfgWP.VCgen) =
struct
open LogicUsage
module WP = Calculus.Cfg(VCG)
let prove_strategy collection model kf strategy =
let cfg = WpStrategy.cfg_of_strategy strategy in
let bhv = WpStrategy.get_bhv strategy in
let index = Wpo.Function( kf , bhv ) in
if WpRTE.missing_guards model kf then
Wp_parameters.warning ~current:false ~once:true
"Missing RTE guards" ;
try
let (results,_) = WP.compute cfg strategy in
List.iter
(fun wp ->
let wcs = VCG.compile_wp index wp in
collection := Bag.concat !collection wcs
) results
with Warning.Error(source,reason) ->
Wp_parameters.failure
~current:false "From %s: %s" source reason
class wp (model:WpContext.model) =
object
val mutable lemmas : LogicUsage.logic_lemma Bag.t = Bag.empty
val mutable annots : WpStrategy.strategy Bag.t KFmap.t = KFmap.empty
method model = model
method add_lemma lemma = lemmas <- Bag.append lemmas lemma
method add_strategy strategy =
let kf = WpStrategy.get_kf strategy in
let sf = try KFmap.find kf annots with Not_found -> Bag.empty in
annots <- KFmap.add kf (Bag.append sf strategy) annots
method compute : Wpo.t Bag.t =
begin
let collection = ref Bag.empty in
Lang.F.release () ;
WpContext.on_context (model,WpContext.Global)
begin fun () ->
LogicUsage.iter_lemmas VCG.register_lemma ;
Bag.iter (fun l ->
if l.lem_kind <> `Axiom then
let vc = VCG.compile_lemma l in
collection := Bag.append !collection vc
) lemmas ;
end () ;
KFmap.iter
(fun kf strategies ->
WpContext.on_context (model,WpContext.Kf kf)
begin fun () ->
LogicUsage.iter_lemmas VCG.register_lemma ;
Bag.iter (prove_strategy collection model kf) strategies ;
end ()
) annots ;
lemmas <- Bag.empty ;
annots <- KFmap.empty ;
Lang.F.release () ;
!collection
end
end
end
(* -------------------------------------------------------------------------- *)
(* --- Dump Computer --- *)
(* -------------------------------------------------------------------------- *)
module DUMPER = Calculus.Cfg(CfgDump)
let dumper () =
let driver = Driver.load_driver () in
let model = Factory.(instance default driver) in
object
val mutable wptasks = []
method model = model
method add_lemma (_ : LogicUsage.logic_lemma) = ()
method add_strategy strategy =
wptasks <- strategy :: wptasks
method compute : Wpo.t Bag.t =
begin
(* Generates Wpos and accumulate exported goals *)
List.iter
(fun strategy ->
let cfg = WpStrategy.cfg_of_strategy strategy in
let kf = Cil2cfg.cfg_kf cfg in
let bhv = WpStrategy.behavior_name_of_strategy strategy in
CfgDump.fopen kf bhv ;
try
ignore (DUMPER.compute cfg strategy) ;
CfgDump.flush ()
with err ->
CfgDump.flush () ;
raise err
) wptasks ;
wptasks <- [] ;
Bag.empty
end
end
(* -------------------------------------------------------------------------- *)
(* --- Generators --- *)
(* -------------------------------------------------------------------------- *)
let generators = WpContext.MINDEX.create 1
let computer setup driver =
let model = Factory.instance setup driver in
try WpContext.MINDEX.find generators model
with Not_found ->
let module VCG = (val CfgWP.vcgen setup driver) in
let module CC = Computer(VCG) in
let computer = (new CC.wp model :> computer) in
WpContext.MINDEX.add generators model computer ; computer
(* -------------------------------------------------------------------------- *)
src/plugins/wp/wpGenerator.mli
+ 3
− 0
View file @ 55565c87
......@@ -48,3 +48,6 @@ val compute_selection : computer ->
?bhv:string list ->
?prop:string list ->
unit -> Wpo.t Bag.t
val dumper : unit -> computer
val computer : Factory.setup -> Factory.driver -> computer
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment