From 078a8ca367236fbbd377472339e3af9eebd03149 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 21 Jan 2021 11:43:14 +0100
Subject: [PATCH] [wp] new generator API
---
src/plugins/wp/Generator.ml | 68 +++++++++++++++++++++++++++-------
src/plugins/wp/Generator.mli | 17 +++++----
src/plugins/wp/VC.ml | 21 +++++------
src/plugins/wp/VC.mli | 3 +-
src/plugins/wp/register.ml | 63 +++++--------------------------
src/plugins/wp/wpGenerator.mli | 1 -
6 files changed, 84 insertions(+), 89 deletions(-)
diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml
index 9743f526096..beb32219b4f 100644
--- a/src/plugins/wp/Generator.ml
+++ b/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
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Generator.mli b/src/plugins/wp/Generator.mli
index b8ea58c425d..18e2e598791 100644
--- a/src/plugins/wp/Generator.mli
+++ b/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
diff --git a/src/plugins/wp/VC.ml b/src/plugins/wp/VC.ml
index c3a52fece6f..f921d0000a3 100644
--- a/src/plugins/wp/VC.ml
+++ b/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 --- *)
diff --git a/src/plugins/wp/VC.mli b/src/plugins/wp/VC.mli
index f073fffb021..d39e04dc2ca 100644
--- a/src/plugins/wp/VC.mli
+++ b/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} *)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 0d9cc989747..0174cc73384 100644
--- a/src/plugins/wp/register.ml
+++ b/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
diff --git a/src/plugins/wp/wpGenerator.mli b/src/plugins/wp/wpGenerator.mli
index bf7e8b697c1..8152205db34 100644
--- a/src/plugins/wp/wpGenerator.mli
+++ b/src/plugins/wp/wpGenerator.mli
@@ -48,4 +48,3 @@ val compute_selection : computer ->
?bhv:string list ->
?prop:string list ->
unit -> Wpo.t Bag.t
-
--
GitLab