From d754d76fd0912b78e495cab0eb2fa73405c00952 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 13 Apr 2022 14:19:21 +0000
Subject: [PATCH 01/43] Add direct Klever concurrency specials

---
 src/analyses/libraryFunctions.ml    | 5 ++++-
 src/analyses/mutexEventsAnalysis.ml | 6 ++++--
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 0c00391dcb..ce89391691 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -24,7 +24,8 @@ let classify' fn exps =
     `Unknown fn
   in
   match fn with
-  | "pthread_create" ->
+  | "pthread_create"
+  | "pthread_create_N" -> (* Klever *)
     begin match exps with
       | [id;_;fn;x] -> `ThreadCreate (id, fn, x)
       | _ -> strange_arguments ()
@@ -72,6 +73,7 @@ let classify' fn exps =
   | "pthread_rwlock_wrlock" | "GetResource" | "_raw_spin_lock"
   | "_raw_spin_lock_flags" | "_raw_spin_lock_irqsave" | "_raw_spin_lock_irq" | "_raw_spin_lock_bh"
   | "spin_lock_irqsave" | "spin_lock"
+  | "ldv_mutex_model_lock" | "ldv_spin_model_lock" (* Klever *)
     -> `Lock (get_bool "sem.lock.fail", true, true)
   | "pthread_mutex_lock" | "__pthread_mutex_lock"
     -> `Lock (get_bool "sem.lock.fail", true, false)
@@ -84,6 +86,7 @@ let classify' fn exps =
   | "mutex_unlock" | "ReleaseResource" | "_write_unlock" | "_read_unlock" | "_raw_spin_unlock_irqrestore"
   | "pthread_mutex_unlock" | "__pthread_mutex_unlock" | "spin_unlock_irqrestore" | "up_read" | "up_write"
   | "up"
+  | "ldv_mutex_model_unlock" | "ldv_spin_model_unlock" (* Klever *)
     -> `Unlock
   | x -> `Unknown x
 
diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml
index 4a3ef078ce..050b8de600 100644
--- a/src/analyses/mutexEventsAnalysis.ml
+++ b/src/analyses/mutexEventsAnalysis.ml
@@ -77,7 +77,8 @@ struct
     let unlock remove_fn =
       match f.vname, arglist with
       | _, [arg]
-      | ("spin_unlock_irqrestore" | "_raw_spin_unlock_irqrestore"), [arg; _] ->
+      | ("spin_unlock_irqrestore" | "_raw_spin_unlock_irqrestore"), [arg; _]
+      | "ldv_mutex_model_unlock", [arg; _] -> (* Klever *)
         List.iter (fun e ->
             ctx.split () [Events.Unlock (remove_fn e)]
           ) (eval_exp_addr (Analyses.ask_of_ctx ctx) arg);
@@ -92,7 +93,8 @@ struct
     | `Lock (failing, rw, nonzero_return_when_aquired), _ ->
       begin match f.vname, arglist with
         | _, [arg]
-        | "spin_lock_irqsave", [arg; _] ->
+        | "spin_lock_irqsave", [arg; _]
+        | "ldv_mutex_model_lock", [arg; _] -> (* Klever *)
           (*print_endline @@ "Mutex `Lock "^f.vname;*)
           lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv arg
         | _ -> failwith "lock has multiple arguments"

From 8f3160943db3dc36a622b0914242a3fa496a2978 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 13 Apr 2022 14:20:08 +0000
Subject: [PATCH 02/43] Add special rtnl_lock from Linux

---
 src/analyses/mutexEventsAnalysis.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml
index 050b8de600..a7448af4f4 100644
--- a/src/analyses/mutexEventsAnalysis.ml
+++ b/src/analyses/mutexEventsAnalysis.ml
@@ -11,6 +11,7 @@ open GobConfig
 
 let big_kernel_lock = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[big kernel lock]" intType))
 let console_sem = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[console semaphore]" intType))
+let rtnl_lock = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[rtnl_lock]" intType))
 let verifier_atomic = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[__VERIFIER_atomic]" intType))
 
 module Spec: MCPSpec =
@@ -118,10 +119,14 @@ struct
       (*print_endline @@ "Mutex `Unlock "^f.vname;*)
       unlock remove_rw
     | _, "spinlock_check" -> ()
-    | _, "acquire_console_sem" when get_bool "kernel" ->
+    | _, "acquire_console_sem"-> (* TODO: removed for Klever: when get_bool "kernel" *)
       ctx.emit (Events.Lock (console_sem, true))
-    | _, "release_console_sem" when get_bool "kernel" ->
+    | _, "release_console_sem" -> (* TODO: removed for Klever: when get_bool "kernel" *)
       ctx.emit (Events.Unlock console_sem)
+    | _, "rtnl_lock"->
+      ctx.emit (Events.Lock (rtnl_lock, true))
+    | _, ("rtnl_unlock" | "__rtnl_unlock") ->
+      ctx.emit (Events.Unlock rtnl_lock)
     | _, "__builtin_prefetch" | _, "misc_deregister" ->
       ()
     | _, "__VERIFIER_atomic_begin" when get_bool "ana.sv-comp.functions" ->

From 1fbf9105c125d1bf4903d43ea477cd88cbb0df6b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 13 Apr 2022 14:20:19 +0000
Subject: [PATCH 03/43] Add symb_locks to ldv-races conf

---
 conf/ldv-races.json | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/conf/ldv-races.json b/conf/ldv-races.json
index 2414413de4..2b30576e1b 100644
--- a/conf/ldv-races.json
+++ b/conf/ldv-races.json
@@ -27,7 +27,9 @@
       "access",
       "escape",
       "expRelation",
