From e026c8cc051a449f6dc49d636b224ddef44bed91 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 5 May 2022 14:45:30 +0200
Subject: [PATCH] [Eva] Removes module type Abstract.Interface, which is
exactly Structure.External.
---
.../value/partitioning/partitioning_index.ml | 10 +----
.../value/partitioning/partitioning_index.mli | 9 +----
src/plugins/value/utils/abstract.ml | 12 ++----
src/plugins/value/utils/abstract.mli | 37 +++++--------------
src/plugins/value/utils/structure.ml | 1 +
src/plugins/value/utils/structure.mli | 15 ++++++++
6 files changed, 30 insertions(+), 54 deletions(-)
diff --git a/src/plugins/value/partitioning/partitioning_index.ml b/src/plugins/value/partitioning/partitioning_index.ml
index 431e0f05ebb..29660a56c04 100644
--- a/src/plugins/value/partitioning/partitioning_index.ml
+++ b/src/plugins/value/partitioning/partitioning_index.ml
@@ -20,17 +20,9 @@
(* *)
(**************************************************************************)
-module type Domain = sig
- include Abstract_domain.Lattice
- include Datatype.S_with_collections with type t = state
- include Abstract.Interface with type t := state
- and type 'a key := 'a Abstract_domain.key
-end
-
(** Partition of the abstract states, computed for each node by the
dataflow analysis. *)
-module Make
- (Domain : Domain)
+module Make (Domain : Abstract.Domain.External)
= struct
module Index = Hashtbl.Make (Cvalue_domain.Subpart)
diff --git a/src/plugins/value/partitioning/partitioning_index.mli b/src/plugins/value/partitioning/partitioning_index.mli
index 7d119f87db2..21bdef9d1fd 100644
--- a/src/plugins/value/partitioning/partitioning_index.mli
+++ b/src/plugins/value/partitioning/partitioning_index.mli
@@ -30,14 +30,7 @@
Partitioning index relies on an heuristics on the cvalue domain,
and is very inefficient without it. *)
-module type Domain = sig
- include Abstract_domain.Lattice
- include Datatype.S_with_collections with type t = state
- include Abstract.Interface with type t := state
- and type 'a key := 'a Abstract_domain.key
-end
-
-module Make (Domain: Domain) : sig
+module Make (Domain: Abstract.Domain.External) : sig
type t
(** Creates an empty index. *)
diff --git a/src/plugins/value/utils/abstract.ml b/src/plugins/value/utils/abstract.ml
index 1b5be7c02b3..266de82c9fb 100644
--- a/src/plugins/value/utils/abstract.ml
+++ b/src/plugins/value/utils/abstract.ml
@@ -20,15 +20,6 @@
(* *)
(**************************************************************************)
-(** External interface of an abstraction, built by {!Structure.Open}. *)
-module type Interface = sig
- type t
- type 'a key
- val mem : 'a key -> bool
- val get : 'a key -> (t -> 'a) option
- val set : 'a key -> 'a -> t -> t
-end
-
module Value = struct
module V = struct
@@ -46,6 +37,7 @@ module Value = struct
include Internal
include Structure.External with type t := t
and type 'a key := 'a key
+ and type 'a data := 'a data
end
end
@@ -66,6 +58,7 @@ module Location = struct
include Internal
include Structure.External with type t := location
and type 'a key := 'a key
+ and type 'a data := 'a data
end
end
@@ -86,6 +79,7 @@ module Domain = struct
include Internal
include Structure.External with type t := t
and type 'a key := 'a key
+ and type 'a data := 'a data
val get_cvalue: (t -> Cvalue.Model.t) option
val get_cvalue_or_top: t -> Cvalue.Model.t
diff --git a/src/plugins/value/utils/abstract.mli b/src/plugins/value/utils/abstract.mli
index 087cae69ffc..1e27948b1c3 100644
--- a/src/plugins/value/utils/abstract.mli
+++ b/src/plugins/value/utils/abstract.mli
@@ -33,28 +33,6 @@
Note that their behavior is undefined if an abstraction contains
several times the same leaf module. *)
-(** External interface of an abstraction, built by {!Structure.Open}. *)
-module type Interface = sig
- type t
- type 'a key
-
- (** Tests whether a key belongs to the module. *)
- val mem : 'a key -> bool
-
- (** For a key of type [k key]:
- - if the values of type [t] contain a subpart of type [k] from a module
- identified by the key, then [get key] returns an accessor for it.
- - otherwise, [get key] returns None. *)
- val get : 'a key -> (t -> 'a) option
-
- (** For a key of type [k key]:
- - if the values of type [t] contain a subpart of type [k] from a module
- identified by the key, then [set key v t] returns the value [t] in which
- this subpart has been replaced by [v].
- - otherwise, [set key _] is the identity function. *)
- val set : 'a key -> 'a -> t -> t
-end
-
(** Key and structure for abstract values.
See {structure.mli} for more details. *)
module Value : sig
@@ -69,8 +47,9 @@ module Value : sig
module type External = sig
include Internal
- include Interface with type t := t
- and type 'a key := 'a key
+ include Structure.External with type t := t
+ and type 'a key := 'a key
+ and type 'a data := 'a data
end
end
@@ -88,8 +67,9 @@ module Location : sig
module type External = sig
include Internal
- include Interface with type t := location
- and type 'a key := 'a key
+ include Structure.External with type t := location
+ and type 'a key := 'a key
+ and type 'a data := 'a data
end
end
@@ -107,8 +87,9 @@ module Domain : sig
module type External = sig
include Internal
- include Interface with type t := t
- and type 'a key := 'a key
+ include Structure.External with type t := t
+ and type 'a key := 'a key
+ and type 'a data := 'a data
(** Special accessors for the main cvalue domain. *)
val get_cvalue: (t -> Cvalue.Model.t) option
diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml
index c16589366c5..0df7cdad3ee 100644
--- a/src/plugins/value/utils/structure.ml
+++ b/src/plugins/value/utils/structure.ml
@@ -143,6 +143,7 @@ end
module type External = sig
type t
type 'a key
+ type 'a data
val mem : 'a key -> bool
val get : 'a key -> (t -> 'a) option
val set : 'a key -> 'a -> t -> t
diff --git a/src/plugins/value/utils/structure.mli b/src/plugins/value/utils/structure.mli
index e98ec0c7b05..942ffb87331 100644
--- a/src/plugins/value/utils/structure.mli
+++ b/src/plugins/value/utils/structure.mli
@@ -89,8 +89,22 @@ end
module type External = sig
type t
type 'a key
+ type 'a data
+
+ (** Tests whether a key belongs to the module. *)
val mem : 'a key -> bool
+
+ (** For a key of type [k key]:
+ - if the values of type [t] contain a subpart of type [k] from a module
+ identified by the key, then [get key] returns an accessor for it.
+ - otherwise, [get key] returns None. *)
val get : 'a key -> (t -> 'a) option
+
+ (** For a key of type [k key]:
+ - if the values of type [t] contain a subpart of type [k] from a module
+ identified by the key, then [set key v t] returns the value [t] in which
+ this subpart has been replaced by [v].
+ - otherwise, [set key _] is the identity function. *)
val set : 'a key -> 'a -> t -> t
end
@@ -100,3 +114,4 @@ module Open
(Data : Internal with type 'a structure := 'a Shape.structure)
: External with type t := Data.t
and type 'a key := 'a Shape.key
+ and type 'a data := 'a Shape.data
--
GitLab