From 36de121dc54c445d83e9002c6692f00cd5e38485 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Thu, 3 Oct 2019 05:08:38 -0700 Subject: [PATCH] [starvation] change domain to use critical pairs `(set of locks held, event)` Summary: The old domain keeps two sets: - `events` are things (including lock acquisitions) which eventually happen during the execution of a procedure. - `order` are pairs of `(lock, event)` such that there is a trace through the procedure which at some point acquires `lock` and before releasing it performs `event`. A deadlock would be reported if for two procedures, `(lock1,lock2)` is in `order` of procedure 1 and `(lock2,lock1)` is in `order` of procedure 2. This condition/domain allowed for the false positive fixed in the tests, as well as was unwieldy, because it required translating between the two sets. The new domain has only one set of "critical pairs" `(locks, event)` such that there is a trace where `event` occurs, and *right before it occurs* the locks held are exactly `locks` (no over/under approximation). This allows keeping all information in one set, simplifies the procedure call handling and eliminates the known false positive. Reviewed By: mityal Differential Revision: D17686944 fbshipit-source-id: 3c68bb957 --- infer/src/concurrency/starvation.ml | 186 ++++---- infer/src/concurrency/starvationDomain.ml | 443 +++++++++++------- infer/src/concurrency/starvationDomain.mli | 100 ++-- .../java/starvation/MasterLock.java | 4 +- .../codetoanalyze/java/starvation/issues.exp | 4 +- 5 files changed, 429 insertions(+), 308 deletions(-) diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 53b6b7594..700cafdd9 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -75,14 +75,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> None in - let is_java = Summary.get_proc_name summary |> Typ.Procname.is_java in + let procname = Summary.get_proc_name summary in + let is_java = Typ.Procname.is_java procname in let do_lock locks loc astate = - List.filter_map ~f:get_lock_path locks |> Domain.acquire tenv astate loc + List.filter_map ~f:get_lock_path locks |> Domain.acquire tenv astate ~procname ~loc in let do_unlock locks astate = List.filter_map ~f:get_lock_path locks |> Domain.release astate in let do_call callee loc astate = Payload.read ~caller_summary:summary ~callee_pname:callee - |> Option.value_map ~default:astate ~f:(Domain.integrate_summary tenv astate callee loc) + |> Option.value_map ~default:astate ~f:(fun callee_summary -> + Domain.integrate_summary tenv ~caller_summary:astate ~callee_summary ~callee ~loc ) in match instr with | Assign _ | Assume _ | Call (_, Indirect _, _, _, _) | Metadata _ -> @@ -94,11 +96,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Lock locks -> do_lock locks loc astate | GuardLock guard -> - Domain.lock_guard tenv astate guard loc + Domain.lock_guard tenv astate guard ~procname ~loc | GuardConstruct {guard; lock; acquire_now} -> ( match get_lock_path lock with | Some lock_path -> - Domain.add_guard tenv astate guard lock_path ~acquire_now loc + Domain.add_guard tenv astate guard lock_path ~acquire_now ~procname ~loc | None -> log_parse_error "Couldn't parse lock in guard constructor" callee actuals ; astate ) @@ -116,17 +118,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct do_lock locks loc astate |> do_unlock locks | NoEffect when is_java && is_ui_thread_model callee -> let explanation = F.asprintf "it calls %a" pname_pp callee in - Domain.set_on_ui_thread astate loc explanation - | NoEffect when is_java && StarvationModels.is_strict_mode_violation tenv callee actuals -> - Domain.strict_mode_call callee loc astate - | NoEffect -> - if is_java then - may_block tenv callee actuals - |> Option.map ~f:(fun sev -> Domain.blocking_call callee sev loc astate) - |> IOption.value_default_f ~f:(fun () -> do_call callee loc astate) - else - (* in C++/Obj C we only care about deadlocks, not starvation errors *) + Domain.set_on_ui_thread astate ~loc explanation + | NoEffect when is_java && is_strict_mode_violation tenv callee actuals -> + Domain.strict_mode_call ~callee ~loc astate + | NoEffect when is_java -> ( + match may_block tenv callee actuals with + | Some sev -> + Domain.blocking_call ~callee sev ~loc astate + | None -> do_call callee loc astate ) + | NoEffect -> + (* in C++/Obj C we only care about deadlocks, not starvation errors *) + do_call callee loc astate ) let pp_session_name _node fmt = F.pp_print_string fmt "starvation" @@ -136,10 +139,9 @@ module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.N let analyze_procedure {Callbacks.exe_env; summary} = let proc_desc = Summary.get_proc_desc summary in - let open StarvationDomain in - let pname = Procdesc.get_proc_name proc_desc in - let tenv = Exe_env.get_tenv exe_env pname in - if StarvationModels.should_skip_analysis tenv pname [] then summary + let procname = Procdesc.get_proc_name proc_desc in + let tenv = Exe_env.get_tenv exe_env procname in + if StarvationModels.should_skip_analysis tenv procname [] then summary else let formals = FormalMap.make proc_desc in let proc_data = ProcData.make summary tenv formals in @@ -148,7 +150,7 @@ let analyze_procedure {Callbacks.exe_env; summary} = if not (Procdesc.is_java_synchronized proc_desc) then StarvationDomain.bottom else let lock = - match pname with + match procname with | Typ.Procname.Java java_pname when Typ.Procname.Java.is_static java_pname -> (* this is crafted so as to match synchronized(CLASSNAME.class) constructs *) Typ.Procname.Java.get_class_type_name java_pname @@ -156,22 +158,15 @@ let analyze_procedure {Callbacks.exe_env; summary} = | _ -> FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> (base, [])) in - StarvationDomain.acquire tenv StarvationDomain.bottom loc (Option.to_list lock) + StarvationDomain.acquire tenv StarvationDomain.bottom ~procname ~loc (Option.to_list lock) in let initial = ConcurrencyModels.runs_on_ui_thread ~attrs_of_pname:Summary.OnDisk.proc_resolve_attributes tenv proc_desc - |> Option.value_map ~default:initial ~f:(StarvationDomain.set_on_ui_thread initial loc) + |> Option.value_map ~default:initial ~f:(StarvationDomain.set_on_ui_thread initial ~loc) in let filter_blocks = - if is_nonblocking tenv proc_desc then fun ({events; order} as astate) -> - { astate with - events= EventDomain.filter (function {elem= MayBlock _} -> false | _ -> true) events - ; order= - OrderDomain.filter - (function {elem= {eventually= {elem= MayBlock _}}} -> false | _ -> true) - order } - else Fn.id + if is_nonblocking tenv proc_desc then StarvationDomain.filter_blocking_calls else Fn.id in Analyzer.compute_post proc_data ~initial |> Option.map ~f:filter_blocks @@ -313,29 +308,28 @@ let should_report_deadlock_on_current_proc current_elem endpoint_elem = (not Config.deduplicate) || let open StarvationDomain in - match (current_elem.Order.elem.first, current_elem.Order.elem.eventually.elem) with - | _, (MayBlock _ | StrictModeCall _) -> + match (endpoint_elem.CriticalPair.elem.event, current_elem.CriticalPair.elem.event) with + | _, (MayBlock _ | StrictModeCall _) | (MayBlock _ | StrictModeCall _), _ -> (* should never happen *) - L.die InternalError "Deadlock cannot occur without two lock events: %a" Order.pp current_elem - | ((Var.LogicalVar _, _), []), _ -> + L.die InternalError "Deadlock cannot occur without two lock events: %a" CriticalPair.pp + current_elem + | LockAcquire ((Var.LogicalVar _, _), []), _ -> (* first elem is a class object (see [lock_of_class]), so always report because the - reverse ordering on the events will not occur *) + reverse ordering on the events will not occur -- FIXME WHY? *) true - | ((Var.LogicalVar _, _), _ :: _), _ | _, LockAcquire ((Var.LogicalVar _, _), _) -> + | LockAcquire ((Var.LogicalVar _, _), _ :: _), _ | _, LockAcquire ((Var.LogicalVar _, _), _) -> (* first elem has an ident root, but has a non-empty access path, which means we are not filtering out local variables (see [exec_instr]), or, second elem has an ident root, which should not happen if we are filtering locals *) - L.die InternalError "Deadlock cannot occur on these logical variables: %a @." Order.pp + L.die InternalError "Deadlock cannot occur on these logical variables: %a @." CriticalPair.pp current_elem - | ((_, typ1), _), LockAcquire ((_, typ2), _) -> + | LockAcquire ((_, typ1), _), LockAcquire ((_, typ2), _) -> (* 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 c < 0 || Int.equal 0 c && (* same class, so choose depending on location *) - Location.compare current_elem.Order.elem.eventually.Event.loc - endpoint_elem.Order.elem.eventually.Event.loc - < 0 + Location.compare current_elem.CriticalPair.loc endpoint_elem.CriticalPair.loc < 0 let should_report pdesc = @@ -368,7 +362,7 @@ let fold_reportable_summaries (tenv, current_summary) clazz ~init ~f = List.fold methods ~init ~f -let report_lockless_violations (tenv, summary) {StarvationDomain.events} report_map = +let report_lockless_violations (tenv, summary) StarvationDomain.{critical_pairs} report_map = let open StarvationDomain in (* this is inneficient as it climbs the hierarchy potentially twice *) let is_annotated_lockless tenv pname = @@ -383,43 +377,45 @@ let report_lockless_violations (tenv, summary) {StarvationDomain.events} report_ let pname = Summary.get_proc_name summary in if not (is_annotated_lockless tenv pname) then report_map else - let report_violation (event : Event.t) report_map = - match event.elem with + let report_violation ({elem= {event}} as critical_pair : CriticalPair.t) report_map = + match event with | LockAcquire _ -> let error_message = Format.asprintf "Method %a is annotated %s but%a." pname_pp pname (MF.monospaced_to_string Annotations.lockless) Event.describe event in - let loc = Event.get_loc event in - let ltr = Event.make_trace pname event in + let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:pname critical_pair in + let ltr = CriticalPair.make_trace pname critical_pair in ReportMap.add_lockless_violation pname loc ltr error_message report_map | _ -> report_map in - EventDomain.fold report_violation events report_map + CriticalPairs.fold report_violation critical_pairs report_map (* Note about how many times we report a deadlock: normally twice, at each trace starting point. - Due to the fact we look for deadlocks in the summaries of the class at the root of a path, - this will fail when (a) the lock is of class type (ie as used in static sync methods), because - then the root is an identifier of type java.lang.Class and (b) when the lock belongs to an - inner class but this is no longer obvious in the path, because of nested-class path normalisation. - 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. *) -let report_deadlocks env {StarvationDomain.order; ui} report_map' = + Due to the fact we look for deadlocks in the summaries of the class at the root of a path, + this will fail when (a) the lock is of class type (ie as used in static sync methods), because + then the root is an identifier of type java.lang.Class and (b) when the lock belongs to an + inner class but this is no longer obvious in the path, because of nested-class path normalisation. + 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. *) +let report_deadlocks env StarvationDomain.{critical_pairs; ui} report_map' = let open StarvationDomain in let _, current_summary = env in let current_pname = Summary.get_proc_name current_summary in let report_endpoint_elem current_elem endpoint_pname elem report_map = if not - ( Order.may_deadlock current_elem elem + ( CriticalPair.may_deadlock current_elem elem && should_report_deadlock_on_current_proc current_elem elem ) then report_map else - 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 + let () = + debug "Possible deadlock:@.%a@.%a@." CriticalPair.pp current_elem CriticalPair.pp elem + in + match (current_elem.CriticalPair.elem.event, elem.CriticalPair.elem.event) with | LockAcquire lock1, LockAcquire lock2 -> let error_message = Format.asprintf @@ -428,25 +424,30 @@ let report_deadlocks env {StarvationDomain.order; ui} report_map' = pname_pp current_pname pname_pp endpoint_pname Lock.describe lock1 Lock.describe lock2 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 first_trace = + CriticalPair.make_trace ~header:"[Trace 1] " current_pname current_elem + in + let second_trace = CriticalPair.make_trace ~header:"[Trace 2] " endpoint_pname elem in let ltr = first_trace @ second_trace in - let loc = Order.get_loc current_elem in + let loc = + CriticalPair.get_earliest_lock_or_call_loc ~procname:current_pname current_elem + in ReportMap.add_deadlock current_pname loc ltr error_message report_map | _, _ -> report_map in let report_on_current_elem elem report_map = - match elem.Order.elem.eventually.elem with + match elem.CriticalPair.elem.event with | MayBlock _ | StrictModeCall _ -> report_map - | LockAcquire endpoint_lock when Lock.equal endpoint_lock elem.Order.elem.first -> + | LockAcquire endpoint_lock + when Acquisitions.lock_is_held endpoint_lock elem.CriticalPair.elem.acquisitions -> let error_message = Format.asprintf "Potential self deadlock. %a%a twice." pname_pp current_pname Lock.pp_locks endpoint_lock in - let ltr = Order.make_trace ~header:"In method " current_pname elem in - let loc = Order.get_loc elem in + let ltr = CriticalPair.make_trace ~header:"In method " current_pname elem in + let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:current_pname elem in ReportMap.add_deadlock current_pname loc ltr error_message report_map | LockAcquire endpoint_lock -> Lock.owner_class endpoint_lock @@ -455,50 +456,59 @@ let report_deadlocks env {StarvationDomain.order; ui} report_map' = and retrieve all the summaries of the methods of that class *) (* for each summary related to the endpoint, analyse and report on its pairs *) fold_reportable_summaries env endpoint_class ~init:report_map - ~f:(fun acc (endpoint_pname, {order= endp_order; ui= endp_ui}) -> + ~f:(fun acc + (endpoint_pname, {critical_pairs= endp_critical_pairs; ui= endp_ui}) + -> if UIThreadDomain.is_bottom ui || UIThreadDomain.is_bottom endp_ui then - OrderDomain.fold (report_endpoint_elem elem endpoint_pname) endp_order acc + CriticalPairs.fold + (report_endpoint_elem elem endpoint_pname) + endp_critical_pairs acc else acc ) ) in - OrderDomain.fold report_on_current_elem order report_map' + CriticalPairs.fold report_on_current_elem critical_pairs report_map' -let report_starvation env {StarvationDomain.events; ui} report_map' = +let report_starvation env {StarvationDomain.critical_pairs; ui} report_map' = let open StarvationDomain in let _, current_summary = env in let current_pname = Summary.get_proc_name current_summary in let report_remote_block ui_explain event current_lock endpoint_pname endpoint_elem report_map = - let lock = endpoint_elem.Order.elem.first in - match endpoint_elem.Order.elem.eventually.elem with - | MayBlock (block_descr, sev) when Lock.equal current_lock lock -> + let acquisitions = endpoint_elem.CriticalPair.elem.acquisitions in + match endpoint_elem.CriticalPair.elem.event with + | MayBlock (block_descr, sev) when Acquisitions.lock_is_held current_lock acquisitions -> let error_message = Format.asprintf "Method %a runs on UI thread (because %a) and%a, which may be held by another thread \ which %s." - pname_pp current_pname UIThreadExplanationDomain.pp ui_explain Lock.pp_locks lock - block_descr + pname_pp current_pname UIThreadExplanationDomain.pp ui_explain Lock.pp_locks + current_lock block_descr + in + let first_trace = CriticalPair.make_trace ~header:"[Trace 1] " current_pname event in + let second_trace = + CriticalPair.make_trace ~header:"[Trace 2] " endpoint_pname endpoint_elem in - let first_trace = Event.make_trace ~header:"[Trace 1] " current_pname event in - let second_trace = Order.make_trace ~header:"[Trace 2] " endpoint_pname endpoint_elem in let ui_trace = UIThreadExplanationDomain.make_trace ~header:"[Trace 1 on UI thread] " current_pname ui_explain in let ltr = first_trace @ second_trace @ ui_trace in - let loc = Event.get_loc event in + let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:current_pname event in ReportMap.add_starvation sev current_pname loc ltr error_message report_map | _ -> report_map in - let report_on_current_elem ui_explain event report_map = - match event.Event.elem with + let report_on_current_elem ui_explain (critical_pair : CriticalPair.t) report_map = + let event = critical_pair.elem.event in + match event with | MayBlock (_, sev) -> let error_message = Format.asprintf "Method %a runs on UI thread (because %a), and may block; %a." pname_pp current_pname UIThreadExplanationDomain.pp ui_explain Event.describe event in - let loc = Event.get_loc event in - let trace = Event.make_trace current_pname event in + let loc = CriticalPair.get_loc critical_pair in + let trace = + CriticalPair.make_trace ~include_acquisitions:false current_pname critical_pair + in let ui_trace = UIThreadExplanationDomain.make_trace ~header:"[Trace on UI thread] " current_pname ui_explain @@ -511,8 +521,10 @@ let report_starvation env {StarvationDomain.events; ui} report_map' = "Method %a runs on UI thread (because %a), and may violate Strict Mode; %a." pname_pp current_pname UIThreadExplanationDomain.pp ui_explain Event.describe event in - let loc = Event.get_loc event in - let trace = Event.make_trace current_pname event in + let loc = CriticalPair.get_loc critical_pair in + let trace = + CriticalPair.make_trace ~include_acquisitions:false current_pname critical_pair + in let ui_trace = UIThreadExplanationDomain.make_trace ~header:"[Trace on UI thread] " current_pname ui_explain @@ -526,12 +538,12 @@ let report_starvation env {StarvationDomain.events; ui} report_map' = and retrieve all the summaries of the methods of that class *) (* for each summary related to the endpoint, analyse and report on its pairs *) fold_reportable_summaries env endpoint_class ~init:report_map - ~f:(fun acc (endpoint_pname, {order; ui}) -> + ~f:(fun acc (endpoint_pname, {critical_pairs; ui}) -> (* skip methods on ui thread, as they cannot run in parallel to us *) if UIThreadDomain.is_bottom ui then - OrderDomain.fold - (report_remote_block ui_explain event endpoint_lock endpoint_pname) - order acc + CriticalPairs.fold + (report_remote_block ui_explain critical_pair endpoint_lock endpoint_pname) + critical_pairs acc else acc ) ) in (* do not report starvation/strict mode warnings on constructors, keep that for callers *) @@ -541,7 +553,7 @@ let report_starvation env {StarvationDomain.events; ui} report_map' = | AbstractDomain.Types.Bottom -> report_map' | AbstractDomain.Types.NonBottom ui_explain -> - EventDomain.fold (report_on_current_elem ui_explain) events report_map' + CriticalPairs.fold (report_on_current_elem ui_explain) critical_pairs report_map' let reporting {Callbacks.procedures; source_file} = diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 965a9fa8a..066365b76 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -47,8 +47,6 @@ module Lock = struct let pp_locks fmt lock = F.fprintf fmt " locks %a" describe lock end -module LockEvent = ExplicitTrace.MakeTraceElem (Lock) (ExplicitTrace.DefaultCallPrinter) - module Event = struct type severity_t = Low | Medium | High [@@deriving compare] @@ -57,132 +55,254 @@ module Event = struct F.pp_print_string fmt msg - type event_t = - | LockAcquire of Lock.t - | MayBlock of (string * severity_t) - | StrictModeCall of string + type t = LockAcquire of Lock.t | MayBlock of (string * severity_t) | StrictModeCall of string [@@deriving compare] - module EventElement = struct - type t = event_t [@@deriving compare] - - let pp fmt = function - | LockAcquire lock -> - F.fprintf fmt "LockAcquire(%a)" Lock.pp lock - | MayBlock (msg, sev) -> - F.fprintf fmt "MayBlock(%s, %a)" msg pp_severity sev - | StrictModeCall msg -> - F.fprintf fmt "StrictModeCall(%s)" msg - - - let describe fmt elem = - match elem with - | LockAcquire lock -> - Lock.pp_locks fmt lock - | MayBlock (msg, _) -> - F.pp_print_string fmt msg - | StrictModeCall msg -> - F.pp_print_string fmt msg - end + let pp fmt = function + | LockAcquire lock -> + F.fprintf fmt "LockAcquire(%a)" Lock.pp lock + | MayBlock (msg, sev) -> + F.fprintf fmt "MayBlock(%s, %a)" msg pp_severity sev + | StrictModeCall msg -> + F.fprintf fmt "StrictModeCall(%s)" msg + + + let describe fmt elem = + match elem with + | LockAcquire lock -> + Lock.pp_locks fmt lock + | MayBlock (msg, _) -> + F.pp_print_string fmt msg + | StrictModeCall msg -> + F.pp_print_string fmt msg - include ExplicitTrace.MakeTraceElem (EventElement) (ExplicitTrace.DefaultCallPrinter) - let make_acquire lock loc = make (LockAcquire lock) loc + let make_acquire lock = LockAcquire lock let make_call_descr callee = F.asprintf "calls %a" pname_pp callee - let make_blocking_call callee sev loc = + let make_blocking_call callee sev = let descr = make_call_descr callee in - make (MayBlock (descr, sev)) loc + MayBlock (descr, sev) - let make_strict_mode_call callee loc = + let make_strict_mode_call callee = let descr = make_call_descr callee in - make (StrictModeCall descr) loc + StrictModeCall descr +end +(** A lock acquisition with source location and procname in which it occurs. + The location & procname are *ignored* for comparisons, and are only for reporting. *) +module Acquisition = struct + type t = + {lock: Lock.t; loc: Location.t [@compare.ignore]; procname: Typ.Procname.t [@compare.ignore]} + [@@deriving compare] - let make_trace ?(header = "") pname elem = - let trace = make_loc_trace elem in - let trace_descr = F.asprintf "%s%a" header pname_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 + let pp fmt {lock} = Lock.pp_locks fmt lock + + let make ~procname ~loc lock = {lock; loc; procname} + + let compare_loc {loc= loc1} {loc= loc2} = Location.compare loc1 loc2 + + let make_trace_step acquisition = + let description = F.asprintf "%a" pp acquisition in + Errlog.make_trace_element 0 acquisition.loc description [] end -module EventDomain = Event.FiniteSet +(** Set of acquisitions; due to order over acquisitions, each lock appears at most once. *) +module Acquisitions = struct + include PrettyPrintable.MakePPSet (Acquisition) -module Order = struct - type order_t = {first: Lock.t; eventually: Event.t} [@@deriving compare] + (* use the fact that location/procname are ignored in comparisons *) + let lock_is_held lock acquisitions = + mem {lock; loc= Location.dummy; procname= Typ.Procname.Linters_dummy_method} acquisitions +end - module OrderElement = struct - type t = order_t +module LockState : sig + include AbstractDomain.WithTop - let compare = compare_order_t + val acquire : procname:Typ.Procname.t -> loc:Location.t -> Lock.t -> t -> t - let pp fmt {first; eventually} = - F.fprintf fmt "{first= %a; eventually= %a}" Lock.pp first Event.pp eventually + val release : Lock.t -> t -> t + val is_lock_taken : Event.t -> t -> bool - let describe fmt {first} = Lock.pp_locks fmt first - end + val get_acquisitions : t -> Acquisitions.t +end = struct + module LockStack = AbstractDomain.StackDomain (Acquisition) + include AbstractDomain.InvertedMap (Lock) (LockStack) - include ExplicitTrace.MakeTraceElem (OrderElement) (ExplicitTrace.DefaultCallPrinter) + let get_stack lock map = find_opt lock map |> Option.value ~default:LockStack.top - let may_deadlock {elem= {first; eventually}} {elem= {first= first'; eventually= eventually'}} = - match (eventually.elem, eventually'.elem) with - | LockAcquire e, LockAcquire e' -> - Lock.equal first e' && Lock.equal first' e - | _, _ -> + let is_lock_taken event map = + match event with + | Event.LockAcquire lock -> + not (LockStack.is_top (get_stack lock map)) + | _ -> false - let make_loc_trace ?(nesting = 0) ({elem= {eventually}} as order) = - let first_trace = make_loc_trace ~nesting order 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 + let acquire ~procname ~loc lock map = + let acquisition = Acquisition.make ~procname ~loc lock in + let current_value = get_stack lock map in + let new_value = LockStack.push acquisition current_value in + add lock new_value map - let make_trace ?(header = "") pname elem = - let trace = make_loc_trace elem in - let trace_descr = F.asprintf "%s%a" header pname_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 + let release lock map = + let current_value = get_stack lock map in + if LockStack.is_top current_value then map + else + let new_value = LockStack.pop current_value in + if LockStack.is_top new_value then remove lock map else add lock new_value map + + + (* FIXME - this should be a O(1) operation by moving it into the lock-state and updating in tandem, + so as to increase sharing between critical pairs. *) + let get_acquisitions map = + fold + (fun _lock lock_stack init -> + List.fold lock_stack ~init ~f:(fun acc acquisition -> Acquisitions.add acquisition acc) ) + map Acquisitions.empty end -module OrderDomain = Order.FiniteSet -module LockStack = AbstractDomain.StackDomain (LockEvent) +module CriticalPairElement = struct + type t = {acquisitions: Acquisitions.t; event: Event.t} [@@deriving compare] -module LockState = struct - include AbstractDomain.InvertedMap (Lock) (LockStack) + let pp fmt {acquisitions; event} = + F.fprintf fmt "{acquisitions= %a; event= %a}" Acquisitions.pp acquisitions Event.pp event - let is_taken lock_event map = - match lock_event.Event.elem with - | Event.LockAcquire lock -> ( - try not (find lock map |> LockStack.is_top) with Caml.Not_found -> false ) - | _ -> - false + let describe = pp +end - let acquire loc map lock_id = - let lock_event = LockEvent.make lock_id loc in - let current_value = try find lock_id map with Caml.Not_found -> LockStack.top in - let new_value = LockStack.push lock_event current_value in - add lock_id new_value map +module CriticalPair = struct + include ExplicitTrace.MakeTraceElem (CriticalPairElement) (ExplicitTrace.DefaultCallPrinter) + let make ~loc acquisitions event = make {acquisitions; event} loc - let release lock_id map = - let current_value = try find lock_id map with Caml.Not_found -> LockStack.top in - if LockStack.is_top current_value then map - else - let new_value = LockStack.pop current_value in - if LockStack.is_top new_value then remove lock_id map else add lock_id new_value map + let is_blocking_call {elem= {event}} = match event with LockAcquire _ -> true | _ -> false + + let get_final_acquire {elem= {event}} = + match event with LockAcquire lock -> Some lock | _ -> None + + + let may_deadlock ({elem= pair1} as t1 : t) ({elem= pair2} as t2 : t) = + Option.both (get_final_acquire t1) (get_final_acquire t2) + |> Option.exists ~f:(fun (lock1, lock2) -> + (not (Lock.equal lock1 lock2)) + && Acquisitions.lock_is_held lock2 pair1.acquisitions + && Acquisitions.lock_is_held lock1 pair2.acquisitions + && Acquisitions.inter pair1.acquisitions pair2.acquisitions |> Acquisitions.is_empty ) + + + let with_callsite t existing_acquisitions call_site = + let f ({acquisitions} as elem : CriticalPairElement.t) = + {elem with acquisitions= Acquisitions.union existing_acquisitions acquisitions} + in + let new_t = map ~f t in + with_callsite new_t call_site + + + let get_earliest_lock_or_call_loc ~procname ({elem= {acquisitions}} as t) = + let initial_loc = get_loc t in + Acquisitions.fold + (fun {procname= acq_procname; loc= acq_loc} acc -> + if + Typ.Procname.equal procname acq_procname + && Int.is_negative (Location.compare acq_loc acc) + then acq_loc + else acc ) + acquisitions initial_loc + + + let make_trace ?(header = "") ?(include_acquisitions = true) top_pname + {elem= {acquisitions; event}; trace; loc} = + let acquisitions_map = + if include_acquisitions then + Acquisitions.fold + (fun ({procname} as acq : Acquisition.t) acc -> + Typ.Procname.Map.update procname + (function None -> Some [acq] | Some acqs -> Some (acq :: acqs)) + acc ) + acquisitions Typ.Procname.Map.empty + else Typ.Procname.Map.empty + in + let header_step = + let description = F.asprintf "%s%a" header pname_pp top_pname in + let loc = Location.dummy in + Errlog.make_trace_element 0 loc description [] + in + (* construct the trace segment starting at [call_site] and ending at next call *) + let make_call_stack_step fake_first_call call_site = + let procname = CallSite.pname call_site in + let trace = + Typ.Procname.Map.find_opt procname acquisitions_map + |> Option.value ~default:[] + (* many acquisitions can be on same line (eg, std::lock) so use stable sort + to produce a deterministic trace *) + |> List.stable_sort ~compare:Acquisition.compare_loc + |> List.map ~f:Acquisition.make_trace_step + in + if CallSite.equal call_site fake_first_call then trace + else + let descr = F.asprintf "%a" ExplicitTrace.DefaultCallPrinter.pp call_site in + let call_step = Errlog.make_trace_element 0 (CallSite.loc call_site) descr [] in + call_step :: trace + in + (* construct a call stack trace with the lock acquisitions interleaved *) + let call_stack = + (* fake outermost call so as to include acquisitions in the top level caller *) + let fake_first_call = CallSite.make top_pname Location.dummy in + List.map (fake_first_call :: trace) ~f:(make_call_stack_step fake_first_call) + in + let endpoint_step = + let endpoint_descr = F.asprintf "%a" Event.describe event in + Errlog.make_trace_element 0 loc endpoint_descr [] + in + List.concat (([header_step] :: call_stack) @ [[endpoint_step]]) +end + +let is_recursive_lock event tenv = + let is_class_and_recursive_lock = function + | {Typ.desc= Tptr ({desc= Tstruct name}, _)} | {desc= Tstruct name} -> + ConcurrencyModels.is_recursive_lock_type name + | typ -> + L.debug Analysis Verbose "Asked if non-struct type %a is a recursive lock type.@." + (Typ.pp_full Pp.text) typ ; + true + in + match event with + | Event.LockAcquire lock_path -> + AccessPath.get_typ lock_path tenv |> Option.exists ~f:is_class_and_recursive_lock + | _ -> + false - let fold_over_events f map init = - let ff _ lock_state acc = List.fold lock_state ~init:acc ~f in - fold ff map init +(** skip adding an order pair [(_, event)] if + - we have no tenv, or, + - [event] is not a lock event, or, + - we do not hold the lock, or, + - the lock is not recursive. *) +let should_skip tenv_opt event lock_state = + Option.exists tenv_opt ~f:(fun tenv -> + LockState.is_lock_taken event lock_state && is_recursive_lock event tenv ) + + +module CriticalPairs = struct + include CriticalPair.FiniteSet + + let with_callsite astate tenv_opt lock_state call_site = + let existing_acquisitions = LockState.get_acquisitions lock_state in + fold + (fun ({elem= {event}} as critical_pair : CriticalPair.t) acc -> + if should_skip tenv_opt event lock_state then acc + else + let new_pair = + CriticalPair.with_callsite critical_pair existing_acquisitions call_site + in + add new_pair acc ) + astate empty end module UIThreadExplanationDomain = struct @@ -231,110 +351,81 @@ module GuardToLockMap = struct end type t = - { events: EventDomain.t - ; guard_map: GuardToLockMap.t + { guard_map: GuardToLockMap.t ; lock_state: LockState.t - ; order: OrderDomain.t + ; critical_pairs: CriticalPairs.t ; ui: UIThreadDomain.t } let bottom = - { events= EventDomain.empty - ; guard_map= GuardToLockMap.empty - ; lock_state= LockState.empty - ; order= OrderDomain.empty + { guard_map= GuardToLockMap.empty + ; lock_state= LockState.top + ; critical_pairs= CriticalPairs.empty ; ui= UIThreadDomain.bottom } -let is_bottom {events; guard_map; lock_state; order; ui} = - EventDomain.is_empty events && GuardToLockMap.is_empty guard_map && OrderDomain.is_empty order - && LockState.is_empty lock_state && UIThreadDomain.is_bottom ui +let is_bottom {guard_map; lock_state; critical_pairs; ui} = + GuardToLockMap.is_empty guard_map && LockState.is_top lock_state + && CriticalPairs.is_empty critical_pairs + && UIThreadDomain.is_bottom ui -let pp fmt {events; guard_map; lock_state; order; ui} = - F.fprintf fmt "{events= %a; guard_map= %a; lock_state= %a; order= %a; ui= %a}" EventDomain.pp - events GuardToLockMap.pp guard_map LockState.pp lock_state OrderDomain.pp order - UIThreadDomain.pp ui +let pp fmt {guard_map; lock_state; critical_pairs; ui} = + F.fprintf fmt "{guard_map= %a; lock_state= %a; critical_pairs= %a; ui= %a}" GuardToLockMap.pp + guard_map LockState.pp lock_state CriticalPairs.pp critical_pairs UIThreadDomain.pp ui let join lhs rhs = - { events= EventDomain.join lhs.events rhs.events - ; guard_map= GuardToLockMap.join lhs.guard_map rhs.guard_map + { guard_map= GuardToLockMap.join lhs.guard_map rhs.guard_map ; lock_state= LockState.join lhs.lock_state rhs.lock_state - ; order= OrderDomain.join lhs.order rhs.order + ; critical_pairs= CriticalPairs.join lhs.critical_pairs rhs.critical_pairs ; ui= UIThreadDomain.join lhs.ui rhs.ui } let widen ~prev ~next ~num_iters:_ = join prev next let ( <= ) ~lhs ~rhs = - EventDomain.( <= ) ~lhs:lhs.events ~rhs:rhs.events - && GuardToLockMap.( <= ) ~lhs:lhs.guard_map ~rhs:rhs.guard_map - && OrderDomain.( <= ) ~lhs:lhs.order ~rhs:rhs.order + GuardToLockMap.( <= ) ~lhs:lhs.guard_map ~rhs:rhs.guard_map && LockState.( <= ) ~lhs:lhs.lock_state ~rhs:rhs.lock_state + && CriticalPairs.( <= ) ~lhs:lhs.critical_pairs ~rhs:rhs.critical_pairs && UIThreadDomain.( <= ) ~lhs:lhs.ui ~rhs:rhs.ui -let is_recursive_lock event tenv = - let is_class_and_recursive_lock = function - | {Typ.desc= Tptr ({desc= Tstruct name}, _)} | {desc= Tstruct name} -> - ConcurrencyModels.is_recursive_lock_type name - | typ -> - L.debug Analysis Verbose "Asked if non-struct type %a is a recursive lock type.@." - (Typ.pp_full Pp.text) typ ; - true - in - match event with - | {Event.elem= LockAcquire lock_path} -> - AccessPath.get_typ lock_path tenv |> Option.exists ~f:is_class_and_recursive_lock - | _ -> - false - - -(** skip adding an order pair [(_, event)] if - - we have no tenv, or, - - [event] is not a lock event, or, - - we do not hold the lock, or, - - the lock is not recursive. *) -let should_skip tenv_opt event lock_state = - Option.exists tenv_opt ~f:(fun tenv -> - LockState.is_taken event lock_state && is_recursive_lock event tenv ) - - (* for every lock b held locally, add a pair (b, event) *) -let add_order_pairs tenv_opt lock_state event acc = +let add_critical_pair tenv_opt lock_state event ~loc acc = if should_skip tenv_opt event lock_state then acc else - let add_first_and_eventually acc ({elem= first; loc} : LockEvent.t) = - let new_elem = Order.make {first; eventually= event} loc in - OrderDomain.add new_elem acc - in - LockState.fold_over_events add_first_and_eventually lock_state acc + (* FIXME we should not do this repeatedly in the fold below *) + let acquisitions = LockState.get_acquisitions lock_state in + let critical_pair = CriticalPair.make ~loc acquisitions event in + CriticalPairs.add critical_pair acc -let acquire tenv ({lock_state; events; order} as astate) loc locks = - let new_events = List.map locks ~f:(fun lock -> Event.make_acquire lock loc) in +let acquire tenv ({lock_state; critical_pairs} as astate) ~procname ~loc locks = { astate with - events= List.fold new_events ~init:events ~f:(fun acc e -> EventDomain.add e acc) - ; order= - List.fold new_events ~init:order ~f:(fun acc e -> - OrderDomain.union acc (add_order_pairs (Some tenv) lock_state e order) ) - ; lock_state= List.fold locks ~init:lock_state ~f:(LockState.acquire loc) } + (* FIXME do one fold not two *) + critical_pairs= + List.fold locks ~init:critical_pairs ~f:(fun acc lock -> + let event = Event.make_acquire lock in + add_critical_pair (Some tenv) lock_state event ~loc acc ) + ; lock_state= + List.fold locks ~init:lock_state ~f:(fun acc lock -> + LockState.acquire ~procname ~loc lock acc ) } -let make_call_with_event tenv_opt new_event astate = +let make_call_with_event tenv_opt new_event ~loc astate = { astate with - events= EventDomain.add new_event astate.events - ; order= add_order_pairs tenv_opt astate.lock_state new_event astate.order } + critical_pairs= + add_critical_pair tenv_opt astate.lock_state new_event ~loc astate.critical_pairs } -let blocking_call callee sev loc astate = - let new_event = Event.make_blocking_call callee sev loc in - make_call_with_event None new_event astate +let blocking_call ~callee sev ~loc astate = + let new_event = Event.make_blocking_call callee sev in + make_call_with_event None new_event ~loc astate -let strict_mode_call callee loc astate = - let new_event = Event.make_strict_mode_call callee loc in - make_call_with_event None new_event astate +let strict_mode_call ~callee ~loc astate = + let new_event = Event.make_strict_mode_call callee in + make_call_with_event None new_event ~loc astate let release ({lock_state} as astate) locks = @@ -342,27 +433,19 @@ let release ({lock_state} as astate) locks = lock_state= List.fold locks ~init:lock_state ~f:(fun acc l -> LockState.release l acc) } -let integrate_summary tenv ({lock_state; events; order; ui} as astate) callee_pname loc - callee_summary = - let callsite = CallSite.make callee_pname loc in - let callee_order = OrderDomain.with_callsite callee_summary.order callsite in - let callee_ui = UIThreadDomain.with_callsite callee_summary.ui callsite in - let should_keep event = should_skip (Some tenv) event lock_state |> not in - let filtered_order = - OrderDomain.filter (fun {elem= {eventually}} -> should_keep eventually) callee_order - in - let callee_events = EventDomain.with_callsite callee_summary.events callsite in - let filtered_events = EventDomain.filter should_keep callee_events in - let order' = - EventDomain.fold (add_order_pairs (Some tenv) lock_state) filtered_events filtered_order +let integrate_summary tenv ~caller_summary:({lock_state; critical_pairs; ui} as astate) ~callee + ~loc ~callee_summary = + let callsite = CallSite.make callee loc in + let critical_pairs' = + CriticalPairs.with_callsite callee_summary.critical_pairs (Some tenv) lock_state callsite in + let callee_ui = UIThreadDomain.with_callsite callee_summary.ui callsite in { astate with - events= EventDomain.join events filtered_events - ; order= OrderDomain.join order order' + critical_pairs= CriticalPairs.join critical_pairs critical_pairs' ; ui= UIThreadDomain.join ui callee_ui } -let set_on_ui_thread ({ui} as astate) loc explain = +let set_on_ui_thread ({ui} as astate) ~loc explain = let ui = UIThreadDomain.join ui (AbstractDomain.Types.NonBottom (UIThreadExplanationDomain.make explain loc)) @@ -370,9 +453,9 @@ let set_on_ui_thread ({ui} as astate) loc explain = {astate with ui} -let add_guard tenv astate guard lock ~acquire_now loc = +let add_guard ~acquire_now ~procname ~loc tenv astate guard lock = let astate = {astate with guard_map= GuardToLockMap.add_guard ~guard ~lock astate.guard_map} in - if acquire_now then acquire tenv astate loc [lock] else astate + if acquire_now then acquire tenv astate ~procname ~loc [lock] else astate let remove_guard astate guard = @@ -389,10 +472,14 @@ let unlock_guard astate guard = FlatLock.get lock_opt |> Option.to_list |> release astate ) -let lock_guard tenv astate guard loc = +let lock_guard ~procname ~loc tenv astate guard = GuardToLockMap.find_opt guard astate.guard_map |> Option.value_map ~default:astate ~f:(fun lock_opt -> - FlatLock.get lock_opt |> Option.to_list |> acquire tenv astate loc ) + FlatLock.get lock_opt |> Option.to_list |> acquire tenv astate ~procname ~loc ) + + +let filter_blocking_calls ({critical_pairs} as astate) = + {astate with critical_pairs= CriticalPairs.filter CriticalPair.is_blocking_call critical_pairs} type summary = t diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index cbba142f3..a92da4a49 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -8,58 +8,67 @@ open! IStd module F = Format -(** Abstraction of a path that represents a lock, special-casing equality and comparisons +(** Abstraction of a path that represents a lock, special-casing comparison to work over type, base variable modulo this and access list *) module Lock : sig - include ExplicitTrace.Element with type t = AccessPath.t + include PrettyPrintable.PrintableOrderedType with type t = AccessPath.t val owner_class : t -> Typ.name option (** Class of the root variable of the path representing the lock *) - val equal : t -> t -> bool - val pp_locks : F.formatter -> t -> unit + + val describe : F.formatter -> t -> unit 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) - | StrictModeCall of string + type t = LockAcquire of Lock.t | MayBlock of (string * severity_t) | StrictModeCall of string [@@deriving compare] - include ExplicitTrace.TraceElem with type elem_t = event_t + val describe : F.formatter -> t -> unit +end - val make_trace : ?header:string -> Typ.Procname.t -> t -> Errlog.loc_trace +module LockState : AbstractDomain.WithTop + +(** A set of lock acquisitions with source locations and procnames. *) +module Acquisitions : sig + type t + + val lock_is_held : Lock.t -> t -> bool + (** is the given lock in the set *) end -module EventDomain : ExplicitTrace.FiniteSet with type elt = Event.t +(** An event and the currently-held locks at the time it occurred. *) +module CriticalPairElement : sig + type t = private {acquisitions: Acquisitions.t; event: Event.t} +end + +(** A [CriticalPairElement] equipped with a call stack. + The intuition is that if we have a critical pair `(locks, event)` in the summary + of a method then there is a trace of that method where `event` occurs, and right + before it occurs the locks held are exactly `locks` (no over/under approximation). + We call it "critical" because the information here alone determines deadlock conditions. +*) +module CriticalPair : sig + type t = private {elem: CriticalPairElement.t; loc: Location.t; trace: CallSite.t list} -(** Represents the existence of a program path to the [first] lock being taken in the current - method or, transitively, a callee *in the same class*, and, which continues (to potentially - another class) until the [eventually] event, schematically -->first-->eventually. - It is guaranteed that during the second part of the trace (first-->eventually) the lock [first] - is not released. *) -module Order : sig - type order_t = private {first: Lock.t; eventually: Event.t} + include PrettyPrintable.PrintableOrderedType with type t := t - include ExplicitTrace.TraceElem with type elem_t = order_t + val get_loc : t -> Location.t + (** outermost callsite location *) + + val get_earliest_lock_or_call_loc : procname:Typ.Procname.t -> t -> Location.t + (** outermost callsite location OR lock acquisition *) val may_deadlock : t -> t -> bool - (** check if two pairs are symmetric in terms of locks, where locks are compared modulo the - variable name at the root of each path. *) - val make_trace : ?header:string -> Typ.Procname.t -> t -> Errlog.loc_trace + val make_trace : + ?header:string -> ?include_acquisitions:bool -> Typ.Procname.t -> t -> Errlog.loc_trace end -module OrderDomain : ExplicitTrace.FiniteSet with type elt = Order.t - -module LockState : AbstractDomain.WithTop +module CriticalPairs : AbstractDomain.FiniteSetS with type elt = CriticalPair.t module UIThreadExplanationDomain : sig include ExplicitTrace.TraceElem with type elem_t = string @@ -74,32 +83,39 @@ module UIThreadDomain : module GuardToLockMap : AbstractDomain.WithTop type t = - { events: EventDomain.t - ; guard_map: GuardToLockMap.t + { guard_map: GuardToLockMap.t ; lock_state: LockState.t - ; order: OrderDomain.t + ; critical_pairs: CriticalPairs.t ; ui: UIThreadDomain.t } include AbstractDomain.WithBottom with type t := t -val acquire : Tenv.t -> t -> Location.t -> Lock.t list -> t +val acquire : Tenv.t -> t -> procname:Typ.Procname.t -> loc:Location.t -> Lock.t list -> t (** simultaneously acquire a number of locks, no-op if list is empty *) val release : t -> Lock.t list -> t (** simultaneously release a number of locks, no-op if list is empty *) -val blocking_call : Typ.Procname.t -> Event.severity_t -> Location.t -> t -> t +val blocking_call : callee:Typ.Procname.t -> Event.severity_t -> loc:Location.t -> t -> t -val strict_mode_call : Typ.Procname.t -> Location.t -> t -> t +val strict_mode_call : callee:Typ.Procname.t -> loc:Location.t -> t -> t -val set_on_ui_thread : t -> Location.t -> string -> t +val set_on_ui_thread : t -> loc:Location.t -> string -> t (** set the property "runs on UI thread" to true by attaching the given explanation string as to why this method is thought to do so *) -val add_guard : Tenv.t -> t -> HilExp.t -> Lock.t -> acquire_now:bool -> Location.t -> t +val add_guard : + acquire_now:bool + -> procname:Typ.Procname.t + -> loc:Location.t + -> Tenv.t + -> t + -> HilExp.t + -> Lock.t + -> t (** Install a mapping from the guard expression to the lock provided, and optionally lock it. *) -val lock_guard : Tenv.t -> t -> HilExp.t -> Location.t -> t +val lock_guard : procname:Typ.Procname.t -> loc:Location.t -> Tenv.t -> t -> HilExp.t -> t (** Acquire the lock the guard was constructed with. *) val remove_guard : t -> HilExp.t -> t @@ -112,4 +128,12 @@ type summary = t val pp_summary : F.formatter -> summary -> unit -val integrate_summary : Tenv.t -> t -> Typ.Procname.t -> Location.t -> summary -> t +val integrate_summary : + Tenv.t + -> caller_summary:t + -> callee:Typ.Procname.t + -> loc:Location.t + -> callee_summary:summary + -> t + +val filter_blocking_calls : t -> t diff --git a/infer/tests/codetoanalyze/java/starvation/MasterLock.java b/infer/tests/codetoanalyze/java/starvation/MasterLock.java index 354159036..31625d24c 100644 --- a/infer/tests/codetoanalyze/java/starvation/MasterLock.java +++ b/infer/tests/codetoanalyze/java/starvation/MasterLock.java @@ -29,7 +29,7 @@ class MasterLock { // both methods hold the master lock so cannot interleave // and thus cannot deadlock - void FP_oneWayOk() { + void oneWayOk() { synchronized (master) { synchronized (x) { synchronized (y) { @@ -38,7 +38,7 @@ class MasterLock { } } - void FP_theOtherWayOk() { + void theOtherWayOk() { synchronized (master) { synchronized (y) { synchronized (x) { diff --git a/infer/tests/codetoanalyze/java/starvation/issues.exp b/infer/tests/codetoanalyze/java/starvation/issues.exp index 30f305058..8ced2bc3a 100644 --- a/infer/tests/codetoanalyze/java/starvation/issues.exp +++ b/infer/tests/codetoanalyze/java/starvation/issues.exp @@ -25,8 +25,6 @@ codetoanalyze/java/starvation/LocklessTests.java, LocklessTestsB.locklessMethod( codetoanalyze/java/starvation/LocklessTests.java, LocklessTestsC.locklessMethod():void, 52, LOCKLESS_VIOLATION, no_bucket, ERROR, [`void LocklessTestsC.locklessMethod()`,Method call: `void LocklessTestsC.takeLock()`, locks `this` in `class LocklessTestsC`] codetoanalyze/java/starvation/MainThreadTest.java, AnnotatedClass.callTransactBad(MainThreadTest):void, 30, STARVATION, no_bucket, ERROR, [`void AnnotatedClass.callTransactBad(MainThreadTest)`,Method call: `void MainThreadTest.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void AnnotatedClass.callTransactBad(MainThreadTest)`,class `AnnotatedClass` is annotated `UiThread`] codetoanalyze/java/starvation/MainThreadTest.java, MainThreadTest.callTransactBad():void, 23, STARVATION, no_bucket, ERROR, [`void MainThreadTest.callTransactBad()`,Method call: `void MainThreadTest.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void MainThreadTest.callTransactBad()`,`void MainThreadTest.callTransactBad()` is annotated `UiThread`] -codetoanalyze/java/starvation/MasterLock.java, MasterLock.FP_oneWayOk():void, 34, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MasterLock.FP_oneWayOk()`, locks `this.x` in `class MasterLock`, locks `this.y` in `class MasterLock`,[Trace 2] `void MasterLock.FP_theOtherWayOk()`, locks `this.y` in `class MasterLock`, locks `this.x` in `class MasterLock`] -codetoanalyze/java/starvation/MasterLock.java, MasterLock.FP_theOtherWayOk():void, 43, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MasterLock.FP_theOtherWayOk()`, locks `this.y` in `class MasterLock`, locks `this.x` in `class MasterLock`,[Trace 2] `void MasterLock.FP_oneWayOk()`, locks `this.x` in `class MasterLock`, locks `this.y` in `class MasterLock`] codetoanalyze/java/starvation/MasterLock.java, MasterLock.oneWayBad():void, 14, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MasterLock.oneWayBad()`, locks `this.a` in `class MasterLock`, locks `this.b` in `class MasterLock`,[Trace 2] `void MasterLock.theOtherWayBad()`, locks `this.b` in `class MasterLock`, locks `this.a` in `class MasterLock`] codetoanalyze/java/starvation/MasterLock.java, MasterLock.theOtherWayBad():void, 22, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MasterLock.theOtherWayBad()`, locks `this.b` in `class MasterLock`, locks `this.a` in `class MasterLock`,[Trace 2] `void MasterLock.oneWayBad()`, locks `this.a` in `class MasterLock`, locks `this.b` in `class MasterLock`] codetoanalyze/java/starvation/MyActivity.java, MyActivity.onCreate(android.os.Bundle):void, 28, STARVATION, no_bucket, ERROR, [`void MyActivity.onCreate(Bundle)`,Method call: `void MyActivity.bad()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void MyActivity.onCreate(Bundle)`,`void MyActivity.onCreate(Bundle)` is a standard UI-thread method] @@ -38,7 +36,7 @@ codetoanalyze/java/starvation/MyActivity.java, MyActivity.onStart():void, 33, ST codetoanalyze/java/starvation/MyActivity.java, MyActivity.onStop():void, 53, STARVATION, no_bucket, ERROR, [`void MyActivity.onStop()`,Method call: `void MyActivity.bad()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void MyActivity.onStop()`,`void MyActivity.onStop()` is a standard UI-thread method] codetoanalyze/java/starvation/NonBlk.java, NonBlk.deadlockABBad():void, 33, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void NonBlk.deadlockABBad()`, locks `this` in `class NonBlk`, locks `this.future` in `class NonBlk`,[Trace 2] `void NonBlk.deadlockBABad()`, locks `this.future` in `class NonBlk`, locks `this` in `class NonBlk`] codetoanalyze/java/starvation/NonBlk.java, NonBlk.deadlockBABad():void, 40, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void NonBlk.deadlockBABad()`, locks `this.future` in `class NonBlk`, locks `this` in `class NonBlk`,[Trace 2] `void NonBlk.deadlockABBad()`, locks `this` in `class NonBlk`, locks `this.future` in `class NonBlk`] -codetoanalyze/java/starvation/ObjWait.java, ObjWait.indirectWaitOnMainWithoutTimeoutBad():void, 46, STARVATION, no_bucket, ERROR, [[Trace 1] `void ObjWait.indirectWaitOnMainWithoutTimeoutBad()`, locks `this.lock` in `class ObjWait`,[Trace 2] `void ObjWait.lockAndWaitOnAnyWithoutTimeoutBad()`, locks `this.lock` in `class ObjWait`,calls `void Object.wait()`,[Trace 1 on UI thread] `void ObjWait.indirectWaitOnMainWithoutTimeoutBad()`,`void ObjWait.indirectWaitOnMainWithoutTimeoutBad()` is annotated `UiThread`] +codetoanalyze/java/starvation/ObjWait.java, ObjWait.indirectWaitOnMainWithoutTimeoutBad():void, 46, STARVATION, no_bucket, ERROR, [[Trace 1] `void ObjWait.indirectWaitOnMainWithoutTimeoutBad()`, locks `this.lock` in `class ObjWait`,[Trace 2] `void ObjWait.lockAndWaitOnAnyWithoutTimeoutBad()`, locks `this.lock` in `class ObjWait`, locks `this.x` in `class ObjWait`,calls `void Object.wait()`,[Trace 1 on UI thread] `void ObjWait.indirectWaitOnMainWithoutTimeoutBad()`,`void ObjWait.indirectWaitOnMainWithoutTimeoutBad()` is annotated `UiThread`] codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithExcessiveTimeout1Bad():void, 31, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithExcessiveTimeout1Bad()`,calls `void Object.wait(long)`,[Trace on UI thread] `void ObjWait.waitOnMainWithExcessiveTimeout1Bad()`,`void ObjWait.waitOnMainWithExcessiveTimeout1Bad()` is annotated `UiThread`] codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithExcessiveTimeout2Bad():void, 38, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithExcessiveTimeout2Bad()`,calls `void Object.wait(long,int)`,[Trace on UI thread] `void ObjWait.waitOnMainWithExcessiveTimeout2Bad()`,`void ObjWait.waitOnMainWithExcessiveTimeout2Bad()` is annotated `UiThread`] codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithoutTimeoutBad():void, 24, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithoutTimeoutBad()`,calls `void Object.wait()`,[Trace on UI thread] `void ObjWait.waitOnMainWithoutTimeoutBad()`,`void ObjWait.waitOnMainWithoutTimeoutBad()` is annotated `UiThread`]