[starvation] substitute arguments over parameters in locks

Reviewed By: skcho

Differential Revision: D19374478

fbshipit-source-id: 48f59327d

infer/src/absint/FormalMap.ml

@@ -39,3 +39,7 @@ let get_formal_base index t =
 let get_formals_indexes = AccessPath.BaseMap.bindings
 
 let pp = AccessPath.BaseMap.pp ~pp_value:Int.pp
+
+let cardinal = AccessPath.BaseMap.cardinal
+
+let iter = AccessPath.BaseMap.iter

infer/src/absint/FormalMap.mli

@@ -31,3 +31,7 @@ val get_formals_indexes : t -> (AccessPath.base * int) list
 (** Get a list of (base * index) pairs. Note: these are sorted by base, not index *)
 
 val pp : F.formatter -> t -> unit [@@warning "-32"]
+
+val cardinal : t -> int
+
+val iter : (AccessPath.base -> int -> unit) -> t -> unit

infer/src/concurrency/starvation.ml

@@ -117,7 +117,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
            {astate with attributes} )
 
 
-  let do_call ProcData.{tenv; summary} lhs callee actuals loc (astate : Domain.t) =
+  let do_call ProcData.{tenv; summary; extras} lhs callee actuals loc (astate : Domain.t) =
     let open Domain in
     let make_ret_attr return_attribute = {empty_summary with return_attribute} in
     let make_thread thread = {empty_summary with thread} in
@@ -198,14 +198,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     (* constructor calls are special-cased because they side-effect the receiver and do not
        return anything *)
     let treat_modeled_summaries () =
-      let callsite = CallSite.make callee loc in
       IList.eval_until_first_some
         [ get_returned_executor_summary
         ; get_thread_assert_summary
         ; get_future_is_done_summary
         ; get_mainLooper_summary
         ; get_callee_summary ]
-      |> Option.map ~f:(Domain.integrate_summary ~tenv ~lhs callsite astate)
+      |> Option.map ~f:(fun summary ->
+             let subst = Lock.make_subst extras actuals in
+             let callsite = CallSite.make callee loc in
+             Domain.integrate_summary ~tenv ~lhs ~subst callsite astate summary )
     in
     IList.eval_until_first_some
       [treat_handler_constructor; treat_thread_constructor; treat_assume; treat_modeled_summaries]

infer/src/concurrency/starvationDomain.ml

@@ -220,6 +220,42 @@ module Lock = struct
   let compare_wrt_reporting {path= (_, typ1), _} {path= (_, typ2), _} =
     (* use string comparison on types as a stable order to decide whether to report a deadlock *)
     String.compare (Typ.to_string typ1) (Typ.to_string typ2)
+
+
+  (** A substitution from formal position indices to actuals. Since we only care about locks, use
+      [None] to denote an argument that cannot be resolved to a lock object. *)
+  type subst = t option Array.t
+
+  let[@warning "-32"] pp_subst fmt subst =
+    PrettyPrintable.pp_collection fmt ~pp_item:(Pp.option pp) (Array.to_list subst)
+
+
+  let make_subst formal_map actuals =
+    let actuals = Array.of_list actuals in
+    let len =
+      (* deal with var args functions *)
+      Int.max (FormalMap.cardinal formal_map) (Array.length actuals)
+    in
+    let subst = Array.create ~len None in
+    FormalMap.iter
+      (fun _base idx ->
+        if idx < Array.length actuals then subst.(idx) <- make formal_map actuals.(idx) )
+      formal_map ;
+    subst
+
+
+  let apply_subst (subst : subst) lock =
+    match lock.root with
+    | Global _ | Class _ ->
+        Some lock
+    | Parameter index -> (
+      try
+        match subst.(index) with
+        | None ->
+            None
+        | Some actual ->
+            Some {actual with path= AccessPath.append actual.path (snd lock.path)}
+      with Invalid_argument _ -> None )
 end
 
 module Event = struct
@@ -258,6 +294,26 @@ module Event = struct
   let make_strict_mode_call callee = StrictModeCall callee
 
   let make_object_wait lock = MonitorWait lock