-      "mhp"
+      "mhp",
+      "var_eq",
+      "symb_locks"
     ],
     "malloc": {
       "wrappers": [

From 717b6a85cb99521936a1d7e3b5c952dcfafb43af Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 27 Nov 2023 12:18:53 +0200
Subject: [PATCH 04/43] Add pthread_join_N to Klever library

---
 src/analyses/libraryFunctions.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index c9afb83617..b94f751568 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -1008,6 +1008,7 @@ let rtnl_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[rtnl_lock
 (** LDV Klever functions. *)
 let klever_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_create_N", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }); (* TODO: add multiple flag to ThreadCreate *)
+    ("pthread_join_N", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval});
     ("ldv_mutex_model_lock", special [__ "lock" []; drop "sign" []] @@ fun lock -> Lock { lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true });
     ("ldv_mutex_model_unlock", special [__ "lock" []; drop "sign" []] @@ fun lock -> Unlock lock);
     ("ldv_spin_model_lock", unknown [drop "sign" []]);

From 670e7cfe1665a527ce1c124bad8494e30d452bd4 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 27 Nov 2023 12:23:06 +0200
Subject: [PATCH 05/43] Add test for Klever's multiple threads

---
 .../51-threadjoins/07-klever-multiple.c       | 24 +++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 tests/regression/51-threadjoins/07-klever-multiple.c

diff --git a/tests/regression/51-threadjoins/07-klever-multiple.c b/tests/regression/51-threadjoins/07-klever-multiple.c
new file mode 100644
index 0000000000..24b2c0b1ca
--- /dev/null
+++ b/tests/regression/51-threadjoins/07-klever-multiple.c
@@ -0,0 +1,24 @@
+//PARAM: --set ana.activated[+] threadJoins --set lib.activated[+] klever
+#include <pthread.h>
+#include <goblint.h>
+
+int g = 0;
+
+void *t_fun(void *arg) {
+  g++; // RACE!
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create_N(&id, NULL, t_fun, NULL); // spawns multiple threads
+  pthread_join(id, NULL);
+
+  g++; // RACE!
+
+  pthread_join_N(id, NULL); // TODO: should this join one (do nothing) or all (like assume join)?
+
+  g++; // RACE!
+
+  return 0;
+}

From 8a95c8a2d4fa776624da179a803c021058563577 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 27 Nov 2023 12:29:07 +0200
Subject: [PATCH 06/43] Add multiple flag to ThreadCreate

---
 src/analyses/base.ml             | 22 +++++++++++-----------
 src/analyses/libraryDesc.ml      |  2 +-
 src/analyses/libraryFunctions.ml |  4 ++--
 3 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index bdae887b4a..3630395282 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1953,8 +1953,8 @@ struct
 
 
 
-  let forkfun (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list) list * bool =
-    let create_thread lval arg v =
+  let forkfun (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list * bool) list =
+    let create_thread ~multiple lval arg v =
       try
         (* try to get function declaration *)
         let fd = Cilfacade.find_varinfo_fundec v in
@@ -1963,7 +1963,7 @@ struct
           | Some x -> [x]
           | None -> List.map (fun x -> MyCFG.unknown_exp) fd.sformals
         in
-        Some (lval, v, args)
+        Some (lval, v, args, multiple)
       with Not_found ->
         if LF.use_special f.vname then None (* we handle this function *)
         else if isFunctionType v.vtype then
@@ -1973,7 +1973,7 @@ struct
             | Some x -> [x]
             | None -> List.map (fun x -> MyCFG.unknown_exp) (Cil.argsToList v_args)
           in
-          Some (lval, v, args)
+          Some (lval, v, args, multiple)
         else (
           M.debug ~category:Analyzer "Not creating a thread from %s because its type is %a" v.vname d_type v.vtype;
           None
@@ -1982,7 +1982,7 @@ struct
     let desc = LF.find f in
     match desc.special args, f.vname with
     (* handling thread creations *)
-    | ThreadCreate { thread = id; start_routine = start; arg = ptc_arg }, _ -> begin
+    | ThreadCreate { thread = id; start_routine = start; arg = ptc_arg; multiple }, _ -> begin
         (* extra sync so that we do not analyze new threads with bottom global invariant *)
         publish_all ctx `Thread;
         (* Collect the threads. *)
@@ -1994,7 +1994,7 @@ struct
           else
             start_funvars
         in
-        List.filter_map (create_thread (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown, false
+        List.filter_map (create_thread ~multiple (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown
       end
     | _, _ when get_bool "sem.unknown_function.spawn" ->
       (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
@@ -2008,8 +2008,8 @@ struct
       let flist = shallow_flist @ deep_flist in
       let addrs = List.concat_map AD.to_var_may flist in
       if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
-      List.filter_map (create_thread None None) addrs, true
-    | _, _ -> [], false
+      List.filter_map (create_thread ~multiple:true None None) addrs
+    | _, _ -> []
 
   let assert_fn ctx e refine =
     (* make the state meet the assertion in the rest of the code *)
@@ -2140,9 +2140,9 @@ struct
       let addr = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in
       (addr, AD.type_of addr)
     in
-    let forks, multiple = forkfun ctx lv f args in
-    if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple3.second forks);
-    List.iter (BatTuple.Tuple3.uncurry (ctx.spawn ~multiple)) forks;
+    let forks = forkfun ctx lv f args in
+    if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple4.second forks);
+    List.iter (fun (lval, f, args, multiple) -> ctx.spawn ~multiple lval f args) forks;
     let st: store = ctx.local in
     let gs = ctx.global in
     let desc = LF.find f in
diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
index 4997b306a9..e426c32235 100644
--- a/src/analyses/libraryDesc.ml
+++ b/src/analyses/libraryDesc.ml
@@ -53,7 +53,7 @@ type special =
   | Assert of { exp: Cil.exp; check: bool; refine: bool; }
   | Lock of { lock: Cil.exp; try_: bool; write: bool; return_on_success: bool; }
   | Unlock of Cil.exp
-  | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; }
+  | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; multiple: bool }
   | ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; }
   | ThreadExit of { ret_val: Cil.exp; }
   | Signal of Cil.exp
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index b94f751568..ab0d04d3ec 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -422,7 +422,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
 
 (** Pthread functions. *)
 let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
-    ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *)
+    ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg; multiple = false }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *)
     ("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *)
     ("pthread_join", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval});
     ("pthread_kill", unknown [drop "thread" []; drop "sig" []]);
@@ -1007,7 +1007,7 @@ let rtnl_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[rtnl_lock
 
 (** LDV Klever functions. *)
 let klever_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
-    ("pthread_create_N", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }); (* TODO: add multiple flag to ThreadCreate *)
+    ("pthread_create_N", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg; multiple = true });
     ("pthread_join_N", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval});
     ("ldv_mutex_model_lock", special [__ "lock" []; drop "sign" []] @@ fun lock -> Lock { lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true });
     ("ldv_mutex_model_unlock", special [__ "lock" []; drop "sign" []] @@ fun lock -> Unlock lock);

From 5a6362e1c0bda3ad0feb3332bf64e95fcea810b8 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 27 Nov 2023 14:32:47 +0200
Subject: [PATCH 07/43] Fix LibraryDslTest compilation

---
 unittest/analyses/libraryDslTest.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/unittest/analyses/libraryDslTest.ml b/unittest/analyses/libraryDslTest.ml
index e1fa23281c..077b81b8fa 100644
--- a/unittest/analyses/libraryDslTest.ml
+++ b/unittest/analyses/libraryDslTest.ml
@@ -11,7 +11,7 @@ let pthread_mutex_lock_desc: LibraryDesc.t = LibraryDsl.(
   )
 
 let pthread_create_desc: LibraryDesc.t = LibraryDsl.(
-    special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [r]; __ "arg" [r]] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }
+    special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [r]; __ "arg" [r]] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg; multiple = false }
   )
 
 let realloc_desc: LibraryDesc.t = LibraryDsl.(

From a3923237a01b4f6476911655e8b006b139337a8a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 30 Nov 2023 12:58:30 +0200
Subject: [PATCH 08/43] Generalize mutex-meet-tid privatization to arbitrary
 digest

---
 src/analyses/apron/relationPriv.apron.ml | 41 +++++++++---------
 src/analyses/basePriv.ml                 | 39 +++++++++--------
 src/analyses/commonPriv.ml               | 54 ++++++++++++++++--------
 3 files changed, 79 insertions(+), 55 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index b386af162b..ad55c425cd 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -844,7 +844,7 @@ struct
 end
 
 (** Per-mutex meet with TIDs. *)
-module PerMutexMeetPrivTID (Cluster: ClusterArg): S  = functor (RD: RelationDomain.RD) ->
+module PerMutexMeetPrivTID (Digest: Digest) (Cluster: ClusterArg): S  = functor (RD: RelationDomain.RD) ->
 struct
   open CommonPerMutex(RD)
   include MutexGlobals
@@ -854,10 +854,7 @@ struct
   module Cluster = NC
   module LRD = NC.LRD
 
-  include PerMutexTidCommon(struct
-      let exclude_not_started () = GobConfig.get_bool "ana.relation.priv.not-started"
-      let exclude_must_joined () = GobConfig.get_bool "ana.relation.priv.must-joined"
-    end)(LRD)
+  include PerMutexTidCommon (Digest) (LRD)
 
   module AV = RD.V
   module P = UnitP
@@ -865,10 +862,9 @@ struct
   let name () = "PerMutexMeetPrivTID(" ^ (Cluster.name ()) ^ (if GobConfig.get_bool "ana.relation.priv.must-joined" then  ",join"  else "") ^ ")"
 
   let get_relevant_writes (ask:Q.ask) m v =
-    let current = ThreadId.get_current ask in
-    let must_joined = ask.f Queries.MustJoinedThreads in
+    let current = Digest.current ask in
     GMutex.fold (fun k v acc ->
-        if compatible ask current must_joined k then
+        if Digest.compatible ask current k then
           LRD.join acc (Cluster.keep_only_protected_globals ask m v)
         else
           acc
@@ -946,8 +942,8 @@ struct
     (* unlock *)
     let rel_side = RD.keep_vars rel_local [g_var] in
     let rel_side = Cluster.unlock (W.singleton g) rel_side in
-    let tid = ThreadId.get_current ask in
-    let sidev = GMutex.singleton tid rel_side in
+    let digest = Digest.current ask in
+    let sidev = GMutex.singleton digest rel_side in
     sideg (V.global g) (G.create_global sidev);
     let l' = L.add lm rel_side l in
     let rel_local' =
@@ -984,8 +980,8 @@ struct
     else
       let rel_side = keep_only_protected_globals ask m rel in
       let rel_side = Cluster.unlock w rel_side in
-      let tid = ThreadId.get_current ask in
-      let sidev = GMutex.singleton tid rel_side in
+      let digest = Digest.current ask in
+      let sidev = GMutex.singleton digest rel_side in
       sideg (V.mutex m) (G.create_mutex sidev);
       let lm = LLock.mutex m in
       let l' = L.add lm rel_side l in
@@ -1069,8 +1065,8 @@ struct
     in
     let rel_side = RD.keep_vars rel g_vars in
     let rel_side = Cluster.unlock (W.top ()) rel_side in (* top W to avoid any filtering *)
-    let tid = ThreadId.get_current ask in
-    let sidev = GMutex.singleton tid rel_side in
+    let digest = Digest.current ask in
+    let sidev = GMutex.singleton digest rel_side in
     sideg V.mutex_inits (G.create_mutex sidev);
     (* Introduction into local state not needed, will be read via initializer *)
     (* Also no side-effect to mutex globals needed, the value here will either by read via the initializer, *)
@@ -1202,17 +1198,24 @@ end
 
 let priv_module: (module S) Lazy.t =
   lazy (
+    let module TIDDigest = ThreadDigest (
+      struct
+        let exclude_not_started () = GobConfig.get_bool "ana.relation.priv.not-started"
+        let exclude_must_joined () = GobConfig.get_bool "ana.relation.priv.must-joined"
+      end
+      )
+    in
     let module Priv: S =
       (val match get_string "ana.relation.privatization" with
          | "top" -> (module Top : S)
          | "protection" -> (module ProtectionBasedPriv (struct let path_sensitive = false end))
          | "protection-path" -> (module ProtectionBasedPriv (struct let path_sensitive = true end))
          | "mutex-meet" -> (module PerMutexMeetPriv)
-         | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (NoCluster))
-         | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (Clustering12)))
-         | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ArbitraryCluster (Clustering2)))
-         | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (ArbitraryCluster (ClusteringMax)))
-         | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (ClusteringPower)))
+         | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (TIDDigest) (NoCluster))
+         | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (TIDDigest) (DownwardClosedCluster (Clustering12)))
+         | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (TIDDigest) (ArbitraryCluster (Clustering2)))
+         | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (TIDDigest) (ArbitraryCluster (ClusteringMax)))
+         | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (TIDDigest) (DownwardClosedCluster (ClusteringPower)))
          | _ -> failwith "ana.relation.privatization: illegal value"
       )
     in
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 3843dda300..0c67347d3f 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -391,14 +391,11 @@ struct
       st
 end
 
-module PerMutexMeetTIDPriv: S =
+module PerMutexMeetTIDPriv (Digest: Digest): S =
 struct
   open Queries.Protection
   include PerMutexMeetPrivBase
-  include PerMutexTidCommon(struct
-      let exclude_not_started () = GobConfig.get_bool "ana.base.priv.not-started"
-      let exclude_must_joined () = GobConfig.get_bool "ana.base.priv.must-joined"
-    end)(CPA)
+  include PerMutexTidCommon (Digest) (CPA)
 
   let iter_sys_vars getg vq vf =
     match vq with
@@ -425,11 +422,10 @@ struct
     r
 
   let get_relevant_writes (ask:Q.ask) m v =
-    let current = ThreadId.get_current ask in
-    let must_joined = ask.f Queries.MustJoinedThreads in
+    let current = Digest.current ask in
     let is_in_Gm x _ = is_protected_by ~protection:Weak ask m x in
     GMutex.fold (fun k v acc ->
-        if compatible ask current must_joined k then
+        if Digest.compatible ask current k then
           CPA.join acc (CPA.filter is_in_Gm v)
         else
           acc
@@ -474,8 +470,8 @@ struct
         CPA.add x v st.cpa
     in
     if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a\n" CilType.Varinfo.pretty x VD.pretty v;
-    let tid = ThreadId.get_current ask in
-    let sidev = GMutex.singleton tid (CPA.singleton x v) in
+    let digest = Digest.current ask in
+    let sidev = GMutex.singleton digest (CPA.singleton x v) in
     let l' = L.add lm (CPA.singleton x v) l in
     let is_recovered_st = ask.f (Queries.MustBeSingleThreaded {since_start = false}) && not @@ ask.f (Queries.MustBeSingleThreaded {since_start = true}) in
     let l' = if is_recovered_st then
@@ -517,8 +513,8 @@ struct
       {st with cpa = cpa'; priv = (w',lmust,l)}
     else
       let is_in_Gm x _ = is_protected_by ~protection:Weak ask m x in
-      let tid = ThreadId.get_current ask in
-      let sidev = GMutex.singleton tid (CPA.filter is_in_Gm st.cpa) in
+      let digest = Digest.current ask in
+      let sidev = GMutex.singleton digest (CPA.filter is_in_Gm st.cpa) in
       sideg (V.mutex m) (G.create_mutex sidev);
       let lm = LLock.mutex m in
       let l' = L.add lm (CPA.filter is_in_Gm st.cpa) l in
@@ -568,13 +564,13 @@ struct
 
   let escape ask getg sideg (st: BaseComponents (D).t) escaped =
     let escaped_cpa = CPA.filter (fun x _ -> EscapeDomain.EscapedVars.mem x escaped) st.cpa in
-    let tid = ThreadId.get_current ask in
-    let sidev = GMutex.singleton tid escaped_cpa in
+    let digest = Digest.current ask in
+    let sidev = GMutex.singleton digest escaped_cpa in
     sideg V.mutex_inits (G.create_mutex sidev);
     let cpa' = CPA.fold (fun x v acc ->
         if EscapeDomain.EscapedVars.mem x escaped (* && is_unprotected ask x *) then (
           if M.tracing then M.tracel "priv" "ESCAPE SIDE %a = %a\n" CilType.Varinfo.pretty x VD.pretty v;
-          let sidev = GMutex.singleton tid (CPA.singleton x v) in
+          let sidev = GMutex.singleton digest (CPA.singleton x v) in
           sideg (V.global x) (G.create_global sidev);
           CPA.remove x acc
         )
@@ -587,8 +583,8 @@ struct
   let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) =
     let cpa = st.cpa in
     let cpa_side = CPA.filter (fun x _ -> is_global ask x) cpa in
-    let tid = ThreadId.get_current ask in
-    let sidev = GMutex.singleton tid cpa_side in
+    let digest = Digest.current ask in
+    let sidev = GMutex.singleton digest cpa_side in
     sideg V.mutex_inits (G.create_mutex sidev);
     (* Introduction into local state not needed, will be read via initializer *)
     (* Also no side-effect to mutex globals needed, the value here will either by read via the initializer, *)
@@ -1790,12 +1786,19 @@ end
 
 let priv_module: (module S) Lazy.t =
   lazy (
+    let module TIDDigest = ThreadDigest (
+      struct
+        let exclude_not_started () = GobConfig.get_bool "ana.relation.priv.not-started"
+        let exclude_must_joined () = GobConfig.get_bool "ana.relation.priv.must-joined"
+      end
+      )
+    in
     let module Priv: S =
       (val match get_string "ana.base.privatization" with
         | "none" -> (module NonePriv: S)
         | "mutex-oplus" -> (module PerMutexOplusPriv)
         | "mutex-meet" -> (module PerMutexMeetPriv)
-        | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv)
+        | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (TIDDigest))
         | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false end))
         | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true end))
         | "mine" -> (module MinePriv)
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 88181000b9..3c8056bb34 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -154,12 +154,44 @@ struct
   end
 end
 
+module type Digest =
+sig
+  include Printable.S
+
+  val current: Q.ask -> t
+  val compatible: Q.ask -> t -> t -> bool
+end
+
 module type PerMutexTidCommonArg = sig
   val exclude_not_started: unit -> bool
   val exclude_must_joined: unit -> bool
 end
 
-module PerMutexTidCommon (Conf:PerMutexTidCommonArg) (LD:Lattice.S) =
+module ThreadDigest (Conf: PerMutexTidCommonArg): Digest =
+struct
+  include ThreadIdDomain.ThreadLifted
+
+  module TID = ThreadIdDomain.Thread
+
+  let current (ask: Q.ask) =
+    ThreadId.get_current ask
+
+  let compatible (ask: Q.ask) (current: t) (other: t) =
+    let must_joined = ask.f Queries.MustJoinedThreads in
+    match current, other with
+    | `Lifted current, `Lifted other ->
+      if (TID.is_unique current) && (TID.equal current other) then
+        false (* self-read *)
+      else if Conf.exclude_not_started () && MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other then
+        false (* other is not started yet *)
+      else if Conf.exclude_must_joined () && MHP.must_be_joined other must_joined then
+        false (* accounted for in local information *)
+      else
+        true
+    | _ -> true
+end
+
+module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) =
 struct
   include ConfCheck.RequireThreadFlagPathSensInit
 
@@ -196,7 +228,7 @@ struct
 
   (* Map from locks to last written values thread-locally *)
   module L = MapDomain.MapBot_LiftTop (LLock) (LD)
-  module GMutex = MapDomain.MapBot_LiftTop (ThreadIdDomain.ThreadLifted) (LD)
+  module GMutex = MapDomain.MapBot_LiftTop (Digest) (LD)
   module GThread = Lattice.Prod (LMust) (L)
 
   module G =
@@ -218,24 +250,10 @@ struct
 
   module D = Lattice.Prod3 (W) (LMust) (L)
 
-  let compatible (ask:Q.ask) current must_joined other =
-    match current, other with
-    | `Lifted current, `Lifted other ->
-      if (TID.is_unique current) && (TID.equal current other) then
-        false (* self-read *)
-      else if Conf.exclude_not_started () && MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other then
-        false (* other is not started yet *)
-      else if Conf.exclude_must_joined () && MHP.must_be_joined other must_joined then
-        false (* accounted for in local information *)
-      else
-        true
-    | _ -> true
-
   let get_relevant_writes_nofilter (ask:Q.ask) v =
-    let current = ThreadId.get_current ask in
-    let must_joined = ask.f Queries.MustJoinedThreads in
+    let current = Digest.current ask in
     GMutex.fold (fun k v acc ->
-        if compatible ask current must_joined k then
+        if Digest.compatible ask current k then
           LD.join acc v
         else
           acc

From 6dfc08ff3aa493a0808edd0ac19914fe8ecde375 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 30 Nov 2023 13:34:26 +0200
Subject: [PATCH 09/43] Simplify CommonPriv.ThreadDigest

---
 src/analyses/apron/relationPriv.apron.ml | 17 +++++------------
 src/analyses/basePriv.ml                 |  9 +--------
 src/analyses/commonPriv.ml               | 11 +++--------
 3 files changed, 9 insertions(+), 28 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index ad55c425cd..a34e052602 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -1198,24 +1198,17 @@ end
 
 let priv_module: (module S) Lazy.t =
   lazy (
-    let module TIDDigest = ThreadDigest (
-      struct
-        let exclude_not_started () = GobConfig.get_bool "ana.relation.priv.not-started"
-        let exclude_must_joined () = GobConfig.get_bool "ana.relation.priv.must-joined"
-      end
-      )
-    in
     let module Priv: S =
       (val match get_string "ana.relation.privatization" with
          | "top" -> (module Top : S)
          | "protection" -> (module ProtectionBasedPriv (struct let path_sensitive = false end))
          | "protection-path" -> (module ProtectionBasedPriv (struct let path_sensitive = true end))
          | "mutex-meet" -> (module PerMutexMeetPriv)
-         | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (TIDDigest) (NoCluster))
-         | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (TIDDigest) (DownwardClosedCluster (Clustering12)))
-         | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (TIDDigest) (ArbitraryCluster (Clustering2)))
-         | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (TIDDigest) (ArbitraryCluster (ClusteringMax)))
-         | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (TIDDigest) (DownwardClosedCluster (ClusteringPower)))
+         | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (ThreadDigest) (NoCluster))
+         | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (ThreadDigest) (DownwardClosedCluster (Clustering12)))
+         | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ThreadDigest) (ArbitraryCluster (Clustering2)))
+         | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (ThreadDigest) (ArbitraryCluster (ClusteringMax)))
+         | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (ThreadDigest) (DownwardClosedCluster (ClusteringPower)))
          | _ -> failwith "ana.relation.privatization: illegal value"
       )
     in
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 0c67347d3f..e600c2a05d 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -1786,19 +1786,12 @@ end
 
 let priv_module: (module S) Lazy.t =
   lazy (
-    let module TIDDigest = ThreadDigest (
-      struct
-        let exclude_not_started () = GobConfig.get_bool "ana.relation.priv.not-started"
-        let exclude_must_joined () = GobConfig.get_bool "ana.relation.priv.must-joined"
-      end
-      )
-    in
     let module Priv: S =
       (val match get_string "ana.base.privatization" with
         | "none" -> (module NonePriv: S)
         | "mutex-oplus" -> (module PerMutexOplusPriv)
         | "mutex-meet" -> (module PerMutexMeetPriv)
-        | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (TIDDigest))
+        | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest))
         | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false end))
         | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true end))
         | "mine" -> (module MinePriv)
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 3c8056bb34..23ed36f7fb 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -162,12 +162,7 @@ sig
   val compatible: Q.ask -> t -> t -> bool
 end
 
-module type PerMutexTidCommonArg = sig
-  val exclude_not_started: unit -> bool
-  val exclude_must_joined: unit -> bool
-end
-
-module ThreadDigest (Conf: PerMutexTidCommonArg): Digest =
+module ThreadDigest: Digest =
 struct
   include ThreadIdDomain.ThreadLifted
 
@@ -182,9 +177,9 @@ struct
     | `Lifted current, `Lifted other ->
       if (TID.is_unique current) && (TID.equal current other) then
         false (* self-read *)
-      else if Conf.exclude_not_started () && MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other then
+      else if GobConfig.get_bool "ana.relation.priv.not-started" && MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other then
         false (* other is not started yet *)
-      else if Conf.exclude_must_joined () && MHP.must_be_joined other must_joined then
+      else if GobConfig.get_bool "ana.relation.priv.must-joined" && MHP.must_be_joined other must_joined then
         false (* accounted for in local information *)
       else
         true

From 05198f9640c3b39f8d7e2d661f76904c76f52d9a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 30 Nov 2023 13:35:36 +0200
Subject: [PATCH 10/43] Avoid MustJoinedThreads query in ThreadDigest if not
 needed

---
 src/analyses/commonPriv.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 23ed36f7fb..2e7ed570fd 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -172,14 +172,13 @@ struct
     ThreadId.get_current ask
 
   let compatible (ask: Q.ask) (current: t) (other: t) =
-    let must_joined = ask.f Queries.MustJoinedThreads in
     match current, other with
     | `Lifted current, `Lifted other ->
-      if (TID.is_unique current) && (TID.equal current other) then
+      if TID.is_unique current && TID.equal current other then
         false (* self-read *)
       else if GobConfig.get_bool "ana.relation.priv.not-started" && MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other then
         false (* other is not started yet *)
-      else if GobConfig.get_bool "ana.relation.priv.must-joined" && MHP.must_be_joined other must_joined then
+      else if GobConfig.get_bool "ana.relation.priv.must-joined" && MHP.must_be_joined other (ask.f Queries.MustJoinedThreads) then
         false (* accounted for in local information *)
       else
         true

From bda139ff7d12e2b59b20b289d89c60fdeef37304 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 5 Dec 2023 17:09:32 +0200
Subject: [PATCH 11/43] Rename Digest.compatible -> accounted_for

---
 src/analyses/apron/relationPriv.apron.ml | 2 +-
 src/analyses/basePriv.ml                 | 2 +-
 src/analyses/commonPriv.ml               | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index a34e052602..6c330e8798 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -864,7 +864,7 @@ struct
   let get_relevant_writes (ask:Q.ask) m v =
     let current = Digest.current ask in
     GMutex.fold (fun k v acc ->
-        if Digest.compatible ask current k then
+        if Digest.accounted_for ask ~current ~other:k then
           LRD.join acc (Cluster.keep_only_protected_globals ask m v)
         else
           acc
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index e600c2a05d..26fb5850a8 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -425,7 +425,7 @@ struct
     let current = Digest.current ask in
     let is_in_Gm x _ = is_protected_by ~protection:Weak ask m x in
     GMutex.fold (fun k v acc ->
-        if Digest.compatible ask current k then
+        if Digest.accounted_for ask ~current ~other:k then
           CPA.join acc (CPA.filter is_in_Gm v)
         else
           acc
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 2e7ed570fd..5f89eecdd8 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -159,7 +159,7 @@ sig
   include Printable.S
 
   val current: Q.ask -> t
-  val compatible: Q.ask -> t -> t -> bool
+  val accounted_for: Q.ask -> current:t -> other:t -> bool
 end
 
 module ThreadDigest: Digest =
@@ -171,7 +171,7 @@ struct
   let current (ask: Q.ask) =
     ThreadId.get_current ask
 
-  let compatible (ask: Q.ask) (current: t) (other: t) =
+  let accounted_for (ask: Q.ask) ~(current: t) ~(other: t) =
     match current, other with
     | `Lifted current, `Lifted other ->
       if TID.is_unique current && TID.equal current other then
@@ -247,7 +247,7 @@ struct
   let get_relevant_writes_nofilter (ask:Q.ask) v =
     let current = Digest.current ask in
     GMutex.fold (fun k v acc ->
-        if Digest.compatible ask current k then
+        if Digest.accounted_for ask ~current ~other:k then
           LD.join acc v
         else
           acc

From 0704cd55cb41cdfb628f6ce96bc137515fd25149 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 5 Dec 2023 17:11:21 +0200
Subject: [PATCH 12/43] Flip Digest.accounted_for implementation to match name

---
 src/analyses/apron/relationPriv.apron.ml |  2 +-
 src/analyses/basePriv.ml                 |  2 +-
 src/analyses/commonPriv.ml               | 12 ++++++------
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 6c330e8798..31dd1fc4f5 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -864,7 +864,7 @@ struct
   let get_relevant_writes (ask:Q.ask) m v =
     let current = Digest.current ask in
     GMutex.fold (fun k v acc ->
-        if Digest.accounted_for ask ~current ~other:k then
+        if not (Digest.accounted_for ask ~current ~other:k) then
           LRD.join acc (Cluster.keep_only_protected_globals ask m v)
         else
           acc
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 26fb5850a8..20ef13244b 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -425,7 +425,7 @@ struct
     let current = Digest.current ask in
     let is_in_Gm x _ = is_protected_by ~protection:Weak ask m x in
     GMutex.fold (fun k v acc ->
-        if Digest.accounted_for ask ~current ~other:k then
+        if not (Digest.accounted_for ask ~current ~other:k) then
           CPA.join acc (CPA.filter is_in_Gm v)
         else
           acc
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 5f89eecdd8..2739578957 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -175,14 +175,14 @@ struct
     match current, other with
     | `Lifted current, `Lifted other ->
       if TID.is_unique current && TID.equal current other then
-        false (* self-read *)
+        true (* self-read *)
       else if GobConfig.get_bool "ana.relation.priv.not-started" && MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other then
-        false (* other is not started yet *)
+        true (* other is not started yet *)
       else if GobConfig.get_bool "ana.relation.priv.must-joined" && MHP.must_be_joined other (ask.f Queries.MustJoinedThreads) then
-        false (* accounted for in local information *)
+        true (* accounted for in local information *)
       else
-        true
-    | _ -> true
+        false
+    | _ -> false
 end
 
 module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) =
@@ -247,7 +247,7 @@ struct
   let get_relevant_writes_nofilter (ask:Q.ask) v =
     let current = Digest.current ask in
     GMutex.fold (fun k v acc ->
-        if Digest.accounted_for ask ~current ~other:k then
+        if not (Digest.accounted_for ask ~current ~other:k) then
           LD.join acc v
         else
           acc

From a5d0f39537933c3a3464cb386f2f9e82c668acc7 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 27 Dec 2023 18:38:06 +0100
Subject: [PATCH 13/43] Code cleanup

---
 .../apron/affineEqualityDomain.apron.ml       | 109 +++++++++++-------
 1 file changed, 69 insertions(+), 40 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 5aa1090dd4..5cd7714682 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -291,15 +291,21 @@ struct
 
   let meet t1 t2 =
     let sup_env = Environment.lce t1.env t2.env in
-    let t1, t2 = change_d t1 sup_env true false, change_d t2 sup_env true false
-    in if is_bot t1 || is_bot t2 then bot() else
+    let t1, t2 = change_d t1 sup_env true false, change_d t2 sup_env true false in
+    if is_bot t1 || is_bot t2 then 
+      bot ()
+    else
+      (* TODO: Why can I be sure that m1 && m2 are all Some here? *)
       let m1, m2 = Option.get t1.d, Option.get t2.d in
-      match m1, m2 with
-      | x, y when is_top_env t1-> {d = Some (dim_add (Environment.dimchange t2.env sup_env) y); env = sup_env}
-      | x, y when is_top_env t2 -> {d = Some (dim_add (Environment.dimchange t1.env sup_env) x); env = sup_env}
-      | x, y ->
-        let rref_matr = Matrix.rref_matrix_with (Matrix.copy x) (Matrix.copy y) in
-        if Option.is_none rref_matr then bot () else
+      if is_top_env t1 then 
+        {d = Some (dim_add (Environment.dimchange t2.env sup_env) m2); env = sup_env} 
+      else if is_top_env t2 then 
+        {d = Some (dim_add (Environment.dimchange t1.env sup_env) m1); env = sup_env}
+      else
+        let rref_matr = Matrix.rref_matrix_with (Matrix.copy m1) (Matrix.copy m2) in
+        if Option.is_none rref_matr then 
+          bot ()
+        else
           {d = rref_matr; env = sup_env}
 
 
@@ -312,12 +318,20 @@ struct
 
   let leq t1 t2 =
     let env_comp = Environment.compare t1.env t2.env in (* Apron's Environment.compare has defined return values. *)
-    if env_comp = -2 || env_comp > 0 then false else
-    if is_bot t1 || is_top_env t2 then true else
-    if is_bot t2 || is_top_env t1 then false else (
+    if env_comp = -2 || env_comp > 0 then
+      (* -2:  environments are not compatible (a variable has different types in the 2 environements *)
+      (* -1: if env1 is a subset of env2,  (OK)  *)
+      (*  0:  if equality,  (OK) *)
+      (* +1: if env1 is a superset of env2, and +2 otherwise (the lce exists and is a strict superset of both) *) 
+      false
+    else if is_bot t1 || is_top_env t2 then 
+      true
+    else if is_bot t2 || is_top_env t1 then 
+      false 
+    else
       let m1, m2 = Option.get t1.d, Option.get t2.d in
       let m1' = if env_comp = 0 then m1 else dim_add (Environment.dimchange t1.env t2.env) m1 in
-      Matrix.is_covered_by m2 m1')
+      Matrix.is_covered_by m2 m1'
 
   let leq a b = timing_wrap "leq" (leq a) b
 
@@ -371,7 +385,11 @@ struct
               lin_disjunc new_r (s + 1) new_a new_b
             | _      -> failwith "Matrix not in rref form" end
     in
-    if is_bot a then b else if is_bot b then a else
+    if is_bot a then 
+      b
+    else if is_bot b then 
+      a
+    else
       match Option.get a.d, Option.get b.d with
       | x, y when is_top_env a || is_top_env b -> {d = Some (Matrix.empty ()); env = Environment.lce a.env b.env}
       | x, y when (Environment.compare a.env b.env <> 0) ->
@@ -388,33 +406,34 @@ struct
     let res = join a b in
     if M.tracing then M.tracel "join" "join a: %s b: %s -> %s \n" (show a) (show b) (show res) ;
     res
+
   let widen a b =
-    let a_env = a.env in
-    let b_env = b.env in
-    if Environment.equal a_env b_env  then
+    if Environment.equal a.env b.env then
       join a b
-    else b
+    else
+      b
 
   let narrow a b = a
+
   let pretty_diff () (x, y) =
     dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
 
-  let remove_rels_with_var x var env imp =
+  let remove_rels_with_var x var env inplace =
     let j0 = Environment.dim_of_var env var in
-    if imp then (Matrix.reduce_col_with x j0; x) else Matrix.reduce_col x j0
+    if inplace then 
+      (Matrix.reduce_col_with x j0; x) 
+    else 
+      Matrix.reduce_col x j0
 
-  let remove_rels_with_var x var env imp = timing_wrap "remove_rels_with_var" (remove_rels_with_var x var env) imp
+  let remove_rels_with_var x var env inplace = timing_wrap "remove_rels_with_var" (remove_rels_with_var x var env) inplace
 
   let forget_vars t vars =
-    if is_bot t || is_top_env t then t
+    if is_bot t || is_top_env t || List.is_empty vars then 
+      t
     else
       let m = Option.get t.d in
-      if List.is_empty vars then t else
-        let rec rem_vars m vars' =
-          begin match vars' with
-            |            [] -> m
-            | x :: xs -> rem_vars (remove_rels_with_var m x t.env true) xs end
-        in {d = Some (Matrix.remove_zero_rows @@ rem_vars (Matrix.copy m) vars); env = t.env}
+      let rem_from m = List.fold_left (fun m' x -> remove_rels_with_var m' x t.env true) m vars in
+      {d = Some (Matrix.remove_zero_rows @@ rem_from (Matrix.copy m)); env = t.env}
 
   let forget_vars t vars =
     let res = forget_vars t vars in
@@ -472,6 +491,7 @@ struct
     if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %s \n exp: %a\n no_ov: %b -> \n %s\n"
         (show t) (Var.to_string var) d_exp exp (Lazy.force no_ov) (show res) ;
     res
+
   let assign_var (t: VarManagement(Vc)(Mx).t) v v' =
     let t = add_vars t [v; v'] in
     let texpr1 = Texpr1.of_expr (t.env) (Var v') in
@@ -489,14 +509,20 @@ struct
     let t_primed = add_vars t primed_vars in
     let multi_t = List.fold_left2 (fun t' v_prime (_,v') -> assign_var t' v_prime v') t_primed primed_vars vv's in
     match multi_t.d with
-    | Some m when not @@ is_top_env multi_t -> let replace_col m x y = let dim_x, dim_y = Environment.dim_of_var multi_t.env x, Environment.dim_of_var multi_t.env y in
-                                                 let col_x = Matrix.get_col m dim_x in
-                                                 Matrix.set_col_with m col_x dim_y in
+    | Some m when not @@ is_top_env multi_t -> 
+      let replace_col m x y = 
+        let dim_x, dim_y = Environment.dim_of_var multi_t.env x, Environment.dim_of_var multi_t.env y in
+        let col_x = Matrix.get_col m dim_x in
+        Matrix.set_col_with m col_x dim_y
+      in
       let m_cp = Matrix.copy m in
-      let switched_m = List.fold_left2 (fun m' x y -> replace_col m' x y) m_cp primed_vars assigned_vars in
+      let switched_m = List.fold_left2 replace_col m_cp primed_vars assigned_vars in
       let res = drop_vars {d = Some switched_m; env = multi_t.env} primed_vars true in
       let x = Option.get res.d in
-      if Matrix.normalize_with x then {d = Some x; env = res.env} else bot ()
+      if Matrix.normalize_with x then 
+        {d = Some x; env = res.env} 
+      else 
+        bot ()
     | _ -> t
 
   let assign_var_parallel t vv's =
@@ -561,14 +587,17 @@ struct
       | _, _ -> overflow_res res
 
   let meet_tcons t tcons expr =
-    let check_const cmp c = if cmp c Mpqf.zero then bot_env else t
-    in
+    let check_const cmp c = if cmp c Mpqf.zero then bot_env else t in
     let meet_vec e =
       (*Flip the sign of the const. val in coeff vec*)
       Vector.mapi_with (fun i x -> if Vector.compare_length_with e (i + 1) = 0 then Mpqf.mone *: x else x) e;
-      let res = if is_bot t then bot () else
-          let opt_m = Matrix.rref_vec_with (Matrix.copy @@ Option.get t.d) e
-          in if Option.is_none opt_m then bot () else {d = opt_m; env = t.env} in
+      let res =
+        if is_bot t then 
+          bot () 
+        else
+          let opt_m = Matrix.rref_vec_with (Matrix.copy @@ Option.get t.d) e in 
+          if Option.is_none opt_m then bot () else {d = opt_m; env = t.env}
+      in
       meet_tcons_one_var_eq res expr
     in
     match get_coeff_vec t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with
@@ -615,9 +644,7 @@ struct
   let relift t = t
 
   let invariant t =
-    match t.d with
-    | None -> []
-    | Some m ->
+    let invariant m =
       let earray = Lincons1.array_make t.env (Matrix.num_rows m) in
       for i = 0 to Lincons1.array_length earray do
         let row = Matrix.get_row m i in
@@ -631,6 +658,8 @@ struct
           Lincons1.{lincons0; env = array_env}
         )
       |> List.of_enum
+    in
+    BatOption.map_default invariant [] t.d
 
   let cil_exp_of_lincons1 = Convert.cil_exp_of_lincons1
 

From fe4a58f5153a7edbfae229a35d0b393d93ab93cc Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 27 Dec 2023 18:57:27 +0100
Subject: [PATCH 14/43] Fix constant printing

---
 .../apron/affineEqualityDomain.apron.ml       | 38 +++++++++++--------
 1 file changed, 22 insertions(+), 16 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 5cd7714682..4f47f6f494 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -243,31 +243,37 @@ struct
       Vector.of_array @@ row
     in
     let vec_to_constraint vec env =
-      let vars, _ = Environment.vars env
-      in let dim_to_str var =
-           let vl =  Vector.nth vec (Environment.dim_of_var env var)
-           in let var_str = Var.to_string var
-           in if vl =: Mpqf.one then "+" ^ var_str
-           else if vl =: Mpqf.mone then "-" ^ var_str
-           else if vl <: Mpqf.mone then Mpqf.to_string vl ^ var_str
-           else if vl >: Mpqf.one then Format.asprintf "+%s" (Mpqf.to_string vl) ^ var_str
-           else ""
+      let vars, _ = Environment.vars env in 
+      let dim_to_str var =
+        let vl =  Vector.nth vec (Environment.dim_of_var env var) in 
+        let var_str = Var.to_string var in 
+        if vl =: Mpqf.one then "+" ^ var_str
+        else if vl =: Mpqf.mone then "-" ^ var_str
+        else if vl <: Mpqf.mone then Mpqf.to_string vl ^ var_str
+        else if vl >: Mpqf.one then Format.asprintf "+%s" (Mpqf.to_string vl) ^ var_str
+        else ""
       in
       let c_to_str vl =
-        if vl >: Mpqf.zero then "-" ^ Mpqf.to_string vl
-        else if vl <: Mpqf.zero then "+" ^ Mpqf.to_string vl
-        else ""
+        if vl =: Mpqf.zero then 
+          ""
+        else
+          let negated = vl *: Mpqf.mone in
+          if negated >: Mpqf.zero then "+" ^ Mpqf.to_string negated
+          else Mpqf.to_string negated
       in
       let res = (String.concat "" @@ Array.to_list @@ Array.map dim_to_str vars)
-                ^ (c_to_str @@ Vector.nth vec (Vector.length vec - 1)) ^ "=0"
-      in if String.starts_with res "+" then String.sub res 1 (String.length res - 1) else res
+                ^ (c_to_str @@ Vector.nth vec (Vector.length vec - 1)) ^ "=0" in 
+      if String.starts_with res "+" then 
+        String.sub res 1 (String.length res - 1)
+      else
+        res
     in
     match t.d with
     | None -> "Bottom Env"
     | Some m when Matrix.is_empty m -> "⊤"
     | Some m ->
-      let constraint_list = List.init (Matrix.num_rows m) (fun i -> vec_to_constraint (conv_to_ints @@ Matrix.get_row m i) t.env)
-      in Format.asprintf "%s" ("[|"^ (String.concat "; " constraint_list) ^"|]")
+      let constraint_list = List.init (Matrix.num_rows m) (fun i -> vec_to_constraint (conv_to_ints @@ Matrix.get_row m i) t.env) in
+      Format.asprintf "%s" ("[|"^ (String.concat "; " constraint_list) ^"|]")
 
   let pretty () (x:t) = text (show x)
   let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nmatrix\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%s</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env)))

From 31065ed0addc6471416ae81b8b915f04dda9eb42 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 27 Dec 2023 19:47:11 +0100
Subject: [PATCH 15/43] Make computations in show directly on Z

---
 .../apron/affineEqualityDomain.apron.ml       | 50 ++++++++++---------
 1 file changed, 26 insertions(+), 24 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 4f47f6f494..a1653bb423 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -230,39 +230,41 @@ struct
 
   let show t =
     let conv_to_ints row =
-      let module BI = IntOps.BigIntOps in
-      let row = Array.copy @@ Vector.to_array row
-      in
-      for i = 0 to Array.length row -1 do
-        let val_i = Mpqf.of_mpz @@ Z_mlgmpidl.mpzf_of_z @@ Mpqf.get_den row.(i)
-        in Array.iteri(fun j x -> row.(j) <- val_i *: x)  row
-      done;
-      let int_arr = Array.init (Array.length row) (fun i -> Mpqf.get_num row.(i))
-      in let div = Mpqf.of_mpz @@ Z_mlgmpidl.mpzf_of_z @@ Array.fold_left BI.gcd int_arr.(0) int_arr
-      in Array.iteri (fun i x -> row.(i) <- x /: div) row;
-      Vector.of_array @@ row
+      let row = Array.copy @@ Vector.to_array row in
+      let mpqf_of_z x = Mpqf.of_mpz @@ Z_mlgmpidl.mpzf_of_z x in
+      let lcm = mpqf_of_z @@ Array.fold_left (fun x y -> Z.lcm x (Mpqf.get_den y)) Z.one row in
+      Array.modify (fun x -> x *: lcm) row;
+      let int_arr = Array.map (fun x -> Mpqf.get_num x) row in
+      let div = Array.fold_left Z.gcd int_arr.(0) int_arr in
+      Array.modify (fun x -> Z.div x div) int_arr;
+      int_arr
     in
-    let vec_to_constraint vec env =
+    let vec_to_constraint arr env =
       let vars, _ = Environment.vars env in 
       let dim_to_str var =
-        let vl =  Vector.nth vec (Environment.dim_of_var env var) in 
+        let vl =  arr.(Environment.dim_of_var env var) in 
         let var_str = Var.to_string var in 
-        if vl =: Mpqf.one then "+" ^ var_str
-        else if vl =: Mpqf.mone then "-" ^ var_str
-        else if vl <: Mpqf.mone then Mpqf.to_string vl ^ var_str
-        else if vl >: Mpqf.one then Format.asprintf "+%s" (Mpqf.to_string vl) ^ var_str
-        else ""
+        if Z.equal vl Z.zero then 
+          ""
+        else if Z.equal vl Z.one then 
+          "+" ^ var_str
+        else if Z.equal vl Z.minus_one then 
+          "-" ^ var_str
+        else if Z.lt vl Z.minus_one then
+          Z.to_string vl ^ var_str
+        else
+          Format.asprintf "+%s" (Z.to_string vl) ^ var_str
       in
-      let c_to_str vl =
-        if vl =: Mpqf.zero then 
+      let const_to_str vl =
+        if Z.equal vl Z.zero then 
           ""
         else
-          let negated = vl *: Mpqf.mone in
-          if negated >: Mpqf.zero then "+" ^ Mpqf.to_string negated
-          else Mpqf.to_string negated
+          let negated = Z.mul vl Z.minus_one in
+          if Z.gt negated Z.zero then "+" ^ Z.to_string negated
+          else Z.to_string negated
       in
       let res = (String.concat "" @@ Array.to_list @@ Array.map dim_to_str vars)
-                ^ (c_to_str @@ Vector.nth vec (Vector.length vec - 1)) ^ "=0" in 
+                ^ (const_to_str arr.(Array.length arr - 1)) ^ "=0" in 
       if String.starts_with res "+" then 
         String.sub res 1 (String.length res - 1)
       else

From 29b8ca2f0d60e0654f83dc7b158f50064406879c Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 27 Dec 2023 20:00:52 +0100
Subject: [PATCH 16/43] A bit more refactoring

---
 .../apron/affineEqualityDomain.apron.ml       | 85 ++++++++++---------
 1 file changed, 43 insertions(+), 42 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index a1653bb423..6c5112c279 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -59,7 +59,9 @@ struct
   let dim_add ch m = timing_wrap "dim add" (dim_add ch) m
 
   let dim_remove (ch: Apron.Dim.change) m del =
-    if Array.length ch.dim = 0 || Matrix.is_empty m then m else (
+    if Array.length ch.dim = 0 || Matrix.is_empty m then 
+      m 
+    else (
       Array.iteri (fun i x-> ch.dim.(i) <- x + i) ch.dim;
       let m' = if not del then let m = Matrix.copy m in Array.fold_left (fun y x -> Matrix.reduce_col_with y x; y) m ch.dim else m in
       Matrix.remove_zero_rows @@ Matrix.del_cols m' ch.dim)
@@ -146,47 +148,46 @@ struct
     let is_const_vec v = Vector.compare_length_with (Vector.filteri (fun i x -> (*Inefficient*)
         Vector.compare_length_with v (i + 1) > 0 && x <>: Mpqf.zero) v) 1 = 0
     in
-    let rec convert_texpr texp =
-      begin match texp with
-        (*If x is a constant, replace it with its const. val. immediately*)
-        | Cst x -> let of_union union =
-                     let open Coeff in
-                     match union with
-                     | Interval _ -> failwith "Not a constant"
-                     | Scalar x -> (match x with
-                         | Float x -> Mpqf.of_float x
-                         | Mpqf x -> x
-                         | Mpfrf x -> Mpfr.to_mpq x) in Vector.set_val zero_vec ((Vector.length zero_vec) - 1) (of_union x)
-        | Var x ->
-          let zero_vec_cp = Vector.copy zero_vec in
-          let entry_only v = Vector.set_val_with v (Environment.dim_of_var t.env x) Mpqf.one; v in
-          begin match t.d with
-            | Some m -> let row = Matrix.find_opt (fun r -> Vector.nth r (Environment.dim_of_var t.env x) =: Mpqf.one) m in
-              begin match row with
-                | Some v when is_const_vec v ->
-                  Vector.set_val_with zero_vec_cp ((Vector.length zero_vec) - 1) (Vector.nth v (Vector.length v - 1)); zero_vec_cp
-                | _ -> entry_only zero_vec_cp end
-            | None -> entry_only zero_vec_cp end
-        | Unop (u, e, _, _) ->
-          begin match u with
-            | Neg -> neg @@ convert_texpr e
-            | Cast -> convert_texpr e (*Ignore since casts in apron are used for floating point nums and rounding in contrast to CIL casts*)
-            | Sqrt -> raise NotLinear end
-        | Binop (b, e1, e2, _, _) ->
-          begin match b with
-            | Add -> let v1 = convert_texpr e1 in Vector.map2_with (+:) v1 (convert_texpr e2); v1
-            | Sub -> let v1 = convert_texpr e1 in Vector.map2_with (+:) v1 (neg @@ convert_texpr e2); v1
-            | Mul ->
-              let x1, x2 = convert_texpr e1, convert_texpr e2 in
-              begin match get_c x1, get_c x2 with
-                | _, Some c -> Vector.apply_with_c_with ( *:) c x1; x1
-                | Some c, _ -> Vector.apply_with_c_with ( *:) c x2; x2
-                | _, _ -> raise NotLinear end
-            | _ -> raise NotLinear end
-      end
-    in match convert_texpr texp with
-    | exception NotLinear -> None
-    | x -> Some(x)
+    let rec convert_texpr = function
+      (*If x is a constant, replace it with its const. val. immediately*)
+      | Cst x -> 
+        let of_union = function
+          | Coeff.Interval _ -> failwith "Not a constant"
+          | Scalar Float x -> Mpqf.of_float x
+          | Scalar Mpqf x -> x
+          | Scalar Mpfrf x -> Mpfr.to_mpq x
+        in 
+        Vector.set_val zero_vec ((Vector.length zero_vec) - 1) (of_union x)
+      | Var x ->
+        let zero_vec_cp = Vector.copy zero_vec in
+        let entry_only v = Vector.set_val_with v (Environment.dim_of_var t.env x) Mpqf.one; v in
+        begin match t.d with
+          | Some m -> 
+            let row = Matrix.find_opt (fun r -> Vector.nth r (Environment.dim_of_var t.env x) =: Mpqf.one) m in
+            begin match row with
+              | Some v when is_const_vec v ->
+                Vector.set_val_with zero_vec_cp ((Vector.length zero_vec) - 1) (Vector.nth v (Vector.length v - 1)); zero_vec_cp
+              | _ -> entry_only zero_vec_cp
+            end
+          | None -> entry_only zero_vec_cp end
+      | Unop (Neg, e, _, _) -> neg @@ convert_texpr e
+      | Unop (Cast, e, _, _) -> convert_texpr e (*Ignore since casts in apron are used for floating point nums and rounding in contrast to CIL casts*)
+      | Unop (Sqrt, e, _, _) -> raise NotLinear
+      | Binop (b, e1, e2, _, _) ->
+        begin match b with
+          | Add -> let v1 = convert_texpr e1 in Vector.map2_with (+:) v1 (convert_texpr e2); v1
+          | Sub -> let v1 = convert_texpr e1 in Vector.map2_with (+:) v1 (neg @@ convert_texpr e2); v1
+          | Mul ->
+            let x1, x2 = convert_texpr e1, convert_texpr e2 in
+            begin match get_c x1, get_c x2 with
+              | _, Some c -> Vector.apply_with_c_with ( *:) c x1; x1
+              | Some c, _ -> Vector.apply_with_c_with ( *:) c x2; x2
+              | _, _ -> raise NotLinear end
+          | _ -> raise NotLinear end
+    in 
+    try
+      Some (convert_texpr texp)
+    with NotLinear -> None
 
   let get_coeff_vec t texp = timing_wrap "coeff_vec" (get_coeff_vec t) texp
 end

From 4f113e1618883ca8a193c40e2481aab14726049e Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 27 Dec 2023 20:12:36 +0100
Subject: [PATCH 17/43] Use modifyi where appropriate

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

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 6c5112c279..9febdb5778 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -53,7 +53,7 @@ struct
   let copy t = {t with d = Option.map Matrix.copy t.d}
 
   let dim_add (ch: Apron.Dim.change) m =
-    Array.iteri (fun i x -> ch.dim.(i) <- x + i) ch.dim;
+    Array.modifyi (fun i x -> x + i) ch.dim; (* could be written Array.modifyi (+) ch.dim; but that's too smart *)
     Matrix.add_empty_columns m ch.dim
 
   let dim_add ch m = timing_wrap "dim add" (dim_add ch) m
@@ -62,7 +62,7 @@ struct
     if Array.length ch.dim = 0 || Matrix.is_empty m then 
       m 
     else (
-      Array.iteri (fun i x-> ch.dim.(i) <- x + i) ch.dim;
+      Array.modifyi (fun i x -> x + i) ch.dim;
       let m' = if not del then let m = Matrix.copy m in Array.fold_left (fun y x -> Matrix.reduce_col_with y x; y) m ch.dim else m in
       Matrix.remove_zero_rows @@ Matrix.del_cols m' ch.dim)
 

From e874d5de5aa6d65e26f1560c18bb3cb5e9c0d4f5 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 27 Dec 2023 20:26:10 +0100
Subject: [PATCH 18/43] Some formatting

---
 .../apron/affineEqualityDomain.apron.ml       | 24 ++++++++++++-------
 1 file changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 9febdb5778..ecd4bdc1d5 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -69,12 +69,19 @@ struct
   let dim_remove ch m del = timing_wrap "dim remove" (dim_remove ch m) del
 
   let change_d t new_env add del =
-    if Environment.equal t.env new_env then t else
-      let dim_change = if add then Environment.dimchange t.env new_env
-        else Environment.dimchange new_env t.env
-      in match t.d with
+    if Environment.equal t.env new_env then 
+      t
+    else
+      match t.d with
       | None -> bot_env
-      | Some m -> {d = Some (if add then dim_add dim_change m else dim_remove dim_change m del); env = new_env}
+      | Some m -> 
+        let dim_change = 
+          if add then 
+            Environment.dimchange t.env new_env
+          else 
+            Environment.dimchange new_env t.env
+        in
+        {d = Some (if add then dim_add dim_change m else dim_remove dim_change m del); env = new_env}
 
   let change_d t new_env add del = timing_wrap "dimension change" (change_d t new_env add) del
 
@@ -133,7 +140,8 @@ struct
 
   include ConvenienceOps(Mpqf)
 
-  let get_c v = match Vector.findi (fun x -> x <>: Mpqf.zero) v with
+  (** Get the constant from the vector if it is a constant *)
+  let get_c v = match Vector.findi ((<>:) Mpqf.zero) v with
     | exception Not_found -> Some Mpqf.zero
     | i when Vector.compare_length_with v (i + 1) = 0 -> Some (Vector.nth v i)
     | _ -> None
@@ -202,8 +210,8 @@ struct
     match get_coeff_vec t texpr  with
     | Some v -> begin match get_c v with
         | Some c when Mpqf.get_den c = IntOps.BigIntOps.one ->
-          let int_val = Mpqf.get_num c
-          in Some int_val, Some int_val
+          let int_val = Mpqf.get_num c in 
+          Some int_val, Some int_val
         | _ -> None, None end
     | _ -> None, None
 

From 059db8d83696c5883a09dae12026a1f4595bbbbb Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Dec 2023 12:24:59 +0100
Subject: [PATCH 19/43] Inline Binop

---
 .../apron/affineEqualityDomain.apron.ml       | 116 +++++++++---------
 1 file changed, 61 insertions(+), 55 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index ecd4bdc1d5..fff6437882 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -59,8 +59,8 @@ struct
   let dim_add ch m = timing_wrap "dim add" (dim_add ch) m
 
   let dim_remove (ch: Apron.Dim.change) m del =
-    if Array.length ch.dim = 0 || Matrix.is_empty m then 
-      m 
+    if Array.length ch.dim = 0 || Matrix.is_empty m then
+      m
     else (
       Array.modifyi (fun i x -> x + i) ch.dim;
       let m' = if not del then let m = Matrix.copy m in Array.fold_left (fun y x -> Matrix.reduce_col_with y x; y) m ch.dim else m in
@@ -69,16 +69,16 @@ struct
   let dim_remove ch m del = timing_wrap "dim remove" (dim_remove ch m) del
 
   let change_d t new_env add del =
-    if Environment.equal t.env new_env then 
+    if Environment.equal t.env new_env then
       t
     else
       match t.d with
       | None -> bot_env
-      | Some m -> 
-        let dim_change = 
-          if add then 
+      | Some m ->
+        let dim_change =
+          if add then
             Environment.dimchange t.env new_env
-          else 
+          else
             Environment.dimchange new_env t.env
         in
         {d = Some (if add then dim_add dim_change m else dim_remove dim_change m del); env = new_env}
@@ -158,19 +158,19 @@ struct
     in
     let rec convert_texpr = function
       (*If x is a constant, replace it with its const. val. immediately*)
-      | Cst x -> 
+      | Cst x ->
         let of_union = function
           | Coeff.Interval _ -> failwith "Not a constant"
           | Scalar Float x -> Mpqf.of_float x
           | Scalar Mpqf x -> x
           | Scalar Mpfrf x -> Mpfr.to_mpq x
-        in 
+        in
         Vector.set_val zero_vec ((Vector.length zero_vec) - 1) (of_union x)
       | Var x ->
         let zero_vec_cp = Vector.copy zero_vec in
         let entry_only v = Vector.set_val_with v (Environment.dim_of_var t.env x) Mpqf.one; v in
         begin match t.d with
-          | Some m -> 
+          | Some m ->
             let row = Matrix.find_opt (fun r -> Vector.nth r (Environment.dim_of_var t.env x) =: Mpqf.one) m in
             begin match row with
               | Some v when is_const_vec v ->
@@ -181,18 +181,24 @@ struct
       | Unop (Neg, e, _, _) -> neg @@ convert_texpr e
       | Unop (Cast, e, _, _) -> convert_texpr e (*Ignore since casts in apron are used for floating point nums and rounding in contrast to CIL casts*)
       | Unop (Sqrt, e, _, _) -> raise NotLinear
-      | Binop (b, e1, e2, _, _) ->
-        begin match b with
-          | Add -> let v1 = convert_texpr e1 in Vector.map2_with (+:) v1 (convert_texpr e2); v1
-          | Sub -> let v1 = convert_texpr e1 in Vector.map2_with (+:) v1 (neg @@ convert_texpr e2); v1
-          | Mul ->
-            let x1, x2 = convert_texpr e1, convert_texpr e2 in
-            begin match get_c x1, get_c x2 with
-              | _, Some c -> Vector.apply_with_c_with ( *:) c x1; x1
-              | Some c, _ -> Vector.apply_with_c_with ( *:) c x2; x2
-              | _, _ -> raise NotLinear end
-          | _ -> raise NotLinear end
-    in 
+      | Binop (Add, e1, e2, _, _) ->
+        let v1 = convert_texpr e1 in
+        let v2 = convert_texpr e2 in
+        Vector.map2_with (+:) v1 v2; v1
+      | Binop (Sub, e1, e2, _, _) ->
+        let v1 = convert_texpr e1 in
+        let v2 = convert_texpr e2 in
+        Vector.map2_with (+:) v1 (neg @@ v2); v1
+      | Binop (Mul, e1, e2, _, _) ->
+        let v1 = convert_texpr e1 in
+        let v2 = convert_texpr e2 in
+        begin match get_c v1, get_c v2 with
+          | _, Some c -> Vector.apply_with_c_with ( *:) c v1; v1
+          | Some c, _ -> Vector.apply_with_c_with ( *:) c v2; v2
+          | _, _ -> raise NotLinear
+        end
+      | Binop _ -> raise NotLinear
+    in
     try
       Some (convert_texpr texp)
     with NotLinear -> None
@@ -210,7 +216,7 @@ struct
     match get_coeff_vec t texpr  with
     | Some v -> begin match get_c v with
         | Some c when Mpqf.get_den c = IntOps.BigIntOps.one ->
-          let int_val = Mpqf.get_num c in 
+          let int_val = Mpqf.get_num c in
           Some int_val, Some int_val
         | _ -> None, None end
     | _ -> None, None
@@ -249,15 +255,15 @@ struct
       int_arr
     in
     let vec_to_constraint arr env =
-      let vars, _ = Environment.vars env in 
+      let vars, _ = Environment.vars env in
       let dim_to_str var =
-        let vl =  arr.(Environment.dim_of_var env var) in 
-        let var_str = Var.to_string var in 
-        if Z.equal vl Z.zero then 
+        let vl =  arr.(Environment.dim_of_var env var) in
+        let var_str = Var.to_string var in
+        if Z.equal vl Z.zero then
           ""
-        else if Z.equal vl Z.one then 
+        else if Z.equal vl Z.one then
           "+" ^ var_str
-        else if Z.equal vl Z.minus_one then 
+        else if Z.equal vl Z.minus_one then
           "-" ^ var_str
         else if Z.lt vl Z.minus_one then
           Z.to_string vl ^ var_str
@@ -265,7 +271,7 @@ struct
           Format.asprintf "+%s" (Z.to_string vl) ^ var_str
       in
       let const_to_str vl =
-        if Z.equal vl Z.zero then 
+        if Z.equal vl Z.zero then
           ""
         else
           let negated = Z.mul vl Z.minus_one in
@@ -273,8 +279,8 @@ struct
           else Z.to_string negated
       in
       let res = (String.concat "" @@ Array.to_list @@ Array.map dim_to_str vars)
-                ^ (const_to_str arr.(Array.length arr - 1)) ^ "=0" in 
-      if String.starts_with res "+" then 
+                ^ (const_to_str arr.(Array.length arr - 1)) ^ "=0" in
+      if String.starts_with res "+" then
         String.sub res 1 (String.length res - 1)
       else
         res
@@ -309,18 +315,18 @@ struct
   let meet t1 t2 =
     let sup_env = Environment.lce t1.env t2.env in
     let t1, t2 = change_d t1 sup_env true false, change_d t2 sup_env true false in
-    if is_bot t1 || is_bot t2 then 
+    if is_bot t1 || is_bot t2 then
       bot ()
     else
       (* TODO: Why can I be sure that m1 && m2 are all Some here? *)
       let m1, m2 = Option.get t1.d, Option.get t2.d in
-      if is_top_env t1 then 
-        {d = Some (dim_add (Environment.dimchange t2.env sup_env) m2); env = sup_env} 
-      else if is_top_env t2 then 
+      if is_top_env t1 then
+        {d = Some (dim_add (Environment.dimchange t2.env sup_env) m2); env = sup_env}
+      else if is_top_env t2 then
         {d = Some (dim_add (Environment.dimchange t1.env sup_env) m1); env = sup_env}
       else
         let rref_matr = Matrix.rref_matrix_with (Matrix.copy m1) (Matrix.copy m2) in
-        if Option.is_none rref_matr then 
+        if Option.is_none rref_matr then
           bot ()
         else
           {d = rref_matr; env = sup_env}
@@ -339,12 +345,12 @@ struct
       (* -2:  environments are not compatible (a variable has different types in the 2 environements *)
       (* -1: if env1 is a subset of env2,  (OK)  *)
       (*  0:  if equality,  (OK) *)
-      (* +1: if env1 is a superset of env2, and +2 otherwise (the lce exists and is a strict superset of both) *) 
+      (* +1: if env1 is a superset of env2, and +2 otherwise (the lce exists and is a strict superset of both) *)
       false
-    else if is_bot t1 || is_top_env t2 then 
+    else if is_bot t1 || is_top_env t2 then
       true
-    else if is_bot t2 || is_top_env t1 then 
-      false 
+    else if is_bot t2 || is_top_env t1 then
+      false
     else
       let m1, m2 = Option.get t1.d, Option.get t2.d in
       let m1' = if env_comp = 0 then m1 else dim_add (Environment.dimchange t1.env t2.env) m1 in
@@ -402,9 +408,9 @@ struct
               lin_disjunc new_r (s + 1) new_a new_b
             | _      -> failwith "Matrix not in rref form" end
     in
-    if is_bot a then 
+    if is_bot a then
       b
-    else if is_bot b then 
+    else if is_bot b then
       a
     else
       match Option.get a.d, Option.get b.d with
@@ -437,15 +443,15 @@ struct
 
   let remove_rels_with_var x var env inplace =
     let j0 = Environment.dim_of_var env var in
-    if inplace then 
-      (Matrix.reduce_col_with x j0; x) 
-    else 
+    if inplace then
+      (Matrix.reduce_col_with x j0; x)
+    else
       Matrix.reduce_col x j0
 
   let remove_rels_with_var x var env inplace = timing_wrap "remove_rels_with_var" (remove_rels_with_var x var env) inplace
 
   let forget_vars t vars =
-    if is_bot t || is_top_env t || List.is_empty vars then 
+    if is_bot t || is_top_env t || List.is_empty vars then
       t
     else
       let m = Option.get t.d in
@@ -526,8 +532,8 @@ struct
     let t_primed = add_vars t primed_vars in
     let multi_t = List.fold_left2 (fun t' v_prime (_,v') -> assign_var t' v_prime v') t_primed primed_vars vv's in
     match multi_t.d with
-    | Some m when not @@ is_top_env multi_t -> 
-      let replace_col m x y = 
+    | Some m when not @@ is_top_env multi_t ->
+      let replace_col m x y =
         let dim_x, dim_y = Environment.dim_of_var multi_t.env x, Environment.dim_of_var multi_t.env y in
         let col_x = Matrix.get_col m dim_x in
         Matrix.set_col_with m col_x dim_y
@@ -536,9 +542,9 @@ struct
       let switched_m = List.fold_left2 replace_col m_cp primed_vars assigned_vars in
       let res = drop_vars {d = Some switched_m; env = multi_t.env} primed_vars true in
       let x = Option.get res.d in
-      if Matrix.normalize_with x then 
-        {d = Some x; env = res.env} 
-      else 
+      if Matrix.normalize_with x then
+        {d = Some x; env = res.env}
+      else
         bot ()
     | _ -> t
 
@@ -609,10 +615,10 @@ struct
       (*Flip the sign of the const. val in coeff vec*)
       Vector.mapi_with (fun i x -> if Vector.compare_length_with e (i + 1) = 0 then Mpqf.mone *: x else x) e;
       let res =
-        if is_bot t then 
-          bot () 
+        if is_bot t then
+          bot ()
         else
-          let opt_m = Matrix.rref_vec_with (Matrix.copy @@ Option.get t.d) e in 
+          let opt_m = Matrix.rref_vec_with (Matrix.copy @@ Option.get t.d) e in
           if Option.is_none opt_m then bot () else {d = opt_m; env = t.env}
       in
       meet_tcons_one_var_eq res expr

From 54860e74b4fc96b4d6301621df7c3ac139efe20b Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Dec 2023 12:27:54 +0100
Subject: [PATCH 20/43] Rename `get_c` to more obvious name

---
 src/cdomains/apron/affineEqualityDomain.apron.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index fff6437882..82fe8fe6b6 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -141,7 +141,7 @@ struct
   include ConvenienceOps(Mpqf)
 
   (** Get the constant from the vector if it is a constant *)
-  let get_c v = match Vector.findi ((<>:) Mpqf.zero) v with
+  let to_constant_opt v = match Vector.findi ((<>:) Mpqf.zero) v with
     | exception Not_found -> Some Mpqf.zero
     | i when Vector.compare_length_with v (i + 1) = 0 -> Some (Vector.nth v i)
     | _ -> None
@@ -192,7 +192,7 @@ struct
       | Binop (Mul, e1, e2, _, _) ->
         let v1 = convert_texpr e1 in
         let v2 = convert_texpr e2 in
-        begin match get_c v1, get_c v2 with
+        begin match to_constant_opt v1, to_constant_opt v2 with
           | _, Some c -> Vector.apply_with_c_with ( *:) c v1; v1
           | Some c, _ -> Vector.apply_with_c_with ( *:) c v2; v2
           | _, _ -> raise NotLinear
@@ -214,7 +214,7 @@ struct
   let bound_texpr t texpr =
     let texpr = Texpr1.to_expr texpr in
     match get_coeff_vec t texpr  with
-    | Some v -> begin match get_c v with
+    | Some v -> begin match to_constant_opt v with
         | Some c when Mpqf.get_den c = IntOps.BigIntOps.one ->
           let int_val = Mpqf.get_num c in
           Some int_val, Some int_val
@@ -625,7 +625,7 @@ struct
     in
     match get_coeff_vec t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with
     | Some v ->
-      begin match get_c v, Tcons1.get_typ tcons with
+      begin match to_constant_opt v, Tcons1.get_typ tcons with
         | Some c, DISEQ -> check_const (=:) c
         | Some c, SUP -> check_const (<=:) c
         | Some c, EQ -> check_const (<>:) c

From f0f47987a6eb8f3d7543900610c00ab36375635c Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Dec 2023 12:36:00 +0100
Subject: [PATCH 21/43] Simplify `bound_texpr`

---
 .../apron/affineEqualityDomain.apron.ml       | 20 ++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 82fe8fe6b6..9ccf2294a3 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -213,20 +213,22 @@ struct
 
   let bound_texpr t texpr =
     let texpr = Texpr1.to_expr texpr in
-    match get_coeff_vec t texpr  with
-    | Some v -> begin match to_constant_opt v with
-        | Some c when Mpqf.get_den c = IntOps.BigIntOps.one ->
-          let int_val = Mpqf.get_num c in
-          Some int_val, Some int_val
-        | _ -> None, None end
+    match Option.bind (get_coeff_vec t texpr) to_constant_opt with
+    | Some c when Mpqf.get_den c = IntOps.BigIntOps.one ->
+      let int_val = Mpqf.get_num c in
+      Some int_val, Some int_val
     | _ -> None, None
 
 
   let bound_texpr d texpr1 =
     let res = bound_texpr d texpr1 in
-    match res with
-    | Some min, Some max ->  if M.tracing then M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string min) (IntOps.BigIntOps.to_string max); res
-    | _ -> res
+    (if M.tracing then
+       match res with
+       | Some min, Some max -> M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string min) (IntOps.BigIntOps.to_string max)
+       | _ -> ()
+    );
+    res
+
 
   let bound_texpr d texpr1 = timing_wrap "bounds calculation" (bound_texpr d) texpr1
 end

From 44596eb2c63cb4ddfd2f3e9c86110978a2d5c361 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Dec 2023 12:41:14 +0100
Subject: [PATCH 22/43] Shorten function

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

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 9ccf2294a3..d2c74a82a2 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -528,7 +528,7 @@ struct
     res
 
   let assign_var_parallel t vv's =
-    let assigned_vars = List.map (function (v, _) -> v) vv's in
+    let assigned_vars = List.map fst vv's in
     let t = add_vars t assigned_vars in
     let primed_vars = List.init (List.length assigned_vars) (fun i -> Var.of_string (Int.to_string i  ^"'")) in (* TODO: we use primed vars in analysis, conflict? *)
     let t_primed = add_vars t primed_vars in

From b6b202ed759eb45d5ef02712a60d9685ab864509 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Dec 2023 12:53:42 +0100
Subject: [PATCH 23/43] Some more making things concise

---
 src/cdomains/apron/affineEqualityDomain.apron.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index d2c74a82a2..0bb0e856c3 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -152,7 +152,7 @@ struct
     let open Apron.Texpr1 in
     let exception NotLinear in
     let zero_vec = Vector.zero_vec @@ Environment.size t.env + 1 in
-    let neg v = Vector.map_with (fun x -> Mpqf.mone *: x) v; v in
+    let neg v = Vector.map_with (( *:) Mpqf.mone) v; v in
     let is_const_vec v = Vector.compare_length_with (Vector.filteri (fun i x -> (*Inefficient*)
         Vector.compare_length_with v (i + 1) > 0 && x <>: Mpqf.zero) v) 1 = 0
     in
@@ -250,8 +250,8 @@ struct
       let row = Array.copy @@ Vector.to_array row in
       let mpqf_of_z x = Mpqf.of_mpz @@ Z_mlgmpidl.mpzf_of_z x in
       let lcm = mpqf_of_z @@ Array.fold_left (fun x y -> Z.lcm x (Mpqf.get_den y)) Z.one row in
-      Array.modify (fun x -> x *: lcm) row;
-      let int_arr = Array.map (fun x -> Mpqf.get_num x) row in
+      Array.modify (( *:) lcm) row;
+      let int_arr = Array.map Mpqf.get_num row in
       let div = Array.fold_left Z.gcd int_arr.(0) int_arr in
       Array.modify (fun x -> Z.div x div) int_arr;
       int_arr
@@ -379,12 +379,12 @@ struct
           let col_a, col_b = Vector.keep_vals col_a max, Vector.keep_vals col_b max in
           if Vector.equal col_a col_b then (a, b, max) else
             let a_rev, b_rev = (Vector.rev_with col_a; col_a), (Vector.rev_with col_b; col_b) in
-            let i = Vector.find2i (fun x y -> x <>: y) a_rev b_rev in
+            let i = Vector.find2i (<>:) a_rev b_rev in
             let (x, y) = Vector.nth a_rev i, Vector.nth b_rev i in
             let r, diff = Vector.length a_rev - (i + 1), x -: y  in
             let a_r, b_r = Matrix.get_row a r, Matrix.get_row b r in
             let sub_col =
-              Vector.map2_with (fun x y -> x -: y) a_rev b_rev;
+              Vector.map2_with (-:) a_rev b_rev;
               Vector.rev_with a_rev;
               a_rev
             in
@@ -581,8 +581,8 @@ struct
     forget_vars res [var]
 
   let substitute_exp t var exp ov =
-    let res = substitute_exp t var exp ov
-    in if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %s \n exp: %a \n -> \n %s\n" (show t) (Var.to_string var) d_exp exp (show res);
+    let res = substitute_exp t var exp ov in
+    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %s \n exp: %a \n -> \n %s\n" (show t) (Var.to_string var) d_exp exp (show res);
     res
 
   let substitute_exp t var exp ov = timing_wrap "substitution" (substitute_exp t var exp) ov

From f0870881960a97a7d3afdd0f1b2f253f1c416794 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Dec 2023 13:00:30 +0100
Subject: [PATCH 24/43] Rename var to `coeff`

---
 src/cdomains/apron/affineEqualityDomain.apron.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 0bb0e856c3..5630888b59 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -259,18 +259,18 @@ struct
     let vec_to_constraint arr env =
       let vars, _ = Environment.vars env in
       let dim_to_str var =
-        let vl =  arr.(Environment.dim_of_var env var) in
+        let coeff =  arr.(Environment.dim_of_var env var) in
         let var_str = Var.to_string var in
-        if Z.equal vl Z.zero then
+        if Z.equal coeff Z.zero then
           ""
-        else if Z.equal vl Z.one then
+        else if Z.equal coeff Z.one then
           "+" ^ var_str
-        else if Z.equal vl Z.minus_one then
+        else if Z.equal coeff Z.minus_one then
           "-" ^ var_str
-        else if Z.lt vl Z.minus_one then
-          Z.to_string vl ^ var_str
+        else if Z.lt coeff Z.minus_one then
+          Z.to_string coeff ^ var_str
         else
-          Format.asprintf "+%s" (Z.to_string vl) ^ var_str
+          Format.asprintf "+%s" (Z.to_string coeff) ^ var_str
       in
       let const_to_str vl =
         if Z.equal vl Z.zero then

From 0dcf8ce52ca8bd4992378ba2072a156ef68a415f Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Dec 2023 13:04:50 +0100
Subject: [PATCH 25/43] Make show more concise

---
 .../apron/affineEqualityDomain.apron.ml         | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 5630888b59..7d01130480 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -260,23 +260,22 @@ struct
       let vars, _ = Environment.vars env in
       let dim_to_str var =
         let coeff =  arr.(Environment.dim_of_var env var) in
-        let var_str = Var.to_string var in
         if Z.equal coeff Z.zero then
           ""
-        else if Z.equal coeff Z.one then
-          "+" ^ var_str
-        else if Z.equal coeff Z.minus_one then
-          "-" ^ var_str
-        else if Z.lt coeff Z.minus_one then
-          Z.to_string coeff ^ var_str
         else
-          Format.asprintf "+%s" (Z.to_string coeff) ^ var_str
+          let coeff_str =
+            if Z.equal coeff Z.one then "+"
+            else if Z.equal coeff Z.minus_one then "-"
+            else if Z.lt coeff Z.minus_one then Z.to_string coeff
+            else Format.asprintf "+%s" (Z.to_string coeff)
+          in
+          coeff_str ^ Var.to_string var
       in
       let const_to_str vl =
         if Z.equal vl Z.zero then
           ""
         else
-          let negated = Z.mul vl Z.minus_one in
+          let negated = Z.neg vl in
           if Z.gt negated Z.zero then "+" ^ Z.to_string negated
           else Z.to_string negated
       in

From 399fb8c4c8fc31d91869e4851056ce0be9010b8f Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Dec 2023 13:11:27 +0100
Subject: [PATCH 26/43] Remove code obscuring imperative nature

---
 .../apron/affineEqualityDomain.apron.ml       | 36 ++++++++++---------
 1 file changed, 19 insertions(+), 17 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 7d01130480..2ec5dabf61 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -376,23 +376,25 @@ struct
         let case_three a b col_a col_b max =
           let col_a, col_b = Vector.copy col_a, Vector.copy col_b in
           let col_a, col_b = Vector.keep_vals col_a max, Vector.keep_vals col_b max in
-          if Vector.equal col_a col_b then (a, b, max) else
-            let a_rev, b_rev = (Vector.rev_with col_a; col_a), (Vector.rev_with col_b; col_b) in
-            let i = Vector.find2i (<>:) a_rev b_rev in
-            let (x, y) = Vector.nth a_rev i, Vector.nth b_rev i in
-            let r, diff = Vector.length a_rev - (i + 1), x -: y  in
-            let a_r, b_r = Matrix.get_row a r, Matrix.get_row b r in
-            let sub_col =
-              Vector.map2_with (-:) a_rev b_rev;
-              Vector.rev_with a_rev;
-              a_rev
-            in
-            let multiply_by_t m t =
-              Matrix.map2i_with (fun i' x c -> if i' <= max then (let beta = c /: diff in
-                                                                  Vector.map2_with (fun u j -> u -: (beta *: j)) x t); x) m sub_col;
-              m
-            in
-            Matrix.remove_row (multiply_by_t a a_r) r, Matrix.remove_row (multiply_by_t b b_r) r, (max - 1)
+          if Vector.equal col_a col_b then
+            (a, b, max)
+          else
+            (
+              Vector.rev_with col_a;
+              Vector.rev_with col_b;
+              let i = Vector.find2i (<>:) col_a col_b in
+              let (x, y) = Vector.nth col_a i, Vector.nth col_b i in
+              let r, diff = Vector.length col_a - (i + 1), x -: y  in
+              let a_r, b_r = Matrix.get_row a r, Matrix.get_row b r in
+              Vector.map2_with (-:) col_a col_b;
+              Vector.rev_with col_a;
+              let multiply_by_t m t =
+                Matrix.map2i_with (fun i' x c -> if i' <= max then (let beta = c /: diff in
+                                                                    Vector.map2_with (fun u j -> u -: (beta *: j)) x t); x) m col_a;
+                m
+              in
+              Matrix.remove_row (multiply_by_t a a_r) r, Matrix.remove_row (multiply_by_t b b_r) r, (max - 1)
+            )
         in
         let col_a, col_b = Matrix.get_col a s, Matrix.get_col b s in
         let nth_zero v i =  match Vector.nth v i with

From 63094e0e1fcee316a2cd8b299dd2699e3e27a193 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Dec 2023 13:22:08 +0100
Subject: [PATCH 27/43] Make use of `uncurry`

---
 src/cdomains/vectorMatrix.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/cdomains/vectorMatrix.ml b/src/cdomains/vectorMatrix.ml
index d652145032..1dd684a4c0 100644
--- a/src/cdomains/vectorMatrix.ml
+++ b/src/cdomains/vectorMatrix.ml
@@ -251,12 +251,14 @@ module ArrayVector: AbstractVector =
 
     let nth = Array.get
 
-    let map2i f v1 v2 = let f' i (v'1, v'2) = f i v'1 v'2 in Array.mapi f' (Array.combine v1 v2) (* TODO: iter2i? *)
+    let map2i f v1 v2 =
+      let f' i = uncurry (f i) in
+      Array.mapi f' (Array.combine v1 v2) (* TODO: iter2i? *)
 
     let map2i_with f v1 v2 = Array.iter2i (fun i x y -> v1.(i) <- f i x y) v1 v2
 
-    let find2i f v1 v2 = let f' (v'1, v'2) = f v'1 v'2 in
-      Array.findi f' (Array.combine v1 v2) (* TODO: iter2i? *)
+    let find2i f v1 v2 =
+      Array.findi (uncurry f) (Array.combine v1 v2) (* TODO: iter2i? *)
 
     let to_array v = v
 

From 79b79d841e17fdbd273a458a0c718c78fa11a1c3 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Dec 2023 13:26:30 +0100
Subject: [PATCH 28/43] Simplify `meet_tcons_one_var_eq`

---
 .../apron/affineEqualityDomain.apron.ml       | 25 +++++++++++--------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 2ec5dabf61..e05400e674 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -601,16 +601,21 @@ struct
     | None -> overflow_res res
     | Some v ->
       let ik = Cilfacade.get_ikind v.vtype in
-      match Bounds.bound_texpr res (Convert.texpr1_of_cil_exp res res.env (Lval (Cil.var v)) true) with
-      | Some _, Some _ when not (Cil.isSigned ik) -> raise NotRefinable (* TODO: unsigned w/o bounds handled differently? *)
-      | Some min, Some max ->
-        assert (Z.equal min max); (* other bounds impossible in affeq *)
-        let (min_ik, max_ik) = IntDomain.Size.range ik in
-        if Z.compare min min_ik < 0 || Z.compare max max_ik > 0 then
-          if IntDomain.should_ignore_overflow ik then bot () else raise NotRefinable
-        else res
-      | exception Convert.Unsupported_CilExp _
-      | _, _ -> overflow_res res
+      if not (Cil.isSigned ik) then
+        raise NotRefinable (* TODO: unsigned w/o bounds handled differently? *)
+      else
+        match Bounds.bound_texpr res (Convert.texpr1_of_cil_exp res res.env (Lval (Cil.var v)) true) with
+        | Some min, Some max ->
+          assert (Z.equal min max); (* other bounds impossible in affeq *)
+          let (min_ik, max_ik) = IntDomain.Size.range ik in
+          if Z.compare min min_ik < 0 || Z.compare max max_ik > 0 then
+            if IntDomain.should_ignore_overflow ik then
+              bot ()
+            else
+              raise NotRefinable
+          else res
+        | exception Convert.Unsupported_CilExp _
+        | _ -> overflow_res res
 
   let meet_tcons t tcons expr =
     let check_const cmp c = if cmp c Mpqf.zero then bot_env else t in

From 097156f2bac7560bd92c5d4aba6babbfb6c6c152 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Dec 2023 13:27:51 +0100
Subject: [PATCH 29/43] Replace Z.compare with bespoke functions

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

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index e05400e674..87accda1b4 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -608,7 +608,7 @@ struct
         | Some min, Some max ->
           assert (Z.equal min max); (* other bounds impossible in affeq *)
           let (min_ik, max_ik) = IntDomain.Size.range ik in
-          if Z.compare min min_ik < 0 || Z.compare max max_ik > 0 then
+          if Z.lt min min_ik || Z.gt max max_ik then
             if IntDomain.should_ignore_overflow ik then
               bot ()
             else

From 0c0f3943c1d324e9e509e3edd4493592e17be8de Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Dec 2023 13:40:00 +0100
Subject: [PATCH 30/43] Some reordering & make `get_coeff_vec` more efficient

---
 .../apron/affineEqualityDomain.apron.ml       | 54 ++++++++++---------
 1 file changed, 29 insertions(+), 25 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 87accda1b4..6f6f7c1280 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -152,7 +152,7 @@ struct
     let open Apron.Texpr1 in
     let exception NotLinear in
     let zero_vec = Vector.zero_vec @@ Environment.size t.env + 1 in
-    let neg v = Vector.map_with (( *:) Mpqf.mone) v; v in
+    let neg v = Vector.map_with Mpqf.neg v; v in
     let is_const_vec v = Vector.compare_length_with (Vector.filteri (fun i x -> (*Inefficient*)
         Vector.compare_length_with v (i + 1) > 0 && x <>: Mpqf.zero) v) 1 = 0
     in
@@ -485,7 +485,7 @@ struct
     let assign_invertible_rels x var b env = timing_wrap "assign_invertible" (assign_invertible_rels x var b) env in
     let assign_uninvertible_rel x var b env =
       let b_length = Vector.length b in
-      Vector.mapi_with (fun i z -> if i < b_length - 1 then Mpqf.mone *: z else z) b;
+      Vector.mapi_with (fun i z -> if i < b_length - 1 then Mpqf.neg z else z) b;
       Vector.set_val_with b (Environment.dim_of_var env var) Mpqf.one;
       let opt_m = Matrix.rref_vec_with x b in
       if Option.is_none opt_m then bot () else
@@ -620,8 +620,9 @@ struct
   let meet_tcons t tcons expr =
     let check_const cmp c = if cmp c Mpqf.zero then bot_env else t in
     let meet_vec e =
-      (*Flip the sign of the const. val in coeff vec*)
-      Vector.mapi_with (fun i x -> if Vector.compare_length_with e (i + 1) = 0 then Mpqf.mone *: x else x) e;
+      (* Flip the sign of the const. val in coeff vec *)
+      let coeff = Vector.nth e (Vector.length e - 1) in
+      Vector.set_val_with e (Vector.length e - 1) (Mpqf.neg coeff);
       let res =
         if is_bot t then
           bot ()
@@ -631,27 +632,30 @@ struct
       in
       meet_tcons_one_var_eq res expr
     in
-    match get_coeff_vec t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with
-    | Some v ->
-      begin match to_constant_opt v, Tcons1.get_typ tcons with
-        | Some c, DISEQ -> check_const (=:) c
-        | Some c, SUP -> check_const (<=:) c
-        | Some c, EQ -> check_const (<>:) c
-        | Some c, SUPEQ -> check_const (<:) c
-        | None, DISEQ
-        | None, SUP ->
-          begin match meet_vec v with
-            | exception NotRefinable -> t
-            | res -> if equal res t then bot_env else t
-          end
-        | None, EQ ->
-          begin match meet_vec v with
-            | exception NotRefinable -> t
-            | res -> if is_bot res then bot_env else res
-          end
-        | _, _ -> t
-      end
-    | None -> t
+    try
+      match get_coeff_vec t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with
+      | Some v ->
+        begin match to_constant_opt v, Tcons1.get_typ tcons with
+          | Some c, DISEQ -> check_const (=:) c
+          | Some c, SUP -> check_const (<=:) c
+          | Some c, EQ -> check_const (<>:) c
+          | Some c, SUPEQ -> check_const (<:) c
+          | None, DISEQ
+          | None, SUP ->
+            if equal (meet_vec v) t then
+              bot_env
+            else
+              t
+          | None, EQ ->
+            let res = meet_vec v in
+            if is_bot res then
+              bot_env
+            else
+              res
+          | _ -> t
+        end
+      | None -> t
+    with NotRefinable -> t
 
   let meet_tcons t tcons expr = timing_wrap "meet_tcons" (meet_tcons t tcons) expr
 

From 3422110111c6621a85caac18db9d4412a5a01cd0 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 9 Jan 2024 18:38:02 +0100
Subject: [PATCH 31/43] Rm outdated comment

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

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 6f6f7c1280..ab24515c28 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -602,7 +602,7 @@ struct
     | Some v ->
       let ik = Cilfacade.get_ikind v.vtype in
       if not (Cil.isSigned ik) then
-        raise NotRefinable (* TODO: unsigned w/o bounds handled differently? *)
+        raise NotRefinable
       else
         match Bounds.bound_texpr res (Convert.texpr1_of_cil_exp res res.env (Lval (Cil.var v)) true) with
         | Some min, Some max ->

From 9452d0881aad4d95e8c6b5eda63d3053c34a91af Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 10 Jan 2024 11:45:57 +0200
Subject: [PATCH 32/43] Add unsound minimal conf with no analyses

---
 conf/min-unsound.json | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 conf/min-unsound.json

diff --git a/conf/min-unsound.json b/conf/min-unsound.json
new file mode 100644
index 0000000000..5195909ffb
--- /dev/null
+++ b/conf/min-unsound.json
@@ -0,0 +1,6 @@
+{
+    "ana": {
+        "activated": [
+        ]
+    }
+}
\ No newline at end of file

From 3b0e0c598e47f9e011d1b9a56904708e78ac079a Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 10 Jan 2024 11:48:50 +0200
Subject: [PATCH 33/43] Add Karoliine as a maintainer to relevant files #1315

---
 dune-project        | 2 +-
 goblint.opam        | 1 +
 goblint.opam.locked | 1 +
 3 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/dune-project b/dune-project
index 37e81f4199..de6e955e60 100644
--- a/dune-project
+++ b/dune-project
@@ -16,7 +16,7 @@
 (homepage "https://goblint.in.tum.de")
 (documentation "https://goblint.readthedocs.io/en/latest/")
 (authors "Simmo Saan" "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ) ; same authors as in .zenodo.json and CITATION.cff
-(maintainers "Simmo Saan <simmo.saan@gmail.com>" "Michael Schwarz <michael.schwarz93@gmail.com>")
+(maintainers "Simmo Saan <simmo.saan@gmail.com>" "Michael Schwarz <michael.schwarz93@gmail.com>" "Karoliine Holter")
 (license MIT)
 
 (package
diff --git a/goblint.opam b/goblint.opam
index b5f1f360dc..7a75a1fb45 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -4,6 +4,7 @@ synopsis: "Static analysis framework for C"
 maintainer: [
   "Simmo Saan <simmo.saan@gmail.com>"
   "Michael Schwarz <michael.schwarz93@gmail.com>"
+  "Karoliine Holter"
 ]
 authors: [
   "Simmo Saan"
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 02eac0bb75..b0a1c9ef20 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -5,6 +5,7 @@ synopsis: "Static analysis framework for C"
 maintainer: [
   "Simmo Saan <simmo.saan@gmail.com>"
   "Michael Schwarz <michael.schwarz93@gmail.com>"
+  "Karoliine Holter"
 ]
 authors: [
   "Simmo Saan"

From 910b152226b7f28d20eabdda2c5578c526ceba49 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 10 Jan 2024 13:45:40 +0200
Subject: [PATCH 34/43] Update extension in debugging documentation

---
 docs/developer-guide/debugging.md | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/docs/developer-guide/debugging.md b/docs/developer-guide/debugging.md
index 5c1db12227..d218e1a8b8 100644
--- a/docs/developer-guide/debugging.md
+++ b/docs/developer-guide/debugging.md
@@ -60,14 +60,14 @@ This will create a file called `goblint.byte`.
 ### Debugging Goblint with VS Code
 
 To debug OCaml programs, you can use the command line interface of `ocamldebug` or make use of the Visual Studio Code
-integration provided by `hackwaly.ocamlearlybird`.
+integration provided by `ocamllabs.ocaml-platform`.
 In the following, we describe the steps necessary to set up this VS Code extension to
 debug Goblint.
 
 ### Setting-up Earlybird
 
-Install the [`hackwaly.ocamlearlybird` extension](https://marketplace.visualstudio.com/items?itemName=hackwaly.ocamlearlybird) in your installation of Visual Studio Code.
-To be able to use this extension, you additionally need to install `ocamlearlybird` on the opam switch you use for Goblint.
+Install the [`ocamllabs.ocaml-platform` extension](https://marketplace.visualstudio.com/items?itemName=ocamllabs.ocaml-platform) in your installation of Visual Studio Code.
+To be able to use this extension, you additionally need to install `earlybird` on the opam switch you use for Goblint.
 To do so, run the following command in the `analyzer` directory:
 
 ```console
@@ -76,7 +76,7 @@ opam install earlybird
 
 ### Providing a Launch Configuration
 
-To let the `hackwaly.ocamlearlybird` extension know which executable it should debug, and which arguments it should pass, we have to provide a configuration file.
+To let the `ocamllabs.ocaml-platform` extension know which executable it should debug, and which arguments it should pass, we have to provide a configuration file.
 The configuration file has to be named `launch.json` and must reside in the `./.vscode` directory. Here is an example `launch.json`:
 
 ```JSON
@@ -92,6 +92,9 @@ The configuration file has to be named `launch.json` and must reside in the `./.
           "tests/regression/00-sanity/01-assert.c",
           "--enable", "ana.int.interval",
         ],
+        "env": {
+          "LD_LIBRARY_PATH": "$LD_LIBRARY_PATH:_build/default/src/common"
+        },
         "stopOnEntry": false,
       }
     ]

