[thread-safety] add choice variables to support partial path-sensitivity

Reviewed By: peterogithub

Differential Revision: D4712228

fbshipit-source-id: 50a9188

infer/src/checkers/ThreadSafety.ml

@@ -49,6 +49,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   type lock_model =
     | Lock
     | Unlock
+    | LockedIfTrue
     | NoEffect
 
 
@@ -68,7 +69,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               | "java.util.concurrent.locks.ReentrantLock"
               | "java.util.concurrent.locks.ReentrantReadWriteLock$ReadLock"
               | "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock"),
-              ("lock" | "tryLock" | "lockInterruptibly") ->
+              ("lock" | "lockInterruptibly") ->
                 Lock
             | ("java.util.concurrent.locks.Lock"
               |"java.util.concurrent.locks.ReentrantLock"
@@ -76,6 +77,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               | "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock"),
               "unlock" ->
                 Unlock
+            | ("java.util.concurrent.locks.Lock"
+              | "java.util.concurrent.locks.ReentrantLock"
+              | "java.util.concurrent.locks.ReentrantReadWriteLock$ReadLock"
+              | "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock"),
+              "tryLock" ->
+                LockedIfTrue
             | _ ->
                 NoEffect
           end
@@ -431,6 +438,21 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                 { astate with locks = true; }
             | Unlock ->
                 { astate with locks = false; }
+            | LockedIfTrue ->
+                begin
+                  match ret_opt with
+                  | Some (ret_id, ret_typ) ->
+                      let attribute_map =
+                        AttributeMapDomain.add_attribute
+                          (AccessPath.of_id ret_id ret_typ)
+                          (Choice Choice.LockHeld)
+                          astate.attribute_map in
+                      { astate with attribute_map; }
+                  | None ->
+                      failwithf
+                        "Procedure %a specified as returning boolean, but returns nothing"
+                        Typ.Procname.pp callee_pname
+                end
             | NoEffect ->
                 match
                   get_summary pdesc callee_pname actuals ~f_resolve_id loc tenv with
@@ -629,6 +651,61 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             lhs_access_path rhs_exp rhs_typ ~f_resolve_id astate.attribute_map extras in
         { astate with accesses; id_map; attribute_map; }
 
