[thread-safety] use boolean domain to track locks

Summary:
Before, we were using a set domain of strings to model a boolean domain.
An explicit boolean domain makes it a bit clear what's going on.

There are two things to note here:
(1) This actually changed the semantics from the old set domain. The set domain wouldn't warn if the lock is held on only one side of a branch, which isn't what we want.
(2) We can't actually test this because the modeling for `Lock.lock()` etc doesn't work :(.
The reason is that the models (which do things like adding attributes for `Lock.lock`) are analyzed for Infer, but not for the checkers.
We'll have to add separate models for thread safety.

Reviewed By: peterogithub

Differential Revision: D4242487

fbshipit-source-id: 9fc599d

infer/src/checkers/AbstractDomain.mli

@@ -47,3 +47,7 @@ module Map (Map : PrettyPrintable.PPMap) (ValueDomain : S) : sig
   include PrettyPrintable.PPMap with type 'a t = 'a Map.t and type key = Map.key
   include S with type astate = ValueDomain.astate Map.t
 end
+
+(** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's
+    true in both branches. *)
+module BooleanAnd : S with type astate = bool

infer/src/checkers/ThreadSafety.ml

@@ -40,21 +40,16 @@ 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 is_unprotected lockstate =
-      (not (Procdesc.is_java_synchronized pdesc)) &&
-      (ThreadSafetyDomain.LocksDomain.is_empty lockstate)
-    in
+  let exec_instr ((lockstate, (readstate,writestate)) as astate) { ProcData.pdesc; } _ =
+    let is_unprotected is_locked =
+      not is_locked && not (Procdesc.is_java_synchronized pdesc) in
     function
     | Sil.Call (_, Const (Cfun pn), _, _, _) ->
         if is_lock_procedure pn
-        then
-          ((ThreadSafetyDomain.LocksDomain.add "locked" lockstate), (readstate,writestate))
+        then true, (readstate,writestate)
         else if is_unlock_procedure pn
-        then
-          ((ThreadSafetyDomain.LocksDomain.remove "locked" lockstate) , (readstate,writestate))
-        else
-          astate
+        then false, (readstate,writestate)
+        else astate
 
     | Sil.Store ((Lfield ( _, _, typ) as lhsfield) , _, _, _) ->
         if is_unprotected lockstate then (* abstracts no lock being held*)

infer/src/checkers/ThreadSafetyDomain.ml

@@ -12,7 +12,12 @@ module PPrawpath = PrettyPrintable.MakePPSet(struct
     let pp_element = AccessPath.pp_raw
   end)
 
-module LocksDomain =  AbstractDomain.FiniteSet(Utils.StringPPSet)
+(** A bool that is true if a lock is definitely held. Note that this is unsound because it assumes
+    the existence of one global lock. In the case that a lock is held on the access to a variable,
+    but the lock held is the wrong one, we will erroneously say that the access is thread-safe.
+    However, this coarse abstraction saves us from the complexity of tracking which locks are held
+    and which memory locations correspond to the same lock. *)
+module LocksDomain = AbstractDomain.BooleanAnd
 
 module PathDomain =  AbstractDomain.FiniteSet(PPrawpath)
 

infer/src/checkers/abstractDomain.ml

@@ -142,3 +142,19 @@ module Map (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
   let pp fmt astate =
     M.pp ~pp_value:ValueDomain.pp fmt astate
 end
+
+module BooleanAnd = struct
+  type astate = bool
+
+  let initial = false
+
+  let (<=) ~lhs ~rhs = lhs || not rhs
+
+  let join = (&&)
+
+  let widen ~prev ~next ~num_iters:_ =
+    join prev next
+
+  let pp fmt astate =
+    F.fprintf fmt "%b" astate
+end

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

@@ -15,6 +15,8 @@ import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
 
+import java.util.concurrent.locks.Lock;
+
 @Documented
 @Target(ElementType.TYPE)
 @Retention(RetentionPolicy.CLASS)
@@ -43,6 +45,36 @@ public class ThreadSafeExample{
     f = 24;
   }
 
+  Lock mLock;
+
+  public void tsBadInOneBranch(boolean b) {
+    if (b) {
+      mLock.lock();
+    }
+    f = 24;
+    if (b) {
+      mLock.unlock();
+    }
+  }
+
+  // doesn't work because we don't model lock
+  public void FP_tsWithLockOk() {
+    mLock.lock();
+    f = 42;
+    mLock.unlock();
+  }
+
+  // doesn't work because we don't model lock
+  public void FP_tsWithLockBothBranchesOk(boolean b) {
+    if (b) {
+      mLock.lock();
+    } else {
+      mLock.lock();
+    }
+    f = 42;
+    mLock.unlock();
+  }
+
 }
 
 class ExtendsThreadSafeExample extends ThreadSafeExample{

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

@@ -2,4 +2,7 @@ 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.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. ]