From cfd9802d894318a2f6cfa2e796f5ad53160f269e Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 23 Apr 2018 13:51:11 -0700 Subject: [PATCH] [racerd] `Precondition` -> `OwnershipPrecondition` Reviewed By: jeremydubreil Differential Revision: D7718403 fbshipit-source-id: 73c5cee --- infer/src/concurrency/RacerD.ml | 13 +++++++------ infer/src/concurrency/RacerDDomain.ml | 14 +++++++------- infer/src/concurrency/RacerDDomain.mli | 17 +++++++++-------- 3 files changed, 23 insertions(+), 21 deletions(-) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 5502664b0..ba3aa142e 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -170,7 +170,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | OwnershipAbstractValue.OwnedIf formal_indexes -> let pre = AccessSnapshot.make locks threads - (AccessSnapshot.Precondition.Conjunction formal_indexes) proc_data.pdesc + (AccessSnapshot.OwnershipPrecondition.Conjunction formal_indexes) + proc_data.pdesc in add_field_access pre | OwnershipAbstractValue.Owned -> @@ -227,7 +228,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in let pre = AccessSnapshot.make astate.locks astate.threads - (AccessSnapshot.Precondition.Conjunction (IntSet.singleton 0)) caller_pdesc + (AccessSnapshot.OwnershipPrecondition.Conjunction (IntSet.singleton 0)) caller_pdesc in AccessDomain.add_access pre container_access AccessDomain.empty in @@ -328,7 +329,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in AccessDomain.add pre combined_accesses caller_accesses in - let conjoin_ownership_pre actual_exp actual_indexes : AccessSnapshot.Precondition.t = + let conjoin_ownership_pre actual_exp actual_indexes : AccessSnapshot.OwnershipPrecondition.t = match actual_exp with | HilExp.Constant _ -> (* the actual is a constant, so it's owned in the caller. *) @@ -360,7 +361,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (* couldn't find access path, don't know if it's owned. assume not *) False in - let update_ownership_pre actual_index (acc: AccessSnapshot.Precondition.t) = + let update_ownership_pre actual_index (acc: AccessSnapshot.OwnershipPrecondition.t) = match acc with | False -> (* precondition can't be satisfied *) @@ -379,12 +380,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let ownership_precondition' = match pre.ownership_precondition with | Conjunction indexes -> - let empty_pre = AccessSnapshot.Precondition.Conjunction IntSet.empty in + let empty_pre = AccessSnapshot.OwnershipPrecondition.Conjunction IntSet.empty in IntSet.fold update_ownership_pre indexes empty_pre | False -> pre.ownership_precondition in - if AccessSnapshot.Precondition.is_true ownership_precondition' then accesses_acc + if AccessSnapshot.OwnershipPrecondition.is_true ownership_precondition' then accesses_acc else let locks' = if pre.lock then LocksDomain.add_lock locks else locks in (* if the access occurred on a main thread in the callee, we should remember this when diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 97e29337d..405e6bdb0 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -404,7 +404,7 @@ module AttributeMapDomain = struct end module AccessSnapshot = struct - module Precondition = struct + module OwnershipPrecondition = struct type t = Conjunction of IntSet.t | False [@@deriving compare] (* precondition is true if the conjunction of owned indexes is empty *) @@ -420,25 +420,25 @@ module AccessSnapshot = struct end type t = - {thread: ThreadsDomain.astate; lock: bool; ownership_precondition: Precondition.t} - [@@deriving compare] + {thread: ThreadsDomain.astate; lock: bool; ownership_precondition: OwnershipPrecondition.t} + [@@deriving compare] 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)) ; + assert (not (OwnershipPrecondition.is_true ownership_precondition)) ; let lock = LocksDomain.is_locked lock || Procdesc.is_java_synchronized pdesc in {thread; lock; ownership_precondition} let is_unprotected {thread; lock; ownership_precondition} = not (ThreadsDomain.is_any_but_self thread) && not lock - && not (Precondition.is_true ownership_precondition) + && not (OwnershipPrecondition.is_true ownership_precondition) let pp fmt {thread; lock; ownership_precondition} = - F.fprintf fmt "Thread: %a Lock: %b Pre: %a" ThreadsDomain.pp thread lock Precondition.pp - ownership_precondition + F.fprintf fmt "Thread: %a Lock: %b Pre: %a" ThreadsDomain.pp thread lock + OwnershipPrecondition.pp ownership_precondition end module AccessDomain = struct diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index a67bbc94c..e6f5d545d 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -78,11 +78,11 @@ module ThreadsDomain : sig assume this by default unless we see evidence to the contrary (annotations, use of locks, etc.) *) | AnyThreadButSelf - (** Current thread can run in parallel with other threads, but not with itself. + (** Current thread can run in parallel with other threads, but not with a copy of itself. (concretization : { t | t \in TIDs ^ t != t_cur } ) *) | AnyThread - (** Current thread can run in parallel with any thread, including itself (concretization: set - of all TIDs ) *) + (** Current thread can run in parallel with any thread, including itself (concretization: + set of all TIDs ) *) include AbstractDomain.WithBottom with type astate := astate @@ -158,10 +158,10 @@ module AttributeMapDomain : sig val add_attribute : AccessPath.t -> Attribute.t -> astate -> astate end -(** Data shared among a set of accesses: current thread, lock(s) held, ownership precondition *) +(** snapshot of the relevant state at the time of a heap access: concurrent thread(s), lock(s) held, ownership precondition *) module AccessSnapshot : sig - (** Precondition for owned access; access is owned if it evaluates to ture *) - module Precondition : sig + (** precondition for owned access; access is owned if it evaluates to true *) + module OwnershipPrecondition : sig type t = | Conjunction of IntSet.t (** Conjunction of "formal index must be owned" predicates. @@ -176,10 +176,11 @@ module AccessSnapshot : sig end type t = private - {thread: ThreadsDomain.astate; lock: bool; ownership_precondition: Precondition.t} + {thread: ThreadsDomain.astate; lock: bool; ownership_precondition: OwnershipPrecondition.t} [@@deriving compare] - val make : LocksDomain.astate -> ThreadsDomain.astate -> Precondition.t -> Procdesc.t -> t + val make : + LocksDomain.astate -> ThreadsDomain.astate -> OwnershipPrecondition.t -> Procdesc.t -> t val is_unprotected : t -> bool (** return true if not protected by lock, thread, or ownership *)