[starvation] record scheduling parallel works via executors

Summary: Capture locations where work is scheduled to run in parallel (here, just Executors). Also add a test file with cases the upcoming whole-program analysis for starvation should catch.

Reviewed By: dulmarod

Differential Revision: D18346880

fbshipit-source-id: 57411b052

infer/src/concurrency/StarvationModels.ml

@@ -202,3 +202,51 @@ let is_annotated_lockless ~attrs_of_pname tenv pname =
   let check annot = Annotations.(ia_ends_with annot lockless) in
   ConcurrencyModels.find_override_or_superclass_annotated ~attrs_of_pname check tenv pname
   |> Option.is_some
+
+
+let schedules_work =
+  let open MethodMatcher in
+  let matcher =
+    [{default with classname= "java.util.concurrent.Executor"; methods= ["execute"]}] |> of_records
+  in
+  fun tenv pname -> matcher tenv pname []
+
+
+type executor_thread_constraint = ForUIThread | ForNonUIThread
+
+(* 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 
+   annotation constraint, if any. *)
+let rec get_executor_thread_constraint tenv (receiver : HilExp.AccessExpression.t) =
+  match receiver with
+  | FieldOffset (_, field_name) ->
+      Typ.Fieldname.Java.get_class field_name
+      |> Typ.Name.Java.from_string |> Tenv.lookup tenv
+      |> Option.map ~f:(fun (tstruct : Typ.Struct.t) -> tstruct.fields @ tstruct.statics)
+      |> Option.bind ~f:(List.find ~f:(fun (fld, _, _) -> Typ.Fieldname.equal fld field_name))
+      |> Option.bind ~f:(fun (_, _, annot) ->
+             if Annotations.(ia_ends_with annot for_ui_thread) then Some ForUIThread
+             else if Annotations.(ia_ends_with annot for_non_ui_thread) then Some ForNonUIThread
+             else None )
+  | Dereference prefix ->
+      get_executor_thread_constraint tenv prefix
+  | _ ->
+      None
+
+
+(* Given an object, find the [run] method in its class and return the procname, if any *)
+let get_run_method_from_runnable tenv runnable =
+  let is_run_method = function
+    | Typ.Procname.Java pname when Typ.Procname.Java.(not (is_static pname)) ->
+        (* confusingly, the parameter list in (non-static?) Java procnames does not contain [this] *)
+        Typ.Procname.Java.(
+          String.equal "run" (get_method pname) && List.is_empty (get_parameters pname))
+    | _ ->
+        false
+  in
+  HilExp.AccessExpression.get_typ runnable tenv
+  |> Option.map ~f:(function Typ.{desc= Tptr (typ, _)} -> typ | typ -> typ)
+  |> Option.bind ~f:Typ.name
+  |> 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)

infer/src/concurrency/StarvationModels.mli

@@ -31,3 +31,16 @@ val is_annotated_nonblocking :
 val is_annotated_lockless :
   attrs_of_pname:(Typ.Procname.t -> ProcAttributes.t option) -> Tenv.t -> Typ.Procname.t -> bool
 (** is procedure transitively annotated [@Lockless] *)
+
+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
+
+val get_executor_thread_constraint :
+  Tenv.t -> HilExp.AccessExpression.t -> executor_thread_constraint option
+(** given an executor receiver, get its thread constraint, if any *)
+
+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 *)

infer/src/concurrency/starvation.ml

@@ -98,6 +98,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | 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 _ ->
         astate
@@ -132,6 +143,8 @@ 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
           match may_block tenv callee actuals with

infer/src/concurrency/starvationDomain.ml

@@ -472,33 +472,49 @@ module BranchGuardDomain = struct
     find_opt acc_exp t |> Option.exists ~f:(function BranchGuard.Thread -> true | _ -> false)
 end
 
