From 84e9bea312fbbd84fe33d2c6dbad4c4ddd325ab2 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Mon, 12 Oct 2020 03:16:14 -0700 Subject: [PATCH] [starvation] improve handling of @NonBlocking annotation Summary: `NonBlocking` methods have starvation errors silenced (but not deadlock ones). This is implemented by summarising as usual and then filtering out such events when the summary is finalised, if the method is annotated as such. It's better to not record the events in the first place. Reviewed By: ezgicicek Differential Revision: D24237465 fbshipit-source-id: 1b24a26f0 --- infer/src/concurrency/starvation.ml | 9 ++++--- infer/src/concurrency/starvationDomain.ml | 31 +++++++++++++--------- infer/src/concurrency/starvationDomain.mli | 5 ++-- 3 files changed, 26 insertions(+), 19 deletions(-) diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 16453a181..1af657050 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -425,18 +425,19 @@ let analyze_procedure ({InterproceduralAnalysis.proc_desc; tenv} as interproc) = in {astate with thread} in - let filter_blocks = - if StarvationModels.is_annotated_nonblocking tenv procname then Domain.filter_blocking_calls - else Fn.id + let set_ignore_blocking_calls_flag astate = + if StarvationModels.is_annotated_nonblocking tenv procname then + Domain.set_ignore_blocking_calls_flag astate + else astate in let initial = Domain.initial (* set the attributes of instance variables set up by all constructors or the class initializer *) |> set_initial_attributes interproc |> set_lock_state_for_synchronized_proc |> set_thread_status_by_annotation + |> set_ignore_blocking_calls_flag in Analyzer.compute_post proc_data ~initial proc_desc - |> Option.map ~f:filter_blocks |> Option.map ~f:(Domain.summary_of_astate proc_desc) diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index dbe187d78..d61747704 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -421,8 +421,6 @@ module CriticalPair = struct let make ~loc acquisitions event thread = make {acquisitions; event; thread} loc - let is_blocking_call {elem= {event}} = match event with LockAcquire _ -> true | _ -> false - let may_deadlock tenv ~(lhs : t) ~lhs_lock ~(rhs : t) = let get_acquired_locks {elem= {event}} = match event with LockAcquire {locks} -> locks | _ -> [] @@ -645,9 +643,11 @@ module ScheduledWorkItem = struct end module ScheduledWorkDomain = AbstractDomain.FiniteSet (ScheduledWorkItem) +module IgnoreBlockingCalls = AbstractDomain.BooleanOr type t = - { guard_map: GuardToLockMap.t + { ignore_blocking_calls: IgnoreBlockingCalls.t + ; guard_map: GuardToLockMap.t ; lock_state: LockState.t ; critical_pairs: CriticalPairs.t ; attributes: AttributeDomain.t @@ -656,7 +656,8 @@ type t = ; var_state: VarDomain.t } let initial = - { guard_map= GuardToLockMap.empty + { ignore_blocking_calls= false + ; guard_map= GuardToLockMap.empty ; lock_state= LockState.top ; critical_pairs= CriticalPairs.empty ; attributes= AttributeDomain.empty @@ -675,7 +676,9 @@ let pp fmt astate = let join lhs rhs = - { guard_map= GuardToLockMap.join lhs.guard_map rhs.guard_map + { ignore_blocking_calls= + IgnoreBlockingCalls.join lhs.ignore_blocking_calls rhs.ignore_blocking_calls + ; guard_map= GuardToLockMap.join lhs.guard_map rhs.guard_map ; lock_state= LockState.join lhs.lock_state rhs.lock_state ; critical_pairs= CriticalPairs.join lhs.critical_pairs rhs.critical_pairs ; attributes= AttributeDomain.join lhs.attributes rhs.attributes @@ -687,7 +690,8 @@ let join lhs rhs = let widen ~prev ~next ~num_iters:_ = join prev next let leq ~lhs ~rhs = - GuardToLockMap.leq ~lhs:lhs.guard_map ~rhs:rhs.guard_map + IgnoreBlockingCalls.leq ~lhs:lhs.ignore_blocking_calls ~rhs:rhs.ignore_blocking_calls + && GuardToLockMap.leq ~lhs:lhs.guard_map ~rhs:rhs.guard_map && LockState.leq ~lhs:lhs.lock_state ~rhs:rhs.lock_state && CriticalPairs.leq ~lhs:lhs.critical_pairs ~rhs:rhs.critical_pairs && AttributeDomain.leq ~lhs:lhs.attributes ~rhs:rhs.attributes @@ -714,9 +718,11 @@ let acquire ?tenv ({lock_state; critical_pairs} as astate) ~procname ~loc locks let make_call_with_event new_event ~loc astate = - { astate with - critical_pairs= - add_critical_pair astate.lock_state new_event astate.thread ~loc astate.critical_pairs } + if astate.ignore_blocking_calls then astate + else + { astate with + critical_pairs= + add_critical_pair astate.lock_state new_event astate.thread ~loc astate.critical_pairs } let blocking_call ~callee sev ~loc astate = @@ -783,10 +789,6 @@ let lock_guard ~procname ~loc tenv astate guard = FlatLock.get lock_opt |> Option.to_list |> acquire ~tenv astate ~procname ~loc ) -let filter_blocking_calls ({critical_pairs} as astate) = - {astate with critical_pairs= CriticalPairs.filter CriticalPair.is_blocking_call critical_pairs} - - let schedule_work loc thread_constraint astate procname = let thread : ThreadDomain.t = match (thread_constraint : StarvationModels.scheduler_thread_constraint) with @@ -885,3 +887,6 @@ let remove_dead_vars (astate : t) deadvars = let var_state = VarDomain.exit_scope astate.var_state deadvars in let attributes = AttributeDomain.exit_scope deadvars astate.attributes in {astate with var_state; attributes} + + +let set_ignore_blocking_calls_flag astate = {astate with ignore_blocking_calls= true} diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index c75bdd9f9..99a9dc12f 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -164,7 +164,8 @@ end module ScheduledWorkDomain : AbstractDomain.FiniteSetS with type elt = ScheduledWorkItem.t type t = - { guard_map: GuardToLockMap.t + { ignore_blocking_calls: bool + ; guard_map: GuardToLockMap.t ; lock_state: LockState.t ; critical_pairs: CriticalPairs.t ; attributes: AttributeDomain.t @@ -239,6 +240,6 @@ val integrate_summary : val summary_of_astate : Procdesc.t -> t -> summary -val filter_blocking_calls : t -> t +val set_ignore_blocking_calls_flag : t -> t val remove_dead_vars : t -> Var.t list -> t