+    | Sil.Prune (prune_exp, _, _, _) ->
+        let rec eval_binop op var e1 e2 =
+          match eval_bexp var e1, eval_bexp var e2 with
+          | Some b1, Some b2 -> Some (op b1 b2)
+          | _ -> None
+        (* return Some bool_value if the given boolean expression evaluates to bool_value when [var]
+           is set to true. return None if it has free variables that stop us from evaluating it *)
+        and eval_bexp var = function
+          | Exp.Var id ->
+              begin
+                match f_resolve_id (Var.of_id id) with
+                | Some ap when AccessPath.Raw.equal ap var -> Some true
+                | _ -> None
+              end
+          | (Exp.Const _) as e ->
+              Some (not (Exp.is_zero e))
+          | Exp.UnOp (Unop.LNot, e, _) ->
+              let b_opt = eval_bexp var e in
+              Option.map ~f:not b_opt
+          | Exp.BinOp (Binop.LAnd, e1, e2) ->
+              eval_binop (&&) var e1 e2
+          | Exp.BinOp (Binop.LOr, e1, e2) ->
+              eval_binop (||) var e1 e2
+          | Exp.BinOp (Binop.Eq, e1, e2) ->
+              eval_binop Bool.equal var e1 e2
+          | Exp.BinOp (Binop.Ne, e1, e2) ->
+              eval_binop (<>) var e1 e2
+          | _ ->
+              (* non-boolean expression; can't evaluate it *)
+              None in
+        let add_choice bool_value acc = function
+          | Choice.LockHeld ->
+              let locks = bool_value in
+              { acc with locks; }
+          | Choice.OnMainThread ->
+              let threads = bool_value in
+              { acc with threads; } in
+
+        begin
+          match AccessPath.of_lhs_exp prune_exp (Typ.Tint IBool) ~f_resolve_id with
+          | Some access_path ->
+              let choices = AttributeMapDomain.get_choices access_path astate.attribute_map in
+              begin
+                match eval_bexp access_path prune_exp with
+                | Some bool_value ->
+                    (* prune (prune_exp) can only evaluate to true if the choice is [bool_value].
+                       add the constraint that the the choice must be [bool_value] to the state *)
+                    List.fold ~f:(add_choice bool_value) ~init:astate choices
+                | None ->
+                    astate
+              end
+          | _ ->
+              astate
+        end
+
     | Sil.Remove_temps (ids, _) ->
         let id_map =
           List.fold
@@ -637,7 +714,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             ids in
         { astate with id_map; }
 
-    |  _  ->
+    | _ ->
         astate
 end
 

infer/src/checkers/ThreadSafetyDomain.ml

@@ -74,16 +74,29 @@ module ThreadsDomain = AbstractDomain.BooleanAnd
 
 module PathDomain = SinkTrace.Make(TraceElem)
 
+module Choice = struct
+  type t =
+    | OnMainThread
+    | LockHeld
+  [@@deriving compare]
+
+  let pp fmt = function
+    | OnMainThread -> F.fprintf fmt "OnMainThread"
+    | LockHeld -> F.fprintf fmt "LockHeld"
+end
+
 module Attribute = struct
   type t =
     | OwnedIf of int option
     | Functional
+    | Choice of Choice.t
   [@@deriving compare]
 
   let pp fmt = function
     | OwnedIf None -> F.fprintf fmt "Owned"
     | OwnedIf (Some formal_index) -> F.fprintf fmt "Owned if formal %d is owned" formal_index
     | Functional -> F.fprintf fmt "Functional"
+    | Choice choice -> Choice.pp fmt choice
 
   let unconditionally_owned = OwnedIf None
 
@@ -117,6 +130,17 @@ module AttributeMapDomain = struct
     with Not_found ->
       None
 
+  let get_choices access_path t =
+    try
+      let attributes = find access_path t in
+      (List.filter_map
+         ~f:(function
+             | Attribute.Choice c -> Some c
+             | _ -> None)
+         (AttributeSetDomain.elements attributes))
+    with Not_found ->
+      []
+
   let add_attribute access_path attribute t =
     let attribute_set =
       (try find access_path t

infer/src/checkers/ThreadSafetyDomain.mli

@@ -43,12 +43,24 @@ module ThreadsDomain : AbstractDomain.S with type astate = bool
 
 module PathDomain : module type of SinkTrace.Make(TraceElem)
 
+(** attribute attached to a boolean variable specifying what it means when the boolean is true *)
+module Choice : sig
+  type t =
+    | OnMainThread (** the current procedure is running on the main thread *)
+    | LockHeld (** a lock is currently held *)
+  [@@deriving compare]
+
+  val pp : F.formatter -> t -> unit
+end
+
 module Attribute : sig
   type t =
     | OwnedIf of int option
     (** owned unconditionally if OwnedIf None, owned when formal at index i is owned otherwise *)
     | Functional
     (** holds a value returned from a callee marked @Functional *)
+    | Choice of Choice.t
+    (** holds a boolean choice variable *)
   [@@deriving compare]
 
   (** alias for OwnedIf None *)
@@ -69,6 +81,9 @@ module AttributeMapDomain : sig
   (** get the formal index of the the formal that must own the given access path (if any) *)
   val get_conditional_ownership_index : AccessPath.Raw.t -> astate -> int option
 
+  (** get the choice attributes associated with the given access path *)
+  val get_choices : AccessPath.Raw.t -> astate -> Choice.t list
+
   val add_attribute : AccessPath.Raw.t -> Attribute.t -> astate -> astate
 end
 

infer/tests/codetoanalyze/java/threadsafety/Locks.java

@@ -83,13 +83,55 @@ public class Locks {
     }
   }
 
-  public void rReentrantLockTryLockOk() {
+  public void reentrantLockTryLockOk() {
     if (mReentrantLock.tryLock()) {
       f = 42;
       mReentrantLock.unlock();
     }
   }
 
+  public void tryLockNoCheckBad() {
+    mReentrantLock.tryLock(); // might return false
+    f = 42;
+  }
+
+  public void tryLockWrongBranchBad() {
+    if (mReentrantLock.tryLock()) {
+    } else {
+      f = 42;
+    }
+  }
+
+  public void tryLockPropagateOk() {
+    boolean result = mReentrantLock.tryLock();
+    boolean copy = result;
+    if (copy) {
+      f = 42;
+    }
+  }
+
+  public void negatedReentrantLockTryLockBad() {
+    if (!mReentrantLock.tryLock()) {
+      f = 42;
+    }
+  }
+
+  public void negatedReentrantLockTryLockOk() {
+    if (!mReentrantLock.tryLock()) {
+
+    } else {
+      f = 42;
+    }
+  }
+
+  // we could catch this by invalidating the choice predicates whenever we update the lock domain
+  public void FN_tryLockStaleBad() {
+    boolean result = mReentrantLock.tryLock();
+    mReentrantLock.unlock();
+    if (result) {
+      f = 42; // oops, actually not safe
+    }
+  }
 
   public void reentrantLockInterruptiblyOk() throws InterruptedException {
     mReentrantLock.lockInterruptibly();
@@ -139,13 +181,6 @@ public class Locks {
     f = 42;
   }
 
-  // we don't model the case where `tryLock` fails
-  public void FN_withReentrantLockTryLockBad() {
-    if (!mReentrantLock.tryLock()) {
-      f = 42;
-    }
-  }
-
   // we shouldn't be able to write when holding a readLock
   public void FN_readLockOk() {
     mReentrantReadWriteLock.readLock().lock();

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

@@ -41,6 +41,9 @@ codetoanalyze/java/threadsafety/Locks.java, void Locks.afterReentrantLockUnlockB
 codetoanalyze/java/threadsafety/Locks.java, void Locks.afterUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f]
 codetoanalyze/java/threadsafety/Locks.java, void Locks.afterWriteLockUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f]
 codetoanalyze/java/threadsafety/Locks.java, void Locks.lockInOneBranchBad(boolean), 4, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f]
+codetoanalyze/java/threadsafety/Locks.java, void Locks.negatedReentrantLockTryLockBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f]
+codetoanalyze/java/threadsafety/Locks.java, void Locks.tryLockNoCheckBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f]
+codetoanalyze/java/threadsafety/Locks.java, void Locks.tryLockWrongBranchBad(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f]
 codetoanalyze/java/threadsafety/Ownership.java, Ownership.<init>(Obj,Object), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_ownAndConditionalOwnOk(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_twoDifferentConditionalOwnsOk(), 4, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f]