From bda139ff7d12e2b59b20b289d89c60fdeef37304 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 5 Dec 2023 17:09:32 +0200 Subject: [PATCH 1/2] 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 2/2] 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