[starvation] extend models of scheduled work

Summary:
In some apps executors are obtained by calling standard framework methods (and not by using DI with annotations).

To treat this style, we need to
- Detect calls that return such executors (`do_executor_effect`) and tag the return result with an `Attribute` indicating that it is now an executor, plus what thread it uses.
- Use that information when calling `execute`, to resolve the executor, if any, and its thread (in `do_work_scheduling` via `AttributeDomain.get_executor_constraint`).
- All this requires a new domain component, mapping variables to attributes.  This extends the component previously used for remembering whether a variable is the result of a check on whether we run on the UI thread.

At the same time, I un-nested some functions from the transfer function for readability.

Reviewed By: skcho

Differential Revision: D18476122

fbshipit-source-id: bc39b5c2f

infer/src/concurrency/StarvationModels.ml

@@ -204,15 +204,15 @@ let is_annotated_lockless ~attrs_of_pname tenv pname =
   |> Option.is_some
 
 
+let executor_type_str = "java.util.concurrent.Executor"
+
 let schedules_work =
   let open MethodMatcher in
-  let matcher =
-    [{default with classname= "java.util.concurrent.Executor"; methods= ["execute"]}] |> of_records
-  in
+  let matcher = [{default with classname= executor_type_str; methods= ["execute"]}] |> of_records in
   fun tenv pname -> matcher tenv pname []
 
 
