From dd53d0af77385ee10ce73b0775ffbf4401c3a379 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Wed, 30 May 2018 10:39:46 -0700 Subject: [PATCH] [starvation] equalise summary and abstract state types Summary: In preparation for allowing unbalanced locking, we need the lock state in the summary. Reviewed By: mbouaziz Differential Revision: D8201932 fbshipit-source-id: 05a1b38 --- infer/src/concurrency/starvation.ml | 20 ++++++++++---------- infer/src/concurrency/starvationDomain.ml | 10 ++++------ infer/src/concurrency/starvationDomain.mli | 10 ++++++---- 3 files changed, 20 insertions(+), 20 deletions(-) diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 6fbe41a1e..7e39cd93c 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -131,9 +131,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} = |> Option.value_map ~default:initial ~f:(StarvationDomain.set_on_ui_thread initial) in Analyzer.compute_post proc_data ~initial - |> Option.value_map ~default:summary ~f:(fun lock_state -> - let lock_order = StarvationDomain.to_summary lock_state in - Payload.update_summary lock_order summary ) + |> Option.value_map ~default:summary ~f:(fun astate -> Payload.update_summary astate summary) let make_trace_with_header ?(header= "") elem pname = @@ -254,7 +252,7 @@ let should_report_deadlock_on_current_proc current_elem endpoint_elem = inner class but this is no longer obvious in the path, because of nested-class path normalisation. The net effect of the above issues is that we will only see these locks in conflicting pairs once, as opposed to twice with all other deadlock pairs. *) -let report_deadlocks tenv current_pdesc (summary, current_main) report_map' = +let report_deadlocks tenv current_pdesc {StarvationDomain.order; ui} report_map' = let open StarvationDomain in let current_pname = Procdesc.get_proc_name current_pdesc in let report_endpoint_elem current_elem endpoint_pname elem report_map = @@ -295,15 +293,17 @@ let report_deadlocks tenv current_pdesc (summary, current_main) report_map' = let endpoint_summaries = get_summaries_of_methods_in_class tenv endpoint_class in (* for each summary related to the endpoint, analyse and report on its pairs *) List.fold endpoint_summaries ~init:report_map ~f: - (fun acc (endp_pname, (endp_summary, endp_ui)) -> - if UIThreadDomain.is_empty current_main || UIThreadDomain.is_empty endp_ui then - OrderDomain.fold (report_endpoint_elem elem endp_pname) endp_summary acc + (fun acc (endp_pname, endpoint_summary) -> + let endp_order = endpoint_summary.order in + let endp_ui = endpoint_summary.ui in + if UIThreadDomain.is_empty ui || UIThreadDomain.is_empty endp_ui then + OrderDomain.fold (report_endpoint_elem elem endp_pname) endp_order acc else acc ) ) in - OrderDomain.fold report_on_current_elem summary report_map' + OrderDomain.fold report_on_current_elem order report_map' -let report_blocks_on_main_thread tenv current_pdesc (order, ui) report_map' = +let report_blocks_on_main_thread tenv current_pdesc {StarvationDomain.order; ui} report_map' = let open StarvationDomain in let current_pname = Procdesc.get_proc_name current_pdesc in let report_remote_block ui_explain current_elem current_lock endpoint_pname endpoint_elem @@ -346,7 +346,7 @@ let report_blocks_on_main_thread tenv current_pdesc (order, ui) report_map' = let endpoint_summaries = get_summaries_of_methods_in_class tenv endpoint_class in (* for each summary related to the endpoint, analyse and report on its pairs *) List.fold endpoint_summaries ~init:report_map ~f: - (fun acc (endpoint_pname, (order, ui)) -> + (fun acc (endpoint_pname, {order; ui}) -> (* skip methods known to run on ui thread, as they cannot run in parallel to us *) if UIThreadDomain.is_empty ui then OrderDomain.fold diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index d5907230a..a5ee90702 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -300,7 +300,8 @@ let release ({lock_state} as astate) lockid = let integrate_summary ({lock_state; order; ui} as astate) callee_pname loc callee_summary = - let callee_order, callee_ui = callee_summary in + let callee_order = callee_summary.order in + let callee_ui = callee_summary.ui 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 = @@ -317,9 +318,6 @@ let set_on_ui_thread ({ui} as astate) explain = {astate with ui= UIThreadDomain.join ui (AbstractDomain.Types.NonBottom explain)} -let to_summary {order; ui} = (order, ui) +type summary = astate -type summary = OrderDomain.astate * UIThreadDomain.astate - -let pp_summary fmt (order, ui) = - F.fprintf fmt "Order: %a, UIThread: %a" OrderDomain.pp order UIThreadDomain.pp ui +let pp_summary = pp diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index e9feaf9fa..6d5a803f1 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -59,10 +59,14 @@ module OrderDomain : sig include AbstractDomain.WithBottom with type astate = t end +module LockState : AbstractDomain.WithBottom + module UIThreadDomain : AbstractDomain.WithBottom with type astate = string AbstractDomain.Types.bottom_lifted -include AbstractDomain.WithBottom +type astate = {lock_state: LockState.astate; order: OrderDomain.astate; ui: UIThreadDomain.astate} + +include AbstractDomain.WithBottom with type astate := astate val acquire : astate -> Location.t -> Lock.t -> astate @@ -76,10 +80,8 @@ val set_on_ui_thread : astate -> string -> astate (** set the property "runs on UI thread" to true by attaching the given explanation string as to why this method is thought to do so *) -type summary = OrderDomain.astate * UIThreadDomain.astate +type summary = astate val pp_summary : F.formatter -> summary -> unit -val to_summary : astate -> summary - val integrate_summary : astate -> Typ.Procname.t -> Location.t -> summary -> astate