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

[starvation] improve deadlock reports

Browse Source 
Summary:
The deadlock reports (the actual string) were too low level, in order to avoid bug hash clashes. Now that we deduplicate this is less of an issue, so it's an opportunity to improve readability.

```
      Potential deadlock.
    Trace 1 (starts at `void Interproc.interproc1Bad(InterprocA)`) first locks `this` in class `Interproc*` (line 9 in `void Interproc.interproc1Bad(InterprocA)`) and then locks `b` in class `InterprocA*` (line 14 in `void Interproc.interproc2Bad(InterprocA)`).
    Trace 2 (starts at `void InterprocA.interproc1Bad(Interproc)`), first locks `this` in class `InterprocA*` (line 37 in `void InterprocA.interproc1Bad(Interproc)`) and then locks `d` in class `Interproc*` (line 42 in `void InterprocA.interproc2Bad(Interproc)`).
```

Reviewed By: mbouaziz

Differential Revision: D8394978

fbshipit-source-id: 671ccb0
master
Nikos Gorogiannis 7 years ago committed by Facebook Github Bot
parent db17b13f6a
commit d13b845434
5 changed files with 233 additions and 124 deletions
Show Stats Download Patch File Download Diff File

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

@ -46,6 +46,16 @@ let lock_of_class class_id =
AccessPath.of_id ident typ' AccessPath.of_id ident typ'
let is_call_to_superclass tenv ~caller ~callee =
match (caller, callee) with
| Typ.Procname.Java caller_method, Typ.Procname.Java callee_method ->
let caller_type = Typ.Procname.Java.get_class_type_name caller_method in
let callee_type = Typ.Procname.Java.get_class_type_name callee_method in
PatternMatch.is_subtype tenv caller_type callee_type
| _ ->
false
module TransferFunctions (CFG : ProcCfg.S) = struct module TransferFunctions (CFG : ProcCfg.S) = struct
module CFG = CFG module CFG = CFG
module Domain = StarvationDomain module Domain = StarvationDomain
@ -93,13 +103,21 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let explanation = F.asprintf "it calls %a" (MF.wrap_monospaced Typ.Procname.pp) callee in let explanation = F.asprintf "it calls %a" (MF.wrap_monospaced Typ.Procname.pp) callee in
Domain.set_on_ui_thread astate explanation Domain.set_on_ui_thread astate explanation
| NoEffect -> | NoEffect ->
match Models.may_block tenv callee actuals with let caller = Procdesc.get_proc_name pdesc in
| Some sev -> match Models.may_block tenv callee actuals with
let caller = Procdesc.get_proc_name pdesc in | Some sev ->
Domain.blocking_call ~caller ~callee sev loc astate Domain.blocking_call ~caller ~callee sev loc astate
| None -> | None ->
Payload.read pdesc callee Payload.read pdesc callee
|> Option.value_map ~default:astate ~f:(Domain.integrate_summary astate callee loc) ) |> Option.value_map ~default:astate ~f:(fun summary ->
(* if not calling a method in a superclass then set order to empty
to avoid blaming a caller in one class for deadlock/starvation
happening in the callee class *)
let summary =
if is_call_to_superclass tenv ~caller ~callee then summary
else {summary with Domain.order= Domain.OrderDomain.empty}
in
Domain.integrate_summary astate callee loc summary ) )
| _ -> | _ ->
astate astate
@ -148,7 +166,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
events= EventDomain.filter (function {elem= MayBlock _} -> false | _ -> true) events events= EventDomain.filter (function {elem= MayBlock _} -> false | _ -> true) events
; order= ; order=
OrderDomain.filter OrderDomain.filter
(function {eventually= {elem= MayBlock _}} -> false | _ -> true) (function {elem= {eventually= {elem= MayBlock _}}} -> false | _ -> true)
order } order }
else Fn.id else Fn.id
in in
@ -156,15 +174,22 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
|> Option.value_map ~default:summary ~f:(fun astate -> Payload.update_summary astate summary) |> Option.value_map ~default:summary ~f:(fun astate -> Payload.update_summary astate summary)
let get_summaries_of_methods_in_class tenv clazz = let fold_nonprivate_summaries (tenv, current_pdesc) get_proc_desc clazz ~init ~f =
let tstruct_opt = Tenv.lookup tenv clazz in
let methods = let methods =
Option.value_map tstruct_opt ~default:[] ~f:(fun tstruct -> tstruct.Typ.Struct.methods) Tenv.lookup tenv clazz
|> Option.value_map ~default:[] ~f:(fun tstruct -> tstruct.Typ.Struct.methods)
in
let f acc mthd =
get_proc_desc mthd
|> Option.value_map ~default:acc ~f:(fun other_pdesc ->
match Procdesc.get_access other_pdesc with
| PredSymb.Private ->
acc
| _ ->
Payload.read current_pdesc mthd |> Option.map ~f:(fun payload -> (mthd, payload))
|> Option.value_map ~default:acc ~f:(f acc) )
in in
let summaries = List.rev_filter_map methods ~f:Ondemand.analyze_proc_name in List.fold methods ~init ~f
List.rev_filter_map summaries ~f:(fun sum ->
Option.map sum.Summary.payloads.Payloads.starvation ~f:(fun p ->
(Summary.get_proc_name sum, p) ) )
(** per-procedure report map, which takes care of deduplication *) (** per-procedure report map, which takes care of deduplication *)
@ -222,7 +247,7 @@ end = struct
let mk_deduped_report num_of_reports ({message} as report) = let mk_deduped_report num_of_reports ({message} as report) =
{ report with { report with
message= message=
Printf.sprintf "%s %d more starvation report(s) on the same line suppressed." message Printf.sprintf "%s %d more report(s) on the same line suppressed." message
(num_of_reports - 1) } (num_of_reports - 1) }
in in
let log_loc_reports issuetype compare loc = function let log_loc_reports issuetype compare loc = function
@ -245,29 +270,28 @@ end
let should_report_deadlock_on_current_proc current_elem endpoint_elem = let should_report_deadlock_on_current_proc current_elem endpoint_elem =
let open StarvationDomain in let open StarvationDomain in
match (current_elem.Order.first, current_elem.Order.eventually) with match (current_elem.Order.elem.first, current_elem.Order.elem.eventually.elem) with
| {Event.elem= MayBlock _}, _ | _, {Event.elem= MayBlock _} -> | _, MayBlock _ ->
(* 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" Order.pp current_elem
| {Event.elem= LockAcquire ((Var.LogicalVar _, _), [])}, _ -> | ((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 *)
true true
| {Event.elem= LockAcquire ((Var.LogicalVar _, _), _ :: _)}, _ | ((Var.LogicalVar _, _), _ :: _), _ | _, LockAcquire ((Var.LogicalVar _, _), _) ->
| _, {Event.elem= 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 @." Order.pp
current_elem current_elem
| {Event.elem= LockAcquire ((_, typ1), _)}, {Event.elem= LockAcquire ((_, typ2), _)} -> | ((_, 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.eventually.Event.loc Location.compare current_elem.Order.elem.eventually.Event.loc
endpoint_elem.Order.eventually.Event.loc endpoint_elem.Order.elem.eventually.Event.loc
< 0 < 0
@ -278,9 +302,29 @@ let should_report_deadlock_on_current_proc current_elem endpoint_elem =
inner class but this is no longer obvious in the path, because of nested-class path normalisation. 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 tenv current_pdesc {StarvationDomain.order; ui} report_map' = let report_deadlocks env get_proc_desc {StarvationDomain.order; ui} report_map' =
let open StarvationDomain in let open StarvationDomain in
let tenv, current_pdesc = env in
let current_pname = Procdesc.get_proc_name current_pdesc in let current_pname = Procdesc.get_proc_name current_pdesc in
let pp_acquire fmt (lock, loc, pname) =
F.fprintf fmt "%a (%a in %a)" Lock.pp lock Location.pp loc
(MF.wrap_monospaced Typ.Procname.pp)
pname
in
let pp_thread fmt
( pname
, { Order.loc= loc1
; trace= trace1
; elem= {first= lock1; eventually= {elem= event; loc= loc2; trace= trace2}} } ) =
match event with
| LockAcquire lock2 ->
let pname1 = List.last trace1 |> Option.value_map ~default:pname ~f:CallSite.pname in
let pname2 = List.last trace2 |> Option.value_map ~default:pname1 ~f:CallSite.pname in
F.fprintf fmt "first %a and then %a" pp_acquire (lock1, loc1, pname1) pp_acquire
(lock2, loc2, pname2)
| _ ->
L.die InternalError "Trying to report a deadlock without two lock events."
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
@ -289,15 +333,15 @@ let report_deadlocks tenv current_pdesc {StarvationDomain.order; ui} report_map'
then report_map then report_map
else else
let () = debug "Possible deadlock:@.%a@.%a@." Order.pp current_elem Order.pp elem in let () = debug "Possible deadlock:@.%a@.%a@." Order.pp current_elem Order.pp elem in
match (current_elem.Order.eventually, elem.Order.eventually) with match (current_elem.Order.elem.eventually.elem, elem.Order.elem.eventually.elem) with
| {Event.elem= LockAcquire _}, {Event.elem= LockAcquire _} -> | LockAcquire _, LockAcquire _ ->
let error_message = let error_message =
Format.asprintf Format.asprintf
"Potential deadlock.@.Trace 1 (starts at %a), %a.@.Trace 2 (starts at %a), %a." "Potential deadlock.@.Trace 1 (starts at %a) %a.@.Trace 2 (starts at %a), %a."
(MF.wrap_monospaced Typ.Procname.pp) (MF.wrap_monospaced Typ.Procname.pp)
current_pname Order.pp current_elem current_pname pp_thread (current_pname, current_elem)
(MF.wrap_monospaced Typ.Procname.pp) (MF.wrap_monospaced Typ.Procname.pp)
endpoint_pname Order.pp elem endpoint_pname pp_thread (endpoint_pname, elem)
in in
let first_trace = Order.make_trace ~header:"[Trace 1] " current_pname current_elem in let first_trace = Order.make_trace ~header:"[Trace 1] " current_pname current_elem in
let second_trace = Order.make_trace ~header:"[Trace 2] " endpoint_pname elem in let second_trace = Order.make_trace ~header:"[Trace 2] " endpoint_pname elem in
@ -308,17 +352,16 @@ let report_deadlocks tenv current_pdesc {StarvationDomain.order; ui} 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 with match elem.Order.elem.eventually.elem with
| {Order.eventually= {Event.elem= Event.MayBlock _}} -> | MayBlock _ ->
report_map report_map
| {Order.eventually= {Event.elem= Event.LockAcquire endpoint_lock}} -> | LockAcquire endpoint_lock ->
Lock.owner_class endpoint_lock Lock.owner_class endpoint_lock
|> Option.value_map ~default:report_map ~f:(fun endpoint_class -> |> Option.value_map ~default:report_map ~f:(fun endpoint_class ->
(* get the class of the root variable of the lock in the endpoint elem (* get the class of the root variable of the lock in the endpoint elem
and retrieve all the summaries of the methods of that class *) and retrieve all the summaries of the methods of that class *)
let endpoint_summaries = get_summaries_of_methods_in_class tenv endpoint_class in
(* for each summary related to the endpoint, analyse and report on its pairs *) (* for each summary related to the endpoint, analyse and report on its pairs *)
List.fold endpoint_summaries ~init:report_map ~f: fold_nonprivate_summaries env get_proc_desc endpoint_class ~init:report_map ~f:
(fun acc (endp_pname, endpoint_summary) -> (fun acc (endp_pname, endpoint_summary) ->
let endp_order = endpoint_summary.order in let endp_order = endpoint_summary.order in
let endp_ui = endpoint_summary.ui in let endp_ui = endpoint_summary.ui in
@ -329,13 +372,14 @@ let report_deadlocks tenv current_pdesc {StarvationDomain.order; ui} report_map'
OrderDomain.fold report_on_current_elem order report_map' OrderDomain.fold report_on_current_elem order report_map'
let report_starvation tenv current_pdesc {StarvationDomain.events; ui} report_map' = let report_starvation env get_proc_desc {StarvationDomain.events; ui} report_map' =
let open StarvationDomain in let open StarvationDomain in
let tenv, current_pdesc = env in
let current_pname = Procdesc.get_proc_name current_pdesc in let current_pname = Procdesc.get_proc_name current_pdesc 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 =
match (endpoint_elem.Order.first, endpoint_elem.Order.eventually) with let lock = endpoint_elem.Order.elem.first in
| {Event.elem= Event.LockAcquire lock}, {Event.elem= Event.MayBlock (block_descr, sev)} match endpoint_elem.Order.elem.eventually.elem with
when Lock.equal current_lock lock -> | MayBlock (block_descr, sev) when Lock.equal current_lock lock ->
let error_message = let error_message =
Format.asprintf Format.asprintf
"Method %a runs on UI thread (because %s) and %a, which may be held by another thread \ "Method %a runs on UI thread (because %s) and %a, which may be held by another thread \
@ -353,23 +397,22 @@ let report_starvation tenv current_pdesc {StarvationDomain.events; ui} report_ma
in in
let report_on_current_elem ui_explain event report_map = let report_on_current_elem ui_explain event report_map =
match event.Event.elem with match event.Event.elem with
| Event.MayBlock (_, sev) -> | MayBlock (_, sev) ->
let error_message = let error_message =
Format.asprintf "Method %a runs on UI thread (because %s), and may block; %a." Format.asprintf "Method %a runs on UI thread (because %s), and may block; %a."
(MF.wrap_monospaced Typ.Procname.pp) (MF.wrap_monospaced Typ.Procname.pp)
current_pname ui_explain Event.pp_no_trace event current_pname ui_explain Event.pp event
in in
let loc = Event.get_loc event in let loc = Event.get_loc event in
let ltr = Event.make_trace current_pname event in let ltr = Event.make_trace current_pname event in
ReportMap.add_starvation tenv sev current_pdesc loc ltr error_message report_map ReportMap.add_starvation tenv sev current_pdesc loc ltr error_message report_map
| Event.LockAcquire endpoint_lock -> | LockAcquire endpoint_lock ->
Lock.owner_class endpoint_lock Lock.owner_class endpoint_lock
|> Option.value_map ~default:report_map ~f:(fun endpoint_class -> |> Option.value_map ~default:report_map ~f:(fun endpoint_class ->
(* get the class of the root variable of the lock in the endpoint elem (* get the class of the root variable of the lock in the endpoint elem
and retrieve all the summaries of the methods of that class *) and retrieve all the summaries of the methods of that class *)
let endpoint_summaries = get_summaries_of_methods_in_class tenv endpoint_class in
(* for each summary related to the endpoint, analyse and report on its pairs *) (* for each summary related to the endpoint, analyse and report on its pairs *)
List.fold endpoint_summaries ~init:report_map ~f: fold_nonprivate_summaries env get_proc_desc endpoint_class ~init:report_map ~f:
(fun acc (endpoint_pname, {order; ui}) -> (fun acc (endpoint_pname, {order; ui}) ->
(* skip methods known to run on ui thread, as they cannot run in parallel to us *) (* skip methods known to run on ui thread, as they cannot run in parallel to us *)
if UIThreadDomain.is_empty ui then if UIThreadDomain.is_empty ui then
@ -385,13 +428,14 @@ let report_starvation tenv current_pdesc {StarvationDomain.events; ui} report_ma
EventDomain.fold (report_on_current_elem ui_explain) events report_map' EventDomain.fold (report_on_current_elem ui_explain) events report_map'
let reporting {Callbacks.procedures; exe_env} = let reporting {Callbacks.procedures; get_proc_desc; exe_env} =
let report_procedure (tenv, proc_desc) = let report_procedure ((_, proc_desc) as env) =
die_if_not_java proc_desc ; die_if_not_java proc_desc ;
Payload.read proc_desc (Procdesc.get_proc_name proc_desc) if Procdesc.get_access proc_desc <> PredSymb.Private then
|> Option.iter ~f:(fun summary -> Payload.read proc_desc (Procdesc.get_proc_name proc_desc)
report_deadlocks tenv proc_desc summary ReportMap.empty |> Option.iter ~f:(fun summary ->
|> report_starvation tenv proc_desc summary |> ReportMap.log ) report_deadlocks env get_proc_desc summary ReportMap.empty
|> report_starvation env get_proc_desc summary |> ReportMap.log )
in in
List.iter procedures ~f:report_procedure ; List.iter procedures ~f:report_procedure ;
let sourcefile = exe_env.Exe_env.source_file in let sourcefile = exe_env.Exe_env.source_file in

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

@ -6,7 +6,6 @@
*) *)
open! IStd open! IStd
module F = Format module F = Format
module L = Logging
module MF = MarkupFormatter module MF = MarkupFormatter
module Lock = struct module Lock = struct
@ -57,17 +56,13 @@ module type TraceElem = sig
include PrettyPrintable.PrintableOrderedType with type t := t include PrettyPrintable.PrintableOrderedType with type t := t
val pp_no_trace : F.formatter -> t -> unit
val make : elem_t -> Location.t -> t val make : elem_t -> Location.t -> t
val get_loc : t -> Location.t val get_loc : t -> Location.t
val make_loc_trace : t -> Errlog.loc_trace val make_loc_trace : ?nesting:int -> t -> Errlog.loc_trace
val with_callsite : t -> CallSite.t -> t val with_callsite : t -> CallSite.t -> t
val make_trace : ?header:string -> Typ.Procname.t -> t -> Errlog.loc_trace
end end
module MakeTraceElem (Elem : PrettyPrintable.PrintableOrderedType) : module MakeTraceElem (Elem : PrettyPrintable.PrintableOrderedType) :
@ -78,25 +73,15 @@ struct
type t = {elem: Elem.t; loc: Location.t; trace: CallSite.t list [@compare.ignore]} type t = {elem: Elem.t; loc: Location.t; trace: CallSite.t list [@compare.ignore]}
[@@deriving compare] [@@deriving compare]
let pp_no_trace fmt {elem; loc} = F.fprintf fmt "%a at %a" Elem.pp elem Location.pp loc let pp fmt {elem; loc} = F.fprintf fmt "%a at %a" Elem.pp elem Location.pp loc
let pp fmt e =
let pp_trace fmt = function
| [] ->
()
| trace ->
F.fprintf fmt " (trace: %a)" (Pp.semicolon_seq CallSite.pp) trace
in
F.fprintf fmt "%a%a" pp_no_trace e pp_trace e.trace
let make elem loc = {elem; loc; trace= []} let make elem loc = {elem; loc; trace= []}
let get_loc {loc; trace} = List.hd trace |> Option.value_map ~default:loc ~f:CallSite.loc let get_loc {loc; trace} = List.hd trace |> Option.value_map ~default:loc ~f:CallSite.loc
let make_loc_trace e = let make_loc_trace ?(nesting= 0) e =
let call_trace, nesting = let call_trace, nesting =
List.fold e.trace ~init:([], 0) ~f:(fun (tr, ns) callsite -> List.fold e.trace ~init:([], nesting) ~f:(fun (tr, ns) callsite ->
let elem_descr = let elem_descr =
F.asprintf "Method call: %a" F.asprintf "Method call: %a"
(MF.wrap_monospaced Typ.Procname.pp) (MF.wrap_monospaced Typ.Procname.pp)
@ -111,13 +96,6 @@ struct
let with_callsite elem callsite = {elem with trace= callsite :: elem.trace} let with_callsite elem callsite = {elem with trace= callsite :: elem.trace}
let make_trace ?(header= "") pname elem =
let trace = make_loc_trace elem in
let trace_descr = Format.asprintf "%s%a" header (MF.wrap_monospaced Typ.Procname.pp) pname in
let start_loc = get_loc elem in
let header_step = Errlog.make_trace_element 0 start_loc trace_descr [] in
header_step :: trace
end end
module Event = struct module Event = struct
@ -135,16 +113,6 @@ module Event = struct
F.pp_print_string fmt msg F.pp_print_string fmt msg
end) end)
let is_lock_event e = match e.elem with LockAcquire _ -> true | _ -> false
let locks_equal_modulo_base e e' =
match (e.elem, e'.elem) with
| LockAcquire lock, LockAcquire lock' ->
Lock.equal_modulo_base lock lock'
| _, _ ->
false
let make_acquire lock loc = make (LockAcquire lock) loc let make_acquire lock loc = make (LockAcquire lock) loc
let make_blocking_call ~caller ~callee sev loc = let make_blocking_call ~caller ~callee sev loc =
@ -156,6 +124,14 @@ module Event = struct
caller caller
in in
make (MayBlock (descr, sev)) loc make (MayBlock (descr, sev)) loc
let make_trace ?(header= "") pname elem =
let trace = make_loc_trace elem in
let trace_descr = Format.asprintf "%s%a" header (MF.wrap_monospaced Typ.Procname.pp) pname in
let start_loc = get_loc elem in
let header_step = Errlog.make_trace_element 0 start_loc trace_descr [] in
header_step :: trace
end end
module EventDomain = struct module EventDomain = struct
@ -166,29 +142,30 @@ module EventDomain = struct
end end
module Order = struct module Order = struct
type t = {first: Event.t; eventually: Event.t} [@@deriving compare] type order_t = {first: Lock.t; eventually: Event.t} [@@deriving compare]
let pp fmt {first; eventually} =
F.fprintf fmt "first %a, and before releasing it, %a" Event.pp first Event.pp eventually
module E = struct
type t = order_t
let may_deadlock {first; eventually} {first= first'; eventually= eventually'} = let compare = compare_order_t
Event.locks_equal_modulo_base first eventually'
&& Event.locks_equal_modulo_base first' eventually
let pp fmt {first} = Lock.pp fmt first
end
let make first eventually = include MakeTraceElem (E)
if not (Event.is_lock_event first) then L.(die InternalError) "Expected a lock elem first." ;
{first; eventually}
let may_deadlock {elem= {first; eventually}} {elem= {first= first'; eventually= eventually'}} =
match (eventually.elem, eventually'.elem) with
| LockAcquire e, LockAcquire e' ->
Lock.equal_modulo_base first e' && Lock.equal_modulo_base first' e
| _, _ ->
false
let with_callsite o callsite = {o with first= Event.with_callsite o.first callsite}
let get_loc {first} = Event.get_loc first
let make_loc_trace {first; eventually} = let make_loc_trace ?(nesting= 0) ({elem= {eventually}} as order) =
let first_trace = Event.make_loc_trace first in let first_trace = make_loc_trace ~nesting order in
let eventually_trace = Event.make_loc_trace eventually in let first_nesting = List.length first_trace in
let eventually_trace = Event.make_loc_trace ~nesting:first_nesting eventually in
first_trace @ eventually_trace first_trace @ eventually_trace
@ -297,10 +274,13 @@ let add_order_pairs lock_state event acc =
(* add no pairs whatsoever if we already hold that lock *) (* add no pairs whatsoever if we already hold that lock *)
if LockState.is_taken event lock_state then acc if LockState.is_taken event lock_state then acc
else else
let add_first_and_eventually acc first = let add_first_and_eventually acc f =
(* never add a pair of the form (a,a) -- should never happen due to the check above *) match f.Event.elem with
let elem = Order.make first event in | LockAcquire first ->
OrderDomain.add elem acc let elem = Order.make {first; eventually= event} f.Event.loc in
OrderDomain.add elem acc
| _ ->
acc
in in
LockState.fold_over_events add_first_and_eventually lock_state acc LockState.fold_over_events add_first_and_eventually lock_state acc
@ -326,10 +306,18 @@ let release ({lock_state} as astate) lock =
let integrate_summary ({lock_state; events; order; ui} as astate) callee_pname loc callee_summary = let integrate_summary ({lock_state; events; order; ui} as astate) callee_pname loc callee_summary =
let callsite = CallSite.make callee_pname loc in let callsite = CallSite.make callee_pname loc in
let callee_order = OrderDomain.with_callsite callee_summary.order callsite in let callee_order = OrderDomain.with_callsite callee_summary.order callsite in
let filtered_order =
OrderDomain.filter
(fun {elem= {eventually}} -> LockState.is_taken eventually lock_state |> not)
callee_order
in
let callee_events = EventDomain.with_callsite callee_summary.events callsite in let callee_events = EventDomain.with_callsite callee_summary.events callsite in
let order' = EventDomain.fold (add_order_pairs lock_state) callee_events callee_order in let filtered_events =
EventDomain.filter (fun e -> LockState.is_taken e lock_state |> not) callee_events
in
let order' = EventDomain.fold (add_order_pairs lock_state) filtered_events filtered_order in
{ astate with { astate with
events= EventDomain.join events callee_events events= EventDomain.join events filtered_events
; order= OrderDomain.join order order' ; order= OrderDomain.join order order'
; ui= UIThreadDomain.join ui callee_summary.ui } ; ui= UIThreadDomain.join ui callee_summary.ui }

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

@ -19,41 +19,54 @@ module Lock : sig
val equal : t -> t -> bool val equal : t -> t -> bool
end end
(** Event type. Equality/comparison disregards the call trace but includes location. *) module type TraceElem = sig
module Event : sig type elem_t
type severity_t = Low | Medium | High [@@deriving compare]
type event_t = LockAcquire of Lock.t | MayBlock of (string * severity_t) [@@deriving compare]
type t = private {elem: event_t; loc: Location.t; trace: CallSite.t list} (** An [elem] which occured [loc], after the chain of procedure calls in [trace] *)
type t = private {elem: elem_t; loc: Location.t; trace: CallSite.t list}
include PrettyPrintable.PrintableOrderedType with type t := t include PrettyPrintable.PrintableOrderedType with type t := t
val pp_no_trace : F.formatter -> t -> unit val make : elem_t -> Location.t -> t
val get_loc : t -> Location.t val get_loc : t -> Location.t
(** Starting location of the trace: this is either [loc] if [trace] is empty, or the head of [trace]. *)
val make_loc_trace : ?nesting:int -> t -> Errlog.loc_trace
val with_callsite : t -> CallSite.t -> t
(** Push given callsite onto [trace], extending the call chain by one. *)
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
type severity_t = Low | Medium | High [@@deriving compare]
type event_t = LockAcquire of Lock.t | MayBlock of (string * severity_t) [@@deriving compare]
include TraceElem with type elem_t = event_t
val make_trace : ?header:string -> Typ.Procname.t -> t -> Errlog.loc_trace val make_trace : ?header:string -> Typ.Procname.t -> t -> Errlog.loc_trace
end end
module EventDomain : module type of AbstractDomain.FiniteSet (Event) module EventDomain : module type of AbstractDomain.FiniteSet (Event)
(** Represents either (** Represents the existence of a program path to the [first] lock being taken in the current
- the existence of a program path from the current method to the eventual acquisition of a lock method or, transitively, a callee *in the same class*, and, which continues (to potentially
("eventually"), or, another class) until the [eventually] event, schematically -->first-->eventually.
- the "first" lock being taken *in the current method* and, before its release, the eventual It is guaranteed that during the second part of the trace (first-->eventually) the lock [first]
acquisition of "eventually" *) is not released. *)
module Order : sig module Order : sig
type t = private {first: Event.t; eventually: Event.t} type order_t = private {first: Lock.t; eventually: Event.t}
include PrettyPrintable.PrintableOrderedType with type t := t include TraceElem with type elem_t = order_t
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 (** check if two pairs are symmetric in terms of locks, where locks are compared modulo the
variable name at the root of each path. *) variable name at the root of each path. *)
val get_loc : t -> Location.t
val make_trace : ?header:string -> Typ.Procname.t -> t -> Errlog.loc_trace val make_trace : ?header:string -> Typ.Procname.t -> t -> Errlog.loc_trace
end end

61
infer/tests/codetoanalyze/java/starvation/PubPriv.java
Unescape View File

@ -0,0 +1,61 @@
/*
* Copyright (c) 2018-present, Facebook, Inc.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
import android.os.Binder;
import android.os.RemoteException;
import android.support.annotation.UiThread;
class PubPriv {
Binder b;
@UiThread
private void doTransactOk() throws RemoteException {
b.transact(0, null, null, 0);
}
public void transactBad() throws RemoteException {
doTransactOk();
}
public void alsoBad() throws RemoteException {
transactBad();
}
private void chainOK() throws RemoteException {
alsoBad();
}
Object lockA, lockB;
private void oneWayOk() {
synchronized(lockA) {
synchronized(lockB) {}
}
}
private void anotherWayOk() {
synchronized(lockB) {
synchronized(lockA) {}
}
}
public void callOneWayBad() {
oneWayOk();
}
public void callAnotherWayBad() {
anotherWayOk();
}
private void callOneWayOk() {
oneWayOk();
}
private void callAnotherWayOk() {
anotherWayOk();
}
}

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

@ -26,6 +26,9 @@ codetoanalyze/java/starvation/Interproc.java, void Interproc.interproc1Bad(Inter
codetoanalyze/java/starvation/Intraproc.java, void Intraproc.intraBad(IntraprocA), 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Intraproc.intraBad(IntraprocA)`,locks `this` in class `Intraproc*`,locks `o` in class `IntraprocA*`,[Trace 2] `void IntraprocA.intraBad(Intraproc)`,locks `this` in class `IntraprocA*`,locks `o` in class `Intraproc*`] codetoanalyze/java/starvation/Intraproc.java, void Intraproc.intraBad(IntraprocA), 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Intraproc.intraBad(IntraprocA)`,locks `this` in class `Intraproc*`,locks `o` in class `IntraprocA*`,[Trace 2] `void IntraprocA.intraBad(Intraproc)`,locks `this` in class `IntraprocA*`,locks `o` in class `Intraproc*`]
codetoanalyze/java/starvation/LegacySync.java, Object LegacySync.onUiThreadOpBad(), 25, STARVATION, no_bucket, ERROR, [[Trace 1] `Object LegacySync.onUiThreadOpBad()`,locks `this.LegacySync.table` in class `LegacySync*`,[Trace 2] `void LegacySync.notOnUiThreadSyncedBad()`,locks `this.LegacySync.table` in class `LegacySync*`,calls `Object Future.get()` from `void LegacySync.notOnUiThreadSyncedBad()`] codetoanalyze/java/starvation/LegacySync.java, Object LegacySync.onUiThreadOpBad(), 25, STARVATION, no_bucket, ERROR, [[Trace 1] `Object LegacySync.onUiThreadOpBad()`,locks `this.LegacySync.table` in class `LegacySync*`,[Trace 2] `void LegacySync.notOnUiThreadSyncedBad()`,locks `this.LegacySync.table` in class `LegacySync*`,calls `Object Future.get()` from `void LegacySync.notOnUiThreadSyncedBad()`]
codetoanalyze/java/starvation/NonBlk.java, void NonBlk.deadlockABBad(), 34, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void NonBlk.deadlockABBad()`,locks `this` in class `NonBlk*`,locks `this.NonBlk.future` in class `NonBlk*`,[Trace 2] `void NonBlk.deadlockBABad()`,locks `this.NonBlk.future` in class `NonBlk*`,locks `this` in class `NonBlk*`] codetoanalyze/java/starvation/NonBlk.java, void NonBlk.deadlockABBad(), 34, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void NonBlk.deadlockABBad()`,locks `this` in class `NonBlk*`,locks `this.NonBlk.future` in class `NonBlk*`,[Trace 2] `void NonBlk.deadlockBABad()`,locks `this.NonBlk.future` in class `NonBlk*`,locks `this` in class `NonBlk*`]
codetoanalyze/java/starvation/PubPriv.java, void PubPriv.alsoBad(), 25, STARVATION, no_bucket, ERROR, [`void PubPriv.alsoBad()`,Method call: `void PubPriv.transactBad()`,Method call: `void PubPriv.doTransactOk()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)` from `void PubPriv.doTransactOk()`]
codetoanalyze/java/starvation/PubPriv.java, void PubPriv.callOneWayBad(), 47, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void PubPriv.callOneWayBad()`,Method call: `void PubPriv.oneWayOk()`,locks `this.PubPriv.lockA` in class `PubPriv*`,locks `this.PubPriv.lockB` in class `PubPriv*`,[Trace 2] `void PubPriv.callAnotherWayBad()`,Method call: `void PubPriv.anotherWayOk()`,locks `this.PubPriv.lockB` in class `PubPriv*`,locks `this.PubPriv.lockA` in class `PubPriv*`]
codetoanalyze/java/starvation/PubPriv.java, void PubPriv.transactBad(), 21, STARVATION, no_bucket, ERROR, [`void PubPriv.transactBad()`,Method call: `void PubPriv.doTransactOk()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)` from `void PubPriv.doTransactOk()`]
codetoanalyze/java/starvation/ServiceOnUIThread.java, IBinder ServiceOnUIThread.onBind(Intent), 19, STARVATION, no_bucket, ERROR, [`IBinder ServiceOnUIThread.onBind(Intent)`,Method call: `void ServiceOnUIThread.transactBad()`,calls `boolean IBinder.transact(int,Parcel,Parcel,int)` from `void ServiceOnUIThread.transactBad()`] codetoanalyze/java/starvation/ServiceOnUIThread.java, IBinder ServiceOnUIThread.onBind(Intent), 19, STARVATION, no_bucket, ERROR, [`IBinder ServiceOnUIThread.onBind(Intent)`,Method call: `void ServiceOnUIThread.transactBad()`,calls `boolean IBinder.transact(int,Parcel,Parcel,int)` from `void ServiceOnUIThread.transactBad()`]
codetoanalyze/java/starvation/ServiceOnUIThread.java, void ServiceOnUIThread.transactBad(), 25, STARVATION, no_bucket, ERROR, [`void ServiceOnUIThread.transactBad()`,calls `boolean IBinder.transact(int,Parcel,Parcel,int)` from `void ServiceOnUIThread.transactBad()`] codetoanalyze/java/starvation/ServiceOnUIThread.java, void ServiceOnUIThread.transactBad(), 25, STARVATION, no_bucket, ERROR, [`void ServiceOnUIThread.transactBad()`,calls `boolean IBinder.transact(int,Parcel,Parcel,int)` from `void ServiceOnUIThread.transactBad()`]
codetoanalyze/java/starvation/StaticLock.java, void StaticLock.lockOtherClassOneWayBad(), 23, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void StaticLock.lockOtherClassOneWayBad()`,locks `StaticLock$0` in class `java.lang.Class*`,locks `this` in class `StaticLock*`,[Trace 2] `void StaticLock.lockOtherClassAnotherWayNad()`,locks `this` in class `StaticLock*`,Method call: `void StaticLock.staticSynced()`,locks `StaticLock$0` in class `java.lang.Class*`] codetoanalyze/java/starvation/StaticLock.java, void StaticLock.lockOtherClassOneWayBad(), 23, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void StaticLock.lockOtherClassOneWayBad()`,locks `StaticLock$0` in class `java.lang.Class*`,locks `this` in class `StaticLock*`,[Trace 2] `void StaticLock.lockOtherClassAnotherWayNad()`,locks `this` in class `StaticLock*`,Method call: `void StaticLock.staticSynced()`,locks `StaticLock$0` in class `java.lang.Class*`]

Write Preview
Loading…
Cancel
Save