diff --git a/infer/src/concurrency/ConcurrencyModels.ml b/infer/src/concurrency/ConcurrencyModels.ml index 92f71c3de..eba9782d6 100644 --- a/infer/src/concurrency/ConcurrencyModels.ml +++ b/infer/src/concurrency/ConcurrencyModels.ml @@ -384,19 +384,20 @@ let find_override_or_superclass_annotated ~attrs_of_pname is_annot tenv proc_nam else Typ.Procname.get_class_type_name proc_name |> Option.bind ~f:find_override_or_superclass_aux +let annotated_as ~attrs_of_pname predicate tenv pname = + find_override_or_superclass_annotated ~attrs_of_pname predicate tenv pname |> Option.is_some + + let annotated_as_worker_thread ~attrs_of_pname tenv pname = - find_override_or_superclass_annotated ~attrs_of_pname Annotations.ia_is_worker_thread tenv pname + annotated_as ~attrs_of_pname Annotations.ia_is_worker_thread tenv pname let annotated_as_uithread_equivalent ~attrs_of_pname tenv pname = - find_override_or_superclass_annotated ~attrs_of_pname Annotations.ia_is_uithread_equivalent tenv - pname + annotated_as ~attrs_of_pname Annotations.ia_is_uithread_equivalent tenv pname let runs_on_ui_thread ~attrs_of_pname tenv pname = - annotated_as_worker_thread ~attrs_of_pname tenv pname |> Option.is_none - && ( is_modeled_ui_method tenv pname - || annotated_as_uithread_equivalent ~attrs_of_pname tenv pname |> Option.is_some ) + is_modeled_ui_method tenv pname || annotated_as_uithread_equivalent ~attrs_of_pname tenv pname let cpp_lock_types_matcher = Clang.lock_types_matcher diff --git a/infer/src/concurrency/ConcurrencyModels.mli b/infer/src/concurrency/ConcurrencyModels.mli index da8c96cbf..d912a2937 100644 --- a/infer/src/concurrency/ConcurrencyModels.mli +++ b/infer/src/concurrency/ConcurrencyModels.mli @@ -55,6 +55,9 @@ val find_override_or_superclass_annotated : -> annotation_trail option (** check if a method's transitive annotations satisfy the given predicate *) +val annotated_as_worker_thread : + attrs_of_pname:(Typ.Procname.t -> ProcAttributes.t option) -> Tenv.t -> Typ.Procname.t -> bool + val runs_on_ui_thread : attrs_of_pname:(Typ.Procname.t -> ProcAttributes.t option) -> Tenv.t -> Typ.Procname.t -> bool (** is method not transitively annotated @WorkerThread and is modeled or annotated @UIThread or equivalent? *) diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 3fdfc0ac6..0c996aaf9 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -73,7 +73,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct 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.AnyThread in + let thread = if bool_value then ThreadDomain.UIThread else ThreadDomain.BGThread in {acc with thread} in match HilExp.get_access_exprs assume_exp with @@ -86,7 +86,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let open Domain in match ConcurrencyModels.get_thread_assert_effect callee with | BackgroundThread -> - {astate with thread= ThreadDomain.AnyThread} + {astate with thread= ThreadDomain.BGThread} | MainThread -> {astate with thread= ThreadDomain.UIThread} | MainThreadIfTrue -> @@ -158,9 +158,8 @@ let analyze_procedure {Callbacks.exe_env; summary} = let formals = FormalMap.make proc_desc in let proc_data = ProcData.make summary tenv formals in let loc = Procdesc.get_loc proc_desc in - let initial = - if not (Procdesc.is_java_synchronized proc_desc) then Domain.bottom - else + let set_lock_state_for_synchronized_proc astate = + if Procdesc.is_java_synchronized proc_desc then let lock = match procname with | Typ.Procname.Java java_pname when Typ.Procname.Java.is_static java_pname -> @@ -170,18 +169,27 @@ let analyze_procedure {Callbacks.exe_env; summary} = | _ -> FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> (base, [])) in - Domain.acquire tenv Domain.bottom ~procname ~loc (Option.to_list lock) + Domain.acquire tenv astate ~procname ~loc (Option.to_list lock) + else astate in - let initial = - if ConcurrencyModels.runs_on_ui_thread ~attrs_of_pname tenv procname then - Domain.set_on_ui_thread initial - else initial + let set_thread_status_by_annotation (astate : Domain.t) = + let thread = + if ConcurrencyModels.annotated_as_worker_thread ~attrs_of_pname tenv procname then + Domain.ThreadDomain.BGThread + else if ConcurrencyModels.runs_on_ui_thread ~attrs_of_pname tenv procname then + Domain.ThreadDomain.UIThread + else astate.thread + in + {astate with thread} in let filter_blocks = if StarvationModels.is_annotated_nonblocking ~attrs_of_pname tenv procname then Domain.filter_blocking_calls else Fn.id in + let initial = + Domain.bottom |> set_lock_state_for_synchronized_proc |> set_thread_status_by_annotation + in Analyzer.compute_post proc_data ~initial |> Option.map ~f:filter_blocks |> Option.map ~f:Domain.summary_of_astate diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 09876c104..1b87dcd59 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -12,22 +12,38 @@ module MF = MarkupFormatter let pname_pp = MF.wrap_monospaced Typ.Procname.pp module ThreadDomain = struct - type t = UIThread | AnyThread [@@deriving compare] + type t = UnknownThread | UIThread | BGThread | AnyThread [@@deriving compare, equal] - let top = AnyThread + let bottom = UnknownThread - let is_top = function AnyThread -> true | UIThread -> false + let is_bottom = function UnknownThread -> true | _ -> false - let join st1 st2 = - match (st1, st2) with AnyThread, _ | _, AnyThread -> AnyThread | _, _ -> UIThread + let join lhs rhs = + match (lhs, rhs) with + | UnknownThread, other | other, UnknownThread -> + other + | UIThread, UIThread | BGThread, BGThread -> + lhs + | _, _ -> + AnyThread - let leq ~lhs ~rhs = match (lhs, rhs) with AnyThread, UIThread -> false | _, _ -> true + (* type is just an int, so use [join] to define [leq] *) + let leq ~lhs ~rhs = equal (join lhs rhs) rhs let widen ~prev ~next ~num_iters:_ = join prev next let pp fmt st = - (match st with UIThread -> "UIThread" | AnyThread -> "AnyThread") |> F.pp_print_string fmt + ( match st with + | UnknownThread -> + "UnknownThread" + | UIThread -> + "UIThread" + | BGThread -> + "BGThread" + | AnyThread -> + "AnyThread" ) + |> F.pp_print_string fmt (** Can two thread statuses occur in parallel? Only [UIThread, UIThread] is forbidden. @@ -39,9 +55,30 @@ module ThreadDomain = struct let is_uithread = function UIThread -> true | _ -> false - (* If we know that either the caller or the callee is on UIThread, keep it that way. *) - let integrate_summary ~caller ~callee = - match (caller, callee) with UIThread, _ | _, UIThread -> UIThread | _, _ -> AnyThread + (* If we know that either the caller is a UI/BG thread or both, keep it that way. + Otherwise, we have no info on caller, so use callee's info. *) + let integrate_summary ~caller ~callee = if is_bottom caller then callee else caller + + (** given the current thread state [caller_thread] and the thread state under which a critical pair + occurred, [pair_thread], decide whether to throw away the pair (returning [None]) because it + cannot occur within a call from the current state, or adapt its thread state appropriately. *) + let apply_to_pair caller_thread pair_thread = + match (caller_thread, pair_thread) with + | UnknownThread, _ -> + (* callee pair knows more than us *) + Some pair_thread + | AnyThread, UnknownThread -> + (* callee pair knows nothing and caller has abstracted away info *) + Some AnyThread + | AnyThread, _ -> + (* callee pair is UI / BG / Any and caller has abstracted away info so use callee's knowledge *) + Some pair_thread + | UIThread, BGThread | BGThread, UIThread -> + (* annotations or assertions are incorrectly used in code, just drop the callee pair *) + None + | _, _ -> + (* caller is UI or BG and callee does not disagree, so use that *) + Some caller_thread end module Lock = struct @@ -285,14 +322,15 @@ module CriticalPair = struct ) - let with_callsite t existing_acquisitions call_site thread = - let f (elem : CriticalPairElement.t) = - { elem with - acquisitions= Acquisitions.union existing_acquisitions elem.acquisitions - ; thread= ThreadDomain.integrate_summary ~caller:thread ~callee:elem.thread } - in - let new_t = map ~f t in - with_callsite new_t call_site + let integrate_summary_opt existing_acquisitions call_site (caller_thread : ThreadDomain.t) + (callee_pair : t) = + ThreadDomain.apply_to_pair caller_thread callee_pair.elem.thread + |> Option.map ~f:(fun thread -> + let f (elem : CriticalPairElement.t) = + let acquisitions = Acquisitions.union existing_acquisitions elem.acquisitions in + ({elem with acquisitions; thread} : elem_t) + in + with_callsite (map ~f callee_pair) call_site ) let get_earliest_lock_or_call_loc ~procname ({elem= {acquisitions}} as t) = @@ -394,10 +432,8 @@ module CriticalPairs = struct (fun ({elem= {event}} as critical_pair : CriticalPair.t) acc -> if should_skip (Some tenv) event lock_state then acc else - let new_pair = - CriticalPair.with_callsite critical_pair existing_acquisitions call_site thread - in - add new_pair acc ) + CriticalPair.integrate_summary_opt existing_acquisitions call_site thread critical_pair + |> Option.fold ~init:acc ~f:(fun acc new_pair -> add new_pair acc) ) astate empty end @@ -448,14 +484,14 @@ let bottom = ; lock_state= LockState.top ; critical_pairs= CriticalPairs.empty ; branch_guards= BranchGuardDomain.empty - ; thread= ThreadDomain.top } + ; thread= ThreadDomain.bottom } let is_bottom {guard_map; lock_state; critical_pairs; branch_guards; thread} = GuardToLockMap.is_empty guard_map && LockState.is_top lock_state && CriticalPairs.is_empty critical_pairs && BranchGuardDomain.is_top branch_guards - && ThreadDomain.is_top thread + && ThreadDomain.is_bottom thread let pp fmt {guard_map; lock_state; critical_pairs; branch_guards; thread} = @@ -524,8 +560,6 @@ let release ({lock_state} as astate) locks = lock_state= List.fold locks ~init:lock_state ~f:(fun acc l -> LockState.release l acc) } -let set_on_ui_thread astate = {astate with thread= ThreadDomain.UIThread} - let add_guard ~acquire_now ~procname ~loc tenv astate guard lock = let astate = {astate with guard_map= GuardToLockMap.add_guard ~guard ~lock astate.guard_map} in if acquire_now then acquire tenv astate ~procname ~loc [lock] else astate diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 41ba937a1..7b80abc5a 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -9,19 +9,18 @@ open! IStd module F = Format (** Domain for thread-type. The main goals are - - Track code paths that are explicitly on UI thread (via annotations, or assertions). - - Maintain UI-thread-ness through the call stack (if a callee is on UI thread then the - trace any call site must be on the UI thread too). - - If we are not on the UI thread we assume we are on a background thread. + - Track code paths that are explicitly on UI/BG thread (via annotations, or assertions). + - Maintain UI/BG-thread-ness through the call stack (if a caller is of unknown status and + callee is on UI/BG thread then caller must be on the UI/BG thread too). - Traces with "UI-thread" status cannot interleave but all other combinations can. - - We do not track other annotations (eg WorkerThread or AnyThread) as they can be - erroneously applied -- other checkers should catch those errors (annotation reachability). - - Top is AnyThread, and is used as the initial state for analysis. + - Top is AnyThread, which means that there are executions on both UI and BG threads on + this method. + - Bottom is UnknownThread, and used as initial state. *) module ThreadDomain : sig - type t = UIThread | AnyThread + type t = UnknownThread | UIThread | BGThread | AnyThread - include AbstractDomain.WithTop with type t := t + include AbstractDomain.WithBottom with type t := t end (** Abstraction of a path that represents a lock, special-casing comparison @@ -132,9 +131,6 @@ val blocking_call : callee:Typ.Procname.t -> StarvationModels.severity -> loc:Lo val strict_mode_call : callee:Typ.Procname.t -> loc:Location.t -> t -> t -val set_on_ui_thread : t -> t -(** signal that the procedure is running on UI thread *) - val add_guard : acquire_now:bool -> procname:Typ.Procname.t diff --git a/infer/tests/codetoanalyze/java/starvation/Workers.java b/infer/tests/codetoanalyze/java/starvation/Workers.java index 7ecae8bdd..9a4fa5ae0 100644 --- a/infer/tests/codetoanalyze/java/starvation/Workers.java +++ b/infer/tests/codetoanalyze/java/starvation/Workers.java @@ -23,8 +23,10 @@ class Workers { } // WorkerThread does not propagate up the call stack + // We don't report here, however, since this is an annotation/assertion error, + // not starvation/deadlock. @UiThread - void uiThreadBad() throws RemoteException { + void FN_uiThreadBad() throws RemoteException { workerOk(); } diff --git a/infer/tests/codetoanalyze/java/starvation/issues.exp b/infer/tests/codetoanalyze/java/starvation/issues.exp index 35817cf4b..fc8ba1f81 100644 --- a/infer/tests/codetoanalyze/java/starvation/issues.exp +++ b/infer/tests/codetoanalyze/java/starvation/issues.exp @@ -83,4 +83,3 @@ codetoanalyze/java/starvation/ThreadSensitivity.java, ThreadSensitivity.confused codetoanalyze/java/starvation/ThreadSensitivity.java, ThreadSensitivity.confusedAssertBad(boolean,boolean):void, 83, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadSensitivity.confusedAssertBad(boolean,boolean)`, locks `this.monitorH` in `class ThreadSensitivity`, locks `this.monitorG` in `class ThreadSensitivity`,[Trace 2] `void ThreadSensitivity.confusedAssertBad(boolean,boolean)`, locks `this.monitorG` in `class ThreadSensitivity`, locks `this.monitorH` in `class ThreadSensitivity`] codetoanalyze/java/starvation/ThreadSleep.java, ThreadSleep.indirectSleepOnUIThreadBad():void, 24, STARVATION, no_bucket, ERROR, [[Trace 1] `void ThreadSleep.indirectSleepOnUIThreadBad()`, locks `this.lock` in `class ThreadSleep`,[Trace 2] `void ThreadSleep.lockAndSleepOnNonUIThread()`, locks `this.lock` in `class ThreadSleep`,Method call: `void ThreadSleep.sleepOnAnyThreadOk()`,calls `void Thread.sleep(long)`] codetoanalyze/java/starvation/ThreadSleep.java, ThreadSleep.sleepOnUIThreadBad():void, 17, STARVATION, no_bucket, ERROR, [`void ThreadSleep.sleepOnUIThreadBad()`,calls `void Thread.sleep(long)`] -codetoanalyze/java/starvation/Workers.java, Workers.uiThreadBad():void, 28, STARVATION, no_bucket, ERROR, [`void Workers.uiThreadBad()`,Method call: `void Workers.workerOk()`,Method call: `void Workers.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]