[starvation][whole-program] Looper and Handler models and semantics

Summary: Another way to schedule work in android is by posting it to a `Handler`.  A handler can be constructed out of the main looper, which forces it to schedule work on the UI thread.  To model all this, we add syntactic models for getting the main looper and for creating handlers, and dataflow attributes for tracking that an expression is a looper/the main looper, or a handler constructed out of a looper.

Reviewed By: skcho

Differential Revision: D18706768

fbshipit-source-id: 7c46e6913

infer/src/concurrency/StarvationModels.ml

@@ -213,7 +213,10 @@ let schedules_work =
     [ { default with
         classname= executor_type_str
       ; methods= ["execute"; "schedule"; "scheduleAtFixedRate"; "scheduleWithFixedDelay"; "submit"]
-      } ]
+      }
+    ; { default with
+        classname= "android.os.Handler"
+      ; methods= ["post"; "postAtFrontOfQueue"; "postAtTime"; "postDelayed"] } ]
     |> of_records
   in
   fun tenv pname -> matcher tenv pname []
@@ -239,7 +242,7 @@ let schedules_work_on_bg_thread =
   fun tenv pname -> matcher tenv pname []
 
 
-type executor_thread_constraint = ForUIThread | ForNonUIThread | ForUnknownThread
+type scheduler_thread_constraint = ForUIThread | ForNonUIThread | ForUnknownThread
 [@@deriving equal]
 
 (* Executors are sometimes stored in fields and annotated according to what type of thread 
@@ -307,3 +310,21 @@ let get_returned_executor ~attrs_of_pname tenv callee actuals =
         None )
   | _ ->
       None
+
+
+let is_getMainLooper =
+  let open MethodMatcher in
+  [ { default with
+      classname= "android.os.Looper"
+    ; methods= ["getMainLooper"]
+    ; actuals_pred= List.is_empty } ]
+  |> of_records
+
+
+let is_handler_constructor =
+  let open MethodMatcher in
+  [ { default with
+      classname= "android.os.Handler"
+    ; methods= [Typ.Procname.Java.constructor_method_name]
+    ; actuals_pred= (fun actuals -> not (List.is_empty actuals)) } ]
+  |> of_records

infer/src/concurrency/StarvationModels.mli

@@ -33,14 +33,14 @@ val is_annotated_lockless :
 (** 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 *)
+(** call known to schedule runnable first argument to some executor/handler or subclass *)
 
 (** 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 | ForUnknownThread
+type scheduler_thread_constraint = ForUIThread | ForNonUIThread | ForUnknownThread
 [@@deriving equal]
 
 val get_executor_thread_annotation_constraint :
-  Tenv.t -> HilExp.AccessExpression.t -> executor_thread_constraint option
+  Tenv.t -> HilExp.AccessExpression.t -> scheduler_thread_constraint option
 (** given an executor receiver, get its thread constraint, if any. [None] means lookup somehow failed, 
     whereas [Some UnknownThread] means the receiver is an unannotated executor. *)
 
@@ -52,7 +52,7 @@ val get_returned_executor :
   -> Tenv.t
   -> Typ.Procname.t
   -> HilExp.t list
-  -> executor_thread_constraint option
+  -> scheduler_thread_constraint option
 (** does the function return an executor and of which thread? *)
 
 val schedules_work_on_ui_thread : Tenv.t -> Typ.Procname.t -> bool
@@ -60,3 +60,7 @@ val schedules_work_on_ui_thread : Tenv.t -> Typ.Procname.t -> bool
 
 val schedules_work_on_bg_thread : Tenv.t -> Typ.Procname.t -> bool
 (** method call known to directly schedule work on BG thread *)
+
+val is_getMainLooper : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool
+
+val is_handler_constructor : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool

infer/src/concurrency/starvation.ml

@@ -79,7 +79,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     AttributeDomain.find_opt exp astate.attributes
     |> IOption.if_none_evalopt ~f:(fun () ->
            StarvationModels.get_executor_thread_annotation_constraint tenv exp
-           |> Option.map ~f:(fun constr -> Attribute.Executor constr) )
+           |> Option.map ~f:(fun constr -> Attribute.WorkScheduler constr) )
     |> IOption.if_none_evalopt ~f:(fun () ->
            StarvationModels.get_run_method_from_runnable tenv exp
            |> Option.map ~f:(fun procname -> Attribute.Runnable procname) )
