From 4d2e9c766192c73d213376b7f45122723790142c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 23 Aug 2019 16:32:01 +0200
Subject: [PATCH] [Eva] Structure: separates keys and shapes in two distinct
modules.
Keys for abstract values, locations and states are created in structure.ml.
Shapes are created in the respective modules Value, Location and Domain
in abstract.ml.
---
.../domains/numerors/numerors_domain.ok.ml | 2 +-
src/plugins/value/engine/abstractions.ml | 22 +++++-----
src/plugins/value/register.ml | 2 +-
src/plugins/value/utils/abstract.ml | 6 +--
src/plugins/value/utils/abstract.mli | 3 --
src/plugins/value/utils/structure.ml | 43 +++++++++++++------
src/plugins/value/utils/structure.mli | 26 +++++------
7 files changed, 59 insertions(+), 45 deletions(-)
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ok.ml b/src/plugins/value/domains/numerors/numerors_domain.ok.ml
index 8603b8643b0..cce11b08ae5 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 5360df332a1..35da38654f9 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 d3103749d06..a3e08ecd336 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 54cf436f968..ffc27276b1f 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 ad5037857fb..fbbb260c80c 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 67ebc37548b..40537285227 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 d7a82a7ae9b..a60e91e7b60 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
--
GitLab