-type executor_thread_constraint = ForUIThread | ForNonUIThread
+type executor_thread_constraint = ForUIThread | ForNonUIThread [@@deriving equal]
 
 (* Executors are usually stored in fields and annotated according to what type of thread 
    they schedule work on.  Given an expression representing such a field, try to find the kind of 
@@ -250,3 +250,28 @@ let get_run_method_from_runnable tenv runnable =
   |> Option.bind ~f:(Tenv.lookup tenv)
   |> Option.map ~f:(fun (tstruct : Typ.Struct.t) -> tstruct.methods)
   |> Option.bind ~f:(List.find ~f:is_run_method)
+
+
+(* Syntactically match for certain methods known to return executors. *)
+let get_executor_effect ~attrs_of_pname tenv callee actuals =
+  let type_check =
+    lazy
+      ( attrs_of_pname callee
+      |> Option.exists ~f:(fun (attrs : ProcAttributes.t) ->
+             match attrs.ret_type.Typ.desc with
+             | Tstruct tname | Typ.Tptr ({desc= Tstruct tname}, _) ->
+                 PatternMatch.is_subtype_of_str tenv tname executor_type_str
+             | _ ->
+                 false ) )
+  in
+  match (callee, actuals) with
+  | Typ.Procname.Java java_pname, [] -> (
+    match Typ.Procname.Java.get_method java_pname with
+    | "getForegroundExecutor" when Lazy.force type_check ->
+        Some ForUIThread
+    | "getBackgroundExecutor" when Lazy.force type_check ->
+        Some ForNonUIThread
+    | _ ->
+        None )
+  | _ ->
+      None

infer/src/concurrency/StarvationModels.mli

@@ -36,7 +36,7 @@ val schedules_work : Tenv.t -> Typ.Procname.t -> bool
 (** call known to schedule runnable first argument to some thread/executor *)
 
 (** an instance field holding a reference to an executor may be annotated as running on UI/non-UI thread *)
-type executor_thread_constraint = ForUIThread | ForNonUIThread
+type executor_thread_constraint = ForUIThread | ForNonUIThread [@@deriving equal]
 
 val get_executor_thread_constraint :
   Tenv.t -> HilExp.AccessExpression.t -> executor_thread_constraint option
@@ -44,3 +44,11 @@ val get_executor_thread_constraint :
 
 val get_run_method_from_runnable : Tenv.t -> HilExp.AccessExpression.t -> Typ.Procname.t option
 (** given a receiver, find the [run()] method in the appropriate class *)
+
+val get_executor_effect :
+     attrs_of_pname:(Typ.Procname.t -> ProcAttributes.t option)
+  -> Tenv.t
+  -> Typ.Procname.t
+  -> HilExp.t list
+  -> executor_thread_constraint option
+(** does the function return an executor and of which thread? *)

infer/src/concurrency/starvation.ml

@@ -36,29 +36,90 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   type extras = FormalMap.t
 
+  let log_parse_error error pname actuals =
+    L.debug Analysis Verbose "%s pname:%a actuals:%a@." error Typ.Procname.pp pname
+      (PrettyPrintable.pp_collection ~pp_item:HilExp.pp)
+      actuals
+
+
+  (** convert an expression to a canonical form for a lock identifier *)
+  let get_lock_path extras = function
+    | HilExp.AccessExpression access_exp -> (
+      match HilExp.AccessExpression.to_access_path access_exp with
+      | (((Var.ProgramVar pvar, _) as base), _) as path
+        when FormalMap.is_formal base extras || Pvar.is_global pvar ->
+          Some (AccessPath.inner_class_normalize path)
+      | _ ->
+          (* ignore paths on local or logical variables *)
+          None )
+    | HilExp.Constant (Const.Cclass class_id) ->
+        (* this is a synchronized/lock(CLASSNAME.class) construct *)
+        Some (lock_of_class class_id)
+    | _ ->
+        None
+
+
+  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.BGThread in
+      {acc with thread}
+    in
+    match HilExp.get_access_exprs assume_exp with
+    | [access_expr] when AttributeDomain.is_thread_guard access_expr astate.attributes ->
+        HilExp.eval_boolean_exp access_expr assume_exp |> Option.fold ~init:astate ~f:add_choice
+    | _ ->
+        astate
+
+
+  let do_thread_assert_effect (ret_var, _) callee (astate : Domain.t) =
+    let open Domain in
+    match ConcurrencyModels.get_thread_assert_effect callee with
+    | BackgroundThread ->
+        {astate with thread= ThreadDomain.BGThread}
+    | MainThread ->
+        {astate with thread= ThreadDomain.UIThread}
+    | MainThreadIfTrue ->
+        let attributes = AttributeDomain.add ret_var Attribute.Thread astate.attributes in
+        {astate with attributes}
+    | UnknownThread ->
+        astate
+
+
+  let do_work_scheduling tenv callee actuals loc (astate : Domain.t) =
+    let schedule_work runnable init thread =
+      StarvationModels.get_run_method_from_runnable tenv runnable
+      |> Option.fold ~init ~f:(Domain.schedule_work loc thread)
+    in
+    match actuals with
+    | [HilExp.AccessExpression executor; HilExp.AccessExpression runnable]
+      when StarvationModels.schedules_work tenv callee ->
+        let thread_opt =
+          IList.force_until_first_some
+            [ (* match an executor call that we have a model for *)
+              lazy (StarvationModels.get_executor_thread_constraint tenv executor)
+            ; (* match an executor call where the executor is stored in a variable *)
+              lazy (Domain.AttributeDomain.get_executor_constraint executor astate.attributes) ]
+        in
+        Option.fold thread_opt ~init:astate ~f:(schedule_work runnable)
+    | _ ->
+        astate
+
+
+  let do_executor_effect tenv (ret_var, _) callee actuals astate =
+    let open Domain in
+    StarvationModels.get_executor_effect ~attrs_of_pname tenv callee actuals
+    |> Option.fold ~init:astate ~f:(fun acc effect ->
+           let attributes =
+             AttributeDomain.add ret_var (Attribute.Executor effect) astate.attributes
+           in
+           {acc with attributes} )
+
+
   let exec_instr (astate : Domain.t) {ProcData.summary; tenv; extras} _ (instr : HilInstr.t) =
     let open ConcurrencyModels in
     let open StarvationModels in
-    let log_parse_error error pname actuals =
-      L.debug Analysis Verbose "%s pname:%a actuals:%a@." error Typ.Procname.pp pname
-        (PrettyPrintable.pp_collection ~pp_item:HilExp.pp)
-        actuals
-    in
-    let get_lock_path = function
-      | HilExp.AccessExpression access_exp -> (
-        match HilExp.AccessExpression.to_access_path access_exp with
-        | (((Var.ProgramVar pvar, _) as base), _) as path
-          when FormalMap.is_formal base extras || Pvar.is_global pvar ->
-            Some (AccessPath.inner_class_normalize path)
-        | _ ->
-            (* ignore paths on local or logical variables *)
-            None )
-      | HilExp.Constant (Const.Cclass class_id) ->
-          (* this is a synchronized/lock(CLASSNAME.class) construct *)
-          Some (lock_of_class class_id)
-      | _ ->
-          None
-    in
+    let get_lock_path = get_lock_path extras in
     let procname = Summary.get_proc_name summary in
     let is_java = Typ.Procname.is_java procname in
     let do_lock locks loc astate =
@@ -70,52 +131,17 @@ 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.BGThread 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.BGThread}
-      | 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
-    let do_work_scheduling actuals loc astate =
-      match actuals with
-      (* match an executor call where the second arg is the runnable object *)
-      | [HilExp.AccessExpression executor; HilExp.AccessExpression runnable] ->
-          StarvationModels.get_executor_thread_constraint tenv executor
-          |> Option.fold ~init:astate ~f:(fun init thread ->
-                 StarvationModels.get_run_method_from_runnable tenv runnable
-                 |> Option.fold ~init ~f:(Domain.schedule_work loc thread) )
-      | _ ->
-          astate
-    in
     match instr with
