[starvation] acquisitions mod location

Summary:
The starvation domain keeps a domain element per distinct pair of lock object and source location.  This was used to counteract the imprecision of implicit Quandary-style traces.  Starvation has used explicit traces for a long time now, so keeping all these elements is expensive (in fact, in some cases exponential) and of no value.  Now, lock object identity is the only distinguishing feature of a domain element.

Also, fix some pretty printing for debugging purposes.

Reviewed By: jvillard

Differential Revision: D24829306

fbshipit-source-id: 22e12f9c1

infer/src/absint/ExplicitTrace.ml

@@ -70,7 +70,8 @@ module MakeTraceElemWithComparator
 
     let pp fmt {elem; loc; trace} =
       let pp_trace fmt trace = PrettyPrintable.pp_collection ~pp_item:CallSite.pp fmt trace in
-      F.fprintf fmt "{elem= %a; loc= %a; trace= %a}" Elem.pp elem Location.pp loc pp_trace trace
+      F.fprintf fmt "{@[elem= %a;@;loc= %a;@;trace= %a@]}" Elem.pp elem Location.pp loc pp_trace
+        trace
 
 
     let describe fmt {elem} = Elem.describe fmt elem

infer/src/absint/ExplicitTrace.mli

@@ -52,9 +52,14 @@ module type TraceElem = sig
   module FiniteSet : FiniteSet with type elt = t
 end
 
-(* The [compare] function produced ignores traces but *not* locations *)
-module MakeTraceElem (Elem : Element) (CallPrinter : CallPrinter) :
-  TraceElem with type elem_t = Elem.t
+include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
+  sig
+  [@@@warning "-60"]
+
+  (* The [compare] function produced ignores traces but *not* locations *)
+  module MakeTraceElem (Elem : Element) (CallPrinter : CallPrinter) :
+    TraceElem with type elem_t = Elem.t
+end
 
 (* The [compare] function produced ignores traces *and* locations -- it is just [Elem.compare] *)
 module MakeTraceElemModuloLocation (Elem : Element) (CallPrinter : CallPrinter) :

infer/src/concurrency/starvationDomain.ml

@@ -196,14 +196,17 @@ module Event = struct
   [@@deriving compare]
 
   let pp fmt = function
-    | LockAcquire {locks} ->
-        F.fprintf fmt "LockAcquire(%a)" (PrettyPrintable.pp_collection ~pp_item:Lock.pp) locks
-    | MayBlock {callee; severity} ->
-        F.fprintf fmt "MayBlock(%a, %a)" Procname.pp callee StarvationModels.pp_severity severity
-    | StrictModeCall {callee} ->
-        F.fprintf fmt "StrictModeCall(%a)" Procname.pp callee
-    | MonitorWait {lock} ->
-        F.fprintf fmt "MonitorWait(%a)" Lock.pp lock
+    | LockAcquire {locks; thread} ->
+        F.fprintf fmt "LockAcquire(%a, %a)"
+          (PrettyPrintable.pp_collection ~pp_item:Lock.pp)
+          locks ThreadDomain.pp thread
+    | MayBlock {callee; severity; thread} ->
+        F.fprintf fmt "MayBlock(%a, %a, %a)" Procname.pp callee StarvationModels.pp_severity
+          severity ThreadDomain.pp thread
+    | StrictModeCall {callee; thread} ->
+        F.fprintf fmt "StrictModeCall(%a, %a)" Procname.pp callee ThreadDomain.pp thread
+    | MonitorWait {lock; thread} ->
+        F.fprintf fmt "MonitorWait(%a, %a)" Lock.pp lock ThreadDomain.pp thread
 
 
   let describe fmt elem =
@@ -286,7 +289,8 @@ module Acquisition = struct
   [@@deriving compare]
 
   let pp fmt {lock; loc; procname} =
-    F.fprintf fmt "<lock=%a; loc=%a; procname=%a>" Lock.pp lock Location.pp loc Procname.pp procname
+    F.fprintf fmt "<@[lock=%a;@;loc=%a;@;procname=%a@]>" Lock.pp lock Location.pp loc Procname.pp
+      procname
 
 
   let describe fmt {lock} = Lock.pp_locks fmt lock
@@ -359,7 +363,7 @@ end = struct
   let get_acquisitions {acquisitions} = acquisitions
 
   let pp fmt {map; acquisitions} =
