From 346589f1fb5c45bfeb8e5db1fda83445c9528cff Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Tue, 17 Apr 2018 08:41:32 -0700 Subject: [PATCH] [starvation] track on-main-thread status in summaries Reviewed By: ddino Differential Revision: D7431140 fbshipit-source-id: d127820 --- infer/src/concurrency/starvation.ml | 17 ++++++++---- infer/src/concurrency/starvationDomain.ml | 32 ++++++++++++++-------- infer/src/concurrency/starvationDomain.mli | 4 ++- 3 files changed, 35 insertions(+), 18 deletions(-) diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 6a58b0c44..06658ad1d 100644 --- a/infer/src/concurrency/starvation.ml +++ b/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 diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 093034375..80aa60601 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/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 diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index ff67175b1..422f3b606 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/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