[classloads] record at most one load for each class

Reviewed By: ezgicicek

Differential Revision: D13750609

fbshipit-source-id: cd55a3370

infer/src/concurrency/ExplicitTrace.ml

@@ -20,6 +20,14 @@ module type Element = sig
   val pp_human : Format.formatter -> t -> unit
 end
 
+type 'a comparator = 'a -> Location.t -> 'a -> Location.t -> int
+
+module type Comparator = sig
+  type elem_t
+
+  val comparator : elem_t comparator
+end
+
 module type TraceElem = sig
   type elem_t
 
@@ -38,12 +46,14 @@ module type TraceElem = sig
   module FiniteSet : FiniteSet with type elt = t
 end
 
-module MakeTraceElem (Elem : Element) : TraceElem with type elem_t = Elem.t = struct
+module MakeTraceElemWithComparator (Elem : Element) (Comp : Comparator with type elem_t = Elem.t) :
+  TraceElem with type elem_t = Elem.t = struct
   type elem_t = Elem.t
 
   module T = struct
-    type t = {elem: Elem.t; loc: Location.t; trace: CallSite.t list [@compare.ignore]}
+    type t = {elem: Elem.t; loc: Location.t; trace: CallSite.t list}
-    [@@deriving compare]
+
+    let compare {elem; loc} {elem= elem'; loc= loc'} = Comp.comparator elem loc elem' loc'
 
     let pp fmt {elem} = Elem.pp fmt elem
 
@@ -80,3 +90,23 @@ module MakeTraceElem (Elem : Element) : TraceElem with type elem_t = Elem.t = st
     let with_callsite astate callsite = map (fun e -> with_callsite e callsite) astate
   end
 end
+
+module MakeTraceElem (Elem : Element) : TraceElem with type elem_t = Elem.t = struct
+  module Comp = struct
+    type elem_t = Elem.t
+
+    let comparator elem loc elem' loc' = [%compare: Elem.t * Location.t] (elem, loc) (elem', loc')
+  end
+
+  include MakeTraceElemWithComparator (Elem) (Comp)
+end
+
+module MakeTraceElemModuloLocation (Elem : Element) : TraceElem with type elem_t = Elem.t = struct
+  module Comp = struct
+    type elem_t = Elem.t
+
+    let comparator elem _loc elem' _loc' = Elem.compare elem elem'
+  end
+
+  include MakeTraceElemWithComparator (Elem) (Comp)
+end

infer/src/concurrency/ExplicitTrace.mli

@@ -25,9 +25,7 @@ end
 module type TraceElem = sig
   type elem_t
 
-  (** An [elem] which occured at [loc], after the chain of steps (usually calls) in [trace].
+  (** An [elem] which occured at [loc], after the chain of steps (usually calls) in [trace]. *)
-      The [compare] function ignores traces, meaning any two traces leading to the same [elem] and
-      [loc] are equal.  This has consequences on the powerset domain. *)
   type t = private {elem: elem_t; loc: Location.t; trace: CallSite.t list}
 
   (** Both [pp] and [pp_human] simply call the same function on the trace element. *)
@@ -43,10 +41,12 @@ module type TraceElem = sig
   val with_callsite : t -> CallSite.t -> t
   (** Push given callsite onto trace, extending the call chain by one. *)
 
-  (** A powerset of traces, where there is at most one trace for each dinstinct pair of [elem] and
+  (** A powerset of traces. *)
-      [loc].  The traces in the set have priority over those [add]ed.  [join] is non-deterministic
-      as to which representative is kept (due to the implementation of [Set.union]). *)
   module FiniteSet : FiniteSet with type elt = t
 end
 
+(* The [compare] function produced ignores traces but *not* locations *)
 module MakeTraceElem (Elem : Element) : TraceElem with type elem_t = Elem.t
+
+(* The [compare] function produced ignores traces *and* locations -- it is just [Elem.compare] *)
+module MakeTraceElemModuloLocation (Elem : Element) : TraceElem with type elem_t = Elem.t

infer/src/concurrency/classLoadsDomain.ml

@@ -13,7 +13,7 @@ module ClassLoad = struct
   let pp_human = pp
 end
 
-module Event = ExplicitTrace.MakeTraceElem (ClassLoad)
+module Event = ExplicitTrace.MakeTraceElemModuloLocation (ClassLoad)
 include Event.FiniteSet
 
 let add ({Event.trace} as x) astate =

infer/tests/codetoanalyze/java/classloads/Makefile

@@ -52,9 +52,8 @@ infer-out/report.json: $(JAVA_DEPS) $(SOURCES) $(MAKEFILE_LIST)
 loads.exp: $(LOADS)
 	$(QUIET)for F in $(LOADS) ; do sed -e "s#^#$(TEST_REL_DIR)/$${F%.*}.java, #" $$F ; done | sort > loads.exp
 
-# FIXME change domain so that -u is not needed below
 loads.exp.test: issues.exp.test$(TEST_SUFFIX)
-	$(QUIET)cat $< | sed 's/^\([^,]*\),.*[,\[]\([^,]*\)\]$$/\1, \2/' | sort -u > $@
+	$(QUIET)cat $< | sed 's/^\([^,]*\),.*[,\[]\([^,]*\)\]$$/\1, \2/' | sort > $@
 
 .PHONY: test
 test: loads.exp loads.exp.test

infer/tests/codetoanalyze/java/classloads/Unique.java

@@ -0,0 +1,18 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+class Unique {
+  public static void main(String args[]) {
+    // two loads for the same class with distinct locations and traces should be merged into one
+    UniqueObj u = new UniqueObj();
+    u.foo();
+  }
+}
+
+class UniqueObj {
+  void foo() {}
+}