From e7323dfa3325a1903ff7180b2d211d7d203e8457 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Wed, 9 Oct 2019 06:05:02 -0700 Subject: [PATCH] [starvation] fix dependency between models and domain Summary: StarvationModels depended on StarvationDomain which is the wrong way around, and forbids using *Models from *Domain. Reviewed By: mityal Differential Revision: D17809431 fbshipit-source-id: 5aa369e7c --- infer/src/concurrency/ConcurrencyModels.mli | 1 - infer/src/concurrency/StarvationModels.ml | 9 ++++++++- infer/src/concurrency/StarvationModels.mli | 8 ++++++-- infer/src/concurrency/starvation.ml | 6 +++--- infer/src/concurrency/starvationDomain.ml | 14 +++++--------- infer/src/concurrency/starvationDomain.mli | 9 +++++---- 6 files changed, 27 insertions(+), 20 deletions(-) diff --git a/infer/src/concurrency/ConcurrencyModels.mli b/infer/src/concurrency/ConcurrencyModels.mli index 2e8286fab..a3a130695 100644 --- a/infer/src/concurrency/ConcurrencyModels.mli +++ b/infer/src/concurrency/ConcurrencyModels.mli @@ -6,7 +6,6 @@ *) open! IStd -module F = Format (** effect of call plus Hil expressions being un/locked, if known *) type lock_effect = diff --git a/infer/src/concurrency/StarvationModels.ml b/infer/src/concurrency/StarvationModels.ml index e4083d63f..5b3aac204 100644 --- a/infer/src/concurrency/StarvationModels.ml +++ b/infer/src/concurrency/StarvationModels.ml @@ -6,6 +6,7 @@ *) open! IStd +module F = Format let is_synchronized_library_call = let targets = ["java.lang.StringBuffer"; "java.util.Hashtable"; "java.util.Vector"] in @@ -89,9 +90,15 @@ let empty_or_excessive_timeout actuals = false +type severity = Low | Medium | High [@@deriving compare] + +let pp_severity fmt sev = + let msg = match sev with Low -> "Low" | Medium -> "Medium" | High -> "High" in + F.pp_print_string fmt msg + + let standard_matchers = let open MethodMatcher in - let open StarvationDomain.Event in let high_sev = [ {default with classname= "java.lang.Thread"; methods= ["sleep"]} ; { default with diff --git a/infer/src/concurrency/StarvationModels.mli b/infer/src/concurrency/StarvationModels.mli index f9d39fed1..2637e6a32 100644 --- a/infer/src/concurrency/StarvationModels.mli +++ b/infer/src/concurrency/StarvationModels.mli @@ -6,9 +6,13 @@ *) open! IStd +module F = Format -val may_block : - Tenv.t -> Typ.Procname.t -> HilExp.t list -> StarvationDomain.Event.severity_t option +type severity = Low | Medium | High [@@deriving compare] + +val pp_severity : F.formatter -> severity -> unit + +val may_block : Tenv.t -> Typ.Procname.t -> HilExp.t list -> severity option (** is the method call potentially blocking, given the actuals passed? *) val is_strict_mode_violation : Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 20e96c9f5..6d8737912 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -183,7 +183,7 @@ module ReportMap : sig val add_deadlock : report_add_t - val add_starvation : StarvationDomain.Event.severity_t -> report_add_t + val add_starvation : StarvationModels.severity -> report_add_t val add_strict_mode_violation : report_add_t @@ -192,7 +192,7 @@ module ReportMap : sig val log : IssueLog.t -> Tenv.t -> Procdesc.t -> t -> IssueLog.t end = struct type problem = - | Starvation of StarvationDomain.Event.severity_t + | Starvation of StarvationModels.severity | Deadlock of int | StrictModeViolation of int | LocklessViolation of int @@ -298,7 +298,7 @@ end = struct let lockless_violations = List.filter_map problems ~f:filter_map_lockless_violation in log_reports (compare_reports Int.compare) loc deadlocks issue_log |> log_reports (compare_reports Int.compare) loc lockless_violations - |> log_reports (compare_reports StarvationDomain.Event.compare_severity_t) loc starvations + |> log_reports (compare_reports StarvationModels.compare_severity) loc starvations |> log_reports (compare_reports Int.compare) loc strict_mode_violations in LocMap.fold log_location map start_issue_log diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 78b6e3088..b4400c944 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -48,21 +48,17 @@ module Lock = struct end module Event = struct - type severity_t = Low | Medium | High [@@deriving compare] - - let pp_severity fmt sev = - let msg = match sev with Low -> "Low" | Medium -> "Medium" | High -> "High" in - F.pp_print_string fmt msg - - - type t = LockAcquire of Lock.t | MayBlock of (string * severity_t) | StrictModeCall of string + type t = + | LockAcquire of Lock.t + | MayBlock of (string * StarvationModels.severity) + | StrictModeCall of string [@@deriving compare] let pp fmt = function | LockAcquire lock -> F.fprintf fmt "LockAcquire(%a)" Lock.pp lock | MayBlock (msg, sev) -> - F.fprintf fmt "MayBlock(%s, %a)" msg pp_severity sev + F.fprintf fmt "MayBlock(%s, %a)" msg StarvationModels.pp_severity sev | StrictModeCall msg -> F.fprintf fmt "StrictModeCall(%s)" msg diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index a92da4a49..4203dd06d 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -22,9 +22,10 @@ module Lock : sig end module Event : sig - type severity_t = Low | Medium | High [@@deriving compare] - - type t = LockAcquire of Lock.t | MayBlock of (string * severity_t) | StrictModeCall of string + type t = + | LockAcquire of Lock.t + | MayBlock of (string * StarvationModels.severity) + | StrictModeCall of string [@@deriving compare] val describe : F.formatter -> t -> unit @@ -96,7 +97,7 @@ val acquire : Tenv.t -> t -> procname:Typ.Procname.t -> loc:Location.t -> Lock.t val release : t -> Lock.t list -> t (** simultaneously release a number of locks, no-op if list is empty *) -val blocking_call : callee:Typ.Procname.t -> Event.severity_t -> loc:Location.t -> t -> t +val blocking_call : callee:Typ.Procname.t -> StarvationModels.severity -> loc:Location.t -> t -> t val strict_mode_call : callee:Typ.Procname.t -> loc:Location.t -> t -> t