[starvation] fix FPs due to mishandling wait

Summary:
`Object.wait()` must be called on a locked monitor and it releases the
lock immediately, as far as other threads are concerned
(it also magically re-takes the lock when the monitor is `notified`).
Starvation can only occur if the UI thread is waiting
a lock that is distinct to that being waited on.

The check present was over-approximate in that it was checking that there exists a lock held by the UI thread and the thread issuing the `wait`, but did not make sure that lock was *not* the one waited on.

Amusingly, the e2e test was correct, but the reporting code wasn't.

Reviewed By: dulmarod

Differential Revision: D18782919

fbshipit-source-id: b3b98239e

infer/src/concurrency/StarvationModels.ml

@@ -101,10 +101,6 @@ let standard_matchers =
   let open MethodMatcher in
   let high_sev =
     [ {default with classname= "java.lang.Thread"; methods= ["sleep"]}
-    ; { default with
-        classname= "java.lang.Object"
-      ; methods= ["wait"]
-      ; actuals_pred= empty_or_excessive_timeout }
     ; { default with
         classname= "java.util.concurrent.CountDownLatch"
       ; methods= ["await"]
@@ -140,6 +136,15 @@ let may_block tenv pn actuals =
       Option.some_if (matcher tenv pn actuals) sev )
 
 
+let is_monitor_wait =
+  MethodMatcher.(
+    of_record
+      { default with
+        classname= "java.lang.Object"
+      ; methods= ["wait"]
+      ; actuals_pred= empty_or_excessive_timeout })
+
+
 (* selection is a bit arbitrary as some would be generated anyway if not here; no harm though *)
 (* some, like [file], need manual addition due to our lack of handling dynamic dispatch *)
 let strict_mode_matcher =
@@ -246,8 +251,8 @@ let schedules_work_on_bg_thread =
 type scheduler_thread_constraint = ForUIThread | ForNonUIThread | ForUnknownThread
 [@@deriving equal]
 
-(* Executors are sometimes stored in fields and annotated according to what type of thread 
-   they schedule work on.  Given an expression representing such a field, try to find the kind of 
+(* Executors are sometimes stored in fields and annotated according to what type of thread
+   they schedule work on.  Given an expression representing such a field, try to find the kind of
    annotation constraint, if any. *)
 let rec get_executor_thread_annotation_constraint tenv (receiver : HilExp.AccessExpression.t) =
   match receiver with

infer/src/concurrency/StarvationModels.mli

@@ -17,6 +17,8 @@ val may_block : Tenv.t -> Typ.Procname.t -> HilExp.t list -> severity option
 
 val is_strict_mode_violation : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool
 
+val is_monitor_wait : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool
+
 val is_synchronized_library_call : Tenv.t -> Typ.Procname.t -> bool
 (** does the method call lock-then-unlock the underlying object? legacy Java containers like Vector
     do this, and can interact with explicit locking *)

infer/src/concurrency/starvation.ml

@@ -256,6 +256,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           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 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
@@ -540,17 +542,18 @@ end = struct
 end
 
 let should_report_deadlock_on_current_proc current_elem endpoint_elem =
+  let open Domain in
   (not Config.deduplicate)
   ||
-  let open Domain in
   match (endpoint_elem.CriticalPair.elem.event, current_elem.CriticalPair.elem.event) with
-  | _, (MayBlock _ | StrictModeCall _) | (MayBlock _ | StrictModeCall _), _ ->
+  | _, (MayBlock _ | StrictModeCall _ | MonitorWait _)
+  | (MayBlock _ | StrictModeCall _ | MonitorWait _), _ ->
       (* should never happen *)
       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 -- FIXME WHY? *)
+         reverse ordering on the events will not occur since we don't search the class for static locks *)
       true
   | LockAcquire ((Var.LogicalVar _, _), _ :: _), _ | _, LockAcquire ((Var.LogicalVar _, _), _) ->
       (* first elem has an ident root, but has a non-empty access path, which means we are
@@ -611,6 +614,13 @@ let report_on_parallel_composition ~should_report_starvation tenv pdesc pair loc
     other_pair report_map =
   let open Domain in
   let pname = Procdesc.get_proc_name pdesc in
+  let make_trace_and_loc () =
+    let first_trace = CriticalPair.make_trace ~header:"[Trace 1] " pname pair in
+    let second_trace = CriticalPair.make_trace ~header:"[Trace 2] " other_pname other_pair in
+    let ltr = first_trace @ second_trace in
+    let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:pname pair in
+    (ltr, loc)
+  in
   if CriticalPair.can_run_in_parallel pair other_pair then
     let acquisitions = other_pair.CriticalPair.elem.acquisitions in
     match other_pair.CriticalPair.elem.event with
@@ -621,25 +631,29 @@ let report_on_parallel_composition ~should_report_starvation tenv pdesc pair loc
             "Method %a runs on UI thread and%a, which may be held by another thread which %s."
             pname_pp pname Lock.pp_locks lock block_descr
         in
-        let first_trace = CriticalPair.make_trace ~header:"[Trace 1] " pname pair in
-        let second_trace = CriticalPair.make_trace ~header:"[Trace 2] " other_pname other_pair in
-        let ltr = first_trace @ second_trace in
-        let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:pname pair in
+        let ltr, loc = make_trace_and_loc () in
         ReportMap.add_starvation sev tenv pdesc loc ltr error_message report_map
+    | MonitorWait monitor_lock
+      when should_report_starvation
+           && Acquisitions.lock_is_held lock acquisitions
+           && not (Lock.equal lock monitor_lock) ->
+        let error_message =
+          Format.asprintf
+            "Method %a runs on UI thread and%a, which may be held by another thread which %a."
+            pname_pp pname Lock.pp_locks lock Event.describe other_pair.CriticalPair.elem.event
+        in
+        let ltr, loc = make_trace_and_loc () in
+        ReportMap.add_starvation High tenv pdesc loc ltr error_message report_map
     | LockAcquire other_lock
       when CriticalPair.may_deadlock pair other_pair
            && should_report_deadlock_on_current_proc pair other_pair ->
-        let open Domain in
         let error_message =
           Format.asprintf
             "Potential deadlock. %a (Trace 1) and %a (Trace 2) acquire locks %a and %a in reverse \
              orders."
             pname_pp pname pname_pp other_pname Lock.describe lock Lock.describe other_lock
         in
-        let first_trace = CriticalPair.make_trace ~header:"[Trace 1] " pname pair in
-        let second_trace = CriticalPair.make_trace ~header:"[Trace 2] " other_pname other_pair in
-        let ltr = first_trace @ second_trace in
-        let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:pname pair in
+        let ltr, loc = make_trace_and_loc () in
         ReportMap.add_deadlock tenv pdesc loc ltr error_message report_map
     | _ ->
         report_map
@@ -654,22 +668,32 @@ let report_on_pair ((tenv, summary) as env) (pair : Domain.CriticalPair.t) repor
   let should_report_starvation =
     CriticalPair.is_uithread pair && not (Typ.Procname.is_constructor pname)
   in
+  let make_trace_and_loc () =
+    let loc = CriticalPair.get_loc pair in
+    let ltr = CriticalPair.make_trace ~include_acquisitions:false pname pair in
+    (ltr, loc)
+  in
   match event with
   | MayBlock (_, sev) when should_report_starvation ->
       let error_message =
         Format.asprintf "Method %a runs on UI thread and may block; %a." pname_pp pname
           Event.describe event
       in
-      let loc = CriticalPair.get_loc pair in
-      let ltr = CriticalPair.make_trace ~include_acquisitions:false pname pair in
+      let ltr, loc = make_trace_and_loc () in
       ReportMap.add_starvation sev tenv pdesc loc ltr error_message report_map
+  | MonitorWait _ when should_report_starvation ->
+      let error_message =
+        Format.asprintf "Method %a runs on UI thread and may block; %a." pname_pp pname
+          Event.describe event
+      in
+      let ltr, loc = make_trace_and_loc () in
+      ReportMap.add_starvation High tenv pdesc loc ltr error_message report_map
   | StrictModeCall _ when should_report_starvation ->
       let error_message =
         Format.asprintf "Method %a runs on UI thread and may violate Strict Mode; %a." pname_pp
           pname Event.describe event
       in
-      let loc = CriticalPair.get_loc pair in
-      let ltr = CriticalPair.make_trace ~include_acquisitions:false pname pair in
+      let ltr, loc = make_trace_and_loc () in
       ReportMap.add_strict_mode_violation tenv pdesc loc ltr error_message report_map
   | LockAcquire _ when StarvationModels.is_annotated_lockless ~attrs_of_pname tenv pname ->
       let error_message =

infer/src/concurrency/starvationDomain.ml

@@ -119,6 +119,7 @@ module Event = struct
     | LockAcquire of Lock.t
     | MayBlock of (string * StarvationModels.severity)
     | StrictModeCall of string
+    | MonitorWait of Lock.t
   [@@deriving compare]
 
   let pp fmt = function
@@ -128,6 +129,8 @@ module Event = struct
         F.fprintf fmt "MayBlock(%s, %a)" msg StarvationModels.pp_severity sev
     | StrictModeCall msg ->
         F.fprintf fmt "StrictModeCall(%s)" msg
+    | MonitorWait lock ->
+        F.fprintf fmt "MonitorWait(%a)" Lock.pp lock
 
 
   let describe fmt elem =
@@ -138,6 +141,8 @@ module Event = struct
         F.pp_print_string fmt msg
     | StrictModeCall msg ->
         F.pp_print_string fmt msg
+    | MonitorWait lock ->
+        F.fprintf fmt "calls `wait` on %a" Lock.describe lock
 
 
   let make_acquire lock = LockAcquire lock
@@ -152,6 +157,9 @@ module Event = struct
   let make_strict_mode_call callee =
     let descr = make_call_descr callee in
     StrictModeCall descr
+
+
+  let make_object_wait lock = MonitorWait lock
 end
 
 (** A lock acquisition with source location and procname in which it occurs. The location & procname
@@ -598,6 +606,16 @@ let blocking_call ~callee sev ~loc astate =
   make_call_with_event new_event ~loc astate
 
 
+let wait_on_monitor ~loc actuals astate =
+  match actuals with
+  | HilExp.AccessExpression exp :: _ ->
+      let lock = HilExp.AccessExpression.to_access_path exp in
+      let new_event = Event.make_object_wait lock in
+      make_call_with_event new_event ~loc astate
+  | _ ->
+      astate
+
+
 let strict_mode_call ~callee ~loc astate =
   let new_event = Event.make_strict_mode_call callee in
   make_call_with_event new_event ~loc astate

infer/src/concurrency/starvationDomain.mli

@@ -28,6 +28,8 @@ end
 module Lock : sig
   include PrettyPrintable.PrintableOrderedType with type t = AccessPath.t
 
+  val equal : t -> t -> bool
+
   val owner_class : t -> Typ.name option
   (** Class of the root variable of the path representing the lock *)
 
@@ -41,6 +43,7 @@ module Event : sig
     | LockAcquire of Lock.t
     | MayBlock of (string * StarvationModels.severity)
     | StrictModeCall of string
+    | MonitorWait of Lock.t
   [@@deriving compare]
 
   val describe : F.formatter -> t -> unit
@@ -156,6 +159,8 @@ val release : t -> Lock.t list -> t
 
 val blocking_call : callee:Typ.Procname.t -> StarvationModels.severity -> loc:Location.t -> t -> t
 
+val wait_on_monitor : loc:Location.t -> HilExp.t list -> t -> t
+
 val strict_mode_call : callee:Typ.Procname.t -> loc:Location.t -> t -> t
 
 val add_guard :

infer/tests/codetoanalyze/java/starvation/ObjWait.java

@@ -54,4 +54,18 @@ class ObjWait {
       }
     }
   }
+
+  Object y;
+
+  @UiThread
+  void indirectWaitSameLockOnMainOk() throws InterruptedException {
+    synchronized (y) {
+    }
+  }
+
+  void lockAndWaitSameLockOnAnyOk() throws InterruptedException {
+    synchronized (y) {
+      y.wait();
+    }
+  }
 }

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

