Use variant type for kind of protection instead of bool

src/analyses/basePriv.ml

@@ -653,7 +653,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 ->
@@ -771,7 +771,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. *)

src/analyses/commonPriv.ml

@@ -82,26 +82,28 @@ end
 module Protection =
 struct
   open Q.Protection
+  open Q.ProtectionKind
+
   let is_unprotected ask ?(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=true; protection})
+      ask.f (Q.MayBePublic {global=x; kind=Write; 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 ?(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=true; protection})
+    ask.f (Q.MustBeProtectedBy {mutex=m; global=x; kind=Write; 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

@@ -60,25 +60,31 @@ 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:Queries.ProtectionKind.t -> 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 =
+      let make ~kind ~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 wlocks =
+          match kind with
+          | Queries.ProtectionKind.Write -> locks
+          | ReadWrite -> MustLockset.all ()
+        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 ()))
@@ -90,17 +96,16 @@ struct
     (** 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 =
@@ -196,28 +201,28 @@ struct
   let query (ctx: (D.t, _, _, V.t) ctx) (type a) (q: a Queries.t): a Queries.result =
     let ls, m = ctx.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 (ctx.global (V.protecting v))) in
+    let protecting ~kind mode v = GProtecting.get ~kind mode (G.protecting (ctx.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 ctx.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) ctx.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
@@ -229,8 +234,8 @@ struct
     | 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 (ctx.global (V.protected mutex))) in
+    | Queries.MustProtectedVars {mutex; kind} ->
+      let protected = GProtected.get ~kind Strong (G.protected (ctx.global (V.protected mutex))) in
       VarSet.fold (fun v acc ->
           Queries.VS.add v acc
         ) protected (Queries.VS.empty ())
@@ -241,13 +246,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 (ctx.global g)) in (* readwrite protecting *)
+            let protecting = GProtecting.get ~kind:ReadWrite Strong (G.protecting (ctx.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 (ctx.global g)) in (* readwrite protected *)
+            let protected = GProtected.get ~kind:ReadWrite Strong (G.protected (ctx.global g)) in (* readwrite protected *)
             let s = VarSet.cardinal protected in
             max_protected := max !max_protected s;
             sum_protected := !sum_protected + s;
@@ -289,21 +294,21 @@ struct
         | Some v ->
           if not (MustLocksetRW.is_all (fst octx.local)) then
             let locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd (fst octx.local)) in
-            let write = match kind with
-              | Write | Free -> true
-              | Read -> false
+            let kind = match kind with
+              | Write | Free -> Queries.ProtectionKind.Write
+              | Read -> ReadWrite
               | Call
-              | Spawn -> false (* TODO: nonsense? *)
+              | Spawn -> ReadWrite (* 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
             ctx.sideg (V.protecting v) (G.create_protecting s);
 
             if !AnalysisState.postsolving then (
-              let protecting mode = GProtecting.get ~write mode (G.protecting (ctx.global (V.protecting v))) in
+              let protecting mode = GProtecting.get ~kind mode (G.protecting (ctx.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
+              let protected = G.create_protected @@ GProtected.make ~kind vs in
               MustLockset.iter (fun ml -> ctx.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

src/domains/queries.ml

@@ -36,6 +36,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
@@ -48,10 +53,10 @@ module Protection = 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 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 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. *)