+module ScheduledWorkItem = struct
+  type t = {procname: Typ.Procname.t; loc: Location.t; thread: ThreadDomain.t} [@@deriving compare]
+
+  let pp fmt {procname; loc; thread} =
+    F.fprintf fmt "{procname= %a; loc= %a; thread= %a}" Typ.Procname.pp procname Location.pp loc
+      ThreadDomain.pp thread
+end
+
+module ScheduledWorkDomain = AbstractDomain.FiniteSet (ScheduledWorkItem)
+
 type t =
   { guard_map: GuardToLockMap.t
   ; lock_state: LockState.t
   ; critical_pairs: CriticalPairs.t
   ; branch_guards: BranchGuardDomain.t
-  ; thread: ThreadDomain.t }
+  ; thread: ThreadDomain.t
+  ; scheduled_work: ScheduledWorkDomain.t }
 
 let bottom =
   { guard_map= GuardToLockMap.empty
   ; lock_state= LockState.top
   ; critical_pairs= CriticalPairs.empty
   ; branch_guards= BranchGuardDomain.empty
-  ; thread= ThreadDomain.bottom }
+  ; thread= ThreadDomain.bottom
+  ; scheduled_work= ScheduledWorkDomain.bottom }
 
 
-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_bottom thread
+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
+  && ThreadDomain.is_bottom astate.thread
+  && ScheduledWorkDomain.is_bottom astate.scheduled_work
 
 
-let pp fmt {guard_map; lock_state; critical_pairs; branch_guards; thread} =
+let pp fmt astate =
   F.fprintf fmt
-    "{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
+    "{guard_map= %a; lock_state= %a; critical_pairs= %a; branch_guards= %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
+    ScheduledWorkDomain.pp astate.scheduled_work
 
 
 let join lhs rhs =
@@ -506,7 +522,8 @@ let join lhs rhs =
   ; 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 }
+  ; thread= ThreadDomain.join lhs.thread rhs.thread
+  ; scheduled_work= ScheduledWorkDomain.join lhs.scheduled_work rhs.scheduled_work }
 
 
 let widen ~prev ~next ~num_iters:_ = join prev next
@@ -517,6 +534,7 @@ let leq ~lhs ~rhs =
   && 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
+  && ScheduledWorkDomain.leq ~lhs:lhs.scheduled_work ~rhs:rhs.scheduled_work
 
 
 let add_critical_pair tenv_opt lock_state event thread ~loc acc =
@@ -589,11 +607,25 @@ let filter_blocking_calls ({critical_pairs} as astate) =
   {astate with critical_pairs= CriticalPairs.filter CriticalPair.is_blocking_call critical_pairs}
 
 
-type summary = {critical_pairs: CriticalPairs.t; thread: ThreadDomain.t}
+let schedule_work loc thread_constraint astate procname =
+  let thread =
+    match thread_constraint with
+    | StarvationModels.ForUIThread ->
+        ThreadDomain.UIThread
+    | StarvationModels.ForNonUIThread ->
+        ThreadDomain.BGThread
+  in
+  let work_item = ScheduledWorkItem.{procname; loc; thread} in
+  {astate with scheduled_work= ScheduledWorkDomain.add work_item astate.scheduled_work}
+
+
+type summary =
+  {critical_pairs: CriticalPairs.t; thread: ThreadDomain.t; scheduled_work: ScheduledWorkDomain.t}
 
 let pp_summary fmt (summary : summary) =
-  F.fprintf fmt "{thread= %a; critical_pairs= %a}" ThreadDomain.pp summary.thread CriticalPairs.pp
-    summary.critical_pairs
+  F.fprintf fmt "{thread= %a; critical_pairs= %a; scheduled_work= %a}" ThreadDomain.pp
+    summary.thread CriticalPairs.pp summary.critical_pairs ScheduledWorkDomain.pp
+    summary.scheduled_work
 
 
 let integrate_summary tenv callsite (astate : t) (summary : summary) =
@@ -607,4 +639,7 @@ let integrate_summary tenv callsite (astate : t) (summary : summary) =
 
 
 let summary_of_astate : t -> summary =
