[thread-safety] interprocedural analysis

Summary: Adding this so we can test interprocedural trace-based reporting in a subsequent diff.

Reviewed By: peterogithub

Differential Revision: D4243046

fbshipit-source-id: 7d07f20

infer/src/checkers/ThreadSafety.ml

@@ -63,16 +63,32 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       pathdomainstate
       (AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None))
 
-  let exec_instr ((lockstate, (readstate,writestate)) as astate) { ProcData.pdesc; } _ =
+  let exec_instr ((lockstate, (readstate,writestate)) as astate) { ProcData.pdesc; tenv } _ =
     let is_unprotected is_locked =
       not is_locked && not (Procdesc.is_java_synchronized pdesc) in
     function
     | Sil.Call (_, Const (Cfun pn), _, _, _) ->
-        let lockstate' = match get_lock_model pn with
-          | Lock -> true
-          | Unlock -> false
-          | None -> lockstate in
-        lockstate', snd astate
+        begin
+          (* assuming that modeled procedures do not have useful summaries *)
+          match get_lock_model pn with
+          | Lock ->
+              true, snd astate
+          | Unlock ->
+              false, snd astate
+          | None ->
+              begin
+                match Summary.read_summary tenv pdesc pn with
+                | Some ((callee_lockstate, _) as summary) ->
+                    let lockstate' = callee_lockstate || lockstate in
+                    let _, read_writestate' =
+                      if is_unprotected lockstate'
+                      then ThreadSafetyDomain.join summary astate
+                      else astate in
+                    lockstate', read_writestate'
+                | None ->
+                    astate
+              end
+        end
 
     | Sil.Store ((Lfield ( _, _, typ) as lhsfield) , _, _, _) ->
         if is_unprotected lockstate then (* abstracts no lock being held*)

infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java

@@ -77,6 +77,32 @@ public class ThreadSafeExample{
     mLock.unlock();
   }
 
+  // shouldn't report here because it's a private method
+  private void assignInPrivateMethodOk() {
+    f = 24;
+  }
+
+  // but should report here, because now it's called
+  public void callPublicMethodBad() {
+    assignInPrivateMethodOk();
+  }
+
+  public synchronized void callFromSynchronizedPublicMethodOk() {
+    assignInPrivateMethodOk();
+  }
+
+  private synchronized void synchronizedCallerOk() {
+    assignInPrivateMethodOk();
+  }
+
+  public void callFromUnsynchronizedPublicMethodOk() {
+    synchronizedCallerOk();
+  }
+
+  // doesn't work because we don't model lock
+  public void FP_tsWithLockOk() {
+  }
+
   public void withLockBothBranchesOk(boolean b) {
     if (b) {
       mLock.lock();
@@ -106,7 +132,21 @@ public class ThreadSafeExample{
     mReentrantLock.unlock();
   }
 
-  // our "squish all locks into one" abstraction is not ideal here
+  private void acquireLock() {
+    mLock.lock();
+  }
+
+  public void acquireLockInCalleeOk() {
+    acquireLock();
+    f = 42;
+    mLock.unlock();
+  }
+
+  private void releaseLock() {
+    mLock.unlock();
+  }
+
+  // our "squish all locks into one" abstraction is not ideal here...
   public void FP_unlockOneLock() {
     mLock.lock();
     mReentrantLock.lock();
@@ -115,6 +155,13 @@ public class ThreadSafeExample{
     mLock.unlock();
   }
 
+  // ... or here
+  public void FN_releaseLockInCalleeBad() {
+    mLock.lock();
+    releaseLock();
+    f = 42;
+  }
+
   // we don't model the case where `tryLock` fails
   public void FN_withReentrantLockTryLockBad() {
     if (!mReentrantLock.tryLock()) {

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

@@ -5,5 +5,6 @@ codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeEx
 codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.FP_unlockOneLock(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.FP_unlockOneLock() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]
 codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.afterReentrantLockUnlockBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.afterReentrantLockUnlockBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]
 codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.afterUnlockBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.afterUnlockBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]
+codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.callPublicMethodBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.callPublicMethodBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]
 codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.lockInOneBranchBad(boolean), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.lockInOneBranchBad(boolean) writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]
 codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.tsBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.tsBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]