[starvation] allow aliasing of parameters across threads

Summary:
Introduce a new notion of equality for comparing abstract addresses in distinct threads:
```
(** Abstract address for a lock. There are two notions of equality:

    - Equality for comparing two addresses within the same thread/process/trace. Under this,
      identical globals and identical class objects compare equal. Locks represented by access paths
      rooted at method parameters must have equal access paths to compare equal. Paths rooted at
      locals are ignored.
    - Equality for comparing two addresses in two distinct threads/traces. Globals and class objects
      are compared in the same way, but locks represented by access paths rooted at parameters need
      only have equal access lists (ie [x.f.g == y.f.g]). This allows demonically aliasing
      parameters in *distinct* threads. This relation is used in [may_deadlock]. *)
```

Reviewed By: skcho

Differential Revision: D19347307

fbshipit-source-id: 9f338731b

infer/src/concurrency/starvation.ml

@@ -631,7 +631,8 @@ let report_on_parallel_composition ~should_report_starvation tenv pdesc pair loc
     let acquisitions = other_pair.CriticalPair.elem.acquisitions in
     match other_pair.CriticalPair.elem.event with
     | MayBlock (block_descr, sev)
-      when should_report_starvation && Acquisitions.lock_is_held lock acquisitions ->
+      when should_report_starvation && Acquisitions.lock_is_held_in_other_thread lock acquisitions
+      ->
         let error_message =
           Format.asprintf
             "Method %a runs on UI thread and%a, which may be held by another thread which %s."
@@ -641,7 +642,7 @@ let report_on_parallel_composition ~should_report_starvation tenv pdesc pair loc
         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
+           && Acquisitions.lock_is_held_in_other_thread lock acquisitions
            && not (Lock.equal lock monitor_lock) ->
         let error_message =
           Format.asprintf

infer/src/concurrency/starvationDomain.ml

@@ -104,6 +104,18 @@ module Lock = struct
 
   type t = {root: root; path: path} [@@deriving compare, equal]
 
+  let equal_across_threads t1 t2 =
+    match (t1.root, t2.root) with
+    | Global _, Global _ | Class _, Class _ ->
+        (* globals and class objects must be identical across threads *)
+        equal t1 t2
+    | Parameter _, Parameter _ ->
+        (* parameter position/names can be ignored across threads, if types and accesses are equal *)
+        equal_path t1.path t2.path
+    | _, _ ->
+        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 =
@@ -253,6 +265,13 @@ module Acquisitions = struct
 
   (* use the fact that location/procname are ignored in comparisons *)
   let lock_is_held lock acquisitions = mem (Acquisition.make_dummy lock) acquisitions
+
+  let lock_is_held_in_other_thread lock acquisitions =
+    exists (fun acq -> Lock.equal_across_threads lock acq.lock) acquisitions
+
+
+  let no_locks_common_across_threads acqs1 acqs2 =
+    for_all (fun acq1 -> not (lock_is_held_in_other_thread acq1.lock acqs2)) acqs1
 end
 
 module LockState : sig
@@ -384,10 +403,10 @@ module CriticalPair = struct
     ThreadDomain.can_run_in_parallel pair1.thread pair2.thread
     && Option.both (get_final_acquire t1) (get_final_acquire t2)
        |> Option.exists ~f:(fun (lock1, lock2) ->
-              (not (Lock.equal lock1 lock2))
+              (not (Lock.equal_across_threads lock1 lock2))
-              && Acquisitions.lock_is_held lock2 pair1.acquisitions
+              && Acquisitions.lock_is_held_in_other_thread lock2 pair1.acquisitions
-              && Acquisitions.lock_is_held lock1 pair2.acquisitions
+              && Acquisitions.lock_is_held_in_other_thread lock1 pair2.acquisitions
-              && Acquisitions.inter pair1.acquisitions pair2.acquisitions |> Acquisitions.is_empty
+              && Acquisitions.no_locks_common_across_threads pair1.acquisitions pair2.acquisitions
           )
 
 

infer/src/concurrency/starvationDomain.mli

@@ -23,8 +23,16 @@ module ThreadDomain : sig
   include AbstractDomain.WithBottom with type t := t
 end
 
-(** Abstraction of a path that represents a lock, special-casing comparison to work over type, base
+(** Abstract address for a lock. There are two notions of equality:
-    variable modulo this and access list *)
+
+    - Equality for comparing two addresses within the same thread/process/trace. Under this,
+      identical globals and identical class objects compare equal. Locks represented by access paths
+      rooted at method parameters must have equal access paths to compare equal. Paths rooted at
+      locals are ignored.
+    - Equality for comparing two addresses in two distinct threads/traces. Globals and class objects
+      are compared in the same way, but locks represented by access paths rooted at parameters need
+      only have equal access lists (ie [x.f.g == y.f.g]). This allows demonically aliasing
+      parameters in *distinct* threads. This relation is used in [may_deadlock]. *)
 module Lock : sig
   include PrettyPrintable.PrintableOrderedType
 
