[starvation] make thread domain more precise

Summary:
Add precision to analysis by elaborating the thread-status domain. This is done by having unknown (bottom), UI, BG or Any (both/top) elements in the lattice.  This way, when we branch on thread-identity (if I am on UI thread do this, otherwise do that), we know that in one branch we are on UI thread and on the  other we are *not* on the UI thread (BG thread), where previously the other branch would just go to top.

With this knowledge we can throw away pairs that come from callees which run on a thread that is impossible, given the current caller thread identity.  This can happen when annotations are used incorrectly, and since this is the purview of annot-reachability, we just drop those pairs entirely.

Reviewed By: skcho

Differential Revision: D18202175

fbshipit-source-id: be604054e

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

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

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

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 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) =
-      { elem with
-        acquisitions= Acquisitions.union existing_acquisitions elem.acquisitions
-      ; thread= ThreadDomain.integrate_summary ~caller:thread ~callee:elem.thread }
+             let acquisitions = Acquisitions.union existing_acquisitions elem.acquisitions in
+             ({elem with acquisitions; thread} : elem_t)
            in
-    let new_t = map ~f t in
-    with_callsite new_t call_site
+           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

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

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

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)`]