diff --git a/infer/src/backend/StarvationGlobalAnalysis.ml b/infer/src/backend/StarvationGlobalAnalysis.ml index ae3ec3db5..8f71cd776 100644 --- a/infer/src/backend/StarvationGlobalAnalysis.ml +++ b/infer/src/backend/StarvationGlobalAnalysis.ml @@ -75,15 +75,16 @@ let report exe_env work_set = tenv pattrs pair acc in match pair.elem.event with - | LockAcquire lock -> - let should_report_starvation = - CriticalPair.is_uithread pair && not (Procname.is_constructor procname) - in - WorkHashSet.fold - (fun (other_procname, (other_pair : CriticalPair.t)) () acc -> - Starvation.report_on_parallel_composition ~should_report_starvation tenv pattrs - pair lock other_procname other_pair acc ) - work_set acc + | LockAcquire locks -> + List.fold locks ~init:acc ~f:(fun acc lock -> + let should_report_starvation = + CriticalPair.is_uithread pair && not (Procname.is_constructor procname) + in + WorkHashSet.fold + (fun (other_procname, (other_pair : CriticalPair.t)) () acc -> + Starvation.report_on_parallel_composition ~should_report_starvation tenv + pattrs pair lock other_procname other_pair acc ) + work_set acc ) | _ -> acc ) in diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 67852b358..365fb3fb9 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -605,12 +605,12 @@ let should_report_deadlock_on_current_proc current_elem endpoint_elem = (* should never happen *) L.die InternalError "Deadlock cannot occur without two lock events: %a" CriticalPair.pp current_elem - | LockAcquire endpoint_lock, LockAcquire current_lock -> ( + | LockAcquire endpoint_locks, LockAcquire current_locks -> ( (* first elem is a class object (see [lock_of_class]), so always report because the reverse ordering on the events will not occur since we don't search the class for static locks *) - Lock.is_class_object endpoint_lock + List.exists ~f:Lock.is_class_object endpoint_locks || - match Lock.compare_wrt_reporting endpoint_lock current_lock with + match List.compare Lock.compare_wrt_reporting endpoint_locks current_locks with | 0 -> Location.compare current_elem.CriticalPair.loc endpoint_elem.CriticalPair.loc < 0 | c -> @@ -692,17 +692,19 @@ let report_on_parallel_composition ~should_report_starvation tenv pattrs pair lo in let ltr, loc = make_trace_and_loc () in ReportMap.add_starvation High tenv pattrs loc ltr error_message report_map - | LockAcquire other_lock - when CriticalPair.may_deadlock tenv pair other_pair - && should_report_deadlock_on_current_proc pair other_pair -> - let error_message = - Format.asprintf - "Potential deadlock. %a (Trace 1) and %a (Trace 2) acquire locks %a and %a in reverse \ - orders." - pname_pp pname pname_pp other_pname Lock.describe lock Lock.describe other_lock - in - let ltr, loc = make_trace_and_loc () in - ReportMap.add_deadlock tenv pattrs loc ltr error_message report_map + | LockAcquire _ -> ( + match CriticalPair.may_deadlock tenv ~lhs:pair ~lhs_lock:lock ~rhs:other_pair with + | Some other_lock when should_report_deadlock_on_current_proc pair other_pair -> + let error_message = + Format.asprintf + "Potential deadlock. %a (Trace 1) and %a (Trace 2) acquire locks %a and %a in \ + reverse orders." + pname_pp pname pname_pp other_pname Lock.describe lock Lock.describe other_lock + in + let ltr, loc = make_trace_and_loc () in + ReportMap.add_deadlock tenv pattrs loc ltr error_message report_map + | _ -> + report_map ) | _ -> report_map else report_map @@ -751,26 +753,33 @@ let report_on_pair ~analyze_ondemand tenv pattrs (pair : Domain.CriticalPair.t) let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:pname pair in let ltr = CriticalPair.make_trace pname pair in ReportMap.add_lockless_violation tenv pattrs loc ltr error_message report_map - | LockAcquire lock when Acquisitions.lock_is_held lock pair.elem.acquisitions -> - let error_message = - Format.asprintf "Potential self deadlock. %a%a twice." pname_pp pname Lock.pp_locks lock - in - let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:pname pair in - let ltr = CriticalPair.make_trace ~header:"In method " pname pair in - ReportMap.add_deadlock tenv pattrs loc ltr error_message report_map - | LockAcquire lock when not Config.starvation_whole_program -> - Lock.root_class lock - |> Option.value_map ~default:report_map ~f:(fun other_class -> - (* get the class of the root variable of the lock in the lock acquisition - and retrieve all the summaries of the methods of that class; - then, report on the parallel composition of the current pair and any pair in these - summaries that can indeed run in parallel *) - fold_reportable_summaries analyze_ondemand tenv other_class ~init:report_map - ~f:(fun acc (other_pname, {critical_pairs}) -> - CriticalPairs.fold - (report_on_parallel_composition ~should_report_starvation tenv pattrs pair lock - other_pname) - critical_pairs acc ) ) + | LockAcquire locks -> ( + match + List.find locks ~f:(fun lock -> Acquisitions.lock_is_held lock pair.elem.acquisitions) + with + | Some lock -> + let error_message = + Format.asprintf "Potential self deadlock. %a%a twice." pname_pp pname Lock.pp_locks lock + in + let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:pname pair in + let ltr = CriticalPair.make_trace ~header:"In method " pname pair in + ReportMap.add_deadlock tenv pattrs loc ltr error_message report_map + | None when Config.starvation_whole_program -> + report_map + | None -> + List.fold locks ~init:report_map ~f:(fun acc lock -> + Lock.root_class lock + |> Option.value_map ~default:acc ~f:(fun other_class -> + (* get the class of the root variable of the lock in the lock acquisition + and retrieve all the summaries of the methods of that class; + then, report on the parallel composition of the current pair and any pair in these + summaries that can indeed run in parallel *) + fold_reportable_summaries analyze_ondemand tenv other_class ~init:acc + ~f:(fun acc (other_pname, {critical_pairs}) -> + CriticalPairs.fold + (report_on_parallel_composition ~should_report_starvation tenv pattrs pair + lock other_pname) + critical_pairs acc ) ) ) ) | _ -> report_map diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 487d65cc3..af53f651e 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -107,6 +107,24 @@ module Lock = struct let mk_str t = root_class t |> Option.value_map ~default:"" ~f:Typ.Name.to_string in (* use string comparison on types as a stable order to decide whether to report a deadlock *) String.compare (mk_str t1) (mk_str t2) + + + let apply_subst_to_list subst l = + let rec apply_subst_to_list_inner l = + match l with + | [] -> + ([], false) + | lock :: locks -> ( + let locks', modified = apply_subst_to_list_inner locks in + match apply_subst subst lock with + | None -> + (locks', true) + | Some lock' when (not modified) && phys_equal lock lock' -> + (l, false) + | Some lock' -> + (lock' :: locks', true) ) + in + apply_subst_to_list_inner l |> fst end module AccessExpressionDomain = struct @@ -159,15 +177,15 @@ end module Event = struct type t = - | LockAcquire of Lock.t + | LockAcquire of Lock.t list | MayBlock of (Procname.t * StarvationModels.severity) | StrictModeCall of Procname.t | MonitorWait of Lock.t [@@deriving compare] let pp fmt = function - | LockAcquire lock -> - F.fprintf fmt "LockAcquire(%a)" Lock.pp lock + | LockAcquire locks -> + F.fprintf fmt "LockAcquire(%a)" (PrettyPrintable.pp_collection ~pp_item:Lock.pp) locks | MayBlock (pname, sev) -> F.fprintf fmt "MayBlock(%a, %a)" Procname.pp pname StarvationModels.pp_severity sev | StrictModeCall pname -> @@ -178,8 +196,8 @@ module Event = struct let describe fmt elem = match elem with - | LockAcquire lock -> - Lock.pp_locks fmt lock + | LockAcquire locks -> + Pp.comma_seq Lock.pp_locks fmt locks | MayBlock (pname, _) | StrictModeCall pname -> F.fprintf fmt "calls %a" describe_pname pname | MonitorWait lock -> @@ -195,24 +213,20 @@ module Event = struct let make_object_wait lock = MonitorWait lock let apply_subst subst event = - let make_monitor_wait lock = MonitorWait lock in - let make_lock_acquire lock = LockAcquire lock in - let apply_subst_aux make lock = - match Lock.apply_subst subst lock with - | None -> - None - | Some lock' when phys_equal lock lock' -> - Some event - | Some lock' -> - Some (make lock') - in match event with - | MonitorWait lock -> - apply_subst_aux make_monitor_wait lock - | LockAcquire lock -> - apply_subst_aux make_lock_acquire lock | MayBlock _ | StrictModeCall _ -> Some event + | MonitorWait lock -> + Lock.apply_subst subst lock + |> Option.map ~f:(fun lock' -> if phys_equal lock lock' then event else MonitorWait lock') + | LockAcquire locks -> ( + match Lock.apply_subst_to_list subst locks with + | [] -> + None + | locks' when phys_equal locks locks' -> + Some event + | locks' -> + Some (LockAcquire locks') ) end (** A lock acquisition with source location and procname in which it occurs. The location & procname @@ -275,8 +289,6 @@ module LockState : sig val release : Lock.t -> t -> t - val is_lock_taken : Event.t -> t -> bool - val get_acquisitions : t -> Acquisitions.t end = struct (* abstraction limit for lock counts *) @@ -316,14 +328,6 @@ end = struct let is_top {map} = Map.is_top map - let is_lock_taken event {acquisitions} = - match event with - | Event.LockAcquire lock -> - Acquisitions.mem (Acquisition.make_dummy lock) acquisitions - | _ -> - false - - let acquire ~procname ~loc lock {map; acquisitions} = let should_add_acquisition = ref false in let map = @@ -399,9 +403,10 @@ let is_recursive_lock event tenv = (Typ.pp_full Pp.text) typ ; true in - match event with - | Event.LockAcquire lock_path -> - Lock.get_typ tenv lock_path |> Option.exists ~f:is_class_and_recursive_lock + match (event : Event.t) with + | LockAcquire locks -> + List.exists locks ~f:(fun lock_path -> + Lock.get_typ tenv lock_path |> Option.exists ~f:is_class_and_recursive_lock ) | _ -> false @@ -413,19 +418,19 @@ module CriticalPair = struct let is_blocking_call {elem= {event}} = match event with LockAcquire _ -> true | _ -> false - let get_final_acquire {elem= {event}} = - match event with LockAcquire lock -> Some lock | _ -> None - - - let may_deadlock tenv ({elem= pair1} as t1 : t) ({elem= pair2} as t2 : t) = - ThreadDomain.can_run_in_parallel pair1.thread pair2.thread - && Option.both (get_final_acquire t1) (get_final_acquire t2) - |> Option.exists ~f:(fun (lock1, lock2) -> - (not (Lock.equal_across_threads tenv lock1 lock2)) - && Acquisitions.lock_is_held_in_other_thread tenv lock2 pair1.acquisitions - && Acquisitions.lock_is_held_in_other_thread tenv lock1 pair2.acquisitions - && Acquisitions.no_locks_common_across_threads tenv pair1.acquisitions - pair2.acquisitions ) + let may_deadlock tenv ~(lhs : t) ~lhs_lock ~(rhs : t) = + let get_acquired_locks {elem= {event}} = + match event with LockAcquire locks -> locks | _ -> [] + in + if ThreadDomain.can_run_in_parallel lhs.elem.thread rhs.elem.thread then + get_acquired_locks rhs + |> List.find ~f:(fun rhs_lock -> + (not (Lock.equal_across_threads tenv lhs_lock rhs_lock)) + && Acquisitions.lock_is_held_in_other_thread tenv rhs_lock lhs.elem.acquisitions + && Acquisitions.lock_is_held_in_other_thread tenv lhs_lock rhs.elem.acquisitions + && Acquisitions.no_locks_common_across_threads tenv lhs.elem.acquisitions + rhs.elem.acquisitions ) + else None let apply_subst subst pair = @@ -436,26 +441,34 @@ module CriticalPair = struct Some (map ~f:(fun _elem -> elem') pair) + (** if given [Some tenv], transform a pair so as to remove reentrant locks that are already in + [held_locks] *) + let filter_out_reentrant_relocks tenv_opt held_locks pair = + match (tenv_opt, pair.elem.event) with + | Some tenv, LockAcquire locks -> ( + let filtered_locks = + IList.filter_changed locks ~f:(fun lock -> + (not (Acquisitions.lock_is_held lock held_locks)) + || not (is_recursive_lock pair.elem.event tenv) ) + in + match filtered_locks with + | [] -> + None + | _ when phys_equal filtered_locks locks -> + Some pair + | _ -> + Some (map pair ~f:(fun elem -> {elem with event= LockAcquire filtered_locks})) ) + | _, _ -> + Some pair + + let integrate_summary_opt ?subst ?tenv existing_acquisitions call_site (caller_thread : ThreadDomain.t) (callee_pair : t) = let substitute_pair subst callee_pair = match subst with None -> Some callee_pair | Some subst -> apply_subst subst callee_pair in - let filter_out_reentrant_relock callee_pair = - match tenv with - | None -> - Some callee_pair - | Some tenv - when get_final_acquire callee_pair - |> Option.for_all ~f:(fun lock -> - (not (Acquisitions.lock_is_held lock existing_acquisitions)) - || not (is_recursive_lock callee_pair.elem.event tenv) ) -> - Some callee_pair - | _ -> - None - in substitute_pair subst callee_pair - |> Option.bind ~f:filter_out_reentrant_relock + |> Option.bind ~f:(filter_out_reentrant_relocks tenv existing_acquisitions) |> Option.bind ~f:(fun callee_pair -> ThreadDomain.apply_to_pair caller_thread callee_pair.elem.thread |> Option.map ~f:(fun thread -> @@ -528,17 +541,6 @@ module CriticalPair = struct let can_run_in_parallel t1 t2 = ThreadDomain.can_run_in_parallel t1.elem.thread t2.elem.thread end -(** skip adding an order pair [(_, event)] if - - - we have no tenv, or, - - [event] is not a lock event, or, - - we do not hold the lock, or, - - the lock is not recursive. *) -let should_skip ?tenv event lock_state = - Option.exists tenv ~f:(fun tenv -> - LockState.is_lock_taken event lock_state && is_recursive_lock event tenv ) - - module CriticalPairs = struct include CriticalPair.FiniteSet @@ -548,9 +550,8 @@ module CriticalPairs = struct (fun critical_pair acc -> CriticalPair.integrate_summary_opt ?subst ?tenv existing_acquisitions call_site thread critical_pair - |> Option.fold ~init:acc ~f:(fun acc (new_pair : CriticalPair.t) -> - if should_skip ?tenv new_pair.elem.event lock_state then acc else add new_pair acc ) - ) + |> Option.bind ~f:(CriticalPair.filter_out_reentrant_relocks tenv existing_acquisitions) + |> Option.value_map ~default:acc ~f:(fun new_pair -> add new_pair acc) ) astate empty end @@ -691,19 +692,17 @@ let leq ~lhs ~rhs = let add_critical_pair ?tenv lock_state event thread ~loc acc = - if should_skip ?tenv event lock_state then acc - else - let acquisitions = LockState.get_acquisitions lock_state in - let critical_pair = CriticalPair.make ~loc acquisitions event thread in - CriticalPairs.add critical_pair acc + let acquisitions = LockState.get_acquisitions lock_state in + let critical_pair = CriticalPair.make ~loc acquisitions event thread in + CriticalPair.filter_out_reentrant_relocks tenv acquisitions critical_pair + |> Option.value_map ~default:acc ~f:(fun pair -> CriticalPairs.add pair acc) let acquire ?tenv ({lock_state; critical_pairs} as astate) ~procname ~loc locks = { astate with critical_pairs= - List.fold locks ~init:critical_pairs ~f:(fun acc lock -> - let event = Event.make_acquire lock in - add_critical_pair ?tenv lock_state event astate.thread ~loc acc ) + (let event = Event.make_acquire locks in + add_critical_pair ?tenv lock_state event astate.thread ~loc critical_pairs ) ; lock_state= List.fold locks ~init:lock_state ~f:(fun acc lock -> LockState.acquire ~procname ~loc lock acc ) } diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index c5807945f..3682f22cd 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -57,7 +57,7 @@ end module Event : sig type t = - | LockAcquire of Lock.t + | LockAcquire of Lock.t list | MayBlock of (Procname.t * StarvationModels.severity) | StrictModeCall of Procname.t | MonitorWait of Lock.t @@ -107,8 +107,10 @@ module CriticalPair : sig val get_earliest_lock_or_call_loc : procname:Procname.t -> t -> Location.t (** outermost callsite location OR lock acquisition *) - val may_deadlock : Tenv.t -> t -> t -> bool - (** two pairs can run in parallel and satisfy the conditions for deadlock *) + val may_deadlock : Tenv.t -> lhs:t -> lhs_lock:Lock.t -> rhs:t -> Lock.t option + (** if two pairs can run in parallel and satisfy the conditions for deadlock, when [lhs_lock] of + [lhs] is involved return the lock involved from [rhs], as [LockAcquire] may involve more than + one *) val make_trace : ?header:string -> ?include_acquisitions:bool -> Procname.t -> t -> Errlog.loc_trace