[thread-safety] report on protected write/unprotected read races

Summary: Previously, we wouldn't report races where the write was under synchronization.

Reviewed By: peterogithub

Differential Revision: D4658850

fbshipit-source-id: e9f4c41

infer/src/checkers/ThreadSafety.ml

@@ -529,8 +529,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         let writes =
           match lhs_exp with
           | Lfield (base_exp, _, typ) ->
-              if is_unprotected astate.locks (* abstracts no lock being held *) &&
-                 not (is_marked_functional rhs_exp lhs_typ astate.attribute_map)
+              if is_marked_functional rhs_exp lhs_typ astate.attribute_map
+              then
+                (* we want to forget about writes to @Functional fields altogether, otherwise we'll
+                   report spurious read/write races *)
+                astate.writes
+              else if is_unprotected astate.locks
               then
                 match get_formal_index base_exp typ with
                 | Some formal_index ->
@@ -853,11 +857,13 @@ let filter_conflicting_sinks sink trace =
    access-astate is a non-empty collection of conflicting
    write accesses*)
 let collect_conflicting_writes sink tab =
+  let open ThreadSafetyDomain in
   let procs_and_writes =
     List.map
       ~f:(fun (key,(_, _, writes, _)) ->
           let conflicting_writes =
-            get_possibly_unsafe_writes writes
+            AccessDomain.fold
+              (fun _ accesses acc -> PathDomain.join accesses acc) writes PathDomain.empty
             |> filter_conflicting_sinks sink in
           key, conflicting_writes
         )

infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java

@@ -14,8 +14,9 @@ import javax.annotation.concurrent.ThreadSafe;
 @ThreadSafe
 class ReadWriteRaces{
 
-Integer safe_read;
-Integer racy;
+  // read and write outside of sync races
+  Integer safe_read;
+  Integer racy;
 
   void m0_OK(){
    Integer local;
@@ -40,24 +41,40 @@ Integer racy;
    racy = 99;
   }
 
+  // write inside sync, read outside of sync races
+  Object field1;
+  Object field2;
+  Object field3;
+
   // need to report races involving safe writes in order to get this one
-  public synchronized void FN_syncWrite1() {
-    racy = 42;
+  public synchronized void syncWrite1() {
+    field1 = new Object();
+  }
+
+  public Object unprotectedRead1() {
+    return field1;
   }
 
-  public void FN_syncWrite2() {
+  public void syncWrite2() {
     synchronized(this) {
-      racy = 43;
+      field2 = new Object();
     }
   }
 
+  public Object unprotectedRead2() {
+    return field2;
+  }
+
   private synchronized void syncWrite3() {
-    racy = 44;
+    field3 = new Object();
   }
 
-  public void FN_callSyncWrite3() {
+  public void callSyncWrite3() {
     syncWrite3();
   }
 
+  public Object unprotectedRead3() {
+    return field3;
+  }
 
 }

infer/tests/codetoanalyze/java/threadsafety/issues.exp

@@ -48,6 +48,9 @@ codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedIn
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad2(), 2, THREAD_SAFETY_VIOLATION, [call to void Ownership.writeToFormal(Obj),access to codetoanalyze.java.checkers.Obj.f]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad3(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to codetoanalyze.java.checkers.Obj.f]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToOwnedInCalleeOk2(), 4, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Ownership.field]
+codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead1(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.field1]
+codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead2(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.field2]
+codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead3(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.field3]
 codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m1(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.racy]
 codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m2(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.racy]
 codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m3(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.racy]