[starvation] report binder calls on ui thread

Reviewed By: sblackshear

Differential Revision: D7670674

fbshipit-source-id: 15b858c

infer/src/IR/HilExp.ml

@@ -203,6 +203,8 @@ let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ =
 
 let is_null_literal = function Constant (Cint n) -> IntLit.isnull n | _ -> false
 
+let is_int_zero = function Constant Const.Cint i -> IntLit.iszero i | _ -> false
+
 let rec eval_arithmetic_binop op e1 e2 =
   match (eval e1, eval e2) with
   | Some (Const.Cint i1), Some (Const.Cint i2) ->

infer/src/IR/HilExp.mli

@@ -40,4 +40,6 @@ val get_access_exprs : t -> AccessExpression.t list
 
 val is_null_literal : t -> bool
 
+val is_int_zero : t -> bool
+
 val eval : t -> Const.t option

infer/src/concurrency/starvation.ml

@@ -10,7 +10,7 @@ open! IStd
 module F = Format
 module L = Logging
 
-let debug fmt = F.kasprintf L.d_strln fmt
+let debug fmt = L.(debug Analysis Verbose fmt)
 
 let is_java_static pname =
   match pname with
@@ -20,6 +20,22 @@ let is_java_static pname =
       false
 
 
+(* an IBinder.transact call is an RPC.  If the 4th argument (5th counting `this` as the first)
+   is int-zero then a reply is expected and returned from the remote process, thus potentially
+   blocking.  If the 4th argument is anything else, we assume a one-way call which doesn't block.
+*)
+let is_two_way_binder_transact tenv actuals pn =
+  match pn with
+  | Typ.Procname.Java java_pname ->
+      let classname = Typ.Procname.Java.get_class_type_name java_pname in
+      let mthd = Typ.Procname.Java.get_method java_pname in
+      String.equal mthd "transact"
+      && PatternMatch.is_subtype_of_str tenv classname "android.os.IBinder"
+      && List.nth actuals 4 |> Option.value_map ~default:false ~f:HilExp.is_int_zero
+  | _ ->
+      false
+
+
 let is_on_main_thread pn =
   RacerDConfig.(match Models.get_thread pn with Models.MainThread -> true | _ -> false)
 
@@ -50,7 +66,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   type extras = FormalMap.t
 
-  let exec_instr (astate: Domain.astate) {ProcData.pdesc; extras} _ (instr: HilInstr.t) =
+  let exec_instr (astate: Domain.astate) {ProcData.pdesc; tenv; extras} _ (instr: HilInstr.t) =
     let open RacerDConfig in
     let is_formal base = FormalMap.is_formal base extras in
     let get_path actuals =
@@ -73,20 +89,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Call (_, Direct callee_pname, actuals, _, loc) -> (
       match Models.get_lock callee_pname actuals with
       | Lock ->
-          get_path actuals
-          |> Option.value_map ~default:astate ~f:(fun path -> Domain.acquire path astate loc)
+          get_path actuals |> Option.value_map ~default:astate ~f:(Domain.acquire astate loc)
       | Unlock ->
-          get_path actuals
-          |> Option.value_map ~default:astate ~f:(fun path -> Domain.release path astate)
+          get_path actuals |> Option.value_map ~default:astate ~f:(Domain.release astate)
       | LockedIfTrue ->
           astate
       | NoEffect ->
-          if is_on_main_thread callee_pname then Domain.set_on_main_thread astate
+          if is_two_way_binder_transact tenv actuals callee_pname then
+            Domain.blocking_call callee_pname loc astate
+          else if is_on_main_thread callee_pname then Domain.set_on_main_thread astate
           else
             Summary.read_summary pdesc callee_pname
-            |> Option.value_map ~default:astate ~f:(fun callee_summary ->
-                   Domain.integrate_summary ~caller_state:astate ~callee_summary callee_pname loc
-               ) )
+            |> Option.value_map ~default:astate
+                 ~f:(Domain.integrate_summary astate callee_pname loc) )
     | _ ->
         astate
 
@@ -104,14 +119,6 @@ let should_skip_during_deadlock_reporting _ _ = false
 
 (* currently short-circuited until non-determinism in reporting is dealt with *)
 (* Typ.Name.compare current_class eventually_class < 0 *)
-
-let get_class_of_pname = function
-  | Typ.Procname.Java java_pname ->
-      Some (Typ.Procname.Java.get_class_type_name java_pname)
-  | _ ->
-      None
-
-
 (* let false_if_none a ~f = Option.value_map a ~default:false ~f *)
 (* if same class, report only if the locks order in one of the possible ways *)
 let should_report_if_same_class _ = true
@@ -147,6 +154,13 @@ let get_summary caller_pdesc callee_pdesc =
   |> Option.map ~f:(fun summary -> (callee_pdesc, summary))
 
 
