From 94afd8446c8f16a12787e00fedcc7a0fd0570375 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 21 Mar 2017 15:31:46 -0700 Subject: [PATCH] [thread-safety] rename protectedif -> unprotected Reviewed By: peterogithub Differential Revision: D4740726 fbshipit-source-id: 4b957b9 --- infer/src/checkers/ThreadSafety.ml | 14 +++++++------- infer/src/checkers/ThreadSafetyDomain.ml | 8 ++++---- infer/src/checkers/ThreadSafetyDomain.mli | 7 ++++--- 3 files changed, 15 insertions(+), 14 deletions(-) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 56e9de362..30120e556 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -230,7 +230,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct then match get_formal_index base_exp typ with | Some formal_index -> - let pre = AccessPrecondition.ProtectedIf (Some formal_index) in + let pre = AccessPrecondition.Unprotected (Some formal_index) in let conditional_accesses_for_pre = add_path_to_state access_kind @@ -369,7 +369,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match AccessPath.of_lhs_exp dummy_access_exp receiver_typ ~f_resolve_id with | Some container_ap -> AccessDomain.add_access - (ProtectedIf (Some 0)) + (Unprotected (Some 0)) (make_access container_ap Write callee_loc) AccessDomain.empty | None -> @@ -491,7 +491,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Some formal_index -> (* the actual passed to the current callee is rooted in a formal *) - AccessPrecondition.ProtectedIf (Some formal_index) + AccessPrecondition.Unprotected (Some formal_index) | None -> match AttributeMapDomain.get_conditional_ownership_index @@ -501,7 +501,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Some formal_index -> (* access path conditionally owned if [formal_index] is owned *) - AccessPrecondition.ProtectedIf (Some formal_index) + AccessPrecondition.Unprotected (Some formal_index) | None -> (* access path not rooted in a formal and not conditionally owned *) @@ -518,13 +518,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let update_accesses pre callee_accesses accesses_acc = match pre with | AccessPrecondition.Protected -> update_caller_accesses pre callee_accesses accesses_acc - | AccessPrecondition.ProtectedIf None -> + | AccessPrecondition.Unprotected None -> let pre' = if unprotected then pre else AccessPrecondition.Protected in update_caller_accesses pre' callee_accesses accesses_acc - | AccessPrecondition.ProtectedIf (Some index) -> + | AccessPrecondition.Unprotected (Some index) -> add_ownership_access callee_accesses (List.nth_exn actuals index) accesses_acc in AccessDomain.fold update_accesses callee_accesses astate.accesses in @@ -944,7 +944,7 @@ let get_possibly_unsafe_accesses access_kind accesses = let open ThreadSafetyDomain in AccessDomain.fold (fun pre trace acc -> match pre with - | ProtectedIf _ -> PathDomain.join (filter_by_kind access_kind trace) acc + | Unprotected _ -> PathDomain.join (filter_by_kind access_kind trace) acc | Protected -> acc) accesses PathDomain.empty diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 2fbfc434a..eb4aba869 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -152,15 +152,15 @@ end module AccessPrecondition = struct type t = | Protected - | ProtectedIf of int option + | Unprotected of int option [@@deriving compare] - let unprotected = ProtectedIf None + let unprotected = Unprotected None let pp fmt = function | Protected -> F.fprintf fmt "Protected" - | ProtectedIf (Some index) -> F.fprintf fmt "ProtectedIf %d" index - | ProtectedIf None -> F.fprintf fmt "Unprotected" + | Unprotected (Some index) -> F.fprintf fmt "Unproctected(%d)" index + | Unprotected None -> F.fprintf fmt "Unprotected" module Map = PrettyPrintable.MakePPMap(struct type nonrec t = t diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index 7f56082be..165298375 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -91,9 +91,10 @@ module AccessPrecondition : sig type t = | Protected (** access safe due to held lock (i.e., pre is true *) - | ProtectedIf of int option - (** access safe if the formal at index i is owned (i.e., pre is owned(i)). - ProtectedIf None means unsafe (i.e., pre is false) *) + | Unprotected of int option + (** access rooted in formal at index i. Safe if actual passed at index is owned (i.e., + !owned(i) implies an unsafe access). Unprotected None means the access is unsafe unless a + lock is held in the caller *) [@@deriving compare] (** type of an unprotected access *)