From 0af26b4f34007736996b7e5913942d769cc801a7 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 11 Jan 2024 12:05:07 +0200
Subject: [PATCH 35/43] Add group location to messaging docs

---
 docs/developer-guide/messaging.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/docs/developer-guide/messaging.md b/docs/developer-guide/messaging.md
index 0028d51f87..91fba82b51 100644
--- a/docs/developer-guide/messaging.md
+++ b/docs/developer-guide/messaging.md
@@ -18,7 +18,8 @@ A message consists of the following:
         3. **Context.** Optional. Currently completely abstract, so not very useful.
     * **Group.** For messages related to numerous locations with different texts. Contains the following:
         1. **Group text.** An overall description of the group message.
-        2. **Pieces.** A list of single messages as described above.
+        2. **Group location.** Optional. An overall location of the group message.
+        3. **Pieces.** A list of single messages as described above.
 
 ## Creating
 

From abd1cb6c9834db675e5c5ecbdfa752088f1ad181 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 10 Jan 2024 17:41:22 +0200
Subject: [PATCH 36/43] Add test for local var escaping when assigned to global
 through identity function

---
 .../45-escape/09-id-local-in-global.c         | 25 +++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 tests/regression/45-escape/09-id-local-in-global.c

diff --git a/tests/regression/45-escape/09-id-local-in-global.c b/tests/regression/45-escape/09-id-local-in-global.c
new file mode 100644
index 0000000000..aa5a12c012
--- /dev/null
+++ b/tests/regression/45-escape/09-id-local-in-global.c
@@ -0,0 +1,25 @@
+#include <pthread.h>
+#include <goblint.h>
+
+int* gptr;
+
+void *foo(void* p){
+    *gptr = 17;
+    return NULL;
+}
+
+int* id(int* x) {
+    return x;
+}
+
+int main(){
+    int x = 0;
+    gptr = id(&x);
+    __goblint_check(x==0);
+    pthread_t thread;
+    pthread_create(&thread, NULL, foo, NULL);
+    sleep(3);
+    __goblint_check(x == 0); // UNKNOWN!
+    pthread_join(thread, NULL);
+    return 0;
+}