+let get_class_of_pname = function
+  | Typ.Procname.Java java_pname ->
+      Some (Typ.Procname.Java.get_class_type_name java_pname)
+  | _ ->
+      None
+
+
 let report_deadlocks get_proc_desc tenv pdesc (summary, _) =
   let open StarvationDomain in
   let process_callee_elem caller_pdesc caller_elem callee_pdesc elem =
@@ -203,6 +217,29 @@ let report_deadlocks get_proc_desc tenv pdesc (summary, _) =
   |> Option.iter ~f:(fun curr_class -> LockOrderDomain.iter (report_pair curr_class) summary)
 
 
+let report_direct_blocks_on_main_thread proc_desc summary =
+  let open StarvationDomain in
+  let report_pair ({LockOrder.eventually} as elem) =
+    match eventually with
+    | {LockEvent.event= LockEvent.MayBlock _} ->
+        let caller_loc = Procdesc.get_loc proc_desc in
+        let caller_pname = Procdesc.get_proc_name proc_desc in
+        let error_message =
+          Format.asprintf "May block while on main thread. Eventually: %a" LockEvent.pp_event
+            eventually.LockEvent.event
+        in
+        let exn =
+          Exceptions.Checkers (IssueType.starvation, Localise.verbatim_desc error_message)
+        in
+        let ltr = make_trace_with_header elem caller_loc caller_pname in
+        Specs.get_summary caller_pname
+        |> Option.iter ~f:(fun summary -> Reporting.log_error summary ~loc:caller_loc ~ltr exn)
+    | _ ->
+        ()
+  in
+  LockOrderDomain.iter report_pair summary
+
+
 let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
   let pname = Procdesc.get_proc_name proc_desc in
   let formals = FormalMap.make proc_desc in
@@ -218,8 +255,13 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
           |> Option.map ~f:(fun tn -> Typ.Name.name tn |> Ident.string_to_name |> lock_of_class)
         else FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> (base, []))
       in
-      Option.value_map lock ~default:StarvationDomain.empty ~f:(fun path ->
-          StarvationDomain.acquire path StarvationDomain.empty loc )
+      Option.value_map lock ~default:StarvationDomain.empty
+        ~f:(StarvationDomain.acquire StarvationDomain.empty loc)
+  in
+  let initial =
+    if RacerDConfig.Models.runs_on_ui_thread proc_desc then
+      StarvationDomain.set_on_main_thread initial
+    else initial
   in
   match Analyzer.compute_post proc_data ~initial with
   | None ->
@@ -229,4 +271,6 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
       let updated_summary = Summary.update_summary lock_order summary in
       Option.iter updated_summary.Specs.payload.starvation
         ~f:(report_deadlocks get_proc_desc tenv proc_desc) ;
+      Option.iter updated_summary.Specs.payload.starvation ~f:(fun (sum, main) ->
+          if main then report_direct_blocks_on_main_thread proc_desc sum ) ;
       updated_summary

infer/src/concurrency/starvationDomain.ml

@@ -103,7 +103,12 @@ module LockEvent = struct
 
   let make_acquire lock loc = {event= LockAcquire lock; loc; trace= []}
 
-  let _make_blocks msg loc = {event= MayBlock msg; loc; trace= []}
+  let make_blocks msg loc = {event= MayBlock msg; loc; trace= []}
+
+  let make_blocking_call pname loc =
+    let descr = F.asprintf "Calls %a" Typ.Procname.pp pname in
+    make_blocks descr loc
+
 
   let make_loc_trace ?(reverse= false) e =
     let call_trace, nesting =
@@ -236,16 +241,22 @@ let add_order_pairs ls lock_event acc =
     LockState.fold_over_events add_first_and_eventually ls acc |> add_eventually
 
 
-let acquire lockid ((ls, lo), main) loc =
+let acquire ((ls, lo), main) loc lockid =
   let newlock_event = LockEvent.make_acquire lockid loc in
   let lo' = add_order_pairs ls newlock_event lo in
   let ls' = LockState.acquire lockid newlock_event ls in
   ((ls', lo'), main)
 
 
