From 57ef0791a36176949ed1caf63a2d41f0322d23b2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 21 Jan 2021 17:14:17 +0100
Subject: [PATCH] [wp] new generator API
---
src/plugins/wp/Factory.mli | 2 ++
src/plugins/wp/Generator.ml | 17 +-----------
src/plugins/wp/Generator.mli | 16 ++---------
src/plugins/wp/Makefile.in | 2 +-
src/plugins/wp/cfgGenerator.ml | 49 +++++++++++++++++++++++++++++++++
src/plugins/wp/cfgGenerator.mli | 29 +++++++++++++++++++
src/plugins/wp/cfgWP.ml | 2 +-
src/plugins/wp/wpo.ml | 18 ++++++++++++
src/plugins/wp/wpo.mli | 18 ++++++++++++
9 files changed, 121 insertions(+), 32 deletions(-)
create mode 100644 src/plugins/wp/cfgGenerator.ml
create mode 100644 src/plugins/wp/cfgGenerator.mli
diff --git a/src/plugins/wp/Factory.mli b/src/plugins/wp/Factory.mli
index 913d151300e..e45f966ff83 100644
--- a/src/plugins/wp/Factory.mli
+++ b/src/plugins/wp/Factory.mli
@@ -50,3 +50,5 @@ val parse :
Apply specifications to default setup.
Default setup is [Factory.default].
Default warning is [Wp_parameters.abort]. *)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml
index 07056383cae..dbe19558090 100644
--- a/src/plugins/wp/Generator.ml
+++ b/src/plugins/wp/Generator.ml
@@ -20,9 +20,6 @@
(* *)
(**************************************************************************)
-open Cil_types
-open Wp_parameters
-
(* -------------------------------------------------------------------------- *)
(* --- Model Setup --- *)
(* -------------------------------------------------------------------------- *)
@@ -60,23 +57,11 @@ let user_setup () : Factory.setup =
(* --- WP Computer (main entry points) --- *)
(* -------------------------------------------------------------------------- *)
-class type t =
- object
- method model : WpContext.model
- 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
-
let create
?dump ?legacy
?(setup: Factory.setup option)
?(driver: Factory.driver option)
- () : t =
+ () : Wpo.generator =
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
diff --git a/src/plugins/wp/Generator.mli b/src/plugins/wp/Generator.mli
index 18e2e598791..fc70c5d2fed 100644
--- a/src/plugins/wp/Generator.mli
+++ b/src/plugins/wp/Generator.mli
@@ -18,7 +18,7 @@
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
-(**************************************************************************)
+(*****************************************t*********************************)
open Cil_types
open Wp_parameters
@@ -30,23 +30,11 @@ open Wp_parameters
(** Compute model setup from command line options. *)
val user_setup : unit -> Factory.setup
-class type t =
- object
- method model : WpContext.model
- 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
-
val create :
?dump:bool ->
?legacy:bool ->
?setup:Factory.setup ->
?driver:Factory.driver ->
- unit -> t
+ unit -> Wpo.generator
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index b5be8ba4fe2..ca2827bdb96 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -99,7 +99,7 @@ PLUGIN_CMO:= \
Factory \
cfgInit cfgAnnot cfgCalculus \
calculus cfgDump cfgWP \
- wpGenerator \
+ wpGenerator cfgGenerator \
Generator register VC
PLUGIN_CMI:=
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
new file mode 100644
index 00000000000..0350785f987
--- /dev/null
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- New WP Computer (main entry points) --- *)
+(* -------------------------------------------------------------------------- *)
+
+let generators = WpContext.MINDEX.create 1
+
+let generator 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 WP = CfgCalculus.Make(VCG) in
+ let generator : Wpo.generator =
+ object
+ method model = model
+ method compute_ip _ = Bag.empty
+ method compute_call _ = Bag.empty
+ method compute_main ?fct ?bhv ?prop () =
+ ignore fct ;
+ ignore bhv ;
+ ignore prop ;
+ Bag.empty
+ end in
+ WpContext.MINDEX.add generators model generator ;
+ generator
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgGenerator.mli b/src/plugins/wp/cfgGenerator.mli
new file mode 100644
index 00000000000..16461afeba1
--- /dev/null
+++ b/src/plugins/wp/cfgGenerator.mli
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- New WP Computer (main entry points) --- *)
+(* -------------------------------------------------------------------------- *)
+
+val generator : Factory.setup -> Factory.driver -> Wpo.generator
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 9eb93eac105..4f563fae449 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1407,7 +1407,7 @@ struct
Wpo.VC_Lemma.depends = l.lem_depends ;
Wpo.VC_Lemma.lemma = def ;
Wpo.VC_Lemma.sequent = None ;
- } in
+ } in
let index = match LogicUsage.section_of_lemma l.lem_name with
| LogicUsage.Toplevel _ -> Wpo.Axiomatic None
| LogicUsage.Axiomatic a -> Wpo.Axiomatic (Some a.ax_name) in
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index fde027b2692..50d2653fc06 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -1010,3 +1010,21 @@ let get_files w =
) results []
in
descr_files @ result_files
+
+(* -------------------------------------------------------------------------- *)
+(* --- Generators --- *)
+(* -------------------------------------------------------------------------- *)
+
+class type generator =
+ object
+ method model : WpContext.model
+ method compute_ip : Property.t -> t Bag.t
+ method compute_call : stmt -> t Bag.t
+ method compute_main :
+ ?fct:Wp_parameters.functions ->
+ ?bhv:string list ->
+ ?prop:string list ->
+ unit -> t Bag.t
+ end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index fa6d1c337f4..753c1c38369 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -210,3 +210,21 @@ val pp_goal_flow : Format.formatter -> t -> unit
(** Dynamically exported. *)
val prover_of_name : string -> prover option
+
+(* -------------------------------------------------------------------------- *)
+(* --- Generators --- *)
+(* -------------------------------------------------------------------------- *)
+
+class type generator =
+ object
+ method model : WpContext.model
+ method compute_ip : Property.t -> t Bag.t
+ method compute_call : stmt -> t Bag.t
+ method compute_main :
+ ?fct:Wp_parameters.functions ->
+ ?bhv:string list ->
+ ?prop:string list ->
+ unit -> t Bag.t
+ end
+
+(* -------------------------------------------------------------------------- *)
--
GitLab