[starvation] document false positive

Summary:
Document FP due to imprecision in tracking outer lock release. In a nested `synchronized` block the outer release is not registered by the abstract domain.  The reason is that HIL is not resolving what `$bcvarX` is pointing to (in this case to `lockE`).

Reported by Andreea Costea.

Reviewed By: ezgicicek

Differential Revision: D22186240

fbshipit-source-id: 84e5e72b1

infer/tests/codetoanalyze/java/starvation/ThreadDeadlock.java

@@ -79,4 +79,23 @@ class ThreadDeadlock {
       }
     }
   }
+
+  Object lockE, lockF, lockG;
+
+  public void FP_sequentialEandGOk() {
+    synchronized (lockE) {
+      synchronized (lockF) {
+      }
+    }
+    // at this point we still believe lockE is held
+    synchronized (lockG) {
+    }
+  }
+
+  public void FP_nestedGthenEOk() {
+    synchronized (lockG) {
+      synchronized (lockE) {
+      }
+    }
+  }
 }

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

@@ -78,6 +78,8 @@ codetoanalyze/java/starvation/ThreadCalls.java, ThreadCalls.indirectJoinOnUIThre
 codetoanalyze/java/starvation/ThreadCalls.java, ThreadCalls.indirectSleepOnUIThreadBad():void, 24, STARVATION, no_bucket, ERROR, [[Trace 1] `void ThreadCalls.indirectSleepOnUIThreadBad()`, locks `this.lock` in `class ThreadCalls`,[Trace 2] `void ThreadCalls.lockAndSleepOnNonUIThread()`, locks `this.lock` in `class ThreadCalls`,Method call: `void ThreadCalls.sleepOnAnyThreadOk()`,calls `void Thread.sleep(long)`]
 codetoanalyze/java/starvation/ThreadCalls.java, ThreadCalls.joinOnUIThreadBad(java.lang.Thread):void, 40, STARVATION, no_bucket, ERROR, [`void ThreadCalls.joinOnUIThreadBad(Thread)`,calls `void Thread.join()`]
 codetoanalyze/java/starvation/ThreadCalls.java, ThreadCalls.sleepOnUIThreadBad():void, 17, STARVATION, no_bucket, ERROR, [`void ThreadCalls.sleepOnUIThreadBad()`,calls `void Thread.sleep(long)`]
+codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.FP_nestedGthenEOk():void, 96, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.FP_nestedGthenEOk()`, locks `this.lockG` in `class ThreadDeadlock`, locks `this.lockE` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.FP_sequentialEandGOk()`, locks `this.lockE` in `class ThreadDeadlock`, locks `this.lockG` in `class ThreadDeadlock`]
+codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.FP_sequentialEandGOk():void, 86, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.FP_sequentialEandGOk()`, locks `this.lockE` in `class ThreadDeadlock`, locks `this.lockG` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.FP_nestedGthenEOk()`, locks `this.lockG` in `class ThreadDeadlock`, locks `this.lockE` in `class ThreadDeadlock`]
 codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.annotatedUiThreadBad():void, 35, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.annotatedUiThreadBad()`, locks `this` in `class ThreadDeadlock`, locks `this.lockB` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.annotatedWorkerThreadBad()`, locks `this.lockB` in `class ThreadDeadlock`, locks `this` in `class ThreadDeadlock`]
 codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.annotatedWorkerThreadBad():void, 42, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.annotatedWorkerThreadBad()`, locks `this.lockB` in `class ThreadDeadlock`, locks `this` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.annotatedUiThreadBad()`, locks `this` in `class ThreadDeadlock`, locks `this.lockB` in `class ThreadDeadlock`]
 codetoanalyze/java/starvation/ThreadDeadlock.java, ThreadDeadlock.assertOnBackgroundThreadBad():void, 60, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ThreadDeadlock.assertOnBackgroundThreadBad()`, locks `this.lockC` in `class ThreadDeadlock`, locks `this` in `class ThreadDeadlock`,[Trace 2] `void ThreadDeadlock.assertOnUIThreadBad()`, locks `this` in `class ThreadDeadlock`, locks `this.lockC` in `class ThreadDeadlock`]