From a3923237a01b4f6476911655e8b006b139337a8a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 12:58:30 +0200 Subject: [PATCH 1/5] Generalize mutex-meet-tid privatization to arbitrary digest --- src/analyses/apron/relationPriv.apron.ml | 41 +++++++++--------- src/analyses/basePriv.ml | 39 +++++++++-------- src/analyses/commonPriv.ml | 54 ++++++++++++++++-------- 3 files changed, 79 insertions(+), 55 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index b386af162b..ad55c425cd 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -844,7 +844,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 @@ -854,10 +854,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 @@ -865,10 +862,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 Digest.compatible ask current k then LRD.join acc (Cluster.keep_only_protected_globals ask m v) else acc @@ -946,8 +942,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' = @@ -984,8 +980,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 @@ -1069,8 +1065,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, *) @@ -1202,17 +1198,24 @@ end let priv_module: (module S) Lazy.t = lazy ( + let module TIDDigest = ThreadDigest ( + 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 + ) + in let module Priv: S = (val match get_string "ana.relation.privatization" with | "top" -> (module Top : S) | "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 (TIDDigest) (NoCluster)) + | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (TIDDigest) (DownwardClosedCluster (Clustering12))) + | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (TIDDigest) (ArbitraryCluster (Clustering2))) + | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (TIDDigest) (ArbitraryCluster (ClusteringMax))) + | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (TIDDigest) (DownwardClosedCluster (ClusteringPower))) | _ -> failwith "ana.relation.privatization: illegal value" ) in diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 3843dda300..0c67347d3f 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 Digest.compatible ask current 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, *) @@ -1790,12 +1786,19 @@ end let priv_module: (module S) Lazy.t = lazy ( + let module TIDDigest = ThreadDigest ( + 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 + ) + in let module Priv: S = (val match get_string "ana.base.privatization" with | "none" -> (module NonePriv: S) | "mutex-oplus" -> (module PerMutexOplusPriv) | "mutex-meet" -> (module PerMutexMeetPriv) - | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv) + | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (TIDDigest)) | "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 88181000b9..3c8056bb34 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -154,12 +154,44 @@ struct end end +module type Digest = +sig + include Printable.S + + val current: Q.ask -> t + val compatible: Q.ask -> t -> t -> bool +end + module type PerMutexTidCommonArg = sig val exclude_not_started: unit -> bool val exclude_must_joined: unit -> bool end -module PerMutexTidCommon (Conf:PerMutexTidCommonArg) (LD:Lattice.S) = +module ThreadDigest (Conf: PerMutexTidCommonArg): Digest = +struct + include ThreadIdDomain.ThreadLifted + + module TID = ThreadIdDomain.Thread + + let current (ask: Q.ask) = + ThreadId.get_current ask + + let compatible (ask: Q.ask) (current: t) (other: t) = + let must_joined = ask.f Queries.MustJoinedThreads in + 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 +end + +module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) = struct include ConfCheck.RequireThreadFlagPathSensInit @@ -196,7 +228,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 = @@ -218,24 +250,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 Digest.compatible ask current k then LD.join acc v else acc From 6dfc08ff3aa493a0808edd0ac19914fe8ecde375 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 13:34:26 +0200 Subject: [PATCH 2/5] Simplify CommonPriv.ThreadDigest --- src/analyses/apron/relationPriv.apron.ml | 17 +++++------------ src/analyses/basePriv.ml | 9 +-------- src/analyses/commonPriv.ml | 11 +++-------- 3 files changed, 9 insertions(+), 28 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index ad55c425cd..a34e052602 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -1198,24 +1198,17 @@ end let priv_module: (module S) Lazy.t = lazy ( - let module TIDDigest = ThreadDigest ( - 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 - ) - in let module Priv: S = (val match get_string "ana.relation.privatization" with | "top" -> (module Top : S) | "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 (TIDDigest) (NoCluster)) - | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (TIDDigest) (DownwardClosedCluster (Clustering12))) - | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (TIDDigest) (ArbitraryCluster (Clustering2))) - | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (TIDDigest) (ArbitraryCluster (ClusteringMax))) - | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (TIDDigest) (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 0c67347d3f..e600c2a05d 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -1786,19 +1786,12 @@ end let priv_module: (module S) Lazy.t = lazy ( - let module TIDDigest = ThreadDigest ( - 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 - ) - in let module Priv: S = (val match get_string "ana.base.privatization" with | "none" -> (module NonePriv: S) | "mutex-oplus" -> (module PerMutexOplusPriv) | "mutex-meet" -> (module PerMutexMeetPriv) - | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (TIDDigest)) + | "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 3c8056bb34..23ed36f7fb 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -162,12 +162,7 @@ sig val compatible: Q.ask -> t -> t -> bool end -module type PerMutexTidCommonArg = sig - val exclude_not_started: unit -> bool - val exclude_must_joined: unit -> bool -end - -module ThreadDigest (Conf: PerMutexTidCommonArg): Digest = +module ThreadDigest: Digest = struct include ThreadIdDomain.ThreadLifted @@ -182,9 +177,9 @@ struct | `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 + else if GobConfig.get_bool "ana.relation.priv.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 + else if GobConfig.get_bool "ana.relation.priv.must-joined" && MHP.must_be_joined other must_joined then false (* accounted for in local information *) else true From 05198f9640c3b39f8d7e2d661f76904c76f52d9a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 13:35:36 +0200 Subject: [PATCH 3/5] Avoid MustJoinedThreads query in ThreadDigest if not needed --- src/analyses/commonPriv.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 23ed36f7fb..2e7ed570fd 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -172,14 +172,13 @@ struct ThreadId.get_current ask let compatible (ask: Q.ask) (current: t) (other: t) = - let must_joined = ask.f Queries.MustJoinedThreads in match current, other with | `Lifted current, `Lifted other -> - if (TID.is_unique current) && (TID.equal current other) then + if TID.is_unique current && TID.equal current other then false (* self-read *) else if GobConfig.get_bool "ana.relation.priv.not-started" && MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other then false (* other is not started yet *) - else if GobConfig.get_bool "ana.relation.priv.must-joined" && MHP.must_be_joined other must_joined then + else if GobConfig.get_bool "ana.relation.priv.must-joined" && MHP.must_be_joined other (ask.f Queries.MustJoinedThreads) then false (* accounted for in local information *) else true From bda139ff7d12e2b59b20b289d89c60fdeef37304 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 5 Dec 2023 17:09:32 +0200 Subject: [PATCH 4/5] Rename Digest.compatible -> accounted_for --- src/analyses/apron/relationPriv.apron.ml | 2 +- src/analyses/basePriv.ml | 2 +- src/analyses/commonPriv.ml | 6 +++--- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index a34e052602..6c330e8798 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -864,7 +864,7 @@ struct let get_relevant_writes (ask:Q.ask) m v = let current = Digest.current ask in GMutex.fold (fun k v acc -> - if Digest.compatible ask current k then + if Digest.accounted_for ask ~current ~other:k then LRD.join acc (Cluster.keep_only_protected_globals ask m v) else acc diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index e600c2a05d..26fb5850a8 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -425,7 +425,7 @@ struct 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 Digest.compatible ask current k then + if Digest.accounted_for ask ~current ~other:k then CPA.join acc (CPA.filter is_in_Gm v) else acc diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 2e7ed570fd..5f89eecdd8 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -159,7 +159,7 @@ sig include Printable.S val current: Q.ask -> t - val compatible: Q.ask -> t -> t -> bool + val accounted_for: Q.ask -> current:t -> other:t -> bool end module ThreadDigest: Digest = @@ -171,7 +171,7 @@ struct let current (ask: Q.ask) = ThreadId.get_current ask - let compatible (ask: Q.ask) (current: t) (other: t) = + 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 @@ -247,7 +247,7 @@ struct let get_relevant_writes_nofilter (ask:Q.ask) v = let current = Digest.current ask in GMutex.fold (fun k v acc -> - if Digest.compatible ask current k then + if Digest.accounted_for ask ~current ~other:k then LD.join acc v else acc From 0704cd55cb41cdfb628f6ce96bc137515fd25149 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 5 Dec 2023 17:11:21 +0200 Subject: [PATCH 5/5] Flip Digest.accounted_for implementation to match name --- src/analyses/apron/relationPriv.apron.ml | 2 +- src/analyses/basePriv.ml | 2 +- src/analyses/commonPriv.ml | 12 ++++++------ 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 6c330e8798..31dd1fc4f5 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -864,7 +864,7 @@ struct let get_relevant_writes (ask:Q.ask) m v = let current = Digest.current ask in GMutex.fold (fun k v acc -> - if Digest.accounted_for ask ~current ~other: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 diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 26fb5850a8..20ef13244b 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -425,7 +425,7 @@ struct 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 Digest.accounted_for ask ~current ~other:k then + if not (Digest.accounted_for ask ~current ~other:k) then CPA.join acc (CPA.filter is_in_Gm v) else acc diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 5f89eecdd8..2739578957 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -175,14 +175,14 @@ struct match current, other with | `Lifted current, `Lifted other -> if TID.is_unique current && TID.equal current other then - false (* self-read *) + true (* self-read *) else if GobConfig.get_bool "ana.relation.priv.not-started" && MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other then - false (* other is not started yet *) + 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 - false (* accounted for in local information *) + true (* accounted for in local information *) else - true - | _ -> true + false + | _ -> false end module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) = @@ -247,7 +247,7 @@ struct let get_relevant_writes_nofilter (ask:Q.ask) v = let current = Digest.current ask in GMutex.fold (fun k v acc -> - if Digest.accounted_for ask ~current ~other:k then + if not (Digest.accounted_for ask ~current ~other:k) then LD.join acc v else acc