Replace readwrite protection with read protection

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

@@ -43,10 +43,10 @@ struct
     end
 
     module MakeP (G0: Lattice.S) = struct
-      module ReadWrite =
+      module Read =
       struct
         include G0
-        let name () = "readwrite"
+        let name () = "read"
       end
 
       module Write =
@@ -55,52 +55,59 @@ struct
         let name () = "write"
       end
 
-      module P = Lattice.Prod (ReadWrite) (Write)
+      module P = Lattice.Prod (Read) (Write)
       include Lattice.Prod (P) (P)
 
       let name () = "strong protection * weak protection"
 
-      let get ~write protection (s,w) =
-        let (rw, w) = match protection with
+      let get ~kind protection (s,w) =
+        let (r, w) = match protection with
           | Queries.Protection.Strong -> s
           | Weak -> w
         in
-        if write then w else rw
+        match kind with
+        | Queries.ProtectionKind.Write -> w
+        | Read -> r
+        | ReadWrite -> G0.join r w
     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 =
-        (* 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 ~recovered locks =
+        let locks =
+          match kind with
+          | Queries.ProtectionKind.Write -> (MustLockset.all (), locks)
+          | Read -> (locks, MustLockset.all ()) (* If the access is not a write, set to T so intersection with current write-protecting is identity *)
+          | ReadWrite -> (locks, locks) (* TODO: should never happen? *)
+        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))
+        | Read -> ((vs, vs_empty), (vs, vs_empty))
+        | ReadWrite -> ((vs, vs), (vs, vs)) (* TODO: should never happen? *)
     end
 
     module G =
@@ -196,28 +203,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 +236,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 +248,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 +296,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 -> 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
             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 = Read | 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. *)

tests/regression/13-privatized/56-aget_extern_init_minimal.c

@@ -1,7 +1,7 @@
 // SKIP
 #include <pthread.h>
 #include <stdlib.h>
-
+// NOCHECK
 extern int optind ;
 
 pthread_t hthread  ;

tests/regression/13-privatized/95-protection-read-only.c

@@ -0,0 +1,34 @@
+// PARAM: --enable ana.int.enums --set ana.base.privatization protection-read
+#include <pthread.h>
+#include <goblint.h>
+
+int g = 0;
+pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&m);
+  int x = g;
+  __goblint_check(x == 0); // UNKNOWN!
+  __goblint_check(x == 1); // UNKNOWN!
+  __goblint_check(x != 2); // TODO
+  __goblint_check(x == 3); // UNKNOWN!
+  pthread_mutex_unlock(&m);
+  return NULL;
+}
+
+void *t_fun2(void *arg) {
+  pthread_mutex_lock(&m);
+  g = 2; // not observable by t_fun
+  g = 3;
+  pthread_mutex_unlock(&m);
+  return NULL;
+}
+
+int main() {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_create(&id2, NULL, t_fun2, NULL);
+
+  g = 1; // unprotected write, do g has no write or read+write protection, but is still read-protected by m!
+  return 0;
+}