From 357becaf142e6c2a830a996b9a23740c40479afc Mon Sep 17 00:00:00 2001
From: Karl Vaartnou <vaartnoukarl@gmail.com>
Date: Sat, 3 Jan 2026 23:52:41 +0200
Subject: [PATCH 01/11] Add graph coloring algorithms

---
 dune-project                  |   1 +
 goblint.opam                  |   1 +
 src/domains/accessColoring.ml | 213 ++++++++++++++++++++++++++++++++++
 src/dune                      |   2 +-
 4 files changed, 216 insertions(+), 1 deletion(-)
 create mode 100644 src/domains/accessColoring.ml

diff --git a/dune-project b/dune-project
index 29a3f85309..a7dba96549 100644
--- a/dune-project
+++ b/dune-project
@@ -41,6 +41,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     (goblint-cil (>= 2.1.0)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
     (batteries (>= 3.9.0))
     (patricia-tree (>= 0.14.0))
+    ocamlgraph
     (zarith (>= 1.12))
     (yojson (and (>= 2.0.0) (< 3))) ; json-data-encoding has incompatible yojson representation for yojson 3
     (qcheck-core (>= 0.90))
diff --git a/goblint.opam b/goblint.opam
index b89de32bc8..a44613bbe9 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -42,6 +42,7 @@ depends: [
   "goblint-cil" {>= "2.1.0"}
   "batteries" {>= "3.9.0"}
   "patricia-tree" {>= "0.14.0"}
+  "ocamlgraph"
   "zarith" {>= "1.12"}
   "yojson" {>= "2.0.0" & < "3"}
   "qcheck-core" {>= "0.90"}
diff --git a/src/domains/accessColoring.ml b/src/domains/accessColoring.ml
new file mode 100644
index 0000000000..cb84fa133a
--- /dev/null
+++ b/src/domains/accessColoring.ml
@@ -0,0 +1,213 @@
+module Make (G : Graph.Coloring.G) = struct
+  module C = Graph.Coloring.Make (G)
+  module IntSet = Set.Make (Int)
+
+  type coloring = int C.H.t
+
+  module type ALGORITHM = sig
+    val color : G.t -> coloring
+  end
+
+  let k_color g k = C.coloring g k
+  let color_with (module A : ALGORITHM) g = A.color g
+  let color_of coloring v = C.H.find_opt coloring v
+  let colors_used coloring = C.H.fold (fun _ c acc -> max acc c) coloring 0
+
+  module Greedy : ALGORITHM = struct
+    let color g =
+      let n = G.nb_vertex g in
+      let coloring = C.H.create n in
+      let vertices =
+        G.fold_vertex (fun v acc -> (G.out_degree g v, v) :: acc) g []
+        |> List.sort (fun (d1, _) (d2, _) -> compare d2 d1)
+        |> List.map snd
+      in
+      let next_color v =
+        let used = ref IntSet.empty in
+        G.iter_succ (fun u ->
+            match C.H.find_opt coloring u with
+            | None -> ()
+            | Some c -> used := IntSet.add c !used
+          ) g v;
+        let rec pick c =
+          if IntSet.mem c !used then
+            pick (c + 1)
+          else
+            c
+        in
+        pick 1
+      in
+      List.iter (fun v -> C.H.add coloring v (next_color v)) vertices;
+      coloring
+  end
+
+  module Optimal : ALGORITHM = struct
+    let color g =
+      let max_colors = max 1 (G.nb_vertex g) in
+      let rec loop k =
+        if k > max_colors then
+          raise Graph.Coloring.NoColoring
+        else
+          try C.coloring g k with
+          | Graph.Coloring.NoColoring -> loop (k + 1)
+      in
+      loop 1
+  end
+
+  module Dsatur : ALGORITHM = struct
+    let color g =
+      let n = G.nb_vertex g in
+      let coloring = C.H.create n in
+      let saturation = C.H.create n in
+      let degree = C.H.create n in
+      G.iter_vertex (fun v ->
+          C.H.replace saturation v IntSet.empty;
+          C.H.replace degree v (G.out_degree g v)
+        ) g;
+      let is_colored v = C.H.mem coloring v in
+      let sat_count v =
+        match C.H.find_opt saturation v with
+        | None -> 0
+        | Some s -> IntSet.cardinal s
+      in
+      let choose_vertex () =
+        let pick v best_opt =
+          if is_colored v then
+            best_opt
+          else
+            match best_opt with
+            | None -> Some v
+            | Some best ->
+              let sv = sat_count v in
+              let sb = sat_count best in
+              if sv > sb then
+                Some v
+              else if sv < sb then
+                Some best
+              else (
+                let dv = C.H.find degree v in
+                let db = C.H.find degree best in
+                if dv > db then Some v else Some best
+              )
+        in
+        G.fold_vertex pick g None
+      in
+      let pick_color v =
+        let used =
+          match C.H.find_opt saturation v with
+          | None -> IntSet.empty
+          | Some s -> s
+        in
+        let rec pick c =
+          if IntSet.mem c used then
+            pick (c + 1)
+          else
+            c
+        in
+        pick 1
+      in
+      let rec loop () =
+        match choose_vertex () with
+        | None -> ()
+        | Some v ->
+          let c = pick_color v in
+          C.H.add coloring v c;
+          G.iter_succ (fun u ->
+              if not (is_colored u) then
+                let s =
+                  match C.H.find_opt saturation u with
+                  | None -> IntSet.empty
+                  | Some s -> s
+                in
+                C.H.replace saturation u (IntSet.add c s)
+            ) g v;
+          loop ()
+      in
+      loop ();
+      coloring
+  end
+
+  module Rlf : ALGORITHM = struct
+    module VSet = struct
+      let create n = C.H.create n
+      let mem s v = C.H.mem s v
+      let add s v = C.H.replace s v ()
+      let remove s v = C.H.remove s v
+    end
+
+    let color g =
+      let n = G.nb_vertex g in
+      let coloring = C.H.create n in
+      let uncolored = VSet.create n in
+      G.iter_vertex (fun v -> VSet.add uncolored v) g;
+      let degree v = G.out_degree g v in
+      let pick_start () =
+        G.fold_vertex (fun v best ->
+            if not (VSet.mem uncolored v) then
+              best
+            else
+              match best with
+              | None -> Some v
+              | Some b ->
+                if degree v > degree b then Some v else Some b
+          ) g None
+      in
+      let add_forbidden forbidden v =
+        G.iter_succ (fun u ->
+            if VSet.mem uncolored u then
+              VSet.add forbidden u
+          ) g v
+      in
+      let candidate_score forbidden v =
+        let count = ref 0 in
+        G.iter_succ (fun u ->
+            if VSet.mem forbidden u then
+              incr count
+          ) g v;
+        !count
+      in
+      let pick_candidate forbidden =
+        G.fold_vertex (fun v best ->
+            if not (VSet.mem uncolored v) || VSet.mem forbidden v then
+              best
+            else
+              match best with
+              | None -> Some v
+              | Some b ->
+                let sv = candidate_score forbidden v in
+                let sb = candidate_score forbidden b in
+                if sv > sb then
+                  Some v
+                else if sv < sb then
+                  Some b
+                else if degree v > degree b then
+                  Some v
+                else
+                  Some b
+          ) g None
+      in
+      let rec color_class color =
+        match pick_start () with
+        | None -> ()
+        | Some v0 ->
+          let forbidden = VSet.create n in
+          let add_vertex v =
+            C.H.add coloring v color;
+            VSet.remove uncolored v;
+            add_forbidden forbidden v
+          in
+          add_vertex v0;
+          let rec fill () =
+            match pick_candidate forbidden with
+            | None -> ()
+            | Some v ->
+              add_vertex v;
+              fill ()
+          in
+          fill ();
+          color_class (color + 1)
+      in
+      color_class 1;
+      coloring
+  end
+end
diff --git a/src/dune b/src/dune
index deba41c852..f86673111b 100644
--- a/src/dune
+++ b/src/dune
@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint goblint_memtrace privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs domain_shims
+  (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common ocamlgraph goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs domain_shims
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/reference/library-dependencies.html#alternative-dependencies

From eb9e9d8dba3101e11a044ea2a7b16d2fc435eda0 Mon Sep 17 00:00:00 2001
From: Karl Vaartnou <vaartnoukarl@gmail.com>
Date: Sat, 3 Jan 2026 23:52:08 +0200
Subject: [PATCH 02/11] Add race graph coloring

---
 src/config/options.schema.json |  7 +++
 src/domains/access.ml          | 79 ++++++++++++++++++++++++++++++++--
 2 files changed, 82 insertions(+), 4 deletions(-)

diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index f30a37484c..473ae0a3be 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -2463,6 +2463,13 @@
           "type": "integer",
           "default": 0
         },
+        "race-coloring": {
+          "title": "warn.race-coloring",
+          "description": "Group race warnings by graph coloring (none, greedy, dsatur, rlf, optimal).",
+          "type": "string",
+          "enum": ["none", "greedy", "dsatur", "rlf", "optimal"],
+          "default": "none"
+        },
         "deterministic": {
           "title": "warn.deterministic",
           "description": "Output messages in deterministic order. Useful for cram testing.",
diff --git a/src/domains/access.ml b/src/domains/access.ml
index 823e1cd589..47178a46ec 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -484,6 +484,39 @@ struct
       AS.pretty w.node AS.pretty w.prefix AS.pretty w.type_suffix AS.pretty w.type_suffix_prefix
 end
 
+module InterferenceGraph = struct
+  module Vertex = struct
+    type t = A.t
+
+    let compare = A.compare
+    let hash = A.hash
+    let equal = A.equal
+  end
+
+  module G = Graph.Imperative.Graph.Concrete (Vertex)
+
+  type t = G.t
+
+  let of_warn_accs (warn_accs : WarnAccs.t) =
+    let graph = G.create () in
+    let all = WarnAccs.union_all warn_accs in
+    AS.iter (fun acc -> G.add_vertex graph acc) all;
+    let accs = AS.elements all in
+    let rec loop = function
+      | [] -> ()
+      | a :: rest ->
+        List.iter (fun b ->
+            if may_race a b then
+              G.add_edge graph a b
+          ) rest;
+        loop rest
+    in
+    loop accs;
+    graph
+
+  module Coloring = AccessColoring.Make (G)
+end
+
 let group_may_race (warn_accs:WarnAccs.t) =
   if M.tracing then M.tracei "access" "group_may_race %a" WarnAccs.pretty warn_accs;
   (* BFS to traverse one component with may_race edges *)
@@ -594,7 +627,7 @@ let incr_summary ~safe ~vulnerable ~unsafe grouped_accs =
   | Some n when n >= 100 -> is_all_safe := false; incr unsafe
   | Some n -> is_all_safe := false; incr vulnerable
 
-let print_accesses memo grouped_accs =
+let print_accesses ?coloring memo grouped_accs =
   let allglobs = get_bool "allglobs" in
   let race_threshold = get_int "warn.race-threshold" in
   let msgs race_accs =
@@ -602,8 +635,29 @@ let print_accesses memo grouped_accs =
       let doc = dprintf "%a with %a (conf. %d)  (exp: %a)" AccessKind.pretty kind MCPAccess.A.pretty acc conf d_exp exp in
       (doc, Some (Messages.Location.Node node))
     in
-    AS.elements race_accs
-    |> List.map h
+    match coloring with
+    | None ->
+      AS.elements race_accs
+      |> List.map h
+    | Some coloring ->
+      let module IntMap = Map.Make (Int) in
+      let module C = InterferenceGraph.Coloring in
+      let add_to_map acc map =
+        match C.color_of coloring acc with
+        | None -> map
+        | Some c ->
+          IntMap.update c (function
+              | None -> Some [acc]
+              | Some accs -> Some (acc :: accs)
+            ) map
+      in
+      let color_map = AS.fold add_to_map race_accs IntMap.empty in
+      IntMap.bindings color_map
+      |> List.concat_map (fun (color, accs) ->
+          let header = (dprintf "Color %d" color, None) in
+          let acc_msgs = accs |> List.rev |> List.map h in
+          header :: acc_msgs
+        )
   in
   let group_loc = match memo with
     | (`Var v, _) -> Some (M.Location.CilLocation v.vdecl) (* TODO: offset location *)
@@ -630,6 +684,23 @@ let print_accesses memo grouped_accs =
     )
 
 let warn_global ~safe ~vulnerable ~unsafe warn_accs memo =
+  let coloring =
+    match get_string "warn.race-coloring" with
+    | "" | "none" -> None
+    | "greedy" ->
+      let graph = InterferenceGraph.of_warn_accs warn_accs in
+      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Greedy) graph)
+    | "dsatur" ->
+      let graph = InterferenceGraph.of_warn_accs warn_accs in
+      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Dsatur) graph)
+    | "rlf" ->
+      let graph = InterferenceGraph.of_warn_accs warn_accs in
+      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Rlf) graph)
+    | "optimal" ->
+      let graph = InterferenceGraph.of_warn_accs warn_accs in
+      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Optimal) graph)
+    | _ -> None
+  in
   let grouped_accs = group_may_race warn_accs in (* do expensive component finding only once *)
   incr_summary ~safe ~vulnerable ~unsafe grouped_accs;
-  print_accesses memo grouped_accs
+  print_accesses ?coloring memo grouped_accs

From d48f2c2726cebd2d1a8274bb58db600125fbf3a1 Mon Sep 17 00:00:00 2001
From: Karl Vaartnou <vaartnoukarl@gmail.com>
Date: Mon, 5 Jan 2026 16:38:51 +0200
Subject: [PATCH 03/11] Make race coloring per component

---
 src/domains/access.ml | 57 ++++++++++++++++++++++++++++++-------------
 1 file changed, 40 insertions(+), 17 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index 47178a46ec..2c3f2bd9dd 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -515,6 +515,22 @@ module InterferenceGraph = struct
     graph
 
   module Coloring = AccessColoring.Make (G)
+
+  let of_accesses (accs : AS.t) =
+    let graph = G.create () in
+    AS.iter (fun acc -> G.add_vertex graph acc) accs;
+    let accs_list = AS.elements accs in
+    let rec loop = function
+      | [] -> ()
+      | a :: rest ->
+        List.iter (fun b ->
+            if may_race a b then
+              G.add_edge graph a b
+          ) rest;
+        loop rest
+    in
+    loop accs_list;
+    graph
 end
 
 let group_may_race (warn_accs:WarnAccs.t) =
@@ -627,10 +643,27 @@ let incr_summary ~safe ~vulnerable ~unsafe grouped_accs =
   | Some n when n >= 100 -> is_all_safe := false; incr unsafe
   | Some n -> is_all_safe := false; incr vulnerable
 
-let print_accesses ?coloring memo grouped_accs =
+let print_accesses ?coloring_mode memo grouped_accs =
   let allglobs = get_bool "allglobs" in
   let race_threshold = get_int "warn.race-threshold" in
-  let msgs race_accs =
+  let coloring_for accs =
+    match coloring_mode with
+    | None -> None
+    | Some "greedy" ->
+      let graph = InterferenceGraph.of_accesses accs in
+      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Greedy) graph)
+    | Some "dsatur" ->
+      let graph = InterferenceGraph.of_accesses accs in
+      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Dsatur) graph)
+    | Some "rlf" ->
+      let graph = InterferenceGraph.of_accesses accs in
+      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Rlf) graph)
+    | Some "optimal" ->
+      let graph = InterferenceGraph.of_accesses accs in
+      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Optimal) graph)
+    | Some _ -> None
+  in
+  let msgs ?coloring race_accs =
     let h A.{conf; kind; node; exp; acc} =
       let doc = dprintf "%a with %a (conf. %d)  (exp: %a)" AccessKind.pretty kind MCPAccess.A.pretty acc conf d_exp exp in
       (doc, Some (Messages.Location.Node node))
@@ -675,7 +708,8 @@ let print_accesses ?coloring memo grouped_accs =
           else
             Info
         in
-        M.msg_group severity ?loc:group_loc ~category:Race "Memory location %a (race with conf. %d)" Memo.pretty memo conf (msgs accs);
+        let coloring = coloring_for accs in
+        M.msg_group severity ?loc:group_loc ~category:Race "Memory location %a (race with conf. %d)" Memo.pretty memo conf (msgs ?coloring accs);
         safe_accs
     ) (AS.empty ())
   |> (fun safe_accs ->
@@ -684,23 +718,12 @@ let print_accesses ?coloring memo grouped_accs =
     )
 
 let warn_global ~safe ~vulnerable ~unsafe warn_accs memo =
-  let coloring =
+  let coloring_mode =
     match get_string "warn.race-coloring" with
     | "" | "none" -> None
-    | "greedy" ->
-      let graph = InterferenceGraph.of_warn_accs warn_accs in
-      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Greedy) graph)
-    | "dsatur" ->
-      let graph = InterferenceGraph.of_warn_accs warn_accs in
-      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Dsatur) graph)
-    | "rlf" ->
-      let graph = InterferenceGraph.of_warn_accs warn_accs in
-      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Rlf) graph)
-    | "optimal" ->
-      let graph = InterferenceGraph.of_warn_accs warn_accs in
-      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Optimal) graph)
+    | "greedy" | "dsatur" | "rlf" | "optimal" as mode -> Some mode
     | _ -> None
   in
   let grouped_accs = group_may_race warn_accs in (* do expensive component finding only once *)
   incr_summary ~safe ~vulnerable ~unsafe grouped_accs;
-  print_accesses ?coloring memo grouped_accs
+  print_accesses ?coloring_mode memo grouped_accs

From 2ca1b6d8afddb5e24a2daa6d0a3000040a5053e1 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 22 Jul 2026 14:02:12 +0300
Subject: [PATCH 04/11] Add ocamlgraph to locked dependencies

---
 goblint.opam.locked | 1 +
 1 file changed, 1 insertion(+)

diff --git a/goblint.opam.locked b/goblint.opam.locked
index ad97ddd842..1ad7062bce 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -93,6 +93,7 @@ depends: [
   "ocamlc-loc" {= "3.21.1" & with-dev-setup}
   "ocamlfind" {= "1.9.8"}
   "ocamlformat-rpc-lib" {= "0.29.0" & with-dev-setup}
+  "ocamlgraph" {= "2.2.0"}
   "ocp-indent" {= "1.8.1" & with-dev-setup}
   "odoc" {= "3.0.0" & with-doc}
   "odoc-parser" {= "3.0.0" & with-doc}

From 7706507aa91290383091214a78b82c72c7624a70 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 22 Jul 2026 14:05:53 +0300
Subject: [PATCH 05/11] Inline Access.InterferenceGraph.Vertex

---
 src/domains/access.ml | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index 2c3f2bd9dd..fd06c7890a 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -485,15 +485,8 @@ struct
 end
 
 module InterferenceGraph = struct
-  module Vertex = struct
-    type t = A.t
 
-    let compare = A.compare
-    let hash = A.hash
-    let equal = A.equal
-  end
-
-  module G = Graph.Imperative.Graph.Concrete (Vertex)
+  module G = Graph.Imperative.Graph.Concrete (A)
 
   type t = G.t
 

From 6d33962c6da86b91f90e2f0ad906aa9b4ce7054e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 22 Jul 2026 14:25:42 +0300
Subject: [PATCH 06/11] Extract goblint.ocamlgraph library

---
 scripts/goblint-lib-modules.py                            | 2 ++
 src/domains/access.ml                                     | 2 +-
 src/dune                                                  | 2 +-
 src/index.mld                                             | 3 +++
 .../accessColoring.ml => util/ocamlgraph/coloring.ml}     | 0
 src/util/ocamlgraph/dune                                  | 8 ++++++++
 src/util/ocamlgraph/goblint_ocamlgraph.ml                 | 3 +++
 7 files changed, 18 insertions(+), 2 deletions(-)
 rename src/{domains/accessColoring.ml => util/ocamlgraph/coloring.ml} (100%)
 create mode 100644 src/util/ocamlgraph/dune
 create mode 100644 src/util/ocamlgraph/goblint_ocamlgraph.ml

diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py
index a23888aea8..89cfe808f7 100755
--- a/scripts/goblint-lib-modules.py
+++ b/scripts/goblint-lib-modules.py
@@ -12,6 +12,7 @@
     src_root_path / "util" / "parallel" / "goblint_parallel.ml",
     src_root_path / "solver" / "goblint_solver.ml",
     src_root_path / "util" / "std" / "goblint_std.ml",
+    src_root_path / "util" / "ocamlgraph" / "goblint_ocamlgraph.ml",
 ]
 goblint_lib_modules = set()
 
@@ -39,6 +40,7 @@
 
     # libraries
     "Goblint_std",
+    "Goblint_ocamlgraph",
     "Goblint_constraint",
     "Goblint_parallel",
     "Goblint_solver",
diff --git a/src/domains/access.ml b/src/domains/access.ml
index fd06c7890a..5755df0496 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -507,7 +507,7 @@ module InterferenceGraph = struct
     loop accs;
     graph
 
-  module Coloring = AccessColoring.Make (G)
+  module Coloring = Goblint_ocamlgraph.Coloring.Make (G)
 
   let of_accesses (accs : AS.t) =
     let graph = G.create () in
diff --git a/src/dune b/src/dune
index f86673111b..c9dca091a9 100644
--- a/src/dune
+++ b/src/dune
@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint goblint_memtrace privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common ocamlgraph goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs domain_shims
+  (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common ocamlgraph goblint_ocamlgraph goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs domain_shims
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/reference/library-dependencies.html#alternative-dependencies
diff --git a/src/index.mld b/src/index.mld
index 906eb3ab13..2332dde5e1 100644
--- a/src/index.mld
+++ b/src/index.mld
@@ -40,6 +40,9 @@ The following libraries provide extensions to other OCaml libraries.
 {2 Library goblint.std}
 {!modules:Goblint_std}
 
+{2 Library goblint.ocamlgraph}
+{!modules:Goblint_ocamlgraph}
+
 
 {1 Package utilities}
 The following libraries provide [goblint] package metadata for executables.
diff --git a/src/domains/accessColoring.ml b/src/util/ocamlgraph/coloring.ml
similarity index 100%
rename from src/domains/accessColoring.ml
rename to src/util/ocamlgraph/coloring.ml
diff --git a/src/util/ocamlgraph/dune b/src/util/ocamlgraph/dune
new file mode 100644
index 0000000000..1632ad067d
--- /dev/null
+++ b/src/util/ocamlgraph/dune
@@ -0,0 +1,8 @@
+(include_subdirs no)
+
+(library
+ (name goblint_ocamlgraph)
+ (public_name goblint.ocamlgraph)
+ (libraries
+   ocamlgraph)
+ (instrumentation (backend bisect_ppx)))
diff --git a/src/util/ocamlgraph/goblint_ocamlgraph.ml b/src/util/ocamlgraph/goblint_ocamlgraph.ml
new file mode 100644
index 0000000000..d819cb98ad
--- /dev/null
+++ b/src/util/ocamlgraph/goblint_ocamlgraph.ml
@@ -0,0 +1,3 @@
+(** OCamlgraph library extensions which are completely independent of Goblint. *)
+
+module Coloring = Coloring

From bd6dc3dc8f587e9eb0ad95c57a3bd08bec486f57 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 22 Jul 2026 14:29:36 +0300
Subject: [PATCH 07/11] Remove now-unused Access.InterferenceGraph.of_warn_accs

---
 src/domains/access.ml | 17 -----------------
 1 file changed, 17 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index 5755df0496..5db5dccbb2 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -490,23 +490,6 @@ module InterferenceGraph = struct
 
   type t = G.t
 
-  let of_warn_accs (warn_accs : WarnAccs.t) =
-    let graph = G.create () in
-    let all = WarnAccs.union_all warn_accs in
-    AS.iter (fun acc -> G.add_vertex graph acc) all;
-    let accs = AS.elements all in
-    let rec loop = function
-      | [] -> ()
-      | a :: rest ->
-        List.iter (fun b ->
-            if may_race a b then
-              G.add_edge graph a b
-          ) rest;
-        loop rest
-    in
-    loop accs;
-    graph
-
   module Coloring = Goblint_ocamlgraph.Coloring.Make (G)
 
   let of_accesses (accs : AS.t) =

From 901a7d261fb88a56d5883447a1fe7b7ab4100f53 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 22 Jul 2026 14:43:20 +0300
Subject: [PATCH 08/11] Simplify warn.race-coloring option handling

---
 src/domains/access.ml | 54 +++++++++++++++++++++----------------------
 1 file changed, 26 insertions(+), 28 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index 5db5dccbb2..244de25291 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -619,31 +619,36 @@ let incr_summary ~safe ~vulnerable ~unsafe grouped_accs =
   | Some n when n >= 100 -> is_all_safe := false; incr unsafe
   | Some n -> is_all_safe := false; incr vulnerable
 
-let print_accesses ?coloring_mode memo grouped_accs =
+let coloring_module =
+  lazy (
+    match get_string "warn.race-coloring" with
+    | "none" -> None
+    | "greedy" ->
+      Some (module InterferenceGraph.Coloring.Greedy: InterferenceGraph.Coloring.ALGORITHM)
+    | "dsatur" ->
+      Some (module InterferenceGraph.Coloring.Dsatur)
+    | "rlf" ->
+      Some (module InterferenceGraph.Coloring.Rlf)
+    | "optimal" ->
+      Some (module InterferenceGraph.Coloring.Optimal)
+    | _ -> assert false
+  )
+
+let print_accesses memo grouped_accs =
   let allglobs = get_bool "allglobs" in
   let race_threshold = get_int "warn.race-threshold" in
-  let coloring_for accs =
-    match coloring_mode with
-    | None -> None
-    | Some "greedy" ->
-      let graph = InterferenceGraph.of_accesses accs in
-      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Greedy) graph)
-    | Some "dsatur" ->
-      let graph = InterferenceGraph.of_accesses accs in
-      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Dsatur) graph)
-    | Some "rlf" ->
-      let graph = InterferenceGraph.of_accesses accs in
-      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Rlf) graph)
-    | Some "optimal" ->
-      let graph = InterferenceGraph.of_accesses accs in
-      Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Optimal) graph)
-    | Some _ -> None
-  in
-  let msgs ?coloring race_accs =
+  let msgs race_accs =
     let h A.{conf; kind; node; exp; acc} =
       let doc = dprintf "%a with %a (conf. %d)  (exp: %a)" AccessKind.pretty kind MCPAccess.A.pretty acc conf d_exp exp in
       (doc, Some (Messages.Location.Node node))
     in
+    let coloring =
+      match coloring_module with
+      | lazy None -> None
+      | lazy (Some (module A: InterferenceGraph.Coloring.ALGORITHM)) ->
+        let graph = InterferenceGraph.of_accesses race_accs in
+        Some (A.color graph)
+    in
     match coloring with
     | None ->
       AS.elements race_accs
@@ -684,8 +689,7 @@ let print_accesses ?coloring_mode memo grouped_accs =
           else
             Info
         in
-        let coloring = coloring_for accs in
-        M.msg_group severity ?loc:group_loc ~category:Race "Memory location %a (race with conf. %d)" Memo.pretty memo conf (msgs ?coloring accs);
+        M.msg_group severity ?loc:group_loc ~category:Race "Memory location %a (race with conf. %d)" Memo.pretty memo conf (msgs accs);
         safe_accs
     ) (AS.empty ())
   |> (fun safe_accs ->
@@ -694,12 +698,6 @@ let print_accesses ?coloring_mode memo grouped_accs =
     )
 
 let warn_global ~safe ~vulnerable ~unsafe warn_accs memo =
-  let coloring_mode =
-    match get_string "warn.race-coloring" with
-    | "" | "none" -> None
-    | "greedy" | "dsatur" | "rlf" | "optimal" as mode -> Some mode
-    | _ -> None
-  in
   let grouped_accs = group_may_race warn_accs in (* do expensive component finding only once *)
   incr_summary ~safe ~vulnerable ~unsafe grouped_accs;
-  print_accesses ?coloring_mode memo grouped_accs
+  print_accesses memo grouped_accs

From 35e8e53494081418f57f33b769880a85c9e95507 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 22 Jul 2026 14:58:29 +0300
Subject: [PATCH 09/11] Simplify Access.InterferenceGraph

---
 src/domains/access.ml | 35 ++++++++++++++---------------------
 1 file changed, 14 insertions(+), 21 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index 244de25291..05204d0962 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -484,30 +484,27 @@ struct
       AS.pretty w.node AS.pretty w.prefix AS.pretty w.type_suffix AS.pretty w.type_suffix_prefix
 end
 
-module InterferenceGraph = struct
-
-  module G = Graph.Imperative.Graph.Concrete (A)
-
-  type t = G.t
-
-  module Coloring = Goblint_ocamlgraph.Coloring.Make (G)
+module InterferenceGraph =
+struct
+  include Graph.Imperative.Graph.Concrete (A)
 
   let of_accesses (accs : AS.t) =
-    let graph = G.create () in
-    AS.iter (fun acc -> G.add_vertex graph acc) accs;
+    let graph = create () in
+    AS.iter (fun acc -> add_vertex graph acc) accs;
     let accs_list = AS.elements accs in
     let rec loop = function
       | [] -> ()
       | a :: rest ->
         List.iter (fun b ->
             if may_race a b then
-              G.add_edge graph a b
+              add_edge graph a b
           ) rest;
         loop rest
     in
     loop accs_list;
     graph
 end
+module InterferenceGraphColoring = Goblint_ocamlgraph.Coloring.Make (InterferenceGraph)
 
 let group_may_race (warn_accs:WarnAccs.t) =
   if M.tracing then M.tracei "access" "group_may_race %a" WarnAccs.pretty warn_accs;
@@ -621,16 +618,13 @@ let incr_summary ~safe ~vulnerable ~unsafe grouped_accs =
 
 let coloring_module =
   lazy (
+    let open InterferenceGraphColoring in
     match get_string "warn.race-coloring" with
     | "none" -> None
-    | "greedy" ->
-      Some (module InterferenceGraph.Coloring.Greedy: InterferenceGraph.Coloring.ALGORITHM)
-    | "dsatur" ->
-      Some (module InterferenceGraph.Coloring.Dsatur)
-    | "rlf" ->
-      Some (module InterferenceGraph.Coloring.Rlf)
-    | "optimal" ->
-      Some (module InterferenceGraph.Coloring.Optimal)
+    | "greedy" -> Some (module Greedy: ALGORITHM)
+    | "dsatur" -> Some (module Dsatur)
+    | "rlf" -> Some (module Rlf)
+    | "optimal" -> Some (module Optimal)
     | _ -> assert false
   )
 
@@ -645,7 +639,7 @@ let print_accesses memo grouped_accs =
     let coloring =
       match coloring_module with
       | lazy None -> None
-      | lazy (Some (module A: InterferenceGraph.Coloring.ALGORITHM)) ->
+      | lazy (Some (module A: InterferenceGraphColoring.ALGORITHM)) ->
         let graph = InterferenceGraph.of_accesses race_accs in
         Some (A.color graph)
     in
@@ -655,9 +649,8 @@ let print_accesses memo grouped_accs =
       |> List.map h
     | Some coloring ->
       let module IntMap = Map.Make (Int) in
-      let module C = InterferenceGraph.Coloring in
       let add_to_map acc map =
-        match C.color_of coloring acc with
+        match InterferenceGraphColoring.color_of coloring acc with
         | None -> map
         | Some c ->
           IntMap.update c (function

From 73ba8f4c239dada5a68cec95d1cd046a44374fc3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 22 Jul 2026 14:59:11 +0300
Subject: [PATCH 10/11] Move Access.InterferenceGraph down

---
 src/domains/access.ml | 44 +++++++++++++++++++++----------------------
 1 file changed, 22 insertions(+), 22 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index 05204d0962..efd66c19e4 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -484,28 +484,6 @@ struct
       AS.pretty w.node AS.pretty w.prefix AS.pretty w.type_suffix AS.pretty w.type_suffix_prefix
 end
 
-module InterferenceGraph =
-struct
-  include Graph.Imperative.Graph.Concrete (A)
-
-  let of_accesses (accs : AS.t) =
-    let graph = create () in
-    AS.iter (fun acc -> add_vertex graph acc) accs;
-    let accs_list = AS.elements accs in
-    let rec loop = function
-      | [] -> ()
-      | a :: rest ->
-        List.iter (fun b ->
-            if may_race a b then
-              add_edge graph a b
-          ) rest;
-        loop rest
-    in
-    loop accs_list;
-    graph
-end
-module InterferenceGraphColoring = Goblint_ocamlgraph.Coloring.Make (InterferenceGraph)
-
 let group_may_race (warn_accs:WarnAccs.t) =
   if M.tracing then M.tracei "access" "group_may_race %a" WarnAccs.pretty warn_accs;
   (* BFS to traverse one component with may_race edges *)
@@ -616,6 +594,28 @@ let incr_summary ~safe ~vulnerable ~unsafe grouped_accs =
   | Some n when n >= 100 -> is_all_safe := false; incr unsafe
   | Some n -> is_all_safe := false; incr vulnerable
 
+module InterferenceGraph =
+struct
+  include Graph.Imperative.Graph.Concrete (A)
+
+  let of_accesses (accs : AS.t) =
+    let graph = create () in
+    AS.iter (fun acc -> add_vertex graph acc) accs;
+    let accs_list = AS.elements accs in
+    let rec loop = function
+      | [] -> ()
+      | a :: rest ->
+        List.iter (fun b ->
+            if may_race a b then
+              add_edge graph a b
+          ) rest;
+        loop rest
+    in
+    loop accs_list;
+    graph
+end
+module InterferenceGraphColoring = Goblint_ocamlgraph.Coloring.Make (InterferenceGraph)
+
 let coloring_module =
   lazy (
     let open InterferenceGraphColoring in

From 7abfd0ed9a735028770c80af9c52416fbfa8c486 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 22 Jul 2026 15:02:06 +0300
Subject: [PATCH 11/11] Simplify graph coloring module usage in Access

---
 src/domains/access.ml | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index efd66c19e4..b16aae7fa3 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -636,18 +636,13 @@ let print_accesses memo grouped_accs =
       let doc = dprintf "%a with %a (conf. %d)  (exp: %a)" AccessKind.pretty kind MCPAccess.A.pretty acc conf d_exp exp in
       (doc, Some (Messages.Location.Node node))
     in
-    let coloring =
-      match coloring_module with
-      | lazy None -> None
-      | lazy (Some (module A: InterferenceGraphColoring.ALGORITHM)) ->
-        let graph = InterferenceGraph.of_accesses race_accs in
-        Some (A.color graph)
-    in
-    match coloring with
-    | None ->
+    match coloring_module with
+    | lazy None ->
       AS.elements race_accs
       |> List.map h
-    | Some coloring ->
+    | lazy (Some (module Coloring: InterferenceGraphColoring.ALGORITHM)) ->
+      let graph = InterferenceGraph.of_accesses race_accs in
+      let coloring = Coloring.color graph in
       let module IntMap = Map.Make (Int) in
       let add_to_map acc map =
         match InterferenceGraphColoring.color_of coloring acc with