-let release lockid ((ls, lo), main) = ((LockState.release lockid ls, lo), main)
+let blocking_call pname loc ((ls, lo), main) =
+  let newlock_event = LockEvent.make_blocking_call pname loc in
+  let lo' = add_order_pairs ls newlock_event lo in
+  ((ls, lo'), main)
+
+
+let release ((ls, lo), main) lockid = ((LockState.release lockid ls, lo), main)
 
-let integrate_summary ~caller_state:((ls, lo), main) ~callee_summary callee_pname loc =
+let integrate_summary ((ls, lo), main) callee_pname loc callee_summary =
   let callee_lo, callee_main = callee_summary in
   (* for each pair (b,a) in the callee, add (l,b) and (l,a) to the current state, where
      l is held locally *)

infer/src/concurrency/starvationDomain.mli

@@ -18,6 +18,8 @@ module LockIdentity : PrettyPrintable.PrintableOrderedType with type t = AccessP
 module LockEvent : sig
   type event_t = private LockAcquire of LockIdentity.t | MayBlock of string
 
+  val pp_event : F.formatter -> event_t -> unit
+
   type t = private {event: event_t; loc: Location.t; trace: CallSite.t list}
 
   include PrettyPrintable.PrintableOrderedType with type t := t
@@ -56,9 +58,11 @@ end
 
 include AbstractDomain.WithBottom
 
-val acquire : LockIdentity.t -> astate -> Location.t -> astate
+val acquire : astate -> Location.t -> LockIdentity.t -> astate
+
+val release : astate -> LockIdentity.t -> astate
 
-val release : LockIdentity.t -> astate -> astate
+val blocking_call : Typ.Procname.t -> Location.t -> astate -> astate
 
 val set_on_main_thread : astate -> astate
 
@@ -68,5 +72,4 @@ val pp_summary : F.formatter -> summary -> unit
 
 val to_summary : astate -> summary
 
-val integrate_summary :
-  caller_state:astate -> callee_summary:summary -> Typ.Procname.t -> Location.t -> astate
+val integrate_summary : astate -> Typ.Procname.t -> Location.t -> summary -> astate

infer/tests/codetoanalyze/java/starvation/Binders.java

@@ -0,0 +1,56 @@
+/*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+import android.os.Binder;
+import android.os.RemoteException;
+import android.support.annotation.UiThread;
+
+class Binders {
+  Binder b;
+
+  void doTransact() throws RemoteException {
+    b.transact(0, null, null, 0);
+  }
+
+  void doOneWayTransact() throws RemoteException {
+    b.transact(0, null, null, 1);
+  }
+
+  void interBad() throws RemoteException {
+    b.transact(0, null, null, 0);
+    forceMainThread();
+  }
+
+  void intraBad() throws RemoteException {
+    OurThreadUtils.assertMainThread();
+    doTransact();
+  }
+
+  @UiThread
+  void annotationBad() throws RemoteException {
+    doTransact();
+  }
+
+  void intraOk() throws RemoteException {
+    b.transact(0, null, null, 0);
+  }
+
+  void interOk() throws RemoteException {
+    doTransact();
+  }
+
+  void oneWayOk() throws RemoteException {
+    OurThreadUtils.assertMainThread();
+    doOneWayTransact();
+  }
+
+  void forceMainThread() {
+    OurThreadUtils.assertMainThread();
+  }
+}

infer/tests/codetoanalyze/java/starvation/OurThreadUtils.java

@@ -0,0 +1,14 @@
+/*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+class OurThreadUtils{
+  native static boolean isMainThread();
+  static void assertMainThread(){}
+  static void assertHoldsLock(Object lock){}
+}

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

@@ -1,3 +1,6 @@
+codetoanalyze/java/starvation/Binders.java, void Binders.annotationBad(), 0, STARVATION, ERROR, [Method start: void Binders.annotationBad(),Method call: void Binders.doTransact(),Calls boolean Binder.transact(int,Parcel,Parcel,int)]
+codetoanalyze/java/starvation/Binders.java, void Binders.interBad(), 0, STARVATION, ERROR, [Method start: void Binders.interBad(),Calls boolean Binder.transact(int,Parcel,Parcel,int)]
+codetoanalyze/java/starvation/Binders.java, void Binders.intraBad(), 0, STARVATION, ERROR, [Method start: void Binders.intraBad(),Method call: void Binders.doTransact(),Calls boolean Binder.transact(int,Parcel,Parcel,int)]
 codetoanalyze/java/starvation/InnerClass.java, void InnerClass$InnerClassA.innerOuterBad(), 0, STARVATION, ERROR, [[Trace 1] Locks this in class InnerClass$InnerClassA*,Method call: void InnerClass.bar(),Locks this in class InnerClass*,[Trace 2] Locks this in class InnerClass*,Method call: void InnerClass$InnerClassA.baz(),Locks this in class InnerClass$InnerClassA*]
 codetoanalyze/java/starvation/InnerClass.java, void InnerClass.outerInnerBad(InnerClass$InnerClassA), 0, STARVATION, ERROR, [[Trace 1] Locks this in class InnerClass*,Method call: void InnerClass$InnerClassA.baz(),Locks this in class InnerClass$InnerClassA*,[Trace 2] Method start: InnerClass$InnerClassA.<init>(InnerClass,Object),Locks this in class InnerClass$InnerClassA*,Method call: void InnerClass.bar(),Locks this in class InnerClass*]
 codetoanalyze/java/starvation/Interclass.java, void InterclassA.interclass2Bad(Interclass), 0, STARVATION, ERROR, [[Trace 1] Locks this in class InterclassA*,Method call: void Interclass.interclass2Bad(),Locks this in class Interclass*,[Trace 2] Locks this in class Interclass*,Method call: void InterclassA.interclass1Bad(),Locks this in class InterclassA*]