From b6c8766b113bb523a740537b10c8e8915b4d29af Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Thu, 19 Apr 2018 08:55:30 -0700 Subject: [PATCH] [starvation] report binder calls on ui thread Reviewed By: sblackshear Differential Revision: D7670674 fbshipit-source-id: 15b858c --- infer/src/IR/HilExp.ml | 2 + infer/src/IR/HilExp.mli | 2 + infer/src/concurrency/starvation.ml | 84 ++++++++++++++----- infer/src/concurrency/starvationDomain.ml | 19 ++++- infer/src/concurrency/starvationDomain.mli | 11 ++- .../java/starvation/Binders.java | 56 +++++++++++++ .../java/starvation/OurThreadUtils.java | 14 ++++ .../codetoanalyze/java/starvation/issues.exp | 3 + 8 files changed, 163 insertions(+), 28 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/starvation/Binders.java create mode 100644 infer/tests/codetoanalyze/java/starvation/OurThreadUtils.java diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml index 58328edbc..b5ddb9ce2 100644 --- a/infer/src/IR/HilExp.ml +++ b/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) -> diff --git a/infer/src/IR/HilExp.mli b/infer/src/IR/HilExp.mli index ca494101d..2fbe88d71 100644 --- a/infer/src/IR/HilExp.mli +++ b/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 diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index f2a44c5e7..446b338d9 100644 --- a/infer/src/concurrency/starvation.ml +++ b/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 diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 1039129a8..fa9c7564e 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/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 *) diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 422f3b606..04e69d996 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/java/starvation/Binders.java b/infer/tests/codetoanalyze/java/starvation/Binders.java new file mode 100644 index 000000000..c17b90e00 --- /dev/null +++ b/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(); + } +} diff --git a/infer/tests/codetoanalyze/java/starvation/OurThreadUtils.java b/infer/tests/codetoanalyze/java/starvation/OurThreadUtils.java new file mode 100644 index 000000000..f9199db72 --- /dev/null +++ b/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){} +} diff --git a/infer/tests/codetoanalyze/java/starvation/issues.exp b/infer/tests/codetoanalyze/java/starvation/issues.exp index ce1c6c227..26ac59424 100644 --- a/infer/tests/codetoanalyze/java/starvation/issues.exp +++ b/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.(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*]