From 63586d98df355bf13586d682b5d4dfd345867691 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Wed, 23 Sep 2020 06:34:35 -0700 Subject: [PATCH] [starvation] make analysis work with sil instead of hil Summary: Subtle false positives and negatives in Hil make Sil preferable. This diff gets rid of the CFG-emulation of Hil, while still using Hil expressions. Reviewed By: da319 Differential Revision: D23815026 fbshipit-source-id: 731a6d299 --- infer/src/absint/AbstractDomain.ml | 2 +- infer/src/absint/AbstractDomain.mli | 2 +- infer/src/backend/StarvationGlobalAnalysis.ml | 2 +- infer/src/concurrency/starvation.ml | 176 ++++++++++++------ infer/src/concurrency/starvationDomain.ml | 86 +++++++-- infer/src/concurrency/starvationDomain.mli | 22 ++- .../java/starvation/ThreadDeadlock.java | 5 +- .../codetoanalyze/java/starvation/issues.exp | 2 - 8 files changed, 208 insertions(+), 89 deletions(-) diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index 2af92120d..b11f3541a 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -11,7 +11,7 @@ module F = Format module Types = struct type 'astate bottom_lifted = Bottom | NonBottom of 'astate - type 'astate top_lifted = Top | NonTop of 'astate + type 'astate top_lifted = Top | NonTop of 'astate [@@deriving equal] type ('below, 'astate, 'above) below_above = Below of 'below | Above of 'above | Val of 'astate end diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 4691c8055..f6a379885 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -12,7 +12,7 @@ open! IStd module Types : sig type 'astate bottom_lifted = Bottom | NonBottom of 'astate - type 'astate top_lifted = Top | NonTop of 'astate + type 'astate top_lifted = Top | NonTop of 'astate [@@deriving equal] type ('below, 'astate, 'above) below_above = Below of 'below | Above of 'above | Val of 'astate end diff --git a/infer/src/backend/StarvationGlobalAnalysis.ml b/infer/src/backend/StarvationGlobalAnalysis.ml index 6b89b8de5..ae3ec3db5 100644 --- a/infer/src/backend/StarvationGlobalAnalysis.ml +++ b/infer/src/backend/StarvationGlobalAnalysis.ml @@ -12,7 +12,7 @@ module Domain = StarvationDomain (* given a scheduled-work item, read the summary of the scheduled method from the disk and adapt its contents to the thread it was scheduled too *) let get_summary_of_scheduled_work (work_item : Domain.ScheduledWorkItem.t) = - let astate = {Domain.bottom with thread= work_item.thread} in + let astate = {Domain.initial with thread= work_item.thread} in let callsite = CallSite.make work_item.procname work_item.loc in let open IOption.Let_syntax in let* {Summary.payloads= {starvation}} = Summary.OnDisk.get work_item.procname in diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 825ede7f9..67852b358 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -28,6 +28,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct actuals + let hilexp_of_sil ~add_deref (astate : Domain.t) silexp typ = + let f_resolve_id var = Domain.VarDomain.get var astate.var_state in + HilExp.of_sil ~include_array_indexes:false ~f_resolve_id ~add_deref silexp typ + + + let hilexp_of_sils ~add_deref astate silexps = + List.map silexps ~f:(fun (exp, typ) -> hilexp_of_sil ~add_deref astate exp typ) + + let rec get_access_expr (hilexp : HilExp.t) = match hilexp with | AccessExpression access_exp -> @@ -56,12 +65,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {acc with attributes} ) in match HilExp.get_access_exprs assume_exp with - | [access_expr] when AttributeDomain.is_thread_guard access_expr astate.attributes -> - HilExp.eval_boolean_exp access_expr assume_exp - |> Option.fold ~init:astate ~f:add_thread_choice - | [access_expr] when AttributeDomain.is_future_done_guard access_expr astate.attributes -> - HilExp.eval_boolean_exp access_expr assume_exp - |> Option.fold ~init:astate ~f:(add_future_done_choice access_expr) + | [access_expr] -> + if AttributeDomain.is_thread_guard access_expr astate.attributes then + HilExp.eval_boolean_exp access_expr assume_exp + |> Option.fold ~init:astate ~f:add_thread_choice + else if AttributeDomain.is_future_done_guard access_expr astate.attributes then + HilExp.eval_boolean_exp access_expr assume_exp + |> Option.fold ~init:astate ~f:(add_future_done_choice access_expr) + else astate | _ -> astate @@ -214,8 +225,33 @@ module TransferFunctions (CFG : ProcCfg.S) = struct |> Option.value ~default:astate + let do_metadata (metadata : Sil.instr_metadata) astate = + match metadata with ExitScope (vars, _) -> Domain.remove_dead_vars astate vars | _ -> astate + + + let do_load tenv ~lhs rhs_exp rhs_typ (astate : Domain.t) = + let lhs_var = fst lhs in + let add_deref = match (lhs_var : Var.t) with LogicalVar _ -> true | ProgramVar _ -> false in + let rhs_hil_exp = hilexp_of_sil ~add_deref astate rhs_exp rhs_typ in + let astate = + get_access_expr rhs_hil_exp + |> Option.value_map ~default:astate ~f:(fun acc_exp -> + {astate with var_state= Domain.VarDomain.set lhs_var acc_exp astate.var_state} ) + in + let lhs_hil_acc_exp = HilExp.AccessExpression.base lhs in + do_assignment tenv lhs_hil_acc_exp rhs_hil_exp astate + + + let do_cast tenv id base_typ actuals astate = + match actuals with + | [(e, typ); _sizeof] -> + do_load tenv ~lhs:(Var.of_id id, base_typ) e typ astate + | _ -> + astate + + let exec_instr (astate : Domain.t) ({interproc= {proc_desc; tenv}; formals} as analysis_data) _ - (instr : HilInstr.t) = + instr = let open ConcurrencyModels in let open StarvationModels in let get_lock_path = Domain.Lock.make formals in @@ -225,68 +261,84 @@ module TransferFunctions (CFG : ProcCfg.S) = struct 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 - match instr with - | Assign (lhs_access_exp, rhs_exp, _) -> - do_assignment tenv lhs_access_exp rhs_exp astate - | Metadata (Sil.ExitScope (vars, _)) -> - {astate with attributes= Domain.AttributeDomain.exit_scope vars astate.attributes} - | Metadata _ -> - astate - | Assume (assume_exp, _, _, _) -> - do_assume assume_exp astate - | Call (_, Indirect _, _, _, _) -> + match (instr : Sil.instr) with + | Metadata metadata -> + do_metadata metadata astate + | Prune (exp, _loc, _then_branch, _if_kind) -> + let hil_exp = hilexp_of_sil ~add_deref:false astate exp Typ.boolean in + do_assume hil_exp astate + | Load {id} when Ident.is_none id -> astate - | Call (_, Direct callee, actuals, _, _) when should_skip_analysis tenv callee actuals -> + | Load {id; e; typ} -> + do_load tenv ~lhs:(Var.of_id id, typ) e typ astate + | Store {e1= Lvar lhs_pvar; typ; e2} when Pvar.is_ssa_frontend_tmp lhs_pvar -> + do_load tenv ~lhs:(Var.of_pvar lhs_pvar, typ) e2 typ astate + | Store {e1; typ; e2} -> + let rhs_hil_exp = hilexp_of_sil ~add_deref:false astate e2 typ in + hilexp_of_sil ~add_deref:true astate e1 (Typ.mk_ptr typ) + |> get_access_expr + |> Option.value_map ~default:astate ~f:(fun lhs_hil_acc_exp -> + do_assignment tenv lhs_hil_acc_exp rhs_hil_exp astate ) + | Call (_, Const (Cfun callee), actuals, _, _) + when should_skip_analysis tenv callee (hilexp_of_sils ~add_deref:false astate actuals) -> astate - | Call (ret_base, Direct callee, actuals, _, loc) -> ( - match get_lock_effect callee actuals with - | Lock locks -> - do_lock locks loc astate - | GuardLock guard -> - 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 ~procname ~loc - | None -> - log_parse_error "Couldn't parse lock in guard constructor" callee actuals ; - astate ) - | Unlock locks -> - do_unlock locks astate - | GuardUnlock guard -> - Domain.unlock_guard astate guard - | GuardDestroy guard -> - Domain.remove_guard astate guard - | LockedIfTrue _ | GuardLockedIfTrue _ -> - astate - | NoEffect when is_synchronized_library_call tenv callee -> - (* model a synchronized call without visible internal behaviour *) - let locks = List.hd actuals |> Option.to_list in - do_lock locks loc astate |> do_unlock locks - | NoEffect when is_java && is_strict_mode_violation tenv callee actuals -> - Domain.strict_mode_call ~callee ~loc astate - | NoEffect when is_java && is_monitor_wait tenv callee actuals -> - Domain.wait_on_monitor ~loc formals actuals astate - | NoEffect when is_java && is_future_get tenv callee actuals -> - Domain.future_get ~callee ~loc actuals astate - | NoEffect when is_java -> ( - let ret_exp = HilExp.AccessExpression.base ret_base in - let astate = do_work_scheduling tenv callee actuals loc astate in - match may_block tenv callee actuals with - | Some sev -> - Domain.blocking_call ~callee sev ~loc astate + | Call ((id, base_typ), Const (Cfun callee), actuals, _, _) + when Procname.equal callee BuiltinDecl.__cast -> + do_cast tenv id base_typ actuals astate + | Call ((id, typ), Const (Cfun callee), sil_actuals, loc, _) -> ( + let ret_base = (Var.of_id id, typ) in + let actuals = hilexp_of_sils ~add_deref:false astate sil_actuals in + match get_lock_effect callee actuals with + | Lock locks -> + do_lock locks loc astate + | GuardLock guard -> + 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 ~procname ~loc | None -> - do_call analysis_data ret_exp callee actuals loc astate ) - | NoEffect -> - (* in C++/Obj C we only care about deadlocks, not starvation errors *) - let ret_exp = HilExp.AccessExpression.base ret_base in - do_call analysis_data ret_exp callee actuals loc astate ) + log_parse_error "Couldn't parse lock in guard constructor" callee actuals ; + astate ) + | Unlock locks -> + do_unlock locks astate + | GuardUnlock guard -> + Domain.unlock_guard astate guard + | GuardDestroy guard -> + Domain.remove_guard astate guard + | LockedIfTrue _ | GuardLockedIfTrue _ -> + astate + | NoEffect when is_synchronized_library_call tenv callee -> + (* model a synchronized call without visible internal behaviour *) + let locks = List.hd actuals |> Option.to_list in + do_lock locks loc astate |> do_unlock locks + | NoEffect when is_java && is_strict_mode_violation tenv callee actuals -> + Domain.strict_mode_call ~callee ~loc astate + | NoEffect when is_java && is_monitor_wait tenv callee actuals -> + Domain.wait_on_monitor ~loc formals actuals astate + | NoEffect when is_java && is_future_get tenv callee actuals -> + Domain.future_get ~callee ~loc actuals astate + | NoEffect when is_java -> ( + let ret_exp = HilExp.AccessExpression.base ret_base in + let astate = do_work_scheduling tenv callee actuals loc astate in + match may_block tenv callee actuals with + | Some sev -> + Domain.blocking_call ~callee sev ~loc astate + | None -> + do_call analysis_data ret_exp callee actuals loc astate ) + | NoEffect -> + (* in C++/Obj C we only care about deadlocks, not starvation errors *) + let ret_exp = HilExp.AccessExpression.base ret_base in + do_call analysis_data ret_exp callee actuals loc astate ) + | Call ((id, _), _, _, _, _) -> + (* call havocs LHS *) + Domain.remove_dead_vars astate [Var.of_id id] let pp_session_name _node fmt = F.pp_print_string fmt "starvation" end -module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Normal)) +module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Normal)) (** Compute the attributes (of static variables) set up by the class initializer. *) let set_class_init_attributes procname (astate : Domain.t) = @@ -378,7 +430,7 @@ let analyze_procedure ({InterproceduralAnalysis.proc_desc; tenv} as interproc) = else Fn.id in let initial = - Domain.bottom + Domain.initial (* set the attributes of instance variables set up by all constructors or the class initializer *) |> set_initial_attributes interproc |> set_lock_state_for_synchronized_proc |> set_thread_status_by_annotation diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 55befc542..487d65cc3 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -109,6 +109,54 @@ module Lock = struct String.compare (mk_str t1) (mk_str t2) end +module AccessExpressionDomain = struct + open AbstractDomain.Types + + type t = HilExp.AccessExpression.t top_lifted [@@deriving equal] + + let pp fmt = function + | Top -> + F.pp_print_string fmt "AccExpTop" + | NonTop lock -> + HilExp.AccessExpression.pp fmt lock + + + let top = Top + + let is_top = function Top -> true | NonTop _ -> false + + let join lhs rhs = if equal lhs rhs then lhs else top + + let leq ~lhs ~rhs = equal (join lhs rhs) rhs + + let widen ~prev ~next ~num_iters:_ = join prev next +end + +module VarDomain = struct + include AbstractDomain.SafeInvertedMap (Var) (AccessExpressionDomain) + + let exit_scope init deadvars = + List.fold deadvars ~init ~f:(fun acc deadvar -> + filter + (fun _key acc_exp_opt -> + match acc_exp_opt with + | Top -> + (* should never happen in a safe inverted map *) + false + | NonTop acc_exp -> + let var, _ = HilExp.AccessExpression.get_base acc_exp in + not (Var.equal var deadvar) ) + acc + |> remove deadvar ) + + + let get var astate = + match find_opt var astate with None | Some Top -> None | Some (NonTop x) -> Some x + + + let set var acc_exp astate = add var (NonTop acc_exp) astate +end + module Event = struct type t = | LockAcquire of Lock.t @@ -598,33 +646,26 @@ type t = ; critical_pairs: CriticalPairs.t ; attributes: AttributeDomain.t ; thread: ThreadDomain.t - ; scheduled_work: ScheduledWorkDomain.t } + ; scheduled_work: ScheduledWorkDomain.t + ; var_state: VarDomain.t } -let bottom = +let initial = { guard_map= GuardToLockMap.empty ; lock_state= LockState.top ; critical_pairs= CriticalPairs.empty ; attributes= AttributeDomain.empty ; thread= ThreadDomain.bottom - ; scheduled_work= ScheduledWorkDomain.bottom } - - -let is_bottom astate = - GuardToLockMap.is_empty astate.guard_map - && LockState.is_top astate.lock_state - && CriticalPairs.is_empty astate.critical_pairs - && AttributeDomain.is_top astate.attributes - && ThreadDomain.is_bottom astate.thread - && ScheduledWorkDomain.is_bottom astate.scheduled_work + ; scheduled_work= ScheduledWorkDomain.bottom + ; var_state= VarDomain.top } let pp fmt astate = F.fprintf fmt "{guard_map= %a; lock_state= %a; critical_pairs= %a; attributes= %a; thread= %a; \ - scheduled_work= %a}" + scheduled_work= %a; var_state= %a}" GuardToLockMap.pp astate.guard_map LockState.pp astate.lock_state CriticalPairs.pp astate.critical_pairs AttributeDomain.pp astate.attributes ThreadDomain.pp astate.thread - ScheduledWorkDomain.pp astate.scheduled_work + ScheduledWorkDomain.pp astate.scheduled_work VarDomain.pp astate.var_state let join lhs rhs = @@ -633,7 +674,8 @@ let join lhs rhs = ; critical_pairs= CriticalPairs.join lhs.critical_pairs rhs.critical_pairs ; attributes= AttributeDomain.join lhs.attributes rhs.attributes ; thread= ThreadDomain.join lhs.thread rhs.thread - ; scheduled_work= ScheduledWorkDomain.join lhs.scheduled_work rhs.scheduled_work } + ; scheduled_work= ScheduledWorkDomain.join lhs.scheduled_work rhs.scheduled_work + ; var_state= VarDomain.join lhs.var_state rhs.var_state } let widen ~prev ~next ~num_iters:_ = join prev next @@ -645,6 +687,7 @@ let leq ~lhs ~rhs = && AttributeDomain.leq ~lhs:lhs.attributes ~rhs:rhs.attributes && ThreadDomain.leq ~lhs:lhs.thread ~rhs:rhs.thread && ScheduledWorkDomain.leq ~lhs:lhs.scheduled_work ~rhs:rhs.scheduled_work + && VarDomain.leq ~lhs:lhs.var_state ~rhs:rhs.var_state let add_critical_pair ?tenv lock_state event thread ~loc acc = @@ -825,3 +868,16 @@ let summary_of_astate : Procdesc.t -> t -> summary = ; scheduled_work= astate.scheduled_work ; attributes ; return_attribute } + + +let remove_dead_vars (astate : t) deadvars = + let deadvars = + (* The liveness analysis will kill any variable (such as [this]) immediately after its + last use. This is bad for attributes that need to live until the end of the method, + so we restrict to SSA variables. *) + List.rev_filter deadvars ~f:(fun (v : Var.t) -> + match v with LogicalVar _ -> true | ProgramVar pvar -> Pvar.is_ssa_frontend_tmp pvar ) + in + let var_state = VarDomain.exit_scope astate.var_state deadvars in + let attributes = AttributeDomain.exit_scope deadvars astate.attributes in + {astate with var_state; attributes} diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 168a2ec79..c5807945f 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -45,6 +45,16 @@ module Lock : sig (** a stable order for avoiding reporting deadlocks twice based on the root variable type *) end +module VarDomain : sig + include AbstractDomain.WithTop + + type key = Var.t + + val get : key -> t -> HilExp.AccessExpression.t option + + val set : key -> HilExp.AccessExpression.t -> t -> t +end + module Event : sig type t = | LockAcquire of Lock.t @@ -140,8 +150,6 @@ module AttributeDomain : sig val is_future_done_guard : HilExp.AccessExpression.t -> t -> bool (** does the given expr has attribute [FutureDone x] return [Some x] else [None] *) - - val exit_scope : Var.t list -> t -> t end (** A record of scheduled parallel work: the method scheduled to run, where, and on what thread. *) @@ -159,9 +167,13 @@ type t = ; critical_pairs: CriticalPairs.t ; attributes: AttributeDomain.t ; thread: ThreadDomain.t - ; scheduled_work: ScheduledWorkDomain.t } + ; scheduled_work: ScheduledWorkDomain.t + ; var_state: VarDomain.t } -include AbstractDomain.WithBottom with type t := t +include AbstractDomain.S with type t := t + +val initial : t +(** initial domain state *) val acquire : ?tenv:Tenv.t -> t -> procname:Procname.t -> loc:Location.t -> Lock.t list -> t (** simultaneously acquire a number of locks, no-op if list is empty *) @@ -226,3 +238,5 @@ val integrate_summary : val summary_of_astate : Procdesc.t -> t -> summary val filter_blocking_calls : t -> t + +val remove_dead_vars : t -> Var.t list -> t diff --git a/infer/tests/codetoanalyze/java/starvation/ThreadDeadlock.java b/infer/tests/codetoanalyze/java/starvation/ThreadDeadlock.java index 886445795..2c79f11cb 100644 --- a/infer/tests/codetoanalyze/java/starvation/ThreadDeadlock.java +++ b/infer/tests/codetoanalyze/java/starvation/ThreadDeadlock.java @@ -82,17 +82,16 @@ class ThreadDeadlock { Object lockE, lockF, lockG; - public void FP_sequentialEandGOk() { + public void sequentialEandGOk() { synchronized (lockE) { synchronized (lockF) { } } - // at this point we still believe lockE is held synchronized (lockG) { } } - public void FP_nestedGthenEOk() { + public void nestedGthenEOk() { synchronized (lockG) { synchronized (lockE) { } diff --git a/infer/tests/codetoanalyze/java/starvation/issues.exp b/infer/tests/codetoanalyze/java/starvation/issues.exp index 4a391b274..287043e72 100644 --- a/infer/tests/codetoanalyze/java/starvation/issues.exp +++ b/infer/tests/codetoanalyze/java/starvation/issues.exp @@ -78,8 +78,6 @@ codetoanalyze/java/starvation/ThreadCalls.java, ThreadCalls.indirectJoinOnUIThre codetoanalyze/java/starvation/ThreadCalls.java, ThreadCalls.indirectSleepOnUIThreadBad():void, 24, STARVATION, no_bucket, ERROR, [[Trace 1] `void ThreadCalls.indirectSleepOnUIThreadBad()`, locks `this.lock` in `class ThreadCalls`,[Trace 2] `void ThreadCalls.lockAndSleepOnNonUIThread()`, locks `this.lock` in `class ThreadCalls`,Method call: `void ThreadCalls.sleepOnAnyThreadOk()`,calls `void Thread.sleep(long)`] codetoanalyze/java/starvation/ThreadCalls.java, ThreadCalls.joinOnUIThreadBad(java.lang.Thread):void, 40, STARVATION, no_bucket, ERROR, [`void ThreadCalls.joinOnUIThreadBad(Thread)`,calls `void Thread.join()`] codetoanalyze/java/starvation/ThreadCalls.java, ThreadCalls.sleepOnUIThreadBad():void, 17, STARVATION, no_bucket, ERROR, [`void ThreadCalls.sleepOnUIThreadBad()`,calls `void Thread.sleep(long)`] -codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.FP_nestedGthenEOk():void, 96, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.FP_nestedGthenEOk()`, locks `this.lockG` in `class ThreadDeadlock`, locks `this.lockE` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.FP_sequentialEandGOk()`, locks `this.lockE` in `class ThreadDeadlock`, locks `this.lockG` in `class ThreadDeadlock`] -codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.FP_sequentialEandGOk():void, 86, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.FP_sequentialEandGOk()`, locks `this.lockE` in `class ThreadDeadlock`, locks `this.lockG` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.FP_nestedGthenEOk()`, locks `this.lockG` in `class ThreadDeadlock`, locks `this.lockE` in `class ThreadDeadlock`] codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.annotatedUiThreadBad():void, 35, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.annotatedUiThreadBad()`, locks `this` in `class ThreadDeadlock`, locks `this.lockB` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.annotatedWorkerThreadBad()`, locks `this.lockB` in `class ThreadDeadlock`, locks `this` in `class ThreadDeadlock`] codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.annotatedWorkerThreadBad():void, 42, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.annotatedWorkerThreadBad()`, locks `this.lockB` in `class ThreadDeadlock`, locks `this` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.annotatedUiThreadBad()`, locks `this` in `class ThreadDeadlock`, locks `this.lockB` in `class ThreadDeadlock`] codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.assertOnBackgroundThreadBad():void, 60, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.assertOnBackgroundThreadBad()`, locks `this.lockC` in `class ThreadDeadlock`, locks `this` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.assertOnUIThreadBad()`, locks `this` in `class ThreadDeadlock`, locks `this.lockC` in `class ThreadDeadlock`]