From 031b40c6794f69d13dd36b0872a79d4f4f5c27a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 26 Aug 2019 15:29:51 +0200
Subject: [PATCH] [Eva] Minor changes in the building of abstractions.
Domain_product works on Internal modules.
Location_lift and Domain_lift promote leaf modules into internal modules,
by creating the suitable structure.
---
src/plugins/value/domains/domain_lift.ml | 4 +-
src/plugins/value/domains/domain_lift.mli | 4 +-
src/plugins/value/domains/domain_product.ml | 6 +-
src/plugins/value/domains/domain_product.mli | 6 +-
src/plugins/value/engine/abstractions.ml | 60 ++++++--------------
src/plugins/value/values/location_lift.ml | 4 +-
src/plugins/value/values/location_lift.mli | 8 +--
7 files changed, 37 insertions(+), 55 deletions(-)
diff --git a/src/plugins/value/domains/domain_lift.ml b/src/plugins/value/domains/domain_lift.ml
index d53990a56cc..0256e97c80d 100644
--- a/src/plugins/value/domains/domain_lift.ml
+++ b/src/plugins/value/domains/domain_lift.ml
@@ -37,7 +37,7 @@ end
module Make
- (Domain: Abstract_domain.Internal)
+ (Domain: Abstract_domain.Leaf)
(Convert : Conversion with type internal_value := Domain.value
and type internal_location := Domain.location)
= struct
@@ -45,6 +45,8 @@ module Make
include (Domain : Datatype.S_with_collections with type t = Domain.t)
include (Domain : Abstract_domain.Lattice with type state = Domain.state)
+ let structure = Abstract.Domain.Leaf (Domain.key, (module Domain))
+
let log_category = Domain.log_category
type value = Convert.extended_value
diff --git a/src/plugins/value/domains/domain_lift.mli b/src/plugins/value/domains/domain_lift.mli
index 9e16a8a292e..9ed35656590 100644
--- a/src/plugins/value/domains/domain_lift.mli
+++ b/src/plugins/value/domains/domain_lift.mli
@@ -36,10 +36,10 @@ end
module Make
- (Domain: Abstract_domain.Internal)
+ (Domain: Abstract_domain.Leaf)
(Convert : Conversion with type internal_value := Domain.value
and type internal_location := Domain.location)
- : Abstract_domain.Internal with type state = Domain.state
+ : Abstract.Domain.Internal with type state = Domain.state
and type value = Convert.extended_value
and type location = Convert.extended_location
and type origin = Domain.origin
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index d35d7c7c791..1985b6c173a 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -28,8 +28,8 @@ let product_category = Value_parameters.register_category "domain_product"
module Make
(Value: Abstract_value.S)
- (Left: Abstract_domain.Internal with type value = Value.t)
- (Right: Abstract_domain.Internal with type value = Left.value
+ (Left: Abstract.Domain.Internal with type value = Value.t)
+ (Right: Abstract.Domain.Internal with type value = Left.value
and type location = Left.location)
= struct
@@ -51,6 +51,8 @@ module Make
(struct let module_name = name end)
type state = t
+ let structure = Abstract.Domain.Node (Left.structure, Right.structure)
+
let log_category = product_category
let top = Left.top, Right.top
diff --git a/src/plugins/value/domains/domain_product.mli b/src/plugins/value/domains/domain_product.mli
index c883a94ba8d..859988e2552 100644
--- a/src/plugins/value/domains/domain_product.mli
+++ b/src/plugins/value/domains/domain_product.mli
@@ -24,10 +24,10 @@ val product_category: Value_parameters.category
module Make
(Value: Abstract_value.S)
- (Left: Abstract_domain.Internal with type value = Value.t)
- (Right: Abstract_domain.Internal with type value = Left.value
+ (Left: Abstract.Domain.Internal with type value = Value.t)
+ (Right: Abstract.Domain.Internal with type value = Left.value
and type location = Left.location)
- : Abstract_domain.Internal with type value = Value.t
+ : Abstract.Domain.Internal with type value = Value.t
and type location = Left.location
and type state = Left.state * Right.state
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 3a52d334d1f..07b3f673d88 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -209,30 +209,16 @@ module Internal_Value = struct
| Unit -> fun _ -> ()
in
get structure
- end
-end
-
-(* --- Building domain abstractions ----------------------------------------- *)
-
-module Lift_Domain
- (Value: Abstract.Value.External)
- (Domain: Abstract_domain.Leaf with type location = precise_loc)
- (Struct: sig type v = Domain.value val s : v value end)
-= struct
-
- module Convert = struct
- include Internal_Value.Convert (Value) (Struct)
type extended_location = Main_locations.PLoc.location
let restrict_loc = fun x -> x
let extend_loc = fun x -> x
end
-
- include Domain_lift.Make (Domain) (Convert)
- let key = Domain.key
end
+(* --- Building domain abstractions ----------------------------------------- *)
+
module type internal_domain =
Abstract.Domain.Internal with type location = Precise_locs.precise_location
@@ -245,34 +231,30 @@ let eq_value:
| Abstract.Value.Leaf (key, _) -> Abstract.Value.eq_type key V.key
| _ -> None
-let add_domain (type v) (abstraction: v abstraction) acc =
- let module Acc = (val acc: Acc) in
- let new_domain : (module leaf_domain with type value = Acc.Val.t) =
+let add_domain (type v) (abstraction: v abstraction) (module Acc: Acc) =
+ let domain : (module internal_domain with type value = Acc.Val.t) =
match abstraction.domain with
| Functor make ->
let module Make = (val make: domain_functor) in
- (module Make (Acc.Val))
+ (module Leaf_Domain (Make (Acc.Val)))
| Domain domain ->
match eq_value Acc.Val.structure abstraction.values with
- | Some Structure.Eq -> domain
+ | Some Structure.Eq ->
+ let module Domain = (val domain) in
+ (module Leaf_Domain (Domain))
| None ->
- let module Dom = (val domain : leaf_domain with type value = v) in
+ let module Domain = (val domain : leaf_domain with type value = v) in
let module Struct = struct
- type v = Dom.value
+ type v = Domain.value
let s = abstraction.values
end in
- (module Lift_Domain (Acc.Val) (Dom) (Struct))
+ let module Convert = Internal_Value.Convert (Acc.Val) (Struct) in
+ (module Domain_lift.Make (Domain) (Convert))
in
- let module Domain = (val new_domain) in
- let module Domain = Leaf_Domain (Domain) in
let domain : (module internal_domain with type value = Acc.Val.t) =
- match Acc.Dom.structure with
- | Abstract.Domain.Unit -> (module Domain)
- | s ->
- (module struct
- include Domain_product.Make (Acc.Val) (Acc.Dom) (Domain)
- let structure = Abstract.Domain.Node (s, Domain.structure)
- end)
+ match Abstract.Domain.(eq_structure Acc.Dom.structure Unit) with
+ | Some _ -> domain
+ | None -> (module Domain_product.Make (Acc.Val) (Acc.Dom) ((val domain)))
in
(module struct
module Val = Acc.Val
@@ -325,9 +307,7 @@ let register_value_reduction reduced_product =
let reduce_apron_itv cvalue ival =
match ival with
| None -> begin
- try
- let ival = Cvalue.V.project_ival cvalue in
- cvalue, (Some ival)
+ try cvalue, Some (Cvalue.V.project_ival cvalue)
with Cvalue.V.Not_based_on_null -> cvalue, ival
end
| Some ival ->
@@ -338,7 +318,7 @@ let reduce_apron_itv cvalue ival =
| _ -> ());
let reduced_ival = Ival.narrow ival ival' in
let cvalue = Cvalue.V.inject_ival reduced_ival in
- cvalue, (Some reduced_ival)
+ cvalue, Some reduced_ival
with Cvalue.V.Not_based_on_null -> cvalue, Some ival
let () =
@@ -400,17 +380,13 @@ module Open (Acc: Acc) : S = struct
end
module Unit_Acc (Value: Abstract.Value.External) : Acc = struct
- module PLoc = Main_locations.PLoc
module Struct = struct
type v = Cvalue.V.t
let s = Single (module Main_values.CVal)
end
module Conv = Internal_Value.Convert (Value) (Struct)
module Val = Value
- module Loc = struct
- include Location_lift.Make (PLoc) (Conv)
- let structure = Abstract.Location.Leaf (PLoc.key, (module PLoc))
- end
+ module Loc = Location_lift.Make (Main_locations.PLoc) (Conv)
module Dom = Unit_domain.Make (Value) (Loc)
end
diff --git a/src/plugins/value/values/location_lift.ml b/src/plugins/value/values/location_lift.ml
index 4ae36f3622c..f02568133bb 100644
--- a/src/plugins/value/values/location_lift.ml
+++ b/src/plugins/value/values/location_lift.ml
@@ -32,7 +32,7 @@ module type Conversion = sig
end
module Make
- (Loc: Abstract_location.S)
+ (Loc: Abstract_location.Leaf)
(Convert : Conversion with type internal_value := Loc.value)
= struct
@@ -43,6 +43,8 @@ module Make
and type offset = Loc.offset)
type value = Convert.extended_value
+ let structure = Abstract.Location.Leaf (Loc.key, (module Loc))
+
(* Now lift the functions that contain {!value} in their type. *)
let to_value loc = Convert.extend_val (Loc.to_value loc)
diff --git a/src/plugins/value/values/location_lift.mli b/src/plugins/value/values/location_lift.mli
index 602fbcee455..cd5b46cafaf 100644
--- a/src/plugins/value/values/location_lift.mli
+++ b/src/plugins/value/values/location_lift.mli
@@ -30,11 +30,11 @@ module type Conversion = sig
end
module Make
- (Loc: Abstract_location.S)
+ (Loc: Abstract_location.Leaf)
(Convert : Conversion with type internal_value := Loc.value)
- : Abstract_location.S with type location = Loc.location
- and type offset = Loc.offset
- and type value = Convert.extended_value
+ : Abstract.Location.Internal with type location = Loc.location
+ and type offset = Loc.offset
+ and type value = Convert.extended_value
(*
--
GitLab