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

[starvation] add infrastructure for blocking events other than lock acquisition

Browse Source 
Reviewed By: ddino

Differential Revision: D7428995

fbshipit-source-id: 5e1185d
master
Nikos Gorogiannis 7 years ago committed by Facebook Github Bot
parent 705a2f97b2
commit 0130c09dfc
5 changed files with 126 additions and 66 deletions
Show Stats Download Patch File Download Diff File

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

@ -119,19 +119,22 @@ let should_report_if_same_class _ = true
not (Typ.Name.equal first_class eventually_class) || LockEvent.compare b a >= 0 not (Typ.Name.equal first_class eventually_class) || LockEvent.compare b a >= 0
) ) )) *) ) ) )) *)
let make_loc_trace pname trace_id start_loc elem = let make_trace_with_header ?(header= "") elem start_loc pname =
let open StarvationDomain in let trace = StarvationDomain.LockOrder.make_loc_trace elem in
let header = Printf.sprintf "[Trace %d]" trace_id in
let trace = LockOrder.make_loc_trace elem in
let first_step = List.hd_exn trace in let first_step = List.hd_exn trace in
if Location.equal first_step.Errlog.lt_loc start_loc then if Location.equal first_step.Errlog.lt_loc start_loc then
let trace_descr = header ^ " " ^ first_step.Errlog.lt_description in let trace_descr = header ^ first_step.Errlog.lt_description in
Errlog.make_trace_element 0 start_loc trace_descr [] :: List.tl_exn trace Errlog.make_trace_element 0 start_loc trace_descr [] :: List.tl_exn trace
else else
let trace_descr = Format.asprintf "%s Method start: %a" header Typ.Procname.pp pname in let trace_descr = Format.asprintf "%sMethod start: %a" header Typ.Procname.pp pname in
Errlog.make_trace_element 0 start_loc trace_descr [] :: trace Errlog.make_trace_element 0 start_loc trace_descr [] :: trace
let make_loc_trace pname trace_id start_loc elem =
let header = Printf.sprintf "[Trace %d] " trace_id in
make_trace_with_header ~header elem start_loc pname
let get_summary caller_pdesc callee_pdesc = let get_summary caller_pdesc callee_pdesc =
Summary.read_summary caller_pdesc (Procdesc.get_proc_name callee_pdesc) Summary.read_summary caller_pdesc (Procdesc.get_proc_name callee_pdesc)
|> Option.map ~f:(fun summary -> (callee_pdesc, summary)) |> Option.map ~f:(fun summary -> (callee_pdesc, summary))
@ -146,18 +149,25 @@ let report_deadlocks get_proc_desc tenv pdesc summary =
let callee_loc = Procdesc.get_loc callee_pdesc in let callee_loc = Procdesc.get_loc callee_pdesc in
let caller_pname = Procdesc.get_proc_name caller_pdesc in let caller_pname = Procdesc.get_proc_name caller_pdesc in
let callee_pname = Procdesc.get_proc_name callee_pdesc in let callee_pname = Procdesc.get_proc_name callee_pdesc in
let lock, lock' = match
(caller_elem.LockOrder.eventually.LockEvent.lock, elem.LockOrder.eventually.LockEvent.lock) ( caller_elem.LockOrder.eventually.LockEvent.event
in , elem.LockOrder.eventually.LockEvent.event )
let error_message = with
Format.asprintf "Potential deadlock (%a ; %a)" LockIdentity.pp lock LockIdentity.pp lock' | LockEvent.LockAcquire lock, LockEvent.LockAcquire lock' ->
in let error_message =
let exn = Exceptions.Checkers (IssueType.starvation, Localise.verbatim_desc error_message) in Format.asprintf "Potential deadlock (%a ; %a)" LockIdentity.pp lock LockIdentity.pp
let first_trace = List.rev (make_loc_trace caller_pname 1 caller_loc caller_elem) in lock'
let second_trace = make_loc_trace callee_pname 2 callee_loc elem in in
let ltr = List.rev_append first_trace second_trace in let exn =
Specs.get_summary caller_pname Exceptions.Checkers (IssueType.starvation, Localise.verbatim_desc error_message)
|> Option.iter ~f:(fun summary -> Reporting.log_error summary ~loc:caller_loc ~ltr exn) ) in
let first_trace = List.rev (make_loc_trace caller_pname 1 caller_loc caller_elem) in
let second_trace = make_loc_trace callee_pname 2 callee_loc elem in
let ltr = List.rev_append first_trace second_trace in
Specs.get_summary caller_pname
|> Option.iter ~f:(fun summary -> Reporting.log_error summary ~loc:caller_loc ~ltr exn)
| _, _ ->
() )
in in
let report_pair current_class elem = let report_pair current_class elem =
LockOrder.get_pair elem LockOrder.get_pair elem

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

