[starvation] improve 2-way deadlock reports

Reviewed By: mbouaziz

Differential Revision: D13450650

fbshipit-source-id: 0dbd349d1

infer/src/concurrency/starvation.ml

@@ -354,23 +354,6 @@ let report_deadlocks env {StarvationDomain.order; ui} report_map' =
   let open StarvationDomain in
   let _, current_pdesc = env in
   let current_pname = Procdesc.get_proc_name current_pdesc in
-  let pp_acquire fmt (lock, loc, pname) =
-    F.fprintf fmt "%a (%a in %a)" Lock.pp_human lock Location.pp loc pname_pp pname
-  in
-  let pp_thread fmt
-      ( pname
-      , { Order.loc= loc1
-        ; trace= trace1
-        ; elem= {first= lock1; eventually= {elem= event; loc= loc2; trace= trace2}} } ) =
-    match event with
-    | LockAcquire lock2 ->
-        let pname1 = List.last trace1 |> Option.value_map ~default:pname ~f:CallSite.pname in
-        let pname2 = List.last trace2 |> Option.value_map ~default:pname1 ~f:CallSite.pname in
-        F.fprintf fmt "first %a and then %a" pp_acquire (lock1, loc1, pname1) pp_acquire
-          (lock2, loc2, pname2)
-    | _ ->
-        L.die InternalError "Trying to report a deadlock without two lock events."
-  in
   let report_endpoint_elem current_elem endpoint_pname elem report_map =
     if
       not
@@ -380,12 +363,13 @@ let report_deadlocks env {StarvationDomain.order; ui} 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
-      | LockAcquire _, LockAcquire _ ->
+      | LockAcquire lock1, LockAcquire lock2 ->
           let error_message =
             Format.asprintf
-              "Potential deadlock.@.Trace 1 (starts at %a) %a.@.Trace 2 (starts at %a), %a."
-              pname_pp current_pname pp_thread (current_pname, current_elem) pname_pp
-              endpoint_pname pp_thread (endpoint_pname, elem)
+              "Potential deadlock. %a (Trace 1) and %a (Trace 2) acquire locks %a and %a in \
+               reverse orders."
+              pname_pp current_pname pname_pp endpoint_pname Lock.pp_human lock1 Lock.pp_human
+              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
@@ -402,7 +386,7 @@ let report_deadlocks env {StarvationDomain.order; ui} report_map' =
     | LockAcquire endpoint_lock when Lock.equal endpoint_lock elem.Order.elem.first ->
         let error_message =
           Format.asprintf "Potential self deadlock. %a%a twice." pname_pp current_pname
-            Lock.pp_human endpoint_lock
+            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
@@ -434,7 +418,7 @@ let report_starvation env {StarvationDomain.events; ui} report_map' =
           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_human lock
+            pname_pp current_pname UIThreadExplanationDomain.pp ui_explain Lock.pp_locks lock
             block_descr
         in
         let first_trace = Event.make_trace ~header:"[Trace 1] " current_pname event in

infer/src/concurrency/starvationDomain.ml

@@ -45,12 +45,13 @@ module Lock = struct
   let owner_class ((_, typ), _) = Typ.inner_name typ
 
   let pp_human fmt lock =
-    let owner =
-      owner_class lock
-      |> Option.value_map ~default:"" ~f:(fun typ ->
-             F.asprintf " in %a" (MF.wrap_monospaced Typ.Name.pp) typ )
+    let pp_owner fmt lock =
+      owner_class lock |> Option.iter ~f:(F.fprintf fmt " in %a" (MF.wrap_monospaced Typ.Name.pp))
     in
-    F.fprintf fmt "locks %a%s" (MF.wrap_monospaced AccessPath.pp) lock owner
+    F.fprintf fmt "%a%a" (MF.wrap_monospaced pp) lock pp_owner lock
+
+
+  let pp_locks fmt lock = F.fprintf fmt " locks %a" pp_human lock
 end
 
 module Event = struct
@@ -82,7 +83,7 @@ module Event = struct
     let pp_human fmt elem =
       match elem with
       | LockAcquire lock ->
-          Lock.pp_human fmt lock
+          Lock.pp_locks fmt lock
       | MayBlock (msg, _) ->
           F.pp_print_string fmt msg
       | StrictModeCall msg ->
@@ -127,7 +128,7 @@ module Order = struct
       F.fprintf fmt "{first= %a; eventually= %a}" Lock.pp first Event.pp eventually
 
 
