diff --git a/infer/src/checkers/classLoadsDomain.ml b/infer/src/checkers/classLoadsDomain.ml index 7e2b81340..1abb6fedf 100644 --- a/infer/src/checkers/classLoadsDomain.ml +++ b/infer/src/checkers/classLoadsDomain.ml @@ -12,11 +12,10 @@ module ClassLoad = struct include String let describe = pp - - let pp_call = ExplicitTrace.default_pp_call end -module Event = ExplicitTrace.MakeTraceElemModuloLocation (ClassLoad) +module Event = + ExplicitTrace.MakeTraceElemModuloLocation (ClassLoad) (ExplicitTrace.DefaultCallPrinter) include Event.FiniteSet let add ({Event.trace} as x) astate = diff --git a/infer/src/concurrency/ExplicitTrace.ml b/infer/src/concurrency/ExplicitTrace.ml index c16ced5ab..7c4c41275 100644 --- a/infer/src/concurrency/ExplicitTrace.ml +++ b/infer/src/concurrency/ExplicitTrace.ml @@ -8,10 +8,6 @@ open! IStd module F = Format module MF = MarkupFormatter -let default_pp_call fmt callsite = - F.fprintf fmt "Method call: %a" (MF.wrap_monospaced Typ.Procname.pp) (CallSite.pname callsite) - - module type FiniteSet = sig include AbstractDomain.FiniteSetS @@ -22,8 +18,15 @@ module type Element = sig include PrettyPrintable.PrintableOrderedType val describe : Format.formatter -> t -> unit +end + +module type CallPrinter = PrettyPrintable.PrintableType with type t = CallSite.t + +module DefaultCallPrinter : CallPrinter = struct + type t = CallSite.t - val pp_call : Format.formatter -> CallSite.t -> unit + let pp fmt callsite = + F.fprintf fmt "Method call: %a" (MF.wrap_monospaced Typ.Procname.pp) (CallSite.pname callsite) end type 'a comparator = 'a -> Location.t -> 'a -> Location.t -> int @@ -54,8 +57,10 @@ module type TraceElem = sig module FiniteSet : FiniteSet with type elt = t end -module MakeTraceElemWithComparator (Elem : Element) (Comp : Comparator with type elem_t = Elem.t) : - TraceElem with type elem_t = Elem.t = struct +module MakeTraceElemWithComparator + (Elem : Element) + (CallPrinter : CallPrinter) + (Comp : Comparator with type elem_t = Elem.t) : TraceElem with type elem_t = Elem.t = struct type elem_t = Elem.t module T = struct @@ -66,8 +71,6 @@ module MakeTraceElemWithComparator (Elem : Element) (Comp : Comparator with type let pp fmt {elem} = Elem.pp fmt elem let describe fmt {elem} = Elem.describe fmt elem - - let pp_call = Elem.pp_call end include T @@ -84,7 +87,7 @@ module MakeTraceElemWithComparator (Elem : Element) (Comp : Comparator with type let make_loc_trace ?(nesting = 0) e = let call_trace, nesting = List.fold e.trace ~init:([], nesting) ~f:(fun (tr, ns) callsite -> - let descr = F.asprintf "%a" pp_call callsite in + let descr = F.asprintf "%a" CallPrinter.pp callsite in let call = Errlog.make_trace_element ns (CallSite.loc callsite) descr [] in (call :: tr, ns + 1) ) in @@ -102,22 +105,24 @@ module MakeTraceElemWithComparator (Elem : Element) (Comp : Comparator with type end end -module MakeTraceElem (Elem : Element) : TraceElem with type elem_t = Elem.t = struct +module MakeTraceElem (Elem : Element) (CallPrinter : CallPrinter) : + 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) + include MakeTraceElemWithComparator (Elem) (CallPrinter) (Comp) end -module MakeTraceElemModuloLocation (Elem : Element) : TraceElem with type elem_t = Elem.t = struct +module MakeTraceElemModuloLocation (Elem : Element) (CallPrinter : CallPrinter) : + 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) + include MakeTraceElemWithComparator (Elem) (CallPrinter) (Comp) end diff --git a/infer/src/concurrency/ExplicitTrace.mli b/infer/src/concurrency/ExplicitTrace.mli index 2b5d84c60..7ede52f53 100644 --- a/infer/src/concurrency/ExplicitTrace.mli +++ b/infer/src/concurrency/ExplicitTrace.mli @@ -7,8 +7,6 @@ open! IStd -val default_pp_call : Format.formatter -> CallSite.t -> unit - (** A powerset domain of traces, with bottom = empty and join = union *) module type FiniteSet = sig include AbstractDomain.FiniteSetS @@ -22,10 +20,13 @@ module type Element = sig val describe : Format.formatter -> t -> unit (** Pretty printer used for trace construction; [pp] is used for debug output. *) - - val pp_call : Format.formatter -> CallSite.t -> unit end +module type CallPrinter = PrettyPrintable.PrintableType with type t = CallSite.t + +(** Printer which outputs "Method call: " *) +module DefaultCallPrinter : CallPrinter + module type TraceElem = sig type elem_t @@ -52,7 +53,9 @@ module type TraceElem = sig end (* The [compare] function produced ignores traces but *not* locations *) -module MakeTraceElem (Elem : Element) : TraceElem with type elem_t = Elem.t +module MakeTraceElem (Elem : Element) (CallPrinter : CallPrinter) : + 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 +module MakeTraceElemModuloLocation (Elem : Element) (CallPrinter : CallPrinter) : + TraceElem with type elem_t = Elem.t diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index bc61a8b4c..f9d6f4bcf 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -109,16 +109,19 @@ module Access = struct (MF.monospaced_to_string (Typ.Procname.get_method pname)) | InterfaceCall pname -> F.fprintf fmt "Call to un-annotated interface method %a" Typ.Procname.pp pname +end +module CallPrinter = struct + type t = CallSite.t - let pp_call fmt cs = F.fprintf fmt "call to %a" Typ.Procname.pp (CallSite.pname cs) + let pp fmt cs = F.fprintf fmt "call to %a" Typ.Procname.pp (CallSite.pname cs) end module TraceElem = struct (** This choice means the comparator is insensitive to the location access. This preserves correctness only if the overlying comparator (AccessSnapshot) takes into account the characteristics of the access (eg lock status). *) - include ExplicitTrace.MakeTraceElemModuloLocation (Access) + include ExplicitTrace.MakeTraceElemModuloLocation (Access) (CallPrinter) let is_write {elem} = Access.is_write elem diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index d78bad955..cfcc4d1ab 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -57,8 +57,6 @@ module Lock = struct F.fprintf fmt "%a%a" (MF.wrap_monospaced pp) lock pp_owner lock - let pp_call = ExplicitTrace.default_pp_call - let pp_locks fmt lock = F.fprintf fmt " locks %a" describe lock end @@ -96,12 +94,9 @@ module Event = struct F.pp_print_string fmt msg | StrictModeCall msg -> F.pp_print_string fmt msg - - - let pp_call = ExplicitTrace.default_pp_call end - include ExplicitTrace.MakeTraceElem (EventElement) + include ExplicitTrace.MakeTraceElem (EventElement) (ExplicitTrace.DefaultCallPrinter) let make_acquire lock loc = make (LockAcquire lock) loc @@ -140,11 +135,9 @@ module Order = struct let describe fmt {first} = Lock.pp_locks fmt first - - let pp_call = ExplicitTrace.default_pp_call end - include ExplicitTrace.MakeTraceElem (OrderElement) + include ExplicitTrace.MakeTraceElem (OrderElement) (ExplicitTrace.DefaultCallPrinter) let may_deadlock {elem= {first; eventually}} {elem= {first= first'; eventually= eventually'}} = match (eventually.elem, eventually'.elem) with @@ -207,11 +200,9 @@ module UIThreadExplanationDomain = struct include String let describe = pp - - let pp_call = ExplicitTrace.default_pp_call end - include ExplicitTrace.MakeTraceElem (StringElement) + include ExplicitTrace.MakeTraceElem (StringElement) (ExplicitTrace.DefaultCallPrinter) let join lhs rhs = if List.length lhs.trace <= List.length rhs.trace then lhs else rhs