From ae3ac625271cba9f3c38b230a4b4236ff7c49c81 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 6 Dec 2023 13:04:55 +0200 Subject: [PATCH] Extract digest domain functor in mutex-meet --- src/analyses/apron/relationPriv.apron.ml | 15 ++++------ src/analyses/basePriv.ml | 19 +++++-------- src/analyses/commonPriv.ml | 35 ++++++++++++++---------- 3 files changed, 33 insertions(+), 36 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 31dd1fc4f5..41af766c99 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/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' diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 20ef13244b..88e9c985cf 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -411,25 +411,20 @@ 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 @@ -437,7 +432,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 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' diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 2739578957..0d4962d18b 100644 --- a/src/analyses/commonPriv.ml +++ b/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