From 4940cebb9bf9f26c4c1d0044d0b5c59f039513d6 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 4 Dec 2023 18:49:32 +0100
Subject: [PATCH 01/10] Simplify

---
 .../apron/affineEqualityAnalysis.apron.ml     |  1 -
 src/analyses/apron/apronAnalysis.apron.ml     |  3 +-
 src/analyses/apron/relationAnalysis.apron.ml  |  6 +--
 src/analyses/apron/relationPriv.apron.ml      |  3 +-
 .../apron/affineEqualityDomain.apron.ml       |  5 +--
 src/cdomains/apron/apronDomain.apron.ml       | 11 +++---
 src/cdomains/apron/gobApron.apron.ml          | 37 +++++++++++++++++++
 src/cdomains/apron/gobApron.no-apron.ml       |  0
 src/cdomains/apron/relationDomain.apron.ml    | 28 +++++---------
 src/cdomains/apron/sharedFunctions.apron.ml   | 36 ------------------
 src/dune                                      |  4 ++
 11 files changed, 62 insertions(+), 72 deletions(-)
 create mode 100644 src/cdomains/apron/gobApron.apron.ml
 create mode 100644 src/cdomains/apron/gobApron.no-apron.ml

diff --git a/src/analyses/apron/affineEqualityAnalysis.apron.ml b/src/analyses/apron/affineEqualityAnalysis.apron.ml
index 03a9ecdb57..ce859d87b7 100644
--- a/src/analyses/apron/affineEqualityAnalysis.apron.ml
+++ b/src/analyses/apron/affineEqualityAnalysis.apron.ml
@@ -11,7 +11,6 @@ let spec_module: (module MCPSpec) Lazy.t =
     let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in
     let module RD: RelationDomain.RD =
     struct
-      module Var = AffineEqualityDomain.Var
       module V = AffineEqualityDomain.V
       include AD
     end
diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml
index 29e295a662..72dc81c121 100644
--- a/src/analyses/apron/apronAnalysis.apron.ml
+++ b/src/analyses/apron/apronAnalysis.apron.ml
@@ -12,10 +12,9 @@ let spec_module: (module MCPSpec) Lazy.t =
     let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): ApronDomain.S3) else (module AD)) in
     let module RD: RelationDomain.RD =
     struct
-      module Var = ApronDomain.Var
       module V = ApronDomain.V
       include AD
-      type var = ApronDomain.Var.t
+      type var = GobApron.Var.t
     end
     in
     let module Priv = (val RelationPriv.get_priv ()) in
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index b3c6dcb9b3..b401b58e93 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -285,7 +285,7 @@ struct
     (* there should be smarter ways to do this, e.g. by keeping track of which values are written etc. ... *)
     (* See, e.g, Beckschulze E, Kowalewski S, Brauer J (2012) Access-based localization for octagons. Electron Notes Theor Comput Sci 287:29–40 *)
     (* Also, a local *)
-    let vname = RD.Var.to_string var in
+    let vname = GobApron.Var.to_string var in
     let locals = fundec.sformals @ fundec.slocals in
     match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with (* TODO: optimize *)
     | None -> true
@@ -318,7 +318,7 @@ struct
     RD.remove_filter_with new_rel (fun var ->
         match RV.find_metadata var with
         | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) -> true (* remove caller locals provided they are unreachable *)
-        | Some (Arg _) when not (List.mem_cmp RD.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
+        | Some (Arg _) when not (List.mem_cmp GobApron.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
         | _ -> false (* keep everything else (just added args, globals, global privs) *)
       );
     if M.tracing then M.tracel "combine" "relation enter newd: %a\n" RD.pretty new_rel;
@@ -404,7 +404,7 @@ struct
     in
     let any_local_reachable = any_local_reachable fundec reachable_from_args in
     let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in
-    if M.tracing then M.tracel "combine" "relation remove vars: %a\n" (docList (fun v -> Pretty.text (RD.Var.to_string v))) arg_vars;
+    if M.tracing then M.tracel "combine" "relation remove vars: %a\n" (docList (fun v -> Pretty.text (GobApron.Var.to_string v))) arg_vars;
     RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *)
     let tainted = f_ask.f Queries.MayBeTainted in
     let tainted_vars = TaintPartialContexts.conv_varset tainted in
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index b386af162b..a51fc3545f 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -195,8 +195,7 @@ struct
   end
   module AV =
   struct
-    include RelationDomain.VarMetadataTbl (VM) (RD.Var)
-
+    include RelationDomain.VarMetadataTbl (VM)
 
     let local g = make_var (Local g)
     let unprot g = make_var (Unprot g)
diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index a6f00fdba0..0054f685b1 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -10,7 +10,7 @@ open Batteries
 open GoblintCil
 open Pretty
 module M = Messages
-open Apron
+open GobApron
 open VectorMatrix
 
 module Mpqf = struct
@@ -26,8 +26,7 @@ module Mpqf = struct
   let hash x = 31 * (Z.hash (get_den x)) + Z.hash (get_num x)
 end
 
-module Var = SharedFunctions.Var
-module V = RelationDomain.V(Var)
+module V = RelationDomain.V
 
 (** It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars.
     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. *)
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 7dffafe967..ef9eac9bef 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -4,7 +4,7 @@ open Batteries
 open GoblintCil
 open Pretty
 (* A binding to a selection of Apron-Domains *)
-open Apron
+open GobApron
 open RelationDomain
 open SharedFunctions
 
@@ -29,8 +29,7 @@ let widening_thresholds_apron = ResettableLazy.from_fun (fun () ->
 let reset_lazy () =
   ResettableLazy.reset widening_thresholds_apron
 
-module Var = SharedFunctions.Var
-module V = RelationDomain.V(Var)
+module V = RelationDomain.V
 
 
 module type Manager =
@@ -497,9 +496,9 @@ struct
   let to_yojson (x: t) =
     let constraints =
       A.to_lincons_array Man.mgr x
-      |> SharedFunctions.Lincons1Set.of_earray
-      |> SharedFunctions.Lincons1Set.elements
-      |> List.map (fun lincons1 -> `String (SharedFunctions.Lincons1.show lincons1))
+      |> Lincons1Set.of_earray
+      |> Lincons1Set.elements
+      |> List.map (fun lincons1 -> `String (Lincons1.show lincons1))
     in
     let env = `String (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x))
     in
diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
new file mode 100644
index 0000000000..df20f3c59d
--- /dev/null
+++ b/src/cdomains/apron/gobApron.apron.ml
@@ -0,0 +1,37 @@
+open Batteries
+include Apron
+
+module Var =
+struct
+  include Var
+  let equal x y = Var.compare x y = 0
+end
+
+module Lincons1 =
+struct
+  include Lincons1
+
+  let show = Format.asprintf "%a" print
+  let compare x y = String.compare (show x) (show y) (* HACK *)
+
+  let num_vars x =
+    (* Apron.Linexpr0.get_size returns some internal nonsense, so we count ourselves. *)
+    let size = ref 0 in
+    Lincons1.iter (fun coeff var ->
+        if not (Apron.Coeff.is_zero coeff) then
+          incr size
+      ) x;
+    !size
+end
+
+module Lincons1Set =
+struct
+  include Set.Make (Lincons1)
+
+  let of_earray ({lincons0_array; array_env}: Lincons1.earray): t =
+    Array.enum lincons0_array
+    |> Enum.map (fun (lincons0: Lincons0.t) ->
+        Lincons1.{lincons0; env = array_env}
+      )
+    |> of_enum
+end
diff --git a/src/cdomains/apron/gobApron.no-apron.ml b/src/cdomains/apron/gobApron.no-apron.ml
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml
index e613cad6c3..e68540c41b 100644
--- a/src/cdomains/apron/relationDomain.apron.ml
+++ b/src/cdomains/apron/relationDomain.apron.ml
@@ -5,25 +5,15 @@
 open Batteries
 open GoblintCil
 
-(** Abstracts the extended apron Var. *)
-module type Var =
-sig
-  type t
-  val compare : t -> t -> int
-  val of_string : string -> t
-  val to_string : t -> string
-  val hash : t -> int
-  val equal : t -> t -> bool
-end
-
 module type VarMetadata =
 sig
   type t
   val var_name: t -> string
 end
 
-module VarMetadataTbl (VM: VarMetadata) (Var: Var) =
+module VarMetadataTbl (VM: VarMetadata) =
 struct
+  open GobApron
   module VH = Hashtbl.Make (Var)
 
   let vh = VH.create 113
@@ -57,7 +47,7 @@ end
 
 module type RV =
 sig
-  type t
+  type t = GobApron.Var.t
   type vartable
 
   val vh: vartable
@@ -70,10 +60,11 @@ sig
   val to_cil_varinfo: t -> varinfo Option.t
 end
 
-module V (Var: Var): (RV with type t = Var.t and type vartable = VM.t VarMetadataTbl (VM) (Var).VH.t) =
+module V: (RV with type vartable = VM.t VarMetadataTbl (VM).VH.t) =
 struct
+  open GobApron
   type t = Var.t
-  module VMT = VarMetadataTbl (VM) (Var)
+  module VMT = VarMetadataTbl (VM)
   include VMT
   open VM
 
@@ -105,7 +96,7 @@ end
 module type S2 =
 sig
   type t
-  type var
+  type var = GobApron.Var.t
   type marshal
 
   module Tracked: Tracked
@@ -215,7 +206,6 @@ end
 
 module type RD =
 sig
-  module Var : Var
-  module V : module type of struct include V(Var) end
-  include S3 with type var = Var.t
+  module V : module type of struct include V end
+  include S3
 end
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 059a7f8264..9c229e2d64 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -8,42 +8,6 @@ module M = Messages
 
 module BI = IntOps.BigIntOps
 
-module Var =
-struct
-  include Var
-
-  let equal x y = Var.compare x y = 0
-end
-
-module Lincons1 =
-struct
-  include Lincons1
-
-  let show = Format.asprintf "%a" print
-  let compare x y = String.compare (show x) (show y) (* HACK *)
-
-  let num_vars x =
-    (* Apron.Linexpr0.get_size returns some internal nonsense, so we count ourselves. *)
-    let size = ref 0 in
-    Lincons1.iter (fun coeff var ->
-        if not (Apron.Coeff.is_zero coeff) then
-          incr size
-      ) x;
-    !size
-end
-
-module Lincons1Set =
-struct
-  include Set.Make (Lincons1)
-
-  let of_earray ({lincons0_array; array_env}: Lincons1.earray): t =
-    Array.enum lincons0_array
-    |> Enum.map (fun (lincons0: Lincons0.t) ->
-        Lincons1.{lincons0; env = array_env}
-      )
-    |> of_enum
-end
-
 let int_of_scalar ?round (scalar: Scalar.t) =
   if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *)
     None
diff --git a/src/dune b/src/dune
index acd5348acb..40faae1f3f 100644
--- a/src/dune
+++ b/src/dune
@@ -11,6 +11,10 @@
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies.
+    (select gobApron.ml from
+      (apron -> gobApron.apron.ml)
+      (-> gobApron.no-apron.ml)
+    )
     (select apronDomain.ml from
       (apron apron.octD apron.boxD apron.polkaMPQ zarith_mlgmpidl -> apronDomain.apron.ml)
       (-> apronDomain.no-apron.ml)

From 49eb46df9bf722d0f528f52dbfcb2c8a524ede19 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 4 Dec 2023 19:08:36 +0100
Subject: [PATCH 02/10] Cleanup

---
 src/cdomains/apron/relationDomain.apron.ml | 59 ++++++++++------------
 1 file changed, 26 insertions(+), 33 deletions(-)

diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml
index e68540c41b..aca2346820 100644
--- a/src/cdomains/apron/relationDomain.apron.ml
+++ b/src/cdomains/apron/relationDomain.apron.ml
@@ -1,7 +1,7 @@
 (** Signatures for relational value domains.
 
     See {!ApronDomain} and {!AffineEqualityDomain}. *)
-
+open GobApron
 open Batteries
 open GoblintCil
 
@@ -11,23 +11,6 @@ sig
   val var_name: t -> string
 end
 
-module VarMetadataTbl (VM: VarMetadata) =
-struct
-  open GobApron
-  module VH = Hashtbl.Make (Var)
-
-  let vh = VH.create 113
-
-  let make_var ?name metadata =
-    let name = Option.default_delayed (fun () -> VM.var_name metadata) name in
-    let var = Var.of_string name in
-    VH.replace vh var metadata;
-    var
-
-  let find_metadata (var: Var.t) =
-    VH.find_option vh var
-end
-
 module VM =
 struct
   type t =
@@ -45,10 +28,26 @@ struct
     | Global g -> g.vname
 end
 
+module VarMetadataTbl (VM: VarMetadata) =
+struct
+  module VH = Hashtbl.Make (Var)
+
+  let vh = VH.create 113
+
+  let make_var ?name metadata =
+    let name = Option.default_delayed (fun () -> VM.var_name metadata) name in
+    let var = Var.of_string name in
+    VH.replace vh var metadata;
+    var
+
+  let find_metadata (var: Var.t) =
+    VH.find_option vh var
+end
+
 module type RV =
 sig
-  type t = GobApron.Var.t
-  type vartable
+  type t = Var.t
+  type vartable = VM.t VarMetadataTbl (VM).VH.t
 
   val vh: vartable
   val make_var: ?name:string -> VM.t -> t
@@ -60,13 +59,13 @@ sig
   val to_cil_varinfo: t -> varinfo Option.t
 end
 
-module V: (RV with type vartable = VM.t VarMetadataTbl (VM).VH.t) =
+module V: RV =
 struct
-  open GobApron
+  open VM
+
   type t = Var.t
   module VMT = VarMetadataTbl (VM)
   include VMT
-  open VM
 
   type vartable = VM.t VMT.VH.t
 
@@ -81,12 +80,6 @@ struct
     | _ -> None
 end
 
-module type LinCons =
-sig
-  type t
-  val num_vars: t -> int
-end
-
 module type Tracked =
 sig
   val type_tracked: typ -> bool
@@ -96,7 +89,7 @@ end
 module type S2 =
 sig
   type t
-  type var = GobApron.Var.t
+  type var = Var.t
   type marshal
 
   module Tracked: Tracked
@@ -135,8 +128,8 @@ module type S3 =
 sig
   include S2
 
-  val cil_exp_of_lincons1: Apron.Lincons1.t -> exp option
-  val invariant: t -> Apron.Lincons1.t list
+  val cil_exp_of_lincons1: Lincons1.t -> exp option
+  val invariant: t -> Lincons1.t list
 end
 
 type ('a, 'b) relcomponents_t = {
@@ -206,6 +199,6 @@ end
 
 module type RD =
 sig
-  module V : module type of struct include V end
+  module V : RV
   include S3
 end

From d1b62287dc64b825b3640d5b95ce90394a85d725 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 4 Dec 2023 19:37:06 +0100
Subject: [PATCH 03/10] Move `Environment` things into `GobApron`

---
 .../apron/affineEqualityDomain.apron.ml       | 14 ++---
 src/cdomains/apron/apronDomain.apron.ml       | 25 +++-----
 src/cdomains/apron/gobApron.apron.ml          | 61 +++++++++++++++++++
 src/cdomains/apron/sharedFunctions.apron.ml   | 60 ------------------
 4 files changed, 76 insertions(+), 84 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 0054f685b1..ff2339cd6f 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/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
 
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index ef9eac9bef..077aa971f2 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/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)
diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
index df20f3c59d..c39a3e42db 100644
--- a/src/cdomains/apron/gobApron.apron.ml
+++ b/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
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 9c229e2d64..e66be00ae4 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/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 =

From 4a848e4c809fd9e917ecc5dd5bdfaea234c06ea1 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 4 Dec 2023 19:45:47 +0100
Subject: [PATCH 04/10] Simplify marshal

---
 src/cdomains/apron/apronDomain.apron.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 077aa971f2..ac9d7f0232 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -258,7 +258,7 @@ struct
   let vars x = Environment.ivars_only @@ A.env x
 
   let marshal (x: t): marshal =
-    let vars = Array.map Var.to_string (Array.of_list (Environment.ivars_only (A.env x))) in
+    let vars = Array.map Var.to_string (Array.of_list (vars x)) in
     x.abstract0, vars
 
   let mem_var d v = Environment.mem_var (A.env d) v

From 13ac2001d8eed3060712ac05af74dfd3fc943b1d Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 4 Dec 2023 19:52:21 +0100
Subject: [PATCH 05/10] Some reuse

---
 src/cdomains/apron/apronDomain.apron.ml | 23 +++++++----------------
 1 file changed, 7 insertions(+), 16 deletions(-)

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index ac9d7f0232..03b9558621 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -263,25 +263,16 @@ struct
 
   let mem_var d v = Environment.mem_var (A.env d) v
 
-  let add_vars_with nd vs =
-    let env' = Environment.add_vars (A.env nd) vs in
+  let envop f nd a =
+    let env' = f (A.env nd) a in
     A.change_environment_with Man.mgr nd env' false
 
-  let remove_vars_with nd vs =
-    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' = Environment.remove_filter (A.env nd) f in
-    A.change_environment_with Man.mgr nd env' false
+  let add_vars_with = envop Environment.add_vars
+  let remove_vars_with = envop Environment.remove_vars
+  let remove_filter_with = envop Environment.remove_filter
+  let keep_vars_with = envop Environment.keep_vars
+  let keep_filter_with = envop Environment.keep_filter
 
-  let keep_vars_with nd vs =
-    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' = Environment.keep_filter (A.env nd) f in
-    A.change_environment_with Man.mgr nd env' false
 
   let forget_vars_with nd vs =
     (* Unlike keep_vars_with, this doesn't check mem_var, but assumes valid vars, like assigns *)

From efa239491f9060aa7a89bd9197d82b8e757bd427 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 4 Dec 2023 20:16:51 +0100
Subject: [PATCH 06/10] Add TODO

---
 src/cdomains/apron/affineEqualityDomain.apron.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index ff2339cd6f..5aa1090dd4 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -461,6 +461,7 @@ struct
 
   let assign_exp (t: VarManagement(Vc)(Mx).t) var exp (no_ov: bool Lazy.t) =
     let t = if not @@ Environment.mem_var t.env var then add_vars t [var] else t in
+    (* TODO: Do we need to do a constant folding here? It happens for texpr1_of_cil_exp *)
     match Convert.texpr1_expr_of_cil_exp t t.env exp (Lazy.force no_ov) with
     | exp -> assign_texpr t var exp
     | exception Convert.Unsupported_CilExp _ ->

From 029c1e93daa47624cce2dd94d4ed2c600ed1cc07 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 7 Dec 2023 11:22:05 +0100
Subject: [PATCH 07/10] Add newline back for ocamldoc

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
---
 src/cdomains/apron/relationDomain.apron.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml
index aca2346820..48720b0382 100644
--- a/src/cdomains/apron/relationDomain.apron.ml
+++ b/src/cdomains/apron/relationDomain.apron.ml
@@ -1,6 +1,7 @@
 (** Signatures for relational value domains.
 
     See {!ApronDomain} and {!AffineEqualityDomain}. *)
+
 open GobApron
 open Batteries
 open GoblintCil

From 4fae8c62af777b3199cd63525cb88ae212206d8e Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 7 Dec 2023 11:22:34 +0100
Subject: [PATCH 08/10] Directly use `Apron.Var.t`

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
---
 src/analyses/apron/apronAnalysis.apron.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml
index 72dc81c121..0ba17cdb35 100644
--- a/src/analyses/apron/apronAnalysis.apron.ml
+++ b/src/analyses/apron/apronAnalysis.apron.ml
@@ -14,7 +14,7 @@ let spec_module: (module MCPSpec) Lazy.t =
     struct
       module V = ApronDomain.V
       include AD
-      type var = GobApron.Var.t
+      type var = Apron.Var.t
     end
     in
     let module Priv = (val RelationPriv.get_priv ()) in

From 5f5c1c8cd90b4b3811e37ce46286698dfa103a65 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 7 Dec 2023 11:22:44 +0100
Subject: [PATCH 09/10] Directly use `Apron.Var.t`

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
---
 src/analyses/apron/relationAnalysis.apron.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index b401b58e93..b794c4d70b 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -285,7 +285,7 @@ struct
     (* there should be smarter ways to do this, e.g. by keeping track of which values are written etc. ... *)
     (* See, e.g, Beckschulze E, Kowalewski S, Brauer J (2012) Access-based localization for octagons. Electron Notes Theor Comput Sci 287:29–40 *)
     (* Also, a local *)
-    let vname = GobApron.Var.to_string var in
+    let vname = Apron.Var.to_string var in
     let locals = fundec.sformals @ fundec.slocals in
     match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with (* TODO: optimize *)
     | None -> true

From 129b9c3538c84d72cf70099d367766ececb89cd8 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 7 Dec 2023 17:24:31 +0100
Subject: [PATCH 10/10] Switch `GobApron.Var` to `Apron.Var`

---
 src/analyses/apron/relationAnalysis.apron.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index b794c4d70b..5e128ffc30 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -318,7 +318,7 @@ struct
     RD.remove_filter_with new_rel (fun var ->
         match RV.find_metadata var with
         | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) -> true (* remove caller locals provided they are unreachable *)
-        | Some (Arg _) when not (List.mem_cmp GobApron.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
+        | Some (Arg _) when not (List.mem_cmp Apron.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
         | _ -> false (* keep everything else (just added args, globals, global privs) *)
       );
     if M.tracing then M.tracel "combine" "relation enter newd: %a\n" RD.pretty new_rel;
@@ -404,7 +404,7 @@ struct
     in
     let any_local_reachable = any_local_reachable fundec reachable_from_args in
     let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in
-    if M.tracing then M.tracel "combine" "relation remove vars: %a\n" (docList (fun v -> Pretty.text (GobApron.Var.to_string v))) arg_vars;
+    if M.tracing then M.tracel "combine" "relation remove vars: %a\n" (docList (fun v -> Pretty.text (Apron.Var.to_string v))) arg_vars;
     RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *)
     let tainted = f_ask.f Queries.MayBeTainted in
     let tainted_vars = TaintPartialContexts.conv_varset tainted in