Fix read-write lock access handling

src/analyses/mutexAnalysis.ml

@@ -158,19 +158,20 @@ struct
     include D
     let name () = "lock"
     let may_race ls1 ls2 =
-      is_empty (join ls1 ls2) (* D is reversed, so join is intersect *)
+      (* not mutually exclusive *)
+      not @@ D.exists (fun ((m1, w1) as l1) ->
+          if w1 then
+            (* write lock is exclusive with write lock or read lock *)
+            D.mem l1 ls2 || D.mem (m1, false) ls2
+          else
+            (* read lock is exclusive with just write lock *)
+            D.mem (m1, true) ls2
+        ) ls1
     let should_print ls = not (is_empty ls)
   end
 
   let access ctx (a: Queries.access) =
-    match a with
-    | Point
-    | Memory {write = true; _} ->
-      (* when writing: ignore reader locks *)
-      Lockset.filter snd ctx.local
-    | Memory _ ->
-      (* when reading: bump reader locks to exclusive as they protect reads *)
-      Lockset.map (fun (x,_) -> (x,true)) ctx.local
+    ctx.local
 
   (** Transfer functions: *)
 

src/cdomains/lockDomain.ml

@@ -32,17 +32,20 @@ struct
   (* pair Addr and RW; also change pretty printing*)
   module Lock =
   struct
-    module  L = Printable.Prod (Addr) (RW)
-    include L
+    include Printable.Prod (Addr) (RW)
 
-    let show (a,write) =
-      let addr_str = Addr.show a in
+    let pretty () (a, write) =
       if write then
-        addr_str
+        Addr.pretty () a
       else
-        "read lock " ^ addr_str
-
-    let pretty () x = text (show x)
+        Pretty.dprintf "read lock %a" Addr.pretty a
+
+    include Printable.SimplePretty (
+      struct
+        type nonrec t = t
+        let pretty = pretty
+      end
+      )
   end
 
   (* TODO: use SetDomain.Reverse *)
@@ -86,6 +89,8 @@ struct
   let filter = ReverseAddrSet.filter
   let fold = ReverseAddrSet.fold
   let singleton = ReverseAddrSet.singleton
+  let mem = ReverseAddrSet.mem
+  let exists = ReverseAddrSet.exists
 
   let export_locks ls =
     let f (x,_) set = Mutexes.add x set in

src/domains/access.ml

@@ -10,7 +10,7 @@ module M = Messages
 
 let is_ignorable_type (t: typ): bool =
   match t with
-  | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "spinlock_t"; _ }, _) -> true
+  | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "spinlock_t"; _ }, _) -> true
   | TComp ({ cname = "lock_class_key"; _ }, _) -> true
   | TInt (IInt, attr) when hasAttribute "mutex" attr -> true
   | t when hasAttribute "atomic" (typeAttrs t) -> true (* C11 _Atomic *)

tests/regression/04-mutex/40-rw_lock_rc.c

@@ -24,7 +24,7 @@ static ssize_t my_read(struct file *file, char __user *buf, size_t count, loff_t
 
 static ssize_t my_write(struct file *fp, const char __user *buf, size_t len, loff_t *off) {
   write_lock(&rwlock1);
-  data1 = data1==1 ? 0 : 1; //RACE!
+  data1 = data1==1 ? 0 : 1; //NORACE
   write_unlock(&rwlock1);
 
   write_lock(&rwlock2);

tests/regression/04-mutex/41-pt_rwlock.c

@@ -9,7 +9,7 @@ static pthread_rwlock_t rwlock = PTHREAD_RWLOCK_INITIALIZER;
 void *t_fun(void *arg) {
   pthread_rwlock_wrlock(&rwlock);
   data1++;            // NORACE
-  printf("%d",data2); // RACE
+  printf("%d",data2); // NORACE
   pthread_rwlock_unlock(&rwlock);
   return NULL;
 }
@@ -20,7 +20,7 @@ int main(void) {
 
   pthread_rwlock_rdlock(&rwlock);
   printf("%d",data1); // NORACE
-  data2++;            // RACE
+  data2++;            // NORACE
   pthread_rwlock_unlock(&rwlock);
 
   pthread_join (id, NULL);