[thread-safety] infer accesses that need to be safe from lock usage

Summary:
Whenever we see a use of a lock, infer that the current method can run in a multithreaded context. But only report when there's a write under a lock that can be read or written without synchronization elsewhere.

For now, we only infer this based on the direct usage of a lock; we don't assume a caller runs in a multithreaded context just because its (transitive) callee can.
We can work on that trickier case later, and we can work on smarter inference that takes reads under sync into account. But for now, warning on unprotected writes of reads that occur under sync appears to be too noisy.

Reviewed By: jberdine

Differential Revision: D5918801

fbshipit-source-id: 2450cf2

infer/src/checkers/ThreadSafety.ml

@@ -658,11 +658,20 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           if is_thread_utils_method "assertMainThread" callee_pname then
             {astate with threads= ThreadsDomain.AnyThreadButSelf}
           else
+            (* if we don't have any evidence about whether the current function can run in parallel
+               with other threads or not, start assuming that it can. why use a lock if the function
+               can't run in a multithreaded context? *)
+            let update_for_lock_use = function
+              | ThreadsDomain.AnyThreadButSelf
+               -> ThreadsDomain.AnyThreadButSelf
+              | _
+               -> ThreadsDomain.AnyThread
+            in
             match get_lock_model callee_pname actuals with
             | Lock
-             -> {astate with locks= true}
+             -> {astate with locks= true; threads= update_for_lock_use astate.threads}
             | Unlock
-             -> {astate with locks= false}
+             -> {astate with locks= false; threads= update_for_lock_use astate.threads}
             | LockedIfTrue -> (
               match ret_opt with
               | Some ret_access_path
@@ -670,7 +679,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                     AttributeMapDomain.add_attribute (ret_access_path, []) (Choice Choice.LockHeld)
                       astate.attribute_map
                   in
-                  {astate with attribute_map}
+                  {astate with attribute_map; threads= update_for_lock_use astate.threads}
               | None
                -> L.(die InternalError)
                     "Procedure %a specified as returning boolean, but returns nothing"
@@ -1045,7 +1054,8 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
       let threads =
         if runs_on_ui_thread proc_desc || is_thread_confined_method tenv proc_desc then
           ThreadsDomain.AnyThreadButSelf
-        else if is_marked_thread_safe proc_desc tenv then ThreadsDomain.AnyThread
+        else if Procdesc.is_java_synchronized proc_desc || is_marked_thread_safe proc_desc tenv
+        then ThreadsDomain.AnyThread
         else ThreadsDomain.NoThread
       in
       let add_owned_local acc (name, typ) =
@@ -1456,10 +1466,13 @@ let report_unsafe_accesses
                     else None)
                   accesses
             in
-            report_thread_safety_violation tenv pdesc IssueType.thread_safety_violation
+            if List.is_empty writes_on_background_thread && not (ThreadsDomain.is_any thread) then
-              ~make_description:make_unprotected_write_description
+              reported_acc
-              ~report_kind:(WriteWriteRace writes_on_background_thread) access thread ;
+            else (
-            update_reported access pname reported_acc
+              report_thread_safety_violation tenv pdesc IssueType.thread_safety_violation
+                ~make_description:make_unprotected_write_description
+                ~report_kind:(WriteWriteRace writes_on_background_thread) access thread ;
+              update_reported access pname reported_acc )
         | _
          -> (* Do not report unprotected writes when an access can't run in parallel with itself, or
                for ObjC_Cpp *)
@@ -1478,13 +1491,17 @@ let report_unsafe_accesses
             | AccessPrecondition.Protected _
              -> true
           in
+          let is_conflict other_access pre other_thread =
+            TraceElem.is_write other_access
+            &&
+            if Typ.Procname.is_java pname then ThreadsDomain.is_any thread
+              || ThreadsDomain.is_any other_thread
+            else is_cpp_protected_write pre
+          in
           let all_writes =
             List.filter
               ~f:(fun (other_access, pre, other_thread, _, _) ->
-                TraceElem.is_write other_access
+                is_conflict other_access pre other_thread)
-                && ( not (Typ.Procname.is_java pname) || ThreadsDomain.is_any thread
-                   || ThreadsDomain.is_any other_thread )
-                && is_cpp_protected_write pre)
               accesses
           in
           if List.is_empty all_writes then reported_acc
@@ -1508,10 +1525,10 @@ let report_unsafe_accesses
           in
           let conflicting_writes =
             List.filter
