[starvation] simplify deadlock dedup

Summary: Deadlocks often result in two reports if not deduplicated (two traces), so there is some logic for doing that.  Locks recently became an opaque type, with the `get_access_path` loophole supporting that deduplication ordering.  Fix that here and remove `Lock.get_access_path`.

Reviewed By: jvillard

Differential Revision: D19465223

fbshipit-source-id: b597e3c65

infer/src/concurrency/starvation.ml

@@ -556,24 +556,15 @@ let should_report_deadlock_on_current_proc current_elem endpoint_elem =
       L.die InternalError "Deadlock cannot occur without two lock events: %a" CriticalPair.pp
         current_elem
   | LockAcquire endpoint_lock, LockAcquire current_lock -> (
-    match (Lock.get_access_path endpoint_lock, Lock.get_access_path current_lock) with
-    | ((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 since we don't search the class for static locks *)
-        true
-    | ((Var.LogicalVar _, _), _ :: _), _ | _, ((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 @."
-          CriticalPair.pp current_elem
-    | ((_, typ1), _), ((_, 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.CriticalPair.loc endpoint_elem.CriticalPair.loc < 0 )
+      (* first elem is a class object (see [lock_of_class]), so always report because the
+         reverse ordering on the events will not occur since we don't search the class for static locks *)
+      Lock.is_class_object endpoint_lock
+      ||
+      match Lock.compare_wrt_reporting endpoint_lock current_lock with
+      | 0 ->
+          Location.compare current_elem.CriticalPair.loc endpoint_elem.CriticalPair.loc < 0
+      | c ->
+          c < 0 )
 
 
 let should_report pdesc =

infer/src/concurrency/starvationDomain.ml

@@ -116,6 +116,8 @@ module Lock = struct
         false
 
 
+  let is_class_object = function {root= Class _} -> true | _ -> false
+
   (* using an indentifier for a class object, create an access path representing that lock;
      this is for synchronizing on Java class objects only *)
   let path_of_java_class =
@@ -173,8 +175,6 @@ module Lock = struct
         L.die InternalError "Non-Java methods cannot be synchronized.@\n"
 
 
-  let get_access_path {path} = path
-
   let pp fmt {root; path} =
     let pp_path fmt ((var, typ), accesses) =
       F.fprintf fmt "(%a:%a)" Var.pp var (Typ.pp_full Pp.text) typ ;
@@ -203,6 +203,10 @@ module Lock = struct
 
 
   let pp_locks fmt lock = F.fprintf fmt " locks %a" describe lock
+
+  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)
 end
 
 module Event = struct

infer/src/concurrency/starvationDomain.mli

@@ -49,10 +49,15 @@ module Lock : sig
   (** make a lock if the expression is rooted at a global or a formal parameter, or represents a
       class object *)
 
-  val get_access_path : t -> AccessPath.t
-
   val make_java_synchronized : FormalMap.t -> Procname.t -> t option
   (** create the monitor locked when entering a synchronized java method *)
+
+  val is_class_object : t -> bool
+  (** is the lock a class object such as in [synchronized(MyClass.class){}] or
+      [static synchronized void foo()] *)
+
+  val compare_wrt_reporting : t -> t -> int
+  (** a stable order for avoiding reporting deadlocks twice based on the root variable type *)
 end
 
 module Event : sig