diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml
index 9a2126959e46d505d62f97cad828adf004fce492..07056383cae40e184e59c80043902c57f933423b 100644
--- a/src/plugins/wp/Generator.ml
+++ b/src/plugins/wp/Generator.ml
@@ -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
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index a8b412bebf4578af00c3fddebd0e0cceafc0122f..b5be8ba4fe25d91432e1a7a36efed1b5cedf0998 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -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:=
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index 657deb22733ad05f924bd70a0d67854bf85651d6..7b658aabcb730b8b1e80a6fdf07dc4407556122a 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/src/plugins/wp/cfgDump.ml
@@ -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
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgDump.mli b/src/plugins/wp/cfgDump.mli
index 448a36b2edd3b372808569cae6e2e11b20948333..e4a1c460c5c6d27ee26a42198418fa7f8e9085a6 100644
--- a/src/plugins/wp/cfgDump.mli
+++ b/src/plugins/wp/cfgDump.mli
@@ -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
+
+(**************************************************************************)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 3edbc6f7cf68c4aaad57f94e5153c1105df530a1..9eb93eac1055cb55ef9951b1d52f650859621bdd 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -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
-
-(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgWP.mli b/src/plugins/wp/cfgWP.mli
index fa801f3fb46262636d0397fbb203a626064e4e18..c93dfacd142d35baebb1105a5eef4af94e2b4901 100644
--- a/src/plugins/wp/cfgWP.mli
+++ b/src/plugins/wp/cfgWP.mli
@@ -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
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpContext.ml b/src/plugins/wp/wpContext.ml
index acc32631cad27c54f7759b625abc66d6cde26b94..dfeb7875285396d6f6bba393c865aef0843826c1 100644
--- a/src/plugins/wp/wpContext.ml
+++ b/src/plugins/wp/wpContext.ml
@@ -56,6 +56,8 @@ struct
}
end
+module MINDEX = Hashtbl.Make(MODEL)
+
module MODELS =
struct
diff --git a/src/plugins/wp/wpContext.mli b/src/plugins/wp/wpContext.mli
index a52c5af5f7fbde050c2b4f0b6ec0fb65e5177a89..2994772402f66185ef12ee3530fa74c4818d9cb6 100644
--- a/src/plugins/wp/wpContext.mli
+++ b/src/plugins/wp/wpContext.mli
@@ -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
diff --git a/src/plugins/wp/wpGenerator.ml b/src/plugins/wp/wpGenerator.ml
index 508f6e79c5366adff5352f512738d065dc025864..b45adae1a34cbf0007b2324be781f42572b9d38d 100644
--- a/src/plugins/wp/wpGenerator.ml
+++ b/src/plugins/wp/wpGenerator.ml
@@ -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
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpGenerator.mli b/src/plugins/wp/wpGenerator.mli
index 8152205db349315c7c11fc86212d9c44837b49b8..efbcfc897c347509c14b48091e7fce9b03f9ad34 100644
--- a/src/plugins/wp/wpGenerator.mli
+++ b/src/plugins/wp/wpGenerator.mli
@@ -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