@@ -87,32 +87,31 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   let do_work_scheduling tenv callee actuals loc (astate : Domain.t) =
     let open Domain in
-    let schedule_work runnable thread =
+    let schedule_work (runnable, thread) =
-      match get_exp_attributes tenv runnable astate with
+      get_exp_attributes tenv runnable astate
-      | Some (Attribute.Runnable procname) ->
+      |> Option.bind ~f:(function Attribute.Runnable procname -> Some procname | _ -> None)
-          Domain.schedule_work loc thread astate procname
+      |> Option.fold ~init:astate ~f:(Domain.schedule_work loc thread)
-      | _ ->
-          astate
     in
+    let work_opt =
       match actuals with
       | HilExp.AccessExpression executor :: HilExp.AccessExpression runnable :: _
         when StarvationModels.schedules_work tenv callee ->
           let thread =
-          match get_exp_attributes tenv executor astate with
+            get_exp_attributes tenv executor astate
-          | Some (Attribute.Executor constr) ->
+            |> Option.bind ~f:(function Attribute.WorkScheduler c -> Some c | _ -> None)
-              constr
+            |> Option.value ~default:StarvationModels.ForUnknownThread
-          | _ ->
-              StarvationModels.ForUnknownThread
           in
-        schedule_work runnable thread
+          Some (runnable, thread)
       | HilExp.AccessExpression runnable :: _
         when StarvationModels.schedules_work_on_ui_thread tenv callee ->
-        schedule_work runnable StarvationModels.ForUIThread
+          Some (runnable, StarvationModels.ForUIThread)
       | HilExp.AccessExpression runnable :: _
         when StarvationModels.schedules_work_on_bg_thread tenv callee ->
-        schedule_work runnable StarvationModels.ForNonUIThread
+          Some (runnable, StarvationModels.ForNonUIThread)
       | _ ->
-        astate
+          None
+    in
+    Option.value_map work_opt ~default:astate ~f:schedule_work
 
 
   let do_assignment tenv lhs_access_exp rhs_exp (astate : Domain.t) =
@@ -126,26 +125,51 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   let do_call ProcData.{tenv; summary} lhs callee actuals loc astate =
     let open Domain in
+    let make_ret_attr return_attribute = {empty_summary with return_attribute} in
+    let make_thread thread = {empty_summary with thread} in
     let get_returned_executor_summary () =
       StarvationModels.get_returned_executor ~attrs_of_pname tenv callee actuals
       |> Option.map ~f:(fun thread_constraint ->
-             {empty_summary with return_attribute= Attribute.Executor thread_constraint} )
+             make_ret_attr (Attribute.WorkScheduler thread_constraint) )
     in
     let get_thread_assert_summary () =
       match ConcurrencyModels.get_thread_assert_effect callee with
       | BackgroundThread ->
-          Some {empty_summary with thread= ThreadDomain.BGThread}
+          Some (make_thread ThreadDomain.BGThread)
       | MainThread ->
-          Some {empty_summary with thread= ThreadDomain.UIThread}
+          Some (make_thread ThreadDomain.UIThread)
       | MainThreadIfTrue ->
-          Some {empty_summary with return_attribute= Attribute.ThreadGuard}
+          Some (make_ret_attr Attribute.ThreadGuard)
       | UnknownThread ->
           None
     in
+    let get_mainLooper_summary () =
+      if StarvationModels.is_getMainLooper tenv callee actuals then
+        Some (make_ret_attr (Attribute.Looper StarvationModels.ForUIThread))
+      else None
+    in
     let get_callee_summary () = Payload.read ~caller_summary:summary ~callee_pname:callee in
     let callsite = CallSite.make callee loc in
+    (* constructor calls are special-cased because they side-effect the receiver and do not
+       return anything *)
+    if StarvationModels.is_handler_constructor tenv callee actuals then
+      match actuals with
+      | HilExp.AccessExpression receiver :: HilExp.AccessExpression exp :: _ ->
+          let thread_constraint_attr =
+            AttributeDomain.find_opt exp astate.attributes
+            |> Option.bind ~f:(function Attribute.Looper c -> Some c | _ -> None)
+            |> Option.value ~default:StarvationModels.ForUnknownThread
+            |> fun constr -> Attribute.WorkScheduler constr
+          in
+          let attributes = AttributeDomain.add receiver thread_constraint_attr astate.attributes in
+          {astate with attributes}
+      | _ ->
+          astate
+    else
       get_returned_executor_summary ()
       |> IOption.if_none_evalopt ~f:get_thread_assert_summary
