From 937ae12f2929371b97f9228a892f7a3d555bfb6a Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 30 Nov 2016 09:09:01 -0800 Subject: [PATCH] [thread-safety] adding models for lock methods Summary: We're at risk for some silly false positives without these models. Reviewed By: peterogithub Differential Revision: D4244795 fbshipit-source-id: b0367e6 --- infer/src/checkers/ThreadSafety.ml | 39 ++++++++++--- .../java/threadsafety/ThreadSafeExample.java | 57 +++++++++++++++++-- .../java/threadsafety/issues.exp | 7 ++- 3 files changed, 87 insertions(+), 16 deletions(-) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 454c0dd4c..e7da810d8 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -29,9 +29,32 @@ module TransferFunctions (CFG : ProcCfg.S) = struct module Domain = ThreadSafetyDomain type extras = ProcData.no_extras - let is_lock_procedure pn = Procname.equal pn BuiltinDecl.__set_locked_attribute - - let is_unlock_procedure pn = Procname.equal pn BuiltinDecl.__delete_locked_attribute + type lock_model = + | Lock + | Unlock + | None + + let get_lock_model = function + | Procname.Java java_pname -> + begin + match Procname.java_get_class_name java_pname, Procname.java_get_method java_pname with + | "java.util.concurrent.locks.Lock", "lock" -> + Lock + | "java.util.concurrent.locks.ReentrantLock", + ("lock" | "tryLock" | "lockInterruptibly") -> + Lock + | ("java.util.concurrent.locks.Lock" | "java.util.concurrent.locks.ReentrantLock"), + "unlock" -> + Unlock + | _ -> + None + end + | pname when Procname.equal pname BuiltinDecl.__set_locked_attribute -> + Lock + | pname when Procname.equal pname BuiltinDecl.__delete_locked_attribute -> + Unlock + | _ -> + None let add_path_to_state exp typ pathdomainstate = IList.fold_left @@ -45,11 +68,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct not is_locked && not (Procdesc.is_java_synchronized pdesc) in function | Sil.Call (_, Const (Cfun pn), _, _, _) -> - if is_lock_procedure pn - then true, (readstate,writestate) - else if is_unlock_procedure pn - then false, (readstate,writestate) - else astate + let lockstate' = match get_lock_model pn with + | Lock -> true + | Unlock -> false + | None -> lockstate in + lockstate', snd astate | 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 668af7a93..e222a8902 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java +++ b/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java @@ -16,6 +16,7 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; @Documented @Target(ElementType.TYPE) @@ -46,8 +47,9 @@ public class ThreadSafeExample{ } Lock mLock; + ReentrantLock mReentrantLock; - public void tsBadInOneBranch(boolean b) { + public void lockInOneBranchBad(boolean b) { if (b) { mLock.lock(); } @@ -57,15 +59,25 @@ public class ThreadSafeExample{ } } - // doesn't work because we don't model lock - public void FP_tsWithLockOk() { + public void afterUnlockBad() { + mLock.lock(); + mLock.unlock(); + f = 42; + } + + public void afterReentrantLockUnlockBad() { + mReentrantLock.lock(); + mReentrantLock.unlock(); + f = 42; + } + + public void withLockOk() { mLock.lock(); f = 42; mLock.unlock(); } - // doesn't work because we don't model lock - public void FP_tsWithLockBothBranchesOk(boolean b) { + public void withLockBothBranchesOk(boolean b) { if (b) { mLock.lock(); } else { @@ -75,6 +87,41 @@ public class ThreadSafeExample{ mLock.unlock(); } + public void withReentrantLockOk() { + mReentrantLock.lock(); + f = 42; + mReentrantLock.unlock(); + } + + public void withReentrantLockTryLockOk() { + if (mReentrantLock.tryLock()) { + f = 42; + mReentrantLock.unlock(); + } + } + + public void withReentrantLockInterruptiblyOk() throws InterruptedException { + mReentrantLock.lockInterruptibly(); + f = 42; + mReentrantLock.unlock(); + } + + // our "squish all locks into one" abstraction is not ideal here + public void FP_unlockOneLock() { + mLock.lock(); + mReentrantLock.lock(); + mReentrantLock.unlock(); + f = 42; + mLock.unlock(); + } + + // we don't model the case where `tryLock` fails + public void FN_withReentrantLockTryLockBad() { + if (!mReentrantLock.tryLock()) { + f = 42; + } + } + } class ExtendsThreadSafeExample extends ThreadSafeExample{ diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index 93ea1fa04..e07e96622 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -2,7 +2,8 @@ codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeEx Note: Superclass class codetoanalyze.java.checkers.ThreadSafeExample is marked @ThreadSafe.] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 0, THREAD_SAFETY_ERROR, [Method void ExtendsThreadSafeExample.tsOK() writes to field codetoanalyze.java.checkers.ExtendsThreadSafeExample.field outside of synchronization. Note: Superclass class codetoanalyze.java.checkers.ThreadSafeExample is marked @ThreadSafe.] -codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.FP_tsWithLockBothBranchesOk(boolean), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.FP_tsWithLockBothBranchesOk(boolean) writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ] -codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.FP_tsWithLockOk(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.FP_tsWithLockOk() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ] +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.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. ] -codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.tsBadInOneBranch(boolean), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.tsBadInOneBranch(boolean) writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]