[wp] new generator API

src/plugins/wp/Generator.ml

@@ -23,6 +23,39 @@
 open Cil_types
 open Wp_parameters
 
+(* -------------------------------------------------------------------------- *)
+(* --- Model Setup                                                        --- *)
+(* -------------------------------------------------------------------------- *)
+
+let user_setup () : Factory.setup =
+  begin
+    match Wp_parameters.Model.get () with
+    | ["Runtime"] ->
+        Wp_parameters.abort
+          "Model 'Runtime' is no more available.@\nIt will be reintroduced \
+           in a future release."
+    | ["Logic"] ->
+        Wp_parameters.warning ~once:true
+          "Deprecated 'Logic' model.@\nUse 'Typed' with option '-wp-ref' \
+           instead." ;
+        {
+          mheap = Factory.Typed MemTyped.Fits ;
+          mvar = Factory.Ref ;
+          cint = Cint.Natural ;
+          cfloat = Cfloat.Real ;
+        }
+    | ["Store"] ->
+        Wp_parameters.warning ~once:true
+          "Deprecated 'Store' model.@\nUse 'Typed' instead." ;
+        {
+          mheap = Factory.Typed MemTyped.Fits ;
+          mvar = Factory.Var ;
+          cint = Cint.Natural ;
+          cfloat = Cfloat.Real ;
+        }
+    | spec -> Factory.parse spec
+  end
+
 (* -------------------------------------------------------------------------- *)
 (* --- WP Computer (main entry points)                                    --- *)
 (* -------------------------------------------------------------------------- *)
@@ -30,27 +63,36 @@ open Wp_parameters
 class type t =
   object
     method model : WpContext.model
-    method generate_ip : Property.t -> Wpo.t Bag.t
-    method generate_kf : kernel_function -> Wpo.t Bag.t
-    method generate_call : stmt -> Wpo.t Bag.t
-    method generate_main :
+    method compute_ip : Property.t -> Wpo.t Bag.t
+    method compute_call : stmt -> Wpo.t Bag.t
+    method compute_main :
       ?fct:functions ->
       ?bhv:string list ->
       ?prop:string list ->
       unit -> Wpo.t Bag.t
   end
 
-type computer = [ `Dump | `Legacy | `Cfg ]
-
-let make
-    ?(computer = `Cfg)
+let create
+    ?dump ?legacy
     ?(setup: Factory.setup option)
     ?(driver: Factory.driver option)
     () : t =
-  ignore setup ; ignore driver ;
-  match (computer : computer) with
-  | `Cfg -> assert false
-  | `Dump -> assert false
-  | `Legacy -> assert false
+  let default f = function Some v -> v | None -> f () in
+  let dump = default Wp_parameters.Dump.get dump in
+  let legacy = default Wp_parameters.Dump.get legacy in
+  let driver = default Driver.load_driver driver in
+  let setup = default user_setup setup in
+  ignore legacy ;
+  let cc =
+    if dump
+    then ( Cil2cfg.Dump.process () ; CfgDump.create () )
+    else CfgWP.computer setup driver in
+  let the_model = cc#model in
+  object
+    method model = the_model
+    method compute_ip = WpGenerator.compute_ip cc
+    method compute_call = WpGenerator.compute_call cc
+    method compute_main = WpGenerator.compute_selection cc
+  end
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/Generator.mli

@@ -27,23 +27,24 @@ open Wp_parameters
 (* --- WP Computer (main entry points)                                    --- *)
 (* -------------------------------------------------------------------------- *)
 
+(** Compute model setup from command line options. *)
+val user_setup : unit -> Factory.setup
+
 class type t =
   object
     method model : WpContext.model
-    method generate_ip : Property.t -> Wpo.t Bag.t
-    method generate_kf : kernel_function -> Wpo.t Bag.t
-    method generate_call : stmt -> Wpo.t Bag.t
-    method generate_main :
+    method compute_ip : Property.t -> Wpo.t Bag.t
+    method compute_call : stmt -> Wpo.t Bag.t
+    method compute_main :
       ?fct:functions ->
       ?bhv:string list ->
       ?prop:string list ->
       unit -> Wpo.t Bag.t
   end
 
-type computer = [ `Dump | `Legacy | `Cfg ]
-
-val make :
-  ?computer:computer ->
+val create :
+  ?dump:bool ->
+  ?legacy:bool ->
   ?setup:Factory.setup ->
   ?driver:Factory.driver ->
   unit -> t

src/plugins/wp/VC.ml

@@ -69,24 +69,21 @@ let () = Property_status.register_property_remove_hook remove
 (* --- Generator Interface                                                --- *)
 (* -------------------------------------------------------------------------- *)
 
-let generator ?model () =
+let generator model =
   let setup = match model with
-    | None -> Register.setup ()
-    | Some s -> Factory.parse [s] in
-  let driver = Driver.load_driver () in
-  CfgWP.computer setup driver
+    | None -> None
+    | Some s -> Some (Factory.parse [s]) in
+  Generator.create ~dump:false ?setup ()
 
 let generate_ip ?model ip =
-  let gen = generator ?model () in
-  WpGenerator.compute_ip gen ip
+  (generator model)#compute_ip ip
 
