Move Environment things into GobApron

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -32,7 +32,6 @@ module V = RelationDomain.V
     Furthermore, it provides the function get_coeff_vec that parses an apron expression into a vector of coefficients if the apron expression has an affine form. *)
 module VarManagement (Vec: AbstractVector) (Mx: AbstractMatrix)=
 struct
-  include SharedFunctions.EnvOps
   module Vector = Vec (Mpqf)
   module Matrix = Mx(Mpqf) (Vec)
 
@@ -77,16 +76,18 @@ struct
 
   let change_d t new_env add del = timing_wrap "dimension change" (change_d t new_env add) del
 
+  let vars x = Environment.ivars_only x.env
+
   let add_vars t vars =
     let t = copy t in
-    let env' = add_vars t.env vars in
+    let env' = Environment.add_vars t.env vars in
     change_d t env' true false
 
   let add_vars t vars = timing_wrap "add_vars" (add_vars t) vars
 
   let drop_vars t vars del =
     let t = copy t in
-    let env' = remove_vars t.env vars in
+    let env' = Environment.remove_vars t.env vars in
     change_d t env' false del
 
   let drop_vars t vars = timing_wrap "drop_vars" (drop_vars t) vars
@@ -101,7 +102,7 @@ struct
     t.env <- t'.env
 
   let remove_filter t f =
-    let env' = remove_filter t.env f in
+    let env' = Environment.remove_filter t.env f in
     change_d t env' false false
 
   let remove_filter t f = timing_wrap "remove_filter" (remove_filter t) f
@@ -113,19 +114,18 @@ struct
 
   let keep_filter t f =
     let t = copy t in
-    let env' = keep_filter t.env f in
+    let env' = Environment.keep_filter t.env f in
     change_d t env' false false
 
   let keep_filter t f = timing_wrap "keep_filter" (keep_filter t) f
 
   let keep_vars t vs =
     let t = copy t in
-    let env' = keep_vars t.env vs in
+    let env' = Environment.keep_vars t.env vs in
     change_d t env' false false
 
   let keep_vars t vs = timing_wrap "keep_vars" (keep_vars t) vs
 
-  let vars t = vars t.env
 
   let mem_var t var = Environment.mem_var t.env var
 

src/cdomains/apron/apronDomain.apron.ml

@@ -208,7 +208,6 @@ module type AOpsExtra =
 sig
   type t
   val copy : t -> t
-  val vars_as_array : t -> Var.t array
   val vars : t -> Var.t list
   type marshal
   val unmarshal : marshal -> t
@@ -247,15 +246,6 @@ struct
 
   let copy = A.copy Man.mgr
 
-  let vars_as_array d =
-    let ivs, fvs = Environment.vars (A.env d) in
-    assert (Array.length fvs = 0); (* shouldn't ever contain floats *)
-    ivs
-
-  let vars d =
-    let ivs = vars_as_array d in
-    List.of_enum (Array.enum ivs)
-
   (* marshal type: Abstract0.t and an array of var names *)
   type marshal = Man.mt Abstract0.t * string array
 
@@ -265,30 +255,32 @@ struct
     let env = Environment.make vars [||] in
     {abstract0; env}
 
+  let vars x = Environment.ivars_only @@ A.env x
+
   let marshal (x: t): marshal =
-    let vars = Array.map Var.to_string (vars_as_array x) in
+    let vars = Array.map Var.to_string (Array.of_list (Environment.ivars_only (A.env x))) in
     x.abstract0, vars
 
   let mem_var d v = Environment.mem_var (A.env d) v
 
   let add_vars_with nd vs =
-    let env' = EnvOps.add_vars (A.env nd) vs in
+    let env' = Environment.add_vars (A.env nd) vs in
     A.change_environment_with Man.mgr nd env' false
 
   let remove_vars_with nd vs =
-    let env' = EnvOps.remove_vars (A.env nd) vs in
+    let env' = Environment.remove_vars (A.env nd) vs in
     A.change_environment_with Man.mgr nd env' false
 
   let remove_filter_with nd f =
-    let env' = EnvOps.remove_filter (A.env nd) f in
+    let env' = Environment.remove_filter (A.env nd) f in
     A.change_environment_with Man.mgr nd env' false
 
   let keep_vars_with nd vs =
-    let env' = EnvOps.keep_vars (A.env nd) vs in
+    let env' = Environment.keep_vars (A.env nd) vs in
     A.change_environment_with Man.mgr nd env' false
 
   let keep_filter_with nd f =
-    let env' = EnvOps.keep_filter (A.env nd) f in
+    let env' = Environment.keep_filter (A.env nd) f in
     A.change_environment_with Man.mgr nd env' false
 
   let forget_vars_with nd vs =
@@ -885,7 +877,6 @@ struct
   let unmarshal (b, d) = (BoxD.unmarshal b, D.unmarshal d)
 
   let mem_var (_, d) v = D.mem_var d v
-  let vars_as_array (_, d) = D.vars_as_array d
   let vars (_, d) = D.vars d
 
   let pretty_diff () ((_, d1), (_, d2)) = D.pretty_diff () (d1, d2)

src/cdomains/apron/gobApron.apron.ml

@@ -35,3 +35,64 @@ struct
       )
     |> of_enum
 end