@@ -38,10 +38,10 @@ 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)`]
 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`, locks `this.x` in `class ObjWait`,calls `void Object.wait()`]
-codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithExcessiveTimeout1Bad():void, 31, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithExcessiveTimeout1Bad()`,calls `void Object.wait(long)`]
-codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithExcessiveTimeout2Bad():void, 38, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithExcessiveTimeout2Bad()`,calls `void Object.wait(long,int)`]
-codetoanalyze/java/starvation/ObjWait.java, ObjWait.waitOnMainWithoutTimeoutBad():void, 24, STARVATION, no_bucket, ERROR, [`void ObjWait.waitOnMainWithoutTimeoutBad()`,calls `void Object.wait()`]
+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 `wait` on `this.x` in `class ObjWait`]
+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/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`]
 codetoanalyze/java/starvation/PubPriv.java, PubPriv.callOneWayBad():void, 49, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void PubPriv.callOneWayBad()`,Method call: `void PubPriv.oneWayOk()`, locks `this.lockA` in `class PubPriv`, locks `this.lockB` in `class PubPriv`,[Trace 2] `void PubPriv.callAnotherWayBad()`,Method call: `void PubPriv.anotherWayOk()`, locks `this.lockB` in `class PubPriv`, locks `this.lockA` in `class PubPriv`]