From 0130c09dfc50d8d4d83709115be2030dc6ed2b34 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Tue, 17 Apr 2018 07:27:47 -0700 Subject: [PATCH] [starvation] add infrastructure for blocking events other than lock acquisition Reviewed By: ddino Differential Revision: D7428995 fbshipit-source-id: 5e1185d --- infer/src/concurrency/starvation.ml | 46 ++++--- infer/src/concurrency/starvationDomain.ml | 114 +++++++++++++----- infer/src/concurrency/starvationDomain.mli | 4 +- .../java/starvation/StaticLock.java | 16 +-- .../codetoanalyze/java/starvation/issues.exp | 12 +- 5 files changed, 126 insertions(+), 66 deletions(-) diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index b1d30744c..6a58b0c44 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -119,19 +119,22 @@ let should_report_if_same_class _ = true not (Typ.Name.equal first_class eventually_class) || LockEvent.compare b a >= 0 ) ) )) *) -let make_loc_trace pname trace_id start_loc elem = - let open StarvationDomain in - let header = Printf.sprintf "[Trace %d]" trace_id in - let trace = LockOrder.make_loc_trace elem in +let make_trace_with_header ?(header= "") elem start_loc pname = + let trace = StarvationDomain.LockOrder.make_loc_trace elem in let first_step = List.hd_exn trace in 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 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 +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 = Summary.read_summary caller_pdesc (Procdesc.get_proc_name callee_pdesc) |> 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 caller_pname = Procdesc.get_proc_name caller_pdesc in let callee_pname = Procdesc.get_proc_name callee_pdesc in - let lock, lock' = - (caller_elem.LockOrder.eventually.LockEvent.lock, elem.LockOrder.eventually.LockEvent.lock) - in - let error_message = - Format.asprintf "Potential deadlock (%a ; %a)" LockIdentity.pp lock LockIdentity.pp lock' - in - let exn = Exceptions.Checkers (IssueType.starvation, Localise.verbatim_desc error_message) 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) ) + match + ( caller_elem.LockOrder.eventually.LockEvent.event + , elem.LockOrder.eventually.LockEvent.event ) + with + | LockEvent.LockAcquire lock, LockEvent.LockAcquire lock' -> + let error_message = + Format.asprintf "Potential deadlock (%a ; %a)" LockIdentity.pp lock LockIdentity.pp + lock' + in + let exn = + Exceptions.Checkers (IssueType.starvation, Localise.verbatim_desc error_message) + 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 let report_pair current_class elem = LockOrder.get_pair elem diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 3f32319de..093034375 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -8,6 +8,7 @@ *) open! IStd module F = Format +module L = Logging module LockIdentity = struct type t = AccessPath.t @@ -26,54 +27,94 @@ module LockIdentity = struct let equal lock lock' = Int.equal 0 (compare lock lock') - let equal_modulo_base ((_, typ), aclist) ((_, typ'), aclist') = - Typ.equal typ typ' && AccessPath.equal_access_list aclist aclist' + let equal_modulo_base (((root, typ), aclist) as l) (((root', typ'), aclist') as l') = + 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) = - 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 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 *) let compare e e' = if phys_equal e e' then 0 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 - 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_trace fmt = function | [] -> () | trace -> - Format.fprintf fmt " (trace: %a)" (Pp.semicolon_seq CallSite.pp) trace + F.fprintf fmt " (trace: %a)" (Pp.semicolon_seq CallSite.pp) trace 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 (_, typ), _ = e.lock in - Typ.inner_name typ + match e.event with + | 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 call_trace, nesting = List.fold e.trace ~init:([], 0) ~f:(fun (tr, ns) callsite -> 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 let elem = Errlog.make_trace_element ns (CallSite.loc callsite) elem_descr [] in (elem :: tr, ns + 1) ) 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 res = endpoint :: call_trace in if reverse then res else List.rev res @@ -85,28 +126,29 @@ module LockOrder = struct let pp fmt o = match o.first with | None -> - Format.fprintf fmt "Eventually %a" LockEvent.pp o.eventually + F.fprintf fmt "Eventually %a" LockEvent.pp o.eventually | 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 let get_pair elem = match elem.first with None -> None | Some b -> Some (b, elem.eventually) 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 | 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 - 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 = { o with @@ -129,7 +171,8 @@ module LockOrderDomain = struct 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 module LockStack = AbstractDomain.StackDomain (LockEvent) @@ -137,10 +180,15 @@ module LockStack = AbstractDomain.StackDomain (LockEvent) module LockState = struct 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 lock_id = lock_event.LockEvent.lock in + let acquire lock_id lock_event map = let current_value = try find lock_id map with Not_found -> LockStack.empty in let new_value = LockStack.push lock_event current_value in 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) *) let add_order_pairs ls lock_event acc = (* 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 - let add_eventually_locks acc = + let add_eventually acc = (* 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 else - let elem = LockOrder.make_eventually_locks lock_event in + let elem = LockOrder.make_eventually lock_event in LockOrderDomain.add elem acc 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 *) - 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 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 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 ls' = LockState.acquire newlock_event ls in + let ls' = LockState.acquire lockid newlock_event ls in (ls', lo') diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 71745def5..ff67175b1 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -16,7 +16,9 @@ module LockIdentity : PrettyPrintable.PrintableOrderedType with type t = AccessP (** A lock event. Equality/comparison disregards the call trace but includes location. *) 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 diff --git a/infer/tests/codetoanalyze/java/starvation/StaticLock.java b/infer/tests/codetoanalyze/java/starvation/StaticLock.java index ec09ed221..ef8a99bec 100644 --- a/infer/tests/codetoanalyze/java/starvation/StaticLock.java +++ b/infer/tests/codetoanalyze/java/starvation/StaticLock.java @@ -8,26 +8,26 @@ */ class StaticLock { - static synchronized void static_synced() {} + static synchronized void staticSynced() {} - void lock_same_class_one_way_ok() { + void lockSameClassOneWayOk() { synchronized(StaticLock.class) { - static_synced(); + staticSynced(); } } - static synchronized void lock_same_class_another_way_ok() { + static synchronized void lockSameClassAnotherWayOk() { synchronized(StaticLock.class) { } } - void lock_other_class_one_way_bad() { - synchronized(Object.class) { + void lockOtherClassOneWayBad() { + synchronized(StaticLock.class) { synchronized(this) {} } } - synchronized void lock_other_class_another_way_bad() { - static_synced(); + synchronized void lockOtherClassAnotherWayNad() { + staticSynced(); } } diff --git a/infer/tests/codetoanalyze/java/starvation/issues.exp b/infer/tests/codetoanalyze/java/starvation/issues.exp index f6abe3c6b..a778c7796 100644 --- a/infer/tests/codetoanalyze/java/starvation/issues.exp +++ b/infer/tests/codetoanalyze/java/starvation/issues.exp @@ -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.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.(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/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/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/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/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/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] Locks this in class InnerClass*,Method call: void InnerClass$InnerClassA.baz(),Locks this in class InnerClass$InnerClassA*,[Trace 2] Method start: InnerClass$InnerClassA.(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] 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] 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),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.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*]