[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

@@ -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

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

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

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
 

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
 

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)

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
 
 
 (*