-              ~f:(fun (access, pre, _, _, _) ->
+              ~f:(fun (access, pre, other_thread, _, _) ->
                 match pre with
                 | AccessPrecondition.Unprotected _
-                 -> TraceElem.is_write access
+                 -> TraceElem.is_write access && ThreadsDomain.is_any other_thread
                 | AccessPrecondition.Protected other_excl when is_opposite (excl, other_excl)
                  -> TraceElem.is_write access
                 | _

infer/tests/codetoanalyze/java/threadsafety/Inference.java

@@ -0,0 +1,75 @@
+/*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+package codetoanalyze.java.checkers;
+
+// test that we can infer when code needs to be thread-safe even without annotations
+public class Inference {
+
+  int mField1;
+
+  synchronized void writeUnderLock1Ok() {
+    mField1 = 1;
+  }
+
+  // should report because there's a write in a method that we think can run on multiple threads
+  int unprotectedRead1Bad() {
+    int ret = mField1;
+    return ret;
+  }
+
+  int mField2;
+
+  void writeUnderLock2Ok() {
+    synchronized (this) {
+      mField2 = 2;
+    }
+  }
+
+  int unprotectedRead2Bad() {
+    int ret = mField2;
+    return ret;
+  }
+
+  // TODO: handle these casely separately, since assuming that any method whose (transitive) callee
+  // uses a lock can run on multiple threads may cause a lot of false positives
+  int mField3;
+
+  // empty call that uses a lock
+  synchronized private void useLock() {
+  }
+
+  int useLockInCalleeThenReadBad() {
+    useLock();
+    return mField3;
+  }
+
+  void FN_writeToFieldWrittenInLockUsingMethodBad() {
+    mField3 = 3;
+  }
+
+  int mField4;
+  int mField5;
+
+  synchronized int readInsideSyncCoincidentally() {
+    mField4 = 4; // we will assume this needs to be protected...
+    int ret = mField5; // ...but not this
+    return ret;
+  }
+
+  int read4OutsideSyncBad() {
+    int ret = mField4; // report
+    return ret;
+  }
+
+  void write5OutsideSyncOk() {
+    mField5 = 5; // don't report
+  }
+
+}

infer/tests/codetoanalyze/java/threadsafety/ThreadSafeMethods.java

@@ -83,7 +83,7 @@ class ThreadSafeMethods {
   }
 
   @ThreadSafe
-  public synchronized Object synchronizedReadBad() {
+  public synchronized Object FN_synchronizedReadBad() {
     return this.field5;
   }
 
@@ -92,7 +92,7 @@ class ThreadSafeMethods {
   }
 
   // unprotected write to a field that is read safely in a method marked thread-safe
-  public void writeSameFieldAsThreadSafeMethod3Bad() {
+  public void FN_writeSameFieldAsThreadSafeMethod3Bad() {
     this.field5 = new Object();
   }
 

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

@@ -46,6 +46,9 @@ codetoanalyze/java/threadsafety/Containers.java, void Containers.mapSubclassWrit
 codetoanalyze/java/threadsafety/Containers.java, void Containers.poolBad(), 5, THREAD_SAFETY_VIOLATION, [Write to container `&this.codetoanalyze.java.checkers.Containers.simplePool` via call to `release`]
 codetoanalyze/java/threadsafety/Dispatch.java, void Dispatch.callUnannotatedInterfaceBad(UnannotatedInterface), 1, INTERFACE_NOT_THREAD_SAFE, [Call to un-annotated interface method void UnannotatedInterface.foo()]
 codetoanalyze/java/threadsafety/Dispatch.java, void Dispatch.callUnannotatedInterfaceIndirectBad(NotThreadSafe,UnannotatedInterface), 1, INTERFACE_NOT_THREAD_SAFE, [call to void NotThreadSafe.notThreadSafeOk(UnannotatedInterface),Call to un-annotated interface method void UnannotatedInterface.foo()]
+codetoanalyze/java/threadsafety/Inference.java, int Inference.read4OutsideSyncBad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField4`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField4`]
+codetoanalyze/java/threadsafety/Inference.java, int Inference.unprotectedRead1Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField1`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField1`]
+codetoanalyze/java/threadsafety/Inference.java, int Inference.unprotectedRead2Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField2`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField2`]
 codetoanalyze/java/threadsafety/Locks.java, void Locks.FP_unlockOneLock(), 4, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`]
 codetoanalyze/java/threadsafety/Locks.java, void Locks.afterReentrantLockUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`]
 codetoanalyze/java/threadsafety/Locks.java, void Locks.afterUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`]
@@ -102,7 +105,6 @@ codetoanalyze/java/threadsafety/ThreadSafeExample.java, void YesThreadSafeExtend
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.readSameFieldAsThreadSafeMethod1Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field1`,<Write trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field1`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.readSameFieldAsThreadSafeMethod2Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field4`,<Write trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field4`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.readSameFieldAsThreadSafeMethodWhileSynchronized1Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field1`,<Write trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field1`]
-codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.synchronizedReadBad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field5`,<Write trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field5`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.threadSafeMethodReadBad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field2`,<Write trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field2`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethodsSubclass.readThreadSafeFieldOfOverrideBad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethodsSubclass.subclassField`,<Write trace>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethodsSubclass.subclassField`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, void ThreadSafeMethods.threadSafeMethodWriteBad(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field1`]
@@ -110,6 +112,5 @@ codetoanalyze/java/threadsafety/ThreadSafeMethods.java, void ThreadSafeMethods.t
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, void ThreadSafeMethods.threadSafeVisibleForTestingMethodBad(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field3`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, void ThreadSafeMethods.writeSameFieldAsThreadSafeMethod1Bad(), 2, THREAD_SAFETY_VIOLATION, [<Write on unknown thread>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field1`,<Write on background thread>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field1`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, void ThreadSafeMethods.writeSameFieldAsThreadSafeMethod2Bad(), 1, THREAD_SAFETY_VIOLATION, [<Write on unknown thread>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field4`,<Write on background thread>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field4`]
-codetoanalyze/java/threadsafety/ThreadSafeMethods.java, void ThreadSafeMethods.writeSameFieldAsThreadSafeMethod3Bad(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field5`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, void ThreadSafeMethodsSubclass.safeMethodOverride(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.ThreadSafeMethodsSubclass.subclassField`]
 codetoanalyze/java/threadsafety/ThreadSafeMethods.java, void ThreadSafeMethodsSubclass.writeThreadSafeFieldOfOverrideBad(), 1, THREAD_SAFETY_VIOLATION, [<Write on unknown thread>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethodsSubclass.subclassField`,<Write on background thread>,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethodsSubclass.subclassField`]