[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

@@ -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

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? *)

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

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 )

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? *)

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})

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

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

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}
 
 

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