pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[starvation] extract explicit traces

Browse Source 
Summary: We may want to use these traces more generally, so put them into their own module.

Reviewed By: mbouaziz

Differential Revision: D10084404

fbshipit-source-id: 8f87c17f4
master
Nikos Gorogiannis 6 years ago committed by Facebook Github Bot
parent e11ec33289
commit 9b02c497f8
4 changed files with 134 additions and 92 deletions
Show Stats Download Patch File Download Diff File

77
infer/src/concurrency/ExplicitTrace.ml
Unescape View File

@ -0,0 +1,77 @@
(*
* 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.
*)
open! IStd
module F = Format
module MF = MarkupFormatter
module type FiniteSet = sig
include PrettyPrintable.PPSet
include AbstractDomain.WithBottom with type astate = t
val with_callsite : astate -> CallSite.t -> astate
end
module type TraceElem = sig
type elem_t
type t = private {elem: elem_t; loc: Location.t; trace: CallSite.t list}
include PrettyPrintable.PrintableOrderedType with type t := t
val make : elem_t -> Location.t -> t
val get_loc : t -> Location.t
val make_loc_trace : ?nesting:int -> t -> Errlog.loc_trace
val with_callsite : t -> CallSite.t -> t
module FiniteSet : FiniteSet with type elt = t
end
module MakeTraceElem (Elem : PrettyPrintable.PrintableOrderedType) :
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]
let pp fmt {elem; loc} = F.fprintf fmt "%a at %a" Elem.pp elem Location.pp loc
end
include T
let make elem loc = {elem; loc; trace= []}
let get_loc {loc; trace} = match trace with [] -> loc | hd :: _ -> CallSite.loc hd
let make_loc_trace ?(nesting = 0) e =
let call_trace, nesting =
List.fold e.trace ~init:([], nesting) ~f:(fun (tr, ns) callsite ->
let elem_descr =
F.asprintf "Method call: %a"
(MF.wrap_monospaced Typ.Procname.pp)
(CallSite.pname callsite)
in
let elem = Errlog.make_trace_element ns (CallSite.loc callsite) elem_descr [] in
(elem :: tr, ns + 1) )
in
let endpoint_descr = F.asprintf "%a" Elem.pp e.elem in
let endpoint = Errlog.make_trace_element nesting e.loc endpoint_descr [] in
List.rev (endpoint :: call_trace)
let with_callsite elem callsite = {elem with trace= callsite :: elem.trace}
module FiniteSet = struct
include AbstractDomain.FiniteSet (T)
let with_callsite astate callsite = map (fun e -> with_callsite e callsite) astate
end
end

47
infer/src/concurrency/ExplicitTrace.mli
Unescape View File

@ -0,0 +1,47 @@
(*
* 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.
*)
open! IStd
(** A powerset domain of traces, with bottom = empty and join = union *)
module type FiniteSet = sig
include PrettyPrintable.PPSet
include AbstractDomain.WithBottom with type astate = t
val with_callsite : astate -> CallSite.t -> astate
(** Push given callsite onto all traces in set. Cf [TraceElem.with_callsite] *)
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. *)
type t = private {elem: elem_t; loc: Location.t; trace: CallSite.t list}
include PrettyPrintable.PrintableOrderedType with type t := t
val make : elem_t -> Location.t -> t
val get_loc : t -> Location.t
(** Starting location of the trace: this is either [loc] if [trace==[]], or the head of [trace]. *)
val make_loc_trace : ?nesting:int -> t -> Errlog.loc_trace
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]). *)
module FiniteSet : FiniteSet with type elt = t
end
module MakeTraceElem (Elem : PrettyPrintable.PrintableOrderedType) :
TraceElem with type elem_t = Elem.t

69
infer/src/concurrency/starvationDomain.ml
Unescape View File

