From 90fc5aa1af4b0b734289917c3f713b5bf326a408 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 4 Jun 2024 16:51:16 +0300 Subject: [PATCH] Refine MustBeProtectedBy and MayBePublicWithout query mutex type --- src/analyses/commonPriv.ml | 4 ++-- src/analyses/mutexAnalysis.ml | 5 ++--- src/domains/queries.ml | 4 ++-- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 257fe9a038..3673991fda 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -74,12 +74,12 @@ struct let is_unprotected_without ask ?(write=true) ?(protection=Strong) x m: bool = (if protection = Weak then ThreadFlag.is_currently_multi ask else ThreadFlag.has_ever_been_multi ask) && - ask.f (Q.MayBePublicWithout {global=x; write; without_mutex=Addr (LockDomain.MustLock.to_mval m); protection}) (* TODO: no mutex conversion? *) + ask.f (Q.MayBePublicWithout {global=x; write; without_mutex=m; protection}) let is_protected_by ask ?(protection=Strong) m x: bool = is_global ask x && not (VD.is_immediate_type x.vtype) && - ask.f (Q.MustBeProtectedBy {mutex=Addr (LockDomain.MustLock.to_mval m); global=x; write=true; protection}) (* TODO: no mutex conversion? *) + ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write=true; protection}) let protected_vars (ask: Q.ask): varinfo list = LockDomain.MustLockset.fold (fun ml acc -> diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index b44795b6da..9b6aa4f4ca 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -209,15 +209,14 @@ struct MustLockset.disjoint held_locks protecting | Queries.MayBePublicWithout _ when MustLocksetRW.is_all ls -> false | Queries.MayBePublicWithout {global=v; write; without_mutex; protection} -> - let held_locks = MustLocksetRW.to_must_lockset @@ fst @@ Arg.remove' ctx ~warn:false without_mutex in + let held_locks = MustLockset.remove without_mutex (MustLocksetRW.to_must_lockset ls) in let protecting = protecting ~write protection v in (* TODO: unsound in 29/24, why did we do this before? *) (* if Mutexes.mem verifier_atomic (Lockset.export_locks (Lockset.remove (without_mutex, true) ctx.local)) then false else *) MustLockset.disjoint held_locks protecting - | Queries.MustBeProtectedBy {mutex = Addr mutex_mv; global=v; write; protection} when Mval.is_definite mutex_mv -> (* only definite Addrs can be in must-locksets to begin with, anything else cannot protect anything *) - let ml = LockDomain.MustLock.of_mval mutex_mv in + | Queries.MustBeProtectedBy {mutex = ml; global=v; write; protection} -> let protecting = protecting ~write protection v in (* TODO: unsound in 29/24, why did we do this before? *) (* if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then diff --git a/src/domains/queries.ml b/src/domains/queries.ml index a904f696eb..edb5c44c56 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -49,8 +49,8 @@ end (* Helper definitions for deriving complex parts of Any.compare below. *) type maybepublic = {global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash] -type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: PreValueDomain.Addr.t; protection: Protection.t} [@@deriving ord, hash] -type mustbeprotectedby = {mutex: PreValueDomain.Addr.t; global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash] +type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: LockDomain.MustLock.t; protection: Protection.t} [@@deriving ord, hash] +type mustbeprotectedby = {mutex: LockDomain.MustLock.t; global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash] type mustprotectedvars = {mutex: LockDomain.MustLock.t; write: bool} [@@deriving ord, hash] type access = | Memory of {exp: CilType.Exp.t; var_opt: CilType.Varinfo.t option; kind: AccessKind.t} (** Memory location access (race). *)