[starvation] add path sensitivity restricted to thread status

Summary:
Steal a page from RacerD (and improve interface of) on using certain calls to assert
execution on a particular thread.  Reduces FPs and FNs too.

Reviewed By: dulmarod

Differential Revision: D18199843

fbshipit-source-id: 5bdff0dfe

infer/src/IR/HilExp.ml

@@ -643,6 +643,34 @@ and eval = function
       None
 
 
+let rec eval_boolean_binop op var e1 e2 =
+  Option.both (eval_boolean_exp var e1) (eval_boolean_exp var e2)
+  |> Option.map ~f:(fun (b1, b2) -> op b1 b2)
+
+
+(** 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_boolean_exp var = function
+  | AccessExpression access_expr when AccessExpression.equal access_expr var ->
+      Some true
+  | Constant c ->
+      Some (not (Const.iszero_int_float c))
+  | UnaryOperator (Unop.LNot, e, _) ->
+      eval_boolean_exp var e |> Option.map ~f:not
+  | BinaryOperator (Binop.LAnd, e1, e2) ->
+      eval_boolean_binop ( && ) var e1 e2
+  | BinaryOperator (Binop.LOr, e1, e2) ->
+      eval_boolean_binop ( || ) var e1 e2
+  | BinaryOperator (Binop.Eq, e1, e2) ->
+      eval_boolean_binop Bool.equal var e1 e2
+  | BinaryOperator (Binop.Ne, e1, e2) ->
+      eval_boolean_binop ( <> ) var e1 e2
+  | _ ->
+      (* non-boolean expression; can't evaluate it *)
+      None
+
+
 let rec ignore_cast e = match e with Cast (_, e) -> ignore_cast e | _ -> e
 
 let access_expr_of_exp ~include_array_indexes ~f_resolve_id exp typ =

infer/src/IR/HilExp.mli

@@ -123,6 +123,11 @@ val is_int_zero : t -> bool
 
 val eval : t -> Const.t option
 
+val eval_boolean_exp : AccessExpression.t -> t -> bool option
+(** [eval_boolean_exp var exp] returns [Some bool_value] if the given boolean expression [exp] 
+    evaluates to [bool_value] when [var] is set to true.  Return None if it has free variables 
+    that stop us from evaluating it, or is not a boolean expression. *)
+
 val ignore_cast : t -> t
 
 val access_expr_of_exp :

infer/src/concurrency/ConcurrencyModels.ml

@@ -34,14 +34,17 @@ let is_thread_utils_method method_name_str = function
       false
 
 
-let get_thread = function
+let get_thread_assert_effect = function
   | Typ.Procname.Java java_pname when is_thread_utils_type java_pname -> (
     match Typ.Procname.Java.get_method java_pname with
-    | "assertMainThread" | "assertOnUiThread" | "checkOnMainThread" ->
+    | "assertMainThread" | "assertOnUiThread" | "checkOnMainThread" | "checkIsOnMainThread" ->
         MainThread
-    | "isMainThread" | "isUiThread" ->
+    | "isMainThread" | "isOnMainThread" | "isUiThread" ->
         MainThreadIfTrue
-    | "assertOnBackgroundThread" | "assertOnNonUiThread" | "checkOnNonUiThread" ->
+    | "assertOnBackgroundThread"
+    | "assertOnNonUiThread"
+    | "checkOnNonUiThread"
+    | "checkOnWorkerThread" ->
         BackgroundThread
     | _ ->
         UnknownThread )

infer/src/concurrency/ConcurrencyModels.mli

@@ -29,8 +29,9 @@ val is_thread_utils_method : string -> Typ.Procname.t -> bool
 val get_lock_effect : Typ.Procname.t -> HilExp.t list -> lock_effect
 (** describe how this procedure behaves with respect to locking *)
 
-val get_thread : Typ.Procname.t -> thread
+val get_thread_assert_effect : Typ.Procname.t -> thread
-(** describe how this procedure behaves with respect to thread access *)
+(** In Java, certain methods can be used to assert execution on a specific kind of thread,
+    or return a boolean equivalent to such a fact. *)
 
 val get_current_class_and_annotated_superclasses :
   (Annot.Item.t -> bool) -> Tenv.t -> Typ.Procname.t -> (Typ.name * Typ.name list) option

infer/src/concurrency/RacerD.ml

@@ -273,7 +273,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       else astate
     in
     let astate =
-      match get_thread callee_pname with
+      match get_thread_assert_effect callee_pname with
       | BackgroundThread ->
           {astate with threads= ThreadsDomain.AnyThread}
       | MainThread ->
@@ -405,38 +405,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     {astate with accesses; ownership; attribute_map}
 
 
-  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
-    | HilExp.AccessExpression access_expr ->
-        if AccessExpression.equal access_expr var then Some true else None
-    | HilExp.Constant c ->
-        Some (not (Const.iszero_int_float c))
-    | HilExp.UnaryOperator (Unop.LNot, e, _) ->
-        let b_opt = eval_bexp var e in
-        Option.map ~f:not b_opt
-    | HilExp.BinaryOperator (Binop.LAnd, e1, e2) ->
-        eval_binop ( && ) var e1 e2
-    | HilExp.BinaryOperator (Binop.LOr, e1, e2) ->
-        eval_binop ( || ) var e1 e2
-    | HilExp.BinaryOperator (Binop.Eq, e1, e2) ->
-        eval_binop Bool.equal var e1 e2
-    | HilExp.BinaryOperator (Binop.Ne, e1, e2) ->
-        eval_binop ( <> ) var e1 e2
-    | _ ->
-        (* non-boolean expression; can't evaluate it *)
-        None
-
-
   let do_assume assume_exp loc proc_data (astate : Domain.t) =
     let open Domain in
     let add_choice bool_value (acc : Domain.t) = function
@@ -459,7 +427,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     let astate' =
       match HilExp.get_access_exprs assume_exp with
       | [access_expr] ->
-          eval_bexp access_expr assume_exp
+          HilExp.eval_boolean_exp access_expr assume_exp
           |> Option.fold ~init:astate ~f:(fun init bool_value ->
                  let choices = AttributeMapDomain.get_choices access_expr astate.attribute_map in
                  (* prune (prune_exp) can only evaluate to true if the choice is [bool_value].

infer/src/concurrency/StarvationModels.ml

@@ -192,10 +192,6 @@ let is_strict_mode_violation tenv pn actuals =
   Config.starvation_strict_mode && strict_mode_matcher tenv pn actuals
 
 
-let is_ui_thread_model pn =
-  ConcurrencyModels.(match get_thread pn with MainThread -> true | _ -> false)
-
-
 let is_annotated_nonblocking ~attrs_of_pname tenv pname =
   ConcurrencyModels.find_override_or_superclass_annotated ~attrs_of_pname
     Annotations.ia_is_nonblocking tenv pname

infer/src/concurrency/StarvationModels.mli

@@ -24,9 +24,6 @@ val is_synchronized_library_call : Tenv.t -> Typ.Procname.t -> bool
 val should_skip_analysis : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool
 (** should we treat a method call as skip (eg library methods in guava) to avoid FPs? *)
 
-val is_ui_thread_model : Typ.Procname.t -> bool
-(** is procedure an assertion we are on the UI thread or equivalent *)
-
 val is_annotated_nonblocking :
   attrs_of_pname:(Typ.Procname.t -> ProcAttributes.t option) -> Tenv.t -> Typ.Procname.t -> bool
 (** is procedure transitively annotated [@Nonblocking] *)

infer/src/concurrency/starvation.ml

@@ -70,12 +70,42 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       Payload.read ~caller_summary:summary ~callee_pname:callee
       |> Option.fold ~init:astate ~f:(Domain.integrate_summary tenv callsite)
     in
+    let do_assume assume_exp (astate : Domain.t) =
+      let open Domain in
+      let add_choice (acc : Domain.t) bool_value =
+        let thread = if bool_value then ThreadDomain.UIThread else ThreadDomain.AnyThread in
+        {acc with thread}
+      in
+      match HilExp.get_access_exprs assume_exp with
+      | [access_expr] when BranchGuardDomain.is_thread_guard access_expr astate.branch_guards ->
+          HilExp.eval_boolean_exp access_expr assume_exp |> Option.fold ~init:astate ~f:add_choice
+      | _ ->
+          astate
+    in
+    let do_thread_assert_effect ret_base callee (astate : Domain.t) =
+      let open Domain in
+      match ConcurrencyModels.get_thread_assert_effect callee with
+      | BackgroundThread ->
+          {astate with thread= ThreadDomain.AnyThread}
+      | MainThread ->
+          {astate with thread= ThreadDomain.UIThread}
+      | MainThreadIfTrue ->
+          let ret_access_exp = HilExp.AccessExpression.base ret_base in
+          let branch_guards =
+            BranchGuardDomain.add ret_access_exp BranchGuard.Thread astate.branch_guards
+          in
+          {astate with branch_guards}
+      | UnknownThread ->
+          astate
+    in
     match instr with
-    | Assign _ | Assume _ | Call (_, Indirect _, _, _, _) | Metadata _ ->
+    | Assign _ | Call (_, Indirect _, _, _, _) | Metadata _ ->
         astate
     | Call (_, Direct callee, actuals, _, _) when should_skip_analysis tenv callee actuals ->
         astate
-    | Call (_, Direct callee, actuals, _, loc) -> (
+    | Assume (assume_exp, _, _, _) ->
+        do_assume assume_exp astate
+    | Call (ret_base, Direct callee, actuals, _, loc) -> (
       match get_lock_effect callee actuals with
       | Lock locks ->
           do_lock locks loc astate
@@ -100,11 +130,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           (* model a synchronized call without visible internal behaviour *)
           let locks = List.hd actuals |> Option.to_list in
           do_lock locks loc astate |> do_unlock locks
-      | NoEffect when is_java && is_ui_thread_model callee ->
-          Domain.set_on_ui_thread astate
       | NoEffect when is_java && is_strict_mode_violation tenv callee actuals ->
           Domain.strict_mode_call ~callee ~loc astate
       | NoEffect when is_java -> (
+          let astate = do_thread_assert_effect ret_base callee astate in
           match may_block tenv callee actuals with
           | Some sev ->
               Domain.blocking_call ~callee sev ~loc astate

infer/src/concurrency/starvationDomain.ml

@@ -411,34 +411,65 @@ module GuardToLockMap = struct
   let add_guard astate ~guard ~lock = add guard (FlatLock.v lock) astate
 end
 
+module BranchGuard = struct
+  type t = Nothing | Thread
+
+  let top = Nothing
+
+  let is_top = function Nothing -> true | _ -> false
+
+  let pp fmt t = F.fprintf fmt (match t with Nothing -> "Nothing" | Thread -> "Thread")
+
+  let leq ~lhs ~rhs =
+    match (lhs, rhs) with _, Nothing -> true | Nothing, _ -> false | Thread, Thread -> true
+
+
+  let join lhs rhs = match (lhs, rhs) with Thread, Thread -> lhs | _ -> Nothing
+
+  let widen ~prev ~next ~num_iters:_ = join prev next
+end
+
+module BranchGuardDomain = struct
+  include AbstractDomain.InvertedMap (HilExp.AccessExpression) (BranchGuard)
+
+  let is_thread_guard acc_exp t =
+    find_opt acc_exp t |> Option.exists ~f:(function BranchGuard.Thread -> true | _ -> false)
+end
+
 type t =
   { guard_map: GuardToLockMap.t
   ; lock_state: LockState.t
   ; critical_pairs: CriticalPairs.t
+  ; branch_guards: BranchGuardDomain.t
   ; thread: ThreadDomain.t }
 
 let bottom =
   { guard_map= GuardToLockMap.empty
   ; lock_state= LockState.top
   ; critical_pairs= CriticalPairs.empty
+  ; branch_guards= BranchGuardDomain.empty
   ; thread= ThreadDomain.top }
 
 
-let is_bottom {guard_map; lock_state; critical_pairs; thread} =
+let is_bottom {guard_map; lock_state; critical_pairs; branch_guards; thread} =
   GuardToLockMap.is_empty guard_map && LockState.is_top lock_state
   && CriticalPairs.is_empty critical_pairs
+  && BranchGuardDomain.is_top branch_guards
   && ThreadDomain.is_top thread
 
 
-let pp fmt {guard_map; lock_state; critical_pairs; thread} =
+let pp fmt {guard_map; lock_state; critical_pairs; branch_guards; thread} =
-  F.fprintf fmt "{guard_map= %a; lock_state= %a; critical_pairs= %a; thread= %a}" GuardToLockMap.pp
+  F.fprintf fmt
-    guard_map LockState.pp lock_state CriticalPairs.pp critical_pairs ThreadDomain.pp thread
+    "{guard_map= %a; lock_state= %a; critical_pairs= %a; branch_guards= %a; thread= %a}"
+    GuardToLockMap.pp guard_map LockState.pp lock_state CriticalPairs.pp critical_pairs
+    BranchGuardDomain.pp branch_guards ThreadDomain.pp thread
 
 
 let join lhs rhs =
   { guard_map= GuardToLockMap.join lhs.guard_map rhs.guard_map
   ; lock_state= LockState.join lhs.lock_state rhs.lock_state
   ; critical_pairs= CriticalPairs.join lhs.critical_pairs rhs.critical_pairs
+  ; branch_guards= BranchGuardDomain.join lhs.branch_guards rhs.branch_guards
   ; thread= ThreadDomain.join lhs.thread rhs.thread }
 
 
@@ -448,6 +479,7 @@ let leq ~lhs ~rhs =
   GuardToLockMap.leq ~lhs:lhs.guard_map ~rhs:rhs.guard_map
   && LockState.leq ~lhs:lhs.lock_state ~rhs:rhs.lock_state
   && CriticalPairs.leq ~lhs:lhs.critical_pairs ~rhs:rhs.critical_pairs
+  && BranchGuardDomain.leq ~lhs:lhs.branch_guards ~rhs:rhs.branch_guards
   && ThreadDomain.leq ~lhs:lhs.thread ~rhs:rhs.thread
 
 

infer/src/concurrency/starvationDomain.mli

@@ -96,10 +96,28 @@ module CriticalPairs : AbstractDomain.FiniteSetS with type elt = CriticalPair.t
 
 module GuardToLockMap : AbstractDomain.WithTop
 
+(** tracks whether an expression has been tested for whether we execute on UI thread *)
+module BranchGuard : sig
+  type t = Nothing | Thread
+
+  include AbstractDomain.WithTop with type t := t
+end
+
+(** tracks all expressions currently known to have been tested for conditions in [BranchGuard] *)
+module BranchGuardDomain : sig
+  include
+    AbstractDomain.InvertedMapS
+    with type key = HilExp.AccessExpression.t
+     and type value = BranchGuard.t
+
+  val is_thread_guard : HilExp.AccessExpression.t -> t -> bool
+end
+
 type t =
   { guard_map: GuardToLockMap.t
   ; lock_state: LockState.t
   ; critical_pairs: CriticalPairs.t
+  ; branch_guards: BranchGuardDomain.t
   ; thread: ThreadDomain.t }
 
 include AbstractDomain.WithBottom with type t := t

infer/tests/codetoanalyze/java/starvation/ThreadSensitivity.java

@@ -30,7 +30,7 @@ class ThreadSensitivity {
 
   // the branches in the following two methods are both on main/UI thread so cannot deadlock
 
-  void FP_conditionalIsMainThread_Ok() {
+  void conditionalIsMainThread_Ok() {
     if (OurThreadUtils.isMainThread()) {
       synchronized (monitorC) {
         synchronized (monitorD) {
@@ -39,7 +39,7 @@ class ThreadSensitivity {
     }
   }
 
-  void FP_conditionalIsUiThread_Ok() {
+  void conditionalIsUiThread_Ok() {
     if (OurThreadUtils.isUiThread()) {
       synchronized (monitorD) {
         synchronized (monitorC) {

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

@@ -73,8 +73,6 @@ codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.assertOnBackgr
 codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.assertOnUIThreadBad():void, 52, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.assertOnUIThreadBad()`, locks `this` in `class ThreadDeadlock`, locks `this.lockC` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.assertOnBackgroundThreadBad()`, locks `this.lockC` in `class ThreadDeadlock`, locks `this` in `class ThreadDeadlock`]
 codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.notAnnotatedBBad():void, 77, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.notAnnotatedBBad()`, locks `this.lockD` in `class ThreadDeadlock`, locks `this` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.notAnnotatedBadA()`, locks `this` in `class ThreadDeadlock`, locks `this.lockD` in `class ThreadDeadlock`]
 codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.notAnnotatedBadA():void, 71, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.notAnnotatedBadA()`, locks `this` in `class ThreadDeadlock`, locks `this.lockD` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.notAnnotatedBBad()`, locks `this.lockD` in `class ThreadDeadlock`, locks `this` in `class ThreadDeadlock`]
-codetoanalyze/java/starvation/ThreadSensitivity.java, ThreadSensitivity.FP_conditionalIsMainThread_Ok():void, 35, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadSensitivity.FP_conditionalIsMainThread_Ok()`, locks `this.monitorC` in `class ThreadSensitivity`, locks `this.monitorD` in `class ThreadSensitivity`,[Trace 2] `void ThreadSensitivity.FP_conditionalIsUiThread_Ok()`, locks `this.monitorD` in `class ThreadSensitivity`, locks `this.monitorC` in `class ThreadSensitivity`]
-codetoanalyze/java/starvation/ThreadSensitivity.java, ThreadSensitivity.FP_conditionalIsUiThread_Ok():void, 44, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadSensitivity.FP_conditionalIsUiThread_Ok()`, locks `this.monitorD` in `class ThreadSensitivity`, locks `this.monitorC` in `class ThreadSensitivity`,[Trace 2] `void ThreadSensitivity.FP_conditionalIsMainThread_Ok()`, locks `this.monitorC` in `class ThreadSensitivity`, locks `this.monitorD` in `class ThreadSensitivity`]
 codetoanalyze/java/starvation/ThreadSensitivity.java, ThreadSensitivity.FP_confusedAssertOk(boolean):void, 99, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadSensitivity.FP_confusedAssertOk(boolean)`, locks `this.monitorI` in `class ThreadSensitivity`, locks `this.monitorJ` in `class ThreadSensitivity`,[Trace 2] `void ThreadSensitivity.FP_confusedAssertOk(boolean)`, locks `this.monitorJ` in `class ThreadSensitivity`, locks `this.monitorI` in `class ThreadSensitivity`]
 codetoanalyze/java/starvation/ThreadSensitivity.java, ThreadSensitivity.FP_confusedAssertOk(boolean):void, 106, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadSensitivity.FP_confusedAssertOk(boolean)`, locks `this.monitorJ` in `class ThreadSensitivity`, locks `this.monitorI` in `class ThreadSensitivity`,[Trace 2] `void ThreadSensitivity.FP_confusedAssertOk(boolean)`, locks `this.monitorI` in `class ThreadSensitivity`, locks `this.monitorJ` in `class ThreadSensitivity`]
 codetoanalyze/java/starvation/ThreadSensitivity.java, ThreadSensitivity.conditionalAssertMainThread_Bad(boolean):void, 16, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadSensitivity.conditionalAssertMainThread_Bad(boolean)`, locks `this.monitorA` in `class ThreadSensitivity`, locks `this.monitorB` in `class ThreadSensitivity`,[Trace 2] `void ThreadSensitivity.conditionalAssertMainThread_Bad(boolean)`, locks `this.monitorB` in `class ThreadSensitivity`, locks `this.monitorA` in `class ThreadSensitivity`]