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

Revert again.

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D8395058

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

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

@ -46,16 +46,6 @@ 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
@ -103,21 +93,13 @@ 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 ->
let caller = Procdesc.get_proc_name pdesc in match Models.may_block tenv callee actuals with
match Models.may_block tenv callee actuals with | Some sev ->
| Some sev -> let caller = Procdesc.get_proc_name pdesc in
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:(fun summary -> |> Option.value_map ~default:astate ~f:(Domain.integrate_summary astate callee loc) )
(* 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
@ -166,7 +148,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 {elem= {eventually= {elem= MayBlock _}}} -> false | _ -> true) (function {eventually= {elem= MayBlock _}} -> false | _ -> true)
order } order }
else Fn.id else Fn.id
in in
@ -174,22 +156,15 @@ 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 fold_nonprivate_summaries (tenv, current_pdesc) get_proc_desc clazz ~init ~f = let get_summaries_of_methods_in_class tenv clazz =
let tstruct_opt = Tenv.lookup tenv clazz in
let methods = let methods =
Tenv.lookup tenv clazz Option.value_map tstruct_opt ~default:[] ~f:(fun tstruct -> tstruct.Typ.Struct.methods)
|> 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
List.fold methods ~init ~f let summaries = List.rev_filter_map methods ~f:Ondemand.analyze_proc_name in
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 *)
@ -247,7 +222,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 report(s) on the same line suppressed." message Printf.sprintf "%s %d more starvation 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
@ -270,28 +245,29 @@ 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.elem.first, current_elem.Order.elem.eventually.elem) with match (current_elem.Order.first, current_elem.Order.eventually) with
| _, MayBlock _ -> | {Event.elem= MayBlock _}, _ | _, {Event.elem= 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
| ((Var.LogicalVar _, _), []), _ -> | {Event.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 *)
true true
| ((Var.LogicalVar _, _), _ :: _), _ | _, LockAcquire ((Var.LogicalVar _, _), _) -> | {Event.elem= 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
| ((_, typ1), _), LockAcquire ((_, typ2), _) -> | {Event.elem= LockAcquire ((_, typ1), _)}, {Event.elem= 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.Order.eventually.Event.loc
endpoint_elem.Order.elem.eventually.Event.loc endpoint_elem.Order.eventually.Event.loc
< 0 < 0
@ -302,29 +278,9 @@ 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 env get_proc_desc {StarvationDomain.order; ui} report_map' = let report_deadlocks tenv current_pdesc {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
@ -333,15 +289,15 @@ let report_deadlocks env get_proc_desc {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.elem.eventually.elem, elem.Order.elem.eventually.elem) with match (current_elem.Order.eventually, elem.Order.eventually) with
| LockAcquire _, LockAcquire _ -> | {Event.elem= LockAcquire _}, {Event.elem= 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 pp_thread (current_pname, current_elem) current_pname Order.pp current_elem
(MF.wrap_monospaced Typ.Procname.pp) (MF.wrap_monospaced Typ.Procname.pp)
endpoint_pname pp_thread (endpoint_pname, elem) endpoint_pname Order.pp 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
@ -352,16 +308,17 @@ let report_deadlocks env get_proc_desc {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.Order.elem.eventually.elem with match elem with
| MayBlock _ -> | {Order.eventually= {Event.elem= Event.MayBlock _}} ->
report_map report_map
| LockAcquire endpoint_lock -> | {Order.eventually= {Event.elem= Event.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 *)
fold_nonprivate_summaries env get_proc_desc endpoint_class ~init:report_map ~f: List.fold endpoint_summaries ~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
@ -372,14 +329,13 @@ let report_deadlocks env get_proc_desc {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 env get_proc_desc {StarvationDomain.events; ui} report_map' = let report_starvation tenv current_pdesc {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 =
let lock = endpoint_elem.Order.elem.first in match (endpoint_elem.Order.first, endpoint_elem.Order.eventually) with
match endpoint_elem.Order.elem.eventually.elem with | {Event.elem= Event.LockAcquire lock}, {Event.elem= Event.MayBlock (block_descr, sev)}
| MayBlock (block_descr, sev) when Lock.equal current_lock lock -> 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 \
@ -397,22 +353,23 @@ let report_starvation env get_proc_desc {StarvationDomain.events; ui} report_map
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
| MayBlock (_, sev) -> | Event.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 event current_pname ui_explain Event.pp_no_trace 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
| LockAcquire endpoint_lock -> | Event.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 *)
fold_nonprivate_summaries env get_proc_desc endpoint_class ~init:report_map ~f: List.fold endpoint_summaries ~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
@ -428,14 +385,13 @@ let report_starvation env get_proc_desc {StarvationDomain.events; ui} report_map
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; get_proc_desc; exe_env} = let reporting {Callbacks.procedures; exe_env} =
let report_procedure ((_, proc_desc) as env) = let report_procedure (tenv, proc_desc) =
die_if_not_java proc_desc ; die_if_not_java proc_desc ;
if Procdesc.get_access proc_desc <> PredSymb.Private then Payload.read proc_desc (Procdesc.get_proc_name proc_desc)
Payload.read proc_desc (Procdesc.get_proc_name proc_desc) |> Option.iter ~f:(fun summary ->
|> Option.iter ~f:(fun summary -> report_deadlocks tenv proc_desc summary ReportMap.empty
report_deadlocks env get_proc_desc summary ReportMap.empty |> report_starvation tenv proc_desc summary |> ReportMap.log )
|> 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,6 +6,7 @@
*) *)
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
@ -56,13 +57,17 @@ 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 : ?nesting:int -> t -> Errlog.loc_trace val make_loc_trace : 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) :
@ -73,15 +78,25 @@ 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 fmt {elem; loc} = F.fprintf fmt "%a at %a" Elem.pp elem Location.pp loc let pp_no_trace 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 ?(nesting= 0) e = let make_loc_trace e =
let call_trace, nesting = let call_trace, nesting =
List.fold e.trace ~init:([], nesting) ~f:(fun (tr, ns) callsite -> List.fold e.trace ~init:([], 0) ~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)
@ -96,6 +111,13 @@ 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
@ -113,6 +135,16 @@ 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 =
@ -124,14 +156,6 @@ 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
@ -142,30 +166,29 @@ module EventDomain = struct
end end
module Order = struct module Order = struct
type order_t = {first: Lock.t; eventually: Event.t} [@@deriving compare] type t = {first: Event.t; eventually: Event.t} [@@deriving compare]
module E = struct let pp fmt {first; eventually} =
type t = order_t F.fprintf fmt "first %a, and before releasing it, %a" Event.pp first Event.pp eventually
let compare = compare_order_t
let pp fmt {first} = Lock.pp fmt first let may_deadlock {first; eventually} {first= first'; eventually= eventually'} =
end Event.locks_equal_modulo_base first eventually'
&& Event.locks_equal_modulo_base first' eventually
include MakeTraceElem (E)
let may_deadlock {elem= {first; eventually}} {elem= {first= first'; eventually= eventually'}} = let make first eventually =
match (eventually.elem, eventually'.elem) with if not (Event.is_lock_event first) then L.(die InternalError) "Expected a lock elem first." ;
| LockAcquire e, LockAcquire e' -> {first; eventually}
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 ?(nesting= 0) ({elem= {eventually}} as order) = let make_loc_trace {first; eventually} =
let first_trace = make_loc_trace ~nesting order in let first_trace = Event.make_loc_trace first in
let first_nesting = List.length first_trace in let eventually_trace = Event.make_loc_trace eventually in
let eventually_trace = Event.make_loc_trace ~nesting:first_nesting eventually in
first_trace @ eventually_trace first_trace @ eventually_trace
@ -274,13 +297,10 @@ 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 f = let add_first_and_eventually acc first =
match f.Event.elem with (* never add a pair of the form (a,a) -- should never happen due to the check above *)
| LockAcquire first -> let elem = Order.make first event in
let elem = Order.make {first; eventually= event} f.Event.loc in OrderDomain.add elem acc
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
@ -306,18 +326,10 @@ 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 filtered_events = let order' = EventDomain.fold (add_order_pairs lock_state) callee_events callee_order in
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 filtered_events events= EventDomain.join events callee_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,54 +19,41 @@ module Lock : sig
val equal : t -> t -> bool val equal : t -> t -> bool
end end
module type TraceElem = sig (** Event type. Equality/comparison disregards the call trace but includes location. *)
type elem_t 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]
(** An [elem] which occured [loc], after the chain of procedure calls in [trace] *) type t = private {elem: event_t; loc: Location.t; trace: CallSite.t list}
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 make : elem_t -> Location.t -> t val pp_no_trace : F.formatter -> t -> unit
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 the existence of a program path to the [first] lock being taken in the current (** Represents either
method or, transitively, a callee *in the same class*, and, which continues (to potentially - the existence of a program path from the current method to the eventual acquisition of a lock
another class) until the [eventually] event, schematically -->first-->eventually. ("eventually"), or,
It is guaranteed that during the second part of the trace (first-->eventually) the lock [first] - the "first" lock being taken *in the current method* and, before its release, the eventual
is not released. *) acquisition of "eventually" *)
module Order : sig module Order : sig
type order_t = private {first: Lock.t; eventually: Event.t} type t = private {first: Event.t; eventually: Event.t}
include TraceElem with type elem_t = order_t include PrettyPrintable.PrintableOrderedType with type t := 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

@ -1,61 +0,0 @@
/*
* 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,9 +26,6 @@ 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