From 2bbe7ff9f2f9468fbcd25a258c6ab3cfd6bbd1ad Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Wed, 16 Oct 2019 04:24:34 -0700 Subject: [PATCH] [starvation] simplify domains after removal of ui trace Summary: As per title Reviewed By: mityal Differential Revision: D17928088 fbshipit-source-id: 623463dfe --- infer/src/concurrency/ConcurrencyModels.ml | 6 ++ infer/src/concurrency/ConcurrencyModels.mli | 19 +----- infer/src/concurrency/RacerD.ml | 1 + infer/src/concurrency/RacerDModels.ml | 7 --- infer/src/concurrency/RacerDModels.mli | 4 -- infer/src/concurrency/StarvationModels.ml | 15 ----- infer/src/concurrency/StarvationModels.mli | 12 ---- infer/src/concurrency/starvation.ml | 8 +-- infer/src/concurrency/starvationDomain.ml | 70 ++------------------- infer/src/concurrency/starvationDomain.mli | 12 +--- 10 files changed, 20 insertions(+), 134 deletions(-) diff --git a/infer/src/concurrency/ConcurrencyModels.ml b/infer/src/concurrency/ConcurrencyModels.ml index 26994ec14..021b208b0 100644 --- a/infer/src/concurrency/ConcurrencyModels.ml +++ b/infer/src/concurrency/ConcurrencyModels.ml @@ -390,6 +390,12 @@ let annotated_as_uithread_equivalent ~attrs_of_pname tenv pname = 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 ) + + let cpp_lock_types_matcher = Clang.lock_types_matcher let is_recursive_lock_type = function diff --git a/infer/src/concurrency/ConcurrencyModels.mli b/infer/src/concurrency/ConcurrencyModels.mli index ac3c91e0b..8b02fafa9 100644 --- a/infer/src/concurrency/ConcurrencyModels.mli +++ b/infer/src/concurrency/ConcurrencyModels.mli @@ -32,9 +32,6 @@ val get_lock_effect : Typ.Procname.t -> HilExp.t list -> lock_effect val get_thread : Typ.Procname.t -> thread (** describe how this procedure behaves with respect to thread access *) -val is_modeled_ui_method : Tenv.t -> Typ.Procname.t -> bool -(** is it a modeled UI thread method? *) - val get_current_class_and_annotated_superclasses : (Annot.Item.t -> bool) -> Tenv.t -> Typ.Procname.t -> (Typ.name * Typ.name list) option @@ -57,16 +54,6 @@ 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:(BuiltinDecl.t -> ProcAttributes.t option) - -> Tenv.t - -> Typ.Procname.t - -> annotation_trail option -(** check if a method is transitively annotated @WorkerThread *) - -val annotated_as_uithread_equivalent : - attrs_of_pname:(BuiltinDecl.t -> ProcAttributes.t option) - -> Tenv.t - -> Typ.Procname.t - -> annotation_trail option -(** check if a method is transitively annotated @UIThread or equivalent *) +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/RacerD.ml b/infer/src/concurrency/RacerD.ml index f1b643304..fcc082a5e 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -502,6 +502,7 @@ let analyze_procedure {Callbacks.exe_env; summary} = let proc_name = Summary.get_proc_name summary in let tenv = Exe_env.get_tenv exe_env proc_name in let open RacerDModels in + let open ConcurrencyModels in let method_annotation = (Procdesc.get_attributes proc_desc).method_annotation in let is_initializer tenv proc_name = Typ.Procname.is_constructor proc_name || FbThreadSafety.is_custom_init tenv proc_name diff --git a/infer/src/concurrency/RacerDModels.ml b/infer/src/concurrency/RacerDModels.ml index 0d17c956c..f1669aee7 100644 --- a/infer/src/concurrency/RacerDModels.ml +++ b/infer/src/concurrency/RacerDModels.ml @@ -462,10 +462,3 @@ let is_synchronized_container callee_pname (access_exp : HilExp.AccessExpression false ) | _ -> false - - -let runs_on_ui_thread ~attrs_of_pname tenv pname = - let open ConcurrencyModels in - 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 ) diff --git a/infer/src/concurrency/RacerDModels.mli b/infer/src/concurrency/RacerDModels.mli index 2aef5ff12..678657dfb 100644 --- a/infer/src/concurrency/RacerDModels.mli +++ b/infer/src/concurrency/RacerDModels.mli @@ -52,7 +52,3 @@ val should_flag_interface_call : Tenv.t -> HilExp.t list -> CallFlags.t -> Typ.P val is_synchronized_container : Typ.Procname.t -> HilExp.AccessExpression.t -> Tenv.t -> bool (** is a call on an access expression to a method of a synchronized container? *) - -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/StarvationModels.ml b/infer/src/concurrency/StarvationModels.ml index 3e2f8cf69..5b3aac204 100644 --- a/infer/src/concurrency/StarvationModels.ml +++ b/infer/src/concurrency/StarvationModels.ml @@ -190,18 +190,3 @@ let strict_mode_matcher = let is_strict_mode_violation tenv pn actuals = Config.starvation_strict_mode && strict_mode_matcher tenv pn actuals - - -type uithread_explanation = - | IsModeled of {proc_name: Typ.Procname.t} - | CallsModeled of {proc_name: Typ.Procname.t; callee: Typ.Procname.t} - | Annotated of {proc_name: Typ.Procname.t; trail: ConcurrencyModels.annotation_trail} -[@@deriving compare] - -let get_uithread_explanation ~attrs_of_pname tenv proc_name = - let open ConcurrencyModels in - if annotated_as_worker_thread ~attrs_of_pname tenv proc_name |> Option.is_some then None - else if is_modeled_ui_method tenv proc_name then Some (IsModeled {proc_name}) - else - annotated_as_uithread_equivalent ~attrs_of_pname tenv proc_name - |> Option.map ~f:(fun trail -> Annotated {proc_name; trail}) diff --git a/infer/src/concurrency/StarvationModels.mli b/infer/src/concurrency/StarvationModels.mli index 76d216f91..2637e6a32 100644 --- a/infer/src/concurrency/StarvationModels.mli +++ b/infer/src/concurrency/StarvationModels.mli @@ -23,15 +23,3 @@ val is_synchronized_library_call : Tenv.t -> Typ.Procname.t -> bool val should_skip_analysis : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool (** should we treat a method call as skip (eg library methods in guava) to avoid FPs? *) - -type uithread_explanation = - | IsModeled of {proc_name: Typ.Procname.t} - | CallsModeled of {proc_name: Typ.Procname.t; callee: Typ.Procname.t} - | Annotated of {proc_name: Typ.Procname.t; trail: ConcurrencyModels.annotation_trail} -[@@deriving compare] - -val get_uithread_explanation : - attrs_of_pname:(Typ.Procname.t -> ProcAttributes.t option) - -> Tenv.t - -> Typ.Procname.t - -> uithread_explanation option diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index afc6d7a2e..d8dd8557a 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -119,8 +119,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let locks = List.hd actuals |> Option.to_list in do_lock locks loc astate |> do_unlock locks | NoEffect when is_java && is_ui_thread_model callee -> - Domain.set_on_ui_thread astate ~loc - (Domain.UIThreadElement.CallsModeled {proc_name= procname; callee}) + Domain.set_on_ui_thread astate () | NoEffect when is_java && is_strict_mode_violation tenv callee actuals -> Domain.strict_mode_call ~callee ~loc astate | NoEffect when is_java -> ( @@ -163,8 +162,9 @@ let analyze_procedure {Callbacks.exe_env; summary} = StarvationDomain.acquire tenv StarvationDomain.bottom ~procname ~loc (Option.to_list lock) in let initial = - StarvationModels.get_uithread_explanation ~attrs_of_pname tenv procname - |> Option.value_map ~default:initial ~f:(StarvationDomain.set_on_ui_thread initial ~loc) + if ConcurrencyModels.runs_on_ui_thread ~attrs_of_pname tenv procname then + StarvationDomain.set_on_ui_thread initial () + else initial in let filter_blocks = if is_nonblocking tenv proc_desc then StarvationDomain.filter_blocking_calls else Fn.id diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index b8f93ca39..6b545210e 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -358,65 +358,7 @@ module CriticalPairs = struct astate empty end -module UIThreadElement = struct - type t = StarvationModels.uithread_explanation = - | IsModeled of {proc_name: Typ.Procname.t} - | CallsModeled of {proc_name: Typ.Procname.t; callee: Typ.Procname.t} - | Annotated of {proc_name: Typ.Procname.t; trail: ConcurrencyModels.annotation_trail} - [@@deriving compare] - - let mono_pname = MF.wrap_monospaced Typ.Procname.pp - - let describe fmt = function - | IsModeled {proc_name} -> - F.fprintf fmt "%a is a standard UI-thread method" mono_pname proc_name - | CallsModeled {proc_name= _; callee} -> - F.fprintf fmt "it calls %a" pname_pp callee - | Annotated {proc_name; trail= DirectlyAnnotated} -> - F.fprintf fmt "%a is annotated %a" mono_pname proc_name MF.pp_monospaced - Annotations.ui_thread - | Annotated {proc_name; trail= Override override_pname} -> - F.fprintf fmt "class %a overrides %a, which is annotated %a" mono_pname proc_name - mono_pname override_pname MF.pp_monospaced Annotations.ui_thread - | Annotated {proc_name; trail= SuperClass class_name} -> ( - match Typ.Procname.get_class_type_name proc_name with - | None -> - L.die InternalError "Cannot get class of method %a@." Typ.Procname.pp proc_name - | Some current_class -> - let pp_extends fmt current_class = - if Typ.Name.equal current_class class_name then () - else F.fprintf fmt " extends %a, which" (MF.wrap_monospaced Typ.Name.pp) class_name - in - F.fprintf fmt "class %s%a is annotated %a" - (MF.monospaced_to_string (Typ.Name.name current_class)) - pp_extends current_class MF.pp_monospaced Annotations.ui_thread ) - - - let pp = describe -end - -module UIThreadExplanationDomain = struct - include ExplicitTrace.MakeTraceElem (UIThreadElement) (ExplicitTrace.DefaultCallPrinter) - - let join lhs rhs = if List.length lhs.trace <= List.length rhs.trace then lhs else rhs - - let widen ~prev ~next ~num_iters:_ = join prev next - - let ( <= ) ~lhs:_ ~rhs:_ = true -end - -module UIThreadDomain = struct - include AbstractDomain.BottomLifted (UIThreadExplanationDomain) - - let with_callsite astate callsite = - match astate with - | AbstractDomain.Types.Bottom -> - astate - | AbstractDomain.Types.NonBottom ui_explain -> - AbstractDomain.Types.NonBottom - (UIThreadExplanationDomain.with_callsite ui_explain callsite) -end - +module UIThreadDomain = AbstractDomain.BooleanOr module FlatLock = AbstractDomain.Flat (Lock) module GuardToLockMap = struct @@ -513,17 +455,13 @@ let integrate_summary tenv ~caller_summary:({lock_state; critical_pairs; ui} as let critical_pairs' = CriticalPairs.with_callsite callee_summary.critical_pairs (Some tenv) lock_state callsite in - let callee_ui = UIThreadDomain.with_callsite callee_summary.ui callsite in { astate with critical_pairs= CriticalPairs.join critical_pairs critical_pairs' - ; ui= UIThreadDomain.join ui callee_ui } + ; ui= UIThreadDomain.join ui callee_summary.ui } -let set_on_ui_thread ({ui} as astate) ~loc explain = - let ui = - UIThreadDomain.join ui - (AbstractDomain.Types.NonBottom (UIThreadExplanationDomain.make explain loc)) - in +let set_on_ui_thread ({ui} as astate) () = + let ui = UIThreadDomain.join ui true in {astate with ui} diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 3d43f2f1f..92792f9d2 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -71,13 +71,6 @@ end module CriticalPairs : AbstractDomain.FiniteSetS with type elt = CriticalPair.t -module UIThreadElement : sig - type t = StarvationModels.uithread_explanation = - | IsModeled of {proc_name: Typ.Procname.t} - | CallsModeled of {proc_name: Typ.Procname.t; callee: Typ.Procname.t} - | Annotated of {proc_name: Typ.Procname.t; trail: ConcurrencyModels.annotation_trail} -end - module UIThreadDomain : AbstractDomain.WithBottom module GuardToLockMap : AbstractDomain.WithTop @@ -100,9 +93,8 @@ 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 -> loc:Location.t -> UIThreadElement.t -> t -(** set the property "runs on UI thread" to true by attaching the given explanation as to - why this method is thought to do so *) +val set_on_ui_thread : t -> unit -> t +(** set the property "runs on UI thread" to true *) val add_guard : acquire_now:bool