pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[starvation] change domain to use critical pairs `(set of locks held, event)`

Browse Source 
Summary:
The old domain keeps two sets:
- `events` are things (including lock acquisitions) which eventually happen during the execution of a procedure.
- `order` are pairs of `(lock, event)` such that there is a trace through the procedure which at some point acquires `lock` and before releasing it performs `event`.

A deadlock would be reported if for two procedures, `(lock1,lock2)` is in `order` of procedure 1 and `(lock2,lock1)` is in `order` of procedure 2.  This condition/domain allowed for the false positive fixed in the tests, as well as was unwieldy, because it required translating between the two sets.

The new domain has only one set of "critical pairs" `(locks, event)` such that there is a trace where `event` occurs, and *right before it occurs* the locks held are exactly `locks` (no over/under approximation).  This allows keeping all information in one set, simplifies the procedure call handling and eliminates the known false positive.

Reviewed By: mityal

Differential Revision: D17686944

fbshipit-source-id: 3c68bb957
master
Nikos Gorogiannis 5 years ago committed by Facebook Github Bot
parent fb77efea6a
commit 36de121dc5
5 changed files with 429 additions and 308 deletions
Show Stats Download Patch File Download Diff File

186
infer/src/concurrency/starvation.ml
Unescape View File

@ -75,14 +75,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| _ -> | _ ->
None None
in in
let is_java = Summary.get_proc_name summary |> Typ.Procname.is_java in let procname = Summary.get_proc_name summary in
let is_java = Typ.Procname.is_java procname in
let do_lock locks loc astate = let do_lock locks loc astate =
List.filter_map ~f:get_lock_path locks |> Domain.acquire tenv astate loc List.filter_map ~f:get_lock_path locks |> Domain.acquire tenv astate ~procname ~loc
in in
let do_unlock locks astate = List.filter_map ~f:get_lock_path locks |> Domain.release astate in let do_unlock locks astate = List.filter_map ~f:get_lock_path locks |> Domain.release astate in
let do_call callee loc astate = let do_call callee loc astate =
Payload.read ~caller_summary:summary ~callee_pname:callee Payload.read ~caller_summary:summary ~callee_pname:callee
|> Option.value_map ~default:astate ~f:(Domain.integrate_summary tenv astate callee loc) |> Option.value_map ~default:astate ~f:(fun callee_summary ->
Domain.integrate_summary tenv ~caller_summary:astate ~callee_summary ~callee ~loc )
in in
match instr with match instr with
| Assign _ | Assume _ | Call (_, Indirect _, _, _, _) | Metadata _ -> | Assign _ | Assume _ | Call (_, Indirect _, _, _, _) | Metadata _ ->
@ -94,11 +96,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Lock locks -> | Lock locks ->
do_lock locks loc astate do_lock locks loc astate
| GuardLock guard -> | GuardLock guard ->
Domain.lock_guard tenv astate guard loc Domain.lock_guard tenv astate guard ~procname ~loc
| GuardConstruct {guard; lock; acquire_now} -> ( | GuardConstruct {guard; lock; acquire_now} -> (
match get_lock_path lock with match get_lock_path lock with
| Some lock_path -> | Some lock_path ->
Domain.add_guard tenv astate guard lock_path ~acquire_now loc Domain.add_guard tenv astate guard lock_path ~acquire_now ~procname ~loc
| None -> | None ->
log_parse_error "Couldn't parse lock in guard constructor" callee actuals ; log_parse_error "Couldn't parse lock in guard constructor" callee actuals ;
astate ) astate )
@ -116,17 +118,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
do_lock locks loc astate |> do_unlock locks do_lock locks loc astate |> do_unlock locks
| NoEffect when is_java && is_ui_thread_model callee -> | NoEffect when is_java && is_ui_thread_model callee ->
let explanation = F.asprintf "it calls %a" pname_pp callee in let explanation = F.asprintf "it calls %a" pname_pp callee in
Domain.set_on_ui_thread astate loc explanation Domain.set_on_ui_thread astate ~loc explanation
| NoEffect when is_java && StarvationModels.is_strict_mode_violation tenv callee actuals -> | NoEffect when is_java && is_strict_mode_violation tenv callee actuals ->
Domain.strict_mode_call callee loc astate Domain.strict_mode_call ~callee ~loc astate
| NoEffect -> | NoEffect when is_java -> (
if is_java then match may_block tenv callee actuals with
may_block tenv callee actuals | Some sev ->
|> Option.map ~f:(fun sev -> Domain.blocking_call callee sev loc astate) Domain.blocking_call ~callee sev ~loc astate
|> IOption.value_default_f ~f:(fun () -> do_call callee loc astate) | None ->
else
(* in C++/Obj C we only care about deadlocks, not starvation errors *)
do_call callee loc astate ) do_call callee loc astate )
| NoEffect ->
(* in C++/Obj C we only care about deadlocks, not starvation errors *)
do_call callee loc astate )
let pp_session_name _node fmt = F.pp_print_string fmt "starvation" let pp_session_name _node fmt = F.pp_print_string fmt "starvation"
@ -136,10 +139,9 @@ module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.N
let analyze_procedure {Callbacks.exe_env; summary} = let analyze_procedure {Callbacks.exe_env; summary} =
let proc_desc = Summary.get_proc_desc summary in let proc_desc = Summary.get_proc_desc summary in
let open StarvationDomain in let procname = Procdesc.get_proc_name proc_desc in
let pname = Procdesc.get_proc_name proc_desc in let tenv = Exe_env.get_tenv exe_env procname in
let tenv = Exe_env.get_tenv exe_env pname in if StarvationModels.should_skip_analysis tenv procname [] then summary
if StarvationModels.should_skip_analysis tenv pname [] then summary
else else
let formals = FormalMap.make proc_desc in let formals = FormalMap.make proc_desc in
let proc_data = ProcData.make summary tenv formals in let proc_data = ProcData.make summary tenv formals in
@ -148,7 +150,7 @@ let analyze_procedure {Callbacks.exe_env; summary} =
if not (Procdesc.is_java_synchronized proc_desc) then StarvationDomain.bottom if not (Procdesc.is_java_synchronized proc_desc) then StarvationDomain.bottom
else else
let lock = let lock =
match pname with match procname with
| Typ.Procname.Java java_pname when Typ.Procname.Java.is_static java_pname -> | Typ.Procname.Java java_pname when Typ.Procname.Java.is_static java_pname ->
(* this is crafted so as to match synchronized(CLASSNAME.class) constructs *) (* this is crafted so as to match synchronized(CLASSNAME.class) constructs *)
Typ.Procname.Java.get_class_type_name java_pname Typ.Procname.Java.get_class_type_name java_pname
@ -156,22 +158,15 @@ let analyze_procedure {Callbacks.exe_env; summary} =
| _ -> | _ ->
FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> (base, [])) FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> (base, []))
in in
StarvationDomain.acquire tenv StarvationDomain.bottom loc (Option.to_list lock) StarvationDomain.acquire tenv StarvationDomain.bottom ~procname ~loc (Option.to_list lock)
in in
let initial = let initial =
ConcurrencyModels.runs_on_ui_thread ~attrs_of_pname:Summary.OnDisk.proc_resolve_attributes ConcurrencyModels.runs_on_ui_thread ~attrs_of_pname:Summary.OnDisk.proc_resolve_attributes
tenv proc_desc tenv proc_desc
|> Option.value_map ~default:initial ~f:(StarvationDomain.set_on_ui_thread initial loc) |> Option.value_map ~default:initial ~f:(StarvationDomain.set_on_ui_thread initial ~loc)
in in
let filter_blocks = let filter_blocks =
if is_nonblocking tenv proc_desc then fun ({events; order} as astate) -> if is_nonblocking tenv proc_desc then StarvationDomain.filter_blocking_calls else Fn.id
{ astate with
events= EventDomain.filter (function {elem= MayBlock _} -> false | _ -> true) events
; order=
OrderDomain.filter
(function {elem= {eventually= {elem= MayBlock _}}} -> false | _ -> true)
order }
else Fn.id
in in
Analyzer.compute_post proc_data ~initial Analyzer.compute_post proc_data ~initial
|> Option.map ~f:filter_blocks |> Option.map ~f:filter_blocks
@ -313,29 +308,28 @@ let should_report_deadlock_on_current_proc current_elem endpoint_elem =
(not Config.deduplicate) (not Config.deduplicate)
|| ||
let open StarvationDomain in let open StarvationDomain in
match (current_elem.Order.elem.first, current_elem.Order.elem.eventually.elem) with match (endpoint_elem.CriticalPair.elem.event, current_elem.CriticalPair.elem.event) with
| _, (MayBlock _ | StrictModeCall _) -> | _, (MayBlock _ | StrictModeCall _) | (MayBlock _ | StrictModeCall _), _ ->
(* should never happen *) (* should never happen *)
L.die InternalError "Deadlock cannot occur without two lock events: %a" Order.pp current_elem L.die InternalError "Deadlock cannot occur without two lock events: %a" CriticalPair.pp
| ((Var.LogicalVar _, _), []), _ -> current_elem
| LockAcquire ((Var.LogicalVar _, _), []), _ ->
(* first elem is a class object (see [lock_of_class]), so always report because the (* first elem is a class object (see [lock_of_class]), so always report because the
reverse ordering on the events will not occur *) reverse ordering on the events will not occur -- FIXME WHY? *)
true true
| ((Var.LogicalVar _, _), _ :: _), _ | _, LockAcquire ((Var.LogicalVar _, _), _) -> | LockAcquire ((Var.LogicalVar _, _), _ :: _), _ | _, LockAcquire ((Var.LogicalVar _, _), _) ->
(* first elem has an ident root, but has a non-empty access path, which means we are (* first elem has an ident root, but has a non-empty access path, which means we are
not filtering out local variables (see [exec_instr]), or, not filtering out local variables (see [exec_instr]), or,
second elem has an ident root, which should not happen if we are filtering locals *) second elem has an ident root, which should not happen if we are filtering locals *)
L.die InternalError "Deadlock cannot occur on these logical variables: %a @." Order.pp L.die InternalError "Deadlock cannot occur on these logical variables: %a @." CriticalPair.pp
current_elem current_elem
| ((_, typ1), _), LockAcquire ((_, typ2), _) -> | LockAcquire ((_, typ1), _), LockAcquire ((_, typ2), _) ->
(* use string comparison on types as a stable order to decide whether to report a deadlock *) (* use string comparison on types as a stable order to decide whether to report a deadlock *)
let c = String.compare (Typ.to_string typ1) (Typ.to_string typ2) in let c = String.compare (Typ.to_string typ1) (Typ.to_string typ2) in
c < 0 c < 0
|| Int.equal 0 c || Int.equal 0 c
&& (* same class, so choose depending on location *) && (* same class, so choose depending on location *)
Location.compare current_elem.Order.elem.eventually.Event.loc Location.compare current_elem.CriticalPair.loc endpoint_elem.CriticalPair.loc < 0
endpoint_elem.Order.elem.eventually.Event.loc
< 0
let should_report pdesc = let should_report pdesc =
@ -368,7 +362,7 @@ let fold_reportable_summaries (tenv, current_summary) clazz ~init ~f =
List.fold methods ~init ~f List.fold methods ~init ~f
let report_lockless_violations (tenv, summary) {StarvationDomain.events} report_map = let report_lockless_violations (tenv, summary) StarvationDomain.{critical_pairs} report_map =
let open StarvationDomain in let open StarvationDomain in
(* this is inneficient as it climbs the hierarchy potentially twice *) (* this is inneficient as it climbs the hierarchy potentially twice *)
let is_annotated_lockless tenv pname = let is_annotated_lockless tenv pname =
@ -383,43 +377,45 @@ let report_lockless_violations (tenv, summary) {StarvationDomain.events} report_
let pname = Summary.get_proc_name summary in let pname = Summary.get_proc_name summary in
if not (is_annotated_lockless tenv pname) then report_map if not (is_annotated_lockless tenv pname) then report_map
else else
let report_violation (event : Event.t) report_map = let report_violation ({elem= {event}} as critical_pair : CriticalPair.t) report_map =
match event.elem with match event with
| LockAcquire _ -> | LockAcquire _ ->
let error_message = let error_message =
Format.asprintf "Method %a is annotated %s but%a." pname_pp pname Format.asprintf "Method %a is annotated %s but%a." pname_pp pname
(MF.monospaced_to_string Annotations.lockless) (MF.monospaced_to_string Annotations.lockless)
Event.describe event Event.describe event
in in
let loc = Event.get_loc event in let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:pname critical_pair in
let ltr = Event.make_trace pname event in let ltr = CriticalPair.make_trace pname critical_pair in
ReportMap.add_lockless_violation pname loc ltr error_message report_map ReportMap.add_lockless_violation pname loc ltr error_message report_map
| _ -> | _ ->
report_map report_map
in in
EventDomain.fold report_violation events report_map CriticalPairs.fold report_violation critical_pairs report_map
(* Note about how many times we report a deadlock: normally twice, at each trace starting point. (* Note about how many times we report a deadlock: normally twice, at each trace starting point.
Due to the fact we look for deadlocks in the summaries of the class at the root of a path, Due to the fact we look for deadlocks in the summaries of the class at the root of a path,
this will fail when (a) the lock is of class type (ie as used in static sync methods), because this will fail when (a) the lock is of class type (ie as used in static sync methods), because
then the root is an identifier of type java.lang.Class and (b) when the lock belongs to an then the root is an identifier of type java.lang.Class and (b) when the lock belongs to an
inner class but this is no longer obvious in the path, because of nested-class path normalisation. 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 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. *) once, as opposed to twice with all other deadlock pairs. *)
let report_deadlocks env {StarvationDomain.order; ui} report_map' = let report_deadlocks env StarvationDomain.{critical_pairs; ui} report_map' =
let open StarvationDomain in let open StarvationDomain in
let _, current_summary = env in let _, current_summary = env in
let current_pname = Summary.get_proc_name current_summary in let current_pname = Summary.get_proc_name current_summary in
let report_endpoint_elem current_elem endpoint_pname elem report_map = let report_endpoint_elem current_elem endpoint_pname elem report_map =
if if
not not
( Order.may_deadlock current_elem elem ( CriticalPair.may_deadlock current_elem elem
&& should_report_deadlock_on_current_proc current_elem elem ) && should_report_deadlock_on_current_proc current_elem elem )
then report_map then report_map
else else
let () = debug "Possible deadlock:@.%a@.%a@." Order.pp current_elem Order.pp elem in let () =
match (current_elem.Order.elem.eventually.elem, elem.Order.elem.eventually.elem) with debug "Possible deadlock:@.%a@.%a@." CriticalPair.pp current_elem CriticalPair.pp elem
in
match (current_elem.CriticalPair.elem.event, elem.CriticalPair.elem.event) with
| LockAcquire lock1, LockAcquire lock2 -> | LockAcquire lock1, LockAcquire lock2 ->
let error_message = let error_message =
Format.asprintf Format.asprintf
@ -428,25 +424,30 @@ let report_deadlocks env {StarvationDomain.order; ui} report_map' =
pname_pp current_pname pname_pp endpoint_pname Lock.describe lock1 Lock.describe pname_pp current_pname pname_pp endpoint_pname Lock.describe lock1 Lock.describe
lock2 lock2
in in
let first_trace = Order.make_trace ~header:"[Trace 1] " current_pname current_elem in let first_trace =
let second_trace = Order.make_trace ~header:"[Trace 2] " endpoint_pname elem in CriticalPair.make_trace ~header:"[Trace 1] " current_pname current_elem
in
let second_trace = CriticalPair.make_trace ~header:"[Trace 2] " endpoint_pname elem in
let ltr = first_trace @ second_trace in let ltr = first_trace @ second_trace in
let loc = Order.get_loc current_elem in let loc =
CriticalPair.get_earliest_lock_or_call_loc ~procname:current_pname current_elem
in
ReportMap.add_deadlock current_pname loc ltr error_message report_map ReportMap.add_deadlock current_pname loc ltr error_message report_map
| _, _ -> | _, _ ->
report_map report_map
in in
let report_on_current_elem elem report_map = let report_on_current_elem elem report_map =
match elem.Order.elem.eventually.elem with match elem.CriticalPair.elem.event with
| MayBlock _ | StrictModeCall _ -> | MayBlock _ | StrictModeCall _ ->
report_map report_map
| LockAcquire endpoint_lock when Lock.equal endpoint_lock elem.Order.elem.first -> | LockAcquire endpoint_lock
when Acquisitions.lock_is_held endpoint_lock elem.CriticalPair.elem.acquisitions ->
let error_message = let error_message =
Format.asprintf "Potential self deadlock. %a%a twice." pname_pp current_pname Format.asprintf "Potential self deadlock. %a%a twice." pname_pp current_pname
Lock.pp_locks endpoint_lock Lock.pp_locks endpoint_lock
in in
let ltr = Order.make_trace ~header:"In method " current_pname elem in let ltr = CriticalPair.make_trace ~header:"In method " current_pname elem in
let loc = Order.get_loc elem in let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:current_pname elem in
ReportMap.add_deadlock current_pname loc ltr error_message report_map ReportMap.add_deadlock current_pname loc ltr error_message report_map
| LockAcquire endpoint_lock -> | LockAcquire endpoint_lock ->
Lock.owner_class endpoint_lock Lock.owner_class endpoint_lock
@ -455,50 +456,59 @@ let report_deadlocks env {StarvationDomain.order; ui} report_map' =
and retrieve all the summaries of the methods of that class *) and retrieve all the summaries of the methods of that class *)
(* for each summary related to the endpoint, analyse and report on its pairs *) (* for each summary related to the endpoint, analyse and report on its pairs *)
fold_reportable_summaries env endpoint_class ~init:report_map fold_reportable_summaries env endpoint_class ~init:report_map
~f:(fun acc (endpoint_pname, {order= endp_order; ui= endp_ui}) -> ~f:(fun acc
(endpoint_pname, {critical_pairs= endp_critical_pairs; ui= endp_ui})
->
if UIThreadDomain.is_bottom ui || UIThreadDomain.is_bottom endp_ui then if UIThreadDomain.is_bottom ui || UIThreadDomain.is_bottom endp_ui then
OrderDomain.fold (report_endpoint_elem elem endpoint_pname) endp_order acc CriticalPairs.fold
(report_endpoint_elem elem endpoint_pname)
endp_critical_pairs acc
else acc ) ) else acc ) )
in in
OrderDomain.fold report_on_current_elem order report_map' CriticalPairs.fold report_on_current_elem critical_pairs report_map'
let report_starvation env {StarvationDomain.events; ui} report_map' = let report_starvation env {StarvationDomain.critical_pairs; ui} report_map' =
let open StarvationDomain in let open StarvationDomain in
let _, current_summary = env in let _, current_summary = env in
let current_pname = Summary.get_proc_name current_summary in let current_pname = Summary.get_proc_name current_summary in
let report_remote_block ui_explain event current_lock endpoint_pname endpoint_elem report_map = let report_remote_block ui_explain event current_lock endpoint_pname endpoint_elem report_map =
let lock = endpoint_elem.Order.elem.first in let acquisitions = endpoint_elem.CriticalPair.elem.acquisitions in
match endpoint_elem.Order.elem.eventually.elem with match endpoint_elem.CriticalPair.elem.event with
| MayBlock (block_descr, sev) when Lock.equal current_lock lock -> | MayBlock (block_descr, sev) when Acquisitions.lock_is_held current_lock acquisitions ->
let error_message = let error_message =
Format.asprintf Format.asprintf
"Method %a runs on UI thread (because %a) and%a, which may be held by another thread \ "Method %a runs on UI thread (because %a) and%a, which may be held by another thread \
which %s." which %s."
pname_pp current_pname UIThreadExplanationDomain.pp ui_explain Lock.pp_locks lock pname_pp current_pname UIThreadExplanationDomain.pp ui_explain Lock.pp_locks
block_descr current_lock block_descr
in
let first_trace = CriticalPair.make_trace ~header:"[Trace 1] " current_pname event in
let second_trace =
CriticalPair.make_trace ~header:"[Trace 2] " endpoint_pname endpoint_elem
in in
let first_trace = Event.make_trace ~header:"[Trace 1] " current_pname event in
let second_trace = Order.make_trace ~header:"[Trace 2] " endpoint_pname endpoint_elem in
let ui_trace = let ui_trace =
UIThreadExplanationDomain.make_trace ~header:"[Trace 1 on UI thread] " current_pname UIThreadExplanationDomain.make_trace ~header:"[Trace 1 on UI thread] " current_pname
ui_explain ui_explain
in in
let ltr = first_trace @ second_trace @ ui_trace in let ltr = first_trace @ second_trace @ ui_trace in
let loc = Event.get_loc event in let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:current_pname event in
ReportMap.add_starvation sev current_pname loc ltr error_message report_map ReportMap.add_starvation sev current_pname loc ltr error_message report_map
| _ -> | _ ->
report_map report_map
in in
let report_on_current_elem ui_explain event report_map = let report_on_current_elem ui_explain (critical_pair : CriticalPair.t) report_map =
match event.Event.elem with let event = critical_pair.elem.event in
match event with
| MayBlock (_, sev) -> | MayBlock (_, sev) ->
let error_message = let error_message =
Format.asprintf "Method %a runs on UI thread (because %a), and may block; %a." pname_pp Format.asprintf "Method %a runs on UI thread (because %a), and may block; %a." pname_pp
current_pname UIThreadExplanationDomain.pp ui_explain Event.describe event current_pname UIThreadExplanationDomain.pp ui_explain Event.describe event
in in
let loc = Event.get_loc event in let loc = CriticalPair.get_loc critical_pair in
let trace = Event.make_trace current_pname event in let trace =
CriticalPair.make_trace ~include_acquisitions:false current_pname critical_pair
in
let ui_trace = let ui_trace =
UIThreadExplanationDomain.make_trace ~header:"[Trace on UI thread] " current_pname UIThreadExplanationDomain.make_trace ~header:"[Trace on UI thread] " current_pname
ui_explain ui_explain
@ -511,8 +521,10 @@ let report_starvation env {StarvationDomain.events; ui} report_map' =
"Method %a runs on UI thread (because %a), and may violate Strict Mode; %a." pname_pp "Method %a runs on UI thread (because %a), and may violate Strict Mode; %a." pname_pp
current_pname UIThreadExplanationDomain.pp ui_explain Event.describe event current_pname UIThreadExplanationDomain.pp ui_explain Event.describe event
in in
let loc = Event.get_loc event in let loc = CriticalPair.get_loc critical_pair in
let trace = Event.make_trace current_pname event in let trace =
CriticalPair.make_trace ~include_acquisitions:false current_pname critical_pair
in
let ui_trace = let ui_trace =
UIThreadExplanationDomain.make_trace ~header:"[Trace on UI thread] " current_pname UIThreadExplanationDomain.make_trace ~header:"[Trace on UI thread] " current_pname
ui_explain ui_explain
@ -526,12 +538,12 @@ let report_starvation env {StarvationDomain.events; ui} report_map' =
and retrieve all the summaries of the methods of that class *) and retrieve all the summaries of the methods of that class *)
(* for each summary related to the endpoint, analyse and report on its pairs *) (* for each summary related to the endpoint, analyse and report on its pairs *)
fold_reportable_summaries env endpoint_class ~init:report_map fold_reportable_summaries env endpoint_class ~init:report_map
~f:(fun acc (endpoint_pname, {order; ui}) -> ~f:(fun acc (endpoint_pname, {critical_pairs; ui}) ->
(* skip methods on ui thread, as they cannot run in parallel to us *) (* skip methods on ui thread, as they cannot run in parallel to us *)
if UIThreadDomain.is_bottom ui then if UIThreadDomain.is_bottom ui then
OrderDomain.fold CriticalPairs.fold
(report_remote_block ui_explain event endpoint_lock endpoint_pname) (report_remote_block ui_explain critical_pair endpoint_lock endpoint_pname)
order acc critical_pairs acc
else acc ) ) else acc ) )
in in
(* do not report starvation/strict mode warnings on constructors, keep that for callers *) (* do not report starvation/strict mode warnings on constructors, keep that for callers *)
@ -541,7 +553,7 @@ let report_starvation env {StarvationDomain.events; ui} report_map' =
| AbstractDomain.Types.Bottom -> | AbstractDomain.Types.Bottom ->
report_map' report_map'
| AbstractDomain.Types.NonBottom ui_explain -> | AbstractDomain.Types.NonBottom ui_explain ->
EventDomain.fold (report_on_current_elem ui_explain) events report_map' CriticalPairs.fold (report_on_current_elem ui_explain) critical_pairs report_map'
let reporting {Callbacks.procedures; source_file} = let reporting {Callbacks.procedures; source_file} =

