Generalize mutex-meet over digest domain

src/analyses/apron/relationPriv.apron.ml

@@ -853,8 +853,9 @@ struct
   module NC = Cluster(RD)
   module Cluster = NC
   module LRD = NC.LRD
+  module DigestD = DigestD (Digest) (LRD)
 
-  include PerMutexTidCommon (Digest) (LRD)
+  include PerMutexTidCommon (DigestD) (LRD)
 
   module AV = RD.V
   module P = UnitP
@@ -937,8 +938,7 @@ 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 digest = Digest.current ask in
-    let sidev = GMutex.singleton digest rel_side in
+    let sidev = DigestD.make ask rel_side in
     sideg (V.global g) (G.create_global sidev);
     let l' = L.add lm rel_side l in
     let rel_local' =
@@ -975,8 +975,7 @@ struct
     else
       let rel_side = keep_only_protected_globals ask m rel in
       let rel_side = Cluster.unlock w rel_side in
-      let digest = Digest.current ask in
-      let sidev = GMutex.singleton digest rel_side in
+      let sidev = DigestD.make ask 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
@@ -1060,8 +1059,7 @@ 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 digest = Digest.current ask in
-    let sidev = GMutex.singleton digest rel_side in
+    let sidev = DigestD.make ask 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, *)

src/analyses/basePriv.ml

@@ -395,7 +395,8 @@ module PerMutexMeetTIDPriv (Digest: Digest): S =
 struct
   open Queries.Protection
   include PerMutexMeetPrivBase
-  include PerMutexTidCommon (Digest) (CPA)
+  module DigestD = DigestD (Digest) (CPA)
+  include PerMutexTidCommon (DigestD) (CPA)
 
   let iter_sys_vars getg vq vf =
     match vq with
@@ -465,8 +466,7 @@ 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 digest = Digest.current ask in
-    let sidev = GMutex.singleton digest (CPA.singleton x v) in
+    let sidev = DigestD.make ask (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
@@ -508,8 +508,7 @@ 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 digest = Digest.current ask in
-      let sidev = GMutex.singleton digest (CPA.filter is_in_Gm st.cpa) in
+      let sidev = DigestD.make ask (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
@@ -559,13 +558,12 @@ 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 digest = Digest.current ask in
-    let sidev = GMutex.singleton digest escaped_cpa in
+    let sidev = DigestD.make ask 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 digest (CPA.singleton x v) in
+          let sidev = DigestD.make ask (CPA.singleton x v) in
           sideg (V.global x) (G.create_global sidev);
           CPA.remove x acc
         )
@@ -578,8 +576,7 @@ 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 digest = Digest.current ask in
-    let sidev = GMutex.singleton digest cpa_side in
+    let sidev = DigestD.make ask 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, *)

src/analyses/commonPriv.ml

@@ -185,7 +185,19 @@ struct
     | _ -> false
 end
 
-module DigestD (Digest: Digest) (LD: Lattice.S) =
+module type DigestD =
+sig
+  include Lattice.S
+  type value
+
+  val get_relevant_writes_nofilter: Q.ask -> t -> value
+  val merge_all: t -> value
+  val make: Q.ask -> value -> t
+
+  val map: (value -> value) -> t -> t
+end
+
+module DigestD (Digest: Digest) (LD: Lattice.S): DigestD with type value = LD.t =
 struct
   include MapDomain.MapBot_LiftTop (Digest) (LD)
 
@@ -200,12 +212,13 @@ struct
 
   let merge_all v =
     fold (fun _ v acc -> LD.join acc v) v (LD.bot ())
+
+  let make ask v =
+    singleton (Digest.current ask) v
 end
 
-module PerMutexTidCommon (Digest: Digest) (LD: Lattice.S) =
+module PerMutexTidCommon (DigestD: DigestD) (LD: Lattice.S) =
 struct
-  module DigestD = DigestD (Digest) (LD)
-
   include ConfCheck.RequireThreadFlagPathSensInit
 
   module TID = ThreadIdDomain.Thread