From 21e0644d56cd69f4f578e7f1e5b649b291e3c753 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 30 Nov 2023 16:27:31 +0200
Subject: [PATCH] Add global invariant to maylocksdigest

---
 src/analyses/mayLocksDigest.ml | 26 ++++++++++++++++++++------
 1 file changed, 20 insertions(+), 6 deletions(-)

diff --git a/src/analyses/mayLocksDigest.ml b/src/analyses/mayLocksDigest.ml
index fa5ce7a3d7..4f3bc5308d 100644
--- a/src/analyses/mayLocksDigest.ml
+++ b/src/analyses/mayLocksDigest.ml
@@ -8,13 +8,27 @@ module Arg =
 struct
   module D = LockDomain.MayLocksetNoRW
   module P = IdentityP (D)
-  module G = DefaultSpec.G
-  module V = DefaultSpec.V
 
-  let add ctx (l,r) =
-    D.add l ctx.local
-
-  let remove ctx l =
+  module V =
+  struct
+    include StdV
+    include LockDomain.Addr
+  end
+  module G = SetDomain.Make (D)
+
+  let add (ctx: (D.t, G.t, D.t, V.t) ctx) (l,r) =
+    let l's = ctx.global l in
+    G.iter (fun l' ->
+        if not (D.mem l ctx.local && not (D.mem l l')) then
+          ctx.split (D.add l (D.union ctx.local l')) []
+      ) l's;
+    if D.mem l ctx.local then
+      raise Deadcode
+    else
+      D.add l ctx.local (* for initial empty *)
+
+  let remove (ctx: (D.t, G.t, D.t, V.t) ctx) l =
+    ctx.sideg l (G.singleton ctx.local);
     ctx.local
 end