diff --git a/infer/src/concurrency/ExplicitTrace.ml b/infer/src/concurrency/ExplicitTrace.ml index d3c33ba79..a3ddc5ff6 100644 --- a/infer/src/concurrency/ExplicitTrace.ml +++ b/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]} - [@@deriving compare] + type t = {elem: Elem.t; loc: Location.t; trace: CallSite.t list} + + 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 diff --git a/infer/src/concurrency/ExplicitTrace.mli b/infer/src/concurrency/ExplicitTrace.mli index 1074465dc..e8d8edff2 100644 --- a/infer/src/concurrency/ExplicitTrace.mli +++ b/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]. - 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. *) + (** An [elem] which occured at [loc], after the chain of steps (usually calls) in [trace]. *) 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 - [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]). *) + (** A powerset of traces. *) 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 diff --git a/infer/src/concurrency/classLoadsDomain.ml b/infer/src/concurrency/classLoadsDomain.ml index 76dd4e883..b920c4265 100644 --- a/infer/src/concurrency/classLoadsDomain.ml +++ b/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 = diff --git a/infer/tests/codetoanalyze/java/classloads/Makefile b/infer/tests/codetoanalyze/java/classloads/Makefile index a608eca3b..bdd0d538b 100644 --- a/infer/tests/codetoanalyze/java/classloads/Makefile +++ b/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 diff --git a/infer/tests/codetoanalyze/java/classloads/Unique.java b/infer/tests/codetoanalyze/java/classloads/Unique.java new file mode 100644 index 000000000..9aebe3d19 --- /dev/null +++ b/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() {} +}