From 82a9f1ac65b275988cfd981459def672d3e40590 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Fri, 29 Nov 2019 06:03:59 -0800 Subject: [PATCH] [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 | 25 +++++- infer/src/concurrency/StarvationModels.mli | 12 ++- infer/src/concurrency/starvation.ml | 90 ++++++++++++------- infer/src/concurrency/starvationDomain.ml | 15 ++-- infer/src/concurrency/starvationDomain.mli | 19 ++-- .../ModeledHandler.java | 35 ++++++++ .../java/starvation-whole-program/issues.exp | 1 + 7 files changed, 143 insertions(+), 54 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/starvation-whole-program/ModeledHandler.java diff --git a/infer/src/concurrency/StarvationModels.ml b/infer/src/concurrency/StarvationModels.ml index 83338214e..75c9f4c62 100644 --- a/infer/src/concurrency/StarvationModels.ml +++ b/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 diff --git a/infer/src/concurrency/StarvationModels.mli b/infer/src/concurrency/StarvationModels.mli index 8f578b846..2e8c9cc3a 100644 --- a/infer/src/concurrency/StarvationModels.mli +++ b/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 diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 8143ae50a..6d1552fa2 100644 --- a/infer/src/concurrency/starvation.ml +++ b/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 = - match get_exp_attributes tenv runnable astate with - | Some (Attribute.Runnable procname) -> - Domain.schedule_work loc thread astate procname + let schedule_work (runnable, thread) = + get_exp_attributes tenv runnable astate + |> Option.bind ~f:(function Attribute.Runnable procname -> Some procname | _ -> None) + |> Option.fold ~init:astate ~f:(Domain.schedule_work loc thread) + in + let work_opt = + match actuals with + | HilExp.AccessExpression executor :: HilExp.AccessExpression runnable :: _ + when StarvationModels.schedules_work tenv callee -> + let thread = + get_exp_attributes tenv executor astate + |> Option.bind ~f:(function Attribute.WorkScheduler c -> Some c | _ -> None) + |> Option.value ~default:StarvationModels.ForUnknownThread + in + Some (runnable, thread) + | HilExp.AccessExpression runnable :: _ + when StarvationModels.schedules_work_on_ui_thread tenv callee -> + Some (runnable, StarvationModels.ForUIThread) + | HilExp.AccessExpression runnable :: _ + when StarvationModels.schedules_work_on_bg_thread tenv callee -> + Some (runnable, StarvationModels.ForNonUIThread) | _ -> - astate + None in - 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 - | Some (Attribute.Executor constr) -> - constr - | _ -> - StarvationModels.ForUnknownThread - in - schedule_work runnable thread - | HilExp.AccessExpression runnable :: _ - when StarvationModels.schedules_work_on_ui_thread tenv callee -> - schedule_work runnable StarvationModels.ForUIThread - | HilExp.AccessExpression runnable :: _ - when StarvationModels.schedules_work_on_bg_thread tenv callee -> - schedule_work runnable StarvationModels.ForNonUIThread - | _ -> - astate + Option.value_map work_opt ~default:astate ~f:schedule_work let do_assignment tenv lhs_access_exp rhs_exp (astate : Domain.t) = @@ -126,28 +125,53 @@ 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 - get_returned_executor_summary () - |> IOption.if_none_evalopt ~f:get_thread_assert_summary - |> IOption.if_none_evalopt ~f:get_callee_summary - |> Option.fold ~init:astate ~f:(Domain.integrate_summary ~tenv ~lhs callsite) + (* 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) let exec_instr (astate : Domain.t) ({ProcData.summary; tenv; extras} as procdata) _ diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 0caf03cb3..ad051726b 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/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 = - find_opt acc_exp t |> Option.bind ~f:(function Attribute.Executor c -> Some c | _ -> None) + let get_scheduler_constraint acc_exp t = + 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 -> diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 1b0811d71..06fba8b48 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/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 - has been assigned an executor object. *) +(** Tracks expression attributes *) module Attribute : sig type t = | Nothing - | ThreadGuard - | Executor of StarvationModels.executor_thread_constraint - | Runnable of Typ.Procname.t + | ThreadGuard (** is boolean equivalent to whether on UI thread *) + | Runnable of Typ.Procname.t (** is a Runnable/Callable with given "run" procname *) + | 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 : - HilExp.AccessExpression.t -> t -> StarvationModels.executor_thread_constraint option + val get_scheduler_constraint : + 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 = diff --git a/infer/tests/codetoanalyze/java/starvation-whole-program/ModeledHandler.java b/infer/tests/codetoanalyze/java/starvation-whole-program/ModeledHandler.java new file mode 100644 index 000000000..591801b8d --- /dev/null +++ b/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(); + } + }); + } +} diff --git a/infer/tests/codetoanalyze/java/starvation-whole-program/issues.exp b/infer/tests/codetoanalyze/java/starvation-whole-program/issues.exp index 8c8a96c66..07d7b289c 100644 --- a/infer/tests/codetoanalyze/java/starvation-whole-program/issues.exp +++ b/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`]