+
+  let apply_subst subst event =
+    let make_monitor_wait lock = MonitorWait lock in
+    let make_lock_acquire lock = LockAcquire lock in
+    let apply_subst_aux make lock =
+      match Lock.apply_subst subst lock with
+      | None ->
+          None
+      | Some lock' when phys_equal lock lock' ->
+          Some event
+      | Some lock' ->
+          Some (make lock')
+    in
+    match event with
+    | MonitorWait lock ->
+        apply_subst_aux make_monitor_wait lock
+    | LockAcquire lock ->
+        apply_subst_aux make_lock_acquire lock
+    | MayBlock _ | StrictModeCall _ ->
+        Some event
 end
 
 (** A lock acquisition with source location and procname in which it occurs. The location & procname
@@ -280,6 +336,15 @@ module Acquisition = struct
 
 
   let make_dummy lock = {lock; loc= Location.dummy; procname= Procname.Linters_dummy_method}
+
+  let apply_subst subst acquisition =
+    match Lock.apply_subst subst acquisition.lock with
+    | None ->
+        None
+    | Some lock when phys_equal acquisition.lock lock ->
+        Some acquisition
+    | Some lock ->
+        Some {acquisition with lock}
 end
 
 (** Set of acquisitions; due to order over acquisitions, each lock appears at most once. *)
@@ -295,6 +360,13 @@ module Acquisitions = struct
 
   let no_locks_common_across_threads tenv acqs1 acqs2 =
     for_all (fun acq1 -> not (lock_is_held_in_other_thread tenv acq1.lock acqs2)) acqs1
+
+
+  let apply_subst subst acqs =
+    fold
+      (fun acq acc ->
+        match Acquisition.apply_subst subst acq with None -> acc | Some acq' -> add acq' acc )
+      acqs empty
 end
 
 module LockState : sig
@@ -409,8 +481,32 @@ module CriticalPairElement = struct
 
 
   let describe = pp
+
+  let apply_subst subst elem =
+    match Event.apply_subst subst elem.event with
+    | None ->
+        None
+    | Some event' ->
+        let acquisitions' = Acquisitions.apply_subst subst elem.acquisitions in
+        Some {elem with acquisitions= acquisitions'; event= event'}
 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.path tenv |> Option.exists ~f:is_class_and_recursive_lock
+  | _ ->
+      false
+
+
 module CriticalPair = struct
   include ExplicitTrace.MakeTraceElem (CriticalPairElement) (ExplicitTrace.DefaultCallPrinter)
 
@@ -433,15 +529,42 @@ module CriticalPair = struct
                    pair2.acquisitions )
 
 
-  let integrate_summary_opt existing_acquisitions call_site (caller_thread : ThreadDomain.t)
+  let apply_subst subst pair =
-      (callee_pair : t) =
+    match CriticalPairElement.apply_subst subst pair.elem with
-    ThreadDomain.apply_to_pair caller_thread callee_pair.elem.thread
+    | None ->
-    |> Option.map ~f:(fun thread ->
+        None
-           let f (elem : CriticalPairElement.t) =
+    | Some elem' ->
-             let acquisitions = Acquisitions.union existing_acquisitions elem.acquisitions in
+        Some (map ~f:(fun _elem -> elem') pair)
-             ({elem with acquisitions; thread} : elem_t)
+
-           in
+
-           with_callsite (map ~f callee_pair) call_site )
+  let integrate_summary_opt ?subst ?tenv existing_acquisitions call_site
+      (caller_thread : ThreadDomain.t) (callee_pair : t) =
+    let substitute_pair subst callee_pair =
+      match subst with None -> Some callee_pair | Some subst -> apply_subst subst callee_pair
+    in
+    let filter_out_reentrant_relock callee_pair =
+      match tenv with
+      | None ->
+          Some callee_pair
+      | Some tenv
+        when get_final_acquire callee_pair
+             |> Option.for_all ~f:(fun lock ->
+                    (not (Acquisitions.lock_is_held lock existing_acquisitions))
+                    || not (is_recursive_lock callee_pair.elem.event tenv) ) ->
+          Some callee_pair
+      | _ ->
+          None
+    in
+    substitute_pair subst callee_pair
+    |> Option.bind ~f:filter_out_reentrant_relock
+    |> Option.bind ~f:(fun callee_pair ->
+           ThreadDomain.apply_to_pair caller_thread callee_pair.elem.thread
+           |> Option.map ~f:(fun thread ->
+                  let f (elem : CriticalPairElement.t) =
+                    let acquisitions = Acquisitions.union existing_acquisitions elem.acquisitions in
+                    ({elem with acquisitions; thread} : elem_t)
+                  in
+                  with_callsite (map ~f callee_pair) call_site ) )
 
 
   let get_earliest_lock_or_call_loc ~procname ({elem= {acquisitions}} as t) =
@@ -506,22 +629,6 @@ module CriticalPair = struct
   let can_run_in_parallel t1 t2 = ThreadDomain.can_run_in_parallel t1.elem.thread t2.elem.thread
 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.path tenv |> Option.exists ~f:is_class_and_recursive_lock
-  | _ ->
-      false
-
-
 (** skip adding an order pair [(_, event)] if
 
     - we have no tenv, or,
@@ -536,14 +643,15 @@ let should_skip ?tenv event lock_state =
 module CriticalPairs = struct
   include CriticalPair.FiniteSet
 
-  let with_callsite astate ?tenv lock_state call_site thread =
+  let with_callsite astate ?tenv ?subst lock_state call_site thread =
     let existing_acquisitions = LockState.get_acquisitions lock_state in
     fold
-      (fun ({elem= {event}} as critical_pair : CriticalPair.t) acc ->
+      (fun critical_pair acc ->
-        if should_skip ?tenv event lock_state then acc
+        CriticalPair.integrate_summary_opt ?subst ?tenv existing_acquisitions call_site thread
-        else
+          critical_pair
-          CriticalPair.integrate_summary_opt existing_acquisitions call_site thread critical_pair
+        |> Option.fold ~init:acc ~f:(fun acc (new_pair : CriticalPair.t) ->
-          |> Option.fold ~init:acc ~f:(fun acc new_pair -> add new_pair acc) )
+               if should_skip ?tenv new_pair.elem.event lock_state then acc else add new_pair acc )
+        )
       astate empty
 end
 
@@ -820,9 +928,9 @@ let pp_summary fmt (summary : summary) =
     AttributeDomain.pp summary.attributes
 
 
-let integrate_summary ?tenv ?lhs callsite (astate : t) (summary : summary) =
+let integrate_summary ?tenv ?lhs ?subst callsite (astate : t) (summary : summary) =
   let critical_pairs' =
-    CriticalPairs.with_callsite summary.critical_pairs ?tenv astate.lock_state callsite
+    CriticalPairs.with_callsite summary.critical_pairs ?tenv ?subst astate.lock_state callsite
       astate.thread
   in
   { astate with

infer/src/concurrency/starvationDomain.mli

@@ -58,6 +58,11 @@ module Lock : sig
 
   val compare_wrt_reporting : t -> t -> int
   (** a stable order for avoiding reporting deadlocks twice based on the root variable type *)
+
+  (** substitution type : a map from (0-based) positional index to lock options *)
+  type subst
+
+  val make_subst : FormalMap.t -> HilExp.t list -> subst
 end
 
 module Event : sig
@@ -228,7 +233,13 @@ val empty_summary : summary
 val pp_summary : F.formatter -> summary -> unit
 
 val integrate_summary :
-  ?tenv:Tenv.t -> ?lhs:HilExp.AccessExpression.t -> CallSite.t -> t -> summary -> t
+     ?tenv:Tenv.t
+  -> ?lhs:HilExp.AccessExpression.t
+  -> ?subst:Lock.subst
+  -> CallSite.t
+  -> t
+  -> summary
+  -> t
 (** apply a callee summary to the current abstract state; [lhs] is the expression assigned the
     returned value, if any *)
 

infer/tests/codetoanalyze/cpp/starvation/crossfile-1.cpp

@@ -8,9 +8,9 @@
 #include "crossfile-1.h"
 
 // a deadlock should be reported here
-void CrossFileOne::lock_my_mutex_first_then_the_other() {
+void CrossFileOne::lock_my_mutex_first_then_the_other(CrossFileTwo* other) {
   _mutex.lock();
-  _other->just_lock_my_mutex();
+  other->just_lock_my_mutex();
   _mutex.unlock();
 }
 

infer/tests/codetoanalyze/cpp/starvation/crossfile-1.h

@@ -22,12 +22,11 @@ class CrossFileOne;
 class CrossFileOne {
  public:
   CrossFileOne() {}
-  void lock_my_mutex_first_then_the_other();
+  void lock_my_mutex_first_then_the_other(CrossFileTwo* other);
   void just_lock_my_mutex();
 
  private:
   std::mutex _mutex;
-  CrossFileTwo* _other;
 };
 
 #endif

infer/tests/codetoanalyze/cpp/starvation/crossfile-2.cpp

@@ -8,9 +8,9 @@
 #include "crossfile-2.h"
 
 // a deadlock should be reported here
-void CrossFileTwo::lock_my_mutex_first_then_the_other() {
+void CrossFileTwo::lock_my_mutex_first_then_the_other(CrossFileOne* other) {
   _mutex.lock();
-  _other->just_lock_my_mutex();
+  other->just_lock_my_mutex();
   _mutex.unlock();
 }
 

infer/tests/codetoanalyze/cpp/starvation/crossfile-2.h

@@ -20,12 +20,11 @@ class CrossFileTwo;
 class CrossFileTwo {
  public:
   CrossFileTwo() {}
-  void lock_my_mutex_first_then_the_other();
+  void lock_my_mutex_first_then_the_other(CrossFileOne* other);
   void just_lock_my_mutex();
 
  private:
   std::mutex _mutex;
-  CrossFileOne* _other;
 };
 
 #endif

infer/tests/codetoanalyze/cpp/starvation/issues.exp

@@ -6,8 +6,8 @@ codetoanalyze/cpp/starvation/basics.cpp, basics::SelfDeadlock::interproc1_bad, 1
 codetoanalyze/cpp/starvation/basics.cpp, basics::SelfDeadlock::thread_bad, 105, DEADLOCK, no_bucket, ERROR, [In method `basics::SelfDeadlock::thread_bad`, locks `this.mutex_` in `class basics::SelfDeadlock`, locks `this.mutex_` in `class basics::SelfDeadlock`]
 codetoanalyze/cpp/starvation/basics.cpp, basics::WithGuard::thread1_bad, 44, DEADLOCK, no_bucket, ERROR, [[Trace 1] `basics::WithGuard::thread1_bad`, locks `this.mutex_1` in `class basics::WithGuard`, locks `this.mutex_2` in `class basics::WithGuard`,[Trace 2] `basics::WithGuard::thread2_bad`, locks `this.mutex_2` in `class basics::WithGuard`, locks `this.mutex_1` in `class basics::WithGuard`]
 codetoanalyze/cpp/starvation/basics.cpp, basics::WithGuard::thread2_bad, 49, DEADLOCK, no_bucket, ERROR, [[Trace 1] `basics::WithGuard::thread2_bad`, locks `this.mutex_2` in `class basics::WithGuard`, locks `this.mutex_1` in `class basics::WithGuard`,[Trace 2] `basics::WithGuard::thread1_bad`, locks `this.mutex_1` in `class basics::WithGuard`, locks `this.mutex_2` in `class basics::WithGuard`]
-codetoanalyze/cpp/starvation/crossfile-1.cpp, CrossFileOne::lock_my_mutex_first_then_the_other, 12, DEADLOCK, no_bucket, ERROR, [[Trace 1] `CrossFileOne::lock_my_mutex_first_then_the_other`, locks `this._mutex` in `class CrossFileOne`,Method call: `CrossFileTwo::just_lock_my_mutex`, locks `this._mutex` in `class CrossFileTwo`,[Trace 2] `CrossFileTwo::lock_my_mutex_first_then_the_other`, locks `this._mutex` in `class CrossFileTwo`,Method call: `CrossFileOne::just_lock_my_mutex`, locks `this._mutex` in `class CrossFileOne`]
+codetoanalyze/cpp/starvation/crossfile-1.cpp, CrossFileOne::lock_my_mutex_first_then_the_other, 12, DEADLOCK, no_bucket, ERROR, [[Trace 1] `CrossFileOne::lock_my_mutex_first_then_the_other`, locks `this._mutex` in `class CrossFileOne`,Method call: `CrossFileTwo::just_lock_my_mutex`, locks `other._mutex` in `class CrossFileTwo`,[Trace 2] `CrossFileTwo::lock_my_mutex_first_then_the_other`, locks `this._mutex` in `class CrossFileTwo`,Method call: `CrossFileOne::just_lock_my_mutex`, locks `other._mutex` in `class CrossFileOne`]
-codetoanalyze/cpp/starvation/crossfile-2.cpp, CrossFileTwo::lock_my_mutex_first_then_the_other, 12, DEADLOCK, no_bucket, ERROR, [[Trace 1] `CrossFileTwo::lock_my_mutex_first_then_the_other`, locks `this._mutex` in `class CrossFileTwo`,Method call: `CrossFileOne::just_lock_my_mutex`, locks `this._mutex` in `class CrossFileOne`,[Trace 2] `CrossFileOne::lock_my_mutex_first_then_the_other`, locks `this._mutex` in `class CrossFileOne`,Method call: `CrossFileTwo::just_lock_my_mutex`, locks `this._mutex` in `class CrossFileTwo`]
+codetoanalyze/cpp/starvation/crossfile-2.cpp, CrossFileTwo::lock_my_mutex_first_then_the_other, 12, DEADLOCK, no_bucket, ERROR, [[Trace 1] `CrossFileTwo::lock_my_mutex_first_then_the_other`, locks `this._mutex` in `class CrossFileTwo`,Method call: `CrossFileOne::just_lock_my_mutex`, locks `other._mutex` in `class CrossFileOne`,[Trace 2] `CrossFileOne::lock_my_mutex_first_then_the_other`, locks `this._mutex` in `class CrossFileOne`,Method call: `CrossFileTwo::just_lock_my_mutex`, locks `other._mutex` in `class CrossFileTwo`]
 codetoanalyze/cpp/starvation/skip.cpp, skipped::Skip::not_skipped_bad, 19, DEADLOCK, no_bucket, ERROR, [In method `skipped::Skip::not_skipped_bad`,Method call: `skipped::Skip::private_deadlock`, locks `this.mutex_` in `class skipped::Skip`, locks `this.mutex_` in `class skipped::Skip`]
 codetoanalyze/cpp/starvation/skip.cpp, skipped::SkipTemplate<void>::not_skipped_bad, 44, DEADLOCK, no_bucket, ERROR, [In method `skipped::SkipTemplate<void>::not_skipped_bad`,Method call: `skipped::SkipTemplate<void>::private_deadlock`, locks `this.mutex_` in `class skipped::SkipTemplate<void>`, locks `this.mutex_` in `class skipped::SkipTemplate<void>`]
-codetoanalyze/cpp/starvation/skip.cpp, skipped::UseTemplate::foo, 53, DEADLOCK, no_bucket, ERROR, [In method `skipped::UseTemplate::foo`,Method call: `skipped::SkipTemplate<void>::not_skipped_bad`,Method call: `skipped::SkipTemplate<void>::private_deadlock`, locks `this.mutex_` in `class skipped::SkipTemplate<void>`, locks `this.mutex_` in `class skipped::SkipTemplate<void>`]
+codetoanalyze/cpp/starvation/skip.cpp, skipped::UseTemplate::foo, 51, DEADLOCK, no_bucket, ERROR, [In method `skipped::UseTemplate::foo`,Method call: `skipped::SkipTemplate<void>::not_skipped_bad`,Method call: `skipped::SkipTemplate<void>::private_deadlock`, locks `this.x.mutex_` in `class skipped::UseTemplate`, locks `this.x.mutex_` in `class skipped::UseTemplate`]

infer/tests/codetoanalyze/cpp/starvation/skip.cpp

@@ -47,11 +47,12 @@ class SkipTemplate {
 class UseTemplate {
  public:
   void foo() {
-    SkipTemplate<void> x;
-
     x.skipped_ok();
     x.not_skipped_bad();
   }
+
+ private:
+  SkipTemplate<void> x;
 };
 
 } // namespace skipped

infer/tests/codetoanalyze/java/starvation-dedup/issues.exp

@@ -3,5 +3,5 @@ codetoanalyze/java/starvation-dedup/Dedup.java, Dedup.callMethodWithMultipleBloc
 codetoanalyze/java/starvation-dedup/Dedup.java, Dedup.callMethodWithMultipleBlocksBad():void, 28, STARVATION, no_bucket, ERROR, [`void Dedup.callMethodWithMultipleBlocksBad()`,calls `Object Future.get()`]
 codetoanalyze/java/starvation-dedup/Dedup.java, Dedup.onUiThreadBad():void, 20, STARVATION, no_bucket, ERROR, [`void Dedup.onUiThreadBad()`,Method call: `void Dedup.callMethodWithMultipleBlocksBad()`,calls `void CountDownLatch.await()`]
 codetoanalyze/java/starvation-dedup/Dedup.java, Dedup.oneWayBad():void, 35, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Dedup.oneWayBad()`, locks `this.lockA` in `class Dedup`, locks `this.lockB` in `class Dedup`,[Trace 2] `void Dedup.anotherWayBad()`, locks `this.lockB` in `class Dedup`, locks `this.lockA` in `class Dedup`]
-codetoanalyze/java/starvation-dedup/Interproc.java, Interproc.interproc1Bad(InterprocA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Interproc.interproc1Bad(InterprocA)`, locks `this` in `class Interproc`,Method call: `void Interproc.interproc2(InterprocA)`, locks `b` in `class InterprocA`,[Trace 2] `void InterprocA.interproc1Bad(Interproc)`, locks `this` in `class InterprocA`,Method call: `void InterprocA.interproc2(Interproc)`, locks `d` in `class Interproc`]
+codetoanalyze/java/starvation-dedup/Interproc.java, Interproc.interproc1Bad(InterprocA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Interproc.interproc1Bad(InterprocA)`, locks `this` in `class Interproc`,Method call: `void Interproc.interproc2(InterprocA)`, locks `a` in `class InterprocA`,[Trace 2] `void InterprocA.interproc1Bad(Interproc)`, locks `this` in `class InterprocA`,Method call: `void InterprocA.interproc2(Interproc)`, locks `c` in `class Interproc`]
 codetoanalyze/java/starvation-dedup/Intraproc.java, Intraproc.intraBad(IntraprocA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Intraproc.intraBad(IntraprocA)`, locks `this` in `class Intraproc`, locks `o` in `class IntraprocA`,[Trace 2] `void IntraprocA.intraBad(Intraproc)`, locks `this` in `class IntraprocA`, locks `o` in `class Intraproc`]

infer/tests/codetoanalyze/java/starvation/Interproc.java

@@ -6,52 +6,52 @@
  */
 
 class Interproc {
-  synchronized void interproc1Bad(InterprocA a) {
+  synchronized void lockThisThenParamBad(InterprocA a) {
-    interproc2Bad(a);
+    lockParamA(a);
   }
 
-  void interproc2Bad(InterprocA b) {
+  void lockParamA(InterprocA b) {
     synchronized (b) {
     }
   }
 
-  synchronized void interproc1Ok(InterprocB a) {
+  synchronized void lockThisThenParamOk(InterprocB a) {
-    interproc2Ok(a);
+    lockParamB(a);
   }
 
-  void interproc2Ok(InterprocB b) {
+  void lockParamB(InterprocB b) {
     synchronized (b) {
     }
   }
 
-  void reentrant1Ok(InterprocB b) {
+  void lockThisTwiceOk(InterprocB b) {
     synchronized (this) {
       synchronized (b) {
-        reentrant2Ok();
+        lockThis();
       }
     }
   }
 
-  synchronized void reentrant2Ok() {}
+  synchronized void lockThis() {}
 }
 
 class InterprocA {
-  synchronized void interproc1Bad(Interproc c) {
+  synchronized void lockThisThenParamBad(Interproc c) {
-    interproc2Bad(c);
+    lockParam(c);
   }
 
-  void interproc2Bad(Interproc d) {
+  void lockParam(Interproc d) {
     synchronized (d) {
     }
   }
 }
 
 class InterprocB {
-  void interproc1Ok(Interproc c) {
+  void lockParamThenThisOk(Interproc c) {
     synchronized (c) {
-      interproc2Ok(c);
+      lockThis(c);
     }
   }
 
-  synchronized void interproc2Ok(Interproc d) {}
+  synchronized void lockThis(Interproc d) {}
 }

infer/tests/codetoanalyze/java/starvation/Parameters.java

@@ -31,11 +31,11 @@ class Parameters {
   Parameters someObject;
 
   // Next two methods will deadlock
-  public synchronized void FN_oneWayEmulateSyncBad() {
+  public synchronized void oneWayEmulateSyncBad() {
     emulateSynchronized(someObject);
   }
 
-  public void FN_anotherWayEmulateSyncBad() {
+  public void anotherWayEmulateSyncBad() {
     synchronized (someObject) {
       synchronized (this) {
       }

infer/tests/codetoanalyze/java/starvation/issues.exp

@@ -12,15 +12,14 @@ codetoanalyze/java/starvation/FutureGet.java, FutureGet.getTimeout64BitsBad():vo
 codetoanalyze/java/starvation/FutureGet.java, FutureGet.getTimeoutOneDayBad():void, 43, STARVATION, no_bucket, ERROR, [`void FutureGet.getTimeoutOneDayBad()`,calls `Object Future.get(long,TimeUnit)`]
 codetoanalyze/java/starvation/FutureGet.java, FutureGet.getTimeoutOneHourBad():void, 59, STARVATION, no_bucket, ERROR, [`void FutureGet.getTimeoutOneHourBad()`,calls `Object Future.get(long,TimeUnit)`]
 codetoanalyze/java/starvation/IndirectBlock.java, IndirectBlock.takeExpensiveLockOnUiThreadBad():void, 23, STARVATION, no_bucket, ERROR, [[Trace 1] `void IndirectBlock.takeExpensiveLockOnUiThreadBad()`, locks `this.expensiveLock` in `class IndirectBlock`,[Trace 2] `void IndirectBlock.doTransactUnderLock()`, locks `this.expensiveLock` in `class IndirectBlock`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
-codetoanalyze/java/starvation/IndirectBlock.java, IndirectBlock.takeRemoteExpensiveLockOnUiThreadBad(IndirectInterproc):void, 35, STARVATION, no_bucket, ERROR, [[Trace 1] `void IndirectBlock.takeRemoteExpensiveLockOnUiThreadBad(IndirectInterproc)`,Method call: `void IndirectInterproc.takeLock()`, locks `this` in `class IndirectInterproc`,[Trace 2] `void IndirectInterproc.doTransactUnderLock(Binder)`, locks `this` in `class IndirectInterproc`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
+codetoanalyze/java/starvation/IndirectBlock.java, IndirectBlock.takeRemoteExpensiveLockOnUiThreadBad(IndirectInterproc):void, 35, STARVATION, no_bucket, ERROR, [[Trace 1] `void IndirectBlock.takeRemoteExpensiveLockOnUiThreadBad(IndirectInterproc)`,Method call: `void IndirectInterproc.takeLock()`, locks `i` in `class IndirectInterproc`,[Trace 2] `void IndirectInterproc.doTransactUnderLock(Binder)`, locks `this` in `class IndirectInterproc`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
-codetoanalyze/java/starvation/InnerClass.java, InnerClass$InnerClassA.<init>(InnerClass,java.lang.Object), 55, DEADLOCK, no_bucket, ERROR, [[Trace 1] `InnerClass$InnerClassA.<init>(InnerClass,Object)`, locks `this` in `class InnerClass$InnerClassA`,Method call: `void InnerClass.lockOuter()`, locks `this` in `class InnerClass`,[Trace 2] `void InnerClass.FP_outerInnerOk(InnerClass$InnerClassA)`, locks `this` in `class InnerClass`,Method call: `void InnerClass$InnerClassA.lockInner()`, locks `this` in `class InnerClass$InnerClassA`]
+codetoanalyze/java/starvation/InnerClass.java, InnerClass$InnerClassA.<init>(InnerClass,java.lang.Object), 55, DEADLOCK, no_bucket, ERROR, [[Trace 1] `InnerClass$InnerClassA.<init>(InnerClass,Object)`, locks `this` in `class InnerClass$InnerClassA`,Method call: `void InnerClass.lockOuter()`, locks `this$0` in `class InnerClass`,[Trace 2] `void InnerClass.FP_outerInnerOk(InnerClass$InnerClassA)`, locks `this` in `class InnerClass`,Method call: `void InnerClass$InnerClassA.lockInner()`, locks `a` in `class InnerClass$InnerClassA`]
-codetoanalyze/java/starvation/InnerClass.java, InnerClass$InnerClassA.innerOuterBad():void, 39, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void InnerClass$InnerClassA.innerOuterBad()`, locks `this` in `class InnerClass$InnerClassA`,Method call: `void InnerClass.lockOuter()`, locks `this` in `class InnerClass`,[Trace 2] `void InnerClass.FP_outerInnerOk(InnerClass$InnerClassA)`, locks `this` in `class InnerClass`,Method call: `void InnerClass$InnerClassA.lockInner()`, locks `this` in `class InnerClass$InnerClassA`]
+codetoanalyze/java/starvation/InnerClass.java, InnerClass.FP_outerInnerOk(InnerClass$InnerClassA):void, 21, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void InnerClass.FP_outerInnerOk(InnerClass$InnerClassA)`, locks `this` in `class InnerClass`,Method call: `void InnerClass$InnerClassA.lockInner()`, locks `a` in `class InnerClass$InnerClassA`,[Trace 2] `void InnerClass$InnerClassA.innerOuterBad()`, locks `this` in `class InnerClass$InnerClassA`,Method call: `void InnerClass.lockOuter()`, locks `this.this$0` in `class InnerClass$InnerClassA`]
-codetoanalyze/java/starvation/InnerClass.java, InnerClass.FP_outerInnerOk(InnerClass$InnerClassA):void, 21, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void InnerClass.FP_outerInnerOk(InnerClass$InnerClassA)`, locks `this` in `class InnerClass`,Method call: `void InnerClass$InnerClassA.lockInner()`, locks `this` in `class InnerClass$InnerClassA`,[Trace 2] `InnerClass$InnerClassA.<init>(InnerClass,Object)`, locks `this` in `class InnerClass$InnerClassA`,Method call: `void InnerClass.lockOuter()`, locks `this` in `class InnerClass`]
+codetoanalyze/java/starvation/InnerClass.java, InnerClass.FP_outerInnerOk(InnerClass$InnerClassA):void, 21, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void InnerClass.FP_outerInnerOk(InnerClass$InnerClassA)`, locks `this` in `class InnerClass`,Method call: `void InnerClass$InnerClassA.lockInner()`, locks `a` in `class InnerClass$InnerClassA`,[Trace 2] `InnerClass$InnerClassA.<init>(InnerClass,Object)`, locks `this` in `class InnerClass$InnerClassA`,Method call: `void InnerClass.lockOuter()`, locks `this$0` in `class InnerClass`]
-codetoanalyze/java/starvation/InnerClass.java, InnerClass.FP_outerInnerOk(InnerClass$InnerClassA):void, 21, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void InnerClass.FP_outerInnerOk(InnerClass$InnerClassA)`, locks `this` in `class InnerClass`,Method call: `void InnerClass$InnerClassA.lockInner()`, locks `this` in `class InnerClass$InnerClassA`,[Trace 2] `void InnerClass$InnerClassA.innerOuterBad()`, locks `this` in `class InnerClass$InnerClassA`,Method call: `void InnerClass.lockOuter()`, locks `this` in `class InnerClass`]
+codetoanalyze/java/starvation/Interclass.java, Interclass.interclass1Bad(InterclassA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Interclass.interclass1Bad(InterclassA)`, locks `this` in `class Interclass`,Method call: `void InterclassA.interclass1Bad()`, locks `a` in `class InterclassA`,[Trace 2] `void InterclassA.interclass2Bad(Interclass)`, locks `this` in `class InterclassA`,Method call: `void Interclass.interclass2Bad()`, locks `i` in `class Interclass`]
-codetoanalyze/java/starvation/Interclass.java, Interclass.interclass1Bad(InterclassA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Interclass.interclass1Bad(InterclassA)`, locks `this` in `class Interclass`,Method call: `void InterclassA.interclass1Bad()`, locks `this` in `class InterclassA`,[Trace 2] `void InterclassA.interclass2Bad(Interclass)`, locks `this` in `class InterclassA`,Method call: `void Interclass.interclass2Bad()`, locks `this` in `class Interclass`]
+codetoanalyze/java/starvation/Interclass.java, InterclassA.interclass2Bad(Interclass):void, 37, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void InterclassA.interclass2Bad(Interclass)`, locks `this` in `class InterclassA`,Method call: `void Interclass.interclass2Bad()`, locks `i` in `class Interclass`,[Trace 2] `void Interclass.interclass1Bad(InterclassA)`, locks `this` in `class Interclass`,Method call: `void InterclassA.interclass1Bad()`, locks `a` in `class InterclassA`]
-codetoanalyze/java/starvation/Interclass.java, InterclassA.interclass2Bad(Interclass):void, 37, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void InterclassA.interclass2Bad(Interclass)`, locks `this` in `class InterclassA`,Method call: `void Interclass.interclass2Bad()`, locks `this` in `class Interclass`,[Trace 2] `void Interclass.interclass1Bad(InterclassA)`, locks `this` in `class Interclass`,Method call: `void InterclassA.interclass1Bad()`, locks `this` in `class InterclassA`]
+codetoanalyze/java/starvation/Interproc.java, Interproc.lockThisThenParamBad(InterprocA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Interproc.lockThisThenParamBad(InterprocA)`, locks `this` in `class Interproc`,Method call: `void Interproc.lockParamA(InterprocA)`, locks `a` in `class InterprocA`,[Trace 2] `void InterprocA.lockThisThenParamBad(Interproc)`, locks `this` in `class InterprocA`,Method call: `void InterprocA.lockParam(Interproc)`, locks `c` in `class Interproc`]
-codetoanalyze/java/starvation/Interproc.java, Interproc.interproc1Bad(InterprocA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Interproc.interproc1Bad(InterprocA)`, locks `this` in `class Interproc`,Method call: `void Interproc.interproc2Bad(InterprocA)`, locks `b` in `class InterprocA`,[Trace 2] `void InterprocA.interproc1Bad(Interproc)`, locks `this` in `class InterprocA`,Method call: `void InterprocA.interproc2Bad(Interproc)`, locks `d` in `class Interproc`]
+codetoanalyze/java/starvation/Interproc.java, InterprocA.lockThisThenParamBad(Interproc):void, 40, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void InterprocA.lockThisThenParamBad(Interproc)`, locks `this` in `class InterprocA`,Method call: `void InterprocA.lockParam(Interproc)`, locks `c` in `class Interproc`,[Trace 2] `void Interproc.lockThisThenParamBad(InterprocA)`, locks `this` in `class Interproc`,Method call: `void Interproc.lockParamA(InterprocA)`, locks `a` in `class InterprocA`]
-codetoanalyze/java/starvation/Interproc.java, InterprocA.interproc1Bad(Interproc):void, 40, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void InterprocA.interproc1Bad(Interproc)`, locks `this` in `class InterprocA`,Method call: `void InterprocA.interproc2Bad(Interproc)`, locks `d` in `class Interproc`,[Trace 2] `void Interproc.interproc1Bad(InterprocA)`, locks `this` in `class Interproc`,Method call: `void Interproc.interproc2Bad(InterprocA)`, locks `b` in `class InterprocA`]
 codetoanalyze/java/starvation/Intraproc.java, Intraproc.intraBad(IntraprocA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Intraproc.intraBad(IntraprocA)`, locks `this` in `class Intraproc`, locks `o` in `class IntraprocA`,[Trace 2] `void IntraprocA.intraBad(Intraproc)`, locks `this` in `class IntraprocA`, locks `o` in `class Intraproc`]
 codetoanalyze/java/starvation/Intraproc.java, IntraprocA.intraBad(Intraproc):void, 35, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void IntraprocA.intraBad(Intraproc)`, locks `this` in `class IntraprocA`, locks `o` in `class Intraproc`,[Trace 2] `void Intraproc.intraBad(IntraprocA)`, locks `this` in `class Intraproc`, locks `o` in `class IntraprocA`]
 codetoanalyze/java/starvation/LegacySync.java, LegacySync.onUiThreadOpBad():java.lang.Object, 25, STARVATION, no_bucket, ERROR, [[Trace 1] `Object LegacySync.onUiThreadOpBad()`, locks `this.table` in `class LegacySync`,[Trace 2] `void LegacySync.notOnUiThreadSyncedBad()`, locks `this.table` in `class LegacySync`,calls `Object Future.get()`]
@@ -46,6 +45,8 @@ codetoanalyze/java/starvation/ObjWait.java, ObjWait.indirectWaitOnMainWithoutTim
 codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithExcessiveTimeout1Bad():void, 31, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithExcessiveTimeout1Bad()`,calls `wait` on `this.o` in `class ObjWait`]
 codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithExcessiveTimeout2Bad():void, 38, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithExcessiveTimeout2Bad()`,calls `wait` on `this.o` in `class ObjWait`]
 codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithoutTimeoutBad():void, 24, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithoutTimeoutBad()`,calls `wait` on `this.o` in `class ObjWait`]
+codetoanalyze/java/starvation/Parameters.java, Parameters.anotherWayEmulateSyncBad():void, 39, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Parameters.anotherWayEmulateSyncBad()`, locks `this.someObject` in `class Parameters`, locks `this` in `class Parameters`,[Trace 2] `void Parameters.oneWayEmulateSyncBad()`, locks `this` in `class Parameters`,Method call: `void Parameters.emulateSynchronized(Parameters)`, locks `this.someObject` in `class Parameters`]
+codetoanalyze/java/starvation/Parameters.java, Parameters.oneWayEmulateSyncBad():void, 35, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Parameters.oneWayEmulateSyncBad()`, locks `this` in `class Parameters`,Method call: `void Parameters.emulateSynchronized(Parameters)`, locks `this.someObject` in `class Parameters`,[Trace 2] `void Parameters.anotherWayEmulateSyncBad()`, locks `this.someObject` in `class Parameters`, locks `this` in `class Parameters`]
 codetoanalyze/java/starvation/Parameters.java, Parameters.otherWaySyncOnParamBad(java.lang.Object):void, 20, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Parameters.otherWaySyncOnParamBad(Object)`, locks `x` in `class java.lang.Object`, locks `this` in `class Parameters`,[Trace 2] `void Parameters.oneWaySyncOnParamBad(Object)`, locks `this` in `class Parameters`,Method call: `void Parameters.syncOnParam(Object)`, locks `x` in `class java.lang.Object`]
 codetoanalyze/java/starvation/PubPriv.java, PubPriv.alsoBad():void, 25, STARVATION, no_bucket, ERROR, [`void PubPriv.alsoBad()`,Method call: `void PubPriv.transactBad()`,Method call: `void PubPriv.doTransactOk()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
 codetoanalyze/java/starvation/PubPriv.java, PubPriv.callAnotherWayBad():void, 53, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void PubPriv.callAnotherWayBad()`,Method call: `void PubPriv.anotherWayOk()`, locks `this.lockB` in `class PubPriv`, locks `this.lockA` in `class PubPriv`,[Trace 2] `void PubPriv.callOneWayBad()`,Method call: `void PubPriv.oneWayOk()`, locks `this.lockA` in `class PubPriv`, locks `this.lockB` in `class PubPriv`]