+
+(** A few code elements for environment changes from functions as remove_vars etc. have been moved to sharedFunctions as they are needed in a similar way inside affineEqualityDomain.
+    A module that includes various methods used by variable handling operations such as add_vars, remove_vars etc. in apronDomain and affineEqualityDomain. *)
+module Environment =
+struct
+  include Environment
+
+  let ivars_only env =
+    let ivs, fvs = Environment.vars env in
+    assert (Array.length fvs = 0); (* shouldn't ever contain floats *)
+    List.of_enum (Array.enum ivs)
+
+  let add_vars env vs =
+    let vs' =
+      vs
+      |> List.enum
+      |> Enum.filter (fun v -> not (Environment.mem_var env v))
+      |> Array.of_enum
+    in
+    Environment.add env vs' [||]
+
+  let remove_vars env vs =
+    let vs' =
+      vs
+      |> List.enum
+      |> Enum.filter (fun v -> Environment.mem_var env v)
+      |> Array.of_enum
+    in
+    Environment.remove env vs'
+
+  let remove_filter env f =
+    let vs' =
+      ivars_only env
+      |> List.enum
+      |> Enum.filter f
+      |> Array.of_enum
+    in
+    Environment.remove env vs'
+
+  let keep_vars env vs =
+    (* Instead of iterating over all vars in env and doing a linear lookup in vs just to remove them,
+        make a new env with just the desired vs. *)
+    let vs' =
+      vs
+      |> List.enum
+      |> Enum.filter (fun v -> Environment.mem_var env v)
+      |> Array.of_enum
+    in
+    Environment.make vs' [||]
+
+  let keep_filter env f =
+    (* Instead of removing undesired vars,
+       make a new env with just the desired vars. *)
+    let vs' =
+      ivars_only env
+      |> List.enum
+      |> Enum.filter f
+      |> Array.of_enum
+    in
+    Environment.make vs' [||]
+end

src/cdomains/apron/sharedFunctions.apron.ml

@@ -255,66 +255,6 @@ struct
   include CilOfApron (V)
 end
 
-(** A few code elements for environment changes from functions as remove_vars etc. have been moved to sharedFunctions as they are needed in a similar way inside affineEqualityDomain.
-    A module that includes various methods used by variable handling operations such as add_vars, remove_vars etc. in apronDomain and affineEqualityDomain. *)
-module EnvOps =
-struct
-  let vars env =
-    let ivs, fvs = Environment.vars env in
-    assert (Array.length fvs = 0); (* shouldn't ever contain floats *)
-    List.of_enum (Array.enum ivs)
-
-  let add_vars env vs =
-    let vs' =
-      vs
-      |> List.enum
-      |> Enum.filter (fun v -> not (Environment.mem_var env v))
-      |> Array.of_enum
-    in
-    Environment.add env vs' [||]
-
-  let remove_vars env vs =
-    let vs' =
-      vs
-      |> List.enum
-      |> Enum.filter (fun v -> Environment.mem_var env v)
-      |> Array.of_enum
-    in
-    Environment.remove env vs'
-
-  let remove_filter env f =
-    let vs' =
-      vars env
-      |> List.enum
-      |> Enum.filter f
-      |> Array.of_enum
-    in
-    Environment.remove env vs'
-
-  let keep_vars env vs =
-    (* Instead of iterating over all vars in env and doing a linear lookup in vs just to remove them,
-        make a new env with just the desired vs. *)
-    let vs' =
-      vs
-      |> List.enum
-      |> Enum.filter (fun v -> Environment.mem_var env v)
-      |> Array.of_enum
-    in
-    Environment.make vs' [||]
-
-  let keep_filter env f =
-    (* Instead of removing undesired vars,
-       make a new env with just the desired vars. *)
-    let vs' =
-      vars env
-      |> List.enum
-      |> Enum.filter f
-      |> Array.of_enum
-    in
-    Environment.make vs' [||]
-
-end
-
 (** A more specific module type for RelationDomain.RelD2 with ConvBounds integrated and various apron elements.
     It is designed to be the interface for the D2 modules in affineEqualityDomain and apronDomain and serves as a functor argument for AssertionModule. *)
 module type AssertionRelS =