443
infer/src/concurrency/starvationDomain.ml
Unescape View File

@ -47,8 +47,6 @@ module Lock = struct
let pp_locks fmt lock = F.fprintf fmt " locks %a" describe lock let pp_locks fmt lock = F.fprintf fmt " locks %a" describe lock
end end
module LockEvent = ExplicitTrace.MakeTraceElem (Lock) (ExplicitTrace.DefaultCallPrinter)
module Event = struct module Event = struct
type severity_t = Low | Medium | High [@@deriving compare] type severity_t = Low | Medium | High [@@deriving compare]
@ -57,132 +55,254 @@ module Event = struct
F.pp_print_string fmt msg F.pp_print_string fmt msg
type event_t = type t = LockAcquire of Lock.t | MayBlock of (string * severity_t) | StrictModeCall of string
| LockAcquire of Lock.t
| MayBlock of (string * severity_t)
| StrictModeCall of string
[@@deriving compare] [@@deriving compare]
module EventElement = struct let pp fmt = function
type t = event_t [@@deriving compare] | LockAcquire lock ->
F.fprintf fmt "LockAcquire(%a)" Lock.pp lock
let pp fmt = function | MayBlock (msg, sev) ->
| LockAcquire lock -> F.fprintf fmt "MayBlock(%s, %a)" msg pp_severity sev
F.fprintf fmt "LockAcquire(%a)" Lock.pp lock | StrictModeCall msg ->
| MayBlock (msg, sev) -> F.fprintf fmt "StrictModeCall(%s)" msg
F.fprintf fmt "MayBlock(%s, %a)" msg pp_severity sev
| StrictModeCall msg ->
F.fprintf fmt "StrictModeCall(%s)" msg let describe fmt elem =
match elem with
| LockAcquire lock ->
let describe fmt elem = Lock.pp_locks fmt lock
match elem with | MayBlock (msg, _) ->
| LockAcquire lock -> F.pp_print_string fmt msg
Lock.pp_locks fmt lock | StrictModeCall msg ->
| MayBlock (msg, _) -> F.pp_print_string fmt msg
F.pp_print_string fmt msg
| StrictModeCall msg ->
F.pp_print_string fmt msg
end
include ExplicitTrace.MakeTraceElem (EventElement) (ExplicitTrace.DefaultCallPrinter)
let make_acquire lock loc = make (LockAcquire lock) loc let make_acquire lock = LockAcquire lock
let make_call_descr callee = F.asprintf "calls %a" pname_pp callee let make_call_descr callee = F.asprintf "calls %a" pname_pp callee
let make_blocking_call callee sev loc = let make_blocking_call callee sev =
let descr = make_call_descr callee in let descr = make_call_descr callee in
make (MayBlock (descr, sev)) loc MayBlock (descr, sev)
let make_strict_mode_call callee loc = let make_strict_mode_call callee =
let descr = make_call_descr callee in let descr = make_call_descr callee in
make (StrictModeCall descr) loc StrictModeCall descr
end
(** A lock acquisition with source location and procname in which it occurs.
The location & procname are *ignored* for comparisons, and are only for reporting. *)
module Acquisition = struct
type t =
{lock: Lock.t; loc: Location.t [@compare.ignore]; procname: Typ.Procname.t [@compare.ignore]}
[@@deriving compare]
let make_trace ?(header = "") pname elem = let pp fmt {lock} = Lock.pp_locks fmt lock
let trace = make_loc_trace elem in
let trace_descr = F.asprintf "%s%a" header pname_pp pname in let make ~procname ~loc lock = {lock; loc; procname}
let start_loc = get_loc elem in
let header_step = Errlog.make_trace_element 0 start_loc trace_descr [] in let compare_loc {loc= loc1} {loc= loc2} = Location.compare loc1 loc2
header_step :: trace
let make_trace_step acquisition =
let description = F.asprintf "%a" pp acquisition in
Errlog.make_trace_element 0 acquisition.loc description []
end end
module EventDomain = Event.FiniteSet (** Set of acquisitions; due to order over acquisitions, each lock appears at most once. *)
module Acquisitions = struct
include PrettyPrintable.MakePPSet (Acquisition)
module Order = struct (* use the fact that location/procname are ignored in comparisons *)
type order_t = {first: Lock.t; eventually: Event.t} [@@deriving compare] let lock_is_held lock acquisitions =
mem {lock; loc= Location.dummy; procname= Typ.Procname.Linters_dummy_method} acquisitions
end
module OrderElement = struct module LockState : sig
type t = order_t include AbstractDomain.WithTop
let compare = compare_order_t val acquire : procname:Typ.Procname.t -> loc:Location.t -> Lock.t -> t -> t
let pp fmt {first; eventually} = val release : Lock.t -> t -> t
F.fprintf fmt "{first= %a; eventually= %a}" Lock.pp first Event.pp eventually
val is_lock_taken : Event.t -> t -> bool
let describe fmt {first} = Lock.pp_locks fmt first val get_acquisitions : t -> Acquisitions.t
end end = struct
module LockStack = AbstractDomain.StackDomain (Acquisition)
include AbstractDomain.InvertedMap (Lock) (LockStack)
include ExplicitTrace.MakeTraceElem (OrderElement) (ExplicitTrace.DefaultCallPrinter) let get_stack lock map = find_opt lock map |> Option.value ~default:LockStack.top
let may_deadlock {elem= {first; eventually}} {elem= {first= first'; eventually= eventually'}} = let is_lock_taken event map =
match (eventually.elem, eventually'.elem) with match event with
| LockAcquire e, LockAcquire e' -> | Event.LockAcquire lock ->
Lock.equal first e' && Lock.equal first' e not (LockStack.is_top (get_stack lock map))
| _, _ -> | _ ->
false false
let make_loc_trace ?(nesting = 0) ({elem= {eventually}} as order) = let acquire ~procname ~loc lock map =
let first_trace = make_loc_trace ~nesting order in let acquisition = Acquisition.make ~procname ~loc lock in
let first_nesting = List.length first_trace in let current_value = get_stack lock map in
let eventually_trace = Event.make_loc_trace ~nesting:first_nesting eventually in let new_value = LockStack.push acquisition current_value in
first_trace @ eventually_trace add lock new_value map
let make_trace ?(header = "") pname elem = let release lock map =
let trace = make_loc_trace elem in let current_value = get_stack lock map in
let trace_descr = F.asprintf "%s%a" header pname_pp pname in if LockStack.is_top current_value then map
let start_loc = get_loc elem in else
let header_step = Errlog.make_trace_element 0 start_loc trace_descr [] in let new_value = LockStack.pop current_value in
header_step :: trace if LockStack.is_top new_value then remove lock map else add lock new_value map
(* FIXME - this should be a O(1) operation by moving it into the lock-state and updating in tandem,
so as to increase sharing between critical pairs. *)
let get_acquisitions map =
fold
(fun _lock lock_stack init ->
List.fold lock_stack ~init ~f:(fun acc acquisition -> Acquisitions.add acquisition acc) )
map Acquisitions.empty
end end
module OrderDomain = Order.FiniteSet module CriticalPairElement = struct
module LockStack = AbstractDomain.StackDomain (LockEvent) type t = {acquisitions: Acquisitions.t; event: Event.t} [@@deriving compare]
module LockState = struct let pp fmt {acquisitions; event} =
include AbstractDomain.InvertedMap (Lock) (LockStack) F.fprintf fmt "{acquisitions= %a; event= %a}" Acquisitions.pp acquisitions Event.pp event
let is_taken lock_event map =
match lock_event.Event.elem with
| Event.LockAcquire lock -> (
try not (find lock map |> LockStack.is_top) with Caml.Not_found -> false )
| _ ->
false
let describe = pp
end
let acquire loc map lock_id = module CriticalPair = struct
let lock_event = LockEvent.make lock_id loc in include ExplicitTrace.MakeTraceElem (CriticalPairElement) (ExplicitTrace.DefaultCallPrinter)
let current_value = try find lock_id map with Caml.Not_found -> LockStack.top in
let new_value = LockStack.push lock_event current_value in
add lock_id new_value map
let make ~loc acquisitions event = make {acquisitions; event} loc
let release lock_id map = let is_blocking_call {elem= {event}} = match event with LockAcquire _ -> true | _ -> false
let current_value = try find lock_id map with Caml.Not_found -> LockStack.top in
if LockStack.is_top current_value then map let get_final_acquire {elem= {event}} =
else match event with LockAcquire lock -> Some lock | _ -> None
let new_value = LockStack.pop current_value in
if LockStack.is_top new_value then remove lock_id map else add lock_id new_value map
let may_deadlock ({elem= pair1} as t1 : t) ({elem= pair2} as t2 : t) =
Option.both (get_final_acquire t1) (get_final_acquire t2)
|> Option.exists ~f:(fun (lock1, lock2) ->
(not (Lock.equal lock1 lock2))
&& Acquisitions.lock_is_held lock2 pair1.acquisitions
&& Acquisitions.lock_is_held lock1 pair2.acquisitions
&& Acquisitions.inter pair1.acquisitions pair2.acquisitions |> Acquisitions.is_empty )
let with_callsite t existing_acquisitions call_site =
let f ({acquisitions} as elem : CriticalPairElement.t) =
{elem with acquisitions= Acquisitions.union existing_acquisitions acquisitions}
in
let new_t = map ~f t in
with_callsite new_t call_site
let get_earliest_lock_or_call_loc ~procname ({elem= {acquisitions}} as t) =
let initial_loc = get_loc t in
Acquisitions.fold
(fun {procname= acq_procname; loc= acq_loc} acc ->
if
Typ.Procname.equal procname acq_procname
&& Int.is_negative (Location.compare acq_loc acc)
then acq_loc
else acc )
acquisitions initial_loc
let make_trace ?(header = "") ?(include_acquisitions = true) top_pname
{elem= {acquisitions; event}; trace; loc} =
let acquisitions_map =
if include_acquisitions then
Acquisitions.fold
(fun ({procname} as acq : Acquisition.t) acc ->
Typ.Procname.Map.update procname
(function None -> Some [acq] | Some acqs -> Some (acq :: acqs))
acc )
acquisitions Typ.Procname.Map.empty
else Typ.Procname.Map.empty
in
let header_step =
let description = F.asprintf "%s%a" header pname_pp top_pname in
let loc = Location.dummy in
Errlog.make_trace_element 0 loc description []
in
(* construct the trace segment starting at [call_site] and ending at next call *)
let make_call_stack_step fake_first_call call_site =
let procname = CallSite.pname call_site in
let trace =
Typ.Procname.Map.find_opt procname acquisitions_map
|> Option.value ~default:[]
(* many acquisitions can be on same line (eg, std::lock) so use stable sort
to produce a deterministic trace *)
|> List.stable_sort ~compare:Acquisition.compare_loc
|> List.map ~f:Acquisition.make_trace_step
in
if CallSite.equal call_site fake_first_call then trace
else
let descr = F.asprintf "%a" ExplicitTrace.DefaultCallPrinter.pp call_site in
let call_step = Errlog.make_trace_element 0 (CallSite.loc call_site) descr [] in
call_step :: trace
in
(* construct a call stack trace with the lock acquisitions interleaved *)
let call_stack =
(* fake outermost call so as to include acquisitions in the top level caller *)
let fake_first_call = CallSite.make top_pname Location.dummy in
List.map (fake_first_call :: trace) ~f:(make_call_stack_step fake_first_call)
in
let endpoint_step =
let endpoint_descr = F.asprintf "%a" Event.describe event in
Errlog.make_trace_element 0 loc endpoint_descr []
in
List.concat (([header_step] :: call_stack) @ [[endpoint_step]])
end
let is_recursive_lock event tenv =
let is_class_and_recursive_lock = function
| {Typ.desc= Tptr ({desc= Tstruct name}, _)} | {desc= Tstruct name} ->
ConcurrencyModels.is_recursive_lock_type name
| typ ->
L.debug Analysis Verbose "Asked if non-struct type %a is a recursive lock type.@."
(Typ.pp_full Pp.text) typ ;
true
in
match event with
| Event.LockAcquire lock_path ->
AccessPath.get_typ lock_path tenv |> Option.exists ~f:is_class_and_recursive_lock
| _ ->
false
let fold_over_events f map init = (** skip adding an order pair [(_, event)] if
let ff _ lock_state acc = List.fold lock_state ~init:acc ~f in - we have no tenv, or,
fold ff map init - [event] is not a lock event, or,
- we do not hold the lock, or,
- the lock is not recursive. *)
let should_skip tenv_opt event lock_state =
Option.exists tenv_opt ~f:(fun tenv ->
LockState.is_lock_taken event lock_state && is_recursive_lock event tenv )
module CriticalPairs = struct
include CriticalPair.FiniteSet
let with_callsite astate tenv_opt lock_state call_site =
let existing_acquisitions = LockState.get_acquisitions lock_state in
fold
(fun ({elem= {event}} as critical_pair : CriticalPair.t) acc ->
if should_skip tenv_opt event lock_state then acc
else
let new_pair =
CriticalPair.with_callsite critical_pair existing_acquisitions call_site
in
add new_pair acc )
astate empty
end end
module UIThreadExplanationDomain = struct module UIThreadExplanationDomain = struct
@ -231,110 +351,81 @@ module GuardToLockMap = struct
end end
type t = type t =
{ events: EventDomain.t { guard_map: GuardToLockMap.t
; guard_map: GuardToLockMap.t
; lock_state: LockState.t ; lock_state: LockState.t
; order: OrderDomain.t ; critical_pairs: CriticalPairs.t
; ui: UIThreadDomain.t } ; ui: UIThreadDomain.t }
let bottom = let bottom =
{ events= EventDomain.empty { guard_map= GuardToLockMap.empty
; guard_map= GuardToLockMap.empty ; lock_state= LockState.top
; lock_state= LockState.empty ; critical_pairs= CriticalPairs.empty
; order= OrderDomain.empty
; ui= UIThreadDomain.bottom } ; ui= UIThreadDomain.bottom }
let is_bottom {events; guard_map; lock_state; order; ui} = let is_bottom {guard_map; lock_state; critical_pairs; ui} =
EventDomain.is_empty events && GuardToLockMap.is_empty guard_map && OrderDomain.is_empty order GuardToLockMap.is_empty guard_map && LockState.is_top lock_state
&& LockState.is_empty lock_state && UIThreadDomain.is_bottom ui && CriticalPairs.is_empty critical_pairs
&& UIThreadDomain.is_bottom ui
let pp fmt {events; guard_map; lock_state; order; ui} = let pp fmt {guard_map; lock_state; critical_pairs; ui} =
F.fprintf fmt "{events= %a; guard_map= %a; lock_state= %a; order= %a; ui= %a}" EventDomain.pp F.fprintf fmt "{guard_map= %a; lock_state= %a; critical_pairs= %a; ui= %a}" GuardToLockMap.pp
events GuardToLockMap.pp guard_map LockState.pp lock_state OrderDomain.pp order guard_map LockState.pp lock_state CriticalPairs.pp critical_pairs UIThreadDomain.pp ui
UIThreadDomain.pp ui
let join lhs rhs = let join lhs rhs =
{ events= EventDomain.join lhs.events rhs.events { guard_map= GuardToLockMap.join lhs.guard_map rhs.guard_map
; guard_map= GuardToLockMap.join lhs.guard_map rhs.guard_map
; lock_state= LockState.join lhs.lock_state rhs.lock_state ; lock_state= LockState.join lhs.lock_state rhs.lock_state
; order= OrderDomain.join lhs.order rhs.order ; critical_pairs= CriticalPairs.join lhs.critical_pairs rhs.critical_pairs
; ui= UIThreadDomain.join lhs.ui rhs.ui } ; ui= UIThreadDomain.join lhs.ui rhs.ui }
let widen ~prev ~next ~num_iters:_ = join prev next let widen ~prev ~next ~num_iters:_ = join prev next
let ( <= ) ~lhs ~rhs = let ( <= ) ~lhs ~rhs =
EventDomain.( <= ) ~lhs:lhs.events ~rhs:rhs.events GuardToLockMap.( <= ) ~lhs:lhs.guard_map ~rhs:rhs.guard_map
&& GuardToLockMap.( <= ) ~lhs:lhs.guard_map ~rhs:rhs.guard_map
&& OrderDomain.( <= ) ~lhs:lhs.order ~rhs:rhs.order
&& LockState.( <= ) ~lhs:lhs.lock_state ~rhs:rhs.lock_state && LockState.( <= ) ~lhs:lhs.lock_state ~rhs:rhs.lock_state
&& CriticalPairs.( <= ) ~lhs:lhs.critical_pairs ~rhs:rhs.critical_pairs
&& UIThreadDomain.( <= ) ~lhs:lhs.ui ~rhs:rhs.ui && UIThreadDomain.( <= ) ~lhs:lhs.ui ~rhs:rhs.ui
let is_recursive_lock event tenv =
let is_class_and_recursive_lock = function
| {Typ.desc= Tptr ({desc= Tstruct name}, _)} | {desc= Tstruct name} ->
ConcurrencyModels.is_recursive_lock_type name
| typ ->
L.debug Analysis Verbose "Asked if non-struct type %a is a recursive lock type.@."
(Typ.pp_full Pp.text) typ ;
true
in
match event with
| {Event.elem= LockAcquire lock_path} ->
AccessPath.get_typ lock_path tenv |> Option.exists ~f:is_class_and_recursive_lock
| _ ->
false
(** 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_opt event lock_state =
Option.exists tenv_opt ~f:(fun tenv ->
LockState.is_taken event lock_state && is_recursive_lock event tenv )
(* for every lock b held locally, add a pair (b, event) *) (* for every lock b held locally, add a pair (b, event) *)
let add_order_pairs tenv_opt lock_state event acc = let add_critical_pair tenv_opt lock_state event ~loc acc =
if should_skip tenv_opt event lock_state then acc if should_skip tenv_opt event lock_state then acc
else else
let add_first_and_eventually acc ({elem= first; loc} : LockEvent.t) = (* FIXME we should not do this repeatedly in the fold below *)
let new_elem = Order.make {first; eventually= event} loc in let acquisitions = LockState.get_acquisitions lock_state in
OrderDomain.add new_elem acc let critical_pair = CriticalPair.make ~loc acquisitions event in
in CriticalPairs.add critical_pair acc
LockState.fold_over_events add_first_and_eventually lock_state acc
let acquire tenv ({lock_state; events; order} as astate) loc locks = let acquire tenv ({lock_state; critical_pairs} as astate) ~procname ~loc locks =
let new_events = List.map locks ~f:(fun lock -> Event.make_acquire lock loc) in
{ astate with { astate with
events= List.fold new_events ~init:events ~f:(fun acc e -> EventDomain.add e acc) (* FIXME do one fold not two *)
; order= critical_pairs=
List.fold new_events ~init:order ~f:(fun acc e -> List.fold locks ~init:critical_pairs ~f:(fun acc lock ->
OrderDomain.union acc (add_order_pairs (Some tenv) lock_state e order) ) let event = Event.make_acquire lock in
; lock_state= List.fold locks ~init:lock_state ~f:(LockState.acquire loc) } add_critical_pair (Some tenv) lock_state event ~loc acc )
; lock_state=
List.fold locks ~init:lock_state ~f:(fun acc lock ->
LockState.acquire ~procname ~loc lock acc ) }
let make_call_with_event tenv_opt new_event astate = let make_call_with_event tenv_opt new_event ~loc astate =
{ astate with { astate with
events= EventDomain.add new_event astate.events critical_pairs=
; order= add_order_pairs tenv_opt astate.lock_state new_event astate.order } add_critical_pair tenv_opt astate.lock_state new_event ~loc astate.critical_pairs }
let blocking_call callee sev loc astate = let blocking_call ~callee sev ~loc astate =
let new_event = Event.make_blocking_call callee sev loc in let new_event = Event.make_blocking_call callee sev in
make_call_with_event None new_event astate make_call_with_event None new_event ~loc astate
let strict_mode_call callee loc astate = let strict_mode_call ~callee ~loc astate =
let new_event = Event.make_strict_mode_call callee loc in let new_event = Event.make_strict_mode_call callee in
make_call_with_event None new_event astate make_call_with_event None new_event ~loc astate
let release ({lock_state} as astate) locks = let release ({lock_state} as astate) locks =
@ -342,27 +433,19 @@ let release ({lock_state} as astate) locks =
lock_state= List.fold locks ~init:lock_state ~f:(fun acc l -> LockState.release l acc) } lock_state= List.fold locks ~init:lock_state ~f:(fun acc l -> LockState.release l acc) }
let integrate_summary tenv ({lock_state; events; order; ui} as astate) callee_pname loc let integrate_summary tenv ~caller_summary:({lock_state; critical_pairs; ui} as astate) ~callee
callee_summary = ~loc ~callee_summary =
let callsite = CallSite.make callee_pname loc in let callsite = CallSite.make callee loc in
let callee_order = OrderDomain.with_callsite callee_summary.order callsite in let critical_pairs' =
let callee_ui = UIThreadDomain.with_callsite callee_summary.ui callsite in CriticalPairs.with_callsite callee_summary.critical_pairs (Some tenv) lock_state callsite
let should_keep event = should_skip (Some tenv) event lock_state |> not in
let filtered_order =
OrderDomain.filter (fun {elem= {eventually}} -> should_keep eventually) callee_order
in
let callee_events = EventDomain.with_callsite callee_summary.events callsite in
let filtered_events = EventDomain.filter should_keep callee_events in
let order' =
EventDomain.fold (add_order_pairs (Some tenv) lock_state) filtered_events filtered_order
in in
let callee_ui = UIThreadDomain.with_callsite callee_summary.ui callsite in
{ astate with { astate with
events= EventDomain.join events filtered_events critical_pairs= CriticalPairs.join critical_pairs critical_pairs'
; order= OrderDomain.join order order'
; ui= UIThreadDomain.join ui callee_ui } ; ui= UIThreadDomain.join ui callee_ui }
let set_on_ui_thread ({ui} as astate) loc explain = let set_on_ui_thread ({ui} as astate) ~loc explain =
let ui = let ui =
UIThreadDomain.join ui UIThreadDomain.join ui
(AbstractDomain.Types.NonBottom (UIThreadExplanationDomain.make explain loc)) (AbstractDomain.Types.NonBottom (UIThreadExplanationDomain.make explain loc))
@ -370,9 +453,9 @@ let set_on_ui_thread ({ui} as astate) loc explain =
{astate with ui} {astate with ui}
let add_guard tenv astate guard lock ~acquire_now loc = let add_guard ~acquire_now ~procname ~loc tenv astate guard lock =
let astate = {astate with guard_map= GuardToLockMap.add_guard ~guard ~lock astate.guard_map} in let astate = {astate with guard_map= GuardToLockMap.add_guard ~guard ~lock astate.guard_map} in
if acquire_now then acquire tenv astate loc [lock] else astate if acquire_now then acquire tenv astate ~procname ~loc [lock] else astate
let remove_guard astate guard = let remove_guard astate guard =
@ -389,10 +472,14 @@ let unlock_guard astate guard =
FlatLock.get lock_opt |> Option.to_list |> release astate ) FlatLock.get lock_opt |> Option.to_list |> release astate )
let lock_guard tenv astate guard loc = let lock_guard ~procname ~loc tenv astate guard =
GuardToLockMap.find_opt guard astate.guard_map GuardToLockMap.find_opt guard astate.guard_map
|> Option.value_map ~default:astate ~f:(fun lock_opt -> |> Option.value_map ~default:astate ~f:(fun lock_opt ->
FlatLock.get lock_opt |> Option.to_list |> acquire tenv astate loc ) 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}
type summary = t type summary = t

