diff --git a/src/plugins/value/domains/numerors/numerors_domain.ok.ml b/src/plugins/value/domains/numerors/numerors_domain.ok.ml
index 8603b8643b06d45928d41616d7db798b65d68bef..cce11b08ae5810c955c98e83087f1b03ae853cdc 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ok.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ok.ml
@@ -88,7 +88,7 @@ module Numerors_Value = struct
end
let add_numerors_value (module Value: Abstract.Value.Internal) =
- let module External_Value = Structure.Open (Structure.Key_Value) (Value) in
+ let module External_Value = Structure.Open (Abstract.Value) (Value) in
let module V = struct
include Value_product.Make (Value) (Numerors_value)
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 5360df332a1ad973cdeed1d0a09c8a6c7372fc9e..35da38654f944f7a92ca0d5e8d282a0625cb2d57 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -114,7 +114,7 @@ end
module CVal = struct
include Internal_CVal
- include Structure.Open (Structure.Key_Value) (Internal_CVal)
+ include Structure.Open (Abstract.Value) (Internal_CVal)
end
module Internal_PLoc = struct
@@ -153,7 +153,7 @@ let open_value_abstraction value =
let module Value = (val value : Abstract.Value.Internal) in
(module struct
include Value
- include Structure.Open (Structure.Key_Value) (Value)
+ include Structure.Open (Abstract.Value) (Value)
end : V)
let build_value config =
@@ -321,7 +321,7 @@ let add_generic_equalities (module Acc : Abstract) =
let add_equalities (type v) (module Acc : Abstract with type Val.t = v) =
match Acc.Val.structure with
- | Structure.Key_Value.Leaf key ->
+ | Abstract.Value.Leaf key ->
begin
match Structure.Key_Value.eq_type key Main_values.CVal.key with
| None -> add_generic_equalities (module Acc)
@@ -493,7 +493,7 @@ let build_abstractions config =
let module V = (val value : V) in
let abstractions =
match V.structure with
- | Structure.Key_Value.Leaf key
+ | Abstract.Value.Leaf key
when Structure.Key_Value.equal key Main_values.CVal.key ->
default_root_abstraction config
| _ -> build_root_abstraction config value
@@ -617,17 +617,17 @@ module Reduce (Value : Abstract.Value.External) = struct
end
let open_abstractions abstraction =
- let module Abstract = (val abstraction : Abstract) in
- let module Val = Reduce (Abstract.Val) in
+ let module Acc = (val abstraction : Abstract) in
+ let module Val = Reduce (Acc.Val) in
let module Loc = struct
- include Abstract.Loc
+ include Acc.Loc
include Structure.Open
- (Structure.Key_Location)
- (struct include Abstract.Loc type t = location end)
+ (Abstract.Location)
+ (struct include Acc.Loc type t = location end)
end in
let module Domain = struct
- include Abstract.Dom
- include Structure.Open (Structure.Key_Domain) (Abstract.Dom)
+ include Acc.Dom
+ include Structure.Open (Abstract.Domain) (Acc.Dom)
end in
(module struct
module Val = Val
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index d3103749d06ab0fc0e6819ac4ff21ffb6392ead5..a3e08ecd336bedd719960143a3934e04fc8d75d8 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -176,7 +176,7 @@ end
module Val = struct
include CVal
- include Structure.Open (Structure.Key_Value) (CVal)
+ include Structure.Open (Abstract.Value) (CVal)
let reduce t = t
end
diff --git a/src/plugins/value/utils/abstract.ml b/src/plugins/value/utils/abstract.ml
index 54cf436f968546860044cf4e9c28629428996dff..ffc27276b1feea118ffd6463d352f7f202021386 100644
--- a/src/plugins/value/utils/abstract.ml
+++ b/src/plugins/value/utils/abstract.ml
@@ -30,7 +30,7 @@ module type Interface = sig
end
module Value = struct
- include Structure.Key_Value
+ include Structure.Shape (Structure.Key_Value)
module type Internal = sig
include Abstract_value.S
@@ -45,7 +45,7 @@ module Value = struct
end
module Location = struct
- include Structure.Key_Location
+ include Structure.Shape (Structure.Key_Location)
module type Internal = sig
include Abstract_location.S
@@ -60,7 +60,7 @@ module Location = struct
end
module Domain = struct
- include Structure.Key_Domain
+ include Structure.Shape (Structure.Key_Domain)
module type Internal = sig
include Abstract_domain.Internal
diff --git a/src/plugins/value/utils/abstract.mli b/src/plugins/value/utils/abstract.mli
index ad5037857fb279840fcab7c6a6b9d6d5e8a97f9b..fbbb260c80c421be94aa7ad742a8e5e6cbb099f6 100644
--- a/src/plugins/value/utils/abstract.mli
+++ b/src/plugins/value/utils/abstract.mli
@@ -60,7 +60,6 @@ end
module Value : sig
include Structure.Shape
with type 'a key = 'a Structure.Key_Value.key
- and type 'a structure = 'a Structure.Key_Value.structure
module type Internal = sig
include Abstract_value.S
@@ -79,7 +78,6 @@ end
module Location : sig
include Structure.Shape
with type 'a key = 'a Structure.Key_Location.key
- and type 'a structure = 'a Structure.Key_Location.structure
module type Internal = sig
include Abstract_location.S
@@ -98,7 +96,6 @@ end
module Domain : sig
include Structure.Shape
with type 'a key = 'a Structure.Key_Domain.key
- and type 'a structure = 'a Structure.Key_Domain.structure
module type Internal = sig
include Abstract_domain.Internal
diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml
index 67ebc37548be15ce5617930b6a4da6b9b0c3994f..4053728522755508cc7a4b38dda3ff696840fa37 100644
--- a/src/plugins/value/utils/structure.ml
+++ b/src/plugins/value/utils/structure.ml
@@ -36,16 +36,6 @@ module type Key = sig
val tag: 'a key -> int
end
-module type Shape = sig
- include Key
-
- type 'a structure =
- | Void : 'a structure
- | Leaf : 'a key -> 'a structure
- | Node : 'a structure * 'b structure -> ('a * 'b) structure
-end
-
-
module Make (X : sig end) = struct
type 'a key = { tag: int;
@@ -67,17 +57,43 @@ module Make (X : sig end) = struct
let tag x = x.tag
let print fmt x = Format.pp_print_string fmt x.name
+end
+
+module Key_Value = Make (struct end)
+module Key_Location = Make (struct end)
+module Key_Domain = Make (struct end)
+
+module type Shape = sig
+ include Key
type 'a structure =
| Void : 'a structure
| Leaf : 'a key -> 'a structure
| Node : 'a structure * 'b structure -> ('a * 'b) structure
+
+ val eq_structure: 'a structure -> 'b structure -> ('a, 'b) eq option
end
-module Key_Value = Make (struct end)
-module Key_Location = Make (struct end)
-module Key_Domain = Make (struct end)
+module Shape (Key: Key) = struct
+ include Key
+ type 'a structure =
+ | Void : 'a structure
+ | Leaf : 'a Key.key -> 'a structure
+ | Node : 'a structure * 'b structure -> ('a * 'b) structure
+
+ let rec eq_structure : type a b. a structure -> b structure -> (a, b) eq option
+ = fun a b ->
+ match a, b with
+ | Leaf key1, Leaf key2 -> Key.eq_type key1 key2
+ | Node (l1, r1), Node (l2, r2) ->
+ begin
+ match eq_structure l1 l2, eq_structure r1 r2 with
+ | Some Eq, Some Eq -> Some Eq
+ | _, _ -> None
+ end
+ | _, _ -> None
+end
module type Internal = sig
type t
@@ -93,7 +109,6 @@ module type External = sig
val set : 'a key -> 'a -> t -> t
end
-
module Open
(Shape : Shape)
(M : sig type t val structure : t Shape.structure end)
diff --git a/src/plugins/value/utils/structure.mli b/src/plugins/value/utils/structure.mli
index d7a82a7ae9b075dcebab7b7147be64028b2577d8..a60e91e7b609c774de39c2fbc480615c56ec8d03 100644
--- a/src/plugins/value/utils/structure.mli
+++ b/src/plugins/value/utils/structure.mli
@@ -41,6 +41,17 @@ module type Key = sig
val tag: 'a key -> int
end
+module Make (X : sig end) : Key
+
+(** Keys module for the abstract values of Eva. *)
+module Key_Value : Key
+
+(** Keys module for the abstract locations of Eva. *)
+module Key_Location : Key
+
+(** Keys module for the abstract domains of Eva. *)
+module Key_Domain : Key
+
(** A Key module with its structure type. *)
module type Shape = sig
include Key
@@ -52,20 +63,11 @@ module type Shape = sig
| Void : 'a structure
| Leaf : 'a key -> 'a structure
| Node : 'a structure * 'b structure -> ('a * 'b) structure
-end
-module Make (X : sig end) : Shape
-
-
-(** Keys module for the abstract values of Eva. *)
-module Key_Value : Shape
-
-(** Keys module for the abstract locations of Eva. *)
-module Key_Location : Shape
-
-(** Keys module for the abstract domains of Eva. *)
-module Key_Domain : Shape
+ val eq_structure: 'a structure -> 'b structure -> ('a, 'b) eq option
+end
+module Shape (Key : Key) : Shape with type 'a key = 'a Key.key
(** Internal view of the tree, with the structure. *)
module type Internal = sig