[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

@@ -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

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

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
 

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();
+  }
+
 }

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]