Refine MustBeProtectedBy and MayBePublicWithout query mutex type

goblint · Jun 4, 2024 · 90fc5aa · 90fc5aa
1 parent 500b452
commit 90fc5aa
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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). *)