diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index e7da810d8..d138ad9d2 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/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*) diff --git a/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java b/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java index e222a8902..59a404e1b 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java +++ b/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()) { diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index e07e96622..ab8833f27 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/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. ]