@ -49,60 +49,12 @@ module Lock = struct
let owner_class ((_, typ), _) = Typ.inner_name typ
end
module type TraceElem = sig
type elem_t
type t = private {elem: elem_t; loc: Location.t; trace: CallSite.t list}
include PrettyPrintable.PrintableOrderedType with type t := t
val make : elem_t -> Location.t -> t
val get_loc : t -> Location.t
val make_loc_trace : ?nesting:int -> t -> Errlog.loc_trace
val with_callsite : t -> CallSite.t -> t
end
module MakeTraceElem (Elem : PrettyPrintable.PrintableOrderedType) :
TraceElem with type elem_t = Elem.t = struct
type elem_t = Elem.t
type t = {elem: Elem.t; loc: Location.t; trace: CallSite.t list [@compare.ignore]}
[@@deriving compare]
let pp fmt {elem; loc} = F.fprintf fmt "%a at %a" Elem.pp elem Location.pp loc
let make elem loc = {elem; loc; trace= []}
let get_loc {loc; trace} = List.hd trace |> Option.value_map ~default:loc ~f:CallSite.loc
let make_loc_trace ?(nesting = 0) e =
let call_trace, nesting =
List.fold e.trace ~init:([], nesting) ~f:(fun (tr, ns) callsite ->
let elem_descr =
F.asprintf "Method call: %a"
(MF.wrap_monospaced Typ.Procname.pp)
(CallSite.pname callsite)
in
let elem = Errlog.make_trace_element ns (CallSite.loc callsite) elem_descr [] in
(elem :: tr, ns + 1) )
in
let endpoint_descr = F.asprintf "%a" Elem.pp e.elem in
let endpoint = Errlog.make_trace_element nesting e.loc endpoint_descr [] in
List.rev (endpoint :: call_trace)
let with_callsite elem callsite = {elem with trace= callsite :: elem.trace}
end
module Event = struct
type severity_t = Low | Medium | High [@@deriving compare]
type event_t = LockAcquire of Lock.t | MayBlock of (string * severity_t) [@@deriving compare]
include MakeTraceElem (struct
include ExplicitTrace.MakeTraceElem (struct
type t = event_t [@@deriving compare]
let pp fmt = function
@ -133,12 +85,7 @@ module Event = struct
header_step :: trace
end
module EventDomain = struct
include AbstractDomain.FiniteSet (Event)
let with_callsite astate callsite =
fold (fun e acc -> add (Event.with_callsite e callsite) acc) astate empty
end
module EventDomain = Event.FiniteSet
module Order = struct
type order_t = {first: Lock.t; eventually: Event.t} [@@deriving compare]
@ -151,7 +98,7 @@ module Order = struct
let pp fmt {first} = Lock.pp fmt first
end
include MakeTraceElem (E)
include ExplicitTrace.MakeTraceElem (E)
let may_deadlock {elem= {first; eventually}} {elem= {first= first'; eventually= eventually'}} =
match (eventually.elem, eventually'.elem) with
@ -176,13 +123,7 @@ module Order = struct
header_step :: trace
end
module OrderDomain = struct
include AbstractDomain.FiniteSet (Order)
let with_callsite lo callsite =
fold (fun o acc -> add (Order.with_callsite o callsite) acc) lo empty
end
module OrderDomain = Order.FiniteSet
module LockStack = AbstractDomain.StackDomain (Event)
module LockState = struct
@ -216,7 +157,7 @@ module LockState = struct
end
module UIThreadExplanationDomain = struct
include MakeTraceElem (struct
include ExplicitTrace.MakeTraceElem (struct
type t = string [@@deriving compare]
let pp = String.pp

33
infer/src/concurrency/starvationDomain.mli
Unescape View File

@ -19,25 +19,6 @@ module Lock : sig
val equal : t -> t -> bool
end
module type TraceElem = sig
type elem_t
(** An [elem] which occured [loc], after the chain of procedure calls in [trace] *)
type t = private {elem: elem_t; loc: Location.t; trace: CallSite.t list}
include PrettyPrintable.PrintableOrderedType with type t := t
val make : elem_t -> Location.t -> t
val get_loc : t -> Location.t
(** Starting location of the trace: this is either [loc] if [trace] is empty, or the head of [trace]. *)
val make_loc_trace : ?nesting:int -> t -> Errlog.loc_trace
val with_callsite : t -> CallSite.t -> t
(** Push given callsite onto [trace], extending the call chain by one. *)
end
(** Represents the existence of a program path from the current method to the eventual acquisition
of a lock or a blocking call. Equality/comparison disregards the call trace but includes
location. *)
@ -46,12 +27,12 @@ module Event : sig
type event_t = LockAcquire of Lock.t | MayBlock of (string * severity_t) [@@deriving compare]
include TraceElem with type elem_t = event_t
include ExplicitTrace.TraceElem with type elem_t = event_t
val make_trace : ?header:string -> Typ.Procname.t -> t -> Errlog.loc_trace
end
module EventDomain : module type of AbstractDomain.FiniteSet (Event)
module EventDomain : ExplicitTrace.FiniteSet with type elt = Event.t
(** Represents the existence of a program path to the [first] lock being taken in the current
method or, transitively, a callee *in the same class*, and, which continues (to potentially
@ -61,7 +42,7 @@ module EventDomain : module type of AbstractDomain.FiniteSet (Event)
module Order : sig
type order_t = private {first: Lock.t; eventually: Event.t}
include TraceElem with type elem_t = order_t
include ExplicitTrace.TraceElem with type elem_t = order_t
val may_deadlock : t -> t -> bool
(** check if two pairs are symmetric in terms of locks, where locks are compared modulo the
@ -70,16 +51,12 @@ module Order : sig
val make_trace : ?header:string -> Typ.Procname.t -> t -> Errlog.loc_trace
end
module OrderDomain : sig
include PrettyPrintable.PPSet with type elt = Order.t
include AbstractDomain.WithBottom with type astate = t
end
module OrderDomain : ExplicitTrace.FiniteSet with type elt = Order.t
module LockState : AbstractDomain.WithBottom
module UIThreadExplanationDomain : sig
include TraceElem with type elem_t = string
include ExplicitTrace.TraceElem with type elem_t = string
val make_trace : ?header:string -> Typ.Procname.t -> t -> Errlog.loc_trace
end

Write Preview
Loading…
Cancel
Save