diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index f073ae274b..b4e23b65cc 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -843,7 +843,7 @@ struct end (** Per-mutex meet with TIDs. *) -module PerMutexMeetPrivTID (Cluster: ClusterArg): S = functor (RD: RelationDomain.RD) -> +module PerMutexMeetPrivTID (Digest: Digest) (Cluster: ClusterArg): S = functor (RD: RelationDomain.RD) -> struct open CommonPerMutex(RD) include MutexGlobals @@ -853,10 +853,7 @@ struct module Cluster = NC module LRD = NC.LRD - include PerMutexTidCommon(struct - let exclude_not_started () = GobConfig.get_bool "ana.relation.priv.not-started" - let exclude_must_joined () = GobConfig.get_bool "ana.relation.priv.must-joined" - end)(LRD) + include PerMutexTidCommon (Digest) (LRD) module AV = RD.V module P = UnitP @@ -864,10 +861,9 @@ 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 = ThreadId.get_current ask in - let must_joined = ask.f Queries.MustJoinedThreads in + let current = Digest.current ask in GMutex.fold (fun k v acc -> - if compatible ask current must_joined k then + if not (Digest.accounted_for ask ~current ~other:k) then LRD.join acc (Cluster.keep_only_protected_globals ask m v) else acc @@ -945,8 +941,8 @@ 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 tid = ThreadId.get_current ask in - let sidev = GMutex.singleton tid rel_side in + let digest = Digest.current ask in + let sidev = GMutex.singleton digest rel_side in sideg (V.global g) (G.create_global sidev); let l' = L.add lm rel_side l in let rel_local' = @@ -983,8 +979,8 @@ struct else let rel_side = keep_only_protected_globals ask m rel in let rel_side = Cluster.unlock w rel_side in - let tid = ThreadId.get_current ask in - let sidev = GMutex.singleton tid rel_side in + let digest = Digest.current ask in + let sidev = GMutex.singleton digest 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 @@ -1068,8 +1064,8 @@ 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 tid = ThreadId.get_current ask in - let sidev = GMutex.singleton tid rel_side in + let digest = Digest.current ask in + let sidev = GMutex.singleton digest 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, *) @@ -1207,11 +1203,11 @@ let priv_module: (module S) Lazy.t = | "protection" -> (module ProtectionBasedPriv (struct let path_sensitive = false end)) | "protection-path" -> (module ProtectionBasedPriv (struct let path_sensitive = true end)) | "mutex-meet" -> (module PerMutexMeetPriv) - | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (NoCluster)) - | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (Clustering12))) - | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ArbitraryCluster (Clustering2))) - | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (ArbitraryCluster (ClusteringMax))) - | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (ClusteringPower))) + | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (ThreadDigest) (NoCluster)) + | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (ThreadDigest) (DownwardClosedCluster (Clustering12))) + | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ThreadDigest) (ArbitraryCluster (Clustering2))) + | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (ThreadDigest) (ArbitraryCluster (ClusteringMax))) + | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (ThreadDigest) (DownwardClosedCluster (ClusteringPower))) | _ -> failwith "ana.relation.privatization: illegal value" ) in diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 10deaa4d16..479ffc2d93 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -391,14 +391,11 @@ struct st end -module PerMutexMeetTIDPriv: S = +module PerMutexMeetTIDPriv (Digest: Digest): S = struct open Queries.Protection include PerMutexMeetPrivBase - include PerMutexTidCommon(struct - let exclude_not_started () = GobConfig.get_bool "ana.base.priv.not-started" - let exclude_must_joined () = GobConfig.get_bool "ana.base.priv.must-joined" - end)(CPA) + include PerMutexTidCommon (Digest) (CPA) let iter_sys_vars getg vq vf = match vq with @@ -425,11 +422,10 @@ struct r let get_relevant_writes (ask:Q.ask) m v = - let current = ThreadId.get_current ask in - let must_joined = ask.f Queries.MustJoinedThreads in + 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 compatible ask current must_joined k then + if not (Digest.accounted_for ask ~current ~other:k) then CPA.join acc (CPA.filter is_in_Gm v) else acc @@ -474,8 +470,8 @@ 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 tid = ThreadId.get_current ask in - let sidev = GMutex.singleton tid (CPA.singleton x v) in + let digest = Digest.current ask in + let sidev = GMutex.singleton digest (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 @@ -517,8 +513,8 @@ 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 tid = ThreadId.get_current ask in - let sidev = GMutex.singleton tid (CPA.filter is_in_Gm st.cpa) in + let digest = Digest.current ask in + let sidev = GMutex.singleton digest (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 @@ -568,13 +564,13 @@ 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 tid = ThreadId.get_current ask in - let sidev = GMutex.singleton tid escaped_cpa in + let digest = Digest.current ask in + let sidev = GMutex.singleton digest 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 tid (CPA.singleton x v) in + let sidev = GMutex.singleton digest (CPA.singleton x v) in sideg (V.global x) (G.create_global sidev); CPA.remove x acc ) @@ -587,8 +583,8 @@ 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 tid = ThreadId.get_current ask in - let sidev = GMutex.singleton tid cpa_side in + let digest = Digest.current ask in + let sidev = GMutex.singleton digest 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, *) @@ -1782,7 +1778,7 @@ let priv_module: (module S) Lazy.t = | "none" -> (module NonePriv: S) | "mutex-oplus" -> (module PerMutexOplusPriv) | "mutex-meet" -> (module PerMutexMeetPriv) - | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv) + | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest)) | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false end)) | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true end)) | "mine" -> (module MinePriv) diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 90e5b28f82..8c406df665 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -151,12 +151,38 @@ struct end end -module type PerMutexTidCommonArg = sig - val exclude_not_started: unit -> bool - val exclude_must_joined: unit -> bool +module type Digest = +sig + include Printable.S + + val current: Q.ask -> t + val accounted_for: Q.ask -> current:t -> other:t -> bool end -module PerMutexTidCommon (Conf:PerMutexTidCommonArg) (LD:Lattice.S) = +module ThreadDigest: Digest = +struct + include ThreadIdDomain.ThreadLifted + + module TID = ThreadIdDomain.Thread + + let current (ask: Q.ask) = + ThreadId.get_current ask + + let accounted_for (ask: Q.ask) ~(current: t) ~(other: t) = + match current, other with + | `Lifted current, `Lifted other -> + if TID.is_unique current && TID.equal current other then + true (* self-read *) + else if GobConfig.get_bool "ana.relation.priv.not-started" && MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other then + true (* other is not started yet *) + else if GobConfig.get_bool "ana.relation.priv.must-joined" && MHP.must_be_joined other (ask.f Queries.MustJoinedThreads) then + true (* accounted for in local information *) + else + false + | _ -> false +end + +module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) = struct include ConfCheck.RequireThreadFlagPathSensInit @@ -193,7 +219,7 @@ struct (* Map from locks to last written values thread-locally *) module L = MapDomain.MapBot_LiftTop (LLock) (LD) - module GMutex = MapDomain.MapBot_LiftTop (ThreadIdDomain.ThreadLifted) (LD) + module GMutex = MapDomain.MapBot_LiftTop (Digest) (LD) module GThread = Lattice.Prod (LMust) (L) module G = @@ -215,24 +241,10 @@ struct module D = Lattice.Prod3 (W) (LMust) (L) - let compatible (ask:Q.ask) current must_joined other = - match current, other with - | `Lifted current, `Lifted other -> - if (TID.is_unique current) && (TID.equal current other) then - false (* self-read *) - else if Conf.exclude_not_started () && MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other then - false (* other is not started yet *) - else if Conf.exclude_must_joined () && MHP.must_be_joined other must_joined then - false (* accounted for in local information *) - else - true - | _ -> true - let get_relevant_writes_nofilter (ask:Q.ask) v = - let current = ThreadId.get_current ask in - let must_joined = ask.f Queries.MustJoinedThreads in + let current = Digest.current ask in GMutex.fold (fun k v acc -> - if compatible ask current must_joined k then + if not (Digest.accounted_for ask ~current ~other:k) then LD.join acc v else acc