100
infer/src/concurrency/starvationDomain.mli
Unescape View File

@ -8,58 +8,67 @@
open! IStd open! IStd
module F = Format module F = Format
(** Abstraction of a path that represents a lock, special-casing equality and comparisons (** Abstraction of a path that represents a lock, special-casing comparison
to work over type, base variable modulo this and access list *) to work over type, base variable modulo this and access list *)
module Lock : sig module Lock : sig
include ExplicitTrace.Element with type t = AccessPath.t include PrettyPrintable.PrintableOrderedType with type t = AccessPath.t
val owner_class : t -> Typ.name option val owner_class : t -> Typ.name option
(** Class of the root variable of the path representing the lock *) (** Class of the root variable of the path representing the lock *)
val equal : t -> t -> bool
val pp_locks : F.formatter -> t -> unit val pp_locks : F.formatter -> t -> unit
val describe : F.formatter -> t -> unit
end end
(** Represents the existence of a program path from the current method to the eventual acquisition
of a lock or a blocking call. Equality/comparison disregards the call trace but includes
location. *)
module Event : sig module Event : sig
type severity_t = Low | Medium | High [@@deriving compare] type severity_t = Low | Medium | High [@@deriving compare]
type event_t = type t = LockAcquire of Lock.t | MayBlock of (string * severity_t) | StrictModeCall of string
| LockAcquire of Lock.t
| MayBlock of (string * severity_t)
| StrictModeCall of string
[@@deriving compare] [@@deriving compare]
include ExplicitTrace.TraceElem with type elem_t = event_t val describe : F.formatter -> t -> unit
end
val make_trace : ?header:string -> Typ.Procname.t -> t -> Errlog.loc_trace module LockState : AbstractDomain.WithTop
(** A set of lock acquisitions with source locations and procnames. *)
module Acquisitions : sig
type t
val lock_is_held : Lock.t -> t -> bool
(** is the given lock in the set *)
end end
module EventDomain : ExplicitTrace.FiniteSet with type elt = Event.t (** An event and the currently-held locks at the time it occurred. *)
module CriticalPairElement : sig
type t = private {acquisitions: Acquisitions.t; event: Event.t}
end
(** A [CriticalPairElement] equipped with a call stack.
The intuition is that if we have a critical pair `(locks, event)` in the summary
of a method then there is a trace of that method where `event` occurs, and right
before it occurs the locks held are exactly `locks` (no over/under approximation).
We call it "critical" because the information here alone determines deadlock conditions.
*)
module CriticalPair : sig
type t = private {elem: CriticalPairElement.t; loc: Location.t; trace: CallSite.t list}
(** Represents the existence of a program path to the [first] lock being taken in the current include PrettyPrintable.PrintableOrderedType with type t := t
method or, transitively, a callee *in the same class*, and, which continues (to potentially
another class) until the [eventually] event, schematically -->first-->eventually.
It is guaranteed that during the second part of the trace (first-->eventually) the lock [first]
is not released. *)
module Order : sig
type order_t = private {first: Lock.t; eventually: Event.t}
include ExplicitTrace.TraceElem with type elem_t = order_t val get_loc : t -> Location.t
(** outermost callsite location *)
val get_earliest_lock_or_call_loc : procname:Typ.Procname.t -> t -> Location.t
(** outermost callsite location OR lock acquisition *)
val may_deadlock : t -> t -> bool val may_deadlock : t -> t -> bool
(** check if two pairs are symmetric in terms of locks, where locks are compared modulo the
variable name at the root of each path. *)
val make_trace : ?header:string -> Typ.Procname.t -> t -> Errlog.loc_trace val make_trace :
?header:string -> ?include_acquisitions:bool -> Typ.Procname.t -> t -> Errlog.loc_trace
end end
module OrderDomain : ExplicitTrace.FiniteSet with type elt = Order.t module CriticalPairs : AbstractDomain.FiniteSetS with type elt = CriticalPair.t
module LockState : AbstractDomain.WithTop
module UIThreadExplanationDomain : sig module UIThreadExplanationDomain : sig
include ExplicitTrace.TraceElem with type elem_t = string include ExplicitTrace.TraceElem with type elem_t = string
@ -74,32 +83,39 @@ module UIThreadDomain :
module GuardToLockMap : AbstractDomain.WithTop module GuardToLockMap : AbstractDomain.WithTop
type t = type t =
{ events: EventDomain.t { guard_map: GuardToLockMap.t
; guard_map: GuardToLockMap.t
; lock_state: LockState.t ; lock_state: LockState.t
; order: OrderDomain.t ; critical_pairs: CriticalPairs.t
; ui: UIThreadDomain.t } ; ui: UIThreadDomain.t }
include AbstractDomain.WithBottom with type t := t include AbstractDomain.WithBottom with type t := t
val acquire : Tenv.t -> t -> Location.t -> Lock.t list -> t val acquire : Tenv.t -> t -> procname:Typ.Procname.t -> loc:Location.t -> Lock.t list -> t
(** simultaneously acquire a number of locks, no-op if list is empty *) (** simultaneously acquire a number of locks, no-op if list is empty *)
val release : t -> Lock.t list -> t val release : t -> Lock.t list -> t
(** simultaneously release a number of locks, no-op if list is empty *) (** simultaneously release a number of locks, no-op if list is empty *)
val blocking_call : Typ.Procname.t -> Event.severity_t -> Location.t -> t -> t val blocking_call : callee:Typ.Procname.t -> Event.severity_t -> loc:Location.t -> t -> t
val strict_mode_call : Typ.Procname.t -> Location.t -> t -> t val strict_mode_call : callee:Typ.Procname.t -> loc:Location.t -> t -> t
val set_on_ui_thread : t -> Location.t -> string -> t val set_on_ui_thread : t -> loc:Location.t -> string -> t
(** set the property "runs on UI thread" to true by attaching the given explanation string as to (** 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 *) why this method is thought to do so *)
val add_guard : Tenv.t -> t -> HilExp.t -> Lock.t -> acquire_now:bool -> Location.t -> t val add_guard :
acquire_now:bool
-> procname:Typ.Procname.t
-> loc:Location.t
-> Tenv.t
-> t
-> HilExp.t
-> Lock.t
-> t
(** Install a mapping from the guard expression to the lock provided, and optionally lock it. *) (** Install a mapping from the guard expression to the lock provided, and optionally lock it. *)
val lock_guard : Tenv.t -> t -> HilExp.t -> Location.t -> t val lock_guard : procname:Typ.Procname.t -> loc:Location.t -> Tenv.t -> t -> HilExp.t -> t
(** Acquire the lock the guard was constructed with. *) (** Acquire the lock the guard was constructed with. *)
val remove_guard : t -> HilExp.t -> t val remove_guard : t -> HilExp.t -> t
@ -112,4 +128,12 @@ type summary = t
val pp_summary : F.formatter -> summary -> unit val pp_summary : F.formatter -> summary -> unit
val integrate_summary : Tenv.t -> t -> Typ.Procname.t -> Location.t -> summary -> t val integrate_summary :
Tenv.t
-> caller_summary:t
-> callee:Typ.Procname.t
-> loc:Location.t
-> callee_summary:summary
-> t
val filter_blocking_calls : t -> t

