[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

@@ -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
+  type lock_model =
+    | Lock
+    | Unlock
+    | None
 
-  let is_unlock_procedure pn = Procname.equal pn BuiltinDecl.__delete_locked_attribute
+  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*)

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{

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. ]