+      |> IOption.if_none_evalopt ~f:get_mainLooper_summary
+      (* [get_callee_summary] should come after all models *)
       |> IOption.if_none_evalopt ~f:get_callee_summary
       |> Option.fold ~init:astate ~f:(Domain.integrate_summary ~tenv ~lhs callsite)
 

infer/src/concurrency/starvationDomain.ml

@@ -447,8 +447,9 @@ module Attribute = struct
   type t =
     | Nothing
     | ThreadGuard
-    | Executor of StarvationModels.executor_thread_constraint
     | Runnable of Typ.Procname.t
+    | WorkScheduler of StarvationModels.scheduler_thread_constraint
+    | Looper of StarvationModels.scheduler_thread_constraint
   [@@deriving equal]
 
   let top = Nothing
@@ -466,10 +467,12 @@ module Attribute = struct
         F.pp_print_string fmt "Nothing"
     | ThreadGuard ->
         F.pp_print_string fmt "ThreadGuard"
-    | Executor c ->
-        F.fprintf fmt "Executor(%a)" pp_constr c
     | Runnable runproc ->
         F.fprintf fmt "Runnable(%a)" Typ.Procname.pp runproc
+    | WorkScheduler c ->
+        F.fprintf fmt "WorkScheduler(%a)" pp_constr c
+    | Looper c ->
+        F.fprintf fmt "Looper(%a)" pp_constr c
 
 
   let join lhs rhs = if equal lhs rhs then lhs else Nothing
@@ -486,8 +489,8 @@ module AttributeDomain = struct
     find_opt acc_exp t |> Option.exists ~f:(function Attribute.ThreadGuard -> true | _ -> false)
 
 
-  let get_executor_constraint acc_exp t =
+  let get_scheduler_constraint acc_exp t =
-    find_opt acc_exp t |> Option.bind ~f:(function Attribute.Executor c -> Some c | _ -> None)
+    find_opt acc_exp t |> Option.bind ~f:(function Attribute.WorkScheduler c -> Some c | _ -> None)
 
 
   let exit_scope vars t =
@@ -635,7 +638,7 @@ let filter_blocking_calls ({critical_pairs} as astate) =
 
 let schedule_work loc thread_constraint astate procname =
   let thread : ThreadDomain.t =
-    match (thread_constraint : StarvationModels.executor_thread_constraint) with
+    match (thread_constraint : StarvationModels.scheduler_thread_constraint) with
     | ForUIThread ->
         UIThread
     | ForNonUIThread ->

infer/src/concurrency/starvationDomain.mli

@@ -102,19 +102,20 @@ module CriticalPairs : AbstractDomain.FiniteSetS with type elt = CriticalPair.t
 
 module GuardToLockMap : AbstractDomain.WithTop
 
-(** Tracks whether a variable has been tested for whether we execute on UI thread, or 
+(** Tracks expression attributes *)
-    has been assigned an executor object. *)
 module Attribute : sig
   type t =
     | Nothing
-    | ThreadGuard
+    | ThreadGuard  (** is boolean equivalent to whether on UI thread *)
-    | Executor of StarvationModels.executor_thread_constraint
+    | Runnable of Typ.Procname.t  (** is a Runnable/Callable with given "run" procname *)
-    | Runnable of Typ.Procname.t
+    | WorkScheduler of StarvationModels.scheduler_thread_constraint
+        (** exp is something that schedules work on the given thread *)
+    | Looper of StarvationModels.scheduler_thread_constraint  (** Android looper on given thread *)
 
   include AbstractDomain.WithTop with type t := t
 end
 
-(** Tracks all variables assigned values of [Attribute] *)
+(** Tracks all expressions assigned values of [Attribute] *)
 module AttributeDomain : sig
   include
     AbstractDomain.InvertedMapS
@@ -123,8 +124,8 @@ module AttributeDomain : sig
 
   val is_thread_guard : HilExp.AccessExpression.t -> t -> bool
 