4
infer/tests/codetoanalyze/java/starvation/MasterLock.java
Unescape View File

@ -29,7 +29,7 @@ class MasterLock {
// both methods hold the master lock so cannot interleave // both methods hold the master lock so cannot interleave
// and thus cannot deadlock // and thus cannot deadlock
void FP_oneWayOk() { void oneWayOk() {
synchronized (master) { synchronized (master) {
synchronized (x) { synchronized (x) {
synchronized (y) { synchronized (y) {
@ -38,7 +38,7 @@ class MasterLock {
} }
} }
void FP_theOtherWayOk() { void theOtherWayOk() {
synchronized (master) { synchronized (master) {
synchronized (y) { synchronized (y) {
synchronized (x) { synchronized (x) {

4
infer/tests/codetoanalyze/java/starvation/issues.exp
Unescape View File

@ -25,8 +25,6 @@ codetoanalyze/java/starvation/LocklessTests.java, LocklessTestsB.locklessMethod(
codetoanalyze/java/starvation/LocklessTests.java, LocklessTestsC.locklessMethod():void, 52, LOCKLESS_VIOLATION, no_bucket, ERROR, [`void LocklessTestsC.locklessMethod()`,Method call: `void LocklessTestsC.takeLock()`, locks `this` in `class LocklessTestsC`] codetoanalyze/java/starvation/LocklessTests.java, LocklessTestsC.locklessMethod():void, 52, LOCKLESS_VIOLATION, no_bucket, ERROR, [`void LocklessTestsC.locklessMethod()`,Method call: `void LocklessTestsC.takeLock()`, locks `this` in `class LocklessTestsC`]
codetoanalyze/java/starvation/MainThreadTest.java, AnnotatedClass.callTransactBad(MainThreadTest):void, 30, STARVATION, no_bucket, ERROR, [`void AnnotatedClass.callTransactBad(MainThreadTest)`,Method call: `void MainThreadTest.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void AnnotatedClass.callTransactBad(MainThreadTest)`,class `AnnotatedClass` is annotated `UiThread`] codetoanalyze/java/starvation/MainThreadTest.java, AnnotatedClass.callTransactBad(MainThreadTest):void, 30, STARVATION, no_bucket, ERROR, [`void AnnotatedClass.callTransactBad(MainThreadTest)`,Method call: `void MainThreadTest.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void AnnotatedClass.callTransactBad(MainThreadTest)`,class `AnnotatedClass` is annotated `UiThread`]
codetoanalyze/java/starvation/MainThreadTest.java, MainThreadTest.callTransactBad():void, 23, STARVATION, no_bucket, ERROR, [`void MainThreadTest.callTransactBad()`,Method call: `void MainThreadTest.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void MainThreadTest.callTransactBad()`,`void MainThreadTest.callTransactBad()` is annotated `UiThread`] codetoanalyze/java/starvation/MainThreadTest.java, MainThreadTest.callTransactBad():void, 23, STARVATION, no_bucket, ERROR, [`void MainThreadTest.callTransactBad()`,Method call: `void MainThreadTest.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void MainThreadTest.callTransactBad()`,`void MainThreadTest.callTransactBad()` is annotated `UiThread`]
codetoanalyze/java/starvation/MasterLock.java, MasterLock.FP_oneWayOk():void, 34, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MasterLock.FP_oneWayOk()`, locks `this.x` in `class MasterLock`, locks `this.y` in `class MasterLock`,[Trace 2] `void MasterLock.FP_theOtherWayOk()`, locks `this.y` in `class MasterLock`, locks `this.x` in `class MasterLock`]
codetoanalyze/java/starvation/MasterLock.java, MasterLock.FP_theOtherWayOk():void, 43, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MasterLock.FP_theOtherWayOk()`, locks `this.y` in `class MasterLock`, locks `this.x` in `class MasterLock`,[Trace 2] `void MasterLock.FP_oneWayOk()`, locks `this.x` in `class MasterLock`, locks `this.y` in `class MasterLock`]
codetoanalyze/java/starvation/MasterLock.java, MasterLock.oneWayBad():void, 14, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MasterLock.oneWayBad()`, locks `this.a` in `class MasterLock`, locks `this.b` in `class MasterLock`,[Trace 2] `void MasterLock.theOtherWayBad()`, locks `this.b` in `class MasterLock`, locks `this.a` in `class MasterLock`] codetoanalyze/java/starvation/MasterLock.java, MasterLock.oneWayBad():void, 14, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MasterLock.oneWayBad()`, locks `this.a` in `class MasterLock`, locks `this.b` in `class MasterLock`,[Trace 2] `void MasterLock.theOtherWayBad()`, locks `this.b` in `class MasterLock`, locks `this.a` in `class MasterLock`]
codetoanalyze/java/starvation/MasterLock.java, MasterLock.theOtherWayBad():void, 22, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MasterLock.theOtherWayBad()`, locks `this.b` in `class MasterLock`, locks `this.a` in `class MasterLock`,[Trace 2] `void MasterLock.oneWayBad()`, locks `this.a` in `class MasterLock`, locks `this.b` in `class MasterLock`] codetoanalyze/java/starvation/MasterLock.java, MasterLock.theOtherWayBad():void, 22, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MasterLock.theOtherWayBad()`, locks `this.b` in `class MasterLock`, locks `this.a` in `class MasterLock`,[Trace 2] `void MasterLock.oneWayBad()`, locks `this.a` in `class MasterLock`, locks `this.b` in `class MasterLock`]
codetoanalyze/java/starvation/MyActivity.java, MyActivity.onCreate(android.os.Bundle):void, 28, STARVATION, no_bucket, ERROR, [`void MyActivity.onCreate(Bundle)`,Method call: `void MyActivity.bad()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void MyActivity.onCreate(Bundle)`,`void MyActivity.onCreate(Bundle)` is a standard UI-thread method] codetoanalyze/java/starvation/MyActivity.java, MyActivity.onCreate(android.os.Bundle):void, 28, STARVATION, no_bucket, ERROR, [`void MyActivity.onCreate(Bundle)`,Method call: `void MyActivity.bad()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void MyActivity.onCreate(Bundle)`,`void MyActivity.onCreate(Bundle)` is a standard UI-thread method]
@ -38,7 +36,7 @@ codetoanalyze/java/starvation/MyActivity.java, MyActivity.onStart():void, 33, ST
codetoanalyze/java/starvation/MyActivity.java, MyActivity.onStop():void, 53, STARVATION, no_bucket, ERROR, [`void MyActivity.onStop()`,Method call: `void MyActivity.bad()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void MyActivity.onStop()`,`void MyActivity.onStop()` is a standard UI-thread method] codetoanalyze/java/starvation/MyActivity.java, MyActivity.onStop():void, 53, STARVATION, no_bucket, ERROR, [`void MyActivity.onStop()`,Method call: `void MyActivity.bad()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void MyActivity.onStop()`,`void MyActivity.onStop()` is a standard UI-thread method]
codetoanalyze/java/starvation/NonBlk.java, NonBlk.deadlockABBad():void, 33, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void NonBlk.deadlockABBad()`, locks `this` in `class NonBlk`, locks `this.future` in `class NonBlk`,[Trace 2] `void NonBlk.deadlockBABad()`, locks `this.future` in `class NonBlk`, locks `this` in `class NonBlk`] codetoanalyze/java/starvation/NonBlk.java, NonBlk.deadlockABBad():void, 33, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void NonBlk.deadlockABBad()`, locks `this` in `class NonBlk`, locks `this.future` in `class NonBlk`,[Trace 2] `void NonBlk.deadlockBABad()`, locks `this.future` in `class NonBlk`, locks `this` in `class NonBlk`]
codetoanalyze/java/starvation/NonBlk.java, NonBlk.deadlockBABad():void, 40, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void NonBlk.deadlockBABad()`, locks `this.future` in `class NonBlk`, locks `this` in `class NonBlk`,[Trace 2] `void NonBlk.deadlockABBad()`, locks `this` in `class NonBlk`, locks `this.future` in `class NonBlk`] codetoanalyze/java/starvation/NonBlk.java, NonBlk.deadlockBABad():void, 40, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void NonBlk.deadlockBABad()`, locks `this.future` in `class NonBlk`, locks `this` in `class NonBlk`,[Trace 2] `void NonBlk.deadlockABBad()`, locks `this` in `class NonBlk`, locks `this.future` in `class NonBlk`]
codetoanalyze/java/starvation/ObjWait.java, ObjWait.indirectWaitOnMainWithoutTimeoutBad():void, 46, STARVATION, no_bucket, ERROR, [[Trace 1] `void ObjWait.indirectWaitOnMainWithoutTimeoutBad()`, locks `this.lock` in `class ObjWait`,[Trace 2] `void ObjWait.lockAndWaitOnAnyWithoutTimeoutBad()`, locks `this.lock` in `class ObjWait`,calls `void Object.wait()`,[Trace 1 on UI thread] `void ObjWait.indirectWaitOnMainWithoutTimeoutBad()`,`void ObjWait.indirectWaitOnMainWithoutTimeoutBad()` is annotated `UiThread`] codetoanalyze/java/starvation/ObjWait.java, ObjWait.indirectWaitOnMainWithoutTimeoutBad():void, 46, STARVATION, no_bucket, ERROR, [[Trace 1] `void ObjWait.indirectWaitOnMainWithoutTimeoutBad()`, locks `this.lock` in `class ObjWait`,[Trace 2] `void ObjWait.lockAndWaitOnAnyWithoutTimeoutBad()`, locks `this.lock` in `class ObjWait`, locks `this.x` in `class ObjWait`,calls `void Object.wait()`,[Trace 1 on UI thread] `void ObjWait.indirectWaitOnMainWithoutTimeoutBad()`,`void ObjWait.indirectWaitOnMainWithoutTimeoutBad()` is annotated `UiThread`]
codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithExcessiveTimeout1Bad():void, 31, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithExcessiveTimeout1Bad()`,calls `void Object.wait(long)`,[Trace on UI thread] `void ObjWait.waitOnMainWithExcessiveTimeout1Bad()`,`void ObjWait.waitOnMainWithExcessiveTimeout1Bad()` is annotated `UiThread`] codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithExcessiveTimeout1Bad():void, 31, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithExcessiveTimeout1Bad()`,calls `void Object.wait(long)`,[Trace on UI thread] `void ObjWait.waitOnMainWithExcessiveTimeout1Bad()`,`void ObjWait.waitOnMainWithExcessiveTimeout1Bad()` is annotated `UiThread`]
codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithExcessiveTimeout2Bad():void, 38, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithExcessiveTimeout2Bad()`,calls `void Object.wait(long,int)`,[Trace on UI thread] `void ObjWait.waitOnMainWithExcessiveTimeout2Bad()`,`void ObjWait.waitOnMainWithExcessiveTimeout2Bad()` is annotated `UiThread`] codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithExcessiveTimeout2Bad():void, 38, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithExcessiveTimeout2Bad()`,calls `void Object.wait(long,int)`,[Trace on UI thread] `void ObjWait.waitOnMainWithExcessiveTimeout2Bad()`,`void ObjWait.waitOnMainWithExcessiveTimeout2Bad()` is annotated `UiThread`]
codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithoutTimeoutBad():void, 24, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithoutTimeoutBad()`,calls `void Object.wait()`,[Trace on UI thread] `void ObjWait.waitOnMainWithoutTimeoutBad()`,`void ObjWait.waitOnMainWithoutTimeoutBad()` is annotated `UiThread`] codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithoutTimeoutBad():void, 24, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithoutTimeoutBad()`,calls `void Object.wait()`,[Trace on UI thread] `void ObjWait.waitOnMainWithoutTimeoutBad()`,`void ObjWait.waitOnMainWithoutTimeoutBad()` is annotated `UiThread`]

Write Preview
Loading…
Cancel
Save