-    | Assign _ | Call (_, Indirect _, _, _, _) | Metadata _ ->
+    | Assign _ | Call (_, Indirect _, _, _, _) ->
         astate
-    | Call (_, Direct callee, actuals, _, _) when should_skip_analysis tenv callee actuals ->
+    | Metadata (Sil.ExitScope (vars, _)) ->
+        {astate with attributes= Domain.AttributeDomain.exit_scope vars astate.attributes}
+    | Metadata _ ->
         astate
     | Assume (assume_exp, _, _, _) ->
         do_assume assume_exp astate
+    | Call (_, Direct callee, actuals, _, _) when should_skip_analysis tenv callee actuals ->
+        astate
     | Call (ret_base, Direct callee, actuals, _, loc) -> (
       match get_lock_effect callee actuals with
       | Lock locks ->
@@ -143,10 +169,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           do_lock locks loc astate |> do_unlock locks
       | NoEffect when is_java && is_strict_mode_violation tenv callee actuals ->
           Domain.strict_mode_call ~callee ~loc astate
-      | NoEffect when is_java && StarvationModels.schedules_work tenv callee ->
-          do_work_scheduling actuals loc astate
       | NoEffect when is_java -> (
-          let astate = do_thread_assert_effect ret_base callee astate in
+          let astate =
+            do_thread_assert_effect ret_base callee astate
+            |> do_executor_effect tenv ret_base callee actuals
+            |> do_work_scheduling tenv callee actuals loc
+          in
           match may_block tenv callee actuals with
           | Some sev ->
               Domain.blocking_call ~callee sev ~loc astate

infer/src/concurrency/starvationDomain.ml

@@ -442,29 +442,56 @@ module GuardToLockMap = struct
   let add_guard astate ~guard ~lock = add guard (FlatLock.v lock) astate
 end
 
-module BranchGuard = struct
-  type t = Nothing | Thread
+module Attribute = struct
+  type t = Nothing | Thread | Executor of StarvationModels.executor_thread_constraint
+  [@@deriving equal]
 
   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 pp fmt t =
+    ( match t with
+    | Nothing ->
+        "Nothing"
+    | Thread ->
+        "Thread"
+    | Executor StarvationModels.ForUIThread ->
+        "Executor(UI)"
+    | Executor StarvationModels.ForNonUIThread ->
+        "Executor(BG)" )
+    |> F.pp_print_string fmt
 
-  let leq ~lhs ~rhs =
-    match (lhs, rhs) with _, Nothing -> true | Nothing, _ -> false | Thread, Thread -> true
 
+  let join lhs rhs = if equal lhs rhs then lhs else Nothing
 
-  let join lhs rhs = match (lhs, rhs) with Thread, Thread -> lhs | _ -> Nothing
+  let leq ~lhs ~rhs = equal (join lhs rhs) rhs
 
   let widen ~prev ~next ~num_iters:_ = join prev next
 end
 
-module BranchGuardDomain = struct
-  include AbstractDomain.InvertedMap (HilExp.AccessExpression) (BranchGuard)
+module AttributeDomain = struct
+  include AbstractDomain.InvertedMap (Var) (Attribute)
+
+  let is_thread_guard (acc_exp : HilExp.AccessExpression.t) t =
+    match acc_exp with
+    | Base (v, _) ->
+        find_opt v t |> Option.exists ~f:(function Attribute.Thread -> true | _ -> false)
+    | _ ->
+        false
+
+
+  let get_executor_constraint (acc_exp : HilExp.AccessExpression.t) t =
+    match acc_exp with
+    | Base (v, _) ->
+        find_opt v t |> Option.bind ~f:(function Attribute.Executor c -> Some c | _ -> None)
+    | _ ->
+        None
+
 
-  let is_thread_guard acc_exp t =
-    find_opt acc_exp t |> Option.exists ~f:(function BranchGuard.Thread -> true | _ -> false)
+  let exit_scope vars t =
+    let pred key _value = not (List.exists vars ~f:(Var.equal key)) in
+    filter pred t
 end
 
 module ScheduledWorkItem = struct
@@ -481,7 +508,7 @@ type t =
   { guard_map: GuardToLockMap.t
   ; lock_state: LockState.t
   ; critical_pairs: CriticalPairs.t
-  ; branch_guards: BranchGuardDomain.t
+  ; attributes: AttributeDomain.t
   ; thread: ThreadDomain.t
   ; scheduled_work: ScheduledWorkDomain.t }
 
@@ -489,7 +516,7 @@ let bottom =
   { guard_map= GuardToLockMap.empty
   ; lock_state= LockState.top
   ; critical_pairs= CriticalPairs.empty
-  ; branch_guards= BranchGuardDomain.empty
+  ; attributes= AttributeDomain.empty
   ; thread= ThreadDomain.bottom
   ; scheduled_work= ScheduledWorkDomain.bottom }
 
@@ -498,17 +525,17 @@ let is_bottom astate =
   GuardToLockMap.is_empty astate.guard_map
   && LockState.is_top astate.lock_state
   && CriticalPairs.is_empty astate.critical_pairs
-  && BranchGuardDomain.is_top astate.branch_guards
+  && AttributeDomain.is_top astate.attributes
   && ThreadDomain.is_bottom astate.thread
   && ScheduledWorkDomain.is_bottom astate.scheduled_work
 
 
 let pp fmt astate =
   F.fprintf fmt
-    "{guard_map= %a; lock_state= %a; critical_pairs= %a; branch_guards= %a; thread= %a; \
+    "{guard_map= %a; lock_state= %a; critical_pairs= %a; attributes= %a; thread= %a; \
      scheduled_work= %a}"
     GuardToLockMap.pp astate.guard_map LockState.pp astate.lock_state CriticalPairs.pp
-    astate.critical_pairs BranchGuardDomain.pp astate.branch_guards ThreadDomain.pp astate.thread
+    astate.critical_pairs AttributeDomain.pp astate.attributes ThreadDomain.pp astate.thread
     ScheduledWorkDomain.pp astate.scheduled_work
 
 
@@ -516,7 +543,7 @@ 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
+  ; attributes= AttributeDomain.join lhs.attributes rhs.attributes
   ; thread= ThreadDomain.join lhs.thread rhs.thread
   ; scheduled_work= ScheduledWorkDomain.join lhs.scheduled_work rhs.scheduled_work }
 
@@ -527,7 +554,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
+  && AttributeDomain.leq ~lhs:lhs.attributes ~rhs:rhs.attributes
   && ThreadDomain.leq ~lhs:lhs.thread ~rhs:rhs.thread
   && ScheduledWorkDomain.leq ~lhs:lhs.scheduled_work ~rhs:rhs.scheduled_work
 

infer/src/concurrency/starvationDomain.mli

@@ -95,21 +95,24 @@ 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
+(** Tracks whether a variable has been tested for whether we execute on UI thread, or 
+    has been assigned an executor object. *)
+module Attribute : sig
+  type t = Nothing | Thread | Executor of StarvationModels.executor_thread_constraint
 
   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
+(** Tracks all variables assigned values of [Attribute] *)
+module AttributeDomain : sig
+  include AbstractDomain.InvertedMapS with type key = Var.t and type value = Attribute.t
 
   val is_thread_guard : HilExp.AccessExpression.t -> t -> bool
+
+  val get_executor_constraint :
+    HilExp.AccessExpression.t -> t -> StarvationModels.executor_thread_constraint option
+
+  val exit_scope : Var.t list -> t -> t
 end
 
 (** A record of scheduled parallel work: the method scheduled to run, where, and on what thread. *)
@@ -125,7 +128,7 @@ type t =
   { guard_map: GuardToLockMap.t
   ; lock_state: LockState.t
   ; critical_pairs: CriticalPairs.t
-  ; branch_guards: BranchGuardDomain.t
+  ; attributes: AttributeDomain.t
   ; thread: ThreadDomain.t
   ; scheduled_work: ScheduledWorkDomain.t }
 

infer/tests/codetoanalyze/java/starvation/ExecutorRunnable.java

@@ -96,4 +96,58 @@ class ExecutorRunnable {
           }
         });
   }
+
+  public void postDeadlockIndirectBad() {
+    Executors.getForegroundExecutor()
+        .execute(
+            new Runnable() {
+              @Override
+              public void run() {
+                lockAB();
+              }
+            });
+
+    Executors.getBackgroundExecutor()
+        .execute(
+            new Runnable() {
+              @Override
+              public void run() {
+                lockBA();
+              }
+            });
+  }
+
+  public void postOnUIThreadIndirectOk() {
+    Executors.getForegroundExecutor()
+        .execute(
+            new Runnable() {
+              @Override
+              public void run() {
+                lockAB();
+              }
+            });
+
+    Executors.getForegroundExecutor()
+        .execute(
+            new Runnable() {
+              @Override
+              public void run() {
+                lockBA();
+              }
+            });
+  }
+}
+
+class Executors {
+  static Executor uiExecutor;
+
+  static Executor getForegroundExecutor() {
+    return uiExecutor;
+  }
+
+  static Executor bgExecutor;
+
+  static Executor getBackgroundExecutor() {
+    return bgExecutor;
+  }
 }