[starvation] track on-main-thread status in summaries

Reviewed By: ddino

Differential Revision: D7431140

fbshipit-source-id: d127820

infer/src/concurrency/starvation.ml

@@ -20,6 +20,10 @@ let is_java_static pname =
       false
 
 
+let is_on_main_thread pn =
+  RacerDConfig.(match Models.get_thread pn with Models.MainThread -> true | _ -> false)
+
+
 module Summary = Summary.Make (struct
   type payload = StarvationDomain.summary
 
@@ -77,9 +81,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | LockedIfTrue ->
           astate
       | NoEffect ->
-          Summary.read_summary pdesc callee_pname
-          |> Option.value_map ~default:astate ~f:(fun callee_summary ->
-                 Domain.integrate_summary ~caller_state:astate ~callee_summary callee_pname loc ) )
+          if is_on_main_thread callee_pname then Domain.set_on_main_thread astate
+          else
+            Summary.read_summary pdesc callee_pname
+            |> Option.value_map ~default:astate ~f:(fun callee_summary ->
+                   Domain.integrate_summary ~caller_state:astate ~callee_summary callee_pname loc
+               ) )
     | _ ->
         astate
 
@@ -140,7 +147,7 @@ let get_summary caller_pdesc callee_pdesc =
   |> Option.map ~f:(fun summary -> (callee_pdesc, summary))
 
 
-let report_deadlocks get_proc_desc tenv pdesc summary =
+let report_deadlocks get_proc_desc tenv pdesc (summary, _) =
   let open StarvationDomain in
   let process_callee_elem caller_pdesc caller_elem callee_pdesc elem =
     if LockOrder.may_deadlock caller_elem elem && should_report_if_same_class caller_elem then (
@@ -188,7 +195,7 @@ let report_deadlocks get_proc_desc tenv pdesc summary =
                     let proc_descs = List.rev_filter_map methods ~f:get_proc_desc in
                     let summaries = List.rev_filter_map proc_descs ~f:(get_summary pdesc) in
                     (* for each summary related to the endpoint, analyse and report on its pairs *)
-                    List.iter summaries ~f:(fun (callee_pdesc, summary) ->
+                    List.iter summaries ~f:(fun (callee_pdesc, (summary, _)) ->
                         LockOrderDomain.iter (process_callee_elem pdesc elem callee_pdesc) summary
                     ) ) )
   in

infer/src/concurrency/starvationDomain.ml

@@ -207,11 +207,14 @@ module LockState = struct
     fold ff map init
 end
 
-include AbstractDomain.Pair (LockState) (LockOrderDomain)
+module MainThreadDomain = AbstractDomain.BooleanOr
+include AbstractDomain.Pair (AbstractDomain.Pair (LockState) (LockOrderDomain)) (MainThreadDomain)
 
-let empty = (LockState.empty, LockOrderDomain.empty)
+let empty = ((LockState.empty, LockOrderDomain.empty), false)
+
+let is_empty ((ls, lo), main) =
+  LockState.is_empty ls && LockOrderDomain.is_empty lo && MainThreadDomain.is_empty main
 
-let is_empty (ls, lo) = LockState.is_empty ls && LockOrderDomain.is_empty lo
 
 (* for every lock b held locally, add a pair (b, lock_event), plus (None, lock_event) *)
 let add_order_pairs ls lock_event acc =
@@ -233,16 +236,17 @@ let add_order_pairs ls lock_event acc =
     LockState.fold_over_events add_first_and_eventually ls acc |> add_eventually
 
 
-let acquire lockid (ls, lo) loc =
+let acquire lockid ((ls, lo), main) loc =
   let newlock_event = LockEvent.make_acquire lockid loc in
   let lo' = add_order_pairs ls newlock_event lo in
   let ls' = LockState.acquire lockid newlock_event ls in
-  (ls', lo')
+  ((ls', lo'), main)
 
 
-let release lockid (ls, lo) = (LockState.release lockid ls, lo)
+let release lockid ((ls, lo), main) = ((LockState.release lockid ls, lo), main)
 
-let integrate_summary ~caller_state:(ls, lo) ~callee_summary callee_pname loc =
+let integrate_summary ~caller_state:((ls, lo), main) ~callee_summary callee_pname loc =
+  let callee_lo, callee_main = callee_summary in
   (* for each pair (b,a) in the callee, add (l,b) and (l,a) to the current state, where
      l is held locally *)
   let do_elem elem acc =
@@ -251,13 +255,17 @@ let integrate_summary ~caller_state:(ls, lo) ~callee_summary callee_pname loc =
   in
   let callsite = CallSite.make callee_pname loc in
   (* add callsite to the "eventually" trace *)
-  let elems = LockOrderDomain.with_callsite callsite callee_summary in
+  let elems = LockOrderDomain.with_callsite callsite callee_lo in
   let lo' = LockOrderDomain.fold do_elem elems lo in
-  (ls, lo')
+  let main' = MainThreadDomain.join main callee_main in
+  ((ls, lo'), main')
+
 
+let set_on_main_thread (sum, _) = (sum, true)
 
-let to_summary astate = snd astate
+let to_summary ((_, lo), main) = (lo, main)
 
-type summary = LockOrderDomain.astate
+type summary = LockOrderDomain.astate * MainThreadDomain.astate
 
-let pp_summary = LockOrderDomain.pp
+let pp_summary fmt (lo, main) =
+  F.fprintf fmt "LockOrder: %a, MainThread: %a" LockOrderDomain.pp lo MainThreadDomain.pp main

infer/src/concurrency/starvationDomain.mli

@@ -60,7 +60,9 @@ val acquire : LockIdentity.t -> astate -> Location.t -> astate
 
 val release : LockIdentity.t -> astate -> astate
 
-type summary = LockOrderDomain.astate
+val set_on_main_thread : astate -> astate
+
+type summary = LockOrderDomain.astate * bool
 
 val pp_summary : F.formatter -> summary -> unit