-let generate_kf ?model ?(bhv=[]) kf =
-  let gen = generator ?model () in
-  WpGenerator.compute_kf gen ~bhv ~kf ()
+let generate_kf ?model ?bhv ?prop kf =
+  let kfs = Kernel_function.Set.singleton kf in
+  (generator model)#compute_main ~fct:(Fct_list kfs) ?bhv ?prop ()
 
 let generate_call ?model stmt =
-  let gen = generator ?model () in
-  WpGenerator.compute_call gen stmt
+  (generator model)#compute_call stmt
 
 (* -------------------------------------------------------------------------- *)
 (* --- Prover Interface                                                   --- *)

src/plugins/wp/VC.mli

@@ -66,7 +66,8 @@ val iter_kf : (t -> unit) -> ?bhv:string list -> Kernel_function.t -> unit
 *)
 
 val generate_ip : ?model:string -> Property.t -> t Bag.t
-val generate_kf : ?model:string -> ?bhv:string list -> Kernel_function.t -> t Bag.t
+val generate_kf : ?model:string -> ?bhv:string list -> ?prop:string list ->
+  Kernel_function.t -> t Bag.t
 val generate_call : ?model:string -> Cil_types.stmt -> t Bag.t
 
 (** {2 Prover Interface} *)

src/plugins/wp/register.ml

@@ -20,56 +20,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Factory
-
 let dkey_main = Wp_parameters.register_category "main"
 let dkey_raised = Wp_parameters.register_category "raised"
 let wkey_smoke = Wp_parameters.register_warn_category "smoke"
 
-(* --------- Command Line ------------------- *)
-
-let setup () : setup =
-  begin
-    match Wp_parameters.Model.get () with
-    | ["Runtime"] ->
-        Wp_parameters.abort
-          "Model 'Runtime' is no more available.@\nIt will be reintroduced \
-           in a future release."
-    | ["Logic"] ->
-        Wp_parameters.warning ~once:true
-          "Deprecated 'Logic' model.@\nUse 'Typed' with option '-wp-ref' \
-           instead." ;
-        {
-          mheap = Factory.Typed MemTyped.Fits ;
-          mvar = Factory.Ref ;
-          cint = Cint.Natural ;
-          cfloat = Cfloat.Real ;
-        }
-    | ["Store"] ->
-        Wp_parameters.warning ~once:true
-          "Deprecated 'Store' model.@\nUse 'Typed' instead." ;
-        {
-          mheap = Factory.Typed MemTyped.Fits ;
-          mvar = Factory.Var ;
-          cint = Cint.Natural ;
-          cfloat = Cfloat.Real ;
-        }
-    | spec -> Factory.parse spec
-  end
-
-let set_model (s:setup) =
-  Wp_parameters.Model.set [Factory.ident s]
-
-(* --------- WP Computer -------------------- *)
-
-let computer () =
-  if Wp_parameters.Dump.get ()
-  then begin
-    Cil2cfg.Dump.process () ;
-    CfgDump.create ()
-  end
-  else CfgWP.computer (setup ()) (Driver.load_driver ())
-
 (* ------------------------------------------------------------------------ *)
 (* --- Memory Model Hypotheses                                          --- *)
 (* ------------------------------------------------------------------------ *)
@@ -751,11 +705,12 @@ let cmdline_run () =
     if fct <> Wp_parameters.Fct_none then
       begin
         Wp_parameters.feedback ~ontty:`Feedback "Running WP plugin...";
-        let computer = computer () in
+        let generator = Generator.create () in
+        let model = generator#model in
         Ast.compute ();
         Dyncall.compute ();
         if Wp_parameters.RTE.get () then
-          WpRTE.generate_all computer#model ;
+          WpRTE.generate_all model ;
         if Wp_parameters.has_dkey dkey_logicusage then
           begin
             LogicUsage.compute ();
@@ -771,14 +726,14 @@ let cmdline_run () =
         (** TODO entry point *)
         if Wp_parameters.has_dkey dkey_builtins then
           begin
-            WpContext.on_context (computer#model,WpContext.Global)
+            WpContext.on_context (model,WpContext.Global)
               LogicBuiltins.dump ();
           end ;
-        WpTarget.compute computer#model ;
-        wp_compute_memory_context computer#model ;
+        WpTarget.compute model ;
+        wp_compute_memory_context model ;
         if Wp_parameters.CheckMemoryContext.get () then
-          wp_insert_memory_context computer#model ;
-        let goals = WpGenerator.compute_selection computer ~fct ~bhv ~prop () in
+          wp_insert_memory_context model ;
+        let goals = generator#compute_main ~fct ~bhv ~prop () in
         do_wp_proofs goals ;
         begin
           if fct <> Wp_parameters.Fct_all then
@@ -786,7 +741,7 @@ let cmdline_run () =
           else
             do_wp_print () ;
         end ;
-        do_wp_report computer#model ;
+        do_wp_report model ;
       end
   end
 

src/plugins/wp/wpGenerator.mli

@@ -48,4 +48,3 @@ val compute_selection : computer ->
   ?bhv:string list ->
   ?prop:string list ->
   unit -> Wpo.t Bag.t
-