-    let pp_human fmt {first} = Lock.pp_human fmt first
+    let pp_human fmt {first} = Lock.pp_locks fmt first
   end
 
   include ExplicitTrace.MakeTraceElem (OrderElement)

infer/src/concurrency/starvationDomain.mli

@@ -17,6 +17,8 @@ module Lock : sig
   (** Class of the root variable of the path representing the lock *)
 
   val equal : t -> t -> bool
+
+  val pp_locks : F.formatter -> t -> unit
 end
 
 (** Represents the existence of a program path from the current method to the eventual acquisition

infer/tests/codetoanalyze/java/starvation/StaticLock.java

@@ -26,7 +26,7 @@ class StaticLock {
     }
   }
 
-  synchronized void lockOtherClassAnotherWayNad() {
+  synchronized void lockOtherClassAnotherWayBad() {
     staticSynced();
   }
 }

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

@@ -42,7 +42,7 @@ codetoanalyze/java/starvation/PubPriv.java, PubPriv.alsoBad():void, 25, STARVATI
 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`]
 codetoanalyze/java/starvation/PubPriv.java, PubPriv.transactBad():void, 21, STARVATION, no_bucket, ERROR, [`void PubPriv.transactBad()`,Method call: `void PubPriv.doTransactOk()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void PubPriv.transactBad()`,Method call: `void PubPriv.doTransactOk()`,`void PubPriv.doTransactOk()` is annotated `UiThread`]
 codetoanalyze/java/starvation/ServiceOnUIThread.java, ServiceOnUIThread.onBind(android.content.Intent):android.os.IBinder, 19, STARVATION, no_bucket, ERROR, [`IBinder ServiceOnUIThread.onBind(Intent)`,Method call: `void ServiceOnUIThread.transactBad()`,calls `boolean IBinder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `IBinder ServiceOnUIThread.onBind(Intent)`,`IBinder ServiceOnUIThread.onBind(Intent)` is a standard UI-thread method]
-codetoanalyze/java/starvation/StaticLock.java, StaticLock.lockOtherClassOneWayBad():void, 23, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void StaticLock.lockOtherClassOneWayBad()`,locks `StaticLock$0` in `class java.lang.Class`,locks `this` in `class StaticLock`,[Trace 2] `void StaticLock.lockOtherClassAnotherWayNad()`,locks `this` in `class StaticLock`,Method call: `void StaticLock.staticSynced()`,locks `StaticLock$0` in `class java.lang.Class`]
+codetoanalyze/java/starvation/StaticLock.java, StaticLock.lockOtherClassOneWayBad():void, 23, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void StaticLock.lockOtherClassOneWayBad()`, locks `StaticLock$0` in `class java.lang.Class`, locks `this` in `class StaticLock`,[Trace 2] `void StaticLock.lockOtherClassAnotherWayBad()`, locks `this` in `class StaticLock`,Method call: `void StaticLock.staticSynced()`, locks `StaticLock$0` in `class java.lang.Class`]
 codetoanalyze/java/starvation/StrictModeViolation.java, StrictModeViolation.violateStrictModeBad():void, 17, STRICT_MODE_VIOLATION, no_bucket, ERROR, [`void StrictModeViolation.violateStrictModeBad()`,calls `boolean File.canRead()`,[Trace on UI thread] `void StrictModeViolation.violateStrictModeBad()`,`void StrictModeViolation.violateStrictModeBad()` is annotated `UiThread`]
 codetoanalyze/java/starvation/StrictModeViolation.java, StrictModeViolation.violateStrictModeBad():void, 18, STRICT_MODE_VIOLATION, no_bucket, ERROR, [`void StrictModeViolation.violateStrictModeBad()`,calls `boolean File.canWrite()`,[Trace on UI thread] `void StrictModeViolation.violateStrictModeBad()`,`void StrictModeViolation.violateStrictModeBad()` is annotated `UiThread`]
 codetoanalyze/java/starvation/StrictModeViolation.java, StrictModeViolation.violateStrictModeBad():void, 19, STRICT_MODE_VIOLATION, no_bucket, ERROR, [`void StrictModeViolation.violateStrictModeBad()`,calls `boolean File.createNewFile()`,[Trace on UI thread] `void StrictModeViolation.violateStrictModeBad()`,`void StrictModeViolation.violateStrictModeBad()` is annotated `UiThread`]