diff --git a/infer/src/concurrency/StarvationModels.ml b/infer/src/concurrency/StarvationModels.ml index 1e0653cbf..cb3da38ed 100644 --- a/infer/src/concurrency/StarvationModels.ml +++ b/infer/src/concurrency/StarvationModels.ml @@ -204,15 +204,15 @@ let is_annotated_lockless ~attrs_of_pname tenv pname = |> Option.is_some +let executor_type_str = "java.util.concurrent.Executor" + let schedules_work = let open MethodMatcher in - let matcher = - [{default with classname= "java.util.concurrent.Executor"; methods= ["execute"]}] |> of_records - in + let matcher = [{default with classname= executor_type_str; methods= ["execute"]}] |> of_records in fun tenv pname -> matcher tenv pname [] -type executor_thread_constraint = ForUIThread | ForNonUIThread +type executor_thread_constraint = ForUIThread | ForNonUIThread [@@deriving equal] (* 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 @@ -250,3 +250,28 @@ let get_run_method_from_runnable tenv runnable = |> 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) + + +(* Syntactically match for certain methods known to return executors. *) +let get_executor_effect ~attrs_of_pname tenv callee actuals = + let type_check = + lazy + ( attrs_of_pname callee + |> Option.exists ~f:(fun (attrs : ProcAttributes.t) -> + match attrs.ret_type.Typ.desc with + | Tstruct tname | Typ.Tptr ({desc= Tstruct tname}, _) -> + PatternMatch.is_subtype_of_str tenv tname executor_type_str + | _ -> + false ) ) + in + match (callee, actuals) with + | Typ.Procname.Java java_pname, [] -> ( + match Typ.Procname.Java.get_method java_pname with + | "getForegroundExecutor" when Lazy.force type_check -> + Some ForUIThread + | "getBackgroundExecutor" when Lazy.force type_check -> + Some ForNonUIThread + | _ -> + None ) + | _ -> + None diff --git a/infer/src/concurrency/StarvationModels.mli b/infer/src/concurrency/StarvationModels.mli index baeeff075..3aa76f5e3 100644 --- a/infer/src/concurrency/StarvationModels.mli +++ b/infer/src/concurrency/StarvationModels.mli @@ -36,7 +36,7 @@ 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 +type executor_thread_constraint = ForUIThread | ForNonUIThread [@@deriving equal] val get_executor_thread_constraint : Tenv.t -> HilExp.AccessExpression.t -> executor_thread_constraint option @@ -44,3 +44,11 @@ val get_executor_thread_constraint : 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 *) + +val get_executor_effect : + attrs_of_pname:(Typ.Procname.t -> ProcAttributes.t option) + -> Tenv.t + -> Typ.Procname.t + -> HilExp.t list + -> executor_thread_constraint option +(** does the function return an executor and of which thread? *) diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 328f4f837..6f5ad2dbe 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -36,29 +36,90 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type extras = FormalMap.t + let log_parse_error error pname actuals = + L.debug Analysis Verbose "%s pname:%a actuals:%a@." error Typ.Procname.pp pname + (PrettyPrintable.pp_collection ~pp_item:HilExp.pp) + actuals + + + (** convert an expression to a canonical form for a lock identifier *) + let get_lock_path extras = function + | HilExp.AccessExpression access_exp -> ( + match HilExp.AccessExpression.to_access_path access_exp with + | (((Var.ProgramVar pvar, _) as base), _) as path + when FormalMap.is_formal base extras || Pvar.is_global pvar -> + Some (AccessPath.inner_class_normalize path) + | _ -> + (* ignore paths on local or logical variables *) + None ) + | HilExp.Constant (Const.Cclass class_id) -> + (* this is a synchronized/lock(CLASSNAME.class) construct *) + Some (lock_of_class class_id) + | _ -> + None + + + let do_assume assume_exp (astate : Domain.t) = + let open Domain in + let add_choice (acc : Domain.t) bool_value = + let thread = if bool_value then ThreadDomain.UIThread else ThreadDomain.BGThread in + {acc with thread} + in + match HilExp.get_access_exprs assume_exp with + | [access_expr] when AttributeDomain.is_thread_guard access_expr astate.attributes -> + HilExp.eval_boolean_exp access_expr assume_exp |> Option.fold ~init:astate ~f:add_choice + | _ -> + astate + + + let do_thread_assert_effect (ret_var, _) callee (astate : Domain.t) = + let open Domain in + match ConcurrencyModels.get_thread_assert_effect callee with + | BackgroundThread -> + {astate with thread= ThreadDomain.BGThread} + | MainThread -> + {astate with thread= ThreadDomain.UIThread} + | MainThreadIfTrue -> + let attributes = AttributeDomain.add ret_var Attribute.Thread astate.attributes in + {astate with attributes} + | UnknownThread -> + astate + + + let do_work_scheduling tenv callee actuals loc (astate : Domain.t) = + let schedule_work runnable init thread = + StarvationModels.get_run_method_from_runnable tenv runnable + |> Option.fold ~init ~f:(Domain.schedule_work loc thread) + in + match actuals with + | [HilExp.AccessExpression executor; HilExp.AccessExpression runnable] + when StarvationModels.schedules_work tenv callee -> + let thread_opt = + IList.force_until_first_some + [ (* match an executor call that we have a model for *) + lazy (StarvationModels.get_executor_thread_constraint tenv executor) + ; (* match an executor call where the executor is stored in a variable *) + lazy (Domain.AttributeDomain.get_executor_constraint executor astate.attributes) ] + in + Option.fold thread_opt ~init:astate ~f:(schedule_work runnable) + | _ -> + astate + + + let do_executor_effect tenv (ret_var, _) callee actuals astate = + let open Domain in + StarvationModels.get_executor_effect ~attrs_of_pname tenv callee actuals + |> Option.fold ~init:astate ~f:(fun acc effect -> + let attributes = + AttributeDomain.add ret_var (Attribute.Executor effect) astate.attributes + in + {acc with attributes} ) + + let exec_instr (astate : Domain.t) {ProcData.summary; tenv; extras} _ (instr : HilInstr.t) = let open ConcurrencyModels in let open StarvationModels in - let log_parse_error error pname actuals = - L.debug Analysis Verbose "%s pname:%a actuals:%a@." error Typ.Procname.pp pname - (PrettyPrintable.pp_collection ~pp_item:HilExp.pp) - actuals - in - let get_lock_path = function - | HilExp.AccessExpression access_exp -> ( - match HilExp.AccessExpression.to_access_path access_exp with - | (((Var.ProgramVar pvar, _) as base), _) as path - when FormalMap.is_formal base extras || Pvar.is_global pvar -> - Some (AccessPath.inner_class_normalize path) - | _ -> - (* ignore paths on local or logical variables *) - None ) - | HilExp.Constant (Const.Cclass class_id) -> - (* this is a synchronized/lock(CLASSNAME.class) construct *) - Some (lock_of_class class_id) - | _ -> - None - in + let get_lock_path = get_lock_path extras in let procname = Summary.get_proc_name summary in let is_java = Typ.Procname.is_java procname in let do_lock locks loc astate = @@ -70,52 +131,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Payload.read ~caller_summary:summary ~callee_pname:callee |> Option.fold ~init:astate ~f:(Domain.integrate_summary tenv callsite) in - let do_assume assume_exp (astate : Domain.t) = - let open Domain in - let add_choice (acc : Domain.t) bool_value = - let thread = if bool_value then ThreadDomain.UIThread else ThreadDomain.BGThread in - {acc with thread} - in - match HilExp.get_access_exprs assume_exp with - | [access_expr] when BranchGuardDomain.is_thread_guard access_expr astate.branch_guards -> - HilExp.eval_boolean_exp access_expr assume_exp |> Option.fold ~init:astate ~f:add_choice - | _ -> - astate - in - let do_thread_assert_effect ret_base callee (astate : Domain.t) = - let open Domain in - match ConcurrencyModels.get_thread_assert_effect callee with - | BackgroundThread -> - {astate with thread= ThreadDomain.BGThread} - | MainThread -> - {astate with thread= ThreadDomain.UIThread} - | MainThreadIfTrue -> - let ret_access_exp = HilExp.AccessExpression.base ret_base in - let branch_guards = - BranchGuardDomain.add ret_access_exp BranchGuard.Thread astate.branch_guards - in - {astate with branch_guards} - | 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 _ -> + | Assign _ | Call (_, Indirect _, _, _, _) -> astate - | Call (_, Direct callee, actuals, _, _) when should_skip_analysis tenv callee actuals -> + | Metadata (Sil.ExitScope (vars, _)) -> + {astate with attributes= Domain.AttributeDomain.exit_scope vars astate.attributes} + | Metadata _ -> astate | Assume (assume_exp, _, _, _) -> do_assume assume_exp astate + | Call (_, Direct callee, actuals, _, _) when should_skip_analysis tenv callee actuals -> + astate | Call (ret_base, Direct callee, actuals, _, loc) -> ( match get_lock_effect callee actuals with | Lock locks -> @@ -143,10 +169,12 @@ 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 + let astate = + do_thread_assert_effect ret_base callee astate + |> do_executor_effect tenv ret_base callee actuals + |> do_work_scheduling tenv callee actuals loc + in match may_block tenv callee actuals with | Some sev -> Domain.blocking_call ~callee sev ~loc astate diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 7e7178df3..985962445 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -442,29 +442,56 @@ module GuardToLockMap = struct let add_guard astate ~guard ~lock = add guard (FlatLock.v lock) astate end -module BranchGuard = struct - type t = Nothing | Thread +module Attribute = struct + type t = Nothing | Thread | Executor of StarvationModels.executor_thread_constraint + [@@deriving equal] let top = Nothing let is_top = function Nothing -> true | _ -> false - let pp fmt t = F.fprintf fmt (match t with Nothing -> "Nothing" | Thread -> "Thread") + let pp fmt t = + ( match t with + | Nothing -> + "Nothing" + | Thread -> + "Thread" + | Executor StarvationModels.ForUIThread -> + "Executor(UI)" + | Executor StarvationModels.ForNonUIThread -> + "Executor(BG)" ) + |> F.pp_print_string fmt - let leq ~lhs ~rhs = - match (lhs, rhs) with _, Nothing -> true | Nothing, _ -> false | Thread, Thread -> true + let join lhs rhs = if equal lhs rhs then lhs else Nothing - let join lhs rhs = match (lhs, rhs) with Thread, Thread -> lhs | _ -> Nothing + let leq ~lhs ~rhs = equal (join lhs rhs) rhs let widen ~prev ~next ~num_iters:_ = join prev next end -module BranchGuardDomain = struct - include AbstractDomain.InvertedMap (HilExp.AccessExpression) (BranchGuard) +module AttributeDomain = struct + include AbstractDomain.InvertedMap (Var) (Attribute) + + let is_thread_guard (acc_exp : HilExp.AccessExpression.t) t = + match acc_exp with + | Base (v, _) -> + find_opt v t |> Option.exists ~f:(function Attribute.Thread -> true | _ -> false) + | _ -> + false + + + let get_executor_constraint (acc_exp : HilExp.AccessExpression.t) t = + match acc_exp with + | Base (v, _) -> + find_opt v t |> Option.bind ~f:(function Attribute.Executor c -> Some c | _ -> None) + | _ -> + None + - let is_thread_guard acc_exp t = - find_opt acc_exp t |> Option.exists ~f:(function BranchGuard.Thread -> true | _ -> false) + let exit_scope vars t = + let pred key _value = not (List.exists vars ~f:(Var.equal key)) in + filter pred t end module ScheduledWorkItem = struct @@ -481,7 +508,7 @@ type t = { guard_map: GuardToLockMap.t ; lock_state: LockState.t ; critical_pairs: CriticalPairs.t - ; branch_guards: BranchGuardDomain.t + ; attributes: AttributeDomain.t ; thread: ThreadDomain.t ; scheduled_work: ScheduledWorkDomain.t } @@ -489,7 +516,7 @@ let bottom = { guard_map= GuardToLockMap.empty ; lock_state= LockState.top ; critical_pairs= CriticalPairs.empty - ; branch_guards= BranchGuardDomain.empty + ; attributes= AttributeDomain.empty ; thread= ThreadDomain.bottom ; scheduled_work= ScheduledWorkDomain.bottom } @@ -498,17 +525,17 @@ 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 + && AttributeDomain.is_top astate.attributes && ThreadDomain.is_bottom astate.thread && ScheduledWorkDomain.is_bottom astate.scheduled_work let pp fmt astate = F.fprintf fmt - "{guard_map= %a; lock_state= %a; critical_pairs= %a; branch_guards= %a; thread= %a; \ + "{guard_map= %a; lock_state= %a; critical_pairs= %a; attributes= %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 + astate.critical_pairs AttributeDomain.pp astate.attributes ThreadDomain.pp astate.thread ScheduledWorkDomain.pp astate.scheduled_work @@ -516,7 +543,7 @@ let join lhs rhs = { guard_map= GuardToLockMap.join lhs.guard_map rhs.guard_map ; 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 + ; attributes= AttributeDomain.join lhs.attributes rhs.attributes ; thread= ThreadDomain.join lhs.thread rhs.thread ; scheduled_work= ScheduledWorkDomain.join lhs.scheduled_work rhs.scheduled_work } @@ -527,7 +554,7 @@ let leq ~lhs ~rhs = GuardToLockMap.leq ~lhs:lhs.guard_map ~rhs:rhs.guard_map && LockState.leq ~lhs:lhs.lock_state ~rhs:rhs.lock_state && CriticalPairs.leq ~lhs:lhs.critical_pairs ~rhs:rhs.critical_pairs - && BranchGuardDomain.leq ~lhs:lhs.branch_guards ~rhs:rhs.branch_guards + && AttributeDomain.leq ~lhs:lhs.attributes ~rhs:rhs.attributes && ThreadDomain.leq ~lhs:lhs.thread ~rhs:rhs.thread && ScheduledWorkDomain.leq ~lhs:lhs.scheduled_work ~rhs:rhs.scheduled_work diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 3fe224412..2734afc6f 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -95,21 +95,24 @@ module CriticalPairs : AbstractDomain.FiniteSetS with type elt = CriticalPair.t module GuardToLockMap : AbstractDomain.WithTop -(** tracks whether an expression has been tested for whether we execute on UI thread *) -module BranchGuard : sig - type t = Nothing | Thread +(** Tracks whether a variable has been tested for whether we execute on UI thread, or + has been assigned an executor object. *) +module Attribute : sig + type t = Nothing | Thread | Executor of StarvationModels.executor_thread_constraint include AbstractDomain.WithTop with type t := t end -(** tracks all expressions currently known to have been tested for conditions in [BranchGuard] *) -module BranchGuardDomain : sig - include - AbstractDomain.InvertedMapS - with type key = HilExp.AccessExpression.t - and type value = BranchGuard.t +(** Tracks all variables assigned values of [Attribute] *) +module AttributeDomain : sig + include AbstractDomain.InvertedMapS with type key = Var.t and type value = Attribute.t val is_thread_guard : HilExp.AccessExpression.t -> t -> bool + + val get_executor_constraint : + HilExp.AccessExpression.t -> t -> StarvationModels.executor_thread_constraint option + + val exit_scope : Var.t list -> t -> t end (** A record of scheduled parallel work: the method scheduled to run, where, and on what thread. *) @@ -125,7 +128,7 @@ type t = { guard_map: GuardToLockMap.t ; lock_state: LockState.t ; critical_pairs: CriticalPairs.t - ; branch_guards: BranchGuardDomain.t + ; attributes: AttributeDomain.t ; thread: ThreadDomain.t ; scheduled_work: ScheduledWorkDomain.t } diff --git a/infer/tests/codetoanalyze/java/starvation/ExecutorRunnable.java b/infer/tests/codetoanalyze/java/starvation/ExecutorRunnable.java index 4b848e2a1..cf49e4008 100644 --- a/infer/tests/codetoanalyze/java/starvation/ExecutorRunnable.java +++ b/infer/tests/codetoanalyze/java/starvation/ExecutorRunnable.java @@ -96,4 +96,58 @@ class ExecutorRunnable { } }); } + + public void postDeadlockIndirectBad() { + Executors.getForegroundExecutor() + .execute( + new Runnable() { + @Override + public void run() { + lockAB(); + } + }); + + Executors.getBackgroundExecutor() + .execute( + new Runnable() { + @Override + public void run() { + lockBA(); + } + }); + } + + public void postOnUIThreadIndirectOk() { + Executors.getForegroundExecutor() + .execute( + new Runnable() { + @Override + public void run() { + lockAB(); + } + }); + + Executors.getForegroundExecutor() + .execute( + new Runnable() { + @Override + public void run() { + lockBA(); + } + }); + } +} + +class Executors { + static Executor uiExecutor; + + static Executor getForegroundExecutor() { + return uiExecutor; + } + + static Executor bgExecutor; + + static Executor getBackgroundExecutor() { + return bgExecutor; + } }