@ -8,6 +8,7 @@
*) *)
open! IStd open! IStd
module F = Format module F = Format
module L = Logging
module LockIdentity = struct module LockIdentity = struct
type t = AccessPath.t type t = AccessPath.t
@ -26,54 +27,94 @@ module LockIdentity = struct
let equal lock lock' = Int.equal 0 (compare lock lock') let equal lock lock' = Int.equal 0 (compare lock lock')
let equal_modulo_base ((_, typ), aclist) ((_, typ'), aclist') = let equal_modulo_base (((root, typ), aclist) as l) (((root', typ'), aclist') as l') =
Typ.equal typ typ' && AccessPath.equal_access_list aclist aclist' if phys_equal l l' then true
else
match (root, root') with
| Var.LogicalVar _, Var.LogicalVar _ ->
(* only class objects are supposed to appear as idents *)
equal l l'
| Var.ProgramVar _, Var.ProgramVar _ ->
Typ.equal typ typ' && AccessPath.equal_access_list aclist aclist'
| _, _ ->
false
let pp fmt (((_, typ), _) as lock) = let pp fmt (((_, typ), _) as lock) =
Format.fprintf fmt "locks %a in class %a" AccessPath.pp lock (Typ.pp_full Pp.text) typ F.fprintf fmt "Locks %a in class %a" AccessPath.pp lock (Typ.pp_full Pp.text) typ
end end
module LockEvent = struct module LockEvent = struct
type t = {lock: LockIdentity.t; loc: Location.t; trace: CallSite.t list} type event_t = LockAcquire of LockIdentity.t | MayBlock of string [@@deriving compare]
let pp_event fmt = function
| LockAcquire lock ->
LockIdentity.pp fmt lock
| MayBlock msg ->
F.pp_print_string fmt msg
type t = {event: event_t; loc: Location.t; trace: CallSite.t list}
let is_lock_event e = match e.event with LockAcquire _ -> true | _ -> false
(* ignore trace when comparing *) (* ignore trace when comparing *)
let compare e e' = let compare e e' =
if phys_equal e e' then 0 if phys_equal e e' then 0
else else
let res = LockIdentity.compare e.lock e'.lock in let res = compare_event_t e.event e'.event in
if not (Int.equal res 0) then res else Location.compare e.loc e'.loc if not (Int.equal res 0) then res else Location.compare e.loc e'.loc
let locks_equal e e' = LockIdentity.equal e.lock e'.lock let locks_equal e e' =
match (e.event, e'.event) with
| LockAcquire lock, LockAcquire lock' ->
LockIdentity.equal lock lock'
| _, _ ->
false
let locks_equal_modulo_base e e' =
match (e.event, e'.event) with
| LockAcquire lock, LockAcquire lock' ->
LockIdentity.equal_modulo_base lock lock'
| _, _ ->
false
let pp fmt e = let pp fmt e =
let pp_trace fmt = function let pp_trace fmt = function
| [] -> | [] ->
() ()
| trace -> | trace ->
Format.fprintf fmt " (trace: %a)" (Pp.semicolon_seq CallSite.pp) trace F.fprintf fmt " (trace: %a)" (Pp.semicolon_seq CallSite.pp) trace
in in
Format.fprintf fmt "%a at %a%a" LockIdentity.pp e.lock Location.pp e.loc pp_trace e.trace F.fprintf fmt "%a at %a%a" pp_event e.event Location.pp e.loc pp_trace e.trace
let owner_class e = let owner_class e =
let (_, typ), _ = e.lock in match e.event with
Typ.inner_name typ | LockAcquire lock ->
let (_, typ), _ = lock in
Typ.inner_name typ
| _ ->
None
let make_acquire lock loc = {event= LockAcquire lock; loc; trace= []}
let make lock loc = {lock; loc; trace= []} let _make_blocks msg loc = {event= MayBlock msg; loc; trace= []}
let make_loc_trace ?(reverse= false) e = let make_loc_trace ?(reverse= false) 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:([], 0) ~f:(fun (tr, ns) callsite ->
let elem_descr = let elem_descr =
Format.asprintf "Method call: %a" Typ.Procname.pp (CallSite.pname callsite) F.asprintf "Method call: %a" Typ.Procname.pp (CallSite.pname callsite)
in in
let elem = Errlog.make_trace_element ns (CallSite.loc callsite) elem_descr [] in let elem = Errlog.make_trace_element ns (CallSite.loc callsite) elem_descr [] in
(elem :: tr, ns + 1) ) (elem :: tr, ns + 1) )
in in
let endpoint_descr = Format.asprintf "Lock acquisition: %a" LockIdentity.pp e.lock in let endpoint_descr = F.asprintf "%a" pp_event e.event in
let endpoint = Errlog.make_trace_element nesting e.loc endpoint_descr [] in let endpoint = Errlog.make_trace_element nesting e.loc endpoint_descr [] in
let res = endpoint :: call_trace in let res = endpoint :: call_trace in
if reverse then res else List.rev res if reverse then res else List.rev res
@ -85,28 +126,29 @@ module LockOrder = struct
let pp fmt o = let pp fmt o =
match o.first with match o.first with
| None -> | None ->
Format.fprintf fmt "Eventually %a" LockEvent.pp o.eventually F.fprintf fmt "Eventually %a" LockEvent.pp o.eventually
| Some lock -> | Some lock ->
Format.fprintf fmt "First %a and before releasing it %a" LockEvent.pp lock LockEvent.pp F.fprintf fmt "First %a and before releasing it %a" LockEvent.pp lock LockEvent.pp
o.eventually o.eventually
let get_pair elem = match elem.first with None -> None | Some b -> Some (b, elem.eventually) let get_pair elem = match elem.first with None -> None | Some b -> Some (b, elem.eventually)
let may_deadlock elem elem' = let may_deadlock elem elem' =
let locks_equal_modulo_base e e' =
LockIdentity.equal_modulo_base e.LockEvent.lock e'.LockEvent.lock
in
match (elem.first, elem'.first) with match (elem.first, elem'.first) with
| Some b, Some b' -> | Some b, Some b' ->
locks_equal_modulo_base b elem'.eventually && locks_equal_modulo_base b' elem.eventually LockEvent.locks_equal_modulo_base b elem'.eventually
&& LockEvent.locks_equal_modulo_base b' elem.eventually
| _, _ -> | _, _ ->
false false
let make_eventually_locks eventually = {first= None; eventually} let make_eventually eventually = {first= None; eventually}
let make_first_and_eventually b eventually =
if not (LockEvent.is_lock_event b) then L.(die InternalError) "Expected a lock event first." ;
{first= Some b; eventually}
let make_holds_and_locks b eventually = {first= Some b; eventually}
let with_callsite callsite o = let with_callsite callsite o =
{ o with { o with
@ -129,7 +171,8 @@ module LockOrderDomain = struct
let is_eventually_locked lock lo = let is_eventually_locked lock lo =
exists (fun pair -> LockEvent.locks_equal pair.LockOrder.eventually lock) lo LockEvent.is_lock_event lock
&& exists (fun pair -> LockEvent.locks_equal pair.LockOrder.eventually lock) lo
end end
module LockStack = AbstractDomain.StackDomain (LockEvent) module LockStack = AbstractDomain.StackDomain (LockEvent)
@ -137,10 +180,15 @@ module LockStack = AbstractDomain.StackDomain (LockEvent)
module LockState = struct module LockState = struct
include AbstractDomain.InvertedMap (LockIdentity) (LockStack) include AbstractDomain.InvertedMap (LockIdentity) (LockStack)
let is_taken lock map = try not (find lock map |> LockStack.is_empty) with Not_found -> false let is_taken lock_event map =
match lock_event.LockEvent.event with
| LockEvent.LockAcquire lock -> (
try not (find lock map |> LockStack.is_empty) with Not_found -> false )
| _ ->
false
let acquire lock_event map = let acquire lock_id lock_event map =
let lock_id = lock_event.LockEvent.lock in
let current_value = try find lock_id map with Not_found -> LockStack.empty in let current_value = try find lock_id map with Not_found -> LockStack.empty in
let new_value = LockStack.push lock_event current_value in let new_value = LockStack.push lock_event current_value in
add lock_id new_value map add lock_id new_value map
@ -168,27 +216,27 @@ let is_empty (ls, lo) = LockState.is_empty ls && LockOrderDomain.is_empty lo
(* for every lock b held locally, add a pair (b, lock_event), plus (None, lock_event) *) (* for every lock b held locally, add a pair (b, lock_event), plus (None, lock_event) *)
let add_order_pairs ls lock_event acc = let add_order_pairs ls lock_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 lock_event.LockEvent.lock ls then acc if LockState.is_taken lock_event ls then acc
else else
let add_eventually_locks acc = let add_eventually acc =
(* don't add an eventually-locks pair if there is already another with same endpoint*) (* don't add an eventually-locks pair if there is already another with same endpoint*)
if LockOrderDomain.is_eventually_locked lock_event acc then acc if LockOrderDomain.is_eventually_locked lock_event acc then acc
else else
let elem = LockOrder.make_eventually_locks lock_event in let elem = LockOrder.make_eventually lock_event in
LockOrderDomain.add elem acc LockOrderDomain.add elem acc
in in
let add_holds_and_locks acc first = let add_first_and_eventually acc first =
(* never add a pair of the form (a,a) -- should never happen due to the check above *) (* never add a pair of the form (a,a) -- should never happen due to the check above *)
let elem = LockOrder.make_holds_and_locks first lock_event in let elem = LockOrder.make_first_and_eventually first lock_event in
LockOrderDomain.add elem acc LockOrderDomain.add elem acc
in in
LockState.fold_over_events add_holds_and_locks ls acc |> add_eventually_locks LockState.fold_over_events add_first_and_eventually ls acc |> add_eventually
let acquire lockid (ls, lo) loc = let acquire lockid (ls, lo) loc =
let newlock_event = LockEvent.make lockid loc in let newlock_event = LockEvent.make_acquire lockid loc in
let lo' = add_order_pairs ls newlock_event lo in let lo' = add_order_pairs ls newlock_event lo in
let ls' = LockState.acquire newlock_event ls in let ls' = LockState.acquire lockid newlock_event ls in
(ls', lo') (ls', lo')

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

@ -16,7 +16,9 @@ module LockIdentity : PrettyPrintable.PrintableOrderedType with type t = AccessP
(** A lock event. Equality/comparison disregards the call trace but includes location. *) (** A lock event. Equality/comparison disregards the call trace but includes location. *)
module LockEvent : sig module LockEvent : sig
type t = private {lock: LockIdentity.t; loc: Location.t; trace: CallSite.t list} type event_t = private LockAcquire of LockIdentity.t | MayBlock of string
type t = private {event: event_t; loc: Location.t; trace: CallSite.t list}
include PrettyPrintable.PrintableOrderedType with type t := t include PrettyPrintable.PrintableOrderedType with type t := t

16
infer/tests/codetoanalyze/java/starvation/StaticLock.java
Unescape View File

@ -8,26 +8,26 @@
*/ */
class StaticLock { class StaticLock {
static synchronized void static_synced() {} static synchronized void staticSynced() {}
void lock_same_class_one_way_ok() { void lockSameClassOneWayOk() {
synchronized(StaticLock.class) { synchronized(StaticLock.class) {
static_synced(); staticSynced();
} }
} }
static synchronized void lock_same_class_another_way_ok() { static synchronized void lockSameClassAnotherWayOk() {
synchronized(StaticLock.class) { synchronized(StaticLock.class) {
} }
} }
void lock_other_class_one_way_bad() { void lockOtherClassOneWayBad() {
synchronized(Object.class) { synchronized(StaticLock.class) {
synchronized(this) {} synchronized(this) {}
} }
} }
synchronized void lock_other_class_another_way_bad() { synchronized void lockOtherClassAnotherWayNad() {
static_synced(); staticSynced();
} }
} }

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

@ -1,6 +1,6 @@
codetoanalyze/java/starvation/InnerClass.java, void InnerClass$InnerClassA.innerOuterBad(), 0, STARVATION, ERROR, [[Trace 1] Lock acquisition: locks this in class InnerClass$InnerClassA*,Method call: void InnerClass.bar(),Lock acquisition: locks this in class InnerClass*,[Trace 2] Lock acquisition: locks this in class InnerClass*,Method call: void InnerClass$InnerClassA.baz(),Lock acquisition: locks this in class InnerClass$InnerClassA*] codetoanalyze/java/starvation/InnerClass.java, void InnerClass$InnerClassA.innerOuterBad(), 0, STARVATION, ERROR, [[Trace 1] Locks this in class InnerClass$InnerClassA*,Method call: void InnerClass.bar(),Locks this in class InnerClass*,[Trace 2] Locks this in class InnerClass*,Method call: void InnerClass$InnerClassA.baz(),Locks this in class InnerClass$InnerClassA*]
codetoanalyze/java/starvation/InnerClass.java, void InnerClass.outerInnerBad(InnerClass$InnerClassA), 0, STARVATION, ERROR, [[Trace 1] Lock acquisition: locks this in class InnerClass*,Method call: void InnerClass$InnerClassA.baz(),Lock acquisition: locks this in class InnerClass$InnerClassA*,[Trace 2] Method start: InnerClass$InnerClassA.<init>(InnerClass,Object),Lock acquisition: locks this in class InnerClass$InnerClassA*,Method call: void InnerClass.bar(),Lock acquisition: locks this in class InnerClass*] codetoanalyze/java/starvation/InnerClass.java, void InnerClass.outerInnerBad(InnerClass$InnerClassA), 0, STARVATION, ERROR, [[Trace 1] Locks this in class InnerClass*,Method call: void InnerClass$InnerClassA.baz(),Locks this in class InnerClass$InnerClassA*,[Trace 2] Method start: InnerClass$InnerClassA.<init>(InnerClass,Object),Locks this in class InnerClass$InnerClassA*,Method call: void InnerClass.bar(),Locks this in class InnerClass*]
codetoanalyze/java/starvation/Interclass.java, void Interclass.interclass1_bad(InterclassA), 0, STARVATION, ERROR, [[Trace 1] Lock acquisition: locks this in class Interclass*,Method call: void InterclassA.interclass1_bad(),Lock acquisition: locks this in class InterclassA*,[Trace 2] Lock acquisition: locks this in class InterclassA*,Method call: void Interclass.interclass2_bad(),Lock acquisition: locks this in class Interclass*] codetoanalyze/java/starvation/Interclass.java, void Interclass.interclass1_bad(InterclassA), 0, STARVATION, ERROR, [[Trace 1] Locks this in class Interclass*,Method call: void InterclassA.interclass1_bad(),Locks this in class InterclassA*,[Trace 2] Locks this in class InterclassA*,Method call: void Interclass.interclass2_bad(),Locks this in class Interclass*]
codetoanalyze/java/starvation/Interproc.java, void Interproc.interproc1_bad(InterprocA), 0, STARVATION, ERROR, [[Trace 1] Lock acquisition: locks this in class Interproc*,Method call: void Interproc.interproc2_bad(InterprocA),Lock acquisition: locks b in class InterprocA*,[Trace 2] Lock acquisition: locks this in class InterprocA*,Method call: void InterprocA.interproc2_bad(Interproc),Lock acquisition: locks d in class Interproc*] codetoanalyze/java/starvation/Interproc.java, void Interproc.interproc1_bad(InterprocA), 0, STARVATION, ERROR, [[Trace 1] Locks this in class Interproc*,Method call: void Interproc.interproc2_bad(InterprocA),Locks b in class InterprocA*,[Trace 2] Locks this in class InterprocA*,Method call: void InterprocA.interproc2_bad(Interproc),Locks d in class Interproc*]
codetoanalyze/java/starvation/Intraproc.java, void IntraprocA.intra_bad(Intraproc), 0, STARVATION, ERROR, [[Trace 1] Method start: void IntraprocA.intra_bad(Intraproc),Lock acquisition: locks this in class IntraprocA*,Lock acquisition: locks o in class Intraproc*,[Trace 2] Method start: void Intraproc.intra_bad(IntraprocA),Lock acquisition: locks this in class Intraproc*,Lock acquisition: locks o in class IntraprocA*] codetoanalyze/java/starvation/Intraproc.java, void IntraprocA.intra_bad(Intraproc), 0, STARVATION, ERROR, [[Trace 1] Method start: void IntraprocA.intra_bad(Intraproc),Locks this in class IntraprocA*,Locks o in class Intraproc*,[Trace 2] Method start: void Intraproc.intra_bad(IntraprocA),Locks this in class Intraproc*,Locks o in class IntraprocA*]
codetoanalyze/java/starvation/StaticLock.java, void StaticLock.lock_other_class_one_way_bad(), 0, STARVATION, ERROR, [[Trace 1] Method start: void StaticLock.lock_other_class_one_way_bad(),Lock acquisition: locks java.lang.Object$0 in class java.lang.Class*,Lock acquisition: locks this in class StaticLock*,[Trace 2] Lock acquisition: locks this in class StaticLock*,Method call: void StaticLock.static_synced(),Lock acquisition: locks StaticLock$0 in class java.lang.Class*] codetoanalyze/java/starvation/StaticLock.java, void StaticLock.lockOtherClassOneWayBad(), 0, STARVATION, ERROR, [[Trace 1] Method start: void StaticLock.lockOtherClassOneWayBad(),Locks StaticLock$0 in class java.lang.Class*,Locks this in class StaticLock*,[Trace 2] Locks this in class StaticLock*,Method call: void StaticLock.staticSynced(),Locks StaticLock$0 in class java.lang.Class*]

Write Preview
Loading…
Cancel
Save