@@ -73,6 +81,9 @@ module Acquisitions : sig
 
   val lock_is_held : Lock.t -> t -> bool
   (** is the given lock in the set *)
+
+  val lock_is_held_in_other_thread : Lock.t -> t -> bool
+  (** is the given lock held, modulo memory abstraction across threads *)
 end
 
 (** An event and the currently-held locks at the time it occurred. *)

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

@@ -7,10 +7,10 @@
 
 class Interproc {
   synchronized void interproc1Bad(InterprocA a) {
-    interproc2Bad(a);
+    interproc2(a);
   }
 
-  void interproc2Bad(InterprocA b) {
+  void interproc2(InterprocA b) {
     synchronized (b) {
     }
   }
@@ -36,11 +36,11 @@ class Interproc {
 }
 
 class InterprocA {
-  synchronized void FN_interproc1Bad(Interproc c) {
+  synchronized void interproc1Bad(Interproc c) {
-    interproc2Bad(c);
+    interproc2(c);
   }
 
-  void interproc2Bad(Interproc d) {
+  void interproc2(Interproc d) {
     synchronized (d) {
     }
   }

infer/tests/codetoanalyze/java/starvation-dedup/Intraproc.java

@@ -31,7 +31,7 @@ class Intraproc {
 }
 
 class IntraprocA {
-  void FN_intraBad(Intraproc o) {
+  void intraBad(Intraproc o) {
     synchronized (this) {
       synchronized (o) {
       }

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

@@ -3,3 +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/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

@@ -36,7 +36,7 @@ class Interproc {
 }
 
 class InterprocA {
-  synchronized void FN_interproc1Bad(Interproc c) {
+  synchronized void interproc1Bad(Interproc c) {
     interproc2Bad(c);
   }
 

infer/tests/codetoanalyze/java/starvation/Intraproc.java

@@ -31,7 +31,7 @@ class Intraproc {
 }
 
 class IntraprocA {
-  void FN_intraBad(Intraproc o) {
+  void intraBad(Intraproc o) {
     synchronized (this) {
       synchronized (o) {
       }

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

@@ -0,0 +1,44 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+class Parameters {
+  private static void syncOnParam(Object x) {
+    synchronized (x) {
+    }
+  }
+
+  // Next two methods will deadlock
+  public synchronized void oneWaySyncOnParamBad(Object x) {
+    syncOnParam(x);
+  }
+
+  public void otherWaySyncOnParamBad(Object x) {
+    synchronized (x) {
+      synchronized (this) {
+      }
+    }
+  }
+
+  private static void emulateSynchronized(Parameters self) {
+    synchronized (self) {
+    }
+  }
+
+  Parameters someObject;
+
+  // Next two methods will deadlock
+  public synchronized void FN_oneWayEmulateSyncBad() {
+    emulateSynchronized(someObject);
+  }
+
+  public void FN_anotherWayEmulateSyncBad() {
+    synchronized (someObject) {
+      synchronized (this) {
+      }
+    }
+  }
+}

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

@@ -19,6 +19,10 @@ codetoanalyze/java/starvation/InnerClass.java, InnerClass.outerInnerBad(InnerCla
 codetoanalyze/java/starvation/InnerClass.java, InnerClass.outerInnerBad(InnerClass$InnerClassA):void, 16, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void InnerClass.outerInnerBad(InnerClass$InnerClassA)`, locks `this` in `class InnerClass`,Method call: `void InnerClass$InnerClassA.baz()`, locks `this` in `class InnerClass$InnerClassA`,[Trace 2] `void InnerClass$InnerClassA.innerOuterBad()`, locks `this` in `class InnerClass$InnerClassA`,Method call: `void InnerClass.bar()`, 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 `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 `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.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.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()`]
 codetoanalyze/java/starvation/LockSensitivity.java, LockSensitivity.FP_assertHoldsLockAB_Ok():void, 41, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void LockSensitivity.FP_assertHoldsLockAB_Ok()`, locks `this.monitorA` in `class LockSensitivity`, locks `this.monitorB` in `class LockSensitivity`,[Trace 2] `void LockSensitivity.FP_assertHoldsLockBA_Ok()`, locks `this.monitorB` in `class LockSensitivity`, locks `this.monitorA` in `class LockSensitivity`]
 codetoanalyze/java/starvation/LockSensitivity.java, LockSensitivity.FP_assertHoldsLockBA_Ok():void, 46, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void LockSensitivity.FP_assertHoldsLockBA_Ok()`, locks `this.monitorB` in `class LockSensitivity`, locks `this.monitorA` in `class LockSensitivity`,[Trace 2] `void LockSensitivity.FP_assertHoldsLockAB_Ok()`, locks `this.monitorA` in `class LockSensitivity`, locks `this.monitorB` in `class LockSensitivity`]
@@ -42,6 +46,7 @@ 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.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`]
 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`]