From 063812189dbe12731aacb551230b65fc27908cd8 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 11 Jan 2024 12:34:46 +0200
Subject: [PATCH 37/43] Move return functions from base to returnUtil

---
 src/analyses/base.ml   | 10 +---------
 src/analyses/region.ml |  8 +++-----
 src/util/returnUtil.ml |  9 +++++++++
 3 files changed, 13 insertions(+), 14 deletions(-)
 create mode 100644 src/util/returnUtil.ml

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index c470bca026..fb2b5af517 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -6,6 +6,7 @@ open Pretty
 open Analyses
 open GobConfig
 open BaseUtil
+open ReturnUtil
 module A = Analyses
 module H = Hashtbl
 module Q = Queries
@@ -143,13 +144,6 @@ struct
    * Initializing my variables
    **************************************************************************)
 
-  let return_varstore = ref dummyFunDec.svar
-  let return_varinfo () = !return_varstore
-  let return_var () = AD.of_var (return_varinfo ())
-  let return_lval (): lval = (Var (return_varinfo ()), NoOffset)
-
-  let longjmp_return = ref dummyFunDec.svar
-
   let heap_var on_stack ctx =
     let info = match (ctx.ask (Q.AllocVar {on_stack})) with
       | `Lifted vinfo -> vinfo
@@ -2930,8 +2924,6 @@ end
 module type MainSpec = sig
   include MCPSpec
   include BaseDomain.ExpEvaluator
-  val return_lval: unit -> Cil.lval
-  val return_varinfo: unit -> Cil.varinfo
 end
 
 let main_module: (module MainSpec) Lazy.t =
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 5b10586aba..a6ffa54ed6 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -109,8 +109,7 @@ struct
       let old_regpart = ctx.global () in
       let regpart, reg = match exp with
         | Some exp ->
-          let module BS = (val Base.get_main ()) in
-          Reg.assign (BS.return_lval ()) exp (old_regpart, reg)
+          Reg.assign (ReturnUtil.return_lval ()) exp (old_regpart, reg)
         | None -> (old_regpart, reg)
       in
       let regpart, reg = Reg.kill_vars locals (Reg.remove_vars locals (regpart, reg)) in
@@ -143,12 +142,11 @@ struct
     match au with
     | `Lifted reg -> begin
       let old_regpart = ctx.global () in