-  val get_executor_constraint :
+  val get_scheduler_constraint :
-    HilExp.AccessExpression.t -> t -> StarvationModels.executor_thread_constraint option
+    HilExp.AccessExpression.t -> t -> StarvationModels.scheduler_thread_constraint option
 
   val exit_scope : Var.t list -> t -> t
 end
@@ -179,7 +180,7 @@ val unlock_guard : t -> HilExp.t -> t
 (** Release the lock the guard was constructed with. *)
 
 val schedule_work :
-  Location.t -> StarvationModels.executor_thread_constraint -> t -> Typ.Procname.t -> t
+  Location.t -> StarvationModels.scheduler_thread_constraint -> t -> Typ.Procname.t -> t
 (** record the fact that a method is scheduled to run on a certain thread/executor *)
 
 type summary =

infer/tests/codetoanalyze/java/starvation-whole-program/ModeledHandler.java

@@ -0,0 +1,35 @@
+/*
+ * 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.Handler;
+import android.os.Looper;
+import android.os.RemoteException;
+
+class ModeledHandler {
+  static Binder binder;
+
+  private static void doTransact() {
+    try {
+      binder.transact(0, null, null, 0);
+    } catch (RemoteException e) {
+    }
+  }
+
+  // starvation via scheduling a transaction on UI thread
+  public void postBlockingCallToUIThreadBad() {
+    Handler handler = new Handler(Looper.getMainLooper());
+
+    handler.post(
+        new Runnable() {
+          @Override
+          public void run() {
+            doTransact();
+          }
+        });
+  }
+}

infer/tests/codetoanalyze/java/starvation-whole-program/issues.exp

@@ -16,6 +16,7 @@ codetoanalyze/java/starvation-whole-program/ModeledExecutors.java, ModeledExecut
 codetoanalyze/java/starvation-whole-program/ModeledExecutors.java, ModeledExecutors.staticRunBlockingCallToUIThreadBad():void, 61, STARVATION, no_bucket, ERROR, [`void ModeledExecutors.staticRunBlockingCallToUIThreadBad()`,Method call: `void ModeledExecutors$4.run()`,Method call: `void ModeledExecutors.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
 codetoanalyze/java/starvation-whole-program/ModeledExecutors.java, ModeledExecutors.submitBadCallableToUIThreadBad():void, 152, STARVATION, no_bucket, ERROR, [`void ModeledExecutors.submitBadCallableToUIThreadBad()`,Method call: `Object ModeledExecutors$11.call()`,Method call: `void ModeledExecutors.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
 codetoanalyze/java/starvation-whole-program/ModeledExecutors.java, ModeledExecutors.submitBlockingCallToUIThreadBad():void, 125, STARVATION, no_bucket, ERROR, [`void ModeledExecutors.submitBlockingCallToUIThreadBad()`,Method call: `void ModeledExecutors$9.run()`,Method call: `void ModeledExecutors.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
+codetoanalyze/java/starvation-whole-program/ModeledHandler.java, ModeledHandler.postBlockingCallToUIThreadBad():void, 27, STARVATION, no_bucket, ERROR, [`void ModeledHandler.postBlockingCallToUIThreadBad()`,Method call: `void ModeledHandler$1.run()`,Method call: `void ModeledHandler.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
 codetoanalyze/java/starvation-whole-program/MyActivity.java, MyActivity.onCreate(android.os.Bundle):void, 28, STARVATION, no_bucket, ERROR, [`void MyActivity.onCreate(Bundle)`,Method call: `void MyActivity.bad()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
 codetoanalyze/java/starvation-whole-program/MyActivity.java, MyActivity.onDestroy():void, 68, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MyActivity.onDestroy()`, locks `this.monitorC` in `class MyActivity`, locks `this.monitorB` in `class MyActivity`,[Trace 2] `void MyActivity.onPause()`,Method call: `void MyActivity$2.run()`, locks `this.monitorB` in `class MyActivity`, locks `this.monitorC` in `class MyActivity`]
 codetoanalyze/java/starvation-whole-program/MyActivity.java, MyActivity.onPause():void, 76, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MyActivity.onPause()`,Method call: `void MyActivity$2.run()`, locks `this.monitorB` in `class MyActivity`, locks `this.monitorC` in `class MyActivity`,[Trace 2] `void MyActivity.onDestroy()`, locks `this.monitorC` in `class MyActivity`, locks `this.monitorB` in `class MyActivity`]