- fun astate -> {critical_pairs= astate.critical_pairs; thread= astate.thread}
+ fun astate ->
+  { critical_pairs= astate.critical_pairs
+  ; thread= astate.thread
+  ; scheduled_work= astate.scheduled_work }

infer/src/concurrency/starvationDomain.mli

@@ -112,12 +112,22 @@ module BranchGuardDomain : sig
   val is_thread_guard : HilExp.AccessExpression.t -> t -> bool
 end
 
+(** A record of scheduled parallel work: the method scheduled to run, where, and on what thread. *)
+module ScheduledWorkItem : sig
+  type t = {procname: Typ.Procname.t; loc: Location.t; thread: ThreadDomain.t}
+
+  include PrettyPrintable.PrintableOrderedType with type t := t
+end
+
+module ScheduledWorkDomain : AbstractDomain.FiniteSetS with type elt = ScheduledWorkItem.t
+
 type t =
   { guard_map: GuardToLockMap.t
   ; lock_state: LockState.t
   ; critical_pairs: CriticalPairs.t
   ; branch_guards: BranchGuardDomain.t
-  ; thread: ThreadDomain.t }
+  ; thread: ThreadDomain.t
+  ; scheduled_work: ScheduledWorkDomain.t }
 
 include AbstractDomain.WithBottom with type t := t
 
@@ -151,7 +161,12 @@ val remove_guard : t -> HilExp.t -> t
 val unlock_guard : t -> HilExp.t -> t
 (** Release the lock the guard was constructed with. *)
 
-type summary = {critical_pairs: CriticalPairs.t; thread: ThreadDomain.t}
+val schedule_work :
+  Location.t -> StarvationModels.executor_thread_constraint -> t -> Typ.Procname.t -> t
+(** record the fact that a method is scheduled to run on a certain thread/executor *)
+
+type summary =
+  {critical_pairs: CriticalPairs.t; thread: ThreadDomain.t; scheduled_work: ScheduledWorkDomain.t}
 
 val pp_summary : F.formatter -> summary -> unit
 

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

@@ -0,0 +1,99 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+import android.os.Binder;
+import android.os.RemoteException;
+import java.util.concurrent.Executor;
+
+@interface ForUiThread {}
+
+@interface ForNonUiThread {}
+
+class ExecutorRunnable {
+  static Binder binder;
+  @ForUiThread private final Executor mUiThreadExecutor = null;
+  @ForNonUiThread private final Executor mNonUiThreadExecutor = null;
+
+  private static void doTransact() {
+    try {
+      binder.transact(0, null, null, 0);
+    } catch (RemoteException e) {
+    }
+  }
+
+  public void FN_postBlockingCallToUIThreadBad() {
+    mUiThreadExecutor.execute(
+        new Runnable() {
+          @Override
+          public void run() {
+            doTransact();
+          }
+        });
+  }
+
+  public void postBlockingCallToNonUIThreadOk() {
+    mNonUiThreadExecutor.execute(
+        new Runnable() {
+          @Override
+          public void run() {
+            doTransact();
+          }
+        });
+  }
+
+  Object monitorA, monitorB;
+
+  private void lockAB() {
+    synchronized (monitorA) {
+      synchronized (monitorB) {
+      }
+    }
+  }
+
+  private void lockBA() {
+    synchronized (monitorB) {
+      synchronized (monitorA) {
+      }
+    }
+  }
+
+  public void FN_postDeadlockBad() {
+    mUiThreadExecutor.execute(
+        new Runnable() {
+          @Override
+          public void run() {
+            lockAB();
+          }
+        });
+
+    mNonUiThreadExecutor.execute(
+        new Runnable() {
+          @Override
+          public void run() {
+            lockBA();
+          }
+        });
+  }
+
+  public void postOnUIThreadOk() {
+    mUiThreadExecutor.execute(
+        new Runnable() {
+          @Override
+          public void run() {
+            lockAB();
+          }
+        });
+
+    mUiThreadExecutor.execute(
+        new Runnable() {
+          @Override
+          public void run() {
+            lockBA();
+          }
+        });
+  }
+}