-      let module BS = (val Base.get_main ()) in
       let regpart, reg = match lval with
         | None -> (old_regpart, reg)
-        | Some lval -> Reg.assign lval (AddrOf (BS.return_lval ())) (old_regpart, reg)
+        | Some lval -> Reg.assign lval (AddrOf (ReturnUtil.return_lval ())) (old_regpart, reg)
       in
-      let regpart, reg = Reg.remove_vars [BS.return_varinfo ()] (regpart, reg) in
+      let regpart, reg = Reg.remove_vars [ReturnUtil.return_varinfo ()] (regpart, reg) in
       if not (RegPart.leq regpart old_regpart) then
         ctx.sideg () regpart;
       `Lifted reg
diff --git a/src/util/returnUtil.ml b/src/util/returnUtil.ml
new file mode 100644
index 0000000000..a97f538970
--- /dev/null
+++ b/src/util/returnUtil.ml
@@ -0,0 +1,9 @@
+open GoblintCil
+module AD = ValueDomain.AD
+
+let return_varstore = ref dummyFunDec.svar
+let return_varinfo () = !return_varstore
+let return_var () = AD.of_var (return_varinfo ())
+let return_lval (): lval = (Var (return_varinfo ()), NoOffset)
+
+let longjmp_return = ref dummyFunDec.svar
\ No newline at end of file

From 094a52b57a0ddcbd374eab0f0b5f9a27a4cfbd3c Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 11 Jan 2024 12:35:46 +0200
Subject: [PATCH 38/43] Add ask as parameter for excape_rval

---
 src/analyses/threadEscape.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 21a8b69c93..2be4055bbc 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -117,8 +117,7 @@ struct
       end
     | _ -> Queries.Result.top q
 
-  let escape_rval ctx (rval:exp) =
-    let ask = Analyses.ask_of_ctx ctx in
+  let escape_rval ctx ask (rval:exp) =
     let escaped = reachable ask rval in
     let escaped = D.filter (fun v -> not v.vglob) escaped in
 
@@ -133,7 +132,7 @@ struct
     let ask = Analyses.ask_of_ctx ctx in
     let vs = mpt ask (AddrOf lval) in
     if D.exists (fun v -> v.vglob || has_escaped ask v) vs then (
-      let escaped = escape_rval ctx rval in
+      let escaped = escape_rval ctx (Analyses.ask_of_ctx ctx) rval in
       D.join ctx.local escaped
     ) else begin
       ctx.local
@@ -143,7 +142,7 @@ struct
     let desc = LibraryFunctions.find f in
     match desc.special args, f.vname, args with
     | _, "pthread_setspecific" , [key; pt_value] ->
-      let escaped = escape_rval ctx pt_value in
+      let escaped = escape_rval ctx (Analyses.ask_of_ctx ctx) pt_value in
       D.join ctx.local escaped
     | _ -> ctx.local
 

From d39e600a0229f1bda2acf946ed451a98bab55147 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 11 Jan 2024 12:36:40 +0200
Subject: [PATCH 39/43] Implement combine_assign in threadEscape

---
 src/analyses/threadEscape.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 2be4055bbc..3aad5ea5cf 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -138,6 +138,15 @@ struct
       ctx.local
     end
 
+  let combine_assign ctx (lval:lval option) (fexp:exp) f args fc au f_ask : D.t =
+    let ask = Analyses.ask_of_ctx ctx in
+    match lval with
+    | Some lval when D.exists (fun v -> v.vglob || has_escaped ask v) (mpt ask (AddrOf lval)) ->
+      let rval = Lval (ReturnUtil.return_lval ()) in
+      let escaped = escape_rval ctx f_ask rval in
+      D.join ctx.local escaped
+    | _ -> ctx.local
+
   let special ctx (lval: lval option) (f:varinfo) (args:exp list) : D.t =
     let desc = LibraryFunctions.find f in
     match desc.special args, f.vname, args with

From d719842cea889874eb5fc18cf1a31da719a63736 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <44437975+karoliineh@users.noreply.github.com>
Date: Thu, 11 Jan 2024 12:44:25 +0200
Subject: [PATCH 40/43] Use ask variable instead of Analyses.ask_of_ctx ctx

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

diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 3aad5ea5cf..376666c611 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -132,7 +132,7 @@ struct
     let ask = Analyses.ask_of_ctx ctx in
     let vs = mpt ask (AddrOf lval) in
     if D.exists (fun v -> v.vglob || has_escaped ask v) vs then (
-      let escaped = escape_rval ctx (Analyses.ask_of_ctx ctx) rval in
+      let escaped = escape_rval ctx ask rval in
       D.join ctx.local escaped
     ) else begin
       ctx.local

From 34d30fe73cd3c50993cc07aec006e724e3d0f6e7 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 11 Jan 2024 13:51:39 +0200
Subject: [PATCH 41/43] Add comment about f_ask in combine_assign

---
 src/analyses/threadEscape.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 376666c611..f5ff3dc50a 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -143,7 +143,7 @@ struct
     match lval with
     | Some lval when D.exists (fun v -> v.vglob || has_escaped ask v) (mpt ask (AddrOf lval)) ->
       let rval = Lval (ReturnUtil.return_lval ()) in
-      let escaped = escape_rval ctx f_ask rval in
+      let escaped = escape_rval ctx f_ask rval in (* Using f_ask because the return value is only accessible in the context of that function at this point *)
       D.join ctx.local escaped
     | _ -> ctx.local
 

From e847c8f39e2fce8de7f4826fae8b783397cea081 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 11 Jan 2024 15:46:00 +0200
Subject: [PATCH 42/43] Document ReturnUtil

---
 src/goblint_lib.ml     | 1 +
 src/util/returnUtil.ml | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 1bc70f3f52..06c51b0c15 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -402,6 +402,7 @@ module LibraryFunctions = LibraryFunctions
 module BaseUtil = BaseUtil
 module PrecisionUtil = PrecisionUtil
 module ContextUtil = ContextUtil
+module ReturnUtil = ReturnUtil
 module BaseInvariant = BaseInvariant
 module CommonPriv = CommonPriv
 module WideningThresholds = WideningThresholds
diff --git a/src/util/returnUtil.ml b/src/util/returnUtil.ml
index a97f538970..d80ab48ee4 100644
--- a/src/util/returnUtil.ml
+++ b/src/util/returnUtil.ml
@@ -1,3 +1,5 @@
+(** Special variable for return value. *)
+
 open GoblintCil
 module AD = ValueDomain.AD
 

From 69f28b2682b4f070db90918da550a6dbb237ad25 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 11 Jan 2024 15:46:50 +0200
Subject: [PATCH 43/43] Fix goblint-lib-modules.py output

---
 scripts/goblint-lib-modules.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py
index 8ae3b4b3eb..fc6d33b421 100755
--- a/scripts/goblint-lib-modules.py
+++ b/scripts/goblint-lib-modules.py
@@ -65,5 +65,5 @@
 
 missing_modules = src_modules - goblint_lib_modules
 if len(missing_modules) > 0:
-    print(f"Modules missing from {goblint_lib_path}: {missing_modules}")
+    print(f"Modules missing from {goblint_lib_paths[0]}: {missing_modules}")
     sys.exit(1)