-    F.fprintf fmt "{map= %a; acquisitions= %a}" Map.pp map Acquisitions.pp acquisitions
+    F.fprintf fmt "{@[map= %a;@;acquisitions= %a@]}" Map.pp map Acquisitions.pp acquisitions
 
 
   let join lhs rhs =
@@ -431,7 +435,7 @@ module CriticalPairElement = struct
   type t = {acquisitions: Acquisitions.t; event: Event.t} [@@deriving compare]
 
   let pp fmt {acquisitions; event} =
-    F.fprintf fmt "{acquisitions= %a; event= %a}" Acquisitions.pp acquisitions Event.pp event
+    F.fprintf fmt "{@[acquisitions= %a;@;event= %a@]}" Acquisitions.pp acquisitions Event.pp event
 
 
   let describe = pp
@@ -448,7 +452,9 @@ module CriticalPairElement = struct
 end
 
 module CriticalPair = struct
-  include ExplicitTrace.MakeTraceElem (CriticalPairElement) (ExplicitTrace.DefaultCallPrinter)
+  include ExplicitTrace.MakeTraceElemModuloLocation
+            (CriticalPairElement)
+            (ExplicitTrace.DefaultCallPrinter)
 
   let make ~loc acquisitions event = make {acquisitions; event} loc
 
@@ -675,7 +681,7 @@ module ScheduledWorkItem = struct
   type t = {procname: Procname.t; loc: Location.t; thread: ThreadDomain.t} [@@deriving compare]
 
   let pp fmt {procname; loc; thread} =
-    F.fprintf fmt "{procname= %a; loc= %a; thread= %a}" Procname.pp procname Location.pp loc
+    F.fprintf fmt "{@[procname= %a;@;loc= %a;@;thread= %a@]}" Procname.pp procname Location.pp loc
       ThreadDomain.pp thread
 end
 
@@ -705,11 +711,15 @@ let initial =
 
 let pp fmt astate =
   F.fprintf fmt
-    "{guard_map= %a; lock_state= %a; critical_pairs= %a; attributes= %a; thread= %a; \
-     scheduled_work= %a; var_state= %a}"
-    GuardToLockMap.pp astate.guard_map LockState.pp astate.lock_state CriticalPairs.pp
-    astate.critical_pairs AttributeDomain.pp astate.attributes ThreadDomain.pp astate.thread
-    ScheduledWorkDomain.pp astate.scheduled_work VarDomain.pp astate.var_state
+    "{@[guard_map= %a;@;\
+     lock_state= %a;@;\
+     critical_pairs= %a;@;\
+     attributes= %a;@;\
+     thread= %a;@;\
+     scheduled_work= %a;@;\
+     var_state= %a@]}" GuardToLockMap.pp astate.guard_map LockState.pp astate.lock_state
+    CriticalPairs.pp astate.critical_pairs AttributeDomain.pp astate.attributes ThreadDomain.pp
+    astate.thread ScheduledWorkDomain.pp astate.scheduled_work VarDomain.pp astate.var_state
 
 
 let join lhs rhs =

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

@@ -20,7 +20,7 @@ class Dedup {
     callMethodWithMultipleBlocksBad();
   }
 
-  // three reports are expected
+  // two reports are expected, last call location is always deduped in analysis
   @UiThread
   void callMethodWithMultipleBlocksBad() throws InterruptedException, ExecutionException {
     future.get();

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

@@ -1,6 +1,5 @@
 codetoanalyze/java/starvation-dedup/Dedup.java, Dedup.callMethodWithMultipleBlocksBad():void, 26, STARVATION, no_bucket, ERROR, [`void Dedup.callMethodWithMultipleBlocksBad()`,calls `Object Future.get()`]
 codetoanalyze/java/starvation-dedup/Dedup.java, Dedup.callMethodWithMultipleBlocksBad():void, 27, STARVATION, no_bucket, ERROR, [`void Dedup.callMethodWithMultipleBlocksBad()`,calls `void CountDownLatch.await()`]
-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, 9, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Interproc.interproc1Bad(InterprocA)`, locks `this` in `class Interproc`,Method call: `void Interproc.interproc2(InterprocA)`, locks `a` in `class InterprocA`,[Trace 2] `void InterprocA.interproc1Bad(Interproc)`, locks `this` in `class InterprocA`,Method call: `void InterprocA.interproc2(Interproc)`, locks `c` in `class Interproc`]