Extract digest domain functor in mutex-meet

src/analyses/apron/relationPriv.apron.ml

@@ -862,13 +862,8 @@ 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 = Digest.current ask in
-    GMutex.fold (fun k v acc ->
-        if not (Digest.accounted_for ask ~current ~other:k) then
-          LRD.join acc (Cluster.keep_only_protected_globals ask m v)
-        else
-          acc
-      ) v (LRD.bot ())
+    let v = DigestD.map (Cluster.keep_only_protected_globals ask m) v in
+    DigestD.get_relevant_writes_nofilter ask v
 
   type relation_components_t =  RelationDomain.RelComponents (RD) (D).t
 
@@ -879,7 +874,7 @@ struct
       if not inits then
         get_m
       else
-        let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+        let get_mutex_inits = DigestD.merge_all @@ G.mutex @@ getg V.mutex_inits in
         let get_mutex_inits' = Cluster.keep_only_protected_globals ask m get_mutex_inits in
         if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a\n" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits';
         LRD.join get_m get_mutex_inits'
@@ -888,13 +883,13 @@ struct
     r
 
   let get_mutex_global_g_with_mutex_inits inits ask getg g =
-    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g) in
+    let get_mutex_global_g = DigestD.get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g) in
     if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n  get=%a\n" CilType.Varinfo.pretty g LRD.pretty get_mutex_global_g;
     let r =
       if not inits then
         get_mutex_global_g
       else
-        let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+        let get_mutex_inits = DigestD.merge_all @@ G.mutex @@ getg V.mutex_inits in
         let get_mutex_inits' = Cluster.keep_global g get_mutex_inits in
         if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a\n" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits';
         LRD.join get_mutex_global_g get_mutex_inits'

src/analyses/basePriv.ml

@@ -411,33 +411,28 @@ struct
       m
 
   let get_mutex_global_g_with_mutex_inits inits ask getg g =
-    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g) in
+    let get_mutex_global_g = DigestD.get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g) in
     let r = if not inits then
         get_mutex_global_g
       else
-        let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+        let get_mutex_inits = DigestD.merge_all @@ G.mutex @@ getg V.mutex_inits in
         let get_mutex_inits' = CPA.singleton g (CPA.find g get_mutex_inits) in
         CPA.join get_mutex_global_g get_mutex_inits'
     in
     r
 
   let get_relevant_writes (ask:Q.ask) m v =
-    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 not (Digest.accounted_for ask ~current ~other:k) then
-          CPA.join acc (CPA.filter is_in_Gm v)
-        else
-          acc
-      ) v (CPA.bot ())
+    let v = DigestD.map (CPA.filter is_in_Gm) v in
+    DigestD.get_relevant_writes_nofilter ask v
 
   let get_m_with_mutex_inits inits ask getg m =
     let get_m = get_relevant_writes ask m (G.mutex @@ getg (V.mutex m)) in
     let r =
       if not inits then
         get_m
       else
-        let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+        let get_mutex_inits = DigestD.merge_all @@ G.mutex @@ getg V.mutex_inits in
         let is_in_Gm x _ = is_protected_by ~protection:Weak ask m x in
         let get_mutex_inits' = CPA.filter is_in_Gm get_mutex_inits in
         CPA.join get_m get_mutex_inits'
@@ -615,9 +610,9 @@ struct
     else st
 
   let read_unprotected_global getg x =
-    let get_mutex_global_x = merge_all @@ G.mutex @@ getg (V.global x) in
+    let get_mutex_global_x = DigestD.merge_all @@ G.mutex @@ getg (V.global x) in
     let get_mutex_global_x' = CPA.find x get_mutex_global_x in
-    let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+    let get_mutex_inits = DigestD.merge_all @@ G.mutex @@ getg V.mutex_inits in
     let get_mutex_inits' = CPA.find x get_mutex_inits in
     VD.join get_mutex_global_x' get_mutex_inits'
 

src/analyses/commonPriv.ml

@@ -185,8 +185,27 @@ struct
     | _ -> false
 end
 
-module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) =
+module DigestD (Digest: Digest) (LD: Lattice.S) =
 struct
+  include MapDomain.MapBot_LiftTop (Digest) (LD)
+
+  let get_relevant_writes_nofilter (ask: Q.ask) v =
+    let current = Digest.current ask in
+    fold (fun k v acc ->
+        if not (Digest.accounted_for ask ~current ~other:k) then
+          LD.join acc v
+        else
+          acc
+      ) v (LD.bot ())
+
+  let merge_all v =
+    fold (fun _ v acc -> LD.join acc v) v (LD.bot ())
+end
+
+module PerMutexTidCommon (Digest: Digest) (LD: Lattice.S) =
+struct
+  module DigestD = DigestD (Digest) (LD)
+
   include ConfCheck.RequireThreadFlagPathSensInit
 
   module TID = ThreadIdDomain.Thread
@@ -222,7 +241,7 @@ struct
 
   (* Map from locks to last written values thread-locally *)
   module L = MapDomain.MapBot_LiftTop (LLock) (LD)
-  module GMutex = MapDomain.MapBot_LiftTop (Digest) (LD)
+  module GMutex = DigestD
   module GThread = Lattice.Prod (LMust) (L)
 
   module G =
@@ -244,17 +263,5 @@ struct
 
   module D = Lattice.Prod3 (W) (LMust) (L)
 
-  let get_relevant_writes_nofilter (ask:Q.ask) v =
-    let current = Digest.current ask in
-    GMutex.fold (fun k v acc ->
-        if not (Digest.accounted_for ask ~current ~other:k) then
-          LD.join acc v
-        else
-          acc
-      ) v (LD.bot ())
-
-  let merge_all v =
-    GMutex.fold (fun _ v acc -> LD.join acc v) v (LD.bot ())
-
   let startstate () = W.bot (), LMust.top (), L.bot ()
 end