From f7ee0c2a2dc4ffcb544d26411a74a4b2acf28138 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 19 Apr 2018 12:12:55 -0700 Subject: [PATCH] [racerd] use `ThreadsDomain.astate` instead of bool in `AccessData` Reviewed By: ngorogiannis Differential Revision: D7423167 fbshipit-source-id: 79daa3a --- infer/src/concurrency/RacerD.ml | 20 ++++++++------------ infer/src/concurrency/RacerDDomain.ml | 23 ++++++++++++++++++----- infer/src/concurrency/RacerDDomain.mli | 13 +++++++++++-- 3 files changed, 37 insertions(+), 19 deletions(-) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 3bef4e5d9..5502664b0 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -390,7 +390,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (* if the access occurred on a main thread in the callee, we should remember this when moving it to the callee. if we don't know what thread it ran on, use the caller's thread *) - let threads' = if pre.thread then ThreadsDomain.AnyThreadButSelf else threads in + let threads' = + ThreadsDomain.integrate_summary ~callee_astate:pre.thread ~caller_astate:threads + in let pre' = AccessSnapshot.make locks' threads' ownership_precondition' pdesc in update_caller_accesses pre' callee_accesses accesses_acc in @@ -516,15 +518,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct LocksDomain.integrate_summary ~caller_astate:astate.locks ~callee_astate:locks in - let threads = - (* if we know the callee runs on the main thread, assume the caller does too. - otherwise, keep the caller's thread context *) - match threads with - | ThreadsDomain.AnyThreadButSelf -> - threads - | _ -> - astate.threads - in let accesses = add_callee_accesses astate accesses locks threads actuals callee_pname pdesc loc @@ -539,6 +532,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct callee_pdesc in let wobbly_paths = StabilityDomain.join wobbly_paths callee_wps_rebased in + let threads = + ThreadsDomain.integrate_summary ~caller_astate:astate.threads + ~callee_astate:threads + in {locks; threads; accesses; ownership; attribute_map; wobbly_paths} | None -> let should_assume_returns_ownership (call_flags: CallFlags.t) actuals = @@ -1301,8 +1298,7 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi (* protected read. report unprotected writes and opposite protected writes as conflicts *) let can_conflict (pre1: AccessSnapshot.t) (pre2: AccessSnapshot.t) = if pre1.lock && pre2.lock then false - else if pre1.thread && pre2.thread then false - else true + else ThreadsDomain.can_conflict pre1.thread pre2.thread in let conflicting_writes = List.filter diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 09deb560a..97e29337d 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -235,11 +235,21 @@ module ThreadsDomain = struct "AnyThread" ) + (* at least one access is known to occur on a background thread *) + let can_conflict astate1 astate2 = + match join astate1 astate2 with AnyThread -> true | NoThread | AnyThreadButSelf -> false + + let is_empty = function NoThread -> true | _ -> false let is_any_but_self = function AnyThreadButSelf -> true | _ -> false let is_any = function AnyThread -> true | _ -> false + + let integrate_summary ~caller_astate ~callee_astate = + (* if we know the callee runs on the main thread, assume the caller does too. otherwise, keep + the caller's thread context *) + match callee_astate with AnyThreadButSelf -> callee_astate | _ -> caller_astate end module PathDomain = SinkTrace.Make (TraceElem) @@ -409,23 +419,26 @@ module AccessSnapshot = struct F.fprintf fmt "False" end - type t = {thread: bool; lock: bool; ownership_precondition: Precondition.t} [@@deriving compare] + type t = + {thread: ThreadsDomain.astate; lock: bool; ownership_precondition: Precondition.t} + [@@deriving compare] - let make lock threads ownership_precondition pdesc = + let make lock thread ownership_precondition pdesc = (* shouldn't be creating metadata for accesses that are known to be owned; we should discard such accesses *) assert (not (Precondition.is_true ownership_precondition)) ; - let thread = ThreadsDomain.is_any_but_self threads in let lock = LocksDomain.is_locked lock || Procdesc.is_java_synchronized pdesc in {thread; lock; ownership_precondition} let is_unprotected {thread; lock; ownership_precondition} = - not thread && not lock && not (Precondition.is_true ownership_precondition) + not (ThreadsDomain.is_any_but_self thread) && not lock + && not (Precondition.is_true ownership_precondition) let pp fmt {thread; lock; ownership_precondition} = - F.fprintf fmt "Thread: %b Lock: %b Pre: %a" thread lock Precondition.pp ownership_precondition + F.fprintf fmt "Thread: %a Lock: %b Pre: %a" ThreadsDomain.pp thread lock Precondition.pp + ownership_precondition end module AccessDomain = struct diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 64e4340bb..e83cd24c0 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -86,7 +86,15 @@ module ThreadsDomain : sig include AbstractDomain.WithBottom with type astate := astate + val can_conflict : astate -> astate -> bool + (** return true if two accesses with these thread values can run concurrently *) + val is_any : astate -> bool + + val is_any_but_self : astate -> bool + + val integrate_summary : caller_astate:astate -> callee_astate:astate -> astate + (** integrate current state with a callee summary *) end module PathDomain : module type of SinkTrace.Make (TraceElem) @@ -169,8 +177,9 @@ module AccessSnapshot : sig val pp : F.formatter -> t -> unit [@@warning "-32"] end - type t = private {thread: bool; lock: bool; ownership_precondition: Precondition.t} - [@@deriving compare] + type t = private + {thread: ThreadsDomain.astate; lock: bool; ownership_precondition: Precondition.t} + [@@deriving compare] val make : LocksDomain.astate -> ThreadsDomain.astate -> Precondition.t -> Procdesc.t -> t