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