From 0f74016ef51efd3c4e0f9d016798287554a5b173 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 9 Mar 2017 11:36:36 -0800 Subject: [PATCH] [thread-safety] add callee write as protected-if if it's conditionally owned in caller Reviewed By: peterogithub Differential Revision: D4660606 fbshipit-source-id: 8e523c9 --- infer/src/checkers/ThreadSafety.ml | 33 +++++++++++---- infer/src/checkers/ThreadSafetyDomain.ml | 11 +++++ infer/src/checkers/ThreadSafetyDomain.mli | 3 ++ .../java/threadsafety/Ownership.java | 40 +++++++++++++++++++ .../java/threadsafety/issues.exp | 2 + 5 files changed, 81 insertions(+), 8 deletions(-) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 481c95b98..36442eca5 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -456,7 +456,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct if is_owned actual_access_path astate.attribute_map then (* the actual passed to the current callee is owned. drop all the - conditional writes for that actual, since they're all safe *) + conditional accesses for that actual, since they're all safe *) accesses_acc else let base = fst actual_access_path in @@ -464,19 +464,36 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match FormalMap.get_formal_index base extras with | Some formal_index -> (* the actual passed to the current callee is rooted in a - formal. add to conditional writes *) + formal. add to conditional accesses *) PathDomain.Sinks.fold (AccessDomain.add_access (ProtectedIf (Some formal_index))) (PathDomain.sinks callee_conditional_accesses) accesses_acc | None -> - (* access path not owned and not rooted in a formal. add to - unsafe writes *) - PathDomain.Sinks.fold - (AccessDomain.add_access AccessPrecondition.unprotected) - (PathDomain.sinks callee_conditional_accesses) - accesses_acc + begin + match + AttributeMapDomain.get_conditional_ownership_index + actual_access_path + astate.attribute_map + with + |(Some formal_index) -> + (* access path conditionally owned, add to + protected-if accesses *) + PathDomain.Sinks.fold + (AccessDomain.add_access + (ProtectedIf (Some formal_index))) + (PathDomain.sinks callee_conditional_accesses) + accesses_acc + | None -> + (* access path not owned and not rooted in a formal. + add to unprotected accesses *) + PathDomain.Sinks.fold + (AccessDomain.add_access + AccessPrecondition.unprotected) + (PathDomain.sinks callee_conditional_accesses) + accesses_acc + end end | None -> PathDomain.Sinks.fold diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index e66e9947f..add84e93c 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -102,6 +102,17 @@ module AttributeMapDomain = struct with Not_found -> false + let get_conditional_ownership_index access_path t = + try + let attributes = find access_path t in + (List.find_map + ~f:(function + | Attribute.OwnedIf ((Some _) as formal_index_opt) -> formal_index_opt + | _ -> None) + (AttributeSetDomain.elements attributes)) + with Not_found -> + None + let add_attribute access_path attribute t = let attribute_set = (try find access_path t diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index da52f326a..c6d61f4c2 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -64,6 +64,9 @@ module AttributeMapDomain : sig val has_attribute : AccessPath.Raw.t -> Attribute.t -> astate -> bool + (** get the formal index of the the formal that must own the given access path (if any) *) + val get_conditional_ownership_index : AccessPath.Raw.t -> astate -> int option + val add_attribute : AccessPath.Raw.t -> Attribute.t -> astate -> astate end diff --git a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java index c6a06c755..c860768a3 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java +++ b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java @@ -307,4 +307,44 @@ public class Ownership { Obj notOwned = leakThenReturn(); notOwned.f = new Object(); // should warn here } + + private void castThenCall(Obj o) { + Subclass s = (Subclass) o; + s.doWrite(); + } + + void castThenCallOk() { + Obj o = new Obj(); + castThenCall(o); + } + + void castThenCallBad() { + Obj o = getMaybeUnownedObj(); + castThenCall(o); + } + + private Obj castThenReturn(Obj o) { + Subclass s = (Subclass) o; + return s; + } + + void castThenReturnOk() { + Obj o = new Obj(); + castThenReturn(o).f = new Object(); + } + + void castThenReturnBad() { + Obj o = getMaybeUnownedObj(); + castThenReturn(o).f = new Object(); + } + +} + + +class Subclass extends Obj { + + public void doWrite() { + f = new Object(); + } + } diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index 40910a6e1..70d1dc3c8 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -42,6 +42,8 @@ codetoanalyze/java/threadsafety/Locks.java, void Locks.lockInOneBranchBad(boolea codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_ownAndConditionalOwnOk(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_twoDifferentConditionalOwnsOk(), 4, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.cantOwnThisBad(), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.setField(Obj),access to codetoanalyze.java.checkers.Ownership.field] +codetoanalyze/java/threadsafety/Ownership.java, void Ownership.castThenCallBad(), 2, THREAD_SAFETY_VIOLATION, [call to void Ownership.castThenCall(Obj),call to void Subclass.doWrite(),access to codetoanalyze.java.checkers.Obj.f] +codetoanalyze/java/threadsafety/Ownership.java, void Ownership.castThenReturnBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.notOwnedInCalleeBad(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.mutateIfNotNull(Obj),access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.ownInOneBranchBad(Obj,boolean), 5, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.reassignToFormalBad(Obj), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.g]