Merge pull request #1788 from goblint/mutex-refactor-readwrite

Fix variables protected by mutex calculation

Author: sim642

src/analyses/basePriv.ml

@@ -370,7 +370,7 @@ struct
       if atomic || ask.f (GhostVarAvailable (Locked m')) then (
         let cpa = get_m_with_mutex_inits ask getg m' in (* Could be more precise if mutex_inits invariant is added by disjunction instead of joining abstract values. *)
         let inv = CPA.fold (fun v _ acc ->
-            if ask.f (MustBeProtectedBy {mutex = m'; global = v; write = true; protection = Strong}) then
+            if ask.f (MustBeProtectedBy {mutex = m'; global = v; kind = Write; protection = Strong}) then
               let inv = ValueDomain.invariant_global (fun g -> CPA.find g cpa) v in
               Invariant.(acc && inv)
             else
@@ -706,7 +706,7 @@ struct
 
   let threadspawn (ask:Queries.ask) get set (st: BaseComponents (D).t) =
     let is_recovered_st = ask.f (Queries.MustBeSingleThreaded {since_start = false}) && not @@ ask.f (Queries.MustBeSingleThreaded {since_start = true}) in
-    let unprotected_after x = ask.f (Q.MayBePublic {global=x; write=true; protection=Weak}) in
+    let unprotected_after x = ask.f (Q.MayBePublic {global=x; kind=Write; protection=Weak}) in
     if is_recovered_st then
       (* Remove all things that are now unprotected *)
       let cpa' = CPA.fold (fun x v cpa ->
@@ -750,14 +750,14 @@ struct
   let startstate () = ()
 
   let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
-    if is_unprotected ask ~write:false x then
+    if is_unprotected ask ~kind:ReadWrite x then
       VD.join (CPA.find x st.cpa) (getg x)
     else
       CPA.find x st.cpa
 
   let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
     if not invariant then (
-      if is_unprotected ask ~write:false x then
+      if is_unprotected ask ~kind:ReadWrite x then
         sideg x v;
       if !earlyglobs then (* earlyglobs workaround for 13/60 *)
         sideg x v (* TODO: is this needed for anything? 13/60 doesn't work for other reasons *)
@@ -766,7 +766,7 @@ struct
 
   let lock ask getg (st: BaseComponents (D).t) m =
     let cpa' = CPA.mapi (fun x v ->
-        if is_protected_by ask ~write:false m x && is_unprotected ask ~write:false x then (* is_in_Gm *)
+        if is_protected_by ask ~kind:ReadWrite m x && is_unprotected ask ~kind:ReadWrite x then (* is_in_Gm *)
           VD.join (CPA.find x st.cpa) (getg x)
         else
           v
@@ -776,8 +776,8 @@ struct
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     CPA.iter (fun x v  ->
-        if is_protected_by ask ~write:false m x then ( (* is_in_Gm *)
-          if is_unprotected_without ask ~write:false x m then (* is_in_V' *)
+        if is_protected_by ask ~kind:ReadWrite m x then ( (* is_in_Gm *)
+          if is_unprotected_without ask ~kind:ReadWrite x m then (* is_in_V' *)
             sideg x v
         )
       ) st.cpa;
@@ -787,7 +787,7 @@ struct
     let branched_sync () =
       (* required for branched thread creation *)
       CPA.iter (fun x v ->
-          if is_global ask x && is_unprotected ask ~write:false x then
+          if is_global ask x && is_unprotected ask ~kind:ReadWrite x then
             sideg x v
         ) st.cpa;
       st
@@ -832,7 +832,7 @@ struct
     | _ -> ()
 
   let invariant_global (ask: Q.ask) getg g =
-    let locks = ask.f (Q.MustProtectingLocks {global = g; write = false}) in
+    let locks = ask.f (Q.MustProtectingLocks {global = g; kind = ReadWrite}) in
     if LockDomain.MustLockset.is_all locks then
       Invariant.none
     else (
@@ -988,7 +988,7 @@ struct
                 (* Extra precision in implementation to pass tests:
                    If global is read-protected by multiple locks,
                    then inner unlock shouldn't yet publish. *)
-                if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then
+                if not Param.check_read_unprotected || is_unprotected_without ask ~kind:ReadWrite x m then
                   sideg (V.protected x) v;
                 if atomic then
                   sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *)
@@ -1076,7 +1076,7 @@ struct
     | `Left g' -> (* unprotected *)
       ValueDomain.invariant_global (fun g -> getg (V.unprotected g)) g'
     | `Right g' -> (* protected *)
-      let locks = ask.f (Q.MustProtectingLocks {global = g'; write = true}) in
+      let locks = ask.f (Q.MustProtectingLocks {global = g'; kind = Write}) in
       if LockDomain.MustLockset.is_all locks || LockDomain.MustLockset.is_empty locks then
         Invariant.none
       else if VD.equal (getg (V.protected g')) (getg (V.unprotected g')) then

src/analyses/commonPriv.ml

@@ -82,26 +82,28 @@ end
 module Protection =
 struct
   open Q.Protection
-  let is_unprotected ask ?(write=true) ?(protection=Strong) x: bool =
+  open Q.ProtectionKind
+
+  let is_unprotected ask ?(kind=Write) ?(protection=Strong) x: bool =
     let multi = if protection = Weak then ThreadFlag.is_currently_multi ask else ThreadFlag.has_ever_been_multi ask in
     (!GobConfig.earlyglobs && not multi && not (is_excluded_from_earlyglobs x)) ||
     (
       multi &&
-      ask.f (Q.MayBePublic {global=x; write; protection})
+      ask.f (Q.MayBePublic {global=x; kind; protection})
     )
 
-  let is_unprotected_without ask ?(write=true) ?(protection=Strong) x m: bool =
+  let is_unprotected_without ask ?(kind=Write) ?(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=m; protection})
+    ask.f (Q.MayBePublicWithout {global=x; kind; without_mutex=m; protection})
 
-  let is_protected_by ask ?(write=true) ?(protection=Strong) m x: bool =
+  let is_protected_by ask ?(kind=Write) ?(protection=Strong) m x: bool =
     is_global ask x &&
     not (VD.is_immediate_type x.vtype) &&
-    ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write; protection})
+    ask.f (Q.MustBeProtectedBy {mutex=m; global=x; kind; protection})
 
   let protected_vars (ask: Q.ask): varinfo list =
     LockDomain.MustLockset.fold (fun ml acc ->
-        Q.VS.join (ask.f (Q.MustProtectedVars {mutex = ml; write = true})) acc
+        Q.VS.join (ask.f (Q.MustProtectedVars {mutex = ml; kind = Write})) acc
       ) (ask.f Q.MustLockset) (Q.VS.empty ())
     |> Q.VS.elements
 end

src/analyses/mutexAnalysis.ml

@@ -13,6 +13,8 @@ open Analyses
 
 module VarSet = SetDomain.Make (Basetype.Variables)
 
+type access_kind = Read | Write
+
 module Spec =
 struct
   module Arg =
@@ -59,47 +61,51 @@ struct
 
       let name () = "strong protection * weak protection"
 
-      let get ~write protection (s,w) =
+      let get ~kind protection (s,w) =
         let (rw, w) = match protection with
           | Queries.Protection.Strong -> s
           | Weak -> w
         in
-        if write then w else rw
+        match kind with
+        | Queries.ProtectionKind.Write -> w
+        | ReadWrite -> rw
     end
 
     (** Collects information about which variables are protected by which mutexes *)
     module GProtecting: sig
       include Lattice.S
-      val make: write:bool -> recovered:bool -> MustLockset.t -> t
-      val get: write:bool -> Queries.Protection.t -> t -> MustLockset.t
+      val make: kind:access_kind -> recovered:bool -> MustLockset.t -> t
+      val get: kind:Queries.ProtectionKind.t -> Queries.Protection.t -> t -> MustLockset.t
     end = struct
       include MakeP (MustLockset)
 
-      let make ~write ~recovered locks =
-        (* If the access is not a write, set to T so intersection with current write-protecting is identity *)
-        let wlocks = if write then locks else MustLockset.all () in
+      let make ~(kind: access_kind) ~recovered locks =
+        let locks =
+          match kind with
+          | Write -> (locks, locks)
+          | Read -> (locks, MustLockset.all ()) (* If the access is not a write, set to T so intersection with current write-protecting is identity *)
+        in
         if recovered then
           (* If we are in single-threaded mode again, this does not need to be added to set of mutexes protecting in mt-mode only *)
-          ((locks, wlocks), (MustLockset.all (), MustLockset.all ()))
+          (locks, (MustLockset.all (), MustLockset.all ()))
         else
-          ((locks, wlocks), (locks, wlocks))
+          (locks, locks)
     end
 
 
     (** Collects information about which mutex protects which variable *)
     module GProtected: sig
       include Lattice.S
-      val make: write:bool -> VarSet.t -> t
-      val get: write:bool -> Queries.Protection.t -> t -> VarSet.t
+      val make: kind:Queries.ProtectionKind.t -> VarSet.t -> t
+      val get: kind:Queries.ProtectionKind.t -> Queries.Protection.t -> t -> VarSet.t
     end = struct
       include MakeP (VarSet)
 
-      let make ~write vs =
+      let make ~kind vs =
         let vs_empty = VarSet.empty () in
-        if write then
-          ((vs_empty, vs), (vs_empty, vs))
-        else
-          ((vs, vs_empty), (vs, vs_empty))
+        match kind with
+        | Queries.ProtectionKind.Write -> ((vs_empty, vs), (vs_empty, vs))
+        | ReadWrite -> ((vs, vs_empty), (vs, vs_empty))
     end
 
     module G =
@@ -198,43 +204,43 @@ struct
   let query (man: (D.t, _, _, V.t) man) (type a) (q: a Queries.t): a Queries.result =
     let ls, m = man.local in
     (* get the set of mutexes protecting the variable v in the given mode *)
-    let protecting ~write mode v = GProtecting.get ~write mode (G.protecting (man.global (V.protecting v))) in
+    let protecting ~kind mode v = GProtecting.get ~kind mode (G.protecting (man.global (V.protecting v))) in
     match q with
     | Queries.MayBePublic _ when MustLocksetRW.is_all ls -> false
-    | Queries.MayBePublic {global=v; write; protection} ->
+    | Queries.MayBePublic {global=v; kind; protection} ->
       let held_locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd ls) in
-      let protecting = protecting ~write protection v in
+      let protecting = protecting ~kind protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
       (* if Mutexes.mem verifier_atomic (Lockset.export_locks man.local) then
         false
       else *)
       MustLockset.disjoint held_locks protecting
     | Queries.MayBePublicWithout _ when MustLocksetRW.is_all ls -> false
-    | Queries.MayBePublicWithout {global=v; write; without_mutex; protection} ->
+    | Queries.MayBePublicWithout {global=v; kind; without_mutex; protection} ->
       let held_locks = MustLockset.remove without_mutex (MustLocksetRW.to_must_lockset ls) in
-      let protecting = protecting ~write protection v in
+      let protecting = protecting ~kind 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) man.local)) then
         false
       else *)
       MustLockset.disjoint held_locks protecting
-    | Queries.MustBeProtectedBy {mutex = ml; global=v; write; protection} ->
-      let protecting = protecting ~write protection v in
+    | Queries.MustBeProtectedBy {mutex = ml; global=v; kind; protection} ->
+      let protecting = protecting ~kind 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
         true
       else *)
       MustLockset.mem ml protecting
-    | Queries.MustProtectingLocks {global; write} ->
-      protecting ~write Strong global
+    | Queries.MustProtectingLocks {global; kind} ->
+      protecting ~kind Strong global
     | Queries.MustLockset ->
       let held_locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd ls) in
       held_locks
     | Queries.MustBeAtomic ->
       let held_locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd ls) in
       MustLockset.mem (LF.verifier_atomic_var, `NoOffset) held_locks (* TODO: Mval.of_var *)
-    | Queries.MustProtectedVars {mutex; write} ->
-      let protected = GProtected.get ~write Strong (G.protected (man.global (V.protected mutex))) in
+    | Queries.MustProtectedVars {mutex; kind} ->
+      let protected = GProtected.get ~kind Strong (G.protected (man.global (V.protected mutex))) in
       VarSet.fold (fun v acc ->
           Queries.VS.add v acc
         ) protected (Queries.VS.empty ())
@@ -245,13 +251,13 @@ struct
       begin match g with
         | `Left g' -> (* protecting *)
           if GobConfig.get_bool "dbg.print_protection" then (
-            let protecting = GProtecting.get ~write:false Strong (G.protecting (man.global g)) in (* readwrite protecting *)
+            let protecting = GProtecting.get ~kind:ReadWrite Strong (G.protecting (man.global g)) in (* readwrite protecting *)
             let s = MustLockset.cardinal protecting in
             M.info_noloc ~category:Race "Variable %a read-write protected by %d mutex(es): %a" CilType.Varinfo.pretty g' s MustLockset.pretty protecting
           )
         | `Right m -> (* protected *)
           if GobConfig.get_bool "dbg.print_protection" then (
-            let protected = GProtected.get ~write:false Strong (G.protected (man.global g)) in (* readwrite protected *)
+            let protected = GProtected.get ~kind:ReadWrite Strong (G.protected (man.global g)) in (* readwrite protected *)
             let s = VarSet.cardinal protected in
             max_protected := max !max_protected s;
             sum_protected := !sum_protected + s;
@@ -293,25 +299,34 @@ struct
         | Some v ->
           if not (MustLocksetRW.is_all (fst oman.local)) then
             let locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd (fst oman.local)) in
-            let write = match kind with
-              | Write | Free -> true
-              | Read -> false
+            let kind = match kind with
+              | Write | Free -> Write
+              | Read -> Read
               | Call
-              | Spawn -> false (* TODO: nonsense? *)
+              | Spawn -> Read (* TODO: nonsense? *)
             in
-            let s = GProtecting.make ~write ~recovered:is_recovered_to_st locks in
+            let s = GProtecting.make ~kind ~recovered:is_recovered_to_st locks in
             man.sideg (V.protecting v) (G.create_protecting s);
 
             if !AnalysisState.postsolving then (
-              let protecting mode = GProtecting.get ~write mode (G.protecting (man.global (V.protecting v))) in
-              let held_strong = protecting Strong in
-              let held_weak = protecting Weak in
-              let vs = VarSet.singleton v in
-              let protected = G.create_protected @@ GProtected.make ~write vs in
-              MustLockset.iter (fun ml -> man.sideg (V.protected ml) protected) held_strong;
-              (* If the mutex set here is top, it is actually not accessed *)
-              if is_recovered_to_st && not @@ MustLockset.is_all held_weak then
-                MustLockset.iter (fun ml -> man.sideg (V.protected ml) protected) held_weak;
+              let side_protected kind mode =
+                let protecting = GProtecting.get ~kind mode (G.protecting (man.global (V.protecting v))) in
+                (* If the mutex set here is top, it is actually not accessed *)
+                if not @@ MustLockset.is_all protecting then (
+                  let vs = VarSet.singleton v in
+                  let protected = G.create_protected @@ GProtected.make ~kind vs in
+                  MustLockset.iter (fun ml -> man.sideg (V.protected ml) protected) protecting
+                )
+              in
+              let side_protected kind =
+                side_protected kind Strong;
+                if is_recovered_to_st then
+                  side_protected kind Weak
+              in
+              side_protected Queries.ProtectionKind.ReadWrite;
+              match kind with
+              | Write -> side_protected Queries.ProtectionKind.Write
+              | Read -> ()
             )
         | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound."
       in

src/domains/queries.ml

@@ -39,6 +39,11 @@ module MustBool = BoolDomain.MustBool
 
 module Unit = Lattice.Unit
 
+module ProtectionKind =
+struct
+  type t = ReadWrite | Write [@@deriving ord, hash]
+end
+
 (** Different notions of protection for a global variables g by a mutex m
     m protects g strongly if:
     - whenever g is accessed after the program went multi-threaded for the first time, m is held
@@ -55,11 +60,11 @@ module AllocationLocation = struct
 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: 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 mustprotectinglocks = {global: CilType.Varinfo.t; write: bool} [@@deriving ord, hash]
+type maybepublic = {global: CilType.Varinfo.t; kind: ProtectionKind.t; protection: Protection.t} [@@deriving ord, hash]
+type maybepublicwithout = {global: CilType.Varinfo.t; kind: ProtectionKind.t; without_mutex: LockDomain.MustLock.t; protection: Protection.t} [@@deriving ord, hash]
+type mustbeprotectedby = {mutex: LockDomain.MustLock.t; global: CilType.Varinfo.t; kind: ProtectionKind.t; protection: Protection.t} [@@deriving ord, hash]
+type mustprotectedvars = {mutex: LockDomain.MustLock.t; kind: ProtectionKind.t} [@@deriving ord, hash]
+type mustprotectinglocks = {global: CilType.Varinfo.t; kind: ProtectionKind.t} [@@deriving ord, hash]
 type access =
   | Memory of {exp: CilType.Exp.t; var_opt: CilType.Varinfo.t option; kind: AccessKind.t} (** Memory location access (race). *)
   | Point (** Program point and state access (MHP), independent of memory location. *)

tests/regression/13-privatized/19-publish-precision.t

@@ -0,0 +1,21 @@
+  $ goblint --enable dbg.print_protection --enable warn.deterministic 19-publish-precision.c
+  [Warning][Assert] Assertion "glob1 == 0" is unknown. (19-publish-precision.c:30:3-30:30)
+  [Warning][Assert] Assertion "glob1 == 5" is unknown. (19-publish-precision.c:31:3-31:30)
+  [Success][Assert] Assertion "glob1 == 5" will succeed (19-publish-precision.c:17:3-17:30)
+  [Success][Assert] Assertion "glob1 == 0" will succeed (19-publish-precision.c:27:3-27:30)
+  [Info][Race] Mutex mutex1 read-write protects 0 variable(s): {}
+  [Info][Race] Mutex mutex2 read-write protects 1 variable(s): {glob1}
+  [Info][Race] Variable glob1 read-write protected by 1 mutex(es): {mutex2}
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+  [Info][Race] Mutex read-write protection summary:
+    Number of mutexes: 2
+    Max number variables of protected by a mutex: 1
+    Total number of protected variables (including duplicates): 1
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 20
+    dead: 0
+    total lines: 20

tests/regression/13-privatized/20-publish-regression.t

@@ -0,0 +1,20 @@
+  $ goblint --enable dbg.print_protection --enable warn.deterministic 20-publish-regression.c
+  [Success][Assert] Assertion "glob1 == 5" will succeed (20-publish-regression.c:20:3-20:30)
+  [Success][Assert] Assertion "glob1 == 0" will succeed (20-publish-regression.c:29:3-29:30)
+  [Success][Assert] Assertion "glob1 == 0" will succeed (20-publish-regression.c:32:3-32:30)
+  [Info][Race] Mutex mutex1 read-write protects 1 variable(s): {glob1}
+  [Info][Race] Mutex mutex2 read-write protects 0 variable(s): {}
+  [Info][Race] Variable glob1 read-write protected by 1 mutex(es): {mutex1}
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+  [Info][Race] Mutex read-write protection summary:
+    Number of mutexes: 2
+    Max number variables of protected by a mutex: 1
+    Total number of protected variables (including duplicates): 